diff options
author | Chantal Keller <Chantal.Keller@inria.fr> | 2015-01-12 16:28:10 +0100 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@inria.fr> | 2015-01-12 16:28:10 +0100 |
commit | cfb4587e26623318f432c7e3e21711afc2b966e7 (patch) | |
tree | a90c6f372633458aa0766510bcfdc4682eaa8f6a /examples | |
parent | 1e10dcc783b82269cc3fe3bb7419b9c1cc9e0fa7 (diff) | |
download | smtcoq-cfb4587e26623318f432c7e3e21711afc2b966e7.tar.gz smtcoq-cfb4587e26623318f432c7e3e21711afc2b966e7.zip |
Initial import of SMTCoq v1.2
Diffstat (limited to 'examples')
-rw-r--r-- | examples/Example.v | 67 | ||||
-rw-r--r-- | examples/euf.log | 8 | ||||
-rw-r--r-- | examples/euf.smt2 | 11 | ||||
-rw-r--r-- | examples/example.ml | 7 | ||||
-rw-r--r-- | examples/hole4.cnf | 76 | ||||
-rw-r--r-- | examples/hole4.log | 49 | ||||
-rw-r--r-- | examples/sat.cnf | 6 | ||||
-rw-r--r-- | examples/sat.log | 5 |
8 files changed, 229 insertions, 0 deletions
diff --git a/examples/Example.v b/examples/Example.v new file mode 100644 index 0000000..9dacc6a --- /dev/null +++ b/examples/Example.v @@ -0,0 +1,67 @@ +(* "Require Import SMTCoq." is needed to use the SMTCoq program *) + +Require Import SMTCoq. +Require Import Bool. +Local Open Scope int63_scope. + +(* Examples that check ZChaff certificates *) + +Zchaff_Checker "sat.cnf" "sat.log". +Zchaff_Theorem sat "sat.cnf" "sat.log". +Check sat. + +Zchaff_Checker "hole4.cnf" "hole4.log". + +(* Example that checks a VeriT certificate, for logic QF_UF *) + +Section Verit. + Verit_Checker "euf.smt2" "euf.log". +End Verit. + +(* Examples of the zchaff tactic (requires zchaff in your PATH + environment variable): + - with booleans + - with concrete terms *) + +Goal forall a b c, + (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false. +Proof. + zchaff. +Qed. + +Goal forall i j k, + let a := i == j in + let b := j == k in + let c := k == i in + (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false. +Proof. + zchaff. +Qed. + +(* Examples of the verit tactic (requires verit in your PATH environment + variable): + - with booleans + - in logics QF_UF and QF_LIA *) + +Goal forall a b c, ((a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a)) = false. +Proof. + verit. +Qed. + + +Goal forall (a b : Z) (P : Z -> bool) (f : Z -> Z), + (negb (Zeq_bool (f a) b)) || (negb (P (f a))) || (P b). +Proof. + verit. +Qed. + + +Goal forall b1 b2 x1 x2, + implb + (ifb b1 + (ifb b2 (Zeq_bool (2*x1+1) (2*x2+1)) (Zeq_bool (2*x1+1) (2*x2))) + (ifb b2 (Zeq_bool (2*x1) (2*x2+1)) (Zeq_bool (2*x1) (2*x2)))) + ((implb b1 b2) && (implb b2 b1) && (Zeq_bool x1 x2)). +Proof. + verit. +Qed. diff --git a/examples/euf.log b/examples/euf.log new file mode 100644 index 0000000..3bccc6a --- /dev/null +++ b/examples/euf.log @@ -0,0 +1,8 @@ +1:(input (#1:(and #2:(= b a) #3:(= b c) #4:(= c d) #5:(= e c) #6:(= e f) (not #7:(= a f))))) +2:(and (#2) 1 0) +3:(and (#3) 1 1) +4:(and (#5) 1 3) +5:(and (#6) 1 4) +6:(and ((not #7)) 1 5) +7:(eq_transitive ((not #2) (not #3) (not #5) (not #6) #7)) +8:(resolution () 7 2 3 4 5 6) diff --git a/examples/euf.smt2 b/examples/euf.smt2 new file mode 100644 index 0000000..c151654 --- /dev/null +++ b/examples/euf.smt2 @@ -0,0 +1,11 @@ +(set-logic QF_UF) +(declare-sort U 0) +(declare-fun a () U) +(declare-fun b () U) +(declare-fun c () U) +(declare-fun d () U) +(declare-fun e () U) +(declare-fun f () U) +(assert (and (= a b) (= b c) (= c d) (= c e) (= e f) (not (= a f)))) +(check-sat) +(exit) diff --git a/examples/example.ml b/examples/example.ml new file mode 100644 index 0000000..0bb7178 --- /dev/null +++ b/examples/example.ml @@ -0,0 +1,7 @@ +let _ = Printf.printf "Zchaff_checker.checker \"sat.cnf\" \"sat.log\" = %b\n" (Zchaff_checker.checker "sat.cnf" "sat.log") +let _ = Printf.printf "Zchaff_checker.checker \"hole4.cnf\" \"hole4.log\" = %b\n" (Zchaff_checker.checker "hole4.cnf" "hole4.log") + + + + +let _ = Printf.printf "Verit_checker.checker \"euf.smt2\" \"euf.log\" = %b\n" (Verit_checker.checker "euf.smt2" "euf.log") diff --git a/examples/hole4.cnf b/examples/hole4.cnf new file mode 100644 index 0000000..9dd148c --- /dev/null +++ b/examples/hole4.cnf @@ -0,0 +1,76 @@ +p cnf 20 75 +1 2 3 4 0 +5 6 7 8 0 +9 10 11 12 0 +13 14 15 16 0 +17 18 19 20 0 +-1 -2 0 +-1 -3 0 +-1 -4 0 +-2 -3 0 +-2 -4 0 +-3 -4 0 +-5 -6 0 +-5 -7 0 +-5 -8 0 +-6 -7 0 +-6 -8 0 +-7 -8 0 +-9 -10 0 +-9 -11 0 +-9 -12 0 +-10 -11 0 +-10 -12 0 +-11 -12 0 +-13 -14 0 +-13 -15 0 +-13 -16 0 +-14 -15 0 +-14 -16 0 +-15 -16 0 +-17 -18 0 +-17 -19 0 +-17 -20 0 +-18 -19 0 +-18 -20 0 +-19 -20 0 +-1 -5 0 +-1 -9 0 +-1 -13 0 +-1 -17 0 +-5 -9 0 +-5 -13 0 +-5 -17 0 +-9 -13 0 +-9 -17 0 +-13 -17 0 +-2 -6 0 +-2 -10 0 +-2 -14 0 +-2 -18 0 +-6 -10 0 +-6 -14 0 +-6 -18 0 +-10 -14 0 +-10 -18 0 +-14 -18 0 +-3 -7 0 +-3 -11 0 +-3 -15 0 +-3 -19 0 +-7 -11 0 +-7 -15 0 +-7 -19 0 +-11 -15 0 +-11 -19 0 +-15 -19 0 +-4 -8 0 +-4 -12 0 +-4 -16 0 +-4 -20 0 +-8 -12 0 +-8 -16 0 +-8 -20 0 +-12 -16 0 +-12 -20 0 +-16 -20 0 diff --git a/examples/hole4.log b/examples/hole4.log new file mode 100644 index 0000000..ab23cdd --- /dev/null +++ b/examples/hole4.log @@ -0,0 +1,49 @@ +CL: 75 <= 65 1 0 59 56 +CL: 76 <= 55 1 0 69 66 2 75 52 50 47 +CL: 77 <= 60 3 1 72 69 2 46 45 +CL: 78 <= 57 3 0 70 65 +CL: 79 <= 57 3 0 72 66 +CL: 80 <= 67 3 0 60 55 1 49 2 79 78 77 +CL: 81 <= 45 1 0 70 67 3 62 59 56 80 76 44 43 41 38 +CL: 82 <= 61 4 1 74 70 +CL: 83 <= 71 4 1 64 60 3 82 53 49 +CL: 84 <= 51 4 1 64 60 3 73 72 69 2 83 36 35 +CL: 85 <= 48 4 0 73 66 +CL: 86 <= 4 51 68 1 0 78 +CL: 87 <= 71 4 1 48 45 86 39 2 85 64 60 57 +CL: 88 <= 51 4 1 58 55 +CL: 89 <= 82 48 45 0 88 39 2 74 72 70 67 3 87 +CL: 90 <= 58 4 0 74 67 +CL: 91 <= 68 4 0 64 57 3 90 53 46 89 84 +CL: 92 <= 61 4 1 68 65 0 53 49 46 +CL: 93 <= 1 45 61 0 85 69 66 2 92 +CL: 94 <= 53 4 2 71 69 +CL: 95 <= 2 49 73 1 88 94 58 55 93 42 40 37 +CL: 96 <= 58 4 0 73 66 2 39 35 +CL: 97 <= 36 2 0 73 68 4 61 55 +CL: 98 <= 0 58 36 4 2 71 69 65 1 97 96 54 52 50 47 91 95 +CL: 99 <= 71 4 1 54 50 +CL: 100 <= 51 4 1 74 70 3 99 37 35 +CL: 101 <= 68 4 0 54 47 +CL: 102 <= 40 3 1 74 71 4 48 45 +VAR: 1 L: 9 V: 0 A: 100 Lits: 34 38 14 30 3 +VAR: 2 L: 11 V: 0 A: 102 Lits: 28 30 14 34 38 5 +VAR: 3 L: 5 V: 0 A: 56 Lits: 7 23 +VAR: 4 L: 12 V: 1 A: 0 Lits: 2 4 6 8 +VAR: 5 L: 18 V: 0 A: 40 Lits: 11 27 +VAR: 6 L: 19 V: 0 A: 51 Lits: 13 37 +VAR: 7 L: 6 V: 0 A: 59 Lits: 15 23 +VAR: 8 L: 13 V: 0 A: 65 Lits: 9 17 +VAR: 9 L: 2 V: 0 A: 18 Lits: 19 23 +VAR: 10 L: 3 V: 0 A: 20 Lits: 21 23 +VAR: 11 L: 1 V: 1 A: 98 Lits: 34 22 +VAR: 12 L: 4 V: 0 A: 22 Lits: 23 25 +VAR: 13 L: 16 V: 1 A: 3 Lits: 26 28 30 32 +VAR: 14 L: 10 V: 0 A: 101 Lits: 34 38 2 6 29 +VAR: 15 L: 7 V: 0 A: 62 Lits: 23 31 +VAR: 16 L: 14 V: 0 A: 67 Lits: 9 33 +VAR: 17 L: 0 V: 0 A: 81 Lits: 35 +VAR: 18 L: 17 V: 1 A: 4 Lits: 34 36 38 40 +VAR: 19 L: 8 V: 0 A: 63 Lits: 23 39 +VAR: 20 L: 15 V: 0 A: 68 Lits: 9 41 +CONF: 1 == 10 12 14 16 diff --git a/examples/sat.cnf b/examples/sat.cnf new file mode 100644 index 0000000..508791a --- /dev/null +++ b/examples/sat.cnf @@ -0,0 +1,6 @@ +p cnf 3 5 +1 2 3 0 +-1 -2 -3 0 +-1 2 0 +-2 3 0 +-3 1 0 diff --git a/examples/sat.log b/examples/sat.log new file mode 100644 index 0000000..af89d7c --- /dev/null +++ b/examples/sat.log @@ -0,0 +1,5 @@ +CL: 5 <= 2 1 4 +VAR: 1 L: 2 V: 0 A: 2 Lits: 3 4 +VAR: 2 L: 1 V: 0 A: 3 Lits: 5 6 +VAR: 3 L: 0 V: 0 A: 5 Lits: 7 +CONF: 0 == 2 4 6 |