From 3b728a49c482ea447e3b82c7aa1251ad0866c12a Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 24 Aug 2018 07:36:21 -0700 Subject: [PATCH] Add tests that enumerate and verify rewrite rules (#2344) --- src/theory/datatypes/datatypes_sygus.cpp | 2 +- test/regress/Makefile.tests | 36 ++++++++-------- test/regress/regress1/rr-verify/bool-crci.sy | 41 +++++++++++++++++++ test/regress/regress1/rr-verify/bv-term-32.sy | 25 +++++++++++ test/regress/regress1/rr-verify/bv-term.sy | 25 +++++++++++ .../regress/regress1/rr-verify/string-term.sy | 25 +++++++++++ .../regress1/sygus/commutative-stream.sy | 3 +- test/regress/regress1/sygus/trivial-stream.sy | 3 +- test/regress/run_regression.py | 7 ++++ 9 files changed, 146 insertions(+), 21 deletions(-) create mode 100644 test/regress/regress1/rr-verify/bool-crci.sy create mode 100644 test/regress/regress1/rr-verify/bv-term-32.sy create mode 100644 test/regress/regress1/rr-verify/bv-term.sy create mode 100644 test/regress/regress1/rr-verify/string-term.sy 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)) -- 2.30.2