Add more abduction regressions (#7461)

Fixes #5848.

This also fixes an issue leftover from #6605 where a spurious assertion failure was thrown.

Also introduces subfolder regress/regress1/abduction.

diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp
index f3c595720a92ccf88ba94f6901a742bcbd58444a..1888069bce8fde8c8fce56250068d0f0a9168200 100644 (file)
--- a/src/theory/builtin/theory_builtin_type_rules.cpp
+++ b/src/theory/builtin/theory_builtin_type_rules.cpp
@@ -42,7 +42,8 @@ typedef expr::Attribute<GroundTermAttributeId, Node> GroundTermAttribute;
 
 Node SortProperties::mkGroundTerm(TypeNode type)
 {
-  Assert(type.getKind() == kind::SORT_TYPE);
+  // we typically use this method for sorts, although there are other types
+  // where it is used as well, e.g. arrays that are not closed enumerable.
   GroundTermAttribute gta;
   if (type.hasAttribute(gta))
   {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b80fd890b27df4b4054cdb3de1a52bd3056a043c..1c81316c3bff82911ab145eb774df3cd1b6e0bd6 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1489,7 +1489,22 @@ set(regress_0_tests
 # Regression level 1 tests
 
 set(regress_1_tests
-  regress1/abduct-dt.smt2
+  regress1/abduction/sygus-abduct-test-user.smt2
+  regress1/abduction/issue5848-4.smt2
+  regress1/abduction/issue5848-2.smt2
+  regress1/abduction/issue5848.smt2
+  regress1/abduction/issue6605-1.smt2
+  regress1/abduction/abduct-dt.smt2
+  regress1/abduction/sygus-abduct-test-ccore.smt2
+  regress1/abduction/sygus-abduct-test.smt2
+  regress1/abduction/abd-simple-conj-4.smt2
+  regress1/abduction/abduction_streq.readable.smt2
+  regress1/abduction/yoni-true-sol.smt2
+  regress1/abduction/uf-abduct.smt2
+  regress1/abduction/abduction_1255.corecstrs.readable.smt2
+  regress1/abduction/abduction-no-pbe-sym-break.smt2
+  regress1/abduction/issue5848-3-trivial-no-abduct.smt2
+  regress1/abduction/sygus-abduct-ex1-grammar.smt2
   regress1/arith/arith-brab-test.smt2
   regress1/arith/arith-int-004.cvc.smt2
   regress1/arith/arith-int-011.cvc.smt2
@@ -2322,15 +2337,7 @@ set(regress_1_tests
   regress1/strings/update-ex1.smt2
   regress1/strings/update-ex2.smt2
   regress1/strings/username_checker_min.smt2
-  regress1/sygus-abduct-ex1-grammar.smt2
-  regress1/sygus-abduct-test.smt2
-  regress1/sygus-abduct-test-ccore.smt2
-  regress1/sygus-abduct-test-user.smt2
   regress1/sygus/VC22_a.sy
-  regress1/sygus/abd-simple-conj-4.smt2
-  regress1/sygus/abduction_1255.corecstrs.readable.smt2
-  regress1/sygus/abduction_streq.readable.smt2
-  regress1/sygus/abduction-no-pbe-sym-break.smt2
   regress1/sygus/abv.sy
   regress1/sygus/array-grammar-store.sy
   regress1/sygus/array_search_5-Q-easy.sy
@@ -2476,10 +2483,8 @@ set(regress_1_tests
   regress1/sygus/trivial-stream.sy
   regress1/sygus/twolets1.sy
   regress1/sygus/twolets2-orig.sy
-  regress1/sygus/uf-abduct.smt2
   regress1/sygus/unbdd_inv_gen_winf1.sy
   regress1/sygus/univ_2-long-repeat.sy
-  regress1/sygus/yoni-true-sol.smt2
   regress1/sym/q-constant.smt2
   regress1/sym/q-function.smt2
   regress1/sym/qf-function.smt2

diff --git a/test/regress/regress1/abduct-dt.smt2 b/test/regress/regress1/abduct-dt.smt2
deleted file mode 100644 (file)
index d72d15a..0000000
--- a/test/regress/regress1/abduct-dt.smt2
+++ /dev/null
@@ -1,8 +0,0 @@
-; COMMAND-LINE: --produce-abducts
-; SCRUBBER: grep -v -E '(\(define-fun)'
-; EXIT: 0
-(set-logic ALL)
-(declare-datatypes ((List 0)) (((nil) (cons (head Int) (tail List)))))
-(declare-fun x () List)
-(assert (distinct x nil))
-(get-abduct A (= x (cons (head x) (tail x))))

diff --git a/test/regress/regress1/abduction/abd-simple-conj-4.smt2 b/test/regress/regress1/abduction/abd-simple-conj-4.smt2
new file mode 100644 (file)
index 0000000..98bf70f
--- /dev/null
+++ b/test/regress/regress1/abduction/abd-simple-conj-4.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --produce-abducts --sygus-core-connective
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic QF_LIA)
+(set-option :produce-abducts true)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(declare-fun w () Int)
+(declare-fun u () Int)
+(declare-fun v () Int)
+(assert (>= x 0))
+(get-abduct A (>= (+ x y z w u v) 2))

diff --git a/test/regress/regress1/abduction/abduct-dt.smt2 b/test/regress/regress1/abduction/abduct-dt.smt2
new file mode 100644 (file)
index 0000000..d72d15a
--- /dev/null
+++ b/test/regress/regress1/abduction/abduct-dt.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-datatypes ((List 0)) (((nil) (cons (head Int) (tail List)))))
+(declare-fun x () List)
+(assert (distinct x nil))
+(get-abduct A (= x (cons (head x) (tail x))))

diff --git a/test/regress/regress1/abduction/abduction-no-pbe-sym-break.smt2 b/test/regress/regress1/abduction/abduction-no-pbe-sym-break.smt2
new file mode 100644 (file)
index 0000000..79fa4f2
--- /dev/null
+++ b/test/regress/regress1/abduction/abduction-no-pbe-sym-break.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+
+(set-logic UF)
+(set-option :produce-abducts true)
+(declare-const A Bool)
+(declare-const B Bool)
+(declare-const C Bool)
+(assert (=> A C))
+(get-abduct D (=> A B))

diff --git a/test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2 b/test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2
new file mode 100644 (file)
index 0000000..1595b08
--- /dev/null
+++ b/test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2
@@ -0,0 +1,75 @@
+; COMMAND-LINE: --produce-abducts --sygus-core-connective
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+
+
+(set-info :smt-lib-version |2.6|)
+(set-logic QF_SLIA)
+(set-info :source |
+Generated by: Andrew Reynolds
+Generated on: 2018-04-25
+Generator: Kudzu, converted to v2.6 by CVC4
+Application: Symbolic Execution of Javascript
+Target solver: Kaluza
+Publications: "A symbolic execution framework for JavaScript" by P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song, 2010.
+|)
+(set-info :license |"https://creativecommons.org/licenses/by/4.0/"|)
+(set-info :category |"industrial"|)
+(set-info :status unknown)
+(declare-fun T_1 () Bool)
+(declare-fun T_10 () Bool)
+(declare-fun T_11 () Bool)
+(declare-fun T_12 () Bool)
+(declare-fun T_13 () Bool)
+(declare-fun T_14 () Bool)
+(declare-fun T_2 () Bool)
+(declare-fun T_3 () Bool)
+(declare-fun T_4 () Bool)
+(declare-fun T_5 () Bool)
+(declare-fun T_6 () Bool)
+(declare-fun T_7 () Bool)
+(declare-fun T_8 () Bool)
+(declare-fun T_9 () Bool)
+(declare-fun T_a () Bool)
+(declare-fun T_b () Bool)
+(declare-fun T_c () Bool)
+(declare-fun T_d () Bool)
+(declare-fun T_e () Bool)
+(declare-fun T_f () Bool)
+(declare-fun var_0xINPUT_245549 () String)
+(assert (= T_1 (not (= "6JX7G3VKFq" var_0xINPUT_245549))))
+(assert T_1)
+(assert (= T_2 (not (= "" var_0xINPUT_245549))))
+(assert T_2)
+(assert (= T_3 (not (= var_0xINPUT_245549 ""))))
+(assert T_3)
+(assert (= T_4 (not (= "" var_0xINPUT_245549))))
+(assert T_4)
+(assert (= T_5 (= var_0xINPUT_245549 "")))
+(assert (= T_6 (not T_5)))
+(assert T_6)
+(assert (= T_7 (not (= "" var_0xINPUT_245549))))
+(assert T_7)
+(assert (= T_8 (not (= "" var_0xINPUT_245549))))
+(assert T_8)
+(assert (= T_9 (not (= var_0xINPUT_245549 ""))))
+(assert T_9)
+(assert (= T_a (= var_0xINPUT_245549 "")))
+(assert (= T_b (not T_a)))
+(assert T_b)
+(assert (= T_c (not (= "" var_0xINPUT_245549))))
+(assert T_c)
+(assert (= T_d (not (= var_0xINPUT_245549 ""))))
+(assert T_d)
+(assert (= T_e (not (= "" var_0xINPUT_245549))))
+(assert T_e)
+(assert (= T_f (= var_0xINPUT_245549 "")))
+(assert (= T_10 (not T_f)))
+(assert T_10)
+(assert (= T_11 (not (= "" var_0xINPUT_245549))))
+(assert T_11)
+(assert (= T_12 (= var_0xINPUT_245549 "Example:")))
+(assert (= T_13 (not T_12)))
+(assert T_13)
+(assert (= T_14 (not (= var_0xINPUT_245549 "CQALcCP5TB"))))
+(get-abduct A (not T_14))

diff --git a/test/regress/regress1/abduction/abduction_streq.readable.smt2 b/test/regress/regress1/abduction/abduction_streq.readable.smt2
new file mode 100644 (file)
index 0000000..b466ab3
--- /dev/null
+++ b/test/regress/regress1/abduction/abduction_streq.readable.smt2
@@ -0,0 +1,43 @@
+; COMMAND-LINE: --produce-abducts --sygus-core-connective
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+
+(set-info :smt-lib-version |2.6|)
+(set-logic QF_SLIA)
+(set-info :source |
+Generated by: Andrew Reynolds
+Generated on: 2018-04-25
+Generator: Kudzu, converted to v2.6 by CVC4
+Application: Symbolic Execution of Javascript
+Target solver: Kaluza
+Publications: "A symbolic execution framework for JavaScript" by P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song, 2010.
+|)
+(set-info :license |"https://creativecommons.org/licenses/by/4.0/"|)
+(set-info :category |"industrial"|)
+(set-info :status unknown)
+(declare-fun I0_2 () Int)
+(declare-fun I1_2 () Int)
+(declare-fun I2_2 () Int)
+(declare-fun PCTEMP_LHS_1 () String)
+(declare-fun T1_2 () String)
+(declare-fun T2_2 () String)
+(declare-fun T3_2 () String)
+(declare-fun T_2 () Bool)
+(declare-fun T_4 () Bool)
+(declare-fun T_5 () Bool)
+(declare-fun var_0xINPUT_19 () String)
+(assert (= I0_2 (- 5 0)))
+(assert (<= 0 0))
+(assert (<= 0 5))
+(assert (<= 5 I1_2))
+(assert (= I2_2 I1_2))
+(assert (= I0_2 (str.len PCTEMP_LHS_1)))
+(assert (= var_0xINPUT_19 ( str.++ T1_2 T2_2 )))
+(assert (= T2_2 ( str.++ PCTEMP_LHS_1 T3_2 )))
+(assert (= 0 (str.len T1_2)))
+(assert (= I1_2 (str.len var_0xINPUT_19)))
+(assert (= T_2 (= PCTEMP_LHS_1 "Hello")))
+(assert T_2)
+(assert (= T_4 (= PCTEMP_LHS_1 "hello")))
+(assert (= T_5 (not T_4)))
+(get-abduct A T_5)

diff --git a/test/regress/regress1/abduction/issue5848-2.smt2 b/test/regress/regress1/abduction/issue5848-2.smt2
new file mode 100644 (file)
index 0000000..36716c4
--- /dev/null
+++ b/test/regress/regress1/abduction/issue5848-2.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-fun v9 () Bool)
+(get-abduct A (or true v9))

diff --git a/test/regress/regress1/abduction/issue5848-3-trivial-no-abduct.smt2 b/test/regress/regress1/abduction/issue5848-3-trivial-no-abduct.smt2
new file mode 100644 (file)
index 0000000..b64e27b
--- /dev/null
+++ b/test/regress/regress1/abduction/issue5848-3-trivial-no-abduct.smt2
@@ -0,0 +1,5 @@
+; COMMAND-LINE: --produce-abducts
+; EXPECT: none
+(set-logic ALL)
+(assert (= 0.0 (sqrt 1.0)))
+(get-abduct A false)

diff --git a/test/regress/regress1/abduction/issue5848-4.smt2 b/test/regress/regress1/abduction/issue5848-4.smt2
new file mode 100644 (file)
index 0000000..93cd8f5
--- /dev/null
+++ b/test/regress/regress1/abduction/issue5848-4.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --produce-abducts
+; EXPECT: none
+(set-logic UFLRA)
+(declare-sort S0 0)
+(declare-fun S0-0 () S0)
+(declare-fun S0-1 () S0)
+(declare-fun v87 () Bool)
+(get-abduct A (and false (exists ((q117 S0)) (or v87 (and (= S0-1 q117) (= q117 S0-0))))))

diff --git a/test/regress/regress1/abduction/issue5848.smt2 b/test/regress/regress1/abduction/issue5848.smt2
new file mode 100644 (file)
index 0000000..7b87612
--- /dev/null
+++ b/test/regress/regress1/abduction/issue5848.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-fun a () Int)
+(assert (= (mod 0 a) 0))
+(get-abduct A (= a 1))

diff --git a/test/regress/regress1/abduction/issue6605-1.smt2 b/test/regress/regress1/abduction/issue6605-1.smt2
new file mode 100644 (file)
index 0000000..a33fdd9
--- /dev/null
+++ b/test/regress/regress1/abduction/issue6605-1.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(set-option :produce-abducts true)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun c () Int)
+(assert (= (>= b c) (>= 0 a)))
+(assert (= c a))
+(get-abduct d (<= a b))

diff --git a/test/regress/regress1/abduction/sygus-abduct-ex1-grammar.smt2 b/test/regress/regress1/abduction/sygus-abduct-ex1-grammar.smt2
new file mode 100644 (file)
index 0000000..bda2376
--- /dev/null
+++ b/test/regress/regress1/abduction/sygus-abduct-ex1-grammar.smt2
@@ -0,0 +1,28 @@
+; COMMAND-LINE: --produce-abducts --sygus-stream --sygus-abort-size=3
+; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.")
+; SCRUBBER: sed -e 's/.*(>= j (+ 1 1))/SPURIOUS/; s/(define-fun.*//; /^$/d'
+; EXIT: 1
+
+(set-logic QF_LIA)
+(set-option :produce-abducts true)
+
+(declare-fun n () Int)
+(declare-fun m () Int)
+(declare-fun i () Int)
+(declare-fun j () Int)
+
+(assert (and (>= n 0) (>= m 0)))
+(assert (< n i))
+(assert (< (+ i j) m))
+
+; This test ensures that (>= j (+ 1 1)) is not printed as a solution,
+; since it is spurious: (>= j 0) is a stronger solution and will be enumerated
+; first.
+(get-abduct A 
+  (<= n m)
+  ((GA Bool) (GI Int))
+  (
+  (GA Bool ((>= GI GI)))
+  (GI Int ((+ GI GI) (- GI) i j 0 1))
+  )
+)

diff --git a/test/regress/regress1/abduction/sygus-abduct-test-ccore.smt2 b/test/regress/regress1/abduction/sygus-abduct-test-ccore.smt2
new file mode 100644 (file)
index 0000000..86f5fe1
--- /dev/null
+++ b/test/regress/regress1/abduction/sygus-abduct-test-ccore.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --produce-abducts --sygus-core-connective
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+
+(set-logic QF_UFLIRA)
+(declare-fun n () Int)
+(declare-fun m () Int)
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(assert (>= n 1))
+(assert (and (<= n x)(<= x (+ n 5))))
+(assert (and (<= 1 y)(<= y m)))
+
+(get-abduct A (not (< x y)))

diff --git a/test/regress/regress1/abduction/sygus-abduct-test-user.smt2 b/test/regress/regress1/abduction/sygus-abduct-test-user.smt2
new file mode 100644 (file)
index 0000000..bb02ebc
--- /dev/null
+++ b/test/regress/regress1/abduction/sygus-abduct-test-user.smt2
@@ -0,0 +1,31 @@
+; COMMAND-LINE: --produce-abducts
+; COMMAND-LINE: --produce-abducts --sygus-core-connective
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic QF_UFLIRA)
+(set-option :produce-abducts true)
+(declare-fun n () Int)
+(declare-fun m () Int)
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(assert (>= n 1))
+(assert (and (<= n x)(<= x (+ n 5))))
+(assert (and (<= 1 y)(<= y m)))
+
+; Generate a predicate A that is consistent with the above axioms (i.e.
+; their conjunction is SAT), and is such that the conjunction of the above
+; axioms, A and the negation of the conjecture below are UNSAT.
+; The signature of A is below grammar.
+(get-abduct A (not (< x y))
+
+; the grammar for the abduct-to-synthesize
+; notice it does not permit the sygus-core-connective algorithm; this regression
+; tests that we ignore this option properly.
+((Start Bool) (StartInt Int))
+(
+(Start Bool ((< StartInt StartInt)))
+(StartInt Int (n m (+ StartInt StartInt) 0 1))
+)
+
+)

diff --git a/test/regress/regress1/abduction/sygus-abduct-test.smt2 b/test/regress/regress1/abduction/sygus-abduct-test.smt2
new file mode 100644 (file)
index 0000000..ed1ea6d
--- /dev/null
+++ b/test/regress/regress1/abduction/sygus-abduct-test.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --produce-abducts --sygus-stream --sygus-abort-size=2
+; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 1
+
+(set-logic QF_UFLIRA)
+(declare-fun n () Int)
+(declare-fun m () Int)
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(assert (>= n 1))
+(assert (and (<= n x)(<= x (+ n 5))))
+(assert (and (<= 1 y)(<= y m)))
+
+(get-abduct A (not (< x y)))

diff --git a/test/regress/regress1/abduction/uf-abduct.smt2 b/test/regress/regress1/abduction/uf-abduct.smt2
new file mode 100644 (file)
index 0000000..bfcfe39
--- /dev/null
+++ b/test/regress/regress1/abduction/uf-abduct.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic HO_UFLIA)
+(declare-fun f (Int) Int)
+(declare-fun a () Int)
+(assert (and (<= 0 a) (< a 4)))
+(get-abduct ensureF (or (> (f 0) 0) (> (f 1) 0) (> (f 2) 0) (> (f 3) 0)))

