diff options
Diffstat (limited to 'test/regress/regress0/sygus/max.smt2')
| -rw-r--r-- | test/regress/regress0/sygus/max.smt2 | 52 |
1 files changed, 0 insertions, 52 deletions
diff --git a/test/regress/regress0/sygus/max.smt2 b/test/regress/regress0/sygus/max.smt2 deleted file mode 100644 index ab2d4de05..000000000 --- a/test/regress/regress0/sygus/max.smt2 +++ /dev/null @@ -1,52 +0,0 @@ -; EXPECT: unsat -; COMMAND-LINE: --cegqi --lang=smt2.5 - -(set-logic UFDTLIA) - -(declare-datatypes () ((start (startx) - (starty) - (start1) - (start0) - (startplus (startplus1 start) (startplus2 start)) - (startminus (startminus1 start) (startminus2 start)) - (startite (startite1 startbool) (startite2 start) (startite3 start))) - (startbool (startand (startand1 startbool) (startand2 startbool)) - (startor (startor1 startbool) (startor2 startbool)) - (startnot (startnot1 startbool)) - (startleq (startleq1 start) (startleq2 start)) - (starteq (starteq1 start) (starteq2 start)) - (startgeq (startgeq1 start) (startgeq2 start)) - ))) - -(declare-fun eval (start Int Int) Int) -(declare-fun evalbool (startbool Int Int) Bool) - -(assert (forall ((x Int) (y Int)) (! (= (eval startx x y) x) :pattern ((eval startx x y))))) -(assert (forall ((x Int) (y Int)) (! (= (eval starty x y) y) :pattern ((eval starty x y))))) -(assert (forall ((x Int) (y Int)) (! (= (eval start0 x y) 0) :pattern ((eval start0 x y))))) -(assert (forall ((x Int) (y Int)) (! (= (eval start1 x y) 1) :pattern ((eval start1 x y))))) -(assert (forall ((s1 start) (s2 start) (x Int) (y Int)) (! (= (eval (startplus s1 s2) x y) (+ (eval s1 x y) (eval s2 x y))) :pattern ((eval (startplus s1 s2) x y))))) -(assert (forall ((s1 start) (s2 start) (x Int) (y Int)) (! (= (eval (startminus s1 s2) x y) (- (eval s1 x y) (eval s2 x y))) :pattern ((eval (startminus s1 s2) x y))))) -(assert (forall ((s1 startbool) (s2 start) (s3 start) (x Int) (y Int)) (! (= (eval (startite s1 s2 s3) x y) (ite (evalbool s1 x y) (eval s2 x y) (eval s3 x y))) - :pattern ((eval (startite s1 s2 s3) x y))))) - -(assert (forall ((s1 startbool) (s2 startbool) (x Int) (y Int)) (! (= (evalbool (startand s1 s2) x y) (and (evalbool s1 x y) (evalbool s2 x y))) - :pattern ((evalbool (startand s1 s2) x y))))) -(assert (forall ((s1 startbool) (s2 startbool) (x Int) (y Int)) (! (= (evalbool (startor s1 s2) x y) (or (evalbool s1 x y) (evalbool s2 x y))) - :pattern ((evalbool (startor s1 s2) x y))))) -(assert (forall ((s1 startbool) (x Int) (y Int)) (! (= (evalbool (startnot s1) x y) (not (evalbool s1 x y))) - :pattern ((evalbool (startnot s1) x y))))) -(assert (forall ((s1 start) (s2 start) (x Int) (y Int)) (! (= (evalbool (startleq s1 s2) x y) (<= (eval s1 x y) (eval s2 x y))) - :pattern ((evalbool (startleq s1 s2) x y))))) -(assert (forall ((s1 start) (s2 start) (x Int) (y Int)) (! (= (evalbool (starteq s1 s2) x y) (= (eval s1 x y) (eval s2 x y))) - :pattern ((evalbool (starteq s1 s2) x y))))) -(assert (forall ((s1 start) (s2 start) (x Int) (y Int)) (! (= (evalbool (startgeq s1 s2) x y) (>= (eval s1 x y) (eval s2 x y))) - :pattern ((evalbool (startgeq s1 s2) x y))))) - - -(define-fun P ((fmax start) (x Int) (y Int)) Bool (and (>= (eval fmax x y) x) (>= (eval fmax x y) y) (or (= (eval fmax x y) x) (= (eval fmax x y) y)))) - -(assert (forall ((fmax start)) (! (exists ((x Int) (y Int)) (not (P fmax x y))) :sygus))) - - -(check-sat) |