(set-option :backend none)
; arity 2
(declare-datatype Color ( ( red ) ( green ) ))
; arity 2
(declare-fun mix (Color Color) Color)
(x-interpret-fun mix
(x-mapping
((green green) red)
((red green) green)
((green red) green)
)
? )
(assert (= green (mix red green)))
(assert (exists ((x Color)) (= (mix x x) x)))
(x-ground :debug :sql)
(x-debug solver functions)
(x-debug solver groundings)
(x-debug db tables)
(x-debug db _xmt_interp_mix_g)
------- RESULTS ------------------
(declare-datatype Color ((red) (green)))
(declare-fun mix (Color Color) Color)
; ==== Query =============================
;-- exclude(0)
;SELECT *
; FROM (-- Join(7)
; SELECT eq_("green", _xmt_interp_mix_G_2.G) AS G
; FROM _xmt_interp_mix_G AS _xmt_interp_mix_G_2
; WHERE (NOT is_id(_xmt_interp_mix_G_2.G) OR _xmt_interp_mix_G_2.G != "green")
; AND "red" = _xmt_interp_mix_G_2.a_1
; AND "green" = _xmt_interp_mix_G_2.a_2)
; WHERE G <> "true"
; ==== Query =============================
;-- exclude(0)
;SELECT *
; FROM (-- Agg (7)
; SELECT or_aggregate(G) as G
; FROM (SELECT NULL AS x, "false" AS G
; UNION ALL
; -- exclude(14)
; SELECT *
; FROM (-- Join(21)
; SELECT _xmt_interp_mix_G_5.a_1 AS x,
; eq_(_xmt_interp_mix_G_5.G, _xmt_interp_mix_G_5.a_1) AS G
; FROM _xmt_interp_mix_G AS _xmt_interp_mix_G_5
; WHERE (NOT is_id(_xmt_interp_mix_G_5.G) OR _xmt_interp_mix_G_5.G = _xmt_interp_mix_G_5.a_1)
; AND _xmt_interp_mix_G_5.a_1 = _xmt_interp_mix_G_5.a_2)
; WHERE G <> "false"))
; WHERE G <> "true"(assert (= (mix red red) red))
Functions2:
- true ()->Bool : Constructor
- false ()->Bool : Constructor
- not ()->Bool : Predefined (true)
- => ()->Bool : Predefined (true)
- and ()->Bool : Predefined (true)
- or ()->Bool : Predefined (true)
- xor ()->Bool : Predefined (true)
- = ()->Bool : Predefined (true)
- distinct ()->Bool : Predefined (true)
- <= ()->Bool : Predefined (true)
- < ()->Bool : Predefined (true)
- >= ()->Bool : Predefined (true)
- > ()->Bool : Predefined (true)
- ite ()->Bool : Predefined (?)
- let ()->Bool : Predefined (?)
- + ()->Real : Predefined (false)
- - ()->Real : Predefined (false)
- * ()->Real : Predefined (false)
- div ()->Real : Predefined (false)
- mod ()->Real : Predefined (false)
- abs ()->Real : Predefined (false)
- red ()->Color : Constructor
- green ()->Color : Constructor
- (_ is red) (Color)->Bool : Predefined (true)
- (_ is green) (Color)->Bool : Predefined (true)
- mix (Color, Color)->Color : Non Boolean (_xmt_interp_mix_G Partial)
Groundings:
=== green ======================================
-- Join(0)
SELECT "green" AS G
=== red ======================================
-- Join(0)
SELECT "red" AS G
=== (mix red green) ======================================
-- Join(0)
SELECT _xmt_interp_mix_G_2.G AS G
FROM _xmt_interp_mix_G AS _xmt_interp_mix_G_2
WHERE "red" = _xmt_interp_mix_G_2.a_1
AND "green" = _xmt_interp_mix_G_2.a_2
=== (top) (= green (mix red green)) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT eq_("green", _xmt_interp_mix_G_2.G) AS G
FROM _xmt_interp_mix_G AS _xmt_interp_mix_G_2
WHERE (NOT is_id(_xmt_interp_mix_G_2.G) OR _xmt_interp_mix_G_2.G = "green")
AND "red" = _xmt_interp_mix_G_2.a_1
AND "green" = _xmt_interp_mix_G_2.a_2
----- UF -----------------------------------------------------------
-- Join(0)
SELECT eq_("green", _xmt_interp_mix_G_2.G) AS G
FROM _xmt_interp_mix_G AS _xmt_interp_mix_G_2
WHERE (NOT is_id(_xmt_interp_mix_G_2.G) OR _xmt_interp_mix_G_2.G != "green")
AND "red" = _xmt_interp_mix_G_2.a_1
AND "green" = _xmt_interp_mix_G_2.a_2
----- G ------------------------------------------------------------
-- Join(0)
SELECT eq_("green", _xmt_interp_mix_G_2.G) AS G
FROM _xmt_interp_mix_G AS _xmt_interp_mix_G_2
WHERE "red" = _xmt_interp_mix_G_2.a_1
AND "green" = _xmt_interp_mix_G_2.a_2
=== x ======================================
-- Join(0)
SELECT _xmt_sort_color_4.G AS x,
_xmt_sort_color_4.G AS G
FROM _xmt_sort_color AS _xmt_sort_color_4
=== (mix x x) ======================================
-- Join(0)
SELECT _xmt_interp_mix_G_5.a_1 AS x,
_xmt_interp_mix_G_5.G AS G
FROM _xmt_interp_mix_G AS _xmt_interp_mix_G_5
WHERE _xmt_interp_mix_G_5.a_1 = _xmt_interp_mix_G_5.a_2
=== (= (mix x x) x) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_mix_G_5.a_1 AS x,
eq_(_xmt_interp_mix_G_5.G, _xmt_interp_mix_G_5.a_1) AS G
FROM _xmt_interp_mix_G AS _xmt_interp_mix_G_5
WHERE (NOT is_id(_xmt_interp_mix_G_5.G) OR _xmt_interp_mix_G_5.G = _xmt_interp_mix_G_5.a_1)
AND _xmt_interp_mix_G_5.a_1 = _xmt_interp_mix_G_5.a_2
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_mix_G_5.a_1 AS x,
eq_(_xmt_interp_mix_G_5.G, _xmt_interp_mix_G_5.a_1) AS G
FROM _xmt_interp_mix_G AS _xmt_interp_mix_G_5
WHERE (NOT is_id(_xmt_interp_mix_G_5.G) OR _xmt_interp_mix_G_5.G != _xmt_interp_mix_G_5.a_1)
AND _xmt_interp_mix_G_5.a_1 = _xmt_interp_mix_G_5.a_2
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_mix_G_5.a_1 AS x,
eq_(_xmt_interp_mix_G_5.G, _xmt_interp_mix_G_5.a_1) AS G
FROM _xmt_interp_mix_G AS _xmt_interp_mix_G_5
WHERE _xmt_interp_mix_G_5.a_1 = _xmt_interp_mix_G_5.a_2
=== (top) (exists ((x Color)) (= (mix x x) x)) ======================================
----- TU -----------------------------------------------------------
-- Agg (0)
SELECT or_aggregate(G) as G
FROM (-- exclude(7)
SELECT *
FROM (-- Join(14)
SELECT _xmt_interp_mix_G_5.a_1 AS x,
eq_(_xmt_interp_mix_G_5.G, _xmt_interp_mix_G_5.a_1) AS G
FROM _xmt_interp_mix_G AS _xmt_interp_mix_G_5
WHERE (NOT is_id(_xmt_interp_mix_G_5.G) OR _xmt_interp_mix_G_5.G = _xmt_interp_mix_G_5.a_1)
AND _xmt_interp_mix_G_5.a_1 = _xmt_interp_mix_G_5.a_2)
WHERE G <> "false")
----- UF -----------------------------------------------------------
-- Agg (0)
SELECT or_aggregate(G) as G
FROM (SELECT NULL AS x, "false" AS G
UNION ALL
-- exclude(7)
SELECT *
FROM (-- Join(14)
SELECT _xmt_interp_mix_G_5.a_1 AS x,
eq_(_xmt_interp_mix_G_5.G, _xmt_interp_mix_G_5.a_1) AS G
FROM _xmt_interp_mix_G AS _xmt_interp_mix_G_5
WHERE (NOT is_id(_xmt_interp_mix_G_5.G) OR _xmt_interp_mix_G_5.G = _xmt_interp_mix_G_5.a_1)
AND _xmt_interp_mix_G_5.a_1 = _xmt_interp_mix_G_5.a_2)
WHERE G <> "false")
----- G ------------------------------------------------------------
-- Agg (0)
SELECT or_aggregate(G) as G
FROM (SELECT NULL AS x, "false" AS G
UNION ALL
-- exclude(7)
SELECT *
FROM (-- Join(14)
SELECT _xmt_interp_mix_G_5.a_1 AS x,
eq_(_xmt_interp_mix_G_5.G, _xmt_interp_mix_G_5.a_1) AS G
FROM _xmt_interp_mix_G AS _xmt_interp_mix_G_5
WHERE (NOT is_id(_xmt_interp_mix_G_5.G) OR _xmt_interp_mix_G_5.G = _xmt_interp_mix_G_5.a_1)
AND _xmt_interp_mix_G_5.a_1 = _xmt_interp_mix_G_5.a_2)
WHERE G <> "false")
===========================================
Tables and Views:
- Bool (table)
- _xmt_sort_color (table)
- _xmt_interp_mix_K (table)
- _xmt_interp_mix_U (view)
- _xmt_interp_mix_G (view)
- sqlite_stat1 (table)
- sqlite_stat4 (table)
TABLE: _xmt_interp_mix_g
┌─────────┬─────────┬─────────────────┐
│ a_1 │ a_2 │ G │
├─────────┼─────────┼─────────────────┤
│ "green" │ "green" │ "red" │
├─────────┼─────────┼─────────────────┤
│ "green" │ "red" │ "green" │
├─────────┼─────────┼─────────────────┤
│ "red" │ "green" │ "green" │
├─────────┼─────────┼─────────────────┤
│ "red" │ "red" │ "(mix red red)" │
└─────────┴─────────┴─────────────────┘