diff --git a/test/regress/regress1/abduction/yoni-true-sol.smt2 b/test/regress/regress1/abduction/yoni-true-sol.smt2
new file mode 100644 (file)
index 0000000..464f7c7
--- /dev/null
+++ b/test/regress/regress1/abduction/yoni-true-sol.smt2
@@ -0,0 +1,20 @@
+; COMMAND-LINE: --produce-abducts
+; EXPECT: (define-fun A () Bool (>= j i))
+(set-logic QF_LIA)
+(set-option :produce-abducts true)
+(declare-fun n () Int)
+(declare-fun m () Int)
+(declare-fun i () Int)
+(declare-fun j () Int)
+(assert (and (>= n 0) (>= m 0)))
+(assert (< n i))
+(assert (< (+ i j) m))
+(get-abduct A
+  (<= n m)
+  ((GA Bool) (GJ Int) (GI Int))
+  (
+  (GA Bool ((>= GJ GI)))
+  (GJ Int ( j))
+  (GI Int ( i))
+  )
+)

diff --git a/test/regress/regress1/sygus-abduct-ex1-grammar.smt2 b/test/regress/regress1/sygus-abduct-ex1-grammar.smt2
deleted file mode 100644 (file)
index bda2376..0000000
--- a/test/regress/regress1/sygus-abduct-ex1-grammar.smt2
+++ /dev/null
@@ -1,28 +0,0 @@
-; COMMAND-LINE: --produce-abducts --sygus-stream --sygus-abort-size=3
-; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.")
-; SCRUBBER: sed -e 's/.*(>= j (+ 1 1))/SPURIOUS/; s/(define-fun.*//; /^$/d'
-; EXIT: 1
-
-(set-logic QF_LIA)
-(set-option :produce-abducts true)
-
-(declare-fun n () Int)
-(declare-fun m () Int)
-(declare-fun i () Int)
-(declare-fun j () Int)
-
-(assert (and (>= n 0) (>= m 0)))
-(assert (< n i))
-(assert (< (+ i j) m))
-
-; This test ensures that (>= j (+ 1 1)) is not printed as a solution,
-; since it is spurious: (>= j 0) is a stronger solution and will be enumerated
-; first.
-(get-abduct A 
-  (<= n m)
-  ((GA Bool) (GI Int))
-  (
-  (GA Bool ((>= GI GI)))
-  (GI Int ((+ GI GI) (- GI) i j 0 1))
-  )
-)

