(set-option :backend none)
(declare-const c Int)
(assert (= 2 (+ 1 (abs 1))))
(assert (= 0 (- 3 1 2)))
(assert (= 2 (+ c (abs 1))))
(assert (= 0 (- c 1 2)))
(assert (= 4 (* 2 2 -1)))
(assert (= 2 (div 4 2)))
(assert (= 1 (mod 3 2)))
(declare-const d Real)
(assert (= 2.1 (+ 1.0 (abs 1.0))))
(assert (= 0.0 (- 3.0 1.0 2.0)))
(assert (= 2.1 (+ d (abs 1.0))))
(assert (= 0.0 (- d 1.0 2.0)))
(assert (= 4.0 (* 2.0 2.0 -1.0)))
(assert (= 2.0 (div 4.0 2.0)))
(assert (= 1.0 (mod 3 2)))
(declare-fun Row (Int) Bool)
(x-interpret-pred Row (x-range 1 8 10 10))
(x-ground :debug :sql)
(x-debug solver groundings)
(x-debug db tables)
(x-debug db _xmt_interp_row_T)
------- RESULTS ------------------
(declare-const c Int)
(declare-const d Real)
(declare-fun Row (Int) Bool)
; ==== Query =============================
;-- exclude(0)
;SELECT *
; FROM (-- Join(7)
; SELECT eq_(2, left_("+", 1, abs_(1))) AS G)
; WHERE G <> "true"(assert (= 2 (+ 1 1)))
; ==== Query =============================
;-- exclude(0)
;SELECT *
; FROM (-- Join(7)
; SELECT eq_(0, left_("-", 3, 1, 2)) AS G)
; WHERE G <> "true"
; ==== Query =============================
;-- Join(0)
;SELECT apply("=", 2, apply("+", "c", abs_(1))) AS G(assert (= 2 (+ c 1)))
; ==== Query =============================
;-- Join(0)
;SELECT apply("=", 0, apply("-", "c", 1, 2)) AS G(assert (= 0 (- c 1 2)))
; ==== Query =============================
;-- exclude(0)
;SELECT *
; FROM (-- Join(7)
; SELECT eq_(4, left_("*", 2, 2, -1)) AS G)
; WHERE G <> "true"(assert false)
; ==== Query =============================
;-- exclude(0)
;SELECT *
; FROM (-- Join(7)
; SELECT eq_(2, left_("div", 4, 2)) AS G)
; WHERE G <> "true"
; ==== Query =============================
;-- exclude(0)
;SELECT *
; FROM (-- Join(7)
; SELECT eq_(1, left_("mod", 3, 2)) AS G)
; WHERE G <> "true"
; ==== Query =============================
;-- exclude(0)
;SELECT *
; FROM (-- Join(7)
; SELECT eq_(2.1, left_("+", 1.0, abs_(1.0))) AS G)
; WHERE G <> "true"(assert (= 2.1 (+ 1 1)))
; ==== Query =============================
;-- exclude(0)
;SELECT *
; FROM (-- Join(7)
; SELECT eq_(0.0, left_("-", 3.0, 1.0, 2.0)) AS G)
; WHERE G <> "true"
; ==== Query =============================
;-- Join(0)
;SELECT apply("=", 2.1, apply("+", "d", abs_(1.0))) AS G(assert (= 2.1 (+ d 1)))
; ==== Query =============================
;-- Join(0)
;SELECT apply("=", 0.0, apply("-", "d", 1.0, 2.0)) AS G(assert (= 0 (- d 1 2)))
; ==== Query =============================
;-- exclude(0)
;SELECT *
; FROM (-- Join(7)
; SELECT eq_(4.0, left_("*", 2.0, 2.0, -1.0)) AS G)
; WHERE G <> "true"(assert false)
; ==== Query =============================
;-- exclude(0)
;SELECT *
; FROM (-- Join(7)
; SELECT eq_(2.0, left_("div", 4.0, 2.0)) AS G)
; WHERE G <> "true"
; ==== Query =============================
;-- exclude(0)
;SELECT *
; FROM (-- Join(7)
; SELECT eq_(1.0, left_("mod", 3, 2)) AS G)
; WHERE G <> "true"
Groundings:
=== 2 ======================================
-- Join(0)
SELECT 2 AS G
=== 1 ======================================
-- Join(0)
SELECT 1 AS G
=== (abs 1) ======================================
-- Join(0)
SELECT abs_(1) AS G
=== (+ 1 (abs 1)) ======================================
-- Join(0)
SELECT left_("+", 1, abs_(1)) AS G
=== (top) (= 2 (+ 1 (abs 1))) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT eq_(2, left_("+", 1, abs_(1))) AS G
----- F ------------------------------------------------------------
-- Join(0)
SELECT eq_(2, left_("+", 1, abs_(1))) AS G
----- G ------------------------------------------------------------
-- Join(0)
SELECT eq_(2, left_("+", 1, abs_(1))) AS G
=== 0 ======================================
-- Join(0)
SELECT 0 AS G
=== 3 ======================================
-- Join(0)
SELECT 3 AS G
=== (- 3 1 2) ======================================
-- Join(0)
SELECT left_("-", 3, 1, 2) AS G
=== (top) (= 0 (- 3 1 2)) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT eq_(0, left_("-", 3, 1, 2)) AS G
----- F ------------------------------------------------------------
-- Join(0)
SELECT eq_(0, left_("-", 3, 1, 2)) AS G
----- G ------------------------------------------------------------
-- Join(0)
SELECT eq_(0, left_("-", 3, 1, 2)) AS G
=== c ======================================
-- Join(0)
SELECT "c" AS G
=== (+ c (abs 1)) ======================================
-- Join(0)
SELECT apply("+", "c", abs_(1)) AS G
=== (top) (= 2 (+ c (abs 1))) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT apply("=", 2, apply("+", "c", abs_(1))) AS G
----- UF -----------------------------------------------------------
-- Join(0)
SELECT apply("=", 2, apply("+", "c", abs_(1))) AS G
----- G ------------------------------------------------------------
-- Join(0)
SELECT apply("=", 2, apply("+", "c", abs_(1))) AS G
=== (- c 1 2) ======================================
-- Join(0)
SELECT apply("-", "c", 1, 2) AS G
=== (top) (= 0 (- c 1 2)) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT apply("=", 0, apply("-", "c", 1, 2)) AS G
----- UF -----------------------------------------------------------
-- Join(0)
SELECT apply("=", 0, apply("-", "c", 1, 2)) AS G
----- G ------------------------------------------------------------
-- Join(0)
SELECT apply("=", 0, apply("-", "c", 1, 2)) AS G
=== 4 ======================================
-- Join(0)
SELECT 4 AS G
=== -1 ======================================
-- Join(0)
SELECT -1 AS G
=== (* 2 2 -1) ======================================
-- Join(0)
SELECT left_("*", 2, 2, -1) AS G
=== (top) (= 4 (* 2 2 -1)) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT eq_(4, left_("*", 2, 2, -1)) AS G
----- F ------------------------------------------------------------
-- Join(0)
SELECT eq_(4, left_("*", 2, 2, -1)) AS G
----- G ------------------------------------------------------------
-- Join(0)
SELECT eq_(4, left_("*", 2, 2, -1)) AS G
=== (div 4 2) ======================================
-- Join(0)
SELECT left_("div", 4, 2) AS G
=== (top) (= 2 (div 4 2)) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT eq_(2, left_("div", 4, 2)) AS G
----- F ------------------------------------------------------------
-- Join(0)
SELECT eq_(2, left_("div", 4, 2)) AS G
----- G ------------------------------------------------------------
-- Join(0)
SELECT eq_(2, left_("div", 4, 2)) AS G
=== (mod 3 2) ======================================
-- Join(0)
SELECT left_("mod", 3, 2) AS G
=== (top) (= 1 (mod 3 2)) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT eq_(1, left_("mod", 3, 2)) AS G
----- F ------------------------------------------------------------
-- Join(0)
SELECT eq_(1, left_("mod", 3, 2)) AS G
----- G ------------------------------------------------------------
-- Join(0)
SELECT eq_(1, left_("mod", 3, 2)) AS G
=== 2.1 ======================================
-- Join(0)
SELECT 2.1 AS G
=== 1.0 ======================================
-- Join(0)
SELECT 1.0 AS G
=== (abs 1.0) ======================================
-- Join(0)
SELECT abs_(1.0) AS G
=== (+ 1.0 (abs 1.0)) ======================================
-- Join(0)
SELECT left_("+", 1.0, abs_(1.0)) AS G
=== (top) (= 2.1 (+ 1.0 (abs 1.0))) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT eq_(2.1, left_("+", 1.0, abs_(1.0))) AS G
----- F ------------------------------------------------------------
-- Join(0)
SELECT eq_(2.1, left_("+", 1.0, abs_(1.0))) AS G
----- G ------------------------------------------------------------
-- Join(0)
SELECT eq_(2.1, left_("+", 1.0, abs_(1.0))) AS G
=== 0.0 ======================================
-- Join(0)
SELECT 0.0 AS G
=== 3.0 ======================================
-- Join(0)
SELECT 3.0 AS G
=== 2.0 ======================================
-- Join(0)
SELECT 2.0 AS G
=== (- 3.0 1.0 2.0) ======================================
-- Join(0)
SELECT left_("-", 3.0, 1.0, 2.0) AS G
=== (top) (= 0.0 (- 3.0 1.0 2.0)) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT eq_(0.0, left_("-", 3.0, 1.0, 2.0)) AS G
----- F ------------------------------------------------------------
-- Join(0)
SELECT eq_(0.0, left_("-", 3.0, 1.0, 2.0)) AS G
----- G ------------------------------------------------------------
-- Join(0)
SELECT eq_(0.0, left_("-", 3.0, 1.0, 2.0)) AS G
=== d ======================================
-- Join(0)
SELECT "d" AS G
=== (+ d (abs 1.0)) ======================================
-- Join(0)
SELECT apply("+", "d", abs_(1.0)) AS G
=== (top) (= 2.1 (+ d (abs 1.0))) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT apply("=", 2.1, apply("+", "d", abs_(1.0))) AS G
----- UF -----------------------------------------------------------
-- Join(0)
SELECT apply("=", 2.1, apply("+", "d", abs_(1.0))) AS G
----- G ------------------------------------------------------------
-- Join(0)
SELECT apply("=", 2.1, apply("+", "d", abs_(1.0))) AS G
=== (- d 1.0 2.0) ======================================
-- Join(0)
SELECT apply("-", "d", 1.0, 2.0) AS G
=== (top) (= 0.0 (- d 1.0 2.0)) ======================================
----- TU -----------------------------------------------------------
-- Join(0)
SELECT apply("=", 0.0, apply("-", "d", 1.0, 2.0)) AS G
----- UF -----------------------------------------------------------
-- Join(0)
SELECT apply("=", 0.0, apply("-", "d", 1.0, 2.0)) AS G
----- G ------------------------------------------------------------
-- Join(0)
SELECT apply("=", 0.0, apply("-", "d", 1.0, 2.0)) AS G
=== 4.0 ======================================
-- Join(0)
SELECT 4.0 AS G
=== -1.0 ======================================
-- Join(0)
SELECT -1.0 AS G
=== (* 2.0 2.0 -1.0) ======================================
-- Join(0)
SELECT left_("*", 2.0, 2.0, -1.0) AS G
=== (top) (= 4.0 (* 2.0 2.0 -1.0)) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT eq_(4.0, left_("*", 2.0, 2.0, -1.0)) AS G
----- F ------------------------------------------------------------
-- Join(0)
SELECT eq_(4.0, left_("*", 2.0, 2.0, -1.0)) AS G
----- G ------------------------------------------------------------
-- Join(0)
SELECT eq_(4.0, left_("*", 2.0, 2.0, -1.0)) AS G
=== (div 4.0 2.0) ======================================
-- Join(0)
SELECT left_("div", 4.0, 2.0) AS G
=== (top) (= 2.0 (div 4.0 2.0)) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT eq_(2.0, left_("div", 4.0, 2.0)) AS G
----- F ------------------------------------------------------------
-- Join(0)
SELECT eq_(2.0, left_("div", 4.0, 2.0)) AS G
----- G ------------------------------------------------------------
-- Join(0)
SELECT eq_(2.0, left_("div", 4.0, 2.0)) AS G
=== (top) (= 1.0 (mod 3 2)) ======================================
----- T ------------------------------------------------------------
-- Join(0)
SELECT eq_(1.0, left_("mod", 3, 2)) AS G
----- F ------------------------------------------------------------
-- Join(0)
SELECT eq_(1.0, left_("mod", 3, 2)) AS G
----- G ------------------------------------------------------------
-- Join(0)
SELECT eq_(1.0, left_("mod", 3, 2)) AS G
===========================================
Tables and Views:
- Bool (table)
- _xmt_interp_row_T (table)
- _xmt_interp_row_TU (view)
- sqlite_stat1 (table)
- sqlite_stat4 (table)
TABLE: _xmt_interp_row_t
┌─────┐
│ a_1 │
├─────┤
│ 1 │
├─────┤
│ 2 │
├─────┤
│ 3 │
├─────┤
│ 4 │
├─────┤
│ 5 │
├─────┤
│ 6 │
├─────┤
│ 7 │
├─────┤
│ 8 │
├─────┤
│ 10 │
└─────┘