Add tests that enumerate and verify rewrite rules (#2344)

9 files changed, 146 insertions, 21 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 7b01d6cb9..18ccd483c 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -1445,7 +1445,7 @@ Node SygusSymBreakNew::SearchSizeInfo::getFairnessLiteral( unsigned s, TheoryDat
       {
         std::stringstream ss;
         ss << "Maximum term size (" << options::sygusAbortSize()
-           << ") for enumerative SyGuS exceeded." << std::endl;
+           << ") for enumerative SyGuS exceeded.";
         throw LogicException(ss.str());
       }
       Assert( !d_this.isNull() );
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index ea3a70362..6400411cb 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1105,8 +1105,8 @@ REG1_TESTS = \
 	regress1/fmf/fore19-exp2-core.smt2 \
 	regress1/fmf/german169.smt2 \
 	regress1/fmf/german73.smt2 \
-	regress1/fmf/issue916-fmf-or.smt2 \
 	regress1/fmf/issue2034-preinit.smt2 \
+	regress1/fmf/issue916-fmf-or.smt2 \
 	regress1/fmf/jasmin-cdt-crash.smt2 \
 	regress1/fmf/ko-bound-set.cvc \
 	regress1/fmf/loopy_coda.smt2 \
@@ -1118,17 +1118,17 @@ REG1_TESTS = \
 	regress1/fmf/radu-quant-set.smt2 \
 	regress1/fmf/refcount24.cvc.smt2 \
 	regress1/fmf/sc-crash-052316.smt2 \
-	regress1/fmf/sort-inf-int.smt2 \
 	regress1/fmf/sort-inf-int-real.smt2 \
+	regress1/fmf/sort-inf-int.smt2 \
 	regress1/fmf/with-ind-104-core.smt2 \
 	regress1/gensys_brn001.smt2 \
 	regress1/ho/auth0068.smt2 \
 	regress1/ho/fta0210.smt2 \
 	regress1/ho/fta0409.smt2 \
-	regress1/ho/hoa0008.smt2 \
 	regress1/ho/ho-exponential-model.smt2 \
 	regress1/ho/ho-matching-enum-2.smt2 \
 	regress1/ho/ho-std-fmf.smt2 \
+	regress1/ho/hoa0008.smt2 \
 	regress1/ho/match-middle.smt2 \
 	regress1/hole6.cvc \
 	regress1/ite5.smt2 \
@@ -1136,8 +1136,8 @@ REG1_TESTS = \
 	regress1/lemmas/pursuit-safety-8.smt \
 	regress1/lemmas/simple_startup_9nodes.abstract.base.smt \
 	regress1/nl/NAVIGATION2.smt2 \
-	regress1/nl/approx-sqrt.smt2 \
 	regress1/nl/approx-sqrt-unsat.smt2 \
+	regress1/nl/approx-sqrt.smt2 \
 	regress1/nl/arctan2-expdef.smt2 \
 	regress1/nl/arrowsmith-050317.smt2 \
 	regress1/nl/bad-050217.smt2 \
@@ -1280,7 +1280,7 @@ REG1_TESTS = \
 	regress1/quantifiers/cdt-0208-to.smt2 \
 	regress1/quantifiers/const.cvc \
 	regress1/quantifiers/constfunc.cvc \
-	regress1/quantifiers/dump-inst.smt2 \
+	regress1/quantifiers/dump-inst.smt2 \  
 	regress1/quantifiers/dump-inst-i.smt2 \
 	regress1/quantifiers/dump-inst-proof.smt2 \
 	regress1/quantifiers/ext-ex-deq-trigger.smt2 \
@@ -1293,8 +1293,8 @@ REG1_TESTS = \
 	regress1/quantifiers/inst-max-level-segf.smt2 \
 	regress1/quantifiers/inst-prop-simp.smt2 \
 	regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 \
-	regress1/quantifiers/isaplanner-goal20.smt2 \
 	regress1/quantifiers/is-even.smt2 \
+	regress1/quantifiers/isaplanner-goal20.smt2 \
 	regress1/quantifiers/javafe.ast.StmtVec.009.smt2 \
 	regress1/quantifiers/lra-vts-inf.smt2 \
 	regress1/quantifiers/mix-coeff.smt2 \
@@ -1329,12 +1329,12 @@ REG1_TESTS = \
 	regress1/quantifiers/qe-partial.smt2 \
 	regress1/quantifiers/quant-wf-int-ind.smt2 \
 	regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 \
-	regress1/quantifiers/repair-const-nterm.smt2 \
 	regress1/quantifiers/recfact.cvc \
+	regress1/quantifiers/repair-const-nterm.smt2 \
 	regress1/quantifiers/rew-to-0211-dd.smt2 \
 	regress1/quantifiers/ricart-agrawala6.smt2 \
-	regress1/quantifiers/set8.smt2 \
 	regress1/quantifiers/set-choice-koikonomou.cvc \
+	regress1/quantifiers/set8.smt2 \
 	regress1/quantifiers/small-pipeline-fixpoint-3.smt2 \
 	regress1/quantifiers/smtcomp-qbv-053118.smt2 \
 	regress1/quantifiers/smtlib384a03.smt2 \
@@ -1390,6 +1390,10 @@ REG1_TESTS = \
 	regress1/rewriterules/length_gen_040_lemma_trigger.smt2 \
 	regress1/rewriterules/reachability_back_to_the_future.smt2 \
 	regress1/rewriterules/read5.smt2 \
+	regress1/rr-verify/bool-crci.sy \
+	regress1/rr-verify/bv-term-32.sy \
+	regress1/rr-verify/bv-term.sy \
+	regress1/rr-verify/string-term.sy \
 	regress1/sep/chain-int.smt2 \
 	regress1/sep/crash1220.smt2 \
 	regress1/sep/dispose-list-4-init.smt2 \
@@ -1501,6 +1505,10 @@ REG1_TESTS = \
 	regress1/strings/repl-empty-sem.smt2 \
 	regress1/strings/repl-soundness-sem.smt2 \
 	regress1/strings/rew-020618.smt2 \
+	regress1/strings/str-code-sat.smt2 \
+	regress1/strings/str-code-unsat-2.smt2 \
+	regress1/strings/str-code-unsat-3.smt2 \
+	regress1/strings/str-code-unsat.smt2 \
 	regress1/strings/str001.smt2 \
 	regress1/strings/str002.smt2 \
 	regress1/strings/str006.smt2 \
@@ -1511,10 +1519,6 @@ REG1_TESTS = \
 	regress1/strings/strings-lt-len5.smt2 \
 	regress1/strings/strings-lt-simple.smt2 \
 	regress1/strings/strip-endpt-sound.smt2 \
-	regress1/strings/str-code-sat.smt2 \
-	regress1/strings/str-code-unsat.smt2 \
-	regress1/strings/str-code-unsat-2.smt2 \
-	regress1/strings/str-code-unsat-3.smt2 \
 	regress1/strings/substr001.smt2 \
 	regress1/strings/type002.smt2 \
 	regress1/strings/type003.smt2 \
@@ -1526,16 +1530,16 @@ REG1_TESTS = \
 	regress1/sygus/array_sum_2_5.sy \
 	regress1/sygus/bvudiv-by-2.sy \
 	regress1/sygus/cegar1.sy \
-	regress1/sygus/cegisunif-depth1.sy \
 	regress1/sygus/cegis-unif-inv-eq-fair.sy \
+	regress1/sygus/cegisunif-depth1.sy \
 	regress1/sygus/cggmp.sy \
 	regress1/sygus/clock-inc-tuple.sy \
-	regress1/sygus/commutative.sy \
 	regress1/sygus/commutative-stream.sy \
-	regress1/sygus/constant.sy \
+	regress1/sygus/commutative.sy \
 	regress1/sygus/constant-bool-si-all.sy \
 	regress1/sygus/constant-dec-tree-bug.sy \
 	regress1/sygus/constant-ite-bv.sy \
+	regress1/sygus/constant.sy \
 	regress1/sygus/crci-ssb-unk.sy \
 	regress1/sygus/crcy-si-rcons.sy \
 	regress1/sygus/crcy-si.sy \
@@ -1589,8 +1593,8 @@ REG1_TESTS = \
 	regress1/sygus/tl-type-0.sy \
 	regress1/sygus/tl-type-4x.sy \
 	regress1/sygus/tl-type.sy \
-	regress1/sygus/trivial-stream.sy \
 	regress1/sygus/triv-type-mismatch-si.sy \
+	regress1/sygus/trivial-stream.sy \
 	regress1/sygus/twolets1.sy \
 	regress1/sygus/twolets2-orig.sy \
 	regress1/sygus/unbdd_inv_gen_ex7.sy \
diff --git a/test/regress/regress1/rr-verify/bool-crci.sy b/test/regress/regress1/rr-verify/bool-crci.sy
new file mode 100644
index 000000000..955245f87
--- /dev/null
+++ b/test/regress/regress1/rr-verify/bool-crci.sy
@@ -0,0 +1,41 @@
+; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break
+; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.")
+; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
+; EXIT: 1
+
+(set-logic BV)
+
+(synth-fun f ( (x Bool) (y Bool) (z Bool) (w Bool) ) Bool 
+ ((Start Bool (
+   (and depth1 depth1)
+   (not depth1)
+   (or depth1 depth1)
+   (xor depth1 depth1)
+ ))
+ (depth1 Bool (
+   (and depth2 depth2)
+   (not depth2)
+   (or depth2 depth2)
+   (xor depth2 depth2)
+   x
+ ))
+ (depth2 Bool (
+   (and depth3 depth3)
+   (not depth3)
+   (or depth3 depth3)
+   (xor depth3 depth3)
+   w
+ ))
+ (depth3 Bool (
+   (and depth4 depth4)
+   (not depth4)
+   (or depth4 depth4)
+   (xor depth4 depth4)
+   y
+ ))
+ (depth4 Bool (
+   z
+ )))
+)
+
+(check-synth)
diff --git a/test/regress/regress1/rr-verify/bv-term-32.sy b/test/regress/regress1/rr-verify/bv-term-32.sy
new file mode 100644
index 000000000..6c07bd8aa
--- /dev/null
+++ b/test/regress/regress1/rr-verify/bv-term-32.sy
@@ -0,0 +1,25 @@
+; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break
+; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
+; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
+; EXIT: 1
+
+(set-logic BV)
+
+(synth-fun f ((s (BitVec 32)) (t (BitVec 32))) (BitVec 32)
+  (
+   (Start (BitVec 32) (
+     s
+     t
+     #x00000000
+     (bvneg  Start)
+     (bvnot  Start)
+     (bvadd  Start Start)
+     (bvmul  Start Start)
+     (bvand  Start Start)
+     (bvlshr Start Start)
+     (bvor   Start Start)
+     (bvshl  Start Start)
+   ))
+))
+
+(check-synth)
diff --git a/test/regress/regress1/rr-verify/bv-term.sy b/test/regress/regress1/rr-verify/bv-term.sy
new file mode 100644
index 000000000..025479f24
--- /dev/null
+++ b/test/regress/regress1/rr-verify/bv-term.sy
@@ -0,0 +1,25 @@
+; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --no-sygus-sym-break
+; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
+; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
+; EXIT: 1
+
+(set-logic BV)
+
+(synth-fun f ((s (BitVec 4)) (t (BitVec 4))) (BitVec 4)
+  (
+   (Start (BitVec 4) (
+     s
+     t
+     #x0
+     (bvneg  Start)
+     (bvnot  Start)
+     (bvadd  Start Start)
+     (bvmul  Start Start)
+     (bvand  Start Start)
+     (bvlshr Start Start)
+     (bvor   Start Start)
+     (bvshl  Start Start)
+   ))
+))
+
+(check-synth)
diff --git a/test/regress/regress1/rr-verify/string-term.sy b/test/regress/regress1/rr-verify/string-term.sy
new file mode 100644
index 000000000..8f6593148
--- /dev/null
+++ b/test/regress/regress1/rr-verify/string-term.sy
@@ -0,0 +1,25 @@
+; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break
+; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
+; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
+; EXIT: 1
+
+(set-logic SLIA)
+
+(synth-fun f ((x String) (y String) (z Int)) String (
+(Start String (
+  x y "A" "B" ""
+  (str.++ Start Start)
+  (str.replace Start Start Start)
+  (str.at Start StartInt)
+  (int.to.str StartInt)
+  (str.substr Start StartInt StartInt)))
+(StartInt Int (
+  0 1 z
+  (+ StartInt StartInt)
+  (- StartInt StartInt)
+  (str.len Start)
+  (str.to.int Start)
+  (str.indexof Start Start StartInt)))
+))
+
+(check-synth)
diff --git a/test/regress/regress1/sygus/commutative-stream.sy b/test/regress/regress1/sygus/commutative-stream.sy
index b07051d37..ae8d0b8c0 100644
--- a/test/regress/regress1/sygus/commutative-stream.sy
+++ b/test/regress/regress1/sygus/commutative-stream.sy
@@ -1,7 +1,6 @@
 ; EXPECT: (define-fun comm ((x Int) (y Int)) Int (+ x y))
 ; EXPECT: (define-fun comm ((x Int) (y Int)) Int (- x x))
-; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.
-; EXPECT: ")
+; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
 ; EXIT: 1
 
 ; COMMAND-LINE: --sygus-stream --sygus-abort-size=2
diff --git a/test/regress/regress1/sygus/trivial-stream.sy b/test/regress/regress1/sygus/trivial-stream.sy
index 42965ff32..b8b08d03b 100644
--- a/test/regress/regress1/sygus/trivial-stream.sy
+++ b/test/regress/regress1/sygus/trivial-stream.sy
@@ -1,7 +1,6 @@
 ; EXPECT: (define-fun triv ((x Int) (y Int)) Int x)
 ; EXPECT: (define-fun triv ((x Int) (y Int)) Int y)
-; EXPECT: (error "Maximum term size (0) for enumerative SyGuS exceeded.
-; EXPECT: ")
+; EXPECT: (error "Maximum term size (0) for enumerative SyGuS exceeded.")
 ; EXIT: 1
 
 ; COMMAND-LINE: --sygus-stream --sygus-abort-size=0
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 6f6edf058..fa23bd9bf 100755
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -269,6 +269,7 @@ def run_regression(unsat_cores, proofs, dump, wrapper, cvc4_binary,
         extra_command_line_args = []
         if benchmark_ext == '.sy' and \
             '--no-check-synth-sol' not in all_args and \
+            '--sygus-rr' not in all_args and \
             '--check-synth-sol' not in all_args:
             extra_command_line_args = ['--check-synth-sol']
         if re.search(r'^(sat|invalid|unknown)$', expected_output) and \
@@ -326,6 +327,12 @@ def run_regression(unsat_cores, proofs, dump, wrapper, cvc4_binary,
             print(
                 'not ok - Expected exit status "{}" but got "{}" - Flags: {}'.
                 format(expected_exit_status, exit_status, command_line_args))
+            print()
+            print('Output:')
+            print(output)
+            print()
+            print('Error output:')
+            print(error)
         else:
             print('ok - Flags: {}'.format(command_line_args))