diff --git a/test/regress/regress1/sygus-abduct-test-ccore.smt2 b/test/regress/regress1/sygus-abduct-test-ccore.smt2
deleted file mode 100644 (file)
index 86f5fe1..0000000
--- a/test/regress/regress1/sygus-abduct-test-ccore.smt2
+++ /dev/null
@@ -1,15 +0,0 @@
-; COMMAND-LINE: --produce-abducts --sygus-core-connective
-; SCRUBBER: grep -v -E '(\(define-fun)'
-; EXIT: 0
-
-(set-logic QF_UFLIRA)
-(declare-fun n () Int)
-(declare-fun m () Int)
-(declare-fun x () Int)
-(declare-fun y () Int)
-
-(assert (>= n 1))
-(assert (and (<= n x)(<= x (+ n 5))))
-(assert (and (<= 1 y)(<= y m)))
-
-(get-abduct A (not (< x y)))

diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/sygus-abduct-test-user.smt2
deleted file mode 100644 (file)
index bb02ebc..0000000
--- a/test/regress/regress1/sygus-abduct-test-user.smt2
+++ /dev/null
@@ -1,31 +0,0 @@
-; COMMAND-LINE: --produce-abducts
-; COMMAND-LINE: --produce-abducts --sygus-core-connective
-; SCRUBBER: grep -v -E '(\(define-fun)'
-; EXIT: 0
-(set-logic QF_UFLIRA)
-(set-option :produce-abducts true)
-(declare-fun n () Int)
-(declare-fun m () Int)
-(declare-fun x () Int)
-(declare-fun y () Int)
-
-(assert (>= n 1))
-(assert (and (<= n x)(<= x (+ n 5))))
-(assert (and (<= 1 y)(<= y m)))
-
-; Generate a predicate A that is consistent with the above axioms (i.e.
-; their conjunction is SAT), and is such that the conjunction of the above
-; axioms, A and the negation of the conjecture below are UNSAT.
-; The signature of A is below grammar.
-(get-abduct A (not (< x y))
-
-; the grammar for the abduct-to-synthesize
-; notice it does not permit the sygus-core-connective algorithm; this regression
-; tests that we ignore this option properly.
-((Start Bool) (StartInt Int))
-(
-(Start Bool ((< StartInt StartInt)))
-(StartInt Int (n m (+ StartInt StartInt) 0 1))
-)
-
-)

