diff options
Diffstat (limited to 'unit-tests')
| -rw-r--r-- | unit-tests/Makefile | 3 | ||||
| -rw-r--r-- | unit-tests/Tests_lfsc.v | 700 | ||||
| -rw-r--r-- | unit-tests/Tests_verit.v | 139 | ||||
| -rw-r--r-- | unit-tests/Tests_zchaff.v | 12 | ||||
| -rw-r--r-- | unit-tests/bv1.log | 12 | ||||
| -rw-r--r-- | unit-tests/bv1.smt2 | 5 | ||||
| -rw-r--r-- | unit-tests/bv2.log | 15 | ||||
| -rw-r--r-- | unit-tests/bv2.smt2 | 5 | ||||
| -rw-r--r-- | unit-tests/demo_lfsc_bool.v | 199 | ||||
| -rw-r--r-- | unit-tests/demo_lfsc_prop.v | 233 | ||||
| -rw-r--r-- | unit-tests/ex1.lfsc | 23 | ||||
| -rw-r--r-- | unit-tests/ex1.smt2 | 11 | ||||
| -rw-r--r-- | unit-tests/large1.v | 88 | ||||
| -rw-r--r-- | unit-tests/sat6.smt2 | 2 |
14 files changed, 1400 insertions, 47 deletions
diff --git a/unit-tests/Makefile b/unit-tests/Makefile index bed1018..1ad9b57 100644 --- a/unit-tests/Makefile +++ b/unit-tests/Makefile @@ -10,9 +10,10 @@ COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) COQC?=$(COQBIN)coqc -all: $(OBJ) Tests_zchaff.vo Tests_verit.vo +all: zchaff verit lfsc zchaff: $(ZCHAFFLOG) Tests_zchaff.vo verit: $(VERITLOG) Tests_verit.vo +lfsc: Tests_lfsc.vo logs: $(OBJ) diff --git a/unit-tests/Tests_lfsc.v b/unit-tests/Tests_lfsc.v new file mode 100644 index 0000000..9734fde --- /dev/null +++ b/unit-tests/Tests_lfsc.v @@ -0,0 +1,700 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2019 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +Add Rec LoadPath "../src" as SMTCoq. + +Require Import SMTCoq. +Require Import Bool PArray Int63 List ZArith Logic. + + +Infix "-->" := implb (at level 60, right associativity) : bool_scope. + + +Section BV. + +Import BVList.BITVECTOR_LIST. +Local Open Scope bv_scope. + + Goal forall (a b c: bitvector 4), + (c = (bv_and a b)) -> + ((bv_and (bv_and c a) b) = c). + Proof. + smt. + Qed. + + Goal forall (bv1 bv2 bv3: bitvector 4), + bv1 = #b|0|0|0|0| /\ + bv2 = #b|1|0|0|0| /\ + bv3 = #b|1|1|0|0| -> + bv_ultP bv1 bv2 /\ bv_ultP bv2 bv3. + Proof. + smt. + Qed. + + + Goal forall (a: bitvector 32), a = a. + Proof. + smt. + Qed. + + (* TODO: will be ok when symmetry of equality is back for verit *) + (* Goal forall (bv1 bv2: bitvector 4), *) + (* bv1 = bv2 <-> bv2 = bv1. *) + (* Proof. *) + (* smt. *) + (* Qed. *) + +End BV. + + +Section Arrays. + + Import FArray. + Local Open Scope farray_scope. + + + Goal forall (a:farray Z Z) i j, i = j -> a[i] = a[j]. + Proof. + smt. + Qed. + + Goal forall (a b: farray Z Z) + (v w x y: Z) + (g: farray Z Z -> Z) + (f: Z -> Z), + (a[x <- v] = b) /\ a[y <- w] = b -> + (f x) = (f y) \/ (g a) = (g b). + Proof. + smt. + Qed. + + + (* TODO *) + (* Goal forall (a b c d: farray Z Z), *) + (* b[0%Z <- 4] = c -> *) + (* d = b[0%Z <- 4][1%Z <- 4] -> *) + (* a = d[1%Z <- b[1%Z]] -> *) + (* a = c. *) + (* Proof. *) + (* smt. *) + (* Qed. *) + + +(* + Goal forall (a b: farray Z Z) i, + (select (store (store (store a i 3%Z) 1%Z (select (store b i 4) i)) 2%Z 2%Z) 1%Z) = 4. + Proof. + smt. + rewrite read_over_other_write; try easy. + rewrite read_over_same_write; try easy; try apply Z_compdec. + rewrite read_over_same_write; try easy; try apply Z_compdec. + Qed. +*) + + +End Arrays. + + +Section EUF. + + Goal forall + (x y: Z) + (f: Z -> Z), + y = x -> (f x) = (f y). + Proof. + smt. + Qed. + + (* TODO: will be ok when symmetry of equality is back for verit *) + (* Goal forall *) + (* (x y: Z) *) + (* (f: Z -> Z), *) + (* (f x) = (f y) -> (f y) = (f x). *) + (* Proof. *) + (* smt. *) + (* Qed. *) + + + Goal forall + (x y: Z) + (f: Z -> Z), + x + 1 = (y + 1) -> (f y) = (f x). + Proof. + smt. + Qed. + + + Goal forall + (x y: Z) + (f: Z -> Z), + x = (y + 1) -> (f y) = (f (x - 1)). + Proof. + smt. + Qed. + + Goal forall + (x y: Z) + (f: Z -> Z), + x = (y + 1) -> (f (y + 1)) = (f x). + Proof. + smt. + Qed. + +End EUF. + + +Section LIA. + + + (* TODO: will be ok when symmetry of equality is back for verit *) + (* Goal forall (a b: Z), a = b <-> b = a. *) + (* Proof. *) + (* smt. *) + (* Qed. *) + + Goal forall (x y: Z), (x >= y) -> (y < x) \/ (x = y). + Proof. + smt. + Qed. + + + Goal forall (f : Z -> Z) (a:Z), ((f a) > 1) -> ((f a) + 1) >= 2 \/((f a) = 30) . + Proof. + smt. + Qed. + + Goal forall x: Z, (x = 0%Z) -> (8 >= 0). + Proof. + smt. + Qed. + + Goal forall x: Z, ~ (x < 0%Z) -> (8 >= 0). + Proof. + smt. + Qed. + + Goal forall (a b: Z), a < b -> a < (b + 1). + Proof. + smt. + Qed. + + Goal forall (a b: Z), (a < b) -> (a + 2) < (b + 3). + Proof. + smt. + Qed. + + + Goal forall a b, a < b -> a < (b + 10). + Proof. + smt. + Qed. + + +End LIA. + + +Section PR. + + Local Open Scope int63_scope. + +(* Simple connectors *) + +Goal forall (a:bool), a || negb a. + smt. +Qed. + +Goal forall a, negb (a || negb a) = false. + smt. +Qed. + +Goal forall a, (a && negb a) = false. + smt. +Qed. + +Goal forall a, negb (a && negb a). + smt. +Qed. + +Goal forall a, a --> a. + smt. +Qed. + +Goal forall a, negb (a --> a) = false. + smt. +Qed. + + +Goal forall a , (xorb a a) || negb (xorb a a). + smt. +Qed. + + +Goal forall a, (a||negb a) || negb (a||negb a). + smt. +Qed. + +(* Polarities *) + +Goal forall a b, andb (orb (negb (negb a)) b) (negb (orb a b)) = false. +Proof. + smt. +Qed. + + +Goal forall a b, andb (orb a b) (andb (negb a) (negb b)) = false. +Proof. + smt. +Qed. + +(* Multiple negations *) + +Goal forall a, orb a (negb (negb (negb a))) = true. +Proof. + smt. +Qed. + + +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. + smt. +Qed. + + +Goal true. + smt. +Qed. + +Goal negb false. + smt. +Qed. + + +Goal forall a, Bool.eqb a a. +Proof. + smt. +Qed. + + +Goal forall (a:bool), a = a. + smt. +Qed. + +Goal (false || true) && false = false. +Proof. + smt. +Qed. + + +Goal negb true = false. +Proof. + smt. +Qed. + + +Goal false = false. +Proof. + smt. +Qed. + +Goal forall x y, Bool.eqb (xorb x y) ((x && (negb y)) || ((negb x) && y)). +Proof. + smt. +Qed. + + +Goal forall x y, Bool.eqb (x --> y) ((x && y) || (negb x)). +Proof. + smt. +Qed. + + +Goal forall x y z, Bool.eqb (ifb x y z) ((x && y) || ((negb x) && z)). +Proof. + smt. +Qed. + + +Goal forall a b c, (((a && b) || (b && c)) && (negb b)) = false. +Proof. + smt. +Qed. + +Goal forall a, ((a || a) && (negb a)) = false. +Proof. + smt. +Qed. + + +Goal forall a, (negb (a || (negb a))) = false. +Proof. + smt. +Qed. + + +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. + smt. +Qed. + + +(** The same goal above with a, b and c are concrete terms *) +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. + smt. +Qed. + + +Goal forall a b c d, ((a && b) && (c || d) && (negb (c || (a && b && d)))) = false. +Proof. + smt. +Qed. + + +Goal forall a b c d, (a && b && c && ((negb a) || (negb b) || d) && ((negb d) || (negb c))) = false. +Proof. + smt. +Qed. + + +(* Pigeon hole: 4 holes, 5 pigeons *) +Goal forall x11 x12 x13 x14 x15 x21 x22 x23 x24 x25 x31 x32 x33 x34 x35 x41 x42 x43 x44 x45, ( + (orb (negb x11) (negb x21)) && + (orb (negb x11) (negb x31)) && + (orb (negb x11) (negb x41)) && + (orb (negb x21) (negb x31)) && + (orb (negb x21) (negb x41)) && + (orb (negb x31) (negb x41)) && + + (orb (negb x12) (negb x22)) && + (orb (negb x12) (negb x32)) && + (orb (negb x12) (negb x42)) && + (orb (negb x22) (negb x32)) && + (orb (negb x22) (negb x42)) && + (orb (negb x32) (negb x42)) && + + (orb (negb x13) (negb x23)) && + (orb (negb x13) (negb x33)) && + (orb (negb x13) (negb x43)) && + (orb (negb x23) (negb x33)) && + (orb (negb x23) (negb x43)) && + (orb (negb x33) (negb x43)) && + + (orb (negb x14) (negb x24)) && + (orb (negb x14) (negb x34)) && + (orb (negb x14) (negb x44)) && + (orb (negb x24) (negb x34)) && + (orb (negb x24) (negb x44)) && + (orb (negb x34) (negb x44)) && + + (orb (negb x15) (negb x25)) && + (orb (negb x15) (negb x35)) && + (orb (negb x15) (negb x45)) && + (orb (negb x25) (negb x35)) && + (orb (negb x25) (negb x45)) && + (orb (negb x35) (negb x45)) && + + + (orb (negb x11) (negb x12)) && + (orb (negb x11) (negb x13)) && + (orb (negb x11) (negb x14)) && + (orb (negb x11) (negb x15)) && + (orb (negb x12) (negb x13)) && + (orb (negb x12) (negb x14)) && + (orb (negb x12) (negb x15)) && + (orb (negb x13) (negb x14)) && + (orb (negb x13) (negb x15)) && + (orb (negb x14) (negb x15)) && + + (orb (negb x21) (negb x22)) && + (orb (negb x21) (negb x23)) && + (orb (negb x21) (negb x24)) && + (orb (negb x21) (negb x25)) && + (orb (negb x22) (negb x23)) && + (orb (negb x22) (negb x24)) && + (orb (negb x22) (negb x25)) && + (orb (negb x23) (negb x24)) && + (orb (negb x23) (negb x25)) && + (orb (negb x24) (negb x25)) && + + (orb (negb x31) (negb x32)) && + (orb (negb x31) (negb x33)) && + (orb (negb x31) (negb x34)) && + (orb (negb x31) (negb x35)) && + (orb (negb x32) (negb x33)) && + (orb (negb x32) (negb x34)) && + (orb (negb x32) (negb x35)) && + (orb (negb x33) (negb x34)) && + (orb (negb x33) (negb x35)) && + (orb (negb x34) (negb x35)) && + + (orb (negb x41) (negb x42)) && + (orb (negb x41) (negb x43)) && + (orb (negb x41) (negb x44)) && + (orb (negb x41) (negb x45)) && + (orb (negb x42) (negb x43)) && + (orb (negb x42) (negb x44)) && + (orb (negb x42) (negb x45)) && + (orb (negb x43) (negb x44)) && + (orb (negb x43) (negb x45)) && + (orb (negb x44) (negb x45)) && + + + (orb (orb (orb x11 x21) x31) x41) && + (orb (orb (orb x12 x22) x32) x42) && + (orb (orb (orb x13 x23) x33) x43) && + (orb (orb (orb x14 x24) x34) x44) && + (orb (orb (orb x15 x25) x35) x45)) = false. +Proof. + smt. +Qed. + + +Goal forall a b c f p, ((Z.eqb a c) && (Z.eqb b c) && ((negb (Z.eqb (f a) (f b))) || ((p a) && (negb (p b))))) = false. +Proof. + smt. +Qed. + + +Goal forall a b c (p : Z -> bool), ((((p a) && (p b)) || ((p b) && (p c))) && (negb (p b))) = false. +Proof. + smt. +Qed. + + +Goal forall x y z f, ((Z.eqb x y) && (Z.eqb y z) && (negb (Z.eqb (f x) (f z)))) = false. +Proof. + smt. +Qed. + +Goal forall x y z f, ((negb (Z.eqb (f x) (f y))) && (Z.eqb y z) && (Z.eqb (f x) (f (f z))) && (Z.eqb x y)) = false. +Proof. + smt. +Qed. + +Goal forall a b c d e f, ((Z.eqb a b) && (Z.eqb b c) && (Z.eqb c d) && (Z.eqb c e) && (Z.eqb e f) && (negb (Z.eqb a f))) = false. +Proof. + smt. +Qed. + + + +Goal forall x y z, ((x <=? 3) && ((y <=? 7) || (z <=? 9))) --> + ((x + y <=? 10) || (x + z <=? 12)) = true. +Proof. + smt. +Qed. + +Goal forall x, (Z.eqb (x - 3) 7) --> (x >=? 10) = true. +Proof. + smt. +Qed. + + +Goal forall x y, (x >? y) --> (y + 1 <=? x) = true. +Proof. + smt. +Qed. + + +Goal forall x y, Bool.eqb (x <? y) (x <=? y - 1) = true. +Proof. + smt. +Qed. + +Goal forall x y, ((x + y <=? - (3)) && (y >=? 0) + || (x <=? - (3))) && (x >=? 0) = false. + Proof. + smt. + Qed. + +Goal forall x, (andb ((x - 3) <=? 7) (7 <=? (x - 3))) --> (x >=? 10) = true. +Proof. + smt. +Qed. + +Goal forall x, (Z.eqb (x - 3) 7) --> (10 <=? x) = true. +Proof. + smt. +Qed. + + +(* More general examples *) +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. + smt. +Qed. + + +Goal forall (a b : Z) (P : Z -> bool) (f : Z -> Z), + (negb (Z.eqb (f a) b)) || (negb (P (f a))) || (P b). +Proof. + smt. +Qed. + + +Goal forall b1 b2 x1 x2, + (ifb b1 + (ifb b2 (Z.eqb (2*x1+1) (2*x2+1)) (Z.eqb (2*x1+1) (2*x2))) + (ifb b2 (Z.eqb (2*x1) (2*x2+1)) (Z.eqb (2*x1) (2*x2)))) --> + ((b1 --> b2) && (b2 --> b1) && (Z.eqb x1 x2)). +Proof. + smt. +Qed. + + +(* With let ... in ... *) +Goal forall b, + let a := b in + a && (negb a) = false. +Proof. + smt. +Qed. + +Goal forall b, + let a := b in + a || (negb a) = true. +Proof. + smt. +Qed. + +(* With concrete terms *) +Goal forall i j, + let a := i == j in + a && (negb a) = false. +Proof. + smt. +Qed. + +Goal forall i j, + let a := i == j in + a || (negb a) = true. +Proof. + smt. +Qed. + + +(* Congruence in which some premises are REFL *) +Goal forall (f:Z -> Z -> Z) x y z, + (Z.eqb x y) --> (Z.eqb (f z x) (f z y)). +Proof. + smt. +Qed. + +Goal forall (f:Z -> Z -> Z) x y z, + (x = y) -> (f z x) = (f z y). +Proof. + smt. +Qed. + +Goal forall (P:Z -> Z -> bool) x y z, + (Z.eqb x y) --> ((P z x) --> (P z y)). +Proof. + smt. +Qed. + + +End PR. + + +Section A_BV_EUF_LIA_PR. + Import BVList.BITVECTOR_LIST FArray. + + Local Open Scope farray_scope. + Local Open Scope bv_scope. + + (* TODO *) + (* Goal forall (bv1 bv2 : bitvector 4) *) + (* (a b c d : farray (bitvector 4) Z), *) + (* bv1 = #b|0|0|0|0| -> *) + (* bv2 = #b|1|0|0|0| -> *) + (* c = b[bv1 <- 4] -> *) + (* d = b[bv1 <- 4][bv2 <- 4] -> *) + (* a = d[bv2 <- b[bv2]] -> *) + (* a = c. *) + (* Proof. *) + (* smt. *) + (* Qed. *) + + (* TODO *) + (* Goal forall (bv1 bv2 : bitvector 4) *) + (* (a b c d : farray (bitvector 4) Z), *) + (* bv1 = #b|0|0|0|0| /\ *) + (* bv2 = #b|1|0|0|0| /\ *) + (* c = b[bv1 <- 4] /\ *) + (* d = b[bv1 <- 4][bv2 <- 4] /\ *) + (* a = d[bv2 <- b[bv2]] -> *) + (* a = c. *) + (* Proof. *) + (* smt. *) + (* Qed. *) + + (** the example in the CAV paper *) + Goal forall (a b: farray Z Z) (v w x y: Z) + (r s: bitvector 4) + (f: Z -> Z) + (g: farray Z Z -> Z) + (h: bitvector 4 -> Z), + a[x <- v] = b /\ a[y <- w] = b -> + r = s /\ h r = v /\ h s = y -> + v < x + 1 /\ v > x - 1 -> + f (h r) = f (h s) \/ g a = g b. + Proof. + smt. (** "cvc4. verit." also solves the goal *) + Qed. + + (** the example in the FroCoS paper *) + Goal forall (a b: farray Z Z) (v w x y z t: Z) + (r s: bitvector 4) + (f: Z -> Z) + (g: farray Z Z -> Z) + (h: bitvector 4 -> Z), + a[x <- v] = b /\ a[y <- w] = b -> + a[z <- w] = b /\ a[t <- v] = b -> + r = s -> v < x + 10 /\ v > x - 5 -> + ~ (g a = g b) \/ f (h r) = f (h s). + Proof. + smt. (** "cvc4. verit." also solves the goal *) + Qed. + + + Goal forall (a b: farray (bitvector 4) Z) + (x y: bitvector 4) + (v: Z), + b[bv_add y x <- v] = a /\ + b = a[bv_add x y <- v] -> + a = b. + Proof. + smt. + (* CVC4 preprocessing hole on BV *) + replace (bv_add x y) with (bv_add y x) + by apply bv_eq_reflect, bv_add_comm. + verit. + Qed. + + Goal forall (a:farray Z Z), a = a. + Proof. + smt. + Qed. + + (* TODO: will be ok when symmetry of equality is back for verit *) + (* Goal forall (a b: farray Z Z), a = b <-> b = a. *) + (* Proof. *) + (* smt. *) + (* Qed. *) + +End A_BV_EUF_LIA_PR. diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v index ba69110..cfb8f16 100644 --- a/unit-tests/Tests_verit.v +++ b/unit-tests/Tests_verit.v @@ -1,3 +1,15 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2019 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + Add Rec LoadPath "../src" as SMTCoq. Require Import SMTCoq. @@ -34,8 +46,14 @@ Lemma fun_const2 : (forall x, g (f x) 2) -> g (f 3) 2. Proof. intros f g Hf. - verit_base Hf; vauto. + verit_bool_base Hf; vauto. Qed. +(* +Toplevel input, characters 916-942: + Warning: Bytecode compiler failed, falling back to standard conversion + [bytecode-compiler-failed,bytecode-compiler] +*) + (* veriT vernacular commands *) @@ -143,9 +161,12 @@ Section Checker_Lia3. Verit_Checker "lia3.smt2" "lia3.vtlog". End Checker_Lia3. +(* TODO: it does not go through anymore + Anomaly: File "trace/smtCommands.ml", line 102, characters 12-18: Assertion failed. Section Checker_Lia4. Verit_Checker "lia4.smt2" "lia4.vtlog". End Checker_Lia4. +*) Section Checker_Lia5. Verit_Checker "lia5.smt2" "lia5.vtlog". @@ -180,6 +201,14 @@ Section Checker_Lia5_holes. End Checker_Lia5_holes. *) +Section Checker_Bv1. + Verit_Checker "bv1.smt2" "bv1.log". +End Checker_Bv1. + +Section Checker_Bv2. + Verit_Checker "bv2.smt2" "bv2.log". +End Checker_Bv2. + Section Sat0. Parse_certif_verit t_i0 t_func0 t_atom0 t_form0 root0 used_roots0 trace0 "sat0.smt2" "sat0.vtlog". @@ -301,10 +330,12 @@ Section Lia3. Compute @Euf_Checker.checker t_i_lia3 t_func_lia3 t_atom_lia3 t_form_lia3 root_lia3 used_roots_lia3 trace_lia3. End Lia3. +(* TODO: it does not go through anymore Section Lia4. Parse_certif_verit t_i_lia4 t_func_lia4 t_atom_lia4 t_form_lia4 root_lia4 used_roots_lia4 trace_lia4 "lia4.smt2" "lia4.vtlog". Compute @Euf_Checker.checker t_i_lia4 t_func_lia4 t_atom_lia4 t_form_lia4 root_lia4 used_roots_lia4 trace_lia4. End Lia4. +*) Section Lia5. Parse_certif_verit t_i_lia5 t_func_lia5 t_atom_lia5 t_form_lia5 root_lia5 used_roots_lia5 trace_lia5 "lia5.smt2" "lia5.vtlog". @@ -346,6 +377,16 @@ Section Lia5_holes. End Lia5_holes. *) +Section Bv1. + Parse_certif_verit t_i_bv1 t_func_bv1 t_atom_bv1 t_form_bv1 root_bv1 used_roots_bv1 trace_bv1 "bv1.smt2" "bv1.log". + Compute @Euf_Checker.checker t_i_bv1 t_func_bv1 t_atom_bv1 t_form_bv1 root_bv1 used_roots_bv1 trace_bv1. +End Bv1. + +Section Bv2. + Parse_certif_verit t_i_bv2 t_func_bv2 t_atom_bv2 t_form_bv2 root_bv2 used_roots_bv2 trace_bv2 "bv2.smt2" "bv2.log". + Compute @Euf_Checker.checker t_i_bv2 t_func_bv2 t_atom_bv2 t_form_bv2 root_bv2 used_roots_bv2 trace_bv2. +End Bv2. + Section Theorem_Sat0. Time Verit_Theorem theorem_sat0 "sat0.smt2" "sat0.vtlog". @@ -443,9 +484,11 @@ Section Theorem_Lia3. Time Verit_Theorem theorem_lia3 "lia3.smt2" "lia3.vtlog". End Theorem_Lia3. +(* TODO: it does not go through anymore Section Theorem_Lia4. Time Verit_Theorem theorem_lia4 "lia4.smt2" "lia4.vtlog". End Theorem_Lia4. +*) Section Theorem_Lia5. Time Verit_Theorem theorem_lia5 "lia5.smt2" "lia5.vtlog". @@ -482,6 +525,14 @@ End Theorem_Lia5_holes. Check theorem_lia5_holes. *) +Section Theorem_Bv1. + Time Verit_Theorem theorem_bv1 "bv1.smt2" "bv1.log". +End Theorem_Bv1. + +Section Theorem_Bv2. + Time Verit_Theorem theorem_bv2 "bv2.smt2" "bv2.log". +End Theorem_Bv2. + (* verit tactic *) @@ -939,18 +990,20 @@ Proof. verit. Qed. +(* TODO: fails with native-coq: "compilation error" Goal forall (i j:int), (i == j) && (negb (i == j)) = false. Proof. verit. - econstructor; eexact Int63Properties.reflect_eqb. + exact int63_compdec. Qed. Goal forall i j, (i == j) || (negb (i == j)). Proof. verit. - econstructor; eexact Int63Properties.reflect_eqb. + exact int63_compdec. Qed. +*) (* Congruence in which some premises are REFL *) @@ -968,103 +1021,100 @@ Proof. Qed. -(* - Local Variables: - coq-load-path: ((rec "../src" "SMTCoq")) - End: -*) - -(* Some examples of using verit with lemmas. Use <verit_base H1 .. Hn; vauto> +(* Some examples of using verit with lemmas. Use <verit_bool_base H1 .. Hn; vauto> to temporarily add the lemmas H1 .. Hn to the verit environment. *) Lemma taut1 : forall f, f 2 =? 0 -> f 2 =? 0. -Proof. intros f p. verit_base p; vauto. Qed. +Proof. intros f p. verit_bool_base p; vauto. Qed. Lemma taut2 : forall f, 0 =? f 2 -> 0 =?f 2. -Proof. intros f p. verit_base p; vauto. Qed. +Proof. intros f p. verit_bool_base p; vauto. Qed. Lemma taut3 : forall f, f 2 =? 0 -> f 3 =? 5 -> f 2 =? 0. -Proof. intros f p1 p2. verit_base p1 p2; vauto. Qed. +Proof. intros f p1 p2. verit_bool_base p1 p2; vauto. Qed. Lemma taut4 : forall f, f 3 =? 5 -> f 2 =? 0 -> f 2 =? 0. -Proof. intros f p1 p2. verit_base p1 p2; vauto. Qed. +Proof. intros f p1 p2. verit_bool_base p1 p2; vauto. Qed. + +(* Lemma test_eq_sym a b : implb (a =? b) (b =? a). *) +(* Proof. verit. *) -Lemma taut5 : - forall f, 0 =? f 2 -> f 2 =? 0. -Proof. intros f p. verit_base p; vauto. Qed. +(* Lemma taut5 : *) +(* forall f, 0 =? f 2 -> f 2 =? 0. *) +(* Proof. intros f p. verit_bool_base p; vauto. Qed. *) Lemma fun_const_Z : forall f , (forall x, f x =? 2) -> f 3 =? 2. -Proof. intros f Hf. verit_base Hf; vauto. Qed. +Proof. intros f Hf. verit_bool_base Hf; vauto. Qed. Lemma lid (A : bool) : A -> A. -Proof. intro a. verit_base a; vauto. Qed. +Proof. intro a. verit_bool_base a; vauto. Qed. Lemma lpartial_id A : (xorb A A) -> (xorb A A). -Proof. intro xa. verit_base xa; vauto. Qed. +Proof. intro xa. verit_bool_base xa; vauto. Qed. Lemma llia1 X Y Z: (X <=? 3) && ((Y <=? 7) || (Z <=? 9)) -> (X + Y <=? 10) || (X + Z <=? 12). -Proof. intro p. verit_base p; vauto. Qed. +Proof. intro p. verit_bool_base p; vauto. Qed. Lemma llia2 X: X - 3 =? 7 -> X >=? 10. -Proof. intro p. verit_base p; vauto. Qed. +Proof. intro p. verit_bool_base p; vauto. Qed. Lemma llia3 X Y: X >? Y -> Y + 1 <=? X. -Proof. intro p. verit_base p; vauto. Qed. +Proof. intro p. verit_bool_base p; vauto. Qed. Lemma llia6 X: andb ((X - 3) <=? 7) (7 <=? (X - 3)) -> X >=? 10. -Proof. intro p. verit_base p; vauto. Qed. +Proof. intro p. verit_bool_base p; vauto. Qed. Lemma even_odd b1 b2 x1 x2: (ifb b1 (ifb b2 (2*x1+1 =? 2*x2+1) (2*x1+1 =? 2*x2)) (ifb b2 (2*x1 =? 2*x2+1) (2*x1 =? 2*x2))) -> ((implb b1 b2) && (implb b2 b1) && (x1 =? x2)). -Proof. intro p. verit_base p; vauto. Qed. +Proof. intro p. verit_bool_base p; vauto. Qed. Lemma lcongr1 (a b : Z) (P : Z -> bool) f: (f a =? b) -> (P (f a)) -> P b. -Proof. intros eqfab pfa. verit_base eqfab pfa; vauto. Qed. +Proof. intros eqfab pfa. verit_bool_base eqfab pfa; vauto. Qed. Lemma lcongr2 (f:Z -> Z -> Z) x y z: x =? y -> f z x =? f z y. -Proof. intro p. verit_base p; vauto. Qed. +Proof. intro p. verit_bool_base p; vauto. Qed. Lemma lcongr3 (P:Z -> Z -> bool) x y z: x =? y -> P z x -> P z y. -Proof. intros eqxy pzx. verit_base eqxy pzx; vauto. Qed. +Proof. intros eqxy pzx. verit_bool_base eqxy pzx; vauto. Qed. Lemma test20 : forall x, (forall a, a <? x) -> 0 <=? x = false. -Proof. intros x H. verit_base H; vauto. Qed. +Proof. intros x H. verit_bool_base H; vauto. Qed. Lemma test21 : forall x, (forall a, negb (x <=? a)) -> negb (0 <=? x). -Proof. intros x H. verit_base H; vauto. Qed. +Proof. intros x H. verit_bool_base H; vauto. Qed. -Lemma un_menteur (a b c d : Z) dit: - dit a =? c -> - dit b =? d -> - (d =? a) || (b =? c) -> - (a =? c) || (a =? d) -> - (b =? c) || (b =? d) -> - a =? d. -Proof. intros H1 H2 H3 H4 H5. verit_base H1 H2 H3 H4 H5; vauto. Qed. +(* Lemma un_menteur (a b c d : Z) dit: *) +(* dit a =? c -> *) +(* dit b =? d -> *) +(* (d =? a) || (b =? c) -> *) +(* (a =? c) || (a =? d) -> *) +(* (b =? c) || (b =? d) -> *) +(* a =? d. *) +(* Proof. intros H1 H2 H3 H4 H5. verit_bool_base H1 H2 H3 H4 H5; vauto. Qed. *) Lemma const_fun_is_eq_val_0 : forall f : Z -> Z, (forall a b, f a =? f b) -> forall x, f x =? f 0. -Proof. intros f Hf. verit_base Hf; vauto. Qed. +Proof. intros f Hf. verit_bool_base Hf; vauto. Qed. (* You can use <Add_lemmas H1 .. Hn> to permanently add the lemmas H1 .. Hn to the environment. If you did so in a section then, at the end of the section, @@ -1143,7 +1193,7 @@ End mult3. (* Hypothesis mult_Sx : forall x y, mult (x+1) y =? mult x y + y. *) (* Lemma mult_1_x : forall x, mult 1 x =? x. *) -(* Proof. verit_base mult_0 mult_Sx. *) +(* Proof. verit_bool_base mult_0 mult_Sx. *) (* Qed. *) (* End mult. *) @@ -1163,8 +1213,7 @@ End implicit_transform. Section list. Variable Zlist : Type. - Hypothesis dec_Zlist : - {eq : Zlist -> Zlist -> bool & forall x y : Zlist, reflect (x = y) (eq x y)}. + Hypothesis dec_Zlist : CompDec Zlist. Variable nil : Zlist. Variable cons : Z -> Zlist -> Zlist. Variable inlist : Z -> Zlist -> bool. @@ -1276,15 +1325,15 @@ Section group. Lemma unique_identity e': (forall z, op e' z =? z) -> e' =? e. - Proof. intros pe'. verit_base pe'; vauto. Qed. + Proof. intros pe'. verit_bool_base pe'; vauto. Qed. Lemma simplification_right x1 x2 y: op x1 y =? op x2 y -> x1 =? x2. - Proof. intro H. verit_base H; vauto. Qed. + Proof. intro H. verit_bool_base H; vauto. Qed. Lemma simplification_left x1 x2 y: op y x1 =? op y x2 -> x1 =? x2. - Proof. intro H. verit_base H; vauto. Qed. + Proof. intro H. verit_bool_base H; vauto. Qed. Clear_lemmas. End group. diff --git a/unit-tests/Tests_zchaff.v b/unit-tests/Tests_zchaff.v index 28251f8..87d6db2 100644 --- a/unit-tests/Tests_zchaff.v +++ b/unit-tests/Tests_zchaff.v @@ -1,3 +1,15 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2019 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + Add Rec LoadPath "../src" as SMTCoq. Require Import SMTCoq. diff --git a/unit-tests/bv1.log b/unit-tests/bv1.log new file mode 100644 index 0000000..fc101e2 --- /dev/null +++ b/unit-tests/bv1.log @@ -0,0 +1,12 @@ +1:(input ((not #1:(= a a)))) +2:(bbvar (#2:(bbT a [#7:(bitof 0 a) #8:(bitof 1 a)]))) +3:(bbeq (#3:(= #1 #4:(and #5:(= #7 #7) #6:(= #8 #8)))) 2 2) +4:(equiv2 (#1 (not #4)) 3) +5:(resolution ((not #4)) 1 4) +6:(not_and ((not #5) (not #6)) 5) +7:(equiv_neg1 (#5 (not #7))) +8:(equiv_neg2 (#5 #7)) +9:(resolution ((not #6)) 7 8 6) +10:(equiv_neg1 (#6 (not #8))) +11:(equiv_neg2 (#6 #8)) +12:(resolution () 10 11 9) diff --git a/unit-tests/bv1.smt2 b/unit-tests/bv1.smt2 new file mode 100644 index 0000000..c23b151 --- /dev/null +++ b/unit-tests/bv1.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_BV) +(declare-fun a () (_ BitVec 2)) +(assert (not (= a a))) +(check-sat) +(exit) diff --git a/unit-tests/bv2.log b/unit-tests/bv2.log new file mode 100644 index 0000000..5bcd227 --- /dev/null +++ b/unit-tests/bv2.log @@ -0,0 +1,15 @@ +1:(input ((not #1:(= a a)))) +2:(bbvar (#2:(bbT a [#7:(bitof 0 a) #8:(bitof 1 a) #9:(bitof 2 a)]))) +3:(bbeq (#3:(= #1 #4:(and #5:(= #7 #7) #6:(= #8 #8) #10:(= #9 #9)))) 2 2) +4:(equiv2 (#1 (not #4)) 3) +5:(resolution ((not #4)) 1 4) +6:(not_and ((not #5) (not #6) (not #10)) 5) +7:(equiv_neg1 (#5 (not #7))) +8:(equiv_neg2 (#5 #7)) +9:(resolution ((not #6) (not #10)) 7 8 6) +10:(equiv_neg1 (#6 (not #8))) +11:(equiv_neg2 (#6 #8)) +12:(resolution ((not #10)) 10 11 9) +13:(equiv_neg1 (#10 (not #9))) +14:(equiv_neg2 (#10 #9)) +15:(resolution () 13 14 12) diff --git a/unit-tests/bv2.smt2 b/unit-tests/bv2.smt2 new file mode 100644 index 0000000..49156c7 --- /dev/null +++ b/unit-tests/bv2.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_BV) +(declare-fun a () (_ BitVec 3)) +(assert (not (= a a))) +(check-sat) +(exit) diff --git a/unit-tests/demo_lfsc_bool.v b/unit-tests/demo_lfsc_bool.v new file mode 100644 index 0000000..d89954f --- /dev/null +++ b/unit-tests/demo_lfsc_bool.v @@ -0,0 +1,199 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2019 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +Require Import SMTCoq. +Require Import Bool PArray Int63 List ZArith BVList Logic. +Import ListNotations. +Local Open Scope list_scope. +Local Open Scope int63_scope. +Local Open Scope Z_scope. +Local Open Scope bv_scope. + + +Infix "-->" := implb (at level 60, right associativity) : bool_scope. + + +Import BVList.BITVECTOR_LIST. +Require Import FArray. + +Section BV. + + Import BVList.BITVECTOR_LIST. + + Local Open Scope bv_scope. + + Goal forall (bv1 bv2 bv3 bv4: bitvector 4), + bv_eq #b|0|0|0|0| bv1 && + bv_eq #b|1|0|0|0| bv2 && + bv_eq #b|1|1|0|0| bv3 --> + bv_eq #b|1|1|1|0| bv4 --> + bv_ult bv1 bv2 || bv_ult bv3 bv1 --> bv_ult bv1 bv3 --> bv_ult bv1 bv4 || bv_ult bv4 bv1. + Proof. + smt. + Qed. + + Goal forall (a: bitvector 32), bv_eq a a. + Proof. + smt. + Qed. + + Goal forall (bv1 bv2: bitvector 4), + (Bool.eqb (bv_eq bv1 bv2) (bv_eq bv2 bv1)). + Proof. + smt. + Qed. + + Goal forall (bv1 bv2 bv3 bv4: bitvector 4), + bv_eq #b|0|0|0|0| bv1 && + bv_eq #b|1|0|0|0| bv2 && + bv_eq #b|1|1|0|0| bv3 --> + bv_eq #b|1|1|1|0| bv4 --> + bv_ult bv1 bv2 || bv_ult bv3 bv1 && bv_ult bv3 bv4. + Proof. + smt. + Qed. + + Goal forall (a b c: bitvector 4), + (bv_eq c (bv_and a b)) --> + (bv_eq (bv_and (bv_and c a) b) c). + Proof. + smt. + Qed. + +End BV. + +Section Arrays. + Import BVList.BITVECTOR_LIST. + Import FArray. + + Local Open Scope farray_scope. + Local Open Scope bv_scope. + + Goal forall (a:farray Z Z), equal a a. + Proof. + smt. + Qed. + + Goal forall (a b: farray Z Z), Bool.eqb (equal a b) (equal b a). + Proof. + smt. + Qed. + + Goal forall (a b: farray (bitvector 8) (bitvector 8)), Bool.eqb (equal a b) (equal b a). + Proof. + smt. + Qed. + + Goal forall (a b c d: farray Z Z), + equal b[0 <- 4] c --> + equal d b[0 <- 4][1 <- 4] && + equal a d[1 <- b[1]] --> + equal a c. + Proof. + smt. + Qed. + + Goal forall (bv1 bv2 : bitvector 4) + (a b c d : farray (bitvector 4) Z), + bv_eq #b|0|0|0|0| bv1 --> + bv_eq #b|1|0|0|0| bv2 --> + equal c b[bv1 <- 4] --> + equal d b[bv1 <- 4][bv2 <- 4] --> + equal a d[bv2 <- b[bv2]] --> + equal a c. + Proof. + smt. + Qed. + + Goal forall (a b: farray Z Z) + (v w x y: Z) + (g: farray Z Z -> Z) + (f: Z -> Z), + (equal a[x <- v] b) && (equal a[y <- w] b) --> (Z.eqb (f x) (f y)) || (Z.eqb (g a) (g b)). + Proof. + smt. + Qed. + +Goal forall (a b: farray Z Z) i, + Z.eqb (select (store (store (store a i 3%Z) 1%Z (select (store b i 4) i)) 2%Z 2%Z) 1%Z) 4. +Proof. + smt. + rewrite read_over_other_write; try easy. + rewrite read_over_same_write; try easy; try apply Z_compdec. + rewrite read_over_same_write; try easy; try apply Z_compdec. +Qed. + +End Arrays. + +Section UF. + + Goal forall + (x y: Z) + (f: Z -> Z), + Z.eqb y x --> Z.eqb (f x) (f y). + Proof. + smt. + Qed. + + Goal forall + (x y: Z) + (f: Z -> Z), + Z.eqb (f x) (f y) --> Z.eqb (f y) (f x). + Proof. + smt. + Qed. + + Goal forall + (x y: Z) + (f: Z -> Z), + Z.eqb (x + 1) (y + 1) --> Z.eqb (f y) (f x). + Proof. + smt. + Qed. + + Goal forall + (x y: Z) + (f: Z -> Z), + Z.eqb x (y + 1) --> Z.eqb (f y) (f (x - 1)). + Proof. + smt. + Qed. + + +Goal forall (f:Z -> Z -> Z) x y z, (Z.eqb x y) --> Z.eqb (f z x) (f z y). +Proof. + smt. +Qed. + +End UF. + + +Section LIA. + + Goal forall (a b: Z), Bool.eqb (Z.eqb a b) (Z.eqb b a). + Proof. + smt. + Qed. + + Goal forall (a b: Z), (Z.eqb a a) && (Z.eqb b b). + Proof. + smt. + Qed. + + +End LIA. + + + + + + diff --git a/unit-tests/demo_lfsc_prop.v b/unit-tests/demo_lfsc_prop.v new file mode 100644 index 0000000..00acfef --- /dev/null +++ b/unit-tests/demo_lfsc_prop.v @@ -0,0 +1,233 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2019 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +Require Import SMTCoq. +Require Import Bool PArray Int63 List ZArith BVList Logic. +Import ListNotations. +Local Open Scope list_scope. +Local Open Scope int63_scope. +Local Open Scope Z_scope. +Local Open Scope bv_scope. + +Import BVList.BITVECTOR_LIST. +Require Import FArray. + + +Section BV. + + Import BVList.BITVECTOR_LIST. + + Local Open Scope bv_scope. + + (* + (** cvc4 preprocesses the entire goal *) + Goal forall (a b c: bitvector 4), + bv_mult a (bv_add b c) = bv_add (bv_mult a b) (bv_mult a c). + *) + + + Goal forall (a b: bitvector 8), + #b|1|0|0|0|0|0|0|0| = a -> + #b|1|0|0|0|0|0|0|0| = b -> (bv_mult a b) = #b|0|0|0|0|0|0|0|0|. + Proof. + smt. + Qed. + +(* + +Goal forall (a b: bitvector 32), a = b. +Proof. smt. Fail Qed. + +*) + + + Goal forall (bv1 bv2 bv3 bv4: bitvector 4), + #b|0|0|0|0| = bv1 /\ + #b|1|0|0|0| = bv2 /\ + #b|1|1|0|0| = bv3 -> + #b|1|1|1|0| = bv4 -> + bv_ultP bv1 bv2 \/ bv_ultP bv3 bv1 -> bv_ultP bv1 bv3 -> bv_ultP bv1 bv4 \/ bv_ultP bv4 bv1. + Proof. + smt. + Qed. + + Goal forall (a: bitvector 32), a = a. + Proof. + smt. + Qed. + + Goal forall (bv1 bv2: bitvector 4), + bv1 = bv2 <-> bv2 = bv1. + Proof. + smt. + Qed. + + Goal forall (bv1 bv2 bv3 bv4: bitvector 4), + bv1 = #b|0|0|0|0| /\ + bv2 = #b|1|0|0|0| /\ + bv3 = #b|1|1|0|0| -> + bv4 = #b|1|1|1|0| -> + bv_ultP bv1 bv2 \/ bv_ultP bv3 bv1 /\ bv_ultP bv3 bv4. + Proof. + smt. + Qed. + + Goal forall (a b c: bitvector 4), + (c = (bv_and a b)) -> + ((bv_and (bv_and c a) b) = c). + Proof. + smt. + Qed. + + + +End BV. + +Section Arrays. + Import BVList.BITVECTOR_LIST. + Import FArray. + + Local Open Scope farray_scope. + Local Open Scope bv_scope. + + Goal forall (a:farray Z Z), a = a. + Proof. + smt. + Qed. + + Goal forall (a b: farray Z Z), a = b <-> b = a. + Proof. + smt. + Qed. + + Goal forall (a b: farray (bitvector 8) (bitvector 8)), a = b <-> b = a. + Proof. + smt. + Qed. + + Goal forall (a b c d: farray Z Z), + b[0 <- 4] = c -> + d = b[0 <- 4][1 <- 4] /\ + a = d[1 <- b[1]] -> + a = c. + Proof. + smt. + Qed. + + Goal forall (bv1 bv2 : bitvector 4) + (a b c d : farray (bitvector 4) Z), + bv1 = #b|0|0|0|0| -> + bv2 = #b|1|0|0|0| -> + c = b[bv1 <- 4] -> + d = b[bv1 <- 4][bv2 <- 4] -> + a = d[bv2 <- b[bv2]] -> + a = c. + Proof. + smt. + Qed. + + Goal forall (a b: farray Z Z) + (v w x y: Z) + (g: farray Z Z -> Z) + (f: Z -> Z), + (a[x <- v] = b) /\ a[y <- w] = b -> + (f x) = (f y) \/ (g a) = (g b). + Proof. + smt. + Qed. + + Goal forall (a b: farray Z Z) i, + a[i <- 3][1 <- b[i <- 4][i]][2 <- 2][1] = 4. + Proof. + smt. + rewrite read_over_other_write; [ | easy]. + rewrite read_over_write. + rewrite read_over_write; auto. +Qed. + +End Arrays. + +Section UF. + + Goal forall + (x y: Z) + (f: Z -> Z), + y = x -> (f x) = (f y). + Proof. + smt. + Qed. + + Goal forall + (x y: Z) + (f: Z -> Z), + (f x) = (f y) -> (f y) = (f x). + Proof. + smt. + Qed. + + Goal forall + (x y: Z) + (f: Z -> Z), + x + 1 = (y + 1) -> (f y) = (f x). + Proof. + smt. + Qed. + + Goal forall + (x y: Z) + (f: Z -> Z), + x = (y + 1) -> (f y) = (f (x - 1)). + Proof. + smt. + Qed. + + Goal forall (f:Z -> Z -> Z) x y z, (x = y) -> (f z x) = (f z y). + Proof. + smt. + Qed. + + Goal forall (t: Type) (p: CompDec t) (x y: t), (x = y) <-> (x = y). + Proof. + smt. + Qed. + +End UF. + + +Section LIA. + + Goal forall a b, a < b -> a < (b + 10). + Proof. + smt. + Qed. + + Goal forall (a b: Z), a = b <-> b = a. + Proof. + smt. + Qed. + + Goal forall (a b: Z), a = a /\ b = b. + Proof. + smt. + Qed. + + Goal forall (a b: Z), a < b -> a < (b + 1). + Proof. + smt. + Qed. + + Goal forall (a b: Z), (a < b) -> (a + 2 < b + 3). + Proof. + smt. + Qed. + +End LIA. diff --git a/unit-tests/ex1.lfsc b/unit-tests/ex1.lfsc new file mode 100644 index 0000000..d96c5be --- /dev/null +++ b/unit-tests/ex1.lfsc @@ -0,0 +1,23 @@ +unsat +(check + ;; Declarations +(% a (term Bool) +(% b (term Bool) +(% c (term Bool) +(% A1 (th_holds (not (impl (and (impl (p_app a) (p_app b)) (impl (p_app b) (p_app c))) (impl (p_app a) (p_app c))))) + ;; Proof of empty clause follows +(: (holds cln) + ;; Preprocessing + ;; Clauses +(decl_atom (p_app b) (\ var3 (\ atom3 +(decl_atom (p_app a) (\ var2 (\ atom2 +(satlem _ _ (asf _ _ _ atom3 (\ lit6 (ast _ _ _ atom2 (\ lit5 (clausify_false (contra _ (or_elim_1 _ _ (not_not_intro _ lit5) (impl_elim _ _ (and_elim_1 _ _ (and_elim_1 _ _ (not_impl_elim _ _ A1))))) lit6)))))) (\ pb2 +(decl_atom (p_app c) (\ var4 (\ atom4 +(satlem _ _ (asf _ _ _ atom4 (\ lit8 (ast _ _ _ atom3 (\ lit7 (clausify_false (contra _ (or_elim_1 _ _ (not_not_intro _ lit7) (impl_elim _ _ (and_elim_2 _ _ (and_elim_1 _ _ (not_impl_elim _ _ A1))))) lit8)))))) (\ pb3 +(satlem _ _ (asf _ _ _ atom2 (\ lit4 (clausify_false (contra _ (and_elim_1 _ _ (not_impl_elim _ _ (and_elim_2 _ _ (not_impl_elim _ _ A1)))) lit4)))) (\ pb4 +(satlem _ _ (ast _ _ _ atom4 (\ lit9 (clausify_false (contra _ lit9 (and_elim_2 _ _ (not_impl_elim _ _ (and_elim_2 _ _ (not_impl_elim _ _ A1)))))))) (\ pb5 + ;; Theory Lemmas +(satlem_simplify _ _ _ (Q _ _ pb2 pb4 var2) (\cl6 +(satlem_simplify _ _ _ (Q _ _ pb3 cl6 var3) (\cl7 +(satlem_simplify _ _ _ (Q _ _ pb5 cl7 var4) (\empty empty))))))))))))))))))))))))))))) +;; diff --git a/unit-tests/ex1.smt2 b/unit-tests/ex1.smt2 new file mode 100644 index 0000000..51685ed --- /dev/null +++ b/unit-tests/ex1.smt2 @@ -0,0 +1,11 @@ +(set-logic QF_SAT) +(declare-fun a () Bool) +(declare-fun b () Bool) +(declare-fun c () Bool) + +(assert (not (=> (and (=> a b) (=> b c)) (=> a c)))) + +(check-sat) + +(exit) + diff --git a/unit-tests/large1.v b/unit-tests/large1.v new file mode 100644 index 0000000..ee3ef55 --- /dev/null +++ b/unit-tests/large1.v @@ -0,0 +1,88 @@ +Require Import SMTCoq. + +(* For Notations *) +Import Bool PArray Int63 List ZArith FArray BVList.BITVECTOR_LIST. +Import ListNotations. +Open Scope list_scope. +Open Scope farray_scope. +Open Scope bv_scope. + +Infix "-->" := implb (at level 60, right associativity) : bool_scope. +Notation "¬ x" := (negb x) (at level 30, right associativity): bool_scope. + + + +Goal forall + (a1 : (farray Z Z)) + ( e1 : Z) + ( e10 : Z) + ( e2 : Z) + ( e3 : Z) + ( e4 : Z) + ( e5 : Z) + ( e6 : Z) + ( e7 : Z) + ( e8 : Z) + ( e9 : Z) + ( i1 : Z) + ( i10 : Z) + ( i2 : Z) + ( i3 : Z) + ( i4 : Z) + ( i5 : Z) + ( i6 : Z) + ( i7 : Z) + ( i8 : Z) + ( i9 : Z) + (sk : (farray Z Z) -> (farray Z Z) -> Z), + + negb (i9 =? i10) && + negb (i8 =? i10) && + negb (i8 =? i9) && + negb (i7 =? i10) && + negb (i7 =? i9) && + negb (i7 =? i8) && + negb (i6 =? i10) && + negb (i6 =? i9) && + negb (i6 =? i8) && + negb (i6 =? i7) && + negb (i5 =? i10) && + negb (i5 =? i9) && + negb (i5 =? i8) && + negb (i5 =? i7) && + negb (i5 =? i6) && + negb (i4 =? i10) && + negb (i4 =? i9) && + negb (i4 =? i8) && + negb (i4 =? i7) && + negb (i4 =? i6) && + negb (i4 =? i5) && + negb (i3 =? i10) && + negb (i3 =? i9) && + negb (i3 =? i8) && + negb (i3 =? i7) && + negb (i3 =? i6) && + negb (i3 =? i5) && + negb (i3 =? i4) && + negb (i2 =? i10) && + negb (i2 =? i9) && + negb (i2 =? i8) && + negb (i2 =? i7) && + negb (i2 =? i6) && + negb (i2 =? i5) && + negb (i2 =? i4) && + negb (i2 =? i3) && + negb (i1 =? i10) && + negb (i1 =? i9) && + negb (i1 =? i8) && + negb (i1 =? i7) && + negb (i1 =? i6) && + negb (i1 =? i5) && + negb (i1 =? i4) && + negb (i1 =? i3) && + negb (i1 =? i2) --> + + ((select (store (store (store (store (store (store (store (store (store (store a1 i1 e1) i2 e2) i3 e3) i4 e4) i5 e5) i6 e6) i7 e7) i8 e8) i9 e9) i10 e10) (sk (store (store (store (store (store (store (store (store (store (store a1 i1 e1) i2 e2) i3 e3) i4 e4) i5 e5) i6 e6) i7 e7) i8 e8) i9 e9) i10 e10) (store (store (store (store (store (store (store (store (store (store a1 i9 e9) i3 e3) i5 e5) i4 e4) i6 e6) i1 e1) i10 e10) i2 e2) i8 e8) i7 e7))) =? (select (store (store (store (store (store (store (store (store (store (store a1 i9 e9) i3 e3) i5 e5) i4 e4) i6 e6) i1 e1) i10 e10) i2 e2) i8 e8) i7 e7) (sk (store (store (store (store (store (store (store (store (store (store a1 i1 e1) i2 e2) i3 e3) i4 e4) i5 e5) i6 e6) i7 e7) i8 e8) i9 e9) i10 e10) (store (store (store (store (store (store (store (store (store (store a1 i9 e9) i3 e3) i5 e5) i4 e4) i6 e6) i1 e1) i10 e10) i2 e2) i8 e8) i7 e7)))). +Proof. + Time smt. +Qed. diff --git a/unit-tests/sat6.smt2 b/unit-tests/sat6.smt2 index acef584..3c73489 100644 --- a/unit-tests/sat6.smt2 +++ b/unit-tests/sat6.smt2 @@ -5,6 +5,6 @@ (declare-fun d () Bool) (assert (and a b)) (assert (or c d)) -(assert (not (or c (and a b d)))) +(assert (not (or c (and a (and b d))))) (check-sat) (exit) |