diff options
Diffstat (limited to 'test/regress/regress0/rewriterules')
39 files changed, 2051 insertions, 0 deletions
diff --git a/test/regress/regress0/rewriterules/Makefile b/test/regress/regress0/rewriterules/Makefile new file mode 100644 index 000000000..82da93d37 --- /dev/null +++ b/test/regress/regress0/rewriterules/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../.. +srcdir = test/regress/regress0/rewriterules + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am new file mode 100644 index 000000000..94b558675 --- /dev/null +++ b/test/regress/regress0/rewriterules/Makefile.am @@ -0,0 +1,36 @@ +BINARY = cvc4 +if PROOF_REGRESSIONS +TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY) +else +TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY) +endif + +MAKEFLAGS = -k + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# 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 + +EXTRA_DIST = $(TESTS) + +#if CVC4_BUILD_PROFILE_COMPETITION +#else +#TESTS += \ +# error.cvc +#endif +# +# and make sure to distribute it +#EXTRA_DIST += \ +# error.cvc + +# synonyms for "check" in this directory +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress0/rewriterules/datatypes.smt2 b/test/regress/regress0/rewriterules/datatypes.smt2 new file mode 100644 index 000000000..a914a0c1f --- /dev/null +++ b/test/regress/regress0/rewriterules/datatypes.smt2 @@ -0,0 +1,101 @@ +;; try to solve datatypes with rewriterules +(set-logic AUFLIA) +(set-info :status unsat) + +;; lists 2 nil +(declare-sort elt 0) ;; we suppose that elt is infinite +(declare-sort list 0) + +(declare-fun nil1 () list) +(declare-fun nil2 () list) +(declare-fun cons (elt list) list) + +;;;;;;;;;;;;;;;;;;;; +;; injective + +(declare-fun inj1 (list) elt) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (inj1 (cons ?e ?l)) ?e))) :pattern ((cons ?e ?l)) ) :rewrite-rule) )) + +(declare-fun inj2 (list) list) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (inj2 (cons ?e ?l)) ?l))) :pattern ((cons ?e ?l)) ) :rewrite-rule) )) + +;;;;;;;;;;;;;;;;;;;; +;; projection + +(declare-fun proj1 (list) elt) +(assert (forall ((?e elt) (?l list)) + (! (= (proj1 (cons ?e ?l)) ?e) :rewrite-rule) )) + +(declare-fun proj2 (list) list) +(assert (forall ((?e elt) (?l list)) + (! (= (proj2 (cons ?e ?l)) ?l) :rewrite-rule) )) + +;;;;;;;;;;;;;;;;;;; +;; test +(declare-fun iscons (list) Bool) +(assert (= (iscons nil1) false)) +(assert (= (iscons nil2) false)) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (iscons (cons ?e ?l)) true))) :pattern ((cons ?e ?l)) ) :rewrite-rule) )) + +(assert (forall ((?l list)) + (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj1 ?l)) ) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj2 ?l)) ) :rewrite-rule) )) + + +(declare-fun isnil1 (list) Bool) +(assert (= (isnil1 nil1) true)) +(assert (= (isnil1 nil2) false)) +(assert (forall ((?e elt) (?l list)) + (! (= (isnil1 (cons ?e ?l)) false) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (=> true (=> (isnil1 ?l) (= ?l nil1))) :rewrite-rule) )) + +(declare-fun isnil2 (list) Bool) +(assert (= (isnil2 nil1) false)) +(assert (= (isnil2 nil2) true)) +(assert (forall ((?e elt) (?l list)) + (! (= (isnil2 (cons ?e ?l)) false) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (=> true (=> (isnil2 ?l) (= ?l nil2))) :rewrite-rule) )) + +;; distinct +(assert (forall ((?l list)) + (! (=> (isnil1 ?l) (and (not (isnil2 ?l)) (not (iscons ?l))) ) :rewrite-rule) )) + +(assert (forall ((?l list)) + (! (=> (isnil2 ?l) (and (not (isnil1 ?l)) (not (iscons ?l))) ) :rewrite-rule) )) + +(assert (forall ((?l list)) + (! (=> (iscons ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l))) ) :rewrite-rule) )) + + +;;;;;;;;;;;;;;;;;;; +;; case-split +(assert (forall ((?l list)) + (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj1 ?l)) ) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj2 ?l)) ) :rewrite-rule) )) + +;;;;;;;;;;;;;;;;;;; +;; finite case-split +(assert (forall ((?l list)) + (! (=> (not (iscons ?l)) (or (isnil1 ?l) (isnil2 ?l))) :rewrite-rule) )) + + + +;;;;; goal + +(declare-fun e () elt) +(declare-fun l1 () list) +(declare-fun l2 () list) + + +(assert (not (=> (iscons l1) (=> (= (proj2 l1) (proj2 l2)) (= l1 (cons (proj1 l1) (proj2 l2))))))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/datatypes2.smt2 b/test/regress/regress0/rewriterules/datatypes2.smt2 new file mode 100644 index 000000000..993cd2002 --- /dev/null +++ b/test/regress/regress0/rewriterules/datatypes2.smt2 @@ -0,0 +1,150 @@ +;; try to solve datatypes with rewriterules +(set-logic AUFLIA) +(set-info :status unsat) + +;; lists 2 nil +(declare-sort elt 0) ;; we suppose that elt is infinite +(declare-sort list 0) + +(declare-fun nil1 () list) +(declare-fun nil2 () list) +(declare-fun cons1 (elt list) list) +(declare-fun cons2 (elt list) list) + +;;;;;;;;;;;;;;;;;;;; +;; injective + +(declare-fun inj1 (list) elt) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (inj1 (cons1 ?e ?l)) ?e))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) + +(declare-fun inj2 (list) list) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (inj2 (cons1 ?e ?l)) ?l))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) + +(declare-fun inj1 (list) elt) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (inj1 (cons2 ?e ?l)) ?e))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) + +(declare-fun inj2 (list) list) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (inj2 (cons2 ?e ?l)) ?l))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) + + +;;;;;;;;;;;;;;;;;;;; +;; projection + +(declare-fun proj11 (list) elt) +(assert (forall ((?e elt) (?l list)) + (! (= (proj11 (cons1 ?e ?l)) ?e) :rewrite-rule) )) + +(declare-fun proj12 (list) list) +(assert (forall ((?e elt) (?l list)) + (! (= (proj12 (cons1 ?e ?l)) ?l) :rewrite-rule) )) + + +(declare-fun proj21 (list) elt) +(assert (forall ((?e elt) (?l list)) + (! (= (proj21 (cons2 ?e ?l)) ?e) :rewrite-rule) )) + +(declare-fun proj22 (list) list) +(assert (forall ((?e elt) (?l list)) + (! (= (proj22 (cons2 ?e ?l)) ?l) :rewrite-rule) )) + + +;;;;;;;;;;;;;;;;;;; +;; test +(declare-fun iscons1 (list) Bool) +(assert (= (iscons1 nil1) false)) +(assert (= (iscons1 nil2) false)) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (iscons1 (cons1 ?e ?l)) true))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (iscons1 (cons2 ?e ?l)) false))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) + +(assert (forall ((?l list)) + (! (! (=> true (=> (iscons1 ?l) (= ?l (cons1 (proj11 ?l) (proj12 ?l))))) :pattern ((proj11 ?l)) ) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (! (=> true (=> (iscons1 ?l) (= ?l (cons1 (proj11 ?l) (proj12 ?l))))) :pattern ((proj12 ?l)) ) :rewrite-rule) )) + + +(declare-fun iscons2 (list) Bool) +(assert (= (iscons2 nil1) false)) +(assert (= (iscons2 nil2) false)) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (iscons2 (cons1 ?e ?l)) false))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (iscons2 (cons2 ?e ?l)) true))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) + +(assert (forall ((?l list)) + (! (! (=> true (=> (iscons2 ?l) (= ?l (cons2 (proj21 ?l) (proj22 ?l))))) :pattern ((proj21 ?l)) ) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (! (=> true (=> (iscons2 ?l) (= ?l (cons2 (proj21 ?l) (proj22 ?l))))) :pattern ((proj22 ?l)) ) :rewrite-rule) )) + + +(declare-fun isnil1 (list) Bool) +(assert (= (isnil1 nil1) true)) +(assert (= (isnil1 nil2) false)) +(assert (forall ((?e elt) (?l list)) + (! (= (isnil1 (cons1 ?e ?l)) false) :rewrite-rule) )) +(assert (forall ((?e elt) (?l list)) + (! (= (isnil1 (cons2 ?e ?l)) false) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (=> true (=> (isnil1 ?l) (= ?l nil1))) :rewrite-rule) )) + +(declare-fun isnil2 (list) Bool) +(assert (= (isnil2 nil1) false)) +(assert (= (isnil2 nil2) true)) +(assert (forall ((?e elt) (?l list)) + (! (= (isnil2 (cons1 ?e ?l)) false) :rewrite-rule) )) +(assert (forall ((?e elt) (?l list)) + (! (= (isnil2 (cons2 ?e ?l)) false) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (=> true (=> (isnil2 ?l) (= ?l nil2))) :rewrite-rule) )) + +;; distinct +(assert (forall ((?l list)) + (! (=> (isnil1 ?l) (and (not (isnil2 ?l)) (not (iscons1 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) )) + +(assert (forall ((?l list)) + (! (=> (isnil2 ?l) (and (not (isnil1 ?l)) (not (iscons1 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) )) + +(assert (forall ((?l list)) + (! (=> (iscons1 ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) )) + +(assert (forall ((?l list)) + (! (=> (iscons2 ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l)) (not (iscons1 ?l))) ) :rewrite-rule) )) + + +;;;;;;;;;;;;;;;;;;; +;; case-split +(assert (forall ((?l list)) + (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj11 ?l)) ) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj12 ?l)) ) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj21 ?l)) ) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj22 ?l)) ) :rewrite-rule) )) + +;;;;;;;;;;;;;;;;;;; +;; finite case-split +(assert (forall ((?l list)) + (! (=> (and (not (iscons1 ?l)) (not (iscons2 ?l))) (or (isnil1 ?l) (isnil2 ?l))) :rewrite-rule) )) + + + +;;;;; goal + +(declare-fun e () elt) +(declare-fun l1 () list) +(declare-fun l2 () list) + + + (assert (not (=> (iscons2 l1) (=> (= (proj22 l1) (proj22 l2)) (= l1 (cons2 (proj21 l1) (proj22 l2))))))) + +;;(assert (= (cons1 l1 l2) (cons2 l1 l2))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/datatypes3.smt2 b/test/regress/regress0/rewriterules/datatypes3.smt2 new file mode 100644 index 000000000..dc3c8e20c --- /dev/null +++ b/test/regress/regress0/rewriterules/datatypes3.smt2 @@ -0,0 +1,137 @@ +;; try to solve datatypes with rewriterules +(set-logic AUFLIA) +(set-info :status unsat) + +;; lists 2 nil +(declare-sort elt 0) ;; we suppose that elt is infinite +(declare-sort list 0) + +(declare-fun nil1 () list) +(declare-fun nil2 () list) +(declare-fun cons1 (elt list) list) +(declare-fun cons2 (elt list) list) + +;;;;;;;;;;;;;;;;;;;; +;; injective + +(declare-fun inj1 (list) elt) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (inj1 (cons1 ?e ?l)) ?e))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) + +(declare-fun inj2 (list) list) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (inj2 (cons1 ?e ?l)) ?l))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) + +(declare-fun inj1 (list) elt) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (inj1 (cons2 ?e ?l)) ?e))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) + +(declare-fun inj2 (list) list) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (inj2 (cons2 ?e ?l)) ?l))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) + + +;;;;;;;;;;;;;;;;;;;; +;; projection + +(declare-fun proj11 (list) elt) +(assert (forall ((?e elt) (?l list)) + (! (= (proj11 (cons1 ?e ?l)) ?e) :rewrite-rule) )) + +(declare-fun proj12 (list) list) +(assert (forall ((?e elt) (?l list)) + (! (= (proj12 (cons1 ?e ?l)) ?l) :rewrite-rule) )) + +(assert (= (proj11 nil1) nil1)) +(assert (= (proj12 nil1) nil1)) +(assert (= (proj11 nil2) nil2)) +(assert (= (proj12 nil2) nil2)) + +(declare-fun proj21 (list) elt) +(assert (forall ((?e elt) (?l list)) + (! (= (proj21 (cons2 ?e ?l)) ?e) :rewrite-rule) )) + +(declare-fun proj22 (list) list) +(assert (forall ((?e elt) (?l list)) + (! (= (proj22 (cons2 ?e ?l)) ?l) :rewrite-rule) )) + +(assert (= (proj21 nil1) nil1)) +(assert (= (proj22 nil1) nil1)) +(assert (= (proj21 nil2) nil2)) +(assert (= (proj22 nil2) nil2)) + + +;;;;;;;;;;;;;;;;;;; +;; test +(declare-fun iscons1 (list) Bool) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (iscons1 (cons1 ?e ?l)) true))) :pattern ((cons1 ?e ?l)) ) :rewrite-rule) )) + +(assert (forall ((?l list)) + (! (! (=> true (=> (iscons1 ?l) (= ?l (cons1 (proj11 ?l) (proj12 ?l))))) :pattern ((proj11 ?l)) ) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (! (=> true (=> (iscons1 ?l) (= ?l (cons1 (proj11 ?l) (proj12 ?l))))) :pattern ((proj12 ?l)) ) :rewrite-rule) )) + + +(declare-fun iscons2 (list) Bool) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (iscons2 (cons2 ?e ?l)) true))) :pattern ((cons2 ?e ?l)) ) :rewrite-rule) )) + +(assert (forall ((?l list)) + (! (! (=> true (=> (iscons2 ?l) (= ?l (cons2 (proj21 ?l) (proj22 ?l))))) :pattern ((proj21 ?l)) ) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (! (=> true (=> (iscons2 ?l) (= ?l (cons2 (proj21 ?l) (proj22 ?l))))) :pattern ((proj22 ?l)) ) :rewrite-rule) )) + + +(declare-fun isnil1 (list) Bool) +(assert (= (isnil1 nil1) true)) + +(declare-fun isnil2 (list) Bool) +(assert (= (isnil2 nil2) true)) + +;; distinct +(assert (forall ((?l list)) + (! (=> (isnil1 ?l) (and (not (isnil2 ?l)) (not (iscons1 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) )) + +(assert (forall ((?l list)) + (! (=> (isnil2 ?l) (and (not (isnil1 ?l)) (not (iscons1 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) )) + +(assert (forall ((?l list)) + (! (=> (iscons1 ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l)) (not (iscons2 ?l))) ) :rewrite-rule) )) + +(assert (forall ((?l list)) + (! (=> (iscons2 ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l)) (not (iscons1 ?l))) ) :rewrite-rule) )) + + +;;;;;;;;;;;;;;;;;;; +;; case-split +(assert (forall ((?l list)) + (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj11 ?l)) ) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj12 ?l)) ) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj21 ?l)) ) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons1 ?l) (iscons2 ?l))) :pattern ((proj22 ?l)) ) :rewrite-rule) )) + +;;;;;;;;;;;;;;;;;;; +;; finite case-split +(assert (forall ((?l list)) + (! (=> (and (not (iscons1 ?l)) (not (iscons2 ?l))) (or (isnil1 ?l) (isnil2 ?l))) :rewrite-rule) )) + + + +;;;;; goal + +(declare-fun e () elt) +(declare-fun l1 () list) +(declare-fun l2 () list) + + +;; (assert (not (=> (iscons2 l1) (=> (= (proj22 l1) (proj22 l2)) (= l1 (cons2 (proj21 l1) (proj22 l2))))))) + +(assert (= (cons1 l1 l2) (cons2 l1 l2))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/datatypes_clark.smt2 b/test/regress/regress0/rewriterules/datatypes_clark.smt2 new file mode 100644 index 000000000..eacb5ff6a --- /dev/null +++ b/test/regress/regress0/rewriterules/datatypes_clark.smt2 @@ -0,0 +1,264 @@ +(set-logic LRA) + +;; DATATYPE +;; nat = succ(pred : nat) | zero, +;; list = cons(car : tree, cdr : list) | null, +;; tree = node(children : list) | leaf(data : nat) +;; END; + +;;;;;;;;;;; +;; nat ;; +;;;;;;;;;;; +(declare-sort nat 0) +(declare-fun zero () nat) +(declare-fun succ (nat) nat) + +;;;;;;;;;;;;;;;; +;; injective + +(declare-fun inj1 (nat) nat) +(assert (forall ((?x1 nat)) + (! (! (=> true (=> true (= (inj1 (succ ?x1)) ?x1))) :pattern ((succ ?x1)) ) :rewrite-rule) )) + + +;;;;;;;;;;;;;;;;;;;; +;; projection + +(declare-fun pred (nat) nat) +(assert (forall ((?x1 nat)) + (! (= (pred (succ ?x1)) ?x1) :rewrite-rule) )) + +(assert (= (pred zero) zero)) + +;;;;;;;;;;;;;;;;;;; +;; test +(declare-fun is_succ (nat) Bool) +(assert (= (is_succ zero) false)) +(assert (forall ((?x1 nat)) + (! (! (=> true (=> true (= (is_succ (succ ?x1)) true))) :pattern ((succ ?x1)) ) :rewrite-rule) )) + +(assert (forall ((?x1 nat)) + (! (! (=> true (=> (is_succ ?x1) (= ?x1 (succ (pred ?x1))))) :pattern ((pred ?x1)) ) :rewrite-rule) )) + +(declare-fun is_zero (nat) Bool) +(assert (= (is_zero zero) true)) +(assert (forall ((?x1 nat)) + (! (=> true (=> (is_zero ?x1) (= ?x1 zero))) :rewrite-rule) )) + +;;; directrr +(assert (forall ((?x1 nat)) + (! (= (is_succ (succ ?x1)) true) :rewrite-rule))) +(assert (forall ((?x1 nat)) + (! (= (is_zero (succ ?x1)) false) :rewrite-rule))) + + +;;;;;;;;;;;;;;;;;;;; +;; distinct +(assert (forall ((?x1 nat)) + (! (=> (is_zero ?x1) (not (is_succ ?x1)) ) :rewrite-rule) )) +(assert (forall ((?x1 nat)) + (! (=> (is_succ ?x1) (not (is_zero ?x1)) ) :rewrite-rule) )) +(assert (forall ((?x1 nat)) + (! (=> (not (is_zero ?x1)) (is_succ ?x1) ) :rewrite-rule) )) +(assert (forall ((?x1 nat)) + (! (=> (not (is_succ ?x1)) (is_zero ?x1) ) :rewrite-rule) )) + +;;;;;;;;;;;;;;;;;;; +;; case-split +(assert (forall ((?x1 nat)) + (! (! (=> true (or (is_zero ?x1) (is_succ ?x1))) :pattern ((pred ?x1)) ) :rewrite-rule) )) + +;;;;;;;;;;;;;;;;;;; +;; non-cyclic +(declare-fun size_nat (nat) Real) +(assert (forall ((?x1 nat)) + (! (! (=> true (> (size_nat (succ ?x1)) (size_nat ?x1))) :pattern ((succ ?x1)) ) :rewrite-rule) )) + + + +;;;;;;;;;;;;;;;;;;;;; +;; list and tree + +(declare-sort list 0) +(declare-sort tree 0) + +;;;;;;;;;;; +;; list ;; +;;;;;;;;;;; + +(declare-fun null () list) +(declare-fun cons (tree list) list) + +(declare-fun node (list) tree) +(declare-fun leaf (nat) tree) + +;;;;;;;;;;;;;;;; +;; injective + +(declare-fun inj2 (list) tree) +(assert (forall ((?x1 tree) (?x2 list)) + (! (! (=> true (=> true (= (inj2 (cons ?x1 ?x2)) ?x1))) :pattern ((cons ?x1 ?x2)) ) :rewrite-rule) )) + +(declare-fun inj3 (list) list) +(assert (forall ((?x1 tree) (?x2 list)) + (! (! (=> true (=> true (= (inj3 (cons ?x1 ?x2)) ?x2))) :pattern ((cons ?x1 ?x2)) ) :rewrite-rule) )) + + +;;;;;;;;;;;;;;;;;;;; +;; projection + +(declare-fun car (list) tree) +(assert (forall ((?x1 tree) (?x2 list)) + (! (= (car (cons ?x1 ?x2)) ?x1) :rewrite-rule) )) + +(assert (= (car null) (node null))) + +(declare-fun cdr (list) list) +(assert (forall ((?x1 tree) (?x2 list)) + (! (= (cdr (cons ?x1 ?x2)) ?x2) :rewrite-rule) )) + +(assert (= (cdr null) null)) + +;;;;;;;;;;;;;;;;;;; +;; test +(declare-fun is_cons (list) Bool) +(assert (= (is_cons null) false)) +(assert (forall ((?x1 tree) (?x2 list)) + (! (! (=> true (=> true (= (is_cons (cons ?x1 ?x2)) true))) :pattern ((cons ?x1 ?x2)) ) :rewrite-rule) )) + +(assert (forall ((?x1 list)) + (! (! (=> true (=> (is_cons ?x1) (= ?x1 (cons (car ?x1) (cdr ?x1))))) :pattern ((car ?x1)) ) :rewrite-rule) )) +(assert (forall ((?x1 list)) + (! (! (=> true (=> (is_cons ?x1) (= ?x1 (cons (car ?x1) (cdr ?x1))))) :pattern ((cdr ?x1)) ) :rewrite-rule) )) + +(declare-fun is_null (list) Bool) +(assert (= (is_null null) true)) + +(assert (forall ((?x1 list)) + (! (! (=> true (=> (is_null ?x1) (= (car ?x1) (node null)))) :pattern ((car ?x1)) ) :rewrite-rule) )) +(assert (forall ((?x1 list)) + (! (! (=> true (=> (is_null ?x1) (= (cdr ?x1) null))) :pattern ((cdr ?x1)) ) :rewrite-rule) )) + +(assert (forall ((?x1 list)) + (! (=> true (=> (is_null ?x1) (= ?x1 null))) :rewrite-rule) )) + +;;; directrr +(assert (forall ((?x1 tree) (?x2 list)) + (! (= (is_cons (cons ?x1 ?x2)) true) :rewrite-rule) )) +(assert (forall ((?x1 tree) (?x2 list)) + (! (= (is_null (cons ?x1 ?x2)) false) :rewrite-rule) )) + + + +;;;;;;;;;;;;;;;;;;;; +;; distinct +(assert (forall ((?x1 list)) + (! (=> (is_null ?x1) (not (is_cons ?x1)) ) :rewrite-rule) )) +(assert (forall ((?x1 list)) + (! (=> (is_cons ?x1) (not (is_null ?x1)) ) :rewrite-rule) )) +(assert (forall ((?x1 list)) + (! (=> (not (is_null ?x1)) (is_cons ?x1) ) :rewrite-rule) )) +(assert (forall ((?x1 list)) + (! (=> (not (is_cons ?x1)) (is_null ?x1) ) :rewrite-rule) )) + +;;;;;;;;;;;;;;;;;;; +;; case-split +(assert (forall ((?x1 list)) + (! (! (=> true (or (is_null ?x1) (is_cons ?x1))) :pattern ((car ?x1)) ) :rewrite-rule) )) +(assert (forall ((?x1 list)) + (! (! (=> true (or (is_null ?x1) (is_cons ?x1))) :pattern ((cdr ?x1)) ) :rewrite-rule) )) + +;;;;;;;;;;;;;;; +;; tree + +;;;;;;;;;;;;;;;; +;; injective + +(declare-fun inj4 (tree) list) +(assert (forall ((?x1 list)) + (! (! (=> true (=> true (= (inj4 (node ?x1)) ?x1))) :pattern ((node ?x1)) ) :rewrite-rule) )) + +(declare-fun inj5 (tree) nat) +(assert (forall ((?x1 nat)) + (! (! (=> true (=> true (= (inj5 (leaf ?x1)) ?x1))) :pattern ((leaf ?x1)) ) :rewrite-rule) )) + + +;;;;;;;;;;;;;;;;;;;; +;; projection + +(declare-fun children (tree) list) +(assert (forall ((?x1 list)) + (! (= (children (node ?x1)) ?x1) :rewrite-rule) )) +(assert (forall ((?x1 nat)) + (! (= (children (leaf ?x1)) null) :rewrite-rule) )) + + +(declare-fun data (tree) nat) +(assert (forall ((?x1 nat)) + (! (= (data (leaf ?x1)) ?x1) :rewrite-rule) )) +(assert (forall ((?x1 list)) + (! (= (data (node ?x1)) zero) :rewrite-rule) )) + +;;;;;;;;;;;;;;;;;;; +;; test +(declare-fun is_node (tree) Bool) +(assert (forall ((?x1 list)) + (! (! (=> true (=> true (= (is_node (node ?x1)) true))) :pattern ((node ?x1)) ) :rewrite-rule) )) + +(assert (forall ((?x1 tree)) + (! (! (=> true (=> (is_node ?x1) (= ?x1 (node (children ?x1))))) :pattern ((children ?x1)) ) :rewrite-rule) )) + +(assert (forall ((?x1 tree)) + (! (! (=> true (=> (is_node ?x1) (= (data ?x1) zero))) :pattern ((data ?x1)) ) :rewrite-rule) )) + + +(declare-fun is_leaf (tree) Bool) +(assert (forall ((?x1 nat)) + (! (! (=> true (=> true (= (is_leaf (leaf ?x1)) true))) :pattern ((leaf ?x1)) ) :rewrite-rule) )) + +(assert (forall ((?x1 tree)) + (! (! (=> true (=> (is_leaf ?x1) (= ?x1 (leaf (data ?x1))))) :pattern ((data ?x1)) ) :rewrite-rule) )) +(assert (forall ((?x1 tree)) + (! (! (=> true (=> (is_leaf ?x1) (= (children ?x1) null))) :pattern ((children ?x1)) ) :rewrite-rule) )) + +;;; directrr +(assert (forall ((?x1 list)) + (! (= (is_node (node ?x1)) true) :rewrite-rule) )) +(assert (forall ((?x1 list)) + (! (= (is_leaf (node ?x1)) false) :rewrite-rule) )) +(assert (forall ((?x1 nat)) + (! (= (is_leaf (leaf ?x1)) true) :rewrite-rule) )) +(assert (forall ((?x1 nat)) + (! (= (is_node (leaf ?x1)) false) :rewrite-rule) )) + + +;;;;;;;;;;;;;;;;;;;; +;; distinct +(assert (forall ((?x1 tree)) + (! (=> (is_node ?x1) (not (is_leaf ?x1)) ) :rewrite-rule) )) +(assert (forall ((?x1 tree)) + (! (=> (is_leaf ?x1) (not (is_node ?x1)) ) :rewrite-rule) )) +(assert (forall ((?x1 tree)) + (! (=> (not (is_node ?x1)) (is_leaf ?x1) ) :rewrite-rule) )) +(assert (forall ((?x1 tree)) + (! (=> (not (is_leaf ?x1)) (is_node ?x1) ) :rewrite-rule) )) + +;;;;;;;;;;;;;;;;;;; +;; case-split +(assert (forall ((?x1 tree)) + (! (! (=> true (or (is_node ?x1) (is_leaf ?x1))) :pattern ((children ?x1)) ) :rewrite-rule) )) + +(assert (forall ((?x1 tree)) + (! (! (=> true (or (is_node ?x1) (is_leaf ?x1))) :pattern ((data ?x1)) ) :rewrite-rule) )) + + +;;;;;;;;;;;;;;;;;; +;; non-cyclic +(declare-fun size_list (list) Real) +(declare-fun size_tree (tree) Real) +(assert (forall ((?x1 tree) (?x2 list)) + (! (! (=> true (and (> (size_list (cons ?x1 ?x2)) (size_tree ?x1)) (> (size_list (cons ?x1 ?x2)) (size_list ?x2)))) :pattern ((cons ?x1 ?x2)) ) :rewrite-rule) )) +(assert (forall ((?x1 list)) + (! (! (=> true (> (size_tree (node ?x1)) (size_list ?x1))) :pattern ((node ?x1)) ) :rewrite-rule) )) +(assert (forall ((?x1 nat)) + (! (! (=> true (> (size_tree (leaf ?x1)) (size_nat ?x1))) :pattern ((leaf ?x1)) ) :rewrite-rule) )) diff --git a/test/regress/regress0/rewriterules/datatypes_sat.smt2 b/test/regress/regress0/rewriterules/datatypes_sat.smt2 new file mode 100644 index 000000000..92576f976 --- /dev/null +++ b/test/regress/regress0/rewriterules/datatypes_sat.smt2 @@ -0,0 +1,101 @@ +;; try to solve datatypes with rewriterules +(set-logic AUFLIA) +(set-info :status sat) + +;; lists 2 nil +(declare-sort elt 0) ;; we suppose that elt is infinite +(declare-sort list 0) + +(declare-fun nil1 () list) +(declare-fun nil2 () list) +(declare-fun cons (elt list) list) + +;;;;;;;;;;;;;;;;;;;; +;; injective + +(declare-fun inj1 (list) elt) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (inj1 (cons ?e ?l)) ?e))) :pattern ((cons ?e ?l)) ) :rewrite-rule) )) + +(declare-fun inj2 (list) list) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (inj2 (cons ?e ?l)) ?l))) :pattern ((cons ?e ?l)) ) :rewrite-rule) )) + +;;;;;;;;;;;;;;;;;;;; +;; projection + +(declare-fun proj1 (list) elt) +(assert (forall ((?e elt) (?l list)) + (! (= (proj1 (cons ?e ?l)) ?e) :rewrite-rule) )) + +(declare-fun proj2 (list) list) +(assert (forall ((?e elt) (?l list)) + (! (= (proj2 (cons ?e ?l)) ?l) :rewrite-rule) )) + +;;;;;;;;;;;;;;;;;;; +;; test +(declare-fun iscons (list) Bool) +(assert (= (iscons nil1) false)) +(assert (= (iscons nil2) false)) +(assert (forall ((?e elt) (?l list)) + (! (! (=> true (=> true (= (iscons (cons ?e ?l)) true))) :pattern ((cons ?e ?l)) ) :rewrite-rule) )) + +(assert (forall ((?l list)) + (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj1 ?l)) ) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj2 ?l)) ) :rewrite-rule) )) + + +(declare-fun isnil1 (list) Bool) +(assert (= (isnil1 nil1) true)) +(assert (= (isnil1 nil2) false)) +(assert (forall ((?e elt) (?l list)) + (! (= (isnil1 (cons ?e ?l)) false) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (=> true (=> (isnil1 ?l) (= ?l nil1))) :rewrite-rule) )) + +(declare-fun isnil2 (list) Bool) +(assert (= (isnil2 nil1) false)) +(assert (= (isnil2 nil2) true)) +(assert (forall ((?e elt) (?l list)) + (! (= (isnil2 (cons ?e ?l)) false) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (=> true (=> (isnil2 ?l) (= ?l nil2))) :rewrite-rule) )) + +;; distinct +(assert (forall ((?l list)) + (! (=> (isnil1 ?l) (and (not (isnil2 ?l)) (not (iscons ?l))) ) :rewrite-rule) )) + +(assert (forall ((?l list)) + (! (=> (isnil2 ?l) (and (not (isnil1 ?l)) (not (iscons ?l))) ) :rewrite-rule) )) + +(assert (forall ((?l list)) + (! (=> (iscons ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l))) ) :rewrite-rule) )) + + +;;;;;;;;;;;;;;;;;;; +;; case-split +(assert (forall ((?l list)) + (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj1 ?l)) ) :rewrite-rule) )) +(assert (forall ((?l list)) + (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj2 ?l)) ) :rewrite-rule) )) + +;;;;;;;;;;;;;;;;;;; +;; finite case-split +(assert (forall ((?l list)) + (! (=> (not (iscons ?l)) (or (isnil1 ?l) (isnil2 ?l))) :rewrite-rule) )) + + + +;;;;; goal + +(declare-fun e () elt) +(declare-fun l1 () list) +(declare-fun l2 () list) + + +(assert (not (=> (iscons l1) (=> (= (proj2 l1) (proj2 l2)) (= l1 (cons (proj1 l2) (proj2 l2))))))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length.smt2 b/test/regress/regress0/rewriterules/length.smt2 new file mode 100644 index 000000000..215698ade --- /dev/null +++ b/test/regress/regress0/rewriterules/length.smt2 @@ -0,0 +1,26 @@ +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (forall ((?l list)) (! (=> (= ?l nil) (= (length ?l) 0)) :rewrite-rule))) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ (length ?l) 1)) :rewrite-rule))) + +;;(assert (forall ((?l list)) (=> (= ?l nil) (= (length ?l) 0)))) + +;;(assert (forall ((?e Int) (?l list) (?l2 list)) (=> (= ?l2 (cons ?e ?l)) (= (length ?l2) (+ (length ?l) 1))))) + + +(assert (not (= (length (cons 1 (cons 2 (cons 3 nil)))) 3))) + +(check-sat) +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen.smt2 b/test/regress/regress0/rewriterules/length_gen.smt2 new file mode 100644 index 000000000..dda478357 --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen.smt2 @@ -0,0 +1,34 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) + +(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 42 nil)) 42))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_010.smt2 b/test/regress/regress0/rewriterules/length_gen_010.smt2 new file mode 100644 index 000000000..7c7663b17 --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_010.smt2 @@ -0,0 +1,34 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) + +(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 10 nil)) 10))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_010_lemma.smt2 b/test/regress/regress0/rewriterules/length_gen_010_lemma.smt2 new file mode 100644 index 000000000..02bc877fc --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_010_lemma.smt2 @@ -0,0 +1,34 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (= (length (cons ?e ?l)) (+ 1 (length ?l))))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)))) + +(assert (forall ((?n Int) (?l list)) (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 10 nil)) 10))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_020.smt2 b/test/regress/regress0/rewriterules/length_gen_020.smt2 new file mode 100644 index 000000000..8e0021175 --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_020.smt2 @@ -0,0 +1,34 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) + +(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 20 nil)) 20))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_020_sat.smt2 b/test/regress/regress0/rewriterules/length_gen_020_sat.smt2 new file mode 100644 index 000000000..cc75eb85a --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_020_sat.smt2 @@ -0,0 +1,34 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status sat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) + +(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 20 nil)) 200))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_040.smt2 b/test/regress/regress0/rewriterules/length_gen_040.smt2 new file mode 100644 index 000000000..687422223 --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_040.smt2 @@ -0,0 +1,34 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) + +(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 40 nil)) 40))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_040_lemma.smt2 b/test/regress/regress0/rewriterules/length_gen_040_lemma.smt2 new file mode 100644 index 000000000..293ea147b --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_040_lemma.smt2 @@ -0,0 +1,34 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (= (length (cons ?e ?l)) (+ 1 (length ?l))))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)))) + +(assert (forall ((?n Int) (?l list)) (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 40 nil)) 40))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_040_lemma_trigger.smt2 b/test/regress/regress0/rewriterules/length_gen_040_lemma_trigger.smt2 new file mode 100644 index 000000000..69f9f97be --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_040_lemma_trigger.smt2 @@ -0,0 +1,35 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (!(= (length (cons ?e ?l)) (+ 1 (length ?l))) :pattern ((length (cons ?e ?l))) ))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :pattern ((gen_cons ?n ?l)) ))) + +(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))) + :pattern ((gen_cons ?n ?l)) ))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 40 nil)) 40))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_080.smt2 b/test/regress/regress0/rewriterules/length_gen_080.smt2 new file mode 100644 index 000000000..061042be3 --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_080.smt2 @@ -0,0 +1,34 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) + +(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 80 nil)) 80))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_1280.smt2 b/test/regress/regress0/rewriterules/length_gen_1280.smt2 new file mode 100644 index 000000000..b613844ce --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_1280.smt2 @@ -0,0 +1,34 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) + +(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 1280 nil)) 1280))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_1280_lemma_trigger.smt2 b/test/regress/regress0/rewriterules/length_gen_1280_lemma_trigger.smt2 new file mode 100644 index 000000000..7d1cf3203 --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_1280_lemma_trigger.smt2 @@ -0,0 +1,35 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (!(= (length (cons ?e ?l)) (+ 1 (length ?l))) :pattern ((length (cons ?e ?l))) ))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :pattern ((gen_cons ?n ?l)) ))) + +(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))) + :pattern ((gen_cons ?n ?l)) ))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 1280 nil)) 1280))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_160.smt2 b/test/regress/regress0/rewriterules/length_gen_160.smt2 new file mode 100644 index 000000000..339c70bb5 --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_160.smt2 @@ -0,0 +1,34 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) + +(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 160 nil)) 160))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_160_lemma.smt2 b/test/regress/regress0/rewriterules/length_gen_160_lemma.smt2 new file mode 100644 index 000000000..28b58183e --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_160_lemma.smt2 @@ -0,0 +1,34 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (= (length (cons ?e ?l)) (+ 1 (length ?l))))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)))) + +(assert (forall ((?n Int) (?l list)) (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 160 nil)) 160))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_160_lemma_trigger.smt2 b/test/regress/regress0/rewriterules/length_gen_160_lemma_trigger.smt2 new file mode 100644 index 000000000..65d0c9570 --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_160_lemma_trigger.smt2 @@ -0,0 +1,35 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (!(= (length (cons ?e ?l)) (+ 1 (length ?l))) :pattern ((length (cons ?e ?l))) ))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :pattern ((gen_cons ?n ?l)) ))) + +(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))) + :pattern ((gen_cons ?n ?l)) ))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 160 nil)) 160))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_160_sat.smt2 b/test/regress/regress0/rewriterules/length_gen_160_sat.smt2 new file mode 100644 index 000000000..e2ed52faf --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_160_sat.smt2 @@ -0,0 +1,34 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status sat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) + +(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 160 nil)) 1600))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_2560.smt2 b/test/regress/regress0/rewriterules/length_gen_2560.smt2 new file mode 100644 index 000000000..2aff61656 --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_2560.smt2 @@ -0,0 +1,34 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) + +(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 2560 nil)) 2560))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_2560_sat.smt2 b/test/regress/regress0/rewriterules/length_gen_2560_sat.smt2 new file mode 100644 index 000000000..3e88e781f --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_2560_sat.smt2 @@ -0,0 +1,34 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) + +(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 2560 nil)) 25600))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_640.smt2 b/test/regress/regress0/rewriterules/length_gen_640.smt2 new file mode 100644 index 000000000..f1dc6bbf2 --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_640.smt2 @@ -0,0 +1,34 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) + +(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 640 nil)) 640))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_640_lemma.smt2 b/test/regress/regress0/rewriterules/length_gen_640_lemma.smt2 new file mode 100644 index 000000000..29d0f1aca --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_640_lemma.smt2 @@ -0,0 +1,34 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (= (length (cons ?e ?l)) (+ 1 (length ?l))))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)))) + +(assert (forall ((?n Int) (?l list)) (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 640 nil)) 640))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_640_sat.smt2 b/test/regress/regress0/rewriterules/length_gen_640_sat.smt2 new file mode 100644 index 000000000..958c2c730 --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_640_sat.smt2 @@ -0,0 +1,34 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) + +(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 640 nil)) 6400))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_inv_1280.smt2 b/test/regress/regress0/rewriterules/length_gen_inv_1280.smt2 new file mode 100644 index 000000000..30e3bc864 --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_inv_1280.smt2 @@ -0,0 +1,34 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) + +(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) + (cons 1 (gen_cons (- ?n 1) ?l)))) :rewrite-rule))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 1280 nil)) 1280))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_inv_160.smt2 b/test/regress/regress0/rewriterules/length_gen_inv_160.smt2 new file mode 100644 index 000000000..9c2a5c307 --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_inv_160.smt2 @@ -0,0 +1,34 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) + +(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) + (cons 1 (gen_cons (- ?n 1) ?l)))) :rewrite-rule))) + +(declare-fun n () Int) + +(assert (not (= (length (gen_cons 160 nil)) 160))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_n.smt2 b/test/regress/regress0/rewriterules/length_gen_n.smt2 new file mode 100644 index 000000000..5d1255eb0 --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_n.smt2 @@ -0,0 +1,45 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule))) + +(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule))) + + +;;(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> (= (length (gen_cons ?n nil)) ?n) (= (length (gen_cons (+ ?n 1) nil)) (+ ?n 1))) )))) + +;;(assert (not (forall ((?n Int) (?l list)) (=> (>= ?n 0) (=> (= (length ?l) ?n) (= (length (cons 1 ?l)) (+ ?n 1))) )))) + +;; (assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> (= (length (gen_cons ?n nil)) ?n) (= (length (cons 1 (gen_cons ?n nil))) (+ ?n 1))) )))) + +;;(assert (not (forall ((?n Int)) (=> (>= ?n 0) (= (gen_cons (+ ?n 1) nil) (cons 1 (gen_cons ?n nil))) )))) + +(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> + (forall ((?l list)) (= (gen_cons ?n (cons 1 ?l)) (cons 1 (gen_cons ?n ?l)))) + (forall ((?l list)) (= (gen_cons (+ ?n 1) (cons 1 ?l)) (cons 1 (gen_cons (+ ?n 1) ?l)))) + ))))) + + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2 b/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2 new file mode 100644 index 000000000..b1462cf98 --- /dev/null +++ b/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2 @@ -0,0 +1,43 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (= (length (cons ?e ?l)) (+ 1 (length ?l))))) + +(declare-fun gen_cons (Int list) list) + +(assert (forall ((?n Int) (?l list)) (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)))) + +(assert (forall ((?n Int) (?l list)) (=> (> ?n 0) (= (gen_cons ?n ?l) + (gen_cons (- ?n 1) (cons 1 ?l)))))) + + +;;(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> (= (length (gen_cons ?n nil)) ?n) (= (length (gen_cons (+ ?n 1) nil)) (+ ?n 1))) )))) + +;;(assert (not (forall ((?n Int) (?l list)) (=> (>= ?n 0) (=> (= (length ?l) ?n) (= (length (cons 1 ?l)) (+ ?n 1))) )))) + +;;(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> (= (length (gen_cons ?n nil)) ?n) (= (length (cons 1 (gen_cons ?n nil))) (+ ?n 1))) )))) + +(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> + (forall ((?l list)) (= (gen_cons ?n (cons 1 ?l)) (cons 1 (gen_cons ?n ?l)))) + (forall ((?l list)) (= (gen_cons (+ ?n 1) (cons 1 ?l)) (cons 1 (gen_cons (+ ?n 1) ?l)))) + ))))) + + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_trick.smt2 b/test/regress/regress0/rewriterules/length_trick.smt2 new file mode 100644 index 000000000..84afc5815 --- /dev/null +++ b/test/regress/regress0/rewriterules/length_trick.smt2 @@ -0,0 +1,32 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + + + + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ (length ?l) 1)) :rewrite-rule))) + +;;(assert (forall ((?l list)) (=> (= ?l nil) (= (length ?l) 0)))) + +;;(assert (forall ((?e Int) (?l list) (?l2 list)) (=> (= ?l2 (cons ?e ?l)) (= (length ?l2) (+ (length ?l) 1))))) + + +(assert (not (= (length (cons 1 (cons 2 (cons 3 nil)))) 3))) + +(check-sat) +(exit) diff --git a/test/regress/regress0/rewriterules/length_trick2.smt2 b/test/regress/regress0/rewriterules/length_trick2.smt2 new file mode 100644 index 000000000..af9e7f07d --- /dev/null +++ b/test/regress/regress0/rewriterules/length_trick2.smt2 @@ -0,0 +1,32 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + + + + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ (length ?l) 1)) :rewrite-rule))) + +;;(assert (forall ((?l list)) (=> (= ?l nil) (= (length ?l) 0)))) + +;;(assert (forall ((?e Int) (?l list) (?l2 list)) (=> (= ?l2 (cons ?e ?l)) (= (length ?l2) (+ (length ?l) 1))))) + +(assert (forall ((?a Int) (?b Int) (?l list)) + (not (> (length (cons ?a (cons ?b ?l))) (length ?l))))) +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_trick3.smt2 b/test/regress/regress0/rewriterules/length_trick3.smt2 new file mode 100644 index 000000000..f6899541b --- /dev/null +++ b/test/regress/regress0/rewriterules/length_trick3.smt2 @@ -0,0 +1,36 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) +;; don't use arith +(declare-sort mynat 0) +(declare-fun zero () mynat) +(declare-fun succ (mynat) mynat) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) mynat) + +(assert (= (length nil) zero)) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (succ (length ?l))) :rewrite-rule))) + +(declare-fun ten_one_cons (list) list) + +(assert (forall ((?l list)) (! (= (ten_one_cons ?l) + (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 ?l) ))))))))) + ) :rewrite-rule))) + +(assert (not (= (length (ten_one_cons nil)) + (succ(succ(succ(succ(succ(succ(succ(succ(succ(succ zero))))))))))))) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/length_trick3_int.smt2 b/test/regress/regress0/rewriterules/length_trick3_int.smt2 new file mode 100644 index 000000000..d58bf55fe --- /dev/null +++ b/test/regress/regress0/rewriterules/length_trick3_int.smt2 @@ -0,0 +1,44 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) + + +;;define length +(declare-fun length (list) Int) + +(assert (= (length nil) 0)) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule))) + +(declare-fun ten_one_cons (list) list) + +(assert (forall ((?l list)) (! (= (ten_one_cons ?l) + (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 ?l) ))))))))) + ) :rewrite-rule))) + +(assert (not (= (length (ten_one_cons nil)) + 10))) + +(check-sat) + +(declare-fun ten_one_ten (list) list) + +(assert (forall ((?l list)) (! (= (ten_one_ten ?l) + (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons (ten_one_cons ?l) ))))))))) + ) :rewrite-rule))) + +(declare-fun two_one_ten (list) list) + +(assert (forall ((?l list)) (! (= (two_one_ten ?l) + (ten_one_cons (ten_one_cons ?l)) + ) :rewrite-rule))) + +(exit) diff --git a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 new file mode 100644 index 000000000..65dc23a10 --- /dev/null +++ b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 @@ -0,0 +1,100 @@ +;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort elt 0) +(declare-sort set 0) + +(declare-fun in (elt set) Bool) + +;;;;;;;;;;;;;;;;;;;; +;; inter + +(declare-fun inter (set set) set) +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (=> (in ?s (inter ?t1 ?t2)) (and (in ?s ?t1) (in ?s ?t2))) :rewrite-rule))) + + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (! (=> (not (in ?s ?t1)) (not (in ?s (inter ?t1 ?t2)))) :pattern ((inter ?t1 ?t2)) ) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (! (=> (not (in ?s ?t2)) (not (in ?s (inter ?t1 ?t2)))) :pattern ((inter ?t1 ?t2)) ) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (=> (and (not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2))) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (=> (and (not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1))) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (! (=> (and (in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2))) :pattern ((inter ?t1 ?t2)) ) :rewrite-rule) )) + +;;;;;;;;;;;;;;;;; +;; union + +(declare-fun union (set set) set) +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (=> (not (in ?s (union ?t1 ?t2))) (and (not (in ?s ?t1)) (not (in ?s ?t2)))) :rewrite-rule))) + + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (! (=> (in ?s ?t1) (in ?s (union ?t1 ?t2))) :pattern ((union ?t1 ?t2)) ) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (! (=> (in ?s ?t2) (in ?s (union ?t1 ?t2))) :pattern ((union ?t1 ?t2)) ) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (=> (and (in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2)) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (=> (and (in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1)) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (! (=> (and (not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2)))) :pattern ((union ?t1 ?t2)) ) :rewrite-rule) )) + +;;;;;;;;;;;;;;;; +;;sing + +(declare-fun sing (elt) set) +(assert (forall ((?s elt)) + (! (! (=> true (in ?s (sing ?s))) :pattern ((sing ?s)) ) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 elt)) + (! (=> true (=> (in ?s (sing ?t1)) (= ?s ?t1))) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 elt)) + (! (=> (not (in ?s (sing ?t1))) (not (= ?s ?t1))) :rewrite-rule) )) + + + +;;;;;;;;;;;;;;;;;;; +;; fullfiling +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (=> (in ?s (union ?t1 ?t2)) (or (in ?s ?t1) (not (in ?s ?t1)))) :rewrite-rule))) + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (! (=> (in ?s ?t1) (or (in ?s ?t2) (not (in ?s ?t2)))) :pattern ((inter ?t1 ?t2))) :rewrite-rule))) + +(assert (forall ((?t1 set) (?t2 set)) (! (=> (not (= ?t1 ?t2)) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2))))) :rewrite-rule))) + +(declare-fun e () elt) +(declare-fun t1 () set) +(declare-fun t2 () set) +(declare-fun t3 () set) + +;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e (union t1 t1))))) +;;(assert (not (=> (in e (union t1 t1)) (in e t1)))) + +;; hyp +;;(assert (=> (in e (union t1 t1)) (in e t1))) + +;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e t1)))) + +;;(assert (or (and (not (in e (union t1 (union t2 t3)))) (in e (union (union t1 t2) t3))) (and (in e (union t1 (union t2 t3))) (not (in e (union (union t1 t2) t3))))) ) +(assert (not (= (union t1 (union t2 t3)) (union (union t1 t2) t3))) ) + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 new file mode 100644 index 000000000..07e9f9643 --- /dev/null +++ b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 @@ -0,0 +1,100 @@ +;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba +(set-logic AUFLIA) +(set-info :status sat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort elt 0) +(declare-sort set 0) + +(declare-fun in (elt set) Bool) + +;;;;;;;;;;;;;;;;;;;; +;; inter + +(declare-fun inter (set set) set) +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (=> (in ?s (inter ?t1 ?t2)) (and (in ?s ?t1) (in ?s ?t2))) :rewrite-rule))) + + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (! (=> (not (in ?s ?t1)) (not (in ?s (inter ?t1 ?t2)))) :pattern ((inter ?t1 ?t2)) ) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (! (=> (not (in ?s ?t2)) (not (in ?s (inter ?t1 ?t2)))) :pattern ((inter ?t1 ?t2)) ) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (=> (and (not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2))) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (=> (and (not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1))) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (! (=> (and (in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2))) :pattern ((inter ?t1 ?t2)) ) :rewrite-rule) )) + +;;;;;;;;;;;;;;;;; +;; union + +(declare-fun union (set set) set) +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (=> (not (in ?s (union ?t1 ?t2))) (and (not (in ?s ?t1)) (not (in ?s ?t2)))) :rewrite-rule))) + + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (! (=> (in ?s ?t1) (in ?s (union ?t1 ?t2))) :pattern ((union ?t1 ?t2)) ) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (! (=> (in ?s ?t2) (in ?s (union ?t1 ?t2))) :pattern ((union ?t1 ?t2)) ) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (=> (and (in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2)) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (=> (and (in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1)) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (! (=> (and (not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2)))) :pattern ((union ?t1 ?t2)) ) :rewrite-rule) )) + +;;;;;;;;;;;;;;;; +;;sing + +(declare-fun sing (elt) set) +(assert (forall ((?s elt)) + (! (! (=> true (in ?s (sing ?s))) :pattern ((sing ?s)) ) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 elt)) + (! (=> true (=> (in ?s (sing ?t1)) (= ?s ?t1))) :rewrite-rule) )) + +(assert (forall ((?s elt) (?t1 elt)) + (! (=> (not (in ?s (sing ?t1))) (not (= ?s ?t1))) :rewrite-rule) )) + + + +;;;;;;;;;;;;;;;;;;; +;; fullfiling +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (=> (in ?s (union ?t1 ?t2)) (or (in ?s ?t1) (not (in ?s ?t1)))) :rewrite-rule))) + +(assert (forall ((?s elt) (?t1 set) (?t2 set)) + (! (! (=> (in ?s ?t1) (or (in ?s ?t2) (not (in ?s ?t2)))) :pattern ((inter ?t1 ?t2))) :rewrite-rule))) + +;; (assert (forall ((?t1 set) (?t2 set)) (! (=> (not (= ?t1 ?t2)) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2))))) ))) + +(declare-fun e () elt) +(declare-fun t1 () set) +(declare-fun t2 () set) +(declare-fun t3 () set) + +;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e (union t1 t1))))) +;;(assert (not (=> (in e (union t1 t1)) (in e t1)))) + +;; hyp +;;(assert (=> (in e (union t1 t1)) (in e t1))) + +;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e t1)))) + +(assert (or (and (not (in e (union t1 (union t2 t3)))) (in e (union (union t1 t2) t3))) (and (in e (union t1 (union t2 t3))) (not (in e (union (union t2 t2) t3))))) ) + + +(check-sat) + +(exit) diff --git a/test/regress/regress0/rewriterules/test_guards.smt2 b/test/regress/regress0/rewriterules/test_guards.smt2 new file mode 100644 index 000000000..98c845fb5 --- /dev/null +++ b/test/regress/regress0/rewriterules/test_guards.smt2 @@ -0,0 +1,45 @@ +;; Same than length.smt2 but the nil case is not a rewrite rule +;; So here the rewrite rules have no guards length + +(set-logic AUFLIA) +(set-info :status unsat) + +;; don't use a datatypes for currently focusing in uf +(declare-sort list 0) +;; don't use arith +(declare-sort mynat 0) +(declare-fun zero () mynat) +(declare-fun succ (mynat) mynat) + +(declare-fun cons (Int list) list) +(declare-fun nil () list) +(declare-fun p (list) Bool) + + +;;define length +(declare-fun length (list) mynat) + +(assert (= (length nil) zero)) + +(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (succ (length ?l))) :rewrite-rule))) + +(declare-fun ten_one_cons (list) list) + +(assert (forall ((?l list)) (! (=> (p ?l) (= (ten_one_cons ?l) + (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 (cons 1 ?l) ))))))))) + )) :rewrite-rule))) + +(declare-fun a () Bool) +(declare-fun b () Bool) +(declare-fun c () Bool) + +(assert (=> a (p nil)) ) +(assert (=> b (p nil)) ) +(assert (or a b)) + +(assert (not (= (length (ten_one_cons nil)) + (succ(succ(succ(succ(succ(succ(succ(succ(succ(succ zero))))))))))))) + +(check-sat) + +(exit) |