(set-option :backend none)
(assert (forall ((x Int)) true))
(assert (exists ((x Int)) true))
(declare-datatype Color ( ( red ) ( green ) ))
(assert (forall ((x Color)) true))
(assert (exists ((x Color)) true))
(declare-fun p (Color) Bool)
(assert (forall ((x Color)) (p x)))
(assert (exists ((x Color)) (p x)))
(declare-fun q (Int) Bool)
(assert (forall ((x Int)) (q x)))
(declare-fun r (Bool) Bool)
(assert (not (exists ((x Bool)) (r x))))
(assert (forall ((x Bool)) (=> (and (r x) (r x)) false)))
(x-ground :debug :sql)
(x-debug solver groundings)
(x-debug db tables)
------- RESULTS ------------------
(declare-datatype Color ((red) (green)))
(declare-fun p (Color) Bool)
(declare-fun q (Int) Bool)
(declare-fun r (Bool) Bool)
; ==== Query =============================
;-- exclude(0)
;SELECT *
; FROM (-- Agg (7)
; SELECT or_aggregate(G) as G
; FROM (SELECT "false" AS G
; UNION ALL
; -- Join(14)
; SELECT "true" AS G))
; WHERE G <> "true"
; ==== Query =============================
;-- exclude(0)
;SELECT *
; FROM (-- Agg (7)
; SELECT or_aggregate(G) as G
; FROM (SELECT "false" AS G
; UNION ALL
; -- Join(14)
; SELECT "true" AS G))
; WHERE G <> "true"
; ==== Query =============================
;-- Agg (0)
;SELECT G as G
; FROM (-- Join(7)
; SELECT _xmt_sort_color_5.G AS x,
; apply("p", _xmt_sort_color_5.G) AS G
; FROM _xmt_sort_color AS _xmt_sort_color_5)(assert (p green))
(assert (p red))
; ==== Query =============================
;-- Agg (0)
;SELECT or_aggregate(G) as G
; FROM (SELECT NULL AS x, "false" AS G
; UNION ALL
; -- Join(7)
; SELECT _xmt_sort_color_5.G AS x,
; apply("p", _xmt_sort_color_5.G) AS G
; FROM _xmt_sort_color AS _xmt_sort_color_5)(assert (or (p green) (p red)))
; ==== Query =============================
;-- Agg (0)
;SELECT "(forall ((x Int)) " || G || ")" as G
; FROM (-- Join(7)
; SELECT "x" AS x,
; apply("q", "x") AS G)(assert (forall ((x Int)) (q x)))
; ==== Query =============================
;-- Agg (0)
;SELECT and_aggregate(G) as G
; FROM (-- Join(7)
; SELECT Bool_12.G AS x,
; apply("not", apply("r", Bool_12.G)) AS G
; FROM Bool AS Bool_12)(assert (and (not (r true)) (not (r false))))
; ==== Query =============================
;-- Agg (0)
;SELECT G as G
; FROM (-- Join(7)
; SELECT Bool_12.G AS x,
; apply("not", apply("r", Bool_12.G)) AS G
; FROM Bool AS Bool_12)(assert (not (r true)))
(assert (not (r false)))
Groundings:
=== true ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT "true" AS G
----- F ------------------------------------------------------------
SELECT "true" AS G WHERE FALSE
----- G ------------------------------------------------------------
-- Join(0)
SELECT "true" AS G
=== (top) (forall ((x Int)) true) ======================================
----- T ------------------------------------------------------------
SELECT "true" AS G WHERE FALSE
----- F ------------------------------------------------------------
SELECT "true" AS G WHERE FALSE
----- G ------------------------------------------------------------
SELECT "true" AS G WHERE FALSE
=== (top) (exists ((x Int)) true) ======================================
----- T ------------------------------------------------------------
-- Agg (0)
SELECT or_aggregate(G) as G
FROM (-- Join(7)
SELECT "true" AS G)
----- F ------------------------------------------------------------
-- Agg (0)
SELECT or_aggregate(G) as G
FROM (SELECT "false" AS G
UNION ALL
-- Join(7)
SELECT "true" AS G)
----- G ------------------------------------------------------------
-- Agg (0)
SELECT or_aggregate(G) as G
FROM (SELECT "false" AS G
UNION ALL
-- Join(7)
SELECT "true" AS G)
=== (top) (forall ((x Color)) true) ======================================
----- T ------------------------------------------------------------
SELECT "true" AS G WHERE FALSE
----- F ------------------------------------------------------------
SELECT "true" AS G WHERE FALSE
----- G ------------------------------------------------------------
SELECT "true" AS G WHERE FALSE
=== (top) (exists ((x Color)) true) ======================================
----- T ------------------------------------------------------------
-- Agg (0)
SELECT or_aggregate(G) as G
FROM (-- Join(7)
SELECT "true" AS G)
----- F ------------------------------------------------------------
-- Agg (0)
SELECT or_aggregate(G) as G
FROM (SELECT "false" AS G
UNION ALL
-- Join(7)
SELECT "true" AS G)
----- G ------------------------------------------------------------
-- Agg (0)
SELECT or_aggregate(G) as G
FROM (SELECT "false" AS G
UNION ALL
-- Join(7)
SELECT "true" AS G)
=== x ======================================
-- Join(0)
SELECT _xmt_sort_color_5.G AS x,
_xmt_sort_color_5.G AS G
FROM _xmt_sort_color AS _xmt_sort_color_5
=== (p x) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_color_5.G AS x,
apply("p", _xmt_sort_color_5.G) AS G
FROM _xmt_sort_color AS _xmt_sort_color_5
----- UF -----------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_color_5.G AS x,
apply("p", _xmt_sort_color_5.G) AS G
FROM _xmt_sort_color AS _xmt_sort_color_5
----- G ------------------------------------------------------------
-- Join(0)
SELECT _xmt_sort_color_5.G AS x,
apply("p", _xmt_sort_color_5.G) AS G
FROM _xmt_sort_color AS _xmt_sort_color_5
=== (top) (forall ((x Color)) (p x)) ======================================
----- TU -----------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, "true" AS G
UNION ALL
-- Join(7)
SELECT _xmt_sort_color_5.G AS x,
apply("p", _xmt_sort_color_5.G) AS G
FROM _xmt_sort_color AS _xmt_sort_color_5)
----- UF -----------------------------------------------------------
-- Agg (0)
SELECT G as G
FROM (-- Join(7)
SELECT _xmt_sort_color_5.G AS x,
apply("p", _xmt_sort_color_5.G) AS G
FROM _xmt_sort_color AS _xmt_sort_color_5)
----- G ------------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, "true" AS G
UNION ALL
-- Join(7)
SELECT _xmt_sort_color_5.G AS x,
apply("p", _xmt_sort_color_5.G) AS G
FROM _xmt_sort_color AS _xmt_sort_color_5)
=== (top) (exists ((x Color)) (p x)) ======================================
----- TU -----------------------------------------------------------
-- Agg (0)
SELECT or_aggregate(G) as G
FROM (-- Join(7)
SELECT _xmt_sort_color_5.G AS x,
apply("p", _xmt_sort_color_5.G) AS G
FROM _xmt_sort_color AS _xmt_sort_color_5)
----- UF -----------------------------------------------------------
-- Agg (0)
SELECT or_aggregate(G) as G
FROM (SELECT NULL AS x, "false" AS G
UNION ALL
-- Join(7)
SELECT _xmt_sort_color_5.G AS x,
apply("p", _xmt_sort_color_5.G) AS G
FROM _xmt_sort_color AS _xmt_sort_color_5)
----- G ------------------------------------------------------------
-- Agg (0)
SELECT or_aggregate(G) as G
FROM (SELECT NULL AS x, "false" AS G
UNION ALL
-- Join(7)
SELECT _xmt_sort_color_5.G AS x,
apply("p", _xmt_sort_color_5.G) AS G
FROM _xmt_sort_color AS _xmt_sort_color_5)
=== x ======================================
-- Join(0)
SELECT "x" AS x,
"x" AS G
=== (q x) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT "x" AS x,
apply("q", "x") AS G
----- UF -----------------------------------------------------------
-- Join(0)
SELECT "x" AS x,
apply("q", "x") AS G
----- G ------------------------------------------------------------
-- Join(0)
SELECT "x" AS x,
apply("q", "x") AS G
=== (top) (forall ((x Int)) (q x)) ======================================
----- TU -----------------------------------------------------------
-- Agg (0)
SELECT "(forall ((x Int)) " || and_aggregate(G) || ")" as G
FROM (SELECT NULL AS x, "true" AS G
UNION ALL
-- Join(7)
SELECT "x" AS x,
apply("q", "x") AS G)
----- UF -----------------------------------------------------------
-- Agg (0)
SELECT "(forall ((x Int)) " || G || ")" as G
FROM (-- Join(7)
SELECT "x" AS x,
apply("q", "x") AS G)
----- G ------------------------------------------------------------
-- Agg (0)
SELECT "(forall ((x Int)) " || and_aggregate(G) || ")" as G
FROM (SELECT NULL AS x, "true" AS G
UNION ALL
-- Join(7)
SELECT "x" AS x,
apply("q", "x") AS G)
=== x ======================================
-- Join(0)
SELECT Bool_12.G AS x,
Bool_12.G AS G
FROM Bool AS Bool_12
=== (r x) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT Bool_12.G AS x,
apply("r", Bool_12.G) AS G
FROM Bool AS Bool_12
----- UF -----------------------------------------------------------
-- Join(0)
SELECT Bool_12.G AS x,
apply("r", Bool_12.G) AS G
FROM Bool AS Bool_12
----- G ------------------------------------------------------------
-- Join(0)
SELECT Bool_12.G AS x,
apply("r", Bool_12.G) AS G
FROM Bool AS Bool_12
=== (exists ((x Bool)) (r x)) ======================================
----- TU -----------------------------------------------------------
-- Agg (0)
SELECT or_aggregate(G) as G
FROM (-- Join(7)
SELECT Bool_12.G AS x,
apply("r", Bool_12.G) AS G
FROM Bool AS Bool_12)
----- UF -----------------------------------------------------------
-- Agg (0)
SELECT or_aggregate(G) as G
FROM (SELECT NULL AS x, "false" AS G
UNION ALL
-- Join(7)
SELECT Bool_12.G AS x,
apply("r", Bool_12.G) AS G
FROM Bool AS Bool_12)
----- G ------------------------------------------------------------
-- Agg (0)
SELECT or_aggregate(G) as G
FROM (SELECT NULL AS x, "false" AS G
UNION ALL
-- Join(7)
SELECT Bool_12.G AS x,
apply("r", Bool_12.G) AS G
FROM Bool AS Bool_12)
=== (top) (not (exists ((x Bool)) (r x))) ======================================
----- TU -----------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, "true" AS G
UNION ALL
-- Join(7)
SELECT Bool_12.G AS x,
apply("not", apply("r", Bool_12.G)) AS G
FROM Bool AS Bool_12)
----- UF -----------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (-- Join(7)
SELECT Bool_12.G AS x,
apply("not", apply("r", Bool_12.G)) AS G
FROM Bool AS Bool_12)
----- G ------------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, "true" AS G
UNION ALL
-- Join(7)
SELECT Bool_12.G AS x,
apply("not", apply("r", Bool_12.G)) AS G
FROM Bool AS Bool_12)
=== (not (r x)) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT Bool_12.G AS x,
apply("not", apply("r", Bool_12.G)) AS G
FROM Bool AS Bool_12
----- UF -----------------------------------------------------------
-- Join(0)
SELECT Bool_12.G AS x,
apply("not", apply("r", Bool_12.G)) AS G
FROM Bool AS Bool_12
----- G ------------------------------------------------------------
-- Join(0)
SELECT Bool_12.G AS x,
apply("not", apply("r", Bool_12.G)) AS G
FROM Bool AS Bool_12
=== false ======================================
----- T ------------------------------------------------------------
SELECT "true" AS G WHERE FALSE
----- F ------------------------------------------------------------
-- Join(0)
SELECT "false" AS G
----- G ------------------------------------------------------------
-- Join(0)
SELECT "false" AS G
=== (or (not (r x)) false) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT Bool_12.G AS x,
apply("not", apply("r", Bool_12.G)) AS G
FROM Bool AS Bool_12
----- UF -----------------------------------------------------------
-- Join(0)
SELECT Bool_12.G AS x,
apply("not", apply("r", Bool_12.G)) AS G
FROM Bool AS Bool_12
----- G ------------------------------------------------------------
-- Join(0)
SELECT Bool_12.G AS x,
apply("not", apply("r", Bool_12.G)) AS G
FROM Bool AS Bool_12
=== (top) (forall ((x Bool)) (or (not (r x)) false)) ======================================
----- TU -----------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, "true" AS G
UNION ALL
-- Join(7)
SELECT Bool_12.G AS x,
apply("not", apply("r", Bool_12.G)) AS G
FROM Bool AS Bool_12)
----- UF -----------------------------------------------------------
-- Agg (0)
SELECT G as G
FROM (-- Join(7)
SELECT Bool_12.G AS x,
apply("not", apply("r", Bool_12.G)) AS G
FROM Bool AS Bool_12)
----- G ------------------------------------------------------------
-- Agg (0)
SELECT and_aggregate(G) as G
FROM (SELECT NULL AS x, "true" AS G
UNION ALL
-- Join(7)
SELECT Bool_12.G AS x,
apply("not", apply("r", Bool_12.G)) AS G
FROM Bool AS Bool_12)
===========================================
Tables and Views:
- Bool (table)
- _xmt_sort_color (table)
- sqlite_stat1 (table)
- sqlite_stat4 (table)