diff --git a/test/regress/regress1/sygus-abduct-test.smt2 b/test/regress/regress1/sygus-abduct-test.smt2
deleted file mode 100644 (file)
index ed1ea6d..0000000
--- a/test/regress/regress1/sygus-abduct-test.smt2
+++ /dev/null
@@ -1,16 +0,0 @@
-; COMMAND-LINE: --produce-abducts --sygus-stream --sygus-abort-size=2
-; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
-; SCRUBBER: grep -v -E '(\(define-fun)'
-; EXIT: 1
-
-(set-logic QF_UFLIRA)
-(declare-fun n () Int)
-(declare-fun m () Int)
-(declare-fun x () Int)
-(declare-fun y () Int)
-
-(assert (>= n 1))
-(assert (and (<= n x)(<= x (+ n 5))))
-(assert (and (<= 1 y)(<= y m)))
-
-(get-abduct A (not (< x y)))

diff --git a/test/regress/regress1/sygus/abd-simple-conj-4.smt2 b/test/regress/regress1/sygus/abd-simple-conj-4.smt2
deleted file mode 100644 (file)
index 98bf70f..0000000
--- a/test/regress/regress1/sygus/abd-simple-conj-4.smt2
+++ /dev/null
@@ -1,13 +0,0 @@
-; COMMAND-LINE: --produce-abducts --sygus-core-connective
-; SCRUBBER: grep -v -E '(\(define-fun)'
-; EXIT: 0
-(set-logic QF_LIA)
-(set-option :produce-abducts true)
-(declare-fun x () Int)
-(declare-fun y () Int)
-(declare-fun z () Int)
-(declare-fun w () Int)
-(declare-fun u () Int)
-(declare-fun v () Int)
-(assert (>= x 0))
-(get-abduct A (>= (+ x y z w u v) 2))

