(set-option :backend none)
(declare-datatype Node (
(n1) (n2) (n3)
))
(declare-datatype Colour ( ( yellow ) ( cyan ) (blue) (green) (red)))
(declare-fun link (Node Node) Bool)
(declare-fun colourOf (Node) Colour)
;!n1 n2 in Node: link(n1 n2) => colourOf(n1) ~= colourOf(n2).
(assert (forall ((n1 Node) (n2 Node))
(=> (link n1 n2)
(not (= (colourOf n1) (colourOf n2))))))
(x-interpret-pred link (x-set (n1 n2) (n2 n3)))
(x-ground)
(x-debug solver groundings)
------- RESULTS ------------------
(declare-datatype Node ((n1) (n2) (n3)))
(declare-datatype Colour ((yellow) (cyan) (blue) (green) (red)))
(declare-fun link (Node Node) Bool)
(declare-fun colourOf (Node) Colour)
(assert (not (= (colourOf n1) (colourOf n2))))
(assert (not (= (colourOf n2) (colourOf n3))))
Groundings:
=== n1 ======================================
-- Join(0)
SELECT _xmt_sort_node.G AS n1,
_xmt_sort_node.G AS G
FROM _xmt_sort_node
=== n2 ======================================
-- Join(0)
SELECT _xmt_sort_node_1.G AS n2,
_xmt_sort_node_1.G AS G
FROM _xmt_sort_node AS _xmt_sort_node_1
=== (link n1 n2) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_link_TU_2.a_1 AS n1,
_xmt_interp_link_TU_2.a_2 AS n2,
"true" AS G
FROM _xmt_interp_link_TU AS _xmt_interp_link_TU_2
----- F ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_link_UF_2.a_1 AS n1,
_xmt_interp_link_UF_2.a_2 AS n2,
"false" AS G
FROM _xmt_interp_link_UF AS _xmt_interp_link_UF_2
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_link_G_2.a_1 AS n1,
_xmt_interp_link_G_2.a_2 AS n2,
_xmt_interp_link_G_2.G AS G
FROM _xmt_interp_link_G AS _xmt_interp_link_G_2
=== (not (link n1 n2)) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_link_UF_2.a_1 AS n1,
_xmt_interp_link_UF_2.a_2 AS n2,
"true" AS G
FROM _xmt_interp_link_UF AS _xmt_interp_link_UF_2
----- F ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_link_TU_2.a_1 AS n1,
_xmt_interp_link_TU_2.a_2 AS n2,
"false" AS G
FROM _xmt_interp_link_TU AS _xmt_interp_link_TU_2
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_link_G_2.a_1 AS n1,
_xmt_interp_link_G_2.a_2 AS n2,
not_(_xmt_interp_link_G_2.G) AS G
FROM _xmt_interp_link_G AS _xmt_interp_link_G_2
=== (colourOf n1) ======================================
-- Join(0)
SELECT _xmt_sort_node.G AS n1,
apply("colourOf", _xmt_sort_node.G) AS G
FROM _xmt_sort_node
=== (colourOf n2) ======================================
-- Join(0)
SELECT _xmt_sort_node_1.G AS n2,
apply("colourOf", _xmt_sort_node_1.G) AS G
FROM _xmt_sort_node AS _xmt_sort_node_1
=== (= (colourOf n1) (colourOf n2)) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS n1,
_xmt_sort_node_1.G AS n2,
apply("=", apply("colourOf", _xmt_sort_node.G), apply("colourOf", _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 n1,
_xmt_sort_node_1.G AS n2,
apply("=", apply("colourOf", _xmt_sort_node.G), apply("colourOf", _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 n1,
_xmt_sort_node_1.G AS n2,
apply("=", apply("colourOf", _xmt_sort_node.G), apply("colourOf", _xmt_sort_node_1.G)) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_1
=== (not (= (colourOf n1) (colourOf n2))) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_node.G AS n1,
_xmt_sort_node_1.G AS n2,
apply("not", apply("=", apply("colourOf", _xmt_sort_node.G), apply("colourOf", _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 n1,
_xmt_sort_node_1.G AS n2,
apply("not", apply("=", apply("colourOf", _xmt_sort_node.G), apply("colourOf", _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 n1,
_xmt_sort_node_1.G AS n2,
apply("not", apply("=", apply("colourOf", _xmt_sort_node.G), apply("colourOf", _xmt_sort_node_1.G))) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_1
=== (or (not (link n1 n2)) (not (= (colourOf n1) (colourOf n2)))) ======================================
----- T ------------------------------------------------------------
-- Agg (0)
SELECT n1, n2,
or_aggregate(G) as G
FROM (-- exclude(7)
SELECT *
FROM (-- Join(14)
SELECT _xmt_interp_link_UF_2.a_1 AS n1,
_xmt_interp_link_UF_2.a_2 AS n2,
"true" AS G
FROM _xmt_interp_link_UF AS _xmt_interp_link_UF_2
UNION ALL
-- Join(14)
SELECT _xmt_sort_node.G AS n1,
_xmt_sort_node_1.G AS n2,
apply("not", apply("=", apply("colourOf", _xmt_sort_node.G), apply("colourOf", _xmt_sort_node_1.G))) AS G
FROM _xmt_sort_node
JOIN _xmt_sort_node AS _xmt_sort_node_1)
WHERE G <> "false")
GROUP BY n1, n2
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_link_TU_2.a_1 AS n1,
_xmt_interp_link_TU_2.a_2 AS n2,
apply("not", apply("=", apply("colourOf", _xmt_interp_link_TU_2.a_1), apply("colourOf", _xmt_interp_link_TU_2.a_2))) AS G
FROM _xmt_interp_link_TU AS _xmt_interp_link_TU_2
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_link_G_2.a_1 AS n1,
_xmt_interp_link_G_2.a_2 AS n2,
or_(not_(_xmt_interp_link_G_2.G), apply("not", apply("=", apply("colourOf", _xmt_interp_link_G_2.a_1), apply("colourOf", _xmt_interp_link_G_2.a_2)))) AS G
FROM _xmt_interp_link_G AS _xmt_interp_link_G_2
=== (top) (forall ((n1 Node) (n2 Node)) (or (not (link n1 n2)) (not (= (colourOf n1) (colourOf n2))))) ======================================
----- TU -----------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS n1, NULL AS n2, "true" AS G
UNION ALL
-- Join(7)
SELECT _xmt_interp_link_TU_2.a_1 AS n1,
_xmt_interp_link_TU_2.a_2 AS n2,
apply("not", apply("=", apply("colourOf", _xmt_interp_link_TU_2.a_1), apply("colourOf", _xmt_interp_link_TU_2.a_2))) AS G
FROM _xmt_interp_link_TU AS _xmt_interp_link_TU_2)
----- UF -----------------------------------------------------------
-- Agg (0)
SELECT G as G
FROM (-- Join(7)
SELECT _xmt_interp_link_TU_2.a_1 AS n1,
_xmt_interp_link_TU_2.a_2 AS n2,
apply("not", apply("=", apply("colourOf", _xmt_interp_link_TU_2.a_1), apply("colourOf", _xmt_interp_link_TU_2.a_2))) AS G
FROM _xmt_interp_link_TU AS _xmt_interp_link_TU_2)
----- G ------------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS n1, NULL AS n2, "true" AS G
UNION ALL
-- Join(7)
SELECT _xmt_interp_link_TU_2.a_1 AS n1,
_xmt_interp_link_TU_2.a_2 AS n2,
apply("not", apply("=", apply("colourOf", _xmt_interp_link_TU_2.a_1), apply("colourOf", _xmt_interp_link_TU_2.a_2))) AS G
FROM _xmt_interp_link_TU AS _xmt_interp_link_TU_2)
=== (top) (and (forall ((n1 Node) (n2 Node)) (or (not (link n1 n2)) (not (= (colourOf n1) (colourOf n2)))))) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT Agg_9_TU.G AS G
FROM (-- Agg (8)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS n1, NULL AS n2, "true" AS G
UNION ALL
-- Join(15)
SELECT _xmt_interp_link_TU_2.a_1 AS n1,
_xmt_interp_link_TU_2.a_2 AS n2,
apply("not", apply("=", apply("colourOf", _xmt_interp_link_TU_2.a_1), apply("colourOf", _xmt_interp_link_TU_2.a_2))) AS G
FROM _xmt_interp_link_TU AS _xmt_interp_link_TU_2)
) AS Agg_9_TU
----- UF -----------------------------------------------------------
-- Agg (0)
SELECT G as G
FROM (-- Join(7)
SELECT _xmt_interp_link_TU_2.a_1 AS n1,
_xmt_interp_link_TU_2.a_2 AS n2,
apply("not", apply("=", apply("colourOf", _xmt_interp_link_TU_2.a_1), apply("colourOf", _xmt_interp_link_TU_2.a_2))) AS G
FROM _xmt_interp_link_TU AS _xmt_interp_link_TU_2)
----- G ------------------------------------------------------------
-- Join(0)
SELECT Agg_9_G.G AS G
FROM (-- Agg (8)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS n1, NULL AS n2, "true" AS G
UNION ALL
-- Join(15)
SELECT _xmt_interp_link_TU_2.a_1 AS n1,
_xmt_interp_link_TU_2.a_2 AS n2,
apply("not", apply("=", apply("colourOf", _xmt_interp_link_TU_2.a_1), apply("colourOf", _xmt_interp_link_TU_2.a_2))) AS G
FROM _xmt_interp_link_TU AS _xmt_interp_link_TU_2)
) AS Agg_9_G
===========================================