(set-option :backend none)
(declare-datatype Color ( (red) (blue) (green) ))
(declare-datatype Either ( (nil) (Left (b Color)) (Right (right Color)) ))
(declare-fun p (Either) Bool)
(x-interpret-pred p (x-set (nil) ((Left blue)) ((Right red))))
(assert (p (Right red)))
(assert (p nil))
(assert (not (p (Left red))))
(assert ((_ is nil) nil))
(assert ((_ is Left) (Left blue)))
(assert (= red (b (Left red))))
(x-ground :debug :sql)
(x-debug solver polymorphic_sorts)
(x-debug solver sorts)
(x-debug solver functions)
(x-debug db _xmt_sort_either)
(x-debug db _xmt_interp_p_G)
(x-debug solver groundings)
(check-sat)
------- RESULTS ------------------
(declare-datatype Color ((red) (blue) (green)))
(declare-datatype Either ((nil) (Left (b Color)) (Right (right Color))))
(declare-fun p (Either) Bool)
; ==== Query =============================
;-- Join(0)
;SELECT "false" AS G
; FROM _xmt_interp_p_UF AS _xmt_interp_p_UF_2
; WHERE construct2("Right", "red") = _xmt_interp_p_UF_2.a_1
; ==== Query =============================
;-- Join(0)
;SELECT "false" AS G
; FROM _xmt_interp_p_UF AS _xmt_interp_p_UF_4
; WHERE "nil" = _xmt_interp_p_UF_4.a_1
; ==== Query =============================
;-- Join(0)
;SELECT "false" AS G
; FROM _xmt_interp_p_TU AS _xmt_interp_p_TU_6
; WHERE construct2("Left", "red") = _xmt_interp_p_TU_6.a_1
; ==== Query =============================
;-- exclude(0)
;SELECT *
; FROM (-- Join(7)
; SELECT apply("(_ is nil)", "nil") AS G)
; WHERE G <> "true"(assert ((_ is nil) nil))
; ==== Query =============================
;-- Join(0)
;SELECT "false" AS G
; FROM _xmt_tester_either_left_f AS _xmt_tester_either_left_f_11
; WHERE construct2("Left", "blue") = _xmt_tester_either_left_f_11.a_1
; ==== Query =============================
;-- exclude(0)
;SELECT *
; FROM (-- Join(7)
; SELECT eq_("red", _xmt_selector_either_b_g_12.G) AS G
; FROM _xmt_selector_either_b_g AS _xmt_selector_either_b_g_12
; WHERE "red" != _xmt_selector_either_b_g_12.G
; AND construct2("Left", "red") = _xmt_selector_either_b_g_12.a_1)
; WHERE G <> "true"
Polymorphic datatypes:
- (unknown): Array
Sorts:
- (Bool: 2) Bool: ((true) (false))
- (infinite) Int
- (infinite) Real
- (infinite) RoundingMode
- (infinite) String
- (infinite) RegLan
- (_xmt_sort_color: 3) Color: ((red) (blue) (green))
- (_xmt_sort_either: 7) Either: ((nil) (Left (b Color)) (Right (right Color)))
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
- blue ()->Color : Constructor
- green ()->Color : Constructor
- (_ is red) (Color)->Bool : Predefined (true)
- (_ is blue) (Color)->Bool : Predefined (true)
- (_ is green) (Color)->Bool : Predefined (true)
- nil ()->Either : Constructor
- Left (Color)->Either : Constructor
- Right (Color)->Either : Constructor
- (_ is nil) (Either)->Bool : Predefined (true)
- (_ is Left) (Either)->Bool : Boolean (_xmt_tester_either_left_t Complete, _xmt_tester_either_left_f Complete, _xmt_tester_either_left_g Complete)
- b (Either)->Color : Non Boolean (_xmt_selector_either_b_g Complete)
- (_ is Right) (Either)->Bool : Boolean (_xmt_tester_either_right_t Complete, _xmt_tester_either_right_f Complete, _xmt_tester_either_right_g Complete)
- right (Either)->Color : Non Boolean (_xmt_selector_either_right_g Complete)
- p (Either)->Bool : Boolean (_xmt_interp_p_TU Complete, _xmt_interp_p_UF Complete, _xmt_interp_p_G Complete)
TABLE: _xmt_sort_either
┌─────────────┬─────────┬─────────┬──────────────────┐
│ constructor │ b │ right │ G │
├─────────────┼─────────┼─────────┼──────────────────┤
│ "nil" │ NULL │ NULL │ "nil" │
├─────────────┼─────────┼─────────┼──────────────────┤
│ "Left" │ "blue" │ NULL │ " (Left blue)" │
├─────────────┼─────────┼─────────┼──────────────────┤
│ "Left" │ "green" │ NULL │ " (Left green)" │
├─────────────┼─────────┼─────────┼──────────────────┤
│ "Left" │ "red" │ NULL │ " (Left red)" │
├─────────────┼─────────┼─────────┼──────────────────┤
│ "Right" │ NULL │ "blue" │ " (Right blue)" │
├─────────────┼─────────┼─────────┼──────────────────┤
│ "Right" │ NULL │ "green" │ " (Right green)" │
├─────────────┼─────────┼─────────┼──────────────────┤
│ "Right" │ NULL │ "red" │ " (Right red)" │
└─────────────┴─────────┴─────────┴──────────────────┘
TABLE: _xmt_interp_p_g
┌──────────────────┬─────────┐
│ a_1 │ G │
├──────────────────┼─────────┤
│ " (Left blue)" │ "true" │
├──────────────────┼─────────┤
│ " (Left green)" │ "false" │
├──────────────────┼─────────┤
│ " (Left red)" │ "false" │
├──────────────────┼─────────┤
│ " (Right blue)" │ "false" │
├──────────────────┼─────────┤
│ " (Right green)" │ "false" │
├──────────────────┼─────────┤
│ " (Right red)" │ "true" │
├──────────────────┼─────────┤
│ "nil" │ "true" │
└──────────────────┴─────────┘
Groundings:
=== red ======================================
-- Join(0)
SELECT "red" AS G
=== (Right red) ======================================
-- Join(0)
SELECT construct2("Right", "red") AS G
=== (top) (p (Right red)) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT "true" AS G
FROM _xmt_interp_p_TU AS _xmt_interp_p_TU_2
WHERE construct2("Right", "red") = _xmt_interp_p_TU_2.a_1
----- F ------------------------------------------------------------
-- Join(0)
SELECT "false" AS G
FROM _xmt_interp_p_UF AS _xmt_interp_p_UF_2
WHERE construct2("Right", "red") = _xmt_interp_p_UF_2.a_1
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_p_G_2.G AS G
FROM _xmt_interp_p_G AS _xmt_interp_p_G_2
WHERE construct2("Right", "red") = _xmt_interp_p_G_2.a_1
=== nil ======================================
-- Join(0)
SELECT "nil" AS G
=== (top) (p nil) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT "true" AS G
FROM _xmt_interp_p_TU AS _xmt_interp_p_TU_4
WHERE "nil" = _xmt_interp_p_TU_4.a_1
----- F ------------------------------------------------------------
-- Join(0)
SELECT "false" AS G
FROM _xmt_interp_p_UF AS _xmt_interp_p_UF_4
WHERE "nil" = _xmt_interp_p_UF_4.a_1
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_p_G_4.G AS G
FROM _xmt_interp_p_G AS _xmt_interp_p_G_4
WHERE "nil" = _xmt_interp_p_G_4.a_1
=== (Left red) ======================================
-- Join(0)
SELECT construct2("Left", "red") AS G
=== (p (Left red)) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT "true" AS G
FROM _xmt_interp_p_TU AS _xmt_interp_p_TU_6
WHERE construct2("Left", "red") = _xmt_interp_p_TU_6.a_1
----- F ------------------------------------------------------------
-- Join(0)
SELECT "false" AS G
FROM _xmt_interp_p_UF AS _xmt_interp_p_UF_6
WHERE construct2("Left", "red") = _xmt_interp_p_UF_6.a_1
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_interp_p_G_6.G AS G
FROM _xmt_interp_p_G AS _xmt_interp_p_G_6
WHERE construct2("Left", "red") = _xmt_interp_p_G_6.a_1
=== (top) (not (p (Left red))) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT "true" AS G
FROM _xmt_interp_p_UF AS _xmt_interp_p_UF_6
WHERE construct2("Left", "red") = _xmt_interp_p_UF_6.a_1
----- F ------------------------------------------------------------
-- Join(0)
SELECT "false" AS G
FROM _xmt_interp_p_TU AS _xmt_interp_p_TU_6
WHERE construct2("Left", "red") = _xmt_interp_p_TU_6.a_1
----- G ------------------------------------------------------------
-- Join(0)
SELECT not_(_xmt_interp_p_G_6.G) AS G
FROM _xmt_interp_p_G AS _xmt_interp_p_G_6
WHERE construct2("Left", "red") = _xmt_interp_p_G_6.a_1
=== (top) ((_ is nil) nil) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT apply("(_ is nil)", "nil") AS G
----- F ------------------------------------------------------------
-- Join(0)
SELECT apply("(_ is nil)", "nil") AS G
----- G ------------------------------------------------------------
-- Join(0)
SELECT apply("(_ is nil)", "nil") AS G
=== blue ======================================
-- Join(0)
SELECT "blue" AS G
=== (Left blue) ======================================
-- Join(0)
SELECT construct2("Left", "blue") AS G
=== (top) ((_ is Left) (Left blue)) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT "true" AS G
FROM _xmt_tester_either_left_t AS _xmt_tester_either_left_t_11
WHERE construct2("Left", "blue") = _xmt_tester_either_left_t_11.a_1
----- F ------------------------------------------------------------
-- Join(0)
SELECT "false" AS G
FROM _xmt_tester_either_left_f AS _xmt_tester_either_left_f_11
WHERE construct2("Left", "blue") = _xmt_tester_either_left_f_11.a_1
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_tester_either_left_g_11.G AS G
FROM _xmt_tester_either_left_g AS _xmt_tester_either_left_g_11
WHERE construct2("Left", "blue") = _xmt_tester_either_left_g_11.a_1
=== (b (Left red)) ======================================
-- Join(0)
SELECT _xmt_selector_either_b_g_12.G AS G
FROM _xmt_selector_either_b_g AS _xmt_selector_either_b_g_12
WHERE construct2("Left", "red") = _xmt_selector_either_b_g_12.a_1
=== (top) (= red (b (Left red))) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT eq_("red", _xmt_selector_either_b_g_12.G) AS G
FROM _xmt_selector_either_b_g AS _xmt_selector_either_b_g_12
WHERE "red" = _xmt_selector_either_b_g_12.G
AND construct2("Left", "red") = _xmt_selector_either_b_g_12.a_1
----- F ------------------------------------------------------------
-- Join(0)
SELECT eq_("red", _xmt_selector_either_b_g_12.G) AS G
FROM _xmt_selector_either_b_g AS _xmt_selector_either_b_g_12
WHERE "red" != _xmt_selector_either_b_g_12.G
AND construct2("Left", "red") = _xmt_selector_either_b_g_12.a_1
----- G ------------------------------------------------------------
-- Join(0)
SELECT eq_("red", _xmt_selector_either_b_g_12.G) AS G
FROM _xmt_selector_either_b_g AS _xmt_selector_either_b_g_12
WHERE construct2("Left", "red") = _xmt_selector_either_b_g_12.a_1
===========================================
(check-sat)