diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-20 09:45:46 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-03-11 11:29:45 -0500 |
| commit | 38d149261763e5f2f65abb21c2b647f2befa7807 (patch) | |
| tree | 51c3019eff61c7f3702f3dc888fb88d3a714f68a /test/regress | |
| parent | 3ed865aa12a94e935038d70b130701045b84a8b8 (diff) | |
Initial refactor of rewrite rules, make theory_rewriterules empty theory. Push kinds to quantifiers/kinds, rewrite rewrite rules in rewriter.
Fix rewrite rule attribute, refactor QCF, instantiation engine does not register rewrite rules, minor clean up.
QCF is now functional backend to rewrite rules. Support boolean variables in QCF. Change check-model to ignore rewrite rules. Incorporate some fixes from master.
Move rewrite of rewrite rules from rewriter to preprocessor, attribute becomes pattern.
Minor fixes to QCF/rewrite engine, removes RE on last call approach. Add option for one inst per round in RE.
Merging rewrite rules into master, check-model current fails on 3 FMF regressions.
Fix check-model issue, a line of code was omitted during merge.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/push-pop/bug326.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/rewriterules/Makefile.am | 11 | ||||
| -rw-r--r-- | test/regress/regress0/rewriterules/simulate_rewriting.smt2 | 2 |
3 files changed, 8 insertions, 7 deletions
diff --git a/test/regress/regress0/push-pop/bug326.smt2 b/test/regress/regress0/push-pop/bug326.smt2 index 8fe88e9f5..51d60e920 100644 --- a/test/regress/regress0/push-pop/bug326.smt2 +++ b/test/regress/regress0/push-pop/bug326.smt2 @@ -31,7 +31,7 @@ (check-sat) (pop) -; EXPECT: sat +; EXPECT: unknown (push);;sat (assert (and (not (R e1 e3)) (R e4 e1))) (check-sat) diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am index b7eac2535..5aba7dcec 100644 --- a/test/regress/regress0/rewriterules/Makefile.am +++ b/test/regress/regress0/rewriterules/Makefile.am @@ -1,4 +1,4 @@ -CVC4_REGRESSION_ARGS ?= --efficient-e-matching +CVC4_REGRESSION_ARGS ?= --rewrite-rules export CVC4_REGRESSION_ARGS # don't override a BINARY imported from a personal.mk @@ -23,10 +23,11 @@ MAKEFLAGS = -k # put it below in "TESTS +=" TESTS = \ length_trick.smt2 length_trick2.smt2 length_gen_020.smt2 \ - datatypes.smt2 datatypes_sat.smt2 set_A_new_fast_tableau-base.smt2 \ - set_A_new_fast_tableau-base_sat.smt2 relation.smt2 simulate_rewriting.smt2 \ - reachability_back_to_the_future.smt2 native_arrays.smt2 -# reachability_bbttf_eT_arrays.smt2 + datatypes.smt2 datatypes_sat.smt2 reachability_back_to_the_future.smt2 \ + relation.smt2 simulate_rewriting.smt2 \ + native_arrays.smt2 + +# reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/rewriterules/simulate_rewriting.smt2 b/test/regress/regress0/rewriterules/simulate_rewriting.smt2 index d1d88a549..838c0cd16 100644 --- a/test/regress/regress0/rewriterules/simulate_rewriting.smt2 +++ b/test/regress/regress0/rewriterules/simulate_rewriting.smt2 @@ -1,6 +1,6 @@ ;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba (set-logic AUFLIA) -(set-info :status sat) +(set-info :status unsat) (declare-sort elt1 0) (declare-sort elt2 0) |