diff --git a/test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2 b/test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2
deleted file mode 100644 (file)
index 79fa4f2..0000000
--- a/test/regress/regress1/sygus/abduction-no-pbe-sym-break.smt2
+++ /dev/null
@@ -1,11 +0,0 @@
-; COMMAND-LINE: --produce-abducts
-; SCRUBBER: grep -v -E '(\(define-fun)'
-; EXIT: 0
-
-(set-logic UF)
-(set-option :produce-abducts true)
-(declare-const A Bool)
-(declare-const B Bool)
-(declare-const C Bool)
-(assert (=> A C))
-(get-abduct D (=> A B))

diff --git a/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2 b/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2
deleted file mode 100644 (file)
index 1595b08..0000000
--- a/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2
+++ /dev/null
@@ -1,75 +0,0 @@
-; COMMAND-LINE: --produce-abducts --sygus-core-connective
-; SCRUBBER: grep -v -E '(\(define-fun)'
-; EXIT: 0
-
-
-(set-info :smt-lib-version |2.6|)
-(set-logic QF_SLIA)
-(set-info :source |
-Generated by: Andrew Reynolds
-Generated on: 2018-04-25
-Generator: Kudzu, converted to v2.6 by CVC4
-Application: Symbolic Execution of Javascript
-Target solver: Kaluza
-Publications: "A symbolic execution framework for JavaScript" by P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song, 2010.
-|)
-(set-info :license |"https://creativecommons.org/licenses/by/4.0/"|)
-(set-info :category |"industrial"|)
-(set-info :status unknown)
-(declare-fun T_1 () Bool)
-(declare-fun T_10 () Bool)
-(declare-fun T_11 () Bool)
-(declare-fun T_12 () Bool)
-(declare-fun T_13 () Bool)
-(declare-fun T_14 () Bool)
-(declare-fun T_2 () Bool)
-(declare-fun T_3 () Bool)
-(declare-fun T_4 () Bool)
-(declare-fun T_5 () Bool)
-(declare-fun T_6 () Bool)
-(declare-fun T_7 () Bool)
-(declare-fun T_8 () Bool)
-(declare-fun T_9 () Bool)
-(declare-fun T_a () Bool)
-(declare-fun T_b () Bool)
-(declare-fun T_c () Bool)
-(declare-fun T_d () Bool)
-(declare-fun T_e () Bool)
-(declare-fun T_f () Bool)
-(declare-fun var_0xINPUT_245549 () String)
-(assert (= T_1 (not (= "6JX7G3VKFq" var_0xINPUT_245549))))
-(assert T_1)
-(assert (= T_2 (not (= "" var_0xINPUT_245549))))
-(assert T_2)
-(assert (= T_3 (not (= var_0xINPUT_245549 ""))))
-(assert T_3)
-(assert (= T_4 (not (= "" var_0xINPUT_245549))))
-(assert T_4)
-(assert (= T_5 (= var_0xINPUT_245549 "")))
-(assert (= T_6 (not T_5)))
-(assert T_6)
-(assert (= T_7 (not (= "" var_0xINPUT_245549))))
-(assert T_7)
-(assert (= T_8 (not (= "" var_0xINPUT_245549))))
-(assert T_8)
-(assert (= T_9 (not (= var_0xINPUT_245549 ""))))
-(assert T_9)
-(assert (= T_a (= var_0xINPUT_245549 "")))
-(assert (= T_b (not T_a)))
-(assert T_b)
-(assert (= T_c (not (= "" var_0xINPUT_245549))))
-(assert T_c)
-(assert (= T_d (not (= var_0xINPUT_245549 ""))))
-(assert T_d)
-(assert (= T_e (not (= "" var_0xINPUT_245549))))
-(assert T_e)
-(assert (= T_f (= var_0xINPUT_245549 "")))
-(assert (= T_10 (not T_f)))
-(assert T_10)
-(assert (= T_11 (not (= "" var_0xINPUT_245549))))
-(assert T_11)
-(assert (= T_12 (= var_0xINPUT_245549 "Example:")))
-(assert (= T_13 (not T_12)))
-(assert T_13)
-(assert (= T_14 (not (= var_0xINPUT_245549 "CQALcCP5TB"))))
-(get-abduct A (not T_14))

