diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-09-06 15:28:07 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-06 15:28:07 -0700 |
commit | 91a5055015a97935d19b3dbf18062e189268a1f9 (patch) | |
tree | fb1fd19d80fb89d71286b462927540c0648d7551 /test/regress/regress1/fmf | |
parent | 7fc142a10140bba5a732237e3adf8fe6729d90e7 (diff) |
Remove SMT1 parser. (#3228)
This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version).
Fixes #2948 and fixes #1313.
Diffstat (limited to 'test/regress/regress1/fmf')
-rw-r--r-- | test/regress/regress1/fmf/Hoare-z3.931718.smt | 49 | ||||
-rw-r--r-- | test/regress/regress1/fmf/Hoare-z3.931718.smtv1.smt2 | 48 |
2 files changed, 48 insertions, 49 deletions
diff --git a/test/regress/regress1/fmf/Hoare-z3.931718.smt b/test/regress/regress1/fmf/Hoare-z3.931718.smt deleted file mode 100644 index 4ab90756c..000000000 --- a/test/regress/regress1/fmf/Hoare-z3.931718.smt +++ /dev/null @@ -1,49 +0,0 @@ -; COMMAND-LINE: --finite-model-find -; EXPECT: sat -(benchmark Isabelle -:status sat -:logic AUFLIA -:extrasorts ( S1 S2 S3 S4 S5 S6 S7 S8 S9 S10 S11) -:extrafuns ( - (f1 S1) - (f2 S1) - (f3 S3 S2 S1) - (f4 S4 S2 S3) - (f5 S4) - (f6 S5 S5 S1) - (f7 S5) - (f8 S6 S5 S5) - (f9 S7 S6) - (f10 S8 S4 S7) - (f11 S9 S10 S8) - (f12 S11 S4 S9) - (f13 S11) - (f14 S4) - (f15 S10) - (f16 S4) - (f17 S10 S4) - (f18 S5 S5 S1) -) -:assumption (not (= f1 f2)) -:assumption (forall (?v0 S2) (?v1 S2) (iff (= (f3 (f4 f5 ?v0) ?v1) f1) (= ?v0 ?v1)) ) -:assumption (not (= (f6 f7 (f8 (f9 (f10 (f11 (f12 f13 f14) f15) f16)) f7)) f1)) -:assumption (= (f6 f7 (f8 (f9 (f10 (f11 (f12 f13 f5) f15) (f17 f15))) f7)) f1) -:assumption (= (f18 f7 (f8 (f9 (f10 (f11 (f12 f13 f14) f15) f16)) f7)) f1) -:assumption (forall (?v0 S5) (= (f6 ?v0 f7) f1) ) -:assumption (forall (?v0 S4) (?v1 S10) (?v2 S4) (?v3 S4) (?v4 S10) (?v5 S4) (iff (= (f10 (f11 (f12 f13 ?v0) ?v1) ?v2) (f10 (f11 (f12 f13 ?v3) ?v4) ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5)))) ) -:assumption (forall (?v0 S5) (?v1 S5) (implies (= (f6 ?v0 ?v1) f1) (= (f18 ?v0 ?v1) f1)) ) -:assumption (forall (?v0 S5) (?v1 S5) (?v2 S5) (implies (= (f6 ?v0 ?v1) f1) (implies (= (f6 ?v2 ?v0) f1) (= (f6 ?v2 ?v1) f1))) ) -:assumption (forall (?v0 S5) (?v1 S7) (?v2 S5) (implies (= (f6 ?v0 (f8 (f9 ?v1) f7)) f1) (implies (= (f6 ?v0 ?v2) f1) (= (f6 ?v0 (f8 (f9 ?v1) ?v2)) f1))) ) -:assumption (forall (?v0 S5) (?v1 S7) (?v2 S5) (implies (= (f6 ?v0 (f8 (f9 ?v1) ?v2)) f1) (and (= (f6 ?v0 (f8 (f9 ?v1) f7)) f1) (= (f6 ?v0 ?v2) f1))) ) -:assumption (forall (?v0 S5) (?v1 S4) (?v2 S10) (?v3 S4) (?v4 S4) (implies (= (f6 ?v0 (f8 (f9 (f10 (f11 (f12 f13 ?v1) ?v2) ?v3)) f7)) f1) (implies (forall (?v5 S2) (?v6 S2) (implies (= (f3 (f4 ?v3 ?v5) ?v6) f1) (= (f3 (f4 ?v4 ?v5) ?v6) f1))) (= (f6 ?v0 (f8 (f9 (f10 (f11 (f12 f13 ?v1) ?v2) ?v4)) f7)) f1))) ) -:assumption (forall (?v0 S5) (?v1 S4) (?v2 S10) (?v3 S4) (?v4 S4) (implies (= (f6 ?v0 (f8 (f9 (f10 (f11 (f12 f13 ?v1) ?v2) ?v3)) f7)) f1) (implies (forall (?v5 S2) (?v6 S2) (implies (= (f3 (f4 ?v4 ?v5) ?v6) f1) (= (f3 (f4 ?v1 ?v5) ?v6) f1))) (= (f6 ?v0 (f8 (f9 (f10 (f11 (f12 f13 ?v4) ?v2) ?v3)) f7)) f1))) ) -:formula true) -; solver: z3 -; timeout: 5.0 -; random seed: 1 -; arguments: -; DISPLAY_PROOF=true -; PROOF_MODE=2 -; -rs:1 -; MODEL=true -; -smt diff --git a/test/regress/regress1/fmf/Hoare-z3.931718.smtv1.smt2 b/test/regress/regress1/fmf/Hoare-z3.931718.smtv1.smt2 new file mode 100644 index 000000000..8ee89145b --- /dev/null +++ b/test/regress/regress1/fmf/Hoare-z3.931718.smtv1.smt2 @@ -0,0 +1,48 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-option :incremental false) +(set-info :status sat) +(set-logic AUFLIA) +(declare-sort S1 0) +(declare-sort S2 0) +(declare-sort S3 0) +(declare-sort S4 0) +(declare-sort S5 0) +(declare-sort S6 0) +(declare-sort S7 0) +(declare-sort S8 0) +(declare-sort S9 0) +(declare-sort S10 0) +(declare-sort S11 0) +(declare-fun f1 () S1) +(declare-fun f2 () S1) +(declare-fun f3 (S3 S2) S1) +(declare-fun f4 (S4 S2) S3) +(declare-fun f5 () S4) +(declare-fun f6 (S5 S5) S1) +(declare-fun f7 () S5) +(declare-fun f8 (S6 S5) S5) +(declare-fun f9 (S7) S6) +(declare-fun f10 (S8 S4) S7) +(declare-fun f11 (S9 S10) S8) +(declare-fun f12 (S11 S4) S9) +(declare-fun f13 () S11) +(declare-fun f14 () S4) +(declare-fun f15 () S10) +(declare-fun f16 () S4) +(declare-fun f17 (S10) S4) +(declare-fun f18 (S5 S5) S1) +(assert (not (= f1 f2))) +(assert (forall ((?v0 S2) (?v1 S2)) (= (= (f3 (f4 f5 ?v0) ?v1) f1) (= ?v0 ?v1)) )) +(assert (not (= (f6 f7 (f8 (f9 (f10 (f11 (f12 f13 f14) f15) f16)) f7)) f1))) +(assert (= (f6 f7 (f8 (f9 (f10 (f11 (f12 f13 f5) f15) (f17 f15))) f7)) f1)) +(assert (= (f18 f7 (f8 (f9 (f10 (f11 (f12 f13 f14) f15) f16)) f7)) f1)) +(assert (forall ((?v0 S5)) (= (f6 ?v0 f7) f1) )) +(assert (forall ((?v0 S4) (?v1 S10) (?v2 S4) (?v3 S4) (?v4 S10) (?v5 S4)) (= (= (f10 (f11 (f12 f13 ?v0) ?v1) ?v2) (f10 (f11 (f12 f13 ?v3) ?v4) ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5)))) )) +(assert (forall ((?v0 S5) (?v1 S5)) (=> (= (f6 ?v0 ?v1) f1) (= (f18 ?v0 ?v1) f1)) )) +(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5)) (=> (= (f6 ?v0 ?v1) f1) (=> (= (f6 ?v2 ?v0) f1) (= (f6 ?v2 ?v1) f1))) )) +(assert (forall ((?v0 S5) (?v1 S7) (?v2 S5)) (let ((_let_0 (f9 ?v1))) (=> (= (f6 ?v0 (f8 _let_0 f7)) f1) (=> (= (f6 ?v0 ?v2) f1) (= (f6 ?v0 (f8 _let_0 ?v2)) f1)))) )) +(assert (forall ((?v0 S5) (?v1 S7) (?v2 S5)) (let ((_let_0 (f9 ?v1))) (=> (= (f6 ?v0 (f8 _let_0 ?v2)) f1) (and (= (f6 ?v0 (f8 _let_0 f7)) f1) (= (f6 ?v0 ?v2) f1)))) )) +(assert (forall ((?v0 S5) (?v1 S4) (?v2 S10) (?v3 S4) (?v4 S4)) (let ((_let_0 (f11 (f12 f13 ?v1) ?v2))) (=> (= (f6 ?v0 (f8 (f9 (f10 _let_0 ?v3)) f7)) f1) (=> (forall ((?v5 S2) (?v6 S2)) (=> (= (f3 (f4 ?v3 ?v5) ?v6) f1) (= (f3 (f4 ?v4 ?v5) ?v6) f1)) ) (= (f6 ?v0 (f8 (f9 (f10 _let_0 ?v4)) f7)) f1)))) )) +(assert (forall ((?v0 S5) (?v1 S4) (?v2 S10) (?v3 S4) (?v4 S4)) (=> (= (f6 ?v0 (f8 (f9 (f10 (f11 (f12 f13 ?v1) ?v2) ?v3)) f7)) f1) (=> (forall ((?v5 S2) (?v6 S2)) (=> (= (f3 (f4 ?v4 ?v5) ?v6) f1) (= (f3 (f4 ?v1 ?v5) ?v6) f1)) ) (= (f6 ?v0 (f8 (f9 (f10 (f11 (f12 f13 ?v4) ?v2) ?v3)) f7)) f1))) )) +(check-sat-assuming ( true )) |