(set-option :backend none)
(declare-datatype node ( (n1) (n2) ))
(declare-fun edge (node node) Bool)
(declare-fun reaches (node node) Bool)
(declare-fun level (node node) Real)
; using level mapping
(assert (forall ((X node) (Y node))
(= (reaches X Y)
(or (edge X Y)
(exists ((Z node))
(and (edge X Z)
(reaches Z Y) (< (level Z Y) (level X Y)))
)))))
(x-interpret-pred edge (x-set (n1 n2) ))
(x-ground :debug :sql)
(x-debug solver groundings)
------- RESULTS ------------------
(declare-datatype node ((n1) (n2)))
(declare-fun edge (node node) Bool)
(declare-fun reaches (node node) Bool)
(declare-fun level (node node) Real)
; ==== Query =============================
;-- Agg (0)
;SELECT G as G
; FROM (-- Join(7)
; SELECT _xmt_view_reaches_2_4.X AS X,
; _xmt_view_reaches_2_4.Y AS Y,
; bool_eq_("true", _xmt_view_reaches_2_4.G, _xmt_view_or_12.G) AS G
; FROM (-- Join(15)
; SELECT _xmt_sort_node.G AS X,
; _xmt_sort_node_1.G AS Y,
; apply("reaches", _xmt_sort_node.G, _xmt_sort_node_1.G) AS G
; FROM _xmt_sort_node
; JOIN _xmt_sort_node AS _xmt_sort_node_1
; ) AS _xmt_view_reaches_2_4
; FULL JOIN (-- Join(15)
; SELECT _xmt_interp_edge_UF_3.a_1 AS X,
; _xmt_interp_edge_UF_3.a_2 AS Y,
; Agg_11_UF.G AS G
; FROM (-- Agg (23)
; SELECT X, Y,
; or_aggregate(G) as G
; FROM (SELECT _xmt_sort_node.G AS X, NULL AS Z, _xmt_sort_node_1.G AS Y, "false" AS G FROM _xmt_sort_node AS _xmt_sort_node JOIN _xmt_sort_node AS _xmt_sort_node_1
; UNION ALL
; -- Join(30)
; SELECT _xmt_interp_edge_TU_5.a_1 AS X,
; _xmt_interp_edge_TU_5.a_2 AS Z,
; _xmt_sort_node_1.G AS Y,
; and_(apply("reaches", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("<", apply("level", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("level", _xmt_interp_edge_TU_5.a_1, _xmt_sort_node_1.G))) AS G
; FROM _xmt_sort_node AS _xmt_sort_node_1
; JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5)
; GROUP BY X, Y
; ) AS Agg_11_UF
; JOIN _xmt_interp_edge_UF AS _xmt_interp_edge_UF_3
; WHERE Agg_11_UF.X = _xmt_interp_edge_UF_3.a_1
; AND Agg_11_UF.Y = _xmt_interp_edge_UF_3.a_2
; ) AS _xmt_view_or_12 ON _xmt_view_or_12.X = _xmt_view_reaches_2_4.X
; AND _xmt_view_or_12.Y = _xmt_view_reaches_2_4.Y)(assert (= (reaches n1 n1) (and (reaches n2 n1) (< (level n2 n1) (level n1 n1)))))
(assert (= (reaches n1 n2) true))
(assert (= (reaches n2 n1) false))
(assert (= (reaches n2 n2) false))
Groundings:
=== X ======================================
-- Join(0)
SELECT _xmt_sort_node.G AS X,
_xmt_sort_node.G AS G
FROM _xmt_sort_node
=== Y ======================================
-- Join(0)
SELECT _xmt_sort_node_1.G AS Y,
_xmt_sort_node_1.G AS G
FROM _xmt_sort_node AS _xmt_sort_node_1
=== (reaches X Y) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS X,
_xmt_sort_node_1.G AS Y,
apply("reaches", _xmt_sort_node.G, _xmt_sort_node_1.G) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_1
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS X,
_xmt_sort_node_1.G AS Y,
apply("reaches", _xmt_sort_node.G, _xmt_sort_node_1.G) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_1
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS X,
_xmt_sort_node_1.G AS Y,
apply("reaches", _xmt_sort_node.G, _xmt_sort_node_1.G) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_1
=== (edge X Y) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_TU_3.a_1 AS X,
_xmt_interp_edge_TU_3.a_2 AS Y,
"true" AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_3
----- F ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_UF_3.a_1 AS X,
_xmt_interp_edge_UF_3.a_2 AS Y,
"false" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_3
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_G_3.a_1 AS X,
_xmt_interp_edge_G_3.a_2 AS Y,
_xmt_interp_edge_G_3.G AS G
FROM _xmt_interp_edge_G AS _xmt_interp_edge_G_3
=== Z ======================================
-- Join(0)
SELECT _xmt_sort_node_4.G AS Z,
_xmt_sort_node_4.G AS G
FROM _xmt_sort_node AS _xmt_sort_node_4
=== (edge X Z) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_TU_5.a_1 AS X,
_xmt_interp_edge_TU_5.a_2 AS Z,
"true" AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5
----- F ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_UF_5.a_1 AS X,
_xmt_interp_edge_UF_5.a_2 AS Z,
"false" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_5
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_G_5.a_1 AS X,
_xmt_interp_edge_G_5.a_2 AS Z,
_xmt_interp_edge_G_5.G AS G
FROM _xmt_interp_edge_G AS _xmt_interp_edge_G_5
=== (reaches Z Y) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node_4.G AS Z,
_xmt_sort_node_1.G AS Y,
apply("reaches", _xmt_sort_node_4.G, _xmt_sort_node_1.G) AS G
FROM _xmt_sort_node AS _xmt_sort_node_4
JOIN _xmt_sort_node AS _xmt_sort_node_1
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node_4.G AS Z,
_xmt_sort_node_1.G AS Y,
apply("reaches", _xmt_sort_node_4.G, _xmt_sort_node_1.G) AS G
FROM _xmt_sort_node AS _xmt_sort_node_4
JOIN _xmt_sort_node AS _xmt_sort_node_1
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node_4.G AS Z,
_xmt_sort_node_1.G AS Y,
apply("reaches", _xmt_sort_node_4.G, _xmt_sort_node_1.G) AS G
FROM _xmt_sort_node AS _xmt_sort_node_4
JOIN _xmt_sort_node AS _xmt_sort_node_1
=== (level Z Y) ======================================
-- Join(0)
SELECT _xmt_sort_node_4.G AS Z,
_xmt_sort_node_1.G AS Y,
apply("level", _xmt_sort_node_4.G, _xmt_sort_node_1.G) AS G
FROM _xmt_sort_node AS _xmt_sort_node_4
JOIN _xmt_sort_node AS _xmt_sort_node_1
=== (level X Y) ======================================
-- Join(0)
SELECT _xmt_sort_node.G AS X,
_xmt_sort_node_1.G AS Y,
apply("level", _xmt_sort_node.G, _xmt_sort_node_1.G) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_1
=== (< (level Z Y) (level X Y)) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node_4.G AS Z,
_xmt_sort_node_1.G AS Y,
_xmt_sort_node.G AS X,
apply("<", apply("level", _xmt_sort_node_4.G, _xmt_sort_node_1.G), apply("level", _xmt_sort_node.G, _xmt_sort_node_1.G)) AS G
FROM _xmt_sort_node AS _xmt_sort_node_4
JOIN _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_sort_node
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node_4.G AS Z,
_xmt_sort_node_1.G AS Y,
_xmt_sort_node.G AS X,
apply("<", apply("level", _xmt_sort_node_4.G, _xmt_sort_node_1.G), apply("level", _xmt_sort_node.G, _xmt_sort_node_1.G)) AS G
FROM _xmt_sort_node AS _xmt_sort_node_4
JOIN _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_sort_node
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node_4.G AS Z,
_xmt_sort_node_1.G AS Y,
_xmt_sort_node.G AS X,
apply("<", apply("level", _xmt_sort_node_4.G, _xmt_sort_node_1.G), apply("level", _xmt_sort_node.G, _xmt_sort_node_1.G)) AS G
FROM _xmt_sort_node AS _xmt_sort_node_4
JOIN _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_sort_node
=== (and (edge X Z) (reaches Z Y) (< (level Z Y) (level X Y))) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_TU_5.a_1 AS X,
_xmt_interp_edge_TU_5.a_2 AS Z,
_xmt_sort_node_1.G AS Y,
and_(apply("reaches", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("<", apply("level", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("level", _xmt_interp_edge_TU_5.a_1, _xmt_sort_node_1.G))) AS G
FROM _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5
----- F ------------------------------------------------------------
-- Agg (0)
SELECT X, Z, Y,
and_aggregate(G) as G
FROM (-- exclude(7)
SELECT *
FROM (-- Join(14)
SELECT _xmt_view_edge_5_9.X AS X,
_xmt_view_edge_5_9.Z AS Z,
_xmt_sort_node_1.G AS Y,
_xmt_view_edge_5_9.G AS G
FROM (-- Join(22)
SELECT _xmt_interp_edge_UF_5.a_1 AS X,
_xmt_interp_edge_UF_5.a_2 AS Z,
"false" AS G
FROM _xmt_interp_edge_UF AS _xmt_interp_edge_UF_5
) AS _xmt_view_edge_5_9
JOIN _xmt_sort_node AS _xmt_sort_node_1
UNION ALL
-- Join(14)
SELECT _xmt_sort_node.G AS X,
_xmt_view_reaches_6_13.Z AS Z,
_xmt_view_reaches_6_13.Y AS Y,
_xmt_view_reaches_6_13.G AS G
FROM (-- Join(22)
SELECT _xmt_sort_node_4.G AS Z,
_xmt_sort_node_1.G AS Y,
apply("reaches", _xmt_sort_node_4.G, _xmt_sort_node_1.G) AS G
FROM _xmt_sort_node AS _xmt_sort_node_4
JOIN _xmt_sort_node AS _xmt_sort_node_1
) AS _xmt_view_reaches_6_13
JOIN _xmt_sort_node
UNION ALL
-- Join(14)
SELECT _xmt_sort_node_4.G AS Z,
_xmt_sort_node_1.G AS Y,
_xmt_sort_node.G AS X,
apply("<", apply("level", _xmt_sort_node_4.G, _xmt_sort_node_1.G), apply("level", _xmt_sort_node.G, _xmt_sort_node_1.G)) AS G
FROM _xmt_sort_node AS _xmt_sort_node_4
JOIN _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_sort_node)
WHERE G <> "true")
GROUP BY X, Z, Y
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_G_5.a_1 AS X,
_xmt_interp_edge_G_5.a_2 AS Z,
_xmt_sort_node_1.G AS Y,
and_(_xmt_interp_edge_G_5.G, apply("reaches", _xmt_interp_edge_G_5.a_2, _xmt_sort_node_1.G), apply("<", apply("level", _xmt_interp_edge_G_5.a_2, _xmt_sort_node_1.G), apply("level", _xmt_interp_edge_G_5.a_1, _xmt_sort_node_1.G))) AS G
FROM _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_interp_edge_G AS _xmt_interp_edge_G_5
=== (exists ((Z node)) (and (edge X Z) (reaches Z Y) (< (level Z Y) (level X Y)))) ======================================
----- TU -----------------------------------------------------------
-- Agg (0)
SELECT X, Y,
or_aggregate(G) as G
FROM (-- Join(7)
SELECT _xmt_interp_edge_TU_5.a_1 AS X,
_xmt_interp_edge_TU_5.a_2 AS Z,
_xmt_sort_node_1.G AS Y,
and_(apply("reaches", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("<", apply("level", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("level", _xmt_interp_edge_TU_5.a_1, _xmt_sort_node_1.G))) AS G
FROM _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5)
GROUP BY X, Y
----- UF -----------------------------------------------------------
-- Agg (0)
SELECT X, Y,
or_aggregate(G) as G
FROM (SELECT _xmt_sort_node.G AS X, NULL AS Z, _xmt_sort_node_1.G AS Y, "false" AS G FROM _xmt_sort_node AS _xmt_sort_node JOIN _xmt_sort_node AS _xmt_sort_node_1
UNION ALL
-- Join(7)
SELECT _xmt_interp_edge_TU_5.a_1 AS X,
_xmt_interp_edge_TU_5.a_2 AS Z,
_xmt_sort_node_1.G AS Y,
and_(apply("reaches", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("<", apply("level", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("level", _xmt_interp_edge_TU_5.a_1, _xmt_sort_node_1.G))) AS G
FROM _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5)
GROUP BY X, Y
----- G ------------------------------------------------------------
-- Agg (0)
SELECT X, Y,
or_aggregate(G) as G
FROM (SELECT _xmt_sort_node.G AS X, NULL AS Z, _xmt_sort_node_1.G AS Y, "false" AS G FROM _xmt_sort_node AS _xmt_sort_node JOIN _xmt_sort_node AS _xmt_sort_node_1
UNION ALL
-- Join(7)
SELECT _xmt_interp_edge_TU_5.a_1 AS X,
_xmt_interp_edge_TU_5.a_2 AS Z,
_xmt_sort_node_1.G AS Y,
and_(apply("reaches", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("<", apply("level", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("level", _xmt_interp_edge_TU_5.a_1, _xmt_sort_node_1.G))) AS G
FROM _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5)
GROUP BY X, Y
=== (or (edge X Y) (exists ((Z node)) (and (edge X Z) (reaches Z Y) (< (level Z Y) (level X Y))))) ======================================
----- T ------------------------------------------------------------
-- Agg (0)
SELECT X, Y,
or_aggregate(G) as G
FROM (-- Join(7)
SELECT _xmt_interp_edge_TU_3.a_1 AS X,
_xmt_interp_edge_TU_3.a_2 AS Y,
"true" AS G
FROM _xmt_interp_edge_TU AS _xmt_interp_edge_TU_3
UNION ALL
-- Agg (7)
SELECT X, Y,
or_aggregate(G) as G
FROM (-- Join(14)
SELECT _xmt_interp_edge_TU_5.a_1 AS X,
_xmt_interp_edge_TU_5.a_2 AS Z,
_xmt_sort_node_1.G AS Y,
and_(apply("reaches", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("<", apply("level", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("level", _xmt_interp_edge_TU_5.a_1, _xmt_sort_node_1.G))) AS G
FROM _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5)
GROUP BY X, Y)
GROUP BY X, Y
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_UF_3.a_1 AS X,
_xmt_interp_edge_UF_3.a_2 AS Y,
Agg_11_UF.G AS G
FROM (-- Agg (8)
SELECT X, Y,
or_aggregate(G) as G
FROM (SELECT _xmt_sort_node.G AS X, NULL AS Z, _xmt_sort_node_1.G AS Y, "false" AS G FROM _xmt_sort_node AS _xmt_sort_node JOIN _xmt_sort_node AS _xmt_sort_node_1
UNION ALL
-- Join(15)
SELECT _xmt_interp_edge_TU_5.a_1 AS X,
_xmt_interp_edge_TU_5.a_2 AS Z,
_xmt_sort_node_1.G AS Y,
and_(apply("reaches", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("<", apply("level", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("level", _xmt_interp_edge_TU_5.a_1, _xmt_sort_node_1.G))) AS G
FROM _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5)
GROUP BY X, Y
) AS Agg_11_UF
JOIN _xmt_interp_edge_UF AS _xmt_interp_edge_UF_3
WHERE Agg_11_UF.X = _xmt_interp_edge_UF_3.a_1
AND Agg_11_UF.Y = _xmt_interp_edge_UF_3.a_2
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_G_3.a_1 AS X,
_xmt_interp_edge_G_3.a_2 AS Y,
or_(_xmt_interp_edge_G_3.G, Agg_11_G.G) AS G
FROM (-- Agg (8)
SELECT X, Y,
or_aggregate(G) as G
FROM (SELECT _xmt_sort_node.G AS X, NULL AS Z, _xmt_sort_node_1.G AS Y, "false" AS G FROM _xmt_sort_node AS _xmt_sort_node JOIN _xmt_sort_node AS _xmt_sort_node_1
UNION ALL
-- Join(15)
SELECT _xmt_interp_edge_TU_5.a_1 AS X,
_xmt_interp_edge_TU_5.a_2 AS Z,
_xmt_sort_node_1.G AS Y,
and_(apply("reaches", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("<", apply("level", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("level", _xmt_interp_edge_TU_5.a_1, _xmt_sort_node_1.G))) AS G
FROM _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5)
GROUP BY X, Y
) AS Agg_11_G
JOIN _xmt_interp_edge_G AS _xmt_interp_edge_G_3
WHERE Agg_11_G.X = _xmt_interp_edge_G_3.a_1
AND Agg_11_G.Y = _xmt_interp_edge_G_3.a_2
=== (= (reaches X Y) (or (edge X Y) (exists ((Z node)) (and (edge X Z) (reaches Z Y) (< (level Z Y) (level X Y)))))) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_G_3.a_1 AS X,
_xmt_interp_edge_G_3.a_2 AS Y,
apply("=", apply("reaches", _xmt_interp_edge_G_3.a_1, _xmt_interp_edge_G_3.a_2), or_(_xmt_interp_edge_G_3.G, Agg_11_G.G)) AS G
FROM (-- Agg (8)
SELECT X, Y,
or_aggregate(G) as G
FROM (SELECT _xmt_sort_node.G AS X, NULL AS Z, _xmt_sort_node_1.G AS Y, "false" AS G FROM _xmt_sort_node AS _xmt_sort_node JOIN _xmt_sort_node AS _xmt_sort_node_1
UNION ALL
-- Join(15)
SELECT _xmt_interp_edge_TU_5.a_1 AS X,
_xmt_interp_edge_TU_5.a_2 AS Z,
_xmt_sort_node_1.G AS Y,
and_(apply("reaches", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("<", apply("level", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("level", _xmt_interp_edge_TU_5.a_1, _xmt_sort_node_1.G))) AS G
FROM _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5)
GROUP BY X, Y
) AS Agg_11_G
JOIN _xmt_interp_edge_G AS _xmt_interp_edge_G_3
WHERE Agg_11_G.X = _xmt_interp_edge_G_3.a_1
AND Agg_11_G.Y = _xmt_interp_edge_G_3.a_2
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_view_reaches_2_4.X AS X,
_xmt_view_reaches_2_4.Y AS Y,
bool_eq_("true", _xmt_view_reaches_2_4.G, _xmt_view_or_12.G) AS G
FROM (-- Join(8)
SELECT _xmt_sort_node.G AS X,
_xmt_sort_node_1.G AS Y,
apply("reaches", _xmt_sort_node.G, _xmt_sort_node_1.G) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_1
) AS _xmt_view_reaches_2_4
FULL JOIN (-- Join(8)
SELECT _xmt_interp_edge_UF_3.a_1 AS X,
_xmt_interp_edge_UF_3.a_2 AS Y,
Agg_11_UF.G AS G
FROM (-- Agg (16)
SELECT X, Y,
or_aggregate(G) as G
FROM (SELECT _xmt_sort_node.G AS X, NULL AS Z, _xmt_sort_node_1.G AS Y, "false" AS G FROM _xmt_sort_node AS _xmt_sort_node JOIN _xmt_sort_node AS _xmt_sort_node_1
UNION ALL
-- Join(23)
SELECT _xmt_interp_edge_TU_5.a_1 AS X,
_xmt_interp_edge_TU_5.a_2 AS Z,
_xmt_sort_node_1.G AS Y,
and_(apply("reaches", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("<", apply("level", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("level", _xmt_interp_edge_TU_5.a_1, _xmt_sort_node_1.G))) AS G
FROM _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5)
GROUP BY X, Y
) AS Agg_11_UF
JOIN _xmt_interp_edge_UF AS _xmt_interp_edge_UF_3
WHERE Agg_11_UF.X = _xmt_interp_edge_UF_3.a_1
AND Agg_11_UF.Y = _xmt_interp_edge_UF_3.a_2
) AS _xmt_view_or_12 ON _xmt_view_or_12.X = _xmt_view_reaches_2_4.X
AND _xmt_view_or_12.Y = _xmt_view_reaches_2_4.Y
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_edge_G_3.a_1 AS X,
_xmt_interp_edge_G_3.a_2 AS Y,
apply("=", apply("reaches", _xmt_interp_edge_G_3.a_1, _xmt_interp_edge_G_3.a_2), or_(_xmt_interp_edge_G_3.G, Agg_11_G.G)) AS G
FROM (-- Agg (8)
SELECT X, Y,
or_aggregate(G) as G
FROM (SELECT _xmt_sort_node.G AS X, NULL AS Z, _xmt_sort_node_1.G AS Y, "false" AS G FROM _xmt_sort_node AS _xmt_sort_node JOIN _xmt_sort_node AS _xmt_sort_node_1
UNION ALL
-- Join(15)
SELECT _xmt_interp_edge_TU_5.a_1 AS X,
_xmt_interp_edge_TU_5.a_2 AS Z,
_xmt_sort_node_1.G AS Y,
and_(apply("reaches", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("<", apply("level", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("level", _xmt_interp_edge_TU_5.a_1, _xmt_sort_node_1.G))) AS G
FROM _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5)
GROUP BY X, Y
) AS Agg_11_G
JOIN _xmt_interp_edge_G AS _xmt_interp_edge_G_3
WHERE Agg_11_G.X = _xmt_interp_edge_G_3.a_1
AND Agg_11_G.Y = _xmt_interp_edge_G_3.a_2
=== (top) (forall ((X node) (Y node)) (= (reaches X Y) (or (edge X Y) (exists ((Z node)) (and (edge X Z) (reaches Z Y) (< (level Z Y) (level 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_view_reaches_2_4.X AS X,
_xmt_view_reaches_2_4.Y AS Y,
bool_eq_("true", _xmt_view_reaches_2_4.G, _xmt_view_or_12.G) AS G
FROM (-- Join(15)
SELECT _xmt_sort_node.G AS X,
_xmt_sort_node_1.G AS Y,
apply("reaches", _xmt_sort_node.G, _xmt_sort_node_1.G) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_1
) AS _xmt_view_reaches_2_4
FULL JOIN (-- Join(15)
SELECT _xmt_interp_edge_UF_3.a_1 AS X,
_xmt_interp_edge_UF_3.a_2 AS Y,
Agg_11_UF.G AS G
FROM (-- Agg (23)
SELECT X, Y,
or_aggregate(G) as G
FROM (SELECT _xmt_sort_node.G AS X, NULL AS Z, _xmt_sort_node_1.G AS Y, "false" AS G FROM _xmt_sort_node AS _xmt_sort_node JOIN _xmt_sort_node AS _xmt_sort_node_1
UNION ALL
-- Join(30)
SELECT _xmt_interp_edge_TU_5.a_1 AS X,
_xmt_interp_edge_TU_5.a_2 AS Z,
_xmt_sort_node_1.G AS Y,
and_(apply("reaches", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("<", apply("level", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("level", _xmt_interp_edge_TU_5.a_1, _xmt_sort_node_1.G))) AS G
FROM _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5)
GROUP BY X, Y
) AS Agg_11_UF
JOIN _xmt_interp_edge_UF AS _xmt_interp_edge_UF_3
WHERE Agg_11_UF.X = _xmt_interp_edge_UF_3.a_1
AND Agg_11_UF.Y = _xmt_interp_edge_UF_3.a_2
) AS _xmt_view_or_12 ON _xmt_view_or_12.X = _xmt_view_reaches_2_4.X
AND _xmt_view_or_12.Y = _xmt_view_reaches_2_4.Y)
----- UF -----------------------------------------------------------
-- Agg (0)
SELECT G as G
FROM (-- Join(7)
SELECT _xmt_view_reaches_2_4.X AS X,
_xmt_view_reaches_2_4.Y AS Y,
bool_eq_("true", _xmt_view_reaches_2_4.G, _xmt_view_or_12.G) AS G
FROM (-- Join(15)
SELECT _xmt_sort_node.G AS X,
_xmt_sort_node_1.G AS Y,
apply("reaches", _xmt_sort_node.G, _xmt_sort_node_1.G) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_1
) AS _xmt_view_reaches_2_4
FULL JOIN (-- Join(15)
SELECT _xmt_interp_edge_UF_3.a_1 AS X,
_xmt_interp_edge_UF_3.a_2 AS Y,
Agg_11_UF.G AS G
FROM (-- Agg (23)
SELECT X, Y,
or_aggregate(G) as G
FROM (SELECT _xmt_sort_node.G AS X, NULL AS Z, _xmt_sort_node_1.G AS Y, "false" AS G FROM _xmt_sort_node AS _xmt_sort_node JOIN _xmt_sort_node AS _xmt_sort_node_1
UNION ALL
-- Join(30)
SELECT _xmt_interp_edge_TU_5.a_1 AS X,
_xmt_interp_edge_TU_5.a_2 AS Z,
_xmt_sort_node_1.G AS Y,
and_(apply("reaches", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("<", apply("level", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("level", _xmt_interp_edge_TU_5.a_1, _xmt_sort_node_1.G))) AS G
FROM _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5)
GROUP BY X, Y
) AS Agg_11_UF
JOIN _xmt_interp_edge_UF AS _xmt_interp_edge_UF_3
WHERE Agg_11_UF.X = _xmt_interp_edge_UF_3.a_1
AND Agg_11_UF.Y = _xmt_interp_edge_UF_3.a_2
) AS _xmt_view_or_12 ON _xmt_view_or_12.X = _xmt_view_reaches_2_4.X
AND _xmt_view_or_12.Y = _xmt_view_reaches_2_4.Y)
----- 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_view_reaches_2_4.X AS X,
_xmt_view_reaches_2_4.Y AS Y,
bool_eq_("true", _xmt_view_reaches_2_4.G, _xmt_view_or_12.G) AS G
FROM (-- Join(15)
SELECT _xmt_sort_node.G AS X,
_xmt_sort_node_1.G AS Y,
apply("reaches", _xmt_sort_node.G, _xmt_sort_node_1.G) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_1
) AS _xmt_view_reaches_2_4
FULL JOIN (-- Join(15)
SELECT _xmt_interp_edge_UF_3.a_1 AS X,
_xmt_interp_edge_UF_3.a_2 AS Y,
Agg_11_UF.G AS G
FROM (-- Agg (23)
SELECT X, Y,
or_aggregate(G) as G
FROM (SELECT _xmt_sort_node.G AS X, NULL AS Z, _xmt_sort_node_1.G AS Y, "false" AS G FROM _xmt_sort_node AS _xmt_sort_node JOIN _xmt_sort_node AS _xmt_sort_node_1
UNION ALL
-- Join(30)
SELECT _xmt_interp_edge_TU_5.a_1 AS X,
_xmt_interp_edge_TU_5.a_2 AS Z,
_xmt_sort_node_1.G AS Y,
and_(apply("reaches", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("<", apply("level", _xmt_interp_edge_TU_5.a_2, _xmt_sort_node_1.G), apply("level", _xmt_interp_edge_TU_5.a_1, _xmt_sort_node_1.G))) AS G
FROM _xmt_sort_node AS _xmt_sort_node_1
JOIN _xmt_interp_edge_TU AS _xmt_interp_edge_TU_5)
GROUP BY X, Y
) AS Agg_11_UF
JOIN _xmt_interp_edge_UF AS _xmt_interp_edge_UF_3
WHERE Agg_11_UF.X = _xmt_interp_edge_UF_3.a_1
AND Agg_11_UF.Y = _xmt_interp_edge_UF_3.a_2
) AS _xmt_view_or_12 ON _xmt_view_or_12.X = _xmt_view_reaches_2_4.X
AND _xmt_view_or_12.Y = _xmt_view_reaches_2_4.Y)
===========================================