diff --git a/test/regress/regress1/sygus/abduction_streq.readable.smt2 b/test/regress/regress1/sygus/abduction_streq.readable.smt2
deleted file mode 100644 (file)
index b466ab3..0000000
--- a/test/regress/regress1/sygus/abduction_streq.readable.smt2
+++ /dev/null
@@ -1,43 +0,0 @@
-; COMMAND-LINE: --produce-abducts --sygus-core-connective
-; SCRUBBER: grep -v -E '(\(define-fun)'
-; EXIT: 0
-
-(set-info :smt-lib-version |2.6|)
-(set-logic QF_SLIA)
-(set-info :source |
-Generated by: Andrew Reynolds
-Generated on: 2018-04-25
-Generator: Kudzu, converted to v2.6 by CVC4
-Application: Symbolic Execution of Javascript
-Target solver: Kaluza
-Publications: "A symbolic execution framework for JavaScript" by P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song, 2010.
-|)
-(set-info :license |"https://creativecommons.org/licenses/by/4.0/"|)
-(set-info :category |"industrial"|)
-(set-info :status unknown)
-(declare-fun I0_2 () Int)
-(declare-fun I1_2 () Int)
-(declare-fun I2_2 () Int)
-(declare-fun PCTEMP_LHS_1 () String)
-(declare-fun T1_2 () String)
-(declare-fun T2_2 () String)
-(declare-fun T3_2 () String)
-(declare-fun T_2 () Bool)
-(declare-fun T_4 () Bool)
-(declare-fun T_5 () Bool)
-(declare-fun var_0xINPUT_19 () String)
-(assert (= I0_2 (- 5 0)))
-(assert (<= 0 0))
-(assert (<= 0 5))
-(assert (<= 5 I1_2))
-(assert (= I2_2 I1_2))
-(assert (= I0_2 (str.len PCTEMP_LHS_1)))
-(assert (= var_0xINPUT_19 ( str.++ T1_2 T2_2 )))
-(assert (= T2_2 ( str.++ PCTEMP_LHS_1 T3_2 )))
-(assert (= 0 (str.len T1_2)))
-(assert (= I1_2 (str.len var_0xINPUT_19)))
-(assert (= T_2 (= PCTEMP_LHS_1 "Hello")))
-(assert T_2)
-(assert (= T_4 (= PCTEMP_LHS_1 "hello")))
-(assert (= T_5 (not T_4)))
-(get-abduct A T_5)

