Initial import of SMTCoq v1.2

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