(set-option :backend none)
(declare-datatype Node ( (a) (b) ))
(declare-datatype Color ( (red) (green) (blue) ))
(declare-fun edge (Node Node) Bool)
(declare-fun keep (Node) Bool)
(declare-fun kept_edge (Node Node) Bool)
(declare-fun color (Node) Color)
(assert (forall ((x Node) (y Node))
(or (keep x) (keep y) (= x y))))
(assert (forall ((x Node) (y Node))
(= (kept_edge x y)
(and (keep x) (keep y) (edge x y)))))
(assert (forall ((x Node) (y Node))
(=> (kept_edge x y)
(not (= (color x) (color y))))))
(assert (forall ((x Node))
(=> (not (keep x))
(= (color x) red))))
(x-interpret-pred edge (x-set (a b)))
(x-ground :debug :sql)
(x-debug solver groundings)
------- RESULTS ------------------
(declare-datatype Node ((a) (b)))
(declare-datatype Color ((red) (green) (blue)))
(declare-fun edge (Node Node) Bool)
(declare-fun keep (Node) Bool)
(declare-fun kept_edge (Node Node) Bool)
(declare-fun color (Node) Color)
; ==== Query =============================
;-- Agg (0)
;SELECT G as G
; FROM (-- Join(7)
; SELECT _xmt_sort_node.G AS x,
; _xmt_sort_node_2.G AS y,
; or_(apply("keep", _xmt_sort_node.G), apply("keep", _xmt_sort_node_2.G), eq_(_xmt_sort_node.G, _xmt_sort_node_2.G)) AS G
; FROM _xmt_sort_node
; JOIN _xmt_sort_node AS _xmt_sort_node_2
; WHERE _xmt_sort_node.G != _xmt_sort_node_2.G)(assert (or (keep a) (keep b)))
(assert (or (keep b) (keep a)))
; ==== Query =============================
;-- Agg (0)
;SELECT G as G
; FROM (-- Join(7)
; SELECT _xmt_interp_edge_G_8.a_1 AS x,
; _xmt_interp_edge_G_8.a_2 AS y,
; apply("=", apply("kept_edge", _xmt_interp_edge_G_8.a_1, _xmt_interp_edge_G_8.a_2), and_(apply("keep", _xmt_interp_edge_G_8.a_1), apply("keep", _xmt_interp_edge_G_8.a_2), _xmt_interp_edge_G_8.G)) AS G
; FROM _xmt_interp_edge_G AS _xmt_interp_edge_G_8)(assert (= (kept_edge a a) false))
(assert (= (kept_edge a b) (and (keep a) (keep b))))
(assert (= (kept_edge b a) false))
(assert (= (kept_edge b b) false))
; ==== Query =============================
;-- Agg (0)
;SELECT G as G
; FROM (-- Join(7)
; SELECT _xmt_sort_node.G AS x,
; _xmt_sort_node_2.G AS y,
; or_(apply("not", apply("kept_edge", _xmt_sort_node.G, _xmt_sort_node_2.G)), apply("not", apply("=", apply("color", _xmt_sort_node.G), apply("color", _xmt_sort_node_2.G)))) AS G
; FROM _xmt_sort_node
; JOIN _xmt_sort_node AS _xmt_sort_node_2)(assert (or (not (kept_edge a a)) (not (= (color a) (color a)))))
(assert (or (not (kept_edge a b)) (not (= (color a) (color b)))))
(assert (or (not (kept_edge b a)) (not (= (color b) (color a)))))
(assert (or (not (kept_edge b b)) (not (= (color b) (color b)))))
; ==== Query =============================
;-- Agg (0)
;SELECT G as G
; FROM (-- Join(7)
; SELECT _xmt_sort_node.G AS x,
; or_(apply("not", apply("not", apply("keep", _xmt_sort_node.G))), apply("=", apply("color", _xmt_sort_node.G), "red")) AS G
; FROM _xmt_sort_node)(assert (or (not (not (keep a))) (= (color a) red)))
(assert (or (not (not (keep b))) (= (color b) red)))
Groundings:
=== x ======================================
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node.G AS G
FROM _xmt_sort_node
=== (keep x) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
apply("keep", _xmt_sort_node.G) AS G
FROM _xmt_sort_node
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
apply("keep", _xmt_sort_node.G) AS G
FROM _xmt_sort_node
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
apply("keep", _xmt_sort_node.G) AS G
FROM _xmt_sort_node
=== y ======================================
-- Join(0)
SELECT _xmt_sort_node_2.G AS y,
_xmt_sort_node_2.G AS G
FROM _xmt_sort_node AS _xmt_sort_node_2
=== (keep y) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node_2.G AS y,
apply("keep", _xmt_sort_node_2.G) AS G
FROM _xmt_sort_node AS _xmt_sort_node_2
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node_2.G AS y,
apply("keep", _xmt_sort_node_2.G) AS G
FROM _xmt_sort_node AS _xmt_sort_node_2
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node_2.G AS y,
apply("keep", _xmt_sort_node_2.G) AS G
FROM _xmt_sort_node AS _xmt_sort_node_2
=== (= x y) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
eq_(_xmt_sort_node.G, _xmt_sort_node_2.G) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
WHERE _xmt_sort_node.G = _xmt_sort_node_2.G
----- F ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
eq_(_xmt_sort_node.G, _xmt_sort_node_2.G) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
WHERE _xmt_sort_node.G != _xmt_sort_node_2.G
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
eq_(_xmt_sort_node.G, _xmt_sort_node_2.G) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
=== (or (keep x) (keep y) (= x y)) ======================================
----- T ------------------------------------------------------------
-- Agg (0)
SELECT x, y,
or_aggregate(G) as G
FROM (-- exclude(7)
SELECT *
FROM (-- Join(14)
SELECT _xmt_view_keep_1_4.x AS x,
_xmt_sort_node_2.G AS y,
_xmt_view_keep_1_4.G AS G
FROM (-- Join(22)
SELECT _xmt_sort_node.G AS x,
apply("keep", _xmt_sort_node.G) AS G
FROM _xmt_sort_node
) AS _xmt_view_keep_1_4
JOIN _xmt_sort_node AS _xmt_sort_node_2
UNION ALL
-- Join(14)
SELECT _xmt_sort_node.G AS x,
_xmt_view_keep_3_7.y AS y,
_xmt_view_keep_3_7.G AS G
FROM (-- Join(22)
SELECT _xmt_sort_node_2.G AS y,
apply("keep", _xmt_sort_node_2.G) AS G
FROM _xmt_sort_node AS _xmt_sort_node_2
) AS _xmt_view_keep_3_7
JOIN _xmt_sort_node
UNION ALL
-- Join(14)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
eq_(_xmt_sort_node.G, _xmt_sort_node_2.G) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
WHERE _xmt_sort_node.G = _xmt_sort_node_2.G)
WHERE G <> "false")
GROUP BY x, y
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
or_(apply("keep", _xmt_sort_node.G), apply("keep", _xmt_sort_node_2.G), eq_(_xmt_sort_node.G, _xmt_sort_node_2.G)) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
WHERE _xmt_sort_node.G != _xmt_sort_node_2.G
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
or_(apply("keep", _xmt_sort_node.G), apply("keep", _xmt_sort_node_2.G), eq_(_xmt_sort_node.G, _xmt_sort_node_2.G)) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
=== (top) (forall ((x Node) (y Node)) (or (keep x) (keep y) (= x y))) ======================================
----- TU -----------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, NULL AS y, "true" AS G
UNION ALL
-- Join(7)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
or_(apply("keep", _xmt_sort_node.G), apply("keep", _xmt_sort_node_2.G), eq_(_xmt_sort_node.G, _xmt_sort_node_2.G)) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
WHERE _xmt_sort_node.G != _xmt_sort_node_2.G)
----- UF -----------------------------------------------------------
-- Agg (0)
SELECT G as G
FROM (-- Join(7)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
or_(apply("keep", _xmt_sort_node.G), apply("keep", _xmt_sort_node_2.G), eq_(_xmt_sort_node.G, _xmt_sort_node_2.G)) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
WHERE _xmt_sort_node.G != _xmt_sort_node_2.G)
----- G ------------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, NULL AS y, "true" AS G
UNION ALL
-- Join(7)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
or_(apply("keep", _xmt_sort_node.G), apply("keep", _xmt_sort_node_2.G), eq_(_xmt_sort_node.G, _xmt_sort_node_2.G)) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
WHERE _xmt_sort_node.G != _xmt_sort_node_2.G)
=== (kept_edge x y) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
apply("kept_edge", _xmt_sort_node.G, _xmt_sort_node_2.G) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
apply("kept_edge", _xmt_sort_node.G, _xmt_sort_node_2.G) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
apply("kept_edge", _xmt_sort_node.G, _xmt_sort_node_2.G) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
=== (edge x y) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_TU_8.a_1 AS x,
_xmt_interp_edge_TU_8.a_2 AS y,
"true" AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_8
----- F ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_UF_8.a_1 AS x,
_xmt_interp_edge_UF_8.a_2 AS y,
"false" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_8
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_G_8.a_1 AS x,
_xmt_interp_edge_G_8.a_2 AS y,
_xmt_interp_edge_G_8.G AS G
FROM _xmt_interp_edge_G AS _xmt_interp_edge_G_8
=== (and (keep x) (keep y) (edge x y)) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_TU_8.a_1 AS x,
_xmt_interp_edge_TU_8.a_2 AS y,
and_(apply("keep", _xmt_interp_edge_TU_8.a_1), apply("keep", _xmt_interp_edge_TU_8.a_2)) AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_8
----- F ------------------------------------------------------------
-- Agg (0)
SELECT x, y,
and_aggregate(G) as G
FROM (-- exclude(7)
SELECT *
FROM (-- Join(14)
SELECT _xmt_view_keep_1_5.x AS x,
_xmt_sort_node_2.G AS y,
_xmt_view_keep_1_5.G AS G
FROM (-- Join(22)
SELECT _xmt_sort_node.G AS x,
apply("keep", _xmt_sort_node.G) AS G
FROM _xmt_sort_node
) AS _xmt_view_keep_1_5
JOIN _xmt_sort_node AS _xmt_sort_node_2
UNION ALL
-- Join(14)
SELECT _xmt_sort_node.G AS x,
_xmt_view_keep_3_8.y AS y,
_xmt_view_keep_3_8.G AS G
FROM (-- Join(22)
SELECT _xmt_sort_node_2.G AS y,
apply("keep", _xmt_sort_node_2.G) AS G
FROM _xmt_sort_node AS _xmt_sort_node_2
) AS _xmt_view_keep_3_8
JOIN _xmt_sort_node
UNION ALL
-- Join(14)
SELECT _xmt_interp_edge_UF_8.a_1 AS x,
_xmt_interp_edge_UF_8.a_2 AS y,
"false" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_8)
WHERE G <> "true")
GROUP BY x, y
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_G_8.a_1 AS x,
_xmt_interp_edge_G_8.a_2 AS y,
and_(apply("keep", _xmt_interp_edge_G_8.a_1), apply("keep", _xmt_interp_edge_G_8.a_2), _xmt_interp_edge_G_8.G) AS G
FROM _xmt_interp_edge_G AS _xmt_interp_edge_G_8
=== (= (kept_edge x y) (and (keep x) (keep y) (edge x y))) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_G_8.a_1 AS x,
_xmt_interp_edge_G_8.a_2 AS y,
apply("=", apply("kept_edge", _xmt_interp_edge_G_8.a_1, _xmt_interp_edge_G_8.a_2), and_(apply("keep", _xmt_interp_edge_G_8.a_1), apply("keep", _xmt_interp_edge_G_8.a_2), _xmt_interp_edge_G_8.G)) AS G
FROM _xmt_interp_edge_G AS _xmt_interp_edge_G_8
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_G_8.a_1 AS x,
_xmt_interp_edge_G_8.a_2 AS y,
apply("=", apply("kept_edge", _xmt_interp_edge_G_8.a_1, _xmt_interp_edge_G_8.a_2), and_(apply("keep", _xmt_interp_edge_G_8.a_1), apply("keep", _xmt_interp_edge_G_8.a_2), _xmt_interp_edge_G_8.G)) AS G
FROM _xmt_interp_edge_G AS _xmt_interp_edge_G_8
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_G_8.a_1 AS x,
_xmt_interp_edge_G_8.a_2 AS y,
apply("=", apply("kept_edge", _xmt_interp_edge_G_8.a_1, _xmt_interp_edge_G_8.a_2), and_(apply("keep", _xmt_interp_edge_G_8.a_1), apply("keep", _xmt_interp_edge_G_8.a_2), _xmt_interp_edge_G_8.G)) AS G
FROM _xmt_interp_edge_G AS _xmt_interp_edge_G_8
=== (top) (forall ((x Node) (y Node)) (= (kept_edge x y) (and (keep x) (keep y) (edge x y)))) ======================================
----- TU -----------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, NULL AS y, "true" AS G
UNION ALL
-- Join(7)
SELECT _xmt_interp_edge_G_8.a_1 AS x,
_xmt_interp_edge_G_8.a_2 AS y,
apply("=", apply("kept_edge", _xmt_interp_edge_G_8.a_1, _xmt_interp_edge_G_8.a_2), and_(apply("keep", _xmt_interp_edge_G_8.a_1), apply("keep", _xmt_interp_edge_G_8.a_2), _xmt_interp_edge_G_8.G)) AS G
FROM _xmt_interp_edge_G AS _xmt_interp_edge_G_8)
----- UF -----------------------------------------------------------
-- Agg (0)
SELECT G as G
FROM (-- Join(7)
SELECT _xmt_interp_edge_G_8.a_1 AS x,
_xmt_interp_edge_G_8.a_2 AS y,
apply("=", apply("kept_edge", _xmt_interp_edge_G_8.a_1, _xmt_interp_edge_G_8.a_2), and_(apply("keep", _xmt_interp_edge_G_8.a_1), apply("keep", _xmt_interp_edge_G_8.a_2), _xmt_interp_edge_G_8.G)) AS G
FROM _xmt_interp_edge_G AS _xmt_interp_edge_G_8)
----- G ------------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, NULL AS y, "true" AS G
UNION ALL
-- Join(7)
SELECT _xmt_interp_edge_G_8.a_1 AS x,
_xmt_interp_edge_G_8.a_2 AS y,
apply("=", apply("kept_edge", _xmt_interp_edge_G_8.a_1, _xmt_interp_edge_G_8.a_2), and_(apply("keep", _xmt_interp_edge_G_8.a_1), apply("keep", _xmt_interp_edge_G_8.a_2), _xmt_interp_edge_G_8.G)) AS G
FROM _xmt_interp_edge_G AS _xmt_interp_edge_G_8)
=== (not (kept_edge x y)) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
apply("not", apply("kept_edge", _xmt_sort_node.G, _xmt_sort_node_2.G)) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
apply("not", apply("kept_edge", _xmt_sort_node.G, _xmt_sort_node_2.G)) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
apply("not", apply("kept_edge", _xmt_sort_node.G, _xmt_sort_node_2.G)) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
=== (color x) ======================================
-- Join(0)
SELECT _xmt_sort_node.G AS x,
apply("color", _xmt_sort_node.G) AS G
FROM _xmt_sort_node
=== (color y) ======================================
-- Join(0)
SELECT _xmt_sort_node_2.G AS y,
apply("color", _xmt_sort_node_2.G) AS G
FROM _xmt_sort_node AS _xmt_sort_node_2
=== (= (color x) (color y)) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
apply("=", apply("color", _xmt_sort_node.G), apply("color", _xmt_sort_node_2.G)) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
apply("=", apply("color", _xmt_sort_node.G), apply("color", _xmt_sort_node_2.G)) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
apply("=", apply("color", _xmt_sort_node.G), apply("color", _xmt_sort_node_2.G)) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
=== (not (= (color x) (color y))) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
apply("not", apply("=", apply("color", _xmt_sort_node.G), apply("color", _xmt_sort_node_2.G))) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
apply("not", apply("=", apply("color", _xmt_sort_node.G), apply("color", _xmt_sort_node_2.G))) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
apply("not", apply("=", apply("color", _xmt_sort_node.G), apply("color", _xmt_sort_node_2.G))) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
=== (or (not (kept_edge x y)) (not (= (color x) (color y)))) ======================================
----- TU -----------------------------------------------------------
-- Agg (0)
SELECT x, y,
or_aggregate(G) as G
FROM (-- Join(7)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
apply("not", apply("kept_edge", _xmt_sort_node.G, _xmt_sort_node_2.G)) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
UNION ALL
-- Join(7)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
apply("not", apply("=", apply("color", _xmt_sort_node.G), apply("color", _xmt_sort_node_2.G))) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2)
GROUP BY x, y
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
or_(apply("not", apply("kept_edge", _xmt_sort_node.G, _xmt_sort_node_2.G)), apply("not", apply("=", apply("color", _xmt_sort_node.G), apply("color", _xmt_sort_node_2.G)))) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
or_(apply("not", apply("kept_edge", _xmt_sort_node.G, _xmt_sort_node_2.G)), apply("not", apply("=", apply("color", _xmt_sort_node.G), apply("color", _xmt_sort_node_2.G)))) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2
=== (top) (forall ((x Node) (y Node)) (or (not (kept_edge x y)) (not (= (color x) (color y))))) ======================================
----- TU -----------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, NULL AS y, "true" AS G
UNION ALL
-- Join(7)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
or_(apply("not", apply("kept_edge", _xmt_sort_node.G, _xmt_sort_node_2.G)), apply("not", apply("=", apply("color", _xmt_sort_node.G), apply("color", _xmt_sort_node_2.G)))) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2)
----- UF -----------------------------------------------------------
-- Agg (0)
SELECT G as G
FROM (-- Join(7)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
or_(apply("not", apply("kept_edge", _xmt_sort_node.G, _xmt_sort_node_2.G)), apply("not", apply("=", apply("color", _xmt_sort_node.G), apply("color", _xmt_sort_node_2.G)))) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2)
----- G ------------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, NULL AS y, "true" AS G
UNION ALL
-- Join(7)
SELECT _xmt_sort_node.G AS x,
_xmt_sort_node_2.G AS y,
or_(apply("not", apply("kept_edge", _xmt_sort_node.G, _xmt_sort_node_2.G)), apply("not", apply("=", apply("color", _xmt_sort_node.G), apply("color", _xmt_sort_node_2.G)))) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_2)
=== (not (keep x)) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
apply("not", apply("keep", _xmt_sort_node.G)) AS G
FROM _xmt_sort_node
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
apply("not", apply("keep", _xmt_sort_node.G)) AS G
FROM _xmt_sort_node
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
apply("not", apply("keep", _xmt_sort_node.G)) AS G
FROM _xmt_sort_node
=== (not (not (keep x))) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
apply("not", apply("not", apply("keep", _xmt_sort_node.G))) AS G
FROM _xmt_sort_node
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
apply("not", apply("not", apply("keep", _xmt_sort_node.G))) AS G
FROM _xmt_sort_node
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
apply("not", apply("not", apply("keep", _xmt_sort_node.G))) AS G
FROM _xmt_sort_node
=== red ======================================
-- Join(0)
SELECT "red" AS G
=== (= (color x) red) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
apply("=", apply("color", _xmt_sort_node.G), "red") AS G
FROM _xmt_sort_node
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
apply("=", apply("color", _xmt_sort_node.G), "red") AS G
FROM _xmt_sort_node
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
apply("=", apply("color", _xmt_sort_node.G), "red") AS G
FROM _xmt_sort_node
=== (or (not (not (keep x))) (= (color x) red)) ======================================
----- TU -----------------------------------------------------------
-- Agg (0)
SELECT x,
or_aggregate(G) as G
FROM (-- Join(7)
SELECT _xmt_sort_node.G AS x,
apply("not", apply("not", apply("keep", _xmt_sort_node.G))) AS G
FROM _xmt_sort_node
UNION ALL
-- Join(7)
SELECT _xmt_sort_node.G AS x,
apply("=", apply("color", _xmt_sort_node.G), "red") AS G
FROM _xmt_sort_node)
GROUP BY x
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
or_(apply("not", apply("not", apply("keep", _xmt_sort_node.G))), apply("=", apply("color", _xmt_sort_node.G), "red")) AS G
FROM _xmt_sort_node
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS x,
or_(apply("not", apply("not", apply("keep", _xmt_sort_node.G))), apply("=", apply("color", _xmt_sort_node.G), "red")) AS G
FROM _xmt_sort_node
=== (top) (forall ((x Node)) (or (not (not (keep x))) (= (color x) red))) ======================================
----- TU -----------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, "true" AS G
UNION ALL
-- Join(7)
SELECT _xmt_sort_node.G AS x,
or_(apply("not", apply("not", apply("keep", _xmt_sort_node.G))), apply("=", apply("color", _xmt_sort_node.G), "red")) AS G
FROM _xmt_sort_node)
----- UF -----------------------------------------------------------
-- Agg (0)
SELECT G as G
FROM (-- Join(7)
SELECT _xmt_sort_node.G AS x,
or_(apply("not", apply("not", apply("keep", _xmt_sort_node.G))), apply("=", apply("color", _xmt_sort_node.G), "red")) AS G
FROM _xmt_sort_node)
----- G ------------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, "true" AS G
UNION ALL
-- Join(7)
SELECT _xmt_sort_node.G AS x,
or_(apply("not", apply("not", apply("keep", _xmt_sort_node.G))), apply("=", apply("color", _xmt_sort_node.G), "red")) AS G
FROM _xmt_sort_node)
===========================================