diff --git a/test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2 b/test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2
deleted file mode 100644 (file)
index b64e27b..0000000
--- a/test/regress/regress1/sygus/issue5848-3-trivial-no-abduct.smt2
+++ /dev/null
@@ -1,5 +0,0 @@
-; COMMAND-LINE: --produce-abducts
-; EXPECT: none
-(set-logic ALL)
-(assert (= 0.0 (sqrt 1.0)))
-(get-abduct A false)

diff --git a/test/regress/regress1/sygus/uf-abduct.smt2 b/test/regress/regress1/sygus/uf-abduct.smt2
deleted file mode 100644 (file)
index bfcfe39..0000000
--- a/test/regress/regress1/sygus/uf-abduct.smt2
+++ /dev/null
@@ -1,8 +0,0 @@
-; COMMAND-LINE: --produce-abducts
-; SCRUBBER: grep -v -E '(\(define-fun)'
-; EXIT: 0
-(set-logic HO_UFLIA)
-(declare-fun f (Int) Int)
-(declare-fun a () Int)
-(assert (and (<= 0 a) (< a 4)))
-(get-abduct ensureF (or (> (f 0) 0) (> (f 1) 0) (> (f 2) 0) (> (f 3) 0)))

diff --git a/test/regress/regress1/sygus/yoni-true-sol.smt2 b/test/regress/regress1/sygus/yoni-true-sol.smt2
deleted file mode 100644 (file)
index 464f7c7..0000000
--- a/test/regress/regress1/sygus/yoni-true-sol.smt2
+++ /dev/null
@@ -1,20 +0,0 @@
-; COMMAND-LINE: --produce-abducts
-; EXPECT: (define-fun A () Bool (>= j i))
-(set-logic QF_LIA)
-(set-option :produce-abducts true)
-(declare-fun n () Int)
-(declare-fun m () Int)
-(declare-fun i () Int)
-(declare-fun j () Int)
-(assert (and (>= n 0) (>= m 0)))
-(assert (< n i))
-(assert (< (+ i j) m))
-(get-abduct A
-  (<= n m)
-  ((GA Bool) (GJ Int) (GI Int))
-  (
-  (GA Bool ((>= GJ GI)))
-  (GJ Int ( j))
-  (GI Int ( i))
-  )
-)