diff options
Diffstat (limited to 'test/regress/regress1/rewriterules')
-rw-r--r-- | test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2 | 54 | ||||
-rw-r--r-- | test/regress/regress1/rewriterules/read5.smt2 | 35 |
2 files changed, 89 insertions, 0 deletions
diff --git a/test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2 b/test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2 new file mode 100644 index 000000000..13f7234e9 --- /dev/null +++ b/test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2 @@ -0,0 +1,54 @@ +;; Back to the Future ... Shuvendu K.Lhiri, Shaz Qadeer +(set-logic AUFLIA) +(set-info :status unsat) + +(declare-sort elt 0) + +(declare-fun f (elt) elt) +(declare-fun Rf (elt elt elt) Bool) + +;;eq +(assert-propagation ((?x elt)) ((?x)) () () (or (= ?x ?x) (not (= ?x ?x))) ) +;; reflexive +(assert-propagation ((?x elt)) ((?x)) () () (Rf ?x ?x ?x) ) +;; step +(assert-propagation ((?x elt)) (((f ?x))) () () (Rf ?x (f ?x) (f ?x)) ) +;; reach +(assert-propagation ((?x1 elt)(?x2 elt)) (((f ?x1))) () ((Rf ?x1 ?x2 ?x2)) (or (= ?x1 ?x2) (Rf ?x1 (f ?x1) ?x2)) ) +;; cycle +(assert-propagation ((?x1 elt)(?x2 elt)) (((f ?x1))) ((= (f ?x1) ?x1)) ((Rf ?x1 ?x2 ?x2)) (= ?x1 ?x2) ) +;; sandwich +(assert-propagation ((?x1 elt)(?x2 elt)) () () ((Rf ?x1 ?x2 ?x1)) (= ?x1 ?x2) ) +;; order1 +(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x1 ?x2 ?x2)(Rf ?x1 ?x3 ?x3)) + (or (Rf ?x1 ?x2 ?x3) (Rf ?x1 ?x3 ?x2)) ) +;; order2 +(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x1 ?x2 ?x3)) + (and (Rf ?x1 ?x2 ?x2) (Rf ?x2 ?x3 ?x3)) ) +;; transitive1 +(assert-propagation ((?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x1 ?x2 ?x2)(Rf ?x2 ?x3 ?x3)) + (Rf ?x1 ?x3 ?x3) ) +;; transitive2 +(assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x0 ?x1 ?x2)(Rf ?x1 ?x3 ?x2)) + (and (Rf ?x0 ?x1 ?x3) (Rf ?x0 ?x3 ?x2)) ) +;;transitive3 +(assert-propagation ((?x0 elt)(?x1 elt)(?x2 elt)(?x3 elt)) () () ((Rf ?x0 ?x1 ?x2)(Rf ?x0 ?x3 ?x1)) + (and (Rf ?x0 ?x3 ?x2) (Rf ?x3 ?x1 ?x2)) ) + +(declare-fun e1 () elt) +(declare-fun e2 () elt) +(declare-fun e3 () elt) +(declare-fun e4 () elt) + + +;; (assert (=> (Rf e1 e2 e3) (Rf e1 (f e1) (f e1)) )) + +;; (assert (=> (Rf e1 e2 e3) (Rf e1 e3 e3) )) + +;; (assert (=> (Rf e1 e2 e3) (or (= e1 e3) (Rf e1 (f e1) e3)) )) + +(assert (not (=> (and (not (= e1 e2)) (Rf e1 e2 e3)) (Rf e1 (f e1) e3) ))) + + +(check-sat) +(exit)
\ No newline at end of file diff --git a/test/regress/regress1/rewriterules/read5.smt2 b/test/regress/regress1/rewriterules/read5.smt2 new file mode 100644 index 000000000..e66df7c7e --- /dev/null +++ b/test/regress/regress1/rewriterules/read5.smt2 @@ -0,0 +1,35 @@ +(set-logic AUF) +(set-info :source | +Translated from old SVC processor verification benchmarks. Contact Clark +Barrett at barrett@cs.nyu.edu for more information. + +This benchmark was automatically translated into SMT-LIB format from +CVC format using CVC Lite +|) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-sort Index 0) +(declare-sort Element 0)(declare-sort Arr 0)(declare-fun aselect (Arr Index) Element)(declare-fun astore (Arr Index Element) Arr)(declare-fun k (Arr Arr) Index) +(declare-fun a () Index) +(declare-fun aaa () Index) +(declare-fun aa () Index) +(declare-fun S () Arr) +(declare-fun vvv () Element) +(declare-fun v () Element) +(declare-fun vv () Element) +(declare-fun bbb () Index) +(declare-fun www () Element) +(declare-fun bb () Index) +(declare-fun ww () Element) +(declare-fun b () Index) +(declare-fun w () Element) +(declare-fun SS () Arr) +(assert (let ((?v_3 (ite (= a aa) false true)) (?v_4 (ite (= aa aaa) false true)) (?v_1 (astore (astore (astore S a v) aa vv) aaa vvv)) (?v_0 (astore S aaa vvv)) (?v_2 (astore S aa vv))) (not (ite (ite (ite (ite (= a aaa) false true) (ite ?v_3 ?v_4 false) false) (ite (= (astore (astore ?v_0 a v) aa vv) ?v_1) (ite (= (astore (astore ?v_0 aa vv) a v) ?v_1) (ite (= (astore (astore ?v_2 a v) aaa vvv) ?v_1) (= (astore (astore ?v_2 aaa vvv) a v) ?v_1) false) false) false) true) (ite (ite (= ?v_1 (astore (astore (astore S bbb www) bb ww) b w)) (ite (ite ?v_3 (ite ?v_4 (ite (ite (= aa b) false true) (ite (ite (= aa bb) false true) (ite (= aa bbb) false true) false) false) false) false) (= (aselect S aa) vv) true) true) (ite (= S (astore SS a v)) (= S (astore SS a (aselect S a))) true) false) false)))) +; rewrite rule definition of arrays theory +(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (=> (not (= ?i ?j)) (= (aselect (astore ?x ?i ?e) ?j) (aselect ?x ?j))) :rewrite-rule))) +(assert (forall ((?x Arr) (?i Index) (?e Element)) (! (=> true (= (aselect (astore ?x ?i ?e) ?i) ?e)) :rewrite-rule))) +(assert (forall ((?x Arr) (?y Arr)) (! (=> (not (= ?x ?y)) (not (= (aselect ?x (k ?x ?y)) (aselect ?y (k ?x ?y))))) :rewrite-rule))) +(assert (forall ((?x Arr) (?y Arr)) (! (! (=> true (or (= ?x ?y) (not (= ?x ?y)))) :pattern (?x)) :rewrite-rule))) +(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (! (=> true (or (= ?i ?j) (not (= ?i ?j)))) :pattern ((aselect (astore ?x ?i ?e) ?j))) :rewrite-rule)))(check-sat) +(exit) |