aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Makefile3
-rw-r--r--src/State.v2
-rw-r--r--src/Trace.v12
-rw-r--r--src/spl/Assumptions.v118
-rw-r--r--src/trace/coqTerms.ml2
-rw-r--r--src/trace/smtCertif.ml6
-rw-r--r--src/trace/smtCommands.ml28
-rw-r--r--src/trace/smtTrace.ml13
-rw-r--r--src/verit/veritLexer.mll3
-rw-r--r--src/verit/veritParser.mly3
-rw-r--r--src/verit/veritSyntax.ml4
-rw-r--r--src/verit/veritSyntax.mli2
-rw-r--r--src/versions/native/Make3
-rw-r--r--src/versions/native/Makefile3
-rw-r--r--src/versions/standard/Make1
-rw-r--r--src/versions/standard/Makefile63
-rw-r--r--unit-tests/Makefile2
-rw-r--r--unit-tests/Tests_verit.v37
18 files changed, 271 insertions, 34 deletions
diff --git a/src/Makefile b/src/Makefile
index 5ab7a2d..c7ac7c5 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -65,7 +65,7 @@ COQDOCLIBS?=-R . SMTCoq
CAMLYACC=$(CAMLBIN)ocamlyacc
CAMLLEX=$(CAMLBIN)ocamllex
-VCMXS=NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi
+VCMXS=NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi
CMXS=trace/smt_tactic.cmxs
CMXA=trace/smtcoq.cmxa
@@ -142,6 +142,7 @@ VFILES:=Trace.v\
spl/Operators.v\
spl/Arithmetic.v\
spl/Syntactic.v\
+ spl/Assumptions.v\
lia/Lia.v\
euf/Euf.v\
cnf/Cnf.v
diff --git a/src/State.v b/src/State.v
index fde25f9..6d31977 100644
--- a/src/State.v
+++ b/src/State.v
@@ -13,6 +13,7 @@
(* *)
(**************************************************************************)
+
Require Import List.
Require Import Bool.
Require Import Int63.
@@ -267,6 +268,7 @@ Module C.
| _ => false
end.
+
Section OR.
Variable or : t -> t -> t.
diff --git a/src/Trace.v b/src/Trace.v
index 3b6ac47..9566c47 100644
--- a/src/Trace.v
+++ b/src/Trace.v
@@ -15,7 +15,7 @@
Require Import Bool Int63 PArray.
-Require Import Misc State SMT_terms Cnf Euf Lia Syntactic Arithmetic Operators.
+Require Import Misc State SMT_terms Cnf Euf Lia Syntactic Arithmetic Operators Assumptions.
Local Open Scope array_scope.
Local Open Scope int63_scope.
@@ -335,8 +335,8 @@ Module Euf_Checker.
| SplDistinctElim (pos:int) (orig:clause_id) (res:_lit)
(* Offer the possibility to discharge parts of the proof to (manual) Coq proofs.
WARNING: this breaks extraction. *)
- | Hole (pos:int) (res:_lit)
- (p:Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) res)
+ | Hole (pos:int) (prem_id:list clause_id) (prem:list C.t) (concl:C.t)
+ (p:interp_conseq_uf (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) prem concl)
.
Local Open Scope list_scope.
@@ -362,7 +362,7 @@ Module Euf_Checker.
| LiaDiseq pos l => S.set_clause s pos (check_diseq t_form t_atom l)
| SplArith pos orig res l => S.set_clause s pos (check_spl_arith t_form t_atom (S.get s orig) res l)
| SplDistinctElim pos orig res => S.set_clause s pos (check_distinct_elim t_form t_atom (S.get s orig) res)
- | @Hole pos res _ => S.set_clause s pos (res::nil)
+ | @Hole pos prem_id prem concl _ => S.set_clause s pos (check_hole s prem_id prem concl)
end.
Lemma step_checker_correct :
@@ -372,7 +372,7 @@ Module Euf_Checker.
forall s, S.valid rho s ->
forall st : step, S.valid rho (step_checker s st).
Proof.
- intros rho H1 H2 H10 s Hs. destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [[Ht1 Ht2] Ht3]. destruct (Atom.check_atom_correct _ H2) as [Ha1 Ha2]. intros [pos res|pos cid lf|pos|pos|pos l|pos l|pos l i|pos cid|pos cid|pos cid i|pos l fl|pos l fl|pos l1 l2 fl|pos cl c|pos l|pos orig res l|pos orig res|pos res p]; simpl; try apply S.valid_set_clause; auto.
+ intros rho H1 H2 H10 s Hs. destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [[Ht1 Ht2] Ht3]. destruct (Atom.check_atom_correct _ H2) as [Ha1 Ha2]. intros [pos res|pos cid lf|pos|pos|pos l|pos l|pos l i|pos cid|pos cid|pos cid i|pos l fl|pos l fl|pos l1 l2 fl|pos cl c|pos l|pos orig res l|pos orig res|pos prem_id prem concl p]; simpl; try apply S.valid_set_clause; auto.
apply S.valid_set_resolve; auto.
apply valid_check_flatten; auto; intros h1 h2 H.
rewrite (Syntactic.check_hatom_correct_bool _ _ _ Ha1 Ha2 _ _ H); auto.
@@ -392,7 +392,7 @@ Module Euf_Checker.
apply valid_check_diseq; auto.
apply valid_check_spl_arith; auto.
apply valid_check_distinct_elim; auto.
- unfold C.valid; simpl; unfold rho; rewrite p; auto.
+ apply valid_check_hole; auto.
Qed.
Definition euf_checker (* t_atom t_form *) s t :=
diff --git a/src/spl/Assumptions.v b/src/spl/Assumptions.v
new file mode 100644
index 0000000..c04cb35
--- /dev/null
+++ b/src/spl/Assumptions.v
@@ -0,0 +1,118 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2016 *)
+(* *)
+(* Michaël Armand *)
+(* Benjamin Grégoire *)
+(* Chantal Keller *)
+(* *)
+(* Inria - École Polytechnique - Université Paris-Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
+Require Import State SMT_terms.
+Require Import List Bool PArray Int63.
+
+Local Open Scope list_scope.
+Local Open Scope bool_scope.
+Local Open Scope int63_scope.
+
+Set Implicit Arguments.
+
+
+(* User-friendly interpretation of clauses and of consequences *)
+Section Interp_UF.
+
+ Fixpoint interp_uf (rho:Valuation.t) (c:C.t) :=
+ match c with
+ | nil => false
+ | l::nil => Lit.interp rho l
+ | l::c => (Lit.interp rho l) || (interp_uf rho c)
+ end.
+
+ Lemma interp_equiv rho c : C.interp rho c = interp_uf rho c.
+ Proof.
+ induction c as [ |l c IHc]; simpl; auto.
+ rewrite IHc. destruct c as [ |l' c]; simpl; auto.
+ now rewrite orb_false_r.
+ Qed.
+
+ Fixpoint interp_conseq_uf (rho:Valuation.t) (prem:list C.t) (concl:C.t) :=
+ match prem with
+ | nil => is_true (interp_uf rho concl)
+ | c::prem => is_true (interp_uf rho c) -> interp_conseq_uf rho prem concl
+ end.
+
+End Interp_UF.
+
+
+(* Small checker for assumptions *)
+
+Section Checker.
+
+ Section Forallb2.
+
+ Variables A B : Type.
+ Variable P : A -> B -> bool.
+
+ Fixpoint forallb2 (xs: list A) (ys:list B) {struct xs} : bool :=
+ match xs, ys with
+ | nil, nil => true
+ | x::xs, y::ys => (P x y) && (forallb2 xs ys)
+ | _, _ => false
+ end.
+
+ End Forallb2.
+
+ Definition check_hole (s:S.t) (prem_id:list clause_id) (prem:list C.t) (concl:C.t) :=
+ if forallb2 (fun id c => forallb2 (fun i j => i == j) (S.get s id) (S.sort_uniq c)) prem_id prem
+ then concl
+ else C._true.
+
+End Checker.
+
+
+Section Checker_correct.
+
+ Variable t_i : array typ_eqb.
+ Variable t_func : array (Atom.tval t_i).
+ Variable t_atom : array Atom.atom.
+ Variable t_form : array Form.form.
+
+ Local Notation rho := (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form).
+
+ (* H1 : Form.check_form t_form *)
+ (* H2 : Atom.check_atom t_atom *)
+ (* H10 : Atom.wt t_i t_func t_atom *)
+
+ Variable s : S.t.
+ Hypothesis Hs : S.valid rho s.
+
+ (* Ht1 : default t_form = Form.Ftrue *)
+ (* Ht2 : Form.wf t_form *)
+ (* Ht3 : Valuation.wf *)
+ (* (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) *)
+ (* t_form) *)
+ (* Ha1 : Atom.wf t_atom *)
+ (* Ha2 : default t_atom = Atom.Acop Atom.CO_xH *)
+
+ Variable pos : int.
+ Variable prem_id : list int.
+ Variable prem : list C.t.
+ Variable concl : C.t.
+ Hypothesis p : interp_conseq_uf
+ (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom)
+ t_form) prem concl.
+
+ Lemma valid_check_hole: C.valid rho (check_hole s prem_id prem concl).
+ (* TODO *)
+ Admitted.
+
+End Checker_correct.
+
+
+Unset Implicit Arguments.
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index f2c24b8..a58fcfa 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -104,6 +104,8 @@ let smt_modules = [ ["SMTCoq";"Misc"];
["SMTCoq";"SMT_terms";"Atom"]
]
+let cState_C_t = gen_constant [["SMTCoq";"State";"C"]] "t"
+
let cdistinct = gen_constant smt_modules "distinct"
let ctype = gen_constant smt_modules "type"
diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml
index 8ed87e4..f39bff4 100644
--- a/src/trace/smtCertif.ml
+++ b/src/trace/smtCertif.ml
@@ -109,7 +109,7 @@ type 'hform rule =
| SplDistinctElim of 'hform clause * 'hform
(* Possibility to introduce "holes" in proofs (that should be filled in Coq) *)
- | Hole of 'hform
+ | Hole of ('hform clause) list * 'hform list
and 'hform clause = {
id : clause_id;
@@ -138,7 +138,7 @@ let used_clauses r =
match r with
| ImmBuildProj (c, _) | ImmBuildDef c | ImmBuildDef2 c
| ImmFlatten (c,_) | SplArith (c,_,_) | SplDistinctElim (c,_) -> [c]
+ | Hole (cs, _) -> cs
| True | False | BuildDef _ | BuildDef2 _ | BuildProj _
| EqTr _ | EqCgr _ | EqCgrP _
- | LiaMicromega _ | LiaDiseq _
- | Hole _ -> []
+ | LiaMicromega _ | LiaDiseq _ -> []
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index de6a8fb..ec89db1 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -65,6 +65,22 @@ let compute_roots roots last_root =
used_roots [] 0 roots !r
+let interp_uf ta tf c =
+ let rec interp = function
+ | [] -> Lazy.force cfalse
+ | [l] -> Form.interp_to_coq (Atom.interp_to_coq ta) tf l
+ | l::c -> mklApp corb [|Form.interp_to_coq (Atom.interp_to_coq ta) tf l; interp c|] in
+ interp c
+
+let interp_conseq_uf (prem, concl) =
+ let ta = Hashtbl.create 17 in
+ let tf = Hashtbl.create 17 in
+ let rec interp = function
+ | [] -> mklApp cis_true [|interp_uf ta tf concl|]
+ | c::prem -> Term.mkArrow (mklApp cis_true [|interp_uf ta tf c|]) (interp prem) in
+ interp prem
+
+
let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf, roots, max_id, confl) =
let t_i' = make_t_i rt in
@@ -72,7 +88,7 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf,
let t_atom' = Atom.interp_tbl ra in
let t_form' = snd (Form.interp_tbl rf) in
- let (tres, last_root, _) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) (Form.interp_to_coq (Atom.interp_to_coq (Hashtbl.create 17)) (Hashtbl.create 17)) (certif_ops (Some [|t_i'; t_func'; t_atom'; t_form'|])) confl false in
+ let (tres, last_root, _) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|t_i'; t_func'; t_atom'; t_form'|])) confl false in
let used_roots = compute_roots roots last_root in
let roots =
let res = Array.make (List.length roots + 1) (mkInt 0) in
@@ -118,7 +134,7 @@ let build_certif (rt, ro, ra, rf, roots, max_id, confl) =
let t_i = make_t_i rt in
let t_func = make_t_func ro t_i in
- let (tres,last_root,_) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) (Form.interp_to_coq (Atom.interp_to_coq (Hashtbl.create 17)) (Hashtbl.create 17)) (certif_ops (Some [|t_i; t_func; t_atom; t_form|])) confl false in
+ let (tres,last_root,_) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|t_i; t_func; t_atom; t_form|])) confl false in
let used_roots = compute_roots roots last_root in
let used_rootsCstr =
let l = List.length used_roots in
@@ -183,10 +199,10 @@ let build_body rt ro ra rf l b (max_id, confl) =
let v = Term.mkRel in
let t_i = make_t_i rt in
- let t_func = Term.lift 1 (make_t_func ro (v 0 (*t_i - 1*))) in
+ let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i - 1*))) in
let t_atom = Atom.interp_tbl ra in
let t_form = snd (Form.interp_tbl rf) in
- let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq (Form.interp_to_coq (Atom.interp_to_coq (Hashtbl.create 17)) (Hashtbl.create 17)) (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl true in
+ let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq interp_conseq_uf (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl true in
let certif =
mklApp cCertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*); mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
@@ -214,10 +230,10 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) =
let v = Term.mkRel in
let t_i = make_t_i rt in
- let t_func = Term.lift 1 (make_t_func ro (v 0 (*t_i*))) in
+ let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i*))) in
let t_atom = Atom.interp_tbl ra in
let t_form = snd (Form.interp_tbl rf) in
- let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq (Form.interp_to_coq (Atom.interp_to_coq (Hashtbl.create 17)) (Hashtbl.create 17)) (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl true in
+ let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq interp_conseq_uf (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl true in
let certif =
mklApp cCertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*); mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index 83b8779..b6f4295 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -334,11 +334,12 @@ let to_coq to_lit interp (cstep,
let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Coq_micromega.M.coq_proofTerm; Coq_micromega.dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Coq_micromega.M.coq_proofTerm|]) in
mklApp cSplArith [|out_c c; out_c orig; res'; l'|]
| SplDistinctElim (c',f) -> mklApp cSplDistinctElim [|out_c c;out_c c'; out_f f|]
- | Hole res ->
+ | Hole (prem_id, concl) ->
+ let prem = List.map (fun cl -> match cl.value with Some l -> l | None -> assert false) prem_id in
let ass_name = Names.id_of_string ("ass"^(string_of_int (
- if isCut then List.length !cuts else Hashtbl.hash res
+ if isCut then List.length !cuts else Hashtbl.hash concl
))) in
- let ass_ty = interp res in
+ let ass_ty = interp (prem, concl) in
let ass_var =
if isCut then (
let ass_var = Term.mkVar ass_name in
@@ -347,7 +348,11 @@ let to_coq to_lit interp (cstep,
) else (
declare_new_variable ass_name ass_ty
) in
- mklApp cHole [|out_c c; out_f res; ass_var|]
+ let out_cl cl = List.fold_right (fun f l -> mklApp ccons [|Lazy.force cint; out_f f; l|]) cl (mklApp cnil [|Lazy.force cint|]) in
+ let prem_id' = List.fold_right (fun c l -> mklApp ccons [|Lazy.force cint; out_c c; l|]) prem_id (mklApp cnil [|Lazy.force cint|]) in
+ let prem' = List.fold_right (fun cl l -> mklApp ccons [|Lazy.force cState_C_t; out_cl cl; l|]) prem (mklApp cnil [|Lazy.force cState_C_t|]) in
+ let concl' = out_cl concl in
+ mklApp cHole [|out_c c; prem_id'; prem'; concl'; ass_var|]
end
| _ -> assert false in
let step = Lazy.force cstep in
diff --git a/src/verit/veritLexer.mll b/src/verit/veritLexer.mll
index 925ba92..2a51a02 100644
--- a/src/verit/veritLexer.mll
+++ b/src/verit/veritLexer.mll
@@ -95,7 +95,8 @@
"tmp_qnt_tidy", TPQT;
"tmp_qnt_simplify", TPQS;
"tmp_skolemize", TPSK;
- "subproof", SUBP ]
+ "subproof", SUBP;
+ "hole", HOLE ]
}
diff --git a/src/verit/veritParser.mly b/src/verit/veritParser.mly
index 6bb9639..7bb4c8e 100644
--- a/src/verit/veritParser.mly
+++ b/src/verit/veritParser.mly
@@ -29,7 +29,7 @@
%token COLON SHARP
%token LPAR RPAR
%token NOT XOR ITE EQ LT LEQ GT GEQ PLUS MINUS MULT OPP LET DIST
-%token INPU DEEP TRUE FALS ANDP ANDN ORP ORN XORP1 XORP2 XORN1 XORN2 IMPP IMPN1 IMPN2 EQUP1 EQUP2 EQUN1 EQUN2 ITEP1 ITEP2 ITEN1 ITEN2 EQRE EQTR EQCO EQCP DLGE LAGE LATA DLDE LADE FINS EINS SKEA SKAA QNTS QNTM RESO AND NOR OR NAND XOR1 XOR2 NXOR1 NXOR2 IMP NIMP1 NIMP2 EQU1 EQU2 NEQU1 NEQU2 ITE1 ITE2 NITE1 NITE2 TPAL TLAP TPLE TPNE TPDE TPSA TPIE TPMA TPBR TPBE TPSC TPPP TPQT TPQS TPSK SUBP
+%token INPU DEEP TRUE FALS ANDP ANDN ORP ORN XORP1 XORP2 XORN1 XORN2 IMPP IMPN1 IMPN2 EQUP1 EQUP2 EQUN1 EQUN2 ITEP1 ITEP2 ITEN1 ITEN2 EQRE EQTR EQCO EQCP DLGE LAGE LATA DLDE LADE FINS EINS SKEA SKAA QNTS QNTM RESO AND NOR OR NAND XOR1 XOR2 NXOR1 NXOR2 IMP NIMP1 NIMP2 EQU1 EQU2 NEQU1 NEQU2 ITE1 ITE2 NITE1 NITE2 TPAL TLAP TPLE TPNE TPDE TPSA TPIE TPMA TPBR TPBE TPSC TPPP TPQT TPQS TPSK SUBP HOLE
%token <int> INT
%token <Big_int.big_int> BIGINT
%token <string> VAR BINDVAR
@@ -122,6 +122,7 @@ typ:
| TPQS { Tpqs }
| TPSK { Tpsk }
| SUBP { Subp }
+ | HOLE { Hole }
;
clause:
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index 97fbac6..2f4a5af 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -24,7 +24,7 @@ open SmtTrace
exception Sat
-type typ = | Inpu | Deep | True | Fals | Andp | Andn | Orp | Orn | Xorp1 | Xorp2 | Xorn1 | Xorn2 | Impp | Impn1 | Impn2 | Equp1 | Equp2 | Equn1 | Equn2 | Itep1 | Itep2 | Iten1 | Iten2 | Eqre | Eqtr | Eqco | Eqcp | Dlge | Lage | Lata | Dlde | Lade | Fins | Eins | Skea | Skaa | Qnts | Qntm | Reso | And | Nor | Or | Nand | Xor1 | Xor2 | Nxor1 | Nxor2 | Imp | Nimp1 | Nimp2 | Equ1 | Equ2 | Nequ1 | Nequ2 | Ite1 | Ite2 | Nite1 | Nite2 | Tpal | Tlap | Tple | Tpne | Tpde | Tpsa | Tpie | Tpma | Tpbr | Tpbe | Tpsc | Tppp | Tpqt | Tpqs | Tpsk | Subp
+type typ = | Inpu | Deep | True | Fals | Andp | Andn | Orp | Orn | Xorp1 | Xorp2 | Xorn1 | Xorn2 | Impp | Impn1 | Impn2 | Equp1 | Equp2 | Equn1 | Equn2 | Itep1 | Itep2 | Iten1 | Iten2 | Eqre | Eqtr | Eqco | Eqcp | Dlge | Lage | Lata | Dlde | Lade | Fins | Eins | Skea | Skaa | Qnts | Qntm | Reso | And | Nor | Or | Nand | Xor1 | Xor2 | Nxor1 | Nxor2 | Imp | Nimp1 | Nimp2 | Equ1 | Equ2 | Nequ1 | Nequ2 | Ite1 | Ite2 | Nite1 | Nite2 | Tpal | Tlap | Tple | Tpne | Tpde | Tpsa | Tpie | Tpma | Tpbr | Tpbe | Tpsc | Tppp | Tpqt | Tpqs | Tpsk | Subp | Hole
(* About equality *)
@@ -278,6 +278,8 @@ let mk_clause (id,typ,value,ids_params) =
(match ids_params with
| id::_ -> mkSplArith (get_clause id) value
| _ -> assert false)
+ (* Holes in proofs *)
+ | Hole -> Other (SmtCertif.Hole (List.map get_clause ids_params, value))
(* Not implemented *)
| Deep -> failwith "VeritSyntax.ml: rule deep_res not implemented yet"
| Fins -> failwith "VeritSyntax.ml: rule forall_inst not implemented yet"
diff --git a/src/verit/veritSyntax.mli b/src/verit/veritSyntax.mli
index cec2d97..281deef 100644
--- a/src/verit/veritSyntax.mli
+++ b/src/verit/veritSyntax.mli
@@ -16,7 +16,7 @@
exception Sat
-type typ = | Inpu | Deep | True | Fals | Andp | Andn | Orp | Orn | Xorp1 | Xorp2 | Xorn1 | Xorn2 | Impp | Impn1 | Impn2 | Equp1 | Equp2 | Equn1 | Equn2 | Itep1 | Itep2 | Iten1 | Iten2 | Eqre | Eqtr | Eqco | Eqcp | Dlge | Lage | Lata | Dlde | Lade | Fins | Eins | Skea | Skaa | Qnts | Qntm | Reso | And | Nor | Or | Nand | Xor1 | Xor2 | Nxor1 | Nxor2 | Imp | Nimp1 | Nimp2 | Equ1 | Equ2 | Nequ1 | Nequ2 | Ite1 | Ite2 | Nite1 | Nite2 | Tpal | Tlap | Tple | Tpne | Tpde | Tpsa | Tpie | Tpma | Tpbr | Tpbe | Tpsc | Tppp | Tpqt | Tpqs | Tpsk | Subp
+type typ = | Inpu | Deep | True | Fals | Andp | Andn | Orp | Orn | Xorp1 | Xorp2 | Xorn1 | Xorn2 | Impp | Impn1 | Impn2 | Equp1 | Equp2 | Equn1 | Equn2 | Itep1 | Itep2 | Iten1 | Iten2 | Eqre | Eqtr | Eqco | Eqcp | Dlge | Lage | Lata | Dlde | Lade | Fins | Eins | Skea | Skaa | Qnts | Qntm | Reso | And | Nor | Or | Nand | Xor1 | Xor2 | Nxor1 | Nxor2 | Imp | Nimp1 | Nimp2 | Equ1 | Equ2 | Nequ1 | Nequ2 | Ite1 | Ite2 | Nite1 | Nite2 | Tpal | Tlap | Tple | Tpne | Tpde | Tpsa | Tpie | Tpma | Tpbr | Tpbe | Tpsc | Tppp | Tpqt | Tpqs | Tpsk | Subp | Hole
val get_clause : int -> SmtAtom.Form.t SmtCertif.clause
val add_clause : int -> SmtAtom.Form.t SmtCertif.clause -> unit
diff --git a/src/versions/native/Make b/src/versions/native/Make
index 75758b2..5659cc7 100644
--- a/src/versions/native/Make
+++ b/src/versions/native/Make
@@ -42,7 +42,7 @@
CMXA = trace/smtcoq.cmxa
CMXS = trace/smt_tactic.cmxs
-VCMXS = "NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi"
+VCMXS = "NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi"
CAMLLEX = $(CAMLBIN)ocamllex
CAMLYACC = $(CAMLBIN)ocamlyacc
@@ -85,6 +85,7 @@ euf/Euf.v
lia/lia.ml
lia/Lia.v
+spl/Assumptions.v
spl/Syntactic.v
spl/Arithmetic.v
spl/Operators.v
diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile
index 5ab7a2d..c7ac7c5 100644
--- a/src/versions/native/Makefile
+++ b/src/versions/native/Makefile
@@ -65,7 +65,7 @@ COQDOCLIBS?=-R . SMTCoq
CAMLYACC=$(CAMLBIN)ocamlyacc
CAMLLEX=$(CAMLBIN)ocamllex
-VCMXS=NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi
+VCMXS=NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_SMTCoq.cmi
CMXS=trace/smt_tactic.cmxs
CMXA=trace/smtcoq.cmxa
@@ -142,6 +142,7 @@ VFILES:=Trace.v\
spl/Operators.v\
spl/Arithmetic.v\
spl/Syntactic.v\
+ spl/Assumptions.v\
lia/Lia.v\
euf/Euf.v\
cnf/Cnf.v
diff --git a/src/versions/standard/Make b/src/versions/standard/Make
index 4d548ad..42d0552 100644
--- a/src/versions/standard/Make
+++ b/src/versions/standard/Make
@@ -99,6 +99,7 @@ euf/Euf.v
lia/lia.ml
lia/Lia.v
+spl/Assumptions.v
spl/Syntactic.v
spl/Arithmetic.v
spl/Operators.v
diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile
index 33ce492..cb92e59 100644
--- a/src/versions/standard/Makefile
+++ b/src/versions/standard/Makefile
@@ -2,7 +2,7 @@
## v # The Coq Proof Assistant ##
## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
## \VV/ # ##
-## // # Makefile automagically generated by coq_makefile V8.5 ##
+## // # Makefile automagically generated by coq_makefile V8.5pl1 ##
#############################################################################
# WARNING
@@ -96,12 +96,22 @@ COQDOC?="$(COQBIN)coqdoc"
COQCHK?="$(COQBIN)coqchk"
COQMKTOP?="$(COQBIN)coqmktop"
-COQSRCLIBS?=-I "$(COQLIB)kernel" -I "$(COQLIB)lib" \
- -I "$(COQLIB)library" -I "$(COQLIB)parsing" -I "$(COQLIB)pretyping" \
- -I "$(COQLIB)interp" -I "$(COQLIB)printing" -I "$(COQLIB)intf" \
- -I "$(COQLIB)proofs" -I "$(COQLIB)tactics" -I "$(COQLIB)tools" \
- -I "$(COQLIB)toplevel" -I "$(COQLIB)stm" -I "$(COQLIB)grammar" \
- -I "$(COQLIB)config" \
+COQSRCLIBS?=-I "$(COQLIB)kernel" \
+-I "$(COQLIB)lib" \
+-I "$(COQLIB)library" \
+-I "$(COQLIB)parsing" \
+-I "$(COQLIB)pretyping" \
+-I "$(COQLIB)interp" \
+-I "$(COQLIB)printing" \
+-I "$(COQLIB)intf" \
+-I "$(COQLIB)proofs" \
+-I "$(COQLIB)tactics" \
+-I "$(COQLIB)tools" \
+-I "$(COQLIB)toplevel" \
+-I "$(COQLIB)stm" \
+-I "$(COQLIB)grammar" \
+-I "$(COQLIB)config" \
+ \
-I "$(COQLIB)/plugins/btauto" \
-I "$(COQLIB)/plugins/cc" \
-I "$(COQLIB)/plugins/decl_mode" \
@@ -168,6 +178,7 @@ VFILES:=versions/standard/Int63/Int63.v\
cnf/Cnf.v\
euf/Euf.v\
lia/Lia.v\
+ spl/Assumptions.v\
spl/Syntactic.v\
spl/Arithmetic.v\
spl/Operators.v\
@@ -413,6 +424,44 @@ uninstall_me.sh: Makefile
uninstall: uninstall_me.sh
sh $<
+.merlin:
+ @echo 'FLG -rectypes' > .merlin
+ @echo "B $(COQLIB) kernel" >> .merlin
+ @echo "B $(COQLIB) lib" >> .merlin
+ @echo "B $(COQLIB) library" >> .merlin
+ @echo "B $(COQLIB) parsing" >> .merlin
+ @echo "B $(COQLIB) pretyping" >> .merlin
+ @echo "B $(COQLIB) interp" >> .merlin
+ @echo "B $(COQLIB) printing" >> .merlin
+ @echo "B $(COQLIB) intf" >> .merlin
+ @echo "B $(COQLIB) proofs" >> .merlin
+ @echo "B $(COQLIB) tactics" >> .merlin
+ @echo "B $(COQLIB) tools" >> .merlin
+ @echo "B $(COQLIB) toplevel" >> .merlin
+ @echo "B $(COQLIB) stm" >> .merlin
+ @echo "B $(COQLIB) grammar" >> .merlin
+ @echo "B $(COQLIB) config" >> .merlin
+ @echo "B cnf" >> .merlin
+ @echo "S cnf" >> .merlin
+ @echo "B euf" >> .merlin
+ @echo "S euf" >> .merlin
+ @echo "B lia" >> .merlin
+ @echo "S lia" >> .merlin
+ @echo "B smtlib2" >> .merlin
+ @echo "S smtlib2" >> .merlin
+ @echo "B trace" >> .merlin
+ @echo "S trace" >> .merlin
+ @echo "B verit" >> .merlin
+ @echo "S verit" >> .merlin
+ @echo "B zchaff" >> .merlin
+ @echo "S zchaff" >> .merlin
+ @echo "B versions/standard" >> .merlin
+ @echo "S versions/standard" >> .merlin
+ @echo "B versions/standard/Int63" >> .merlin
+ @echo "S versions/standard/Int63" >> .merlin
+ @echo "B versions/standard/Array" >> .merlin
+ @echo "S versions/standard/Array" >> .merlin
+
clean::
rm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)
rm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)
diff --git a/unit-tests/Makefile b/unit-tests/Makefile
index 915ee7a..bed1018 100644
--- a/unit-tests/Makefile
+++ b/unit-tests/Makefile
@@ -29,4 +29,4 @@ logs: $(OBJ)
clean:
- rm -rf *~ *.zlog *.vtlog
+ rm -rf *~ $(ZCHAFFLOG) $(VERITLOG)
diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v
index b5edddd..e99e484 100644
--- a/unit-tests/Tests_verit.v
+++ b/unit-tests/Tests_verit.v
@@ -132,6 +132,17 @@ Section Checker_Let2.
End Checker_Let2.
*)
+(* Proofs with holes *)
+(*
+Section Checker_Sat7_holes.
+ Verit_Checker "sat7.smt2" "sat7-with-holes.vtlog".
+End Checker_Sat7_holes.
+
+Section Checker_Lia5_holes.
+ Verit_Checker "lia5.smt2" "lia5-with-holes.vtlog".
+End Checker_Lia5_holes.
+*)
+
Section Sat0.
Parse_certif_verit t_i0 t_func0 t_atom0 t_form0 root0 used_roots0 trace0 "sat0.smt2" "sat0.vtlog".
@@ -285,6 +296,19 @@ Section Let2.
End Let2.
*)
+(* Proofs with holes *)
+(*
+Section Sat7_holes.
+ Parse_certif_verit t_i_sat7_holes t_func_sat7_holes t_atom_sat7_holes t_form_sat7_holes root_sat7_holes used_roots_sat7_holes trace_sat7_holes "sat7.smt2" "sat7-with-holes.vtlog".
+ Compute @Euf_Checker.checker t_i_sat7_holes t_func_sat7_holes t_atom_sat7_holes t_form_sat7_holes root_sat7_holes used_roots_sat7_holes trace_sat7_holes.
+End Sat7_holes.
+
+Section Lia5_holes.
+ Parse_certif_verit t_i_lia5_holes t_func_lia5_holes t_atom_lia5_holes t_form_lia5_holes root_lia5_holes used_roots_lia5_holes trace_lia5_holes "lia5.smt2" "lia5-with-holes.vtlog".
+ Compute @Euf_Checker.checker t_i_lia5_holes t_func_lia5_holes t_atom_lia5_holes t_form_lia5_holes root_lia5_holes used_roots_lia5_holes trace_lia5_holes.
+End Lia5_holes.
+*)
+
Section Theorem_Sat0.
Time Verit_Theorem theorem_sat0 "sat0.smt2" "sat0.vtlog".
@@ -408,6 +432,19 @@ Section Theorem_Let2.
End Theorem_Let2.
*)
+(* Proofs with holes *)
+(*
+Section Theorem_Sat7_holes.
+ Time Verit_Theorem theorem_sat7_holes "sat7.smt2" "sat7-with-holes.vtlog".
+End Theorem_Sat7_holes.
+Check theorem_sat7_holes.
+
+Section Theorem_Lia5_holes.
+ Time Verit_Theorem theorem_lia5_holes "lia5.smt2" "lia5-with-holes.vtlog".
+End Theorem_Lia5_holes.
+Check theorem_lia5_holes.
+*)
+
(* verit tactic *)
generated by cgit (git 2.34.1) at 2024-06-29 04:16:05 +0000