diff options
| -rw-r--r-- | examples/Example.v | 4 | ||||
| -rw-r--r-- | src/SMT_terms.v | 1 | ||||
| -rw-r--r-- | src/Trace.v | 50 | ||||
| -rw-r--r-- | src/smtlib2/smtlib2_genConstr.ml | 6 | ||||
| -rw-r--r-- | src/trace/smtAtom.ml | 356 | ||||
| -rw-r--r-- | src/trace/smtAtom.mli | 5 | ||||
| -rw-r--r-- | src/trace/smtCertif.ml | 28 | ||||
| -rw-r--r-- | src/trace/smtCertif.mli | 15 | ||||
| -rw-r--r-- | src/trace/smtCommands.ml | 12 | ||||
| -rw-r--r-- | src/trace/smtForm.ml | 490 | ||||
| -rw-r--r-- | src/trace/smtForm.mli | 3 | ||||
| -rw-r--r-- | src/trace/smtTrace.ml | 97 | ||||
| -rw-r--r-- | src/verit/verit.ml | 17 | ||||
| -rw-r--r-- | src/verit/verit.mli | 3 | ||||
| -rw-r--r-- | src/verit/veritSyntax.ml | 366 | ||||
| -rw-r--r-- | src/versions/native/structures.ml | 2 | ||||
| -rw-r--r-- | src/zchaff/zchaff.ml | 112 | ||||
| -rw-r--r-- | unit-tests/Tests_verit.v | 35 |
18 files changed, 793 insertions, 809 deletions
diff --git a/examples/Example.v b/examples/Example.v index fe00931..0c50909 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -58,7 +58,6 @@ Proof. verit. Qed. - Goal forall b1 b2 x1 x2, implb (ifb b1 @@ -69,7 +68,6 @@ Proof. verit. Qed. - (* Examples of using the conversion tactics *) Local Open Scope positive_scope. @@ -137,4 +135,4 @@ nat_convert. verit. Qed. -Local Close Scope nat_scope.
\ No newline at end of file +Local Close Scope nat_scope. diff --git a/src/SMT_terms.v b/src/SMT_terms.v index 42b1314..65c0d8f 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -1292,7 +1292,6 @@ Module Atom. let get_type := get_type' t_interp in PArray.forallbi (fun i h => check_aux get_type h (get_type i)) t_atom. - Definition interp_hatom (t_atom : PArray.array atom) := let t_a := t_interp t_atom in PArray.get t_a. diff --git a/src/Trace.v b/src/Trace.v index 0446dae..5b1be7a 100644 --- a/src/Trace.v +++ b/src/Trace.v @@ -88,7 +88,7 @@ Section trace. (* intros a i _ Ha;apply PArray.fold_left_ind;trivial. *) (* intros a0 i0 _ H1;auto. *) Qed. - + End trace. @@ -100,22 +100,22 @@ Module Sat_Checker. | Res (_:int) (_:resolution). Definition resolution_checker s t := - _checker_ (fun s (st:step) => let (pos, r) := st in S.set_resolve s pos r) s t. + _checker_ (fun s (st:step) => let (pos, r) := st in S.set_resolve s pos r) s t. Lemma resolution_checker_correct : forall rho, Valuation.wf rho -> forall s t cid, resolution_checker C.is_false s t cid-> ~S.valid rho s. Proof. - intros rho Hwr;apply _checker__correct. + intros rho Hwr; apply _checker__correct. intros; apply C.is_false_correct; trivial. - intros s Hv (pos, r);apply S.valid_set_resolve;trivial. + intros s Hv (pos, r); apply S.valid_set_resolve; trivial. Qed. - + (** Application to Zchaff *) Definition dimacs := PArray.array (PArray.array _lit). - Definition C_interp_or rho c := + Definition C_interp_or rho c := afold_left _ _ false orb (Lit.interp rho) c. Lemma C_interp_or_spec : forall rho c, @@ -145,7 +145,7 @@ Qed. Inductive certif := | Certif : int -> _trace_ step -> clause_id -> certif. - Definition add_roots s (d:dimacs) := + Definition add_roots s (d:dimacs) := PArray.foldi_right (fun i c s => S.set_clause s i (PArray.to_list c)) d s. Definition checker (d:dimacs) (c:certif) := @@ -161,7 +161,7 @@ Qed. Lemma checker_correct : forall d c, checker d c = true -> - forall rho, Valuation.wf rho -> ~valid rho d. + forall rho, Valuation.wf rho -> ~ valid rho d. Proof. unfold checker; intros d (nclauses, t, confl_id) Hc rho Hwf Hv. apply (resolution_checker_correct Hwf Hc). @@ -169,31 +169,31 @@ Qed. apply S.valid_make; auto. Qed. - Definition interp_var rho x := + Definition interp_var rho x := match compare x 1 with | Lt => true | Eq => false - | Gt => rho (x - 1) + | Gt => rho (x - 1) (* This allows to have variable starting at 1 in the interpretation as in dimacs files *) end. - Lemma theorem_checker : + Lemma theorem_checker : forall d c, checker d c = true -> - forall rho, ~valid (interp_var rho) d. + forall rho, ~ valid (interp_var rho) d. Proof. - intros d c H rho;apply checker_correct with c;trivial. + intros d c H rho; apply checker_correct with c;trivial. split;compute;trivial;discriminate. Qed. End Sat_Checker. Module Cnf_Checker. - + Inductive step := | Res (pos:int) (res:resolution) - | ImmFlatten (pos:int) (cid:clause_id) (lf:_lit) - | CTrue (pos:int) + | ImmFlatten (pos:int) (cid:clause_id) (lf:_lit) + | CTrue (pos:int) | CFalse (pos:int) | BuildDef (pos:int) (l:_lit) | BuildDef2 (pos:int) (l:_lit) @@ -209,15 +209,15 @@ Module Cnf_Checker. Definition step_checker t_form s (st:step) := match st with | Res pos res => S.set_resolve s pos res - | ImmFlatten pos cid lf => S.set_clause s pos (check_flatten t_form s cid lf) + | ImmFlatten pos cid lf => S.set_clause s pos (check_flatten t_form s cid lf) | CTrue pos => S.set_clause s pos Cnf.check_True | CFalse pos => S.set_clause s pos Cnf.check_False | BuildDef pos l => S.set_clause s pos (check_BuildDef t_form l) | BuildDef2 pos l => S.set_clause s pos (check_BuildDef2 t_form l) | BuildProj pos l i => S.set_clause s pos (check_BuildProj t_form l i) - | ImmBuildDef pos cid => S.set_clause s pos (check_ImmBuildDef t_form s cid) + | ImmBuildDef pos cid => S.set_clause s pos (check_ImmBuildDef t_form s cid) | ImmBuildDef2 pos cid => S.set_clause s pos (check_ImmBuildDef2 t_form s cid) - | ImmBuildProj pos cid i => S.set_clause s pos (check_ImmBuildProj t_form s cid i) + | ImmBuildProj pos cid i => S.set_clause s pos (check_ImmBuildProj t_form s cid i) end. Lemma step_checker_correct : forall rho t_form, @@ -257,9 +257,9 @@ Module Cnf_Checker. | Certif : int -> _trace_ step -> int -> certif. Definition checker t_form l (c:certif) := - let (nclauses, t, confl) := c in + let (nclauses, t, confl) := c in Form.check_form t_form && - cnf_checker t_form C.is_false (S.set_clause (S.make nclauses) 0 (l::nil)) t confl. + cnf_checker t_form C.is_false (S.set_clause (S.make nclauses) 0 (l::nil)) t confl. Lemma checker_correct : forall t_form l c, checker t_form l c = true -> @@ -282,11 +282,11 @@ Module Cnf_Checker. Qed. Definition checker_eq t_form l1 l2 l (c:certif) := - negb (Lit.is_pos l) && + negb (Lit.is_pos l) && match t_form.[Lit.blit l] with | Form.Fiff l1' l2' => (l1 == l1') && (l2 == l2') | _ => false - end && + end && checker t_form l c. Lemma checker_eq_correct : forall t_var t_form l1 l2 l c, @@ -317,7 +317,7 @@ Module Euf_Checker. Variable t_atom : array Atom.atom. Variable t_form : array Form.form. - Inductive step := +Inductive step := | Res (pos:int) (res:resolution) | ImmFlatten (pos:int) (cid:clause_id) (lf:_lit) | CTrue (pos:int) @@ -465,7 +465,7 @@ Module Euf_Checker. checker_b (* t_func t_atom t_form *) l b c = true -> Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) l = b. Proof. - unfold checker_b; intros (* t_i t_func t_atom t_form *) l b (nclauses, t, confl); case b; intros H2; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) l); auto; intros H1; elim (checker_correct H2); auto; unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; auto; rewrite Lit.interp_neg, H1; auto. + unfold checker_b; intros (* t_i t_func t_atom t_form *) l b (nclauses, t, confl); case b; intros H2; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) t_form) l); auto; intros H1; elim (checker_correct H2); auto; unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; auto; rewrite Lit.interp_neg, H1; auto. Qed. Definition checker_eq (* t_i t_func t_atom t_form *) l1 l2 l (c:certif) := diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml index ea5a42a..b320d7a 100644 --- a/src/smtlib2/smtlib2_genConstr.ml +++ b/src/smtlib2/smtlib2_genConstr.ml @@ -20,7 +20,6 @@ open SmtForm open SmtMisc open CoqTerms - (* For debugging *) let pp_symbol s = @@ -213,9 +212,8 @@ let make_root ra rf t = and make_root t = match make_root_term t with - | Atom h -> Form.get rf (Fatom h) - | Form f -> f in - + | Atom h -> Form.get rf (Fatom h) + | Form f -> f in make_root t diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 832778a..72e7ed3 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -133,33 +133,33 @@ module Btype = (** Operators *) -type cop = - | CO_xH - | CO_Z0 +type cop = + | CO_xH + | CO_Z0 type uop = - | UO_xO - | UO_xI - | UO_Zpos - | UO_Zneg - | UO_Zopp - -type bop = - | BO_Zplus - | BO_Zminus - | BO_Zmult - | BO_Zlt - | BO_Zle - | BO_Zge - | BO_Zgt - | BO_eq of btype + | UO_xO + | UO_xI + | UO_Zpos + | UO_Zneg + | UO_Zopp + +type bop = + | BO_Zplus + | BO_Zminus + | BO_Zmult + | BO_Zlt + | BO_Zle + | BO_Zge + | BO_Zgt + | BO_eq of btype type nop = | NO_distinct of btype -type op_def = { - tparams : btype array; - tres : btype; +type op_def = { + tparams : btype array; + tres : btype; op_val : Term.constr } type indexed_op = op_def gen_hashed @@ -175,7 +175,7 @@ type op = | Iop of indexed_op module Op = - struct + struct let c_to_coq = function | CO_xH -> Lazy.force cCO_xH | CO_Z0 -> Lazy.force cCO_Z0 @@ -188,18 +188,18 @@ module Op = | CO_xH -> Lazy.force cxH | CO_Z0 -> Lazy.force cZ0 - let u_to_coq = function + let u_to_coq = function | UO_xO -> Lazy.force cUO_xO | UO_xI -> Lazy.force cUO_xI - | UO_Zpos -> Lazy.force cUO_Zpos + | UO_Zpos -> Lazy.force cUO_Zpos | UO_Zneg -> Lazy.force cUO_Zneg | UO_Zopp -> Lazy.force cUO_Zopp - let u_type_of = function + let u_type_of = function | UO_xO | UO_xI -> Tpositive | UO_Zpos | UO_Zneg | UO_Zopp -> TZ - let u_type_arg = function + let u_type_arg = function | UO_xO | UO_xI | UO_Zpos | UO_Zneg -> Tpositive | UO_Zopp -> TZ @@ -210,15 +210,15 @@ module Op = | UO_Zneg -> Lazy.force cZneg | UO_Zopp -> Lazy.force copp - let eq_tbl = Hashtbl.create 17 + let eq_tbl = Hashtbl.create 17 let eq_to_coq t = - try Hashtbl.find eq_tbl t + try Hashtbl.find eq_tbl t with Not_found -> let op = mklApp cBO_eq [|Btype.to_coq t|] in Hashtbl.add eq_tbl t op; op - + let b_to_coq = function | BO_Zplus -> Lazy.force cBO_Zplus | BO_Zminus -> Lazy.force cBO_Zminus @@ -277,14 +277,14 @@ module Op = let i_type_of i = i.hval.tres let i_type_args i = i.hval.tparams - + (* reify table *) type reify_tbl = - { mutable count : int; - tbl : (Term.constr, indexed_op) Hashtbl.t - } + { mutable count : int; + tbl : (Term.constr, indexed_op) Hashtbl.t + } - let create () = + let create () = { count = 0; tbl = Hashtbl.create 17 } @@ -301,10 +301,10 @@ module Op = let interp_tbl tval mk_Tval reify = - let t = Array.make (reify.count + 1) - (mk_Tval [||] Tbool (Lazy.force ctrue)) in - let set _ v = - t.(v.index) <- mk_Tval v.hval.tparams v.hval.tres v.hval.op_val in + let t = Array.make (reify.count + 1) + (mk_Tval [||] Tbool (Lazy.force ctrue)) in + let set _ v = + t.(v.index) <- mk_Tval v.hval.tparams v.hval.tres v.hval.op_val in Hashtbl.iter set reify.tbl; Structures.mkArray (tval, t) @@ -320,12 +320,12 @@ module Op = let b_equal op1 op2 = match op1,op2 with - | BO_eq t1, BO_eq t2 -> Btype.equal t1 t2 - | _ -> op1 == op2 + | BO_eq t1, BO_eq t2 -> Btype.equal t1 t2 + | _ -> op1 == op2 let n_equal op1 op2 = match op1,op2 with - | NO_distinct t1, NO_distinct t2 -> Btype.equal t1 t2 + | NO_distinct t1, NO_distinct t2 -> Btype.equal t1 t2 let i_equal op1 op2 = op1.index == op2.index @@ -334,10 +334,10 @@ module Op = (** Definition of atoms *) -type atom = +type atom = | Acop of cop - | Auop of uop * hatom - | Abop of bop * hatom * hatom + | Auop of uop * hatom + | Abop of bop * hatom * hatom | Anop of nop * hatom array | Aapp of indexed_op * hatom array @@ -371,7 +371,7 @@ and hatom = atom gen_hashed (* | Aapp (op,a) -> "(Aapp "^(string_of_int op.index)^" ("^(Array.fold_left (fun acc h -> acc^" "^(pp_atom h.hval)) "" a)^"))" *) module HashedAtom = - struct + struct type t = atom let equal a b = @@ -379,53 +379,53 @@ module HashedAtom = | Acop opa, Acop opb -> Op.c_equal opa opb | Auop(opa,ha), Auop(opb,hb) -> Op.u_equal opa opb && ha.index == hb.index | Abop(opa,ha1,ha2), Abop(opb,hb1,hb2) -> - Op.b_equal opa opb && ha1.index == hb1.index && ha2.index == hb2.index + Op.b_equal opa opb && ha1.index == hb1.index && ha2.index == hb2.index | Anop (opa,ha), Anop (opb,hb) -> - let na = Array.length ha in - let nb = Array.length hb in - let i = ref (-1) in - Op.n_equal opa opb && na == nb && Array.fold_left (fun b h -> incr i; b && h.index == hb.(!i).index) true ha + let na = Array.length ha in + let nb = Array.length hb in + let i = ref (-1) in + Op.n_equal opa opb && na == nb && Array.fold_left (fun b h -> incr i; b && h.index == hb.(!i).index) true ha | Aapp (va,ha), Aapp (vb,hb) -> - let na = Array.length ha in - let nb = Array.length hb in - let i = ref (-1) in - Op.i_equal va vb && na == nb && Array.fold_left (fun b h -> incr i; b && h.index == hb.(!i).index) true ha + let na = Array.length ha in + let nb = Array.length hb in + let i = ref (-1) in + Op.i_equal va vb && na == nb && Array.fold_left (fun b h -> incr i; b && h.index == hb.(!i).index) true ha | _, _ -> false let hash = function | Acop op -> ((Hashtbl.hash op) lsl 3) lxor 1 | Auop (op,h) -> - (( (h.index lsl 3) + (Hashtbl.hash op)) lsl 3) lxor 2 + (( (h.index lsl 3) + (Hashtbl.hash op)) lsl 3) lxor 2 | Abop (op,h1,h2) -> - (((( (h1.index lsl 2) + h2.index) lsl 3) + Hashtbl.hash op) lsl 3) lxor 3 + (((( (h1.index lsl 2) + h2.index) lsl 3) + Hashtbl.hash op) lsl 3) lxor 3 | Anop (op, args) -> - let hash_args = - match Array.length args with - | 0 -> 0 - | 1 -> args.(0).index - | 2 -> args.(1).index lsl 2 + args.(0).index - | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index in - (hash_args lsl 5 + (Hashtbl.hash op) lsl 3) lxor 4 + let hash_args = + match Array.length args with + | 0 -> 0 + | 1 -> args.(0).index + | 2 -> args.(1).index lsl 2 + args.(0).index + | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index in + (hash_args lsl 5 + (Hashtbl.hash op) lsl 3) lxor 4 | Aapp (op, args) -> - let hash_args = - match Array.length args with - | 0 -> 0 - | 1 -> args.(0).index - | 2 -> args.(1).index lsl 2 + args.(0).index - | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index in - (hash_args lsl 5 + op.index lsl 3) lxor 4 + let hash_args = + match Array.length args with + | 0 -> 0 + | 1 -> args.(0).index + | 2 -> args.(1).index lsl 2 + args.(0).index + | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index in + (hash_args lsl 5 + op.index lsl 3) lxor 4 end module HashAtom = Hashtbl.Make(HashedAtom) -module Atom = - struct +module Atom = + struct type t = hatom let atom h = h.hval - let index h = h.index + let index h = h.index let equal h1 h2 = h1.index == h2.index @@ -442,11 +442,11 @@ module Atom = let rec compute_int = function | Acop c -> - (match c with + (match c with | CO_xH -> 1 | CO_Z0 -> 0) | Auop (op,h) -> - (match op with + (match op with | UO_xO -> 2*(compute_hint h) | UO_xI -> 2*(compute_hint h) + 1 | UO_Zpos -> compute_hint h @@ -464,46 +464,46 @@ module Atom = let rec to_smt fmt h = to_smt_atom fmt (atom h) - and to_smt_atom fmt = function - | Acop _ as a -> to_smt_int fmt (compute_int a) - | Auop (UO_Zopp,h) -> - Format.fprintf fmt "(- "; - to_smt fmt h; - Format.fprintf fmt ")" - | Auop _ as a -> to_smt_int fmt (compute_int a) - | Abop (op,h1,h2) -> to_smt_bop fmt op h1 h2 - | Anop (op,a) -> to_smt_nop fmt op a - | Aapp (op,a) -> - if Array.length a = 0 then ( - Format.fprintf fmt "op_%i" op.index; - ) else ( - Format.fprintf fmt "(op_%i" op.index; - Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) a; + and to_smt_atom fmt = function + | Acop _ as a -> to_smt_int fmt (compute_int a) + | Auop (UO_Zopp,h) -> + Format.fprintf fmt "(- "; + to_smt fmt h; Format.fprintf fmt ")" - ) - - and to_smt_bop fmt op h1 h2 = - let s = match op with - | BO_Zplus -> "+" - | BO_Zminus -> "-" - | BO_Zmult -> "*" - | BO_Zlt -> "<" - | BO_Zle -> "<=" - | BO_Zge -> ">=" - | BO_Zgt -> ">" - | BO_eq _ -> "=" in - Format.fprintf fmt "(%s " s; - to_smt fmt h1; - Format.fprintf fmt " "; - to_smt fmt h2; - Format.fprintf fmt ")" - - and to_smt_nop fmt op a = - let s = match op with - | NO_distinct _ -> "distinct" in - Format.fprintf fmt "(%s" s; - Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) a; - Format.fprintf fmt ")" + | Auop _ as a -> to_smt_int fmt (compute_int a) + | Abop (op,h1,h2) -> to_smt_bop fmt op h1 h2 + | Anop (op,a) -> to_smt_nop fmt op a + | Aapp (op,a) -> + if Array.length a = 0 then ( + Format.fprintf fmt "op_%i" op.index; + ) else ( + Format.fprintf fmt "(op_%i" op.index; + Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) a; + Format.fprintf fmt ")" + ) + + and to_smt_bop fmt op h1 h2 = + let s = match op with + | BO_Zplus -> "+" + | BO_Zminus -> "-" + | BO_Zmult -> "*" + | BO_Zlt -> "<" + | BO_Zle -> "<=" + | BO_Zge -> ">=" + | BO_Zgt -> ">" + | BO_eq _ -> "=" in + Format.fprintf fmt "(%s " s; + to_smt fmt h1; + Format.fprintf fmt " "; + to_smt fmt h2; + Format.fprintf fmt ")" + + and to_smt_nop fmt op a = + let s = match op with + | NO_distinct _ -> "distinct" in + Format.fprintf fmt "(%s" s; + Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) a; + Format.fprintf fmt ")" @@ -512,28 +512,29 @@ module Atom = let check a = match a with | Acop _ -> () - | Auop(op,h) -> - if not (Btype.equal (Op.u_type_arg op) (type_of h)) then - raise (NotWellTyped a) + | Auop(op,h) -> + if not (Btype.equal (Op.u_type_arg op) (type_of h)) + then raise (NotWellTyped a) | Abop(op,h1,h2) -> - let (t1,t2) = Op.b_type_args op in - if not (Btype.equal t1 (type_of h1) && Btype.equal t2 (type_of h2)) - then raise (NotWellTyped a) + let (t1,t2) = Op.b_type_args op in + if not (Btype.equal t1 (type_of h1) && Btype.equal t2 (type_of h2)) + then raise (NotWellTyped a) | Anop(op,ha) -> - let ty = Op.n_type_args op in - Array.iter (fun h -> if not (Btype.equal ty (type_of h)) then raise (NotWellTyped a)) ha + let ty = Op.n_type_args op in + Array.iter (fun h -> if not (Btype.equal ty (type_of h)) then raise (NotWellTyped a)) ha | Aapp(op,args) -> - let tparams = Op.i_type_args op in - Array.iteri (fun i t -> - if not (Btype.equal t (type_of args.(i))) then - raise (NotWellTyped a)) tparams + let tparams = Op.i_type_args op in + Array.iteri (fun i t -> + if not (Btype.equal t (type_of args.(i))) then + raise (NotWellTyped a)) tparams type reify_tbl = - { mutable count : int; - tbl : hatom HashAtom.t - } + { mutable count : int; + tbl : hatom HashAtom.t + } - let create () = + + let create () = { count = 0; tbl = HashAtom.create 17 } @@ -541,7 +542,7 @@ module Atom = reify.count <- 0; HashAtom.clear reify.tbl - let declare reify a = + let declare reify a = check a; let res = {index = reify.count; hval = a} in HashAtom.add reify.tbl a res; @@ -549,7 +550,7 @@ module Atom = res let get reify a = - try HashAtom.find reify.tbl a + try HashAtom.find reify.tbl a with Not_found -> declare reify a @@ -594,26 +595,26 @@ module Atom = try Hashtbl.find op_tbl c with Not_found -> CCunknown in let mk_cop op = get reify (Acop op) in let rec mk_hatom h = - let c, args = Term.decompose_app h in + let c, args = Term.decompose_app h in match get_cst c with - | CCxH -> mk_cop CO_xH - | CCZ0 -> mk_cop CO_Z0 - | CCxO -> mk_uop UO_xO args - | CCxI -> mk_uop UO_xI args - | CCZpos -> mk_uop UO_Zpos args - | CCZneg -> mk_uop UO_Zneg args - | CCZopp -> mk_uop UO_Zopp args - | CCZplus -> mk_bop BO_Zplus args - | CCZminus -> mk_bop BO_Zminus args - | CCZmult -> mk_bop BO_Zmult args - | CCZlt -> mk_bop BO_Zlt args - | CCZle -> mk_bop BO_Zle args - | CCZge -> mk_bop BO_Zge args - | CCZgt -> mk_bop BO_Zgt args - | CCeqb -> mk_bop (BO_eq Tbool) args - | CCeqbP -> mk_bop (BO_eq Tpositive) args - | CCeqbZ -> mk_bop (BO_eq TZ) args - | CCunknown -> mk_unknown c args (Retyping.get_type_of env sigma h) + | CCxH -> mk_cop CO_xH + | CCZ0 -> mk_cop CO_Z0 + | CCxO -> mk_uop UO_xO args + | CCxI -> mk_uop UO_xI args + | CCZpos -> mk_uop UO_Zpos args + | CCZneg -> mk_uop UO_Zneg args + | CCZopp -> mk_uop UO_Zopp args + | CCZplus -> mk_bop BO_Zplus args + | CCZminus -> mk_bop BO_Zminus args + | CCZmult -> mk_bop BO_Zmult args + | CCZlt -> mk_bop BO_Zlt args + | CCZle -> mk_bop BO_Zle args + | CCZge -> mk_bop BO_Zge args + | CCZgt -> mk_bop BO_Zgt args + | CCeqb -> mk_bop (BO_eq Tbool) args + | CCeqbP -> mk_bop (BO_eq Tpositive) args + | CCeqbZ -> mk_bop (BO_eq TZ) args + | CCunknown -> mk_unknown c args (Retyping.get_type_of env sigma h) and mk_uop op = function | [a] -> let h = mk_hatom a in get reify (Auop (op,h)) @@ -621,22 +622,21 @@ module Atom = and mk_bop op = function | [a1;a2] -> - let h1 = mk_hatom a1 in - let h2 = mk_hatom a2 in - get reify (Abop (op,h1,h2)) + let h1 = mk_hatom a1 in + let h2 = mk_hatom a2 in + get reify (Abop (op,h1,h2)) | _ -> assert false and mk_unknown c args ty = let hargs = Array.of_list (List.map mk_hatom args) in - let op = - try Op.of_coq ro c - with | Not_found -> - let targs = Array.map type_of hargs in - let tres = Btype.of_coq rt ty in - Op.declare ro c targs tres in + let op = try Op.of_coq ro c + with Not_found -> + let targs = Array.map type_of hargs in + let tres = Btype.of_coq rt ty in + Op.declare ro c targs tres in get reify (Aapp (op,hargs)) in - mk_hatom c + mk_hatom c let to_coq h = mkInt h.index @@ -645,16 +645,16 @@ module Atom = match a with | Acop op -> mklApp cAcop [|Op.c_to_coq op|] | Auop (op,h) -> mklApp cAuop [|Op.u_to_coq op; to_coq h|] - | Abop (op,h1,h2) -> - mklApp cAbop [|Op.b_to_coq op;to_coq h1; to_coq h2|] + | Abop (op,h1,h2) -> + mklApp cAbop [|Op.b_to_coq op;to_coq h1; to_coq h2|] | Anop (op,ha) -> - let cop = Op.n_to_coq op in - let cargs = Array.fold_right (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|]) ha (mklApp cnil [|Lazy.force cint|]) in - mklApp cAnop [|cop; cargs|] + let cop = Op.n_to_coq op in + let cargs = Array.fold_right (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|]) ha (mklApp cnil [|Lazy.force cint|]) in + mklApp cAnop [|cop; cargs|] | Aapp (op,args) -> - let cop = Op.i_to_coq op in - let cargs = Array.fold_right (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|]) args (mklApp cnil [|Lazy.force cint|]) in - mklApp cAapp [|cop; cargs|] + let cop = Op.i_to_coq op in + let cargs = Array.fold_right (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|]) args (mklApp cnil [|Lazy.force cint|]) in + mklApp cAapp [|cop; cargs|] let dft_atom = lazy (mklApp cAcop [| Lazy.force cCO_xH |]) @@ -677,15 +677,15 @@ module Atom = with Not_found -> let pc = match atom a with - | Acop c -> Op.interp_cop c - | Auop (op,h) -> Term.mkApp (Op.interp_uop op, [|interp_atom h|]) - | Abop (op,h1,h2) -> Term.mkApp (Op.interp_bop op, [|interp_atom h1; interp_atom h2|]) - | Anop (NO_distinct ty as op,ha) -> - let cop = Op.interp_nop op in - let typ = Op.interp_distinct ty in - let cargs = Array.fold_right (fun h l -> mklApp ccons [|typ; interp_atom h; l|]) ha (mklApp cnil [|typ|]) in - Term.mkApp (cop,[|cargs|]) - | Aapp (op,t) -> Term.mkApp (op.hval.op_val, Array.map interp_atom t) in + | Acop c -> Op.interp_cop c + | Auop (op,h) -> Term.mkApp (Op.interp_uop op, [|interp_atom h|]) + | Abop (op,h1,h2) -> Term.mkApp (Op.interp_bop op, [|interp_atom h1; interp_atom h2|]) + | Anop (NO_distinct ty as op,ha) -> + let cop = Op.interp_nop op in + let typ = Op.interp_distinct ty in + let cargs = Array.fold_right (fun h l -> mklApp ccons [|typ; interp_atom h; l|]) ha (mklApp cnil [|typ|]) in + Term.mkApp (cop,[|cargs|]) + | Aapp (op,t) -> Term.mkApp (op.hval.op_val, Array.map interp_atom t) in Hashtbl.add atom_tbl l pc; pc in interp_atom a diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli index cdcdcd1..e6a3c47 100644 --- a/src/trace/smtAtom.mli +++ b/src/trace/smtAtom.mli @@ -142,8 +142,8 @@ module Atom : val get : reify_tbl -> atom -> hatom (** Given a coq term, build the corresponding atom *) - val of_coq : Btype.reify_tbl -> Op.reify_tbl -> reify_tbl -> - Environ.env -> Evd.evar_map -> Term.constr -> t + val of_coq : Btype.reify_tbl -> Op.reify_tbl -> + reify_tbl -> Environ.env -> Evd.evar_map -> Term.constr -> t val to_coq : hatom -> Term.constr @@ -157,6 +157,7 @@ module Atom : (* Generation of atoms *) val hatom_Z_of_int : reify_tbl -> int -> hatom val hatom_Z_of_bigint : reify_tbl -> Big_int.big_int -> hatom + val mk_eq : reify_tbl -> btype -> hatom -> hatom -> hatom val mk_lt : reify_tbl -> hatom -> hatom -> hatom val mk_le : reify_tbl -> hatom -> hatom -> hatom diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml index e4ed262..a0972d4 100644 --- a/src/trace/smtCertif.ml +++ b/src/trace/smtCertif.ml @@ -21,18 +21,18 @@ type used = int type clause_id = int type 'hform rule = - | ImmFlatten of 'hform clause * 'hform + | ImmFlatten of 'hform clause * 'hform (* CNF Transformations *) - | True - (* * true : {true} + | True + (* * true : {true} *) - | False - (* * false : {(not false)} + | False + (* * false : {(not false)} *) - | BuildDef of 'hform (* the first literal of the clause *) + | BuildDef of 'hform (* the first literal of the clause *) (* * and_neg : {(and a_1 ... a_n) (not a_1) ... (not a_n)} - * or_pos : {(not (or a_1 ... a_n)) a_1 ... a_n} + * or_pos : {(not (or a_1 ... a_n)) a_1 ... a_n} * implies_pos : {(not (implies a b)) (not a) b} * xor_pos1 : {(not (xor a b)) a b} * xor_neg1 : {(xor a b) a (not b)} @@ -41,7 +41,7 @@ type 'hform rule = * ite_pos1 : {(not (if_then_else a b c)) a c} * ite_neg1 : {(if_then_else a b c) a (not c)} *) - | BuildDef2 of 'hform (* the first literal of the clause *) + | BuildDef2 of 'hform (* the first literal of the clause *) (* * xor_pos2 : {(not (xor a b)) (not a) (not b)} * xor_neg2 : {(xor a b) (not a) b} * equiv_pos2 : {(not (iff a b)) (not a) b} @@ -50,15 +50,15 @@ type 'hform rule = * ite_neg2 : {(if_then_else a b c) (not a) (not b)} *) - | BuildProj of 'hform * int + | BuildProj of 'hform * int (* * or_neg : {(or a_1 ... a_n) (not a_i)} - * and_pos : {(not (and a_1 ... a_n)) a_i} + * and_pos : {(not (and a_1 ... a_n)) a_i} * implies_neg1 : {(implies a b) a} * implies_neg2 : {(implies a b) (not b)} *) (* Immediate CNF transformation : CNF transformation + Reso *) - | ImmBuildDef of 'hform clause + | ImmBuildDef of 'hform clause (* * not_and : {(not (and a_1 ... a_n))} --> {(not a_1) ... (not a_n)} * or : {(or a_1 ... a_n)} --> {a_1 ... a_n} * implies : {(implies a b)} --> {(not a) b} @@ -78,7 +78,7 @@ type 'hform rule = * not_ite2 : {(not (if_then_else a b c))} --> {(not a) (not b)} *) | ImmBuildProj of 'hform clause * int - (* * and : {(and a_1 ... a_n)} --> {a_i} + (* * and : {(and a_1 ... a_n)} --> {a_i} * not_or : {(not (or a_1 ... a_n))} --> {(not a_i)} * not_implies1 : {(not (implies a b))} --> {a} * not_implies2 : {(not (implies a b))} --> {(not b)} @@ -90,11 +90,11 @@ type 'hform rule = * eq_transitive : {(not (= x_1 x_2)) ... (not (= x_{n-1} x_n)) (= x_1 x_n)} *) | EqCgr of 'hform * ('hform option) list - (* * eq_congruent : {(not (= x_1 y_1)) ... (not (= x_n y_n)) + (* * eq_congruent : {(not (= x_1 y_1)) ... (not (= x_n y_n)) (= (f x_1 ... x_n) (f y_1 ... y_n))} *) | EqCgrP of 'hform * 'hform * ('hform option) list - (* * eq_congruent_pred : {(not (= x_1 y_1)) ... (not (= x_n y_n)) + (* * eq_congruent_pred : {(not (= x_1 y_1)) ... (not (= x_n y_n)) (not (p x_1 ... x_n)) (p y_1 ... y_n)} *) diff --git a/src/trace/smtCertif.mli b/src/trace/smtCertif.mli index dee465c..767dc8b 100644 --- a/src/trace/smtCertif.mli +++ b/src/trace/smtCertif.mli @@ -20,14 +20,15 @@ type 'hform rule = Structures.Micromega_plugin_Certificate.Mc.zArithProof list | SplDistinctElim of 'hform clause * 'hform | Hole of 'hform clause list * 'hform list + and 'hform clause = { - id : clause_id; - mutable kind : 'hform clause_kind; - mutable pos : int option; - mutable used : used; - mutable prev : 'hform clause option; - mutable next : 'hform clause option; - value : 'hform list option; + id : clause_id; + mutable kind : 'hform clause_kind; + mutable pos : int option; + mutable used : used; + mutable prev : 'hform clause option; + mutable next : 'hform clause option; + value : 'hform list option; } and 'hform clause_kind = Root diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index d8ec105..8950022 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -39,7 +39,6 @@ let cchecker_eq_correct = gen_constant euf_checker_modules "checker_eq_correct" let cchecker_eq = gen_constant euf_checker_modules "checker_eq" - (* Given an SMT-LIB2 file and a certif, build the corresponding objects *) let compute_roots roots last_root = @@ -387,12 +386,11 @@ let core_tactic call_solver rt ro ra rf env sigma concl = let cuts = (Btype.get_cuts rt)@cuts in List.fold_right (fun (eqn, eqt) tac -> - Structures.tclTHENLAST (Structures.assert_before (Names.Name eqn) eqt) tac - ) cuts - (Structures.tclTHEN - (Structures.set_evars_tac body_nocast) - (Structures.vm_cast_no_check body_cast)) - + Structures.tclTHENLAST (Structures.assert_before (Names.Name eqn) eqt) tac) + cuts + (Structures.tclTHEN + (Structures.set_evars_tac body_nocast) + (Structures.vm_cast_no_check body_cast)) let tactic call_solver rt ro ra rf = Structures.tclTHEN diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml index 1abea36..069f2ec 100644 --- a/src/trace/smtForm.ml +++ b/src/trace/smtForm.ml @@ -18,17 +18,17 @@ open Util open SmtMisc open CoqTerms -module type ATOM = - sig +module type ATOM = + sig - type t + type t val index : t -> int val equal : t -> t -> bool val is_bool_type : t -> bool - end + end type fop = @@ -42,80 +42,80 @@ type fop = | Fite | Fnot2 of int -type ('a,'f) gen_pform = +type ('a,'f) gen_pform = | Fatom of 'a | Fapp of fop * 'f array module type FORM = - sig - type hatom + sig + type hatom type t type pform = (hatom, t) gen_pform - val pform_true : pform - val pform_false : pform + val pform_true : pform + val pform_false : pform - val equal : t -> t -> bool + val equal : t -> t -> bool - val to_lit : t -> int - val index : t -> int - val pform : t -> pform + val to_lit : t -> int + val index : t -> int + val pform : t -> pform - val neg : t -> t - val is_pos : t -> bool - val is_neg : t -> bool + val neg : t -> t + val is_pos : t -> bool + val is_neg : t -> bool val to_smt : (Format.formatter -> hatom -> unit) -> Format.formatter -> t -> unit - (* Building formula from positive formula *) - exception NotWellTyped of pform - type reify - val create : unit -> reify - val clear : reify -> unit - val get : reify -> pform -> t - - (** Give a coq term, build the corresponding formula *) - val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t - - (** Flattening of [Fand] and [For], removing of [Fnot2] *) - val flatten : reify -> t -> t - - (** Producing Coq terms *) - - val to_coq : t -> Term.constr - - val pform_tbl : reify -> pform array - - val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array - val interp_tbl : reify -> Term.constr * Term.constr - val nvars : reify -> int - (** Producing a Coq term corresponding to the interpretation + (* Building formula from positive formula *) + exception NotWellTyped of pform + type reify + val create : unit -> reify + val clear : reify -> unit + val get : reify -> pform -> t + + (** Give a coq term, build the corresponding formula *) + val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t + + (** Flattening of [Fand] and [For], removing of [Fnot2] *) + val flatten : reify -> t -> t + + (** Producing Coq terms *) + + val to_coq : t -> Term.constr + + val pform_tbl : reify -> pform array + + val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array + val interp_tbl : reify -> Term.constr * Term.constr + val nvars : reify -> int + (** Producing a Coq term corresponding to the interpretation of a formula *) - (** [interp_atom] map [hatom] to coq term, it is better if it produce + (** [interp_atom] map [hatom] to coq term, it is better if it produce shared terms. *) - val interp_to_coq : - (hatom -> Term.constr) -> (int, Term.constr) Hashtbl.t -> - t -> Term.constr + val interp_to_coq : + (hatom -> Term.constr) -> (int, Term.constr) Hashtbl.t -> + t -> Term.constr end module Make (Atom:ATOM) = - struct + struct - type hatom = Atom.t + type hatom = Atom.t type pform = (Atom.t, t) gen_pform - + and hpform = pform gen_hashed - - and t = + + and t = | Pos of hpform - | Neg of hpform + | Neg of hpform let pform_true = Fapp (Ftrue,[||]) let pform_false = Fapp (Ffalse,[||]) - let equal h1 h2 = + let equal h1 h2 = match h1, h2 with | Pos hp1, Pos hp2 -> hp1.index == hp2.index | Neg hp1, Neg hp2 -> hp1.index == hp2.index @@ -132,11 +132,11 @@ module Make (Atom:ATOM) = let neg = function | Pos hp -> Neg hp | Neg hp -> Pos hp - + let is_pos = function | Pos _ -> true | _ -> false - + let is_neg = function | Neg _ -> true | _ -> false @@ -175,63 +175,63 @@ module Make (Atom:ATOM) = module HashedForm = - struct - + struct + type t = pform - - let equal pf1 pf2 = + + let equal pf1 pf2 = match pf1, pf2 with | Fatom ha1, Fatom ha2 -> Atom.equal ha1 ha2 | Fapp(op1,args1), Fapp(op2,args2) -> op1 = op2 && - Array.length args1 == Array.length args2 && - (try - for i = 0 to Array.length args1 - 1 do - if not (equal args1.(i) args2.(i)) then raise Not_found - done; - true - with Not_found -> false) + Array.length args1 == Array.length args2 && + (try + for i = 0 to Array.length args1 - 1 do + if not (equal args1.(i) args2.(i)) then raise Not_found + done; + true + with Not_found -> false) | _, _ -> false - let hash pf = + let hash pf = match pf with - | Fatom ha1 -> Atom.index ha1 * 2 - | Fapp(op, args) -> - let hash_args = - match Array.length args with - | 0 -> 0 - | 1 -> to_lit args.(0) - | 2 -> (to_lit args.(1)) lsl 2 + to_lit args.(0) - | _ -> - (to_lit args.(2)) lsl 4 + (to_lit args.(1)) lsl 2 + - to_lit args.(0) in - (hash_args * 10 + Hashtbl.hash op) * 2 + 1 - + | Fatom ha1 -> Atom.index ha1 * 2 + | Fapp(op, args) -> + let hash_args = + match Array.length args with + | 0 -> 0 + | 1 -> to_lit args.(0) + | 2 -> (to_lit args.(1)) lsl 2 + to_lit args.(0) + | _ -> + (to_lit args.(2)) lsl 4 + (to_lit args.(1)) lsl 2 + + to_lit args.(0) in + (hash_args * 10 + Hashtbl.hash op) * 2 + 1 + end module HashForm = Hashtbl.Make (HashedForm) type reify = { mutable count : int; - tbl : t HashForm.t - } + tbl : t HashForm.t + } exception NotWellTyped of pform - - let check pf = + + let check pf = match pf with | Fatom ha -> if not (Atom.is_bool_type ha) then raise (NotWellTyped pf) | Fapp (op, args) -> - match op with - | Ftrue | Ffalse -> - if Array.length args <> 0 then raise (NotWellTyped pf) - | Fnot2 _ -> - if Array.length args <> 1 then raise (NotWellTyped pf) - | Fand | For -> () - | Fxor | Fimp | Fiff -> - if Array.length args <> 2 then raise (NotWellTyped pf) - | Fite -> - if Array.length args <> 3 then raise (NotWellTyped pf) + match op with + | Ftrue | Ffalse -> + if Array.length args <> 0 then raise (NotWellTyped pf) + | Fnot2 _ -> + if Array.length args <> 1 then raise (NotWellTyped pf) + | Fand | For -> () + | Fxor | Fimp | Fiff -> + if Array.length args <> 2 then raise (NotWellTyped pf) + | Fite -> + if Array.length args <> 3 then raise (NotWellTyped pf) let declare reify pf = check pf; @@ -241,8 +241,8 @@ module Make (Atom:ATOM) = res let create () = - let reify = - { count = 0; + let reify = + { count = 0; tbl = HashForm.create 17 } in let _ = declare reify pform_true in let _ = declare reify pform_false in @@ -256,12 +256,11 @@ module Make (Atom:ATOM) = () let get reify pf = - try HashForm.find reify.tbl pf + try HashForm.find reify.tbl pf with Not_found -> declare reify pf - - (** Given a coq term, build the corresponding formula *) - type coq_cst = + (** Given a coq term, build the corresponding formula *) + type coq_cst = | CCtrue | CCfalse | CCnot @@ -283,11 +282,11 @@ module Make (Atom:ATOM) = let op_tbl () = let tbl = ConstrHashtbl.create 29 in let add (c1,c2) = ConstrHashtbl.add tbl (Lazy.force c1) c2 in - List.iter add + List.iter add [ - ctrue,CCtrue; cfalse,CCfalse; - candb,CCand; corb,CCor; cxorb,CCxor; cimplb,CCimp; cnegb,CCnot; - ceqb,CCiff; cifb,CCifb ]; + ctrue,CCtrue; cfalse,CCfalse; + candb,CCand; corb,CCor; cxorb,CCxor; cimplb,CCimp; cnegb,CCnot; + ceqb,CCiff; cifb,CCifb ]; tbl let op_tbl = lazy (op_tbl ()) @@ -296,125 +295,124 @@ module Make (Atom:ATOM) = let of_coq atom_of_coq reify c = let op_tbl = Lazy.force op_tbl in - let get_cst c = - try ConstrHashtbl.find op_tbl c with Not_found -> CCunknown in + let get_cst c = + try ConstrHashtbl.find op_tbl c with Not_found -> CCunknown in let rec mk_hform h = - let c, args = Term.decompose_app h in - match get_cst c with - | CCtrue -> get reify (Fapp(Ftrue,empty_args)) - | CCfalse -> get reify (Fapp(Ffalse,empty_args)) - | CCnot -> mk_fnot 1 args - | CCand -> mk_fand [] args - | CCor -> mk_for [] args - | CCxor -> op2 (fun l -> Fapp(Fxor,l)) args - | CCiff -> op2 (fun l -> Fapp(Fiff,l)) args - | CCimp -> - (match args with + let c, args = Term.decompose_app h in + match get_cst c with + | CCtrue -> get reify (Fapp(Ftrue,empty_args)) + | CCfalse -> get reify (Fapp(Ffalse,empty_args)) + | CCnot -> mk_fnot 1 args + | CCand -> mk_fand [] args + | CCor -> mk_for [] args + | CCxor -> op2 (fun l -> Fapp(Fxor,l)) args + | CCiff -> op2 (fun l -> Fapp(Fiff,l)) args + | CCimp -> + (match args with | [b1;b2] -> + let l1 = mk_hform b1 in + let l2 = mk_hform b2 in + get reify (Fapp (Fimp, [|l1;l2|])) + | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for implb") + | CCifb -> + (* We should also be able to reify if then else *) + begin match args with + | [b1;b2;b3] -> let l1 = mk_hform b1 in let l2 = mk_hform b2 in - get reify (Fapp (Fimp, [|l1;l2|])) - | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for implb") - | CCifb -> - (* We should also be able to reify if then else *) - begin match args with - | [b1;b2;b3] -> - let l1 = mk_hform b1 in - let l2 = mk_hform b2 in - let l3 = mk_hform b3 in - get reify (Fapp(Fite, [|l1;l2;l3|])) - | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for ifb" - end - | _ -> - let a = atom_of_coq h in - get reify (Fatom a) + let l3 = mk_hform b3 in + get reify (Fapp (Fite, [|l1;l2;l3|])) + | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for ifb" + end + | _ -> + let a = atom_of_coq h in + get reify (Fatom a) and op2 f args = - match args with - | [b1;b2] -> - let l1 = mk_hform b1 in - let l2 = mk_hform b2 in - get reify (f [|l1; l2|]) - | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments" - + match args with + | [b1;b2] -> + let l1 = mk_hform b1 in + let l2 = mk_hform b2 in + get reify (f [|l1; l2|]) + | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments" + and mk_fnot i args = - match args with - | [t] -> - let c,args = Term.decompose_app t in - if Term.eq_constr c (Lazy.force cnegb) then - mk_fnot (i+1) args - else - let q,r = i lsr 1 , i land 1 in - let l = mk_hform t in - let l = if r = 0 then l else neg l in - if q = 0 then l - else get reify (Fapp(Fnot2 q, [|l|])) - | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for negb" - - and mk_fand acc args = - match args with - | [t1;t2] -> - let l2 = mk_hform t2 in - let c, args = Term.decompose_app t1 in - if Term.eq_constr c (Lazy.force candb) then - mk_fand (l2::acc) args - else - let l1 = mk_hform t1 in - get reify (Fapp(Fand, Array.of_list (l1::l2::acc))) - | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for andb" - - and mk_for acc args = - match args with - | [t1;t2] -> - let l2 = mk_hform t2 in - let c, args = Term.decompose_app t1 in - if Term.eq_constr c (Lazy.force corb) then - mk_for (l2::acc) args - else - let l1 = mk_hform t1 in - get reify (Fapp(For, Array.of_list (l1::l2::acc))) - | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in - - let l = mk_hform c in - l + match args with + | [t] -> + let c,args = Term.decompose_app t in + if Term.eq_constr c (Lazy.force cnegb) then + mk_fnot (i+1) args + else + let q,r = i lsr 1 , i land 1 in + let l = mk_hform t in + let l = if r = 0 then l else neg l in + if q = 0 then l + else get reify (Fapp(Fnot2 q, [|l|])) + | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for negb" + + and mk_fand acc args = + match args with + | [t1;t2] -> + let l2 = mk_hform t2 in + let c, args = Term.decompose_app t1 in + if Term.eq_constr c (Lazy.force candb) then + mk_fand (l2::acc) args + else + let l1 = mk_hform t1 in + get reify (Fapp(Fand, Array.of_list (l1::l2::acc))) + | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for andb" + + and mk_for acc args = + match args with + | [t1;t2] -> + let l2 = mk_hform t2 in + let c, args = Term.decompose_app t1 in + if Term.eq_constr c (Lazy.force corb) then + mk_for (l2::acc) args + else + let l1 = mk_hform t1 in + get reify (Fapp(For, Array.of_list (l1::l2::acc))) + | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in + + mk_hform c (** Flattening of Fand and For, removing of Fnot2 *) let set_sign f f' = if is_pos f then f' else neg f' - let rec flatten reify f = + let rec flatten reify f = match pform f with | Fatom _ -> f | Fapp(Fnot2 _,args) -> set_sign f (flatten reify args.(0)) | Fapp(Fand, args) -> set_sign f (flatten_and reify [] (Array.to_list args)) | Fapp(For,args) -> set_sign f (flatten_or reify [] (Array.to_list args)) | Fapp(op,args) -> - (* TODO change Fimp into For ? *) - set_sign f (get reify (Fapp(op, Array.map (flatten reify) args))) + (* TODO change Fimp into For ? *) + set_sign f (get reify (Fapp(op, Array.map (flatten reify) args))) and flatten_and reify acc args = match args with | [] -> get reify (Fapp(Fand, Array.of_list (List.rev acc))) | a::args -> - (* TODO change (not For) and (not Fimp) into Fand *) - match pform a with - | Fapp(Fand, args') when is_pos a -> - let args = Array.fold_right (fun a args -> a::args) args' args in - flatten_and reify acc args - | _ -> flatten_and reify (flatten reify a :: acc) args + (* TODO change (not For) and (not Fimp) into Fand *) + match pform a with + | Fapp(Fand, args') when is_pos a -> + let args = Array.fold_right (fun a args -> a::args) args' args in + flatten_and reify acc args + | _ -> flatten_and reify (flatten reify a :: acc) args and flatten_or reify acc args = (* TODO change Fimp and (not Fand) into For *) match args with | [] -> get reify (Fapp(For, Array.of_list (List.rev acc))) | a::args -> - match pform a with - | Fapp(For, args') when is_pos a -> - let args = Array.fold_right (fun a args -> a::args) args' args in - flatten_or reify acc args - | _ -> flatten_or reify (flatten reify a :: acc) args + match pform a with + | Fapp(For, args') when is_pos a -> + let args = Array.fold_right (fun a args -> a::args) args' args in + flatten_or reify acc args + | _ -> flatten_or reify (flatten reify a :: acc) args - (** Producing Coq terms *) + (** Producing Coq terms *) let to_coq hf = mkInt (to_lit hf) @@ -422,20 +420,20 @@ module Make (Atom:ATOM) = let cargs = Array.make (Array.length args + 1) (mkInt 0) in Array.iteri (fun i hf -> cargs.(i) <- to_coq hf) args; Structures.mkArray (Lazy.force cint, cargs) - + let pf_to_coq = function - | Fatom a -> mklApp cFatom [|mkInt (Atom.index a)|] + | Fatom a -> mklApp cFatom [|mkInt (Atom.index a)|] | Fapp(op,args) -> - match op with - | Ftrue -> Lazy.force cFtrue - | Ffalse -> Lazy.force cFfalse - | Fand -> mklApp cFand [| args_to_coq args|] - | For -> mklApp cFor [| args_to_coq args|] - | Fimp -> mklApp cFimp [| args_to_coq args|] - | Fxor -> mklApp cFxor (Array.map to_coq args) - | Fiff -> mklApp cFiff (Array.map to_coq args) - | Fite -> mklApp cFite (Array.map to_coq args) - | Fnot2 i -> mklApp cFnot2 [|mkInt i; to_coq args.(0)|] + match op with + | Ftrue -> Lazy.force cFtrue + | Ffalse -> Lazy.force cFfalse + | Fand -> mklApp cFand [| args_to_coq args|] + | For -> mklApp cFor [| args_to_coq args|] + | Fimp -> mklApp cFimp [| args_to_coq args|] + | Fxor -> mklApp cFxor (Array.map to_coq args) + | Fiff -> mklApp cFiff (Array.map to_coq args) + | Fite -> mklApp cFite (Array.map to_coq args) + | Fnot2 i -> mklApp cFnot2 [|mkInt i; to_coq args.(0)|] let pform_tbl reify = let t = Array.make reify.count pform_true in @@ -464,55 +462,49 @@ module Make (Atom:ATOM) = (** [interp_atom] map [Atom.t] to coq term, it is better if it produce shared terms. *) let interp_to_coq interp_atom form_tbl f = - let rec interp_form f = + let rec interp_form f = let l = to_lit f in - try Hashtbl.find form_tbl l + try Hashtbl.find form_tbl l with Not_found -> - if is_neg f then - let pc = interp_form (neg f) in - let nc = mklApp cnegb [|pc|] in - Hashtbl.add form_tbl l nc; - nc - else - let pc = - match pform f with - | Fatom a -> interp_atom a - | Fapp(op, args) -> - match op with - | Ftrue -> Lazy.force ctrue - | Ffalse -> Lazy.force cfalse - | Fand -> interp_args candb args - | For -> interp_args corb args - | Fxor -> interp_args cxorb args - | Fimp -> - let r = ref (interp_form args.(Array.length args - 1)) in - for i = Array.length args - 2 downto 0 do - r := mklApp cimplb [|interp_form args.(i); !r|] - done; - !r - | Fiff -> interp_args ceqb args - | Fite -> - (* TODO with if here *) - mklApp cifb (Array.map interp_form args) - | Fnot2 n -> - let r = ref (interp_form args.(0)) in - for i = 1 to n do r := mklApp cnegb [|!r|] done; - !r in - Hashtbl.add form_tbl l pc; - pc + if is_neg f then + let pc = interp_form (neg f) in + let nc = mklApp cnegb [|pc|] in + Hashtbl.add form_tbl l nc; + nc + else + let pc = + match pform f with + | Fatom a -> interp_atom a + | Fapp(op, args) -> + match op with + | Ftrue -> Lazy.force ctrue + | Ffalse -> Lazy.force cfalse + | Fand -> interp_args candb args + | For -> interp_args corb args + | Fxor -> interp_args cxorb args + | Fimp -> + let r = ref (interp_form args.(Array.length args - 1)) in + for i = Array.length args - 2 downto 0 do + r := mklApp cimplb [|interp_form args.(i); !r|] + done; + !r + | Fiff -> interp_args ceqb args + | Fite -> + (* TODO with if here *) + mklApp cifb (Array.map interp_form args) + | Fnot2 n -> + let r = ref (interp_form args.(0)) in + for i = 1 to n do + r := mklApp cnegb [|!r|] + done; + !r in + Hashtbl.add form_tbl l pc; + pc and interp_args op args = let r = ref (interp_form args.(0)) in - for i = 1 to Array.length args - 1 do - r := mklApp op [|!r;interp_form args.(i)|] - done; - !r in - interp_form f - - end - - - - - - - + for i = 1 to Array.length args - 1 do + r := mklApp op [|!r;interp_form args.(i)|] + done; + !r in + interp_form f +end diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli index 2a00228..c372bf5 100644 --- a/src/trace/smtForm.mli +++ b/src/trace/smtForm.mli @@ -37,7 +37,6 @@ type fop = | Fiff | Fite | Fnot2 of int - type ('a,'f) gen_pform = | Fatom of 'a @@ -73,7 +72,7 @@ module type FORM = (** Given a coq term, build the corresponding formula *) val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t - + (** Flattening of [Fand] and [For], removing of [Fnot2] *) val flatten : reify -> t -> t diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml index 4815a77..96d5f0f 100644 --- a/src/trace/smtTrace.ml +++ b/src/trace/smtTrace.ml @@ -20,7 +20,7 @@ open SmtCertif let notUsed = 0 -let next_id = ref 0 +let next_id = ref 0 let clear () = next_id := 0 @@ -31,7 +31,7 @@ let next_id () = (** Basic functions over small certificates *) -let mk_scertif kind ov = +let mk_scertif kind ov = { id = next_id (); kind = kind; @@ -39,13 +39,13 @@ let mk_scertif kind ov = used = notUsed; prev = None; next = None; - value = ov + value = ov } - + (** Roots *) -let mkRootGen ov = +let mkRootGen ov = let pos = next_id () in { id = pos; @@ -54,17 +54,17 @@ let mkRootGen ov = used = notUsed; prev = None; next = None; - value = ov + value = ov } (* let mkRoot = mkRootGen None *) let mkRootV v = mkRootGen (Some v) - -let isRoot k = k == Root + +let isRoot k = k == Root (** Resolutions *) -let mkRes c1 c2 tl = +let mkRes c1 c2 tl = mk_scertif (Res { rc1 = c1; rc2 = c2; rtail = tl }) None let isRes k = @@ -141,7 +141,7 @@ let rec get_pos c = | Some n -> n | _ -> assert false end - | Same c -> get_pos c + | Same c -> get_pos c let eq_clause c1 c2 = (repr c1).id = (repr c2).id @@ -154,49 +154,46 @@ let select c = while not (isRoot !r.kind) do let p = prev !r in (match !r.kind with - | Res res -> - if !r.used == 1 then begin - !r.used <- notUsed; - (* let res = get_res !r "select" in *) - mark res.rc1; mark res.rc2; - List.iter mark res.rtail - end else - skip !r; - | Same _ -> + | Res res -> + if !r.used == 1 then begin + !r.used <- notUsed; + (* let res = get_res !r "select" in *) + mark res.rc1; mark res.rc2; + List.iter mark res.rtail + end else + skip !r; + | Same _ -> skip !r - | _ -> - if !r.used == 1 then - begin - !r.used <- notUsed; - let rl = get_other !r "select" in - List.iter mark (used_clauses rl) - end - else skip !r; + | _ -> + if !r.used == 1 then + begin + !r.used <- notUsed; + let rl = get_other !r "select" in + List.iter mark (used_clauses rl) + end + else skip !r; ); r := p done - (* Compute the number of occurence of each_clause *) - let rec occur c = match c.kind with | Root -> c.used <- c.used + 1 | Res res -> - if c.used == notUsed then + if c.used == notUsed then begin occur res.rc1; occur res.rc2; List.iter occur res.rtail end; c.used <- c.used + 1 | Other res -> - if c.used == notUsed then List.iter occur (used_clauses res); - c.used <- c.used + 1; + if c.used == notUsed then List.iter occur (used_clauses res); + c.used <- c.used + 1; | Same c' -> occur c'; c.used <- c.used + 1 -(* Allocate clause *) - +(* Allocate clauses *) let alloc c = let free_pos = ref [] in @@ -211,12 +208,12 @@ let alloc c = done; (* r is the first clause defined by resolution or another rule, - normaly the first used *) + normally the first used *) let last_set = ref (get_pos (prev !r)) in let decr_clause c = let rc = repr c in - assert (rc.used > notUsed); + assert (rc.used > notUsed); rc.used <- rc.used - 1; if rc.used = notUsed then free_pos := get_pos rc :: !free_pos in @@ -231,14 +228,14 @@ let alloc c = while !r.next <> None do let n = next !r in - assert (!r.used <> notUsed); + assert (!r.used <> notUsed); if isRes !r.kind then decr_res (get_res !r "alloc") else decr_other (get_other !r "alloc"); begin match !free_pos with - | p::free -> free_pos := free; !r.pos <- Some p - | _ -> incr last_set; !r.pos <- Some !last_set + | p::free -> free_pos := free; !r.pos <- Some p + | _ -> incr last_set; !r.pos <- Some !last_set end; r := n done; @@ -277,8 +274,8 @@ let build_certif first_root confl = let to_coq to_lit interp (cstep, cRes, cImmFlatten, cTrue, cFalse, cBuildDef, cBuildDef2, cBuildProj, - cImmBuildProj,cImmBuildDef,cImmBuildDef2, - cEqTr, cEqCgr, cEqCgrP, + cImmBuildProj,cImmBuildDef,cImmBuildDef2, + cEqTr, cEqCgr, cEqCgrP, cLiaMicromega, cLiaDiseq, cSplArith, cSplDistinctElim, cHole) confl = @@ -288,7 +285,7 @@ let to_coq to_lit interp (cstep, let out_c c = mkInt (get_pos c) in let step_to_coq c = match c.kind with - | Res res -> + | Res res -> let size = List.length res.rtail + 3 in let args = Array.make size (mkInt 0) in args.(0) <- mkInt (get_pos res.rc1); @@ -296,10 +293,10 @@ let to_coq to_lit interp (cstep, let l = ref res.rtail in for i = 2 to size - 2 do match !l with - | c::tl -> + | c::tl -> args.(i) <- mkInt (get_pos c); l := tl - | _ -> assert false + | _ -> assert false done; mklApp cRes [|mkInt (get_pos c); Structures.mkArray (Lazy.force cint, args)|] | Other other -> @@ -346,7 +343,7 @@ let to_coq to_lit interp (cstep, end | _ -> assert false in let step = Lazy.force cstep in - let def_step = + let def_step = mklApp cRes [|mkInt 0; Structures.mkArray (Lazy.force cint, [|mkInt 0|]) |] in let r = ref confl in let nc = ref 0 in @@ -382,13 +379,13 @@ let to_coq to_lit interp (cstep, (** Optimization of the trace *) -module MakeOpt (Form:SmtForm.FORM) = - struct +module MakeOpt (Form:SmtForm.FORM) = + struct (* Share the certificate building a common clause *) let share_value c = let tbl = Hashtbl.create 17 in let to_lits v = List.map (Form.to_lit) v in - let process c = + let process c = match c.value with | None -> () | Some v -> @@ -401,7 +398,7 @@ module MakeOpt (Form:SmtForm.FORM) = while !r.next <> None do let next = next !r in process !r; - r := next + r := next done; process !r @@ -430,7 +427,7 @@ module MakeOpt (Form:SmtForm.FORM) = if eq_clause c1 c2 then aux (repr c1 :: rhd) tl1' tl2' else List.rev rhd, tl1, tl2 in aux [] tl1 tl2 - + let share_prefix first_c n = let tbl = HRtbl.create (min n Sys.max_array_length) in let rec share c2 = diff --git a/src/verit/verit.ml b/src/verit/verit.ml index e7ad9b1..643ce8f 100644 --- a/src/verit/verit.ml +++ b/src/verit/verit.ml @@ -53,10 +53,10 @@ let import_trace filename first = raise VeritLexer.Eof with | VeritLexer.Eof -> - close_in chan; - let first = - let aux = VeritSyntax.get_clause !first_num in - match first, aux.value with + close_in chan; + let first = + let aux = VeritSyntax.get_clause !first_num in + match first, aux.value with | Some (root,l), Some (fl::nil) -> if Form.equal l fl then aux @@ -132,17 +132,16 @@ let call_verit rt ro fl root = let (filename, outchan) = Filename.open_temp_file "verit_coq" ".smt2" in export outchan rt ro fl; close_out outchan; - let logfilename = (Filename.chop_extension filename)^".vtlog" in - - let command = "veriT --proof-prune --proof-merge --proof-with-sharing --cnf-definitional --disable-ackermann --input=smtlib2 --proof="^logfilename^" "^filename in + let logfilename = Filename.chop_extension filename ^ ".vtlog" in + let command = "veriT --proof-prune --proof-merge --proof-with-sharing --cnf-definitional --disable-ackermann --input=smtlib2 --proof=" ^ logfilename ^ " " ^ filename in Format.eprintf "%s@." command; let t0 = Sys.time () in let exit_code = Sys.command command in let t1 = Sys.time () in Format.eprintf "Verit = %.5f@." (t1-.t0); if exit_code <> 0 then - failwith ("Verit.call_verit: command "^command^ - " exited with code "^(string_of_int exit_code)); + failwith ("Verit.call_verit: command " ^ command ^ + " exited with code " ^ string_of_int exit_code); try import_trace logfilename (Some root) with diff --git a/src/verit/verit.mli b/src/verit/verit.mli index 3741339..126a02b 100644 --- a/src/verit/verit.mli +++ b/src/verit/verit.mli @@ -21,7 +21,8 @@ val theorem : Names.identifier -> string -> string -> unit val checker : string -> string -> unit val export : out_channel -> - SmtAtom.Btype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Form.t -> unit + SmtAtom.Btype.reify_tbl -> SmtAtom.Op.reify_tbl -> + SmtAtom.Form.t -> unit val call_verit : SmtAtom.Btype.reify_tbl -> SmtAtom.Op.reify_tbl -> diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml index 07a8a74..e03cbec 100644 --- a/src/verit/veritSyntax.ml +++ b/src/verit/veritSyntax.ml @@ -31,32 +31,34 @@ type typ = | Inpu | Deep | True | Fals | Andp | Andn | Orp | Orn | Xorp1 | Xorp2 let get_eq l = match Form.pform l with - | Fatom ha -> - (match Atom.atom ha with - | Abop (BO_eq _,a,b) -> (a,b) - | _ -> failwith "VeritSyntax.get_eq: equality was expected") - | _ -> failwith "VeritSyntax.get_eq: equality was expected" + | Fatom ha -> + (match Atom.atom ha with + | Abop (BO_eq _,a,b) -> (a,b) + | _ -> failwith "VeritSyntax.get_eq: equality was expected") + | _ -> failwith "VeritSyntax.get_eq: equality was expected" let get_at l = match Form.pform l with - | Fatom ha -> ha - | _ -> failwith "VeritSyntax.get_eq: equality was expected" + | Fatom ha -> ha + | _ -> failwith "VeritSyntax.get_eq: equality was expected" let is_eq l = match Form.pform l with - | Fatom ha -> - (match Atom.atom ha with - | Abop (BO_eq _,_,_) -> true - | _ -> false) - | _ -> failwith "VeritSyntax.get_eq: atom was expected" + | Fatom ha -> + (match Atom.atom ha with + | Abop (BO_eq _,_,_) -> true + | _ -> false) + | _ -> failwith "VeritSyntax.get_eq: atom was expected" (* Transitivity *) -let rec list_find_remove p l = - match l with - | [] -> raise Not_found - | t::q -> if p t then (t,q) else let (a,l) = list_find_remove p q in (a,t::l) +let rec list_find_remove p = function + [] -> raise Not_found + | h::t -> if p h + then h, t + else let (a, rest) = list_find_remove p t in + a, h::rest let rec process_trans a b prem res = if List.length prem = 0 then ( @@ -75,77 +77,77 @@ let rec process_trans a b prem res = let mkTrans p = let (concl,prem) = List.partition Form.is_pos p in match concl with - |[c] -> - let a,b = get_eq c in - let prem_val = List.map (fun l -> (l,get_eq l)) prem in - let cert = (process_trans a b prem_val []) in - Other (EqTr (c,cert)) - |_ -> failwith "VeritSyntax.mkTrans: no conclusion or more than one conclusion in transitivity" + |[c] -> + let a,b = get_eq c in + let prem_val = List.map (fun l -> (l,get_eq l)) prem in + let cert = (process_trans a b prem_val []) in + Other (EqTr (c,cert)) + |_ -> failwith "VeritSyntax.mkTrans: no conclusion or more than one conclusion in transitivity" (* Congruence *) let rec process_congr a_args b_args prem res = match a_args,b_args with - | a::a_args,b::b_args -> - (* if a = b *) - (* then process_congr a_args b_args prem (None::res) *) - (* else *) - let (l,(a',b')) = List.find (fun (l,(a',b')) -> ((Atom.equal a a') && (Atom.equal b b'))||((Atom.equal a b') && (Atom.equal b a'))) prem in - process_congr a_args b_args prem ((Some l)::res) - | [],[] -> List.rev res - | _ -> failwith "VeritSyntax.process_congr: incorrect number of arguments in function application" + | a::a_args,b::b_args -> + (* if a = b *) + (* then process_congr a_args b_args prem (None::res) *) + (* else *) + let (l,(a',b')) = List.find (fun (l,(a',b')) -> ((Atom.equal a a') && (Atom.equal b b'))||((Atom.equal a b') && (Atom.equal b a'))) prem in + process_congr a_args b_args prem ((Some l)::res) + | [],[] -> List.rev res + | _ -> failwith "VeritSyntax.process_congr: incorrect number of arguments in function application" let mkCongr p = let (concl,prem) = List.partition Form.is_pos p in match concl with - |[c] -> - let a,b = get_eq c in - let prem_val = List.map (fun l -> (l,get_eq l)) prem in - (match Atom.atom a, Atom.atom b with - | Abop(aop,a1,a2), Abop(bop,b1,b2) when (aop = bop) -> - let a_args = [a1;a2] in - let b_args = [b1;b2] in - let cert = process_congr a_args b_args prem_val [] in - Other (EqCgr (c,cert)) - | Auop (aop,a), Auop (bop,b) when (aop = bop) -> - let a_args = [a] in - let b_args = [b] in - let cert = process_congr a_args b_args prem_val [] in + |[c] -> + let a,b = get_eq c in + let prem_val = List.map (fun l -> (l,get_eq l)) prem in + (match Atom.atom a, Atom.atom b with + | Abop(aop,a1,a2), Abop(bop,b1,b2) when (aop = bop) -> + let a_args = [a1;a2] in + let b_args = [b1;b2] in + let cert = process_congr a_args b_args prem_val [] in + Other (EqCgr (c,cert)) + | Auop (aop,a), Auop (bop,b) when (aop = bop) -> + let a_args = [a] in + let b_args = [b] in + let cert = process_congr a_args b_args prem_val [] in + Other (EqCgr (c,cert)) + | Aapp (a_f,a_args), Aapp (b_f,b_args) -> + if indexed_op_index a_f = indexed_op_index b_f then + let cert = process_congr (Array.to_list a_args) (Array.to_list b_args) prem_val [] in Other (EqCgr (c,cert)) - | Aapp (a_f,a_args), Aapp (b_f,b_args) -> - if indexed_op_index a_f = indexed_op_index b_f then - let cert = process_congr (Array.to_list a_args) (Array.to_list b_args) prem_val [] in - Other (EqCgr (c,cert)) - else failwith "VeritSyntax.mkCongr: left function is different from right fucntion" - | _, _ -> failwith "VeritSyntax.mkCongr: atoms are not applications") - |_ -> failwith "VeritSyntax.mkCongr: no conclusion or more than one conclusion in congruence" + else failwith "VeritSyntax.mkCongr: left function is different from right fucntion" + | _, _ -> failwith "VeritSyntax.mkCongr: atoms are not applications") + |_ -> failwith "VeritSyntax.mkCongr: no conclusion or more than one conclusion in congruence" let mkCongrPred p = let (concl,prem) = List.partition Form.is_pos p in let (prem,prem_P) = List.partition is_eq prem in match concl with - |[c] -> - (match prem_P with - |[p_p] -> - let prem_val = List.map (fun l -> (l,get_eq l)) prem in - (match Atom.atom (get_at c), Atom.atom (get_at p_p) with - | Abop(aop,a1,a2), Abop(bop,b1,b2) when (aop = bop) -> - let a_args = [a1;a2] in - let b_args = [b1;b2] in - let cert = process_congr a_args b_args prem_val [] in - Other (EqCgrP (p_p,c,cert)) - | Aapp (a_f,a_args), Aapp (b_f,b_args) -> - if indexed_op_index a_f = indexed_op_index b_f then - let cert = process_congr (Array.to_list a_args) (Array.to_list b_args) prem_val [] in - Other (EqCgrP (p_p,c,cert)) - else failwith "VeritSyntax.mkCongrPred: unmatching predicates" - | _ -> failwith "VeritSyntax.mkCongrPred : not pred app") - |_ -> failwith "VeritSyntax.mkCongr: no or more than one predicate app premise in congruence") - |[] -> failwith "VeritSyntax.mkCongrPred: no conclusion in congruence" - |_ -> failwith "VeritSyntax.mkCongrPred: more than one conclusion in congruence" + |[c] -> + (match prem_P with + |[p_p] -> + let prem_val = List.map (fun l -> (l,get_eq l)) prem in + (match Atom.atom (get_at c), Atom.atom (get_at p_p) with + | Abop(aop,a1,a2), Abop(bop,b1,b2) when (aop = bop) -> + let a_args = [a1;a2] in + let b_args = [b1;b2] in + let cert = process_congr a_args b_args prem_val [] in + Other (EqCgrP (p_p,c,cert)) + | Aapp (a_f,a_args), Aapp (b_f,b_args) -> + if indexed_op_index a_f = indexed_op_index b_f then + let cert = process_congr (Array.to_list a_args) (Array.to_list b_args) prem_val [] in + Other (EqCgrP (p_p,c,cert)) + else failwith "VeritSyntax.mkCongrPred: unmatching predicates" + | _ -> failwith "VeritSyntax.mkCongrPred : not pred app") + |_ -> failwith "VeritSyntax.mkCongr: no or more than one predicate app premise in congruence") + |[] -> failwith "VeritSyntax.mkCongrPred: no conclusion in congruence" + |_ -> failwith "VeritSyntax.mkCongrPred: more than one conclusion in congruence" (* Linear arithmetic *) @@ -154,29 +156,29 @@ let mkMicromega cl = let _tbl, _f, cert = Lia.build_lia_certif cl in let c = match cert with - | None -> failwith "VeritSyntax.mkMicromega: micromega can't solve this" - | Some c -> c in + | None -> failwith "VeritSyntax.mkMicromega: micromega can't solve this" + | Some c -> c in Other (LiaMicromega (cl,c)) let mkSplArith orig cl = let res = match cl with - | res::nil -> res - | _ -> failwith "VeritSyntax.mkSplArith: wrong number of literals in the resulting clause" in + | res::nil -> res + | _ -> failwith "VeritSyntax.mkSplArith: wrong number of literals in the resulting clause" in try let orig' = match orig.value with - | Some [orig'] -> orig' - | _ -> failwith "VeritSyntax.mkSplArith: wrong number of literals in the premise clause" in + | Some [orig'] -> orig' + | _ -> failwith "VeritSyntax.mkSplArith: wrong number of literals in the premise clause" in let _tbl, _f, cert = Lia.build_lia_certif [Form.neg orig';res] in let c = match cert with - | None -> failwith "VeritSyntax.mkSplArith: micromega can't solve this" - | Some c -> c in + | None -> failwith "VeritSyntax.mkSplArith: micromega can't solve this" + | Some c -> c in Other (SplArith (orig,res,c)) with - | _ -> Other (ImmFlatten (orig, res)) + | _ -> Other (ImmFlatten (orig, res)) (* Elimination of operators *) @@ -184,8 +186,8 @@ let mkSplArith orig cl = let mkDistinctElim old value = let rec find_res l1 l2 = match l1,l2 with - | t1::q1,t2::q2 -> if t1 == t2 then find_res q1 q2 else t2 - | _, _ -> assert false in + | t1::q1,t2::q2 -> if t1 == t2 then find_res q1 q2 else t2 + | _, _ -> assert false in let l1 = match old.value with | Some l -> l | None -> assert false in @@ -204,108 +206,108 @@ let clear_clauses () = Hashtbl.clear clauses let mk_clause (id,typ,value,ids_params) = let kind = match typ with - (* Roots *) - | Inpu -> Root - (* Cnf conversion *) - | True -> Other SmtCertif.True - | Fals -> Other False - | Andn | Orp | Impp | Xorp1 | Xorn1 | Equp1 | Equn1 | Itep1 | Iten1 -> - (match value with - | l::_ -> Other (BuildDef l) - | _ -> assert false) - | Xorp2 | Xorn2 | Equp2 | Equn2 | Itep2 | Iten2 -> - (match value with - | l::_ -> Other (BuildDef2 l) - | _ -> assert false) - | Orn | Andp -> - (match value,ids_params with - | l::_, [p] -> Other (BuildProj (l,p)) - | _ -> assert false) - | Impn1 -> - (match value with - | l::_ -> Other (BuildProj (l,0)) - | _ -> assert false) - | Impn2 -> - (match value with - | l::_ -> Other (BuildProj (l,1)) - | _ -> assert false) - | Nand | Or | Imp | Xor1 | Nxor1 | Equ2 | Nequ2 | Ite1 | Nite1 -> - (match ids_params with - | [id] -> Other (ImmBuildDef (get_clause id)) - | _ -> assert false) - | Xor2 | Nxor2 | Equ1 | Nequ1 | Ite2 | Nite2 -> - (match ids_params with - | [id] -> Other (ImmBuildDef2 (get_clause id)) - | _ -> assert false) - | And | Nor -> - (match ids_params with - | [id;p] -> Other (ImmBuildProj (get_clause id,p)) - | _ -> assert false) - | Nimp1 -> - (match ids_params with - | [id] -> Other (ImmBuildProj (get_clause id,0)) - | _ -> assert false) - | Nimp2 -> - (match ids_params with - | [id] -> Other (ImmBuildProj (get_clause id,1)) - | _ -> assert false) - (* Equality *) - | Eqre -> mkTrans value - | Eqtr -> mkTrans value - | Eqco -> mkCongr value - | Eqcp -> mkCongrPred value - (* Linear integer arithmetic *) - | Dlge | Lage | Lata -> mkMicromega value - | Lade -> mkMicromega value (* TODO: utiliser un solveur plus simple *) - | Dlde -> - (match value with - | l::_ -> Other (LiaDiseq l) - | _ -> assert false) - (* Resolution *) - | Reso -> - (match ids_params with - | cl1::cl2::q -> - let res = {rc1 = get_clause cl1; rc2 = get_clause cl2; rtail = List.map get_clause q} in - Res res - | _ -> assert false) - (* Simplifications *) - | Tpal -> - (match ids_params with - | id::_ -> Same (get_clause id) - | _ -> assert false) - | Tple -> - (match ids_params with - | id::_ -> Same (get_clause id) - | _ -> assert false) - | Tpde -> - (match ids_params with - | id::_ -> mkDistinctElim (get_clause id) value - | _ -> assert false) - | Tpsa | Tlap -> - (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" - | Eins -> failwith "VeritSyntax.ml: rule exists_inst not implemented yet" - | Skea -> failwith "VeritSyntax.ml: rule skolem_ex_ax not implemented yet" - | Skaa -> failwith "VeritSyntax.ml: rule skolem_all_ax not implemented yet" - | Qnts -> failwith "VeritSyntax.ml: rule qnt_simplify_ax not implemented yet" - | Qntm -> failwith "VeritSyntax.ml: rule qnt_merge_ax not implemented yet" - | Tpne -> failwith "VeritSyntax.ml: rule tmp_nary_elim not implemented yet" - | Tpie -> failwith "VeritSyntax.ml: rule tmp_ite_elim not implemented yet" - | Tpma -> failwith "VeritSyntax.ml: rule tmp_macrosubst not implemented yet" - | Tpbr -> failwith "VeritSyntax.ml: rule tmp_betared not implemented yet" - | Tpbe -> failwith "VeritSyntax.ml: rule tmp_bfun_elim not implemented yet" - | Tpsc -> failwith "VeritSyntax.ml: rule tmp_sk_connector not implemented yet" - | Tppp -> failwith "VeritSyntax.ml: rule tmp_pm_process not implemented yet" - | Tpqt -> failwith "VeritSyntax.ml: rule tmp_qnt_tidy not implemented yet" - | Tpqs -> failwith "VeritSyntax.ml: rule tmp_qnt_simplify not implemented yet" - | Tpsk -> failwith "VeritSyntax.ml: rule tmp_skolemize not implemented yet" - | Subp -> failwith "VeritSyntax.ml: rule subproof not implemented yet" + (* Resolution *) + | Reso -> + (match ids_params with + | cl1::cl2::q -> + let res = {rc1 = get_clause cl1; rc2 = get_clause cl2; rtail = List.map get_clause q} in + Res res + | _ -> assert false) + (* Roots *) + | Inpu -> Root + (* Cnf conversion *) + | True -> Other SmtCertif.True + | Fals -> Other False + | Andn | Orp | Impp | Xorp1 | Xorn1 | Equp1 | Equn1 | Itep1 | Iten1 -> + (match value with + | l::_ -> Other (BuildDef l) + | _ -> assert false) + | Xorp2 | Xorn2 | Equp2 | Equn2 | Itep2 | Iten2 -> + (match value with + | l::_ -> Other (BuildDef2 l) + | _ -> assert false) + | Orn | Andp -> + (match value,ids_params with + | l::_, [p] -> Other (BuildProj (l,p)) + | _ -> assert false) + | Impn1 -> + (match value with + | l::_ -> Other (BuildProj (l,0)) + | _ -> assert false) + | Impn2 -> + (match value with + | l::_ -> Other (BuildProj (l,1)) + | _ -> assert false) + | Nand | Or | Imp | Xor1 | Nxor1 | Equ2 | Nequ2 | Ite1 | Nite1 -> + (match ids_params with + | [id] -> Other (ImmBuildDef (get_clause id)) + | _ -> assert false) + | Xor2 | Nxor2 | Equ1 | Nequ1 | Ite2 | Nite2 -> + (match ids_params with + | [id] -> Other (ImmBuildDef2 (get_clause id)) + | _ -> assert false) + | And | Nor -> + (match ids_params with + | [id;p] -> Other (ImmBuildProj (get_clause id,p)) + | _ -> assert false) + | Nimp1 -> + (match ids_params with + | [id] -> Other (ImmBuildProj (get_clause id,0)) + | _ -> assert false) + | Nimp2 -> + (match ids_params with + | [id] -> Other (ImmBuildProj (get_clause id,1)) + | _ -> assert false) + (* Equality *) + | Eqre -> mkTrans value + | Eqtr -> mkTrans value + | Eqco -> mkCongr value + | Eqcp -> mkCongrPred value + (* Linear integer arithmetic *) + | Dlge | Lage | Lata -> mkMicromega value + | Lade -> mkMicromega value (* TODO: utiliser un solveur plus simple *) + | Dlde -> + (match value with + | l::_ -> Other (LiaDiseq l) + | _ -> assert false) + (* Simplifications *) + | Tpal -> + (match ids_params with + | id::_ -> Same (get_clause id) + | _ -> assert false) + | Tple -> + (match ids_params with + | id::_ -> Same (get_clause id) + | _ -> assert false) + | Tpde -> + (match ids_params with + | id::_ -> mkDistinctElim (get_clause id) value + | _ -> assert false) + | Tpsa | Tlap -> + (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" + | Eins -> failwith "VeritSyntax.ml: rule exists_inst not implemented yet" + | Skea -> failwith "VeritSyntax.ml: rule skolem_ex_ax not implemented yet" + | Skaa -> failwith "VeritSyntax.ml: rule skolem_all_ax not implemented yet" + | Qnts -> failwith "VeritSyntax.ml: rule qnt_simplify_ax not implemented yet" + | Qntm -> failwith "VeritSyntax.ml: rule qnt_merge_ax not implemented yet" + | Tpne -> failwith "VeritSyntax.ml: rule tmp_nary_elim not implemented yet" + | Tpie -> failwith "VeritSyntax.ml: rule tmp_ite_elim not implemented yet" + | Tpma -> failwith "VeritSyntax.ml: rule tmp_macrosubst not implemented yet" + | Tpbr -> failwith "VeritSyntax.ml: rule tmp_betared not implemented yet" + | Tpbe -> failwith "VeritSyntax.ml: rule tmp_bfun_elim not implemented yet" + | Tpsc -> failwith "VeritSyntax.ml: rule tmp_sk_connector not implemented yet" + | Tppp -> failwith "VeritSyntax.ml: rule tmp_pm_process not implemented yet" + | Tpqt -> failwith "VeritSyntax.ml: rule tmp_qnt_tidy not implemented yet" + | Tpqs -> failwith "VeritSyntax.ml: rule tmp_qnt_simplify not implemented yet" + | Tpsk -> failwith "VeritSyntax.ml: rule tmp_skolemize not implemented yet" + | Subp -> failwith "VeritSyntax.ml: rule subproof not implemented yet" in let cl = (* TODO: change this into flatten when necessary *) diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml index 42e5792..8db91fd 100644 --- a/src/versions/native/structures.ml +++ b/src/versions/native/structures.ml @@ -60,7 +60,7 @@ let mkTrace step_to_coq next carray _ _ _ _ size step def_step r = if r1 <> 0 then ( let traceq = Array.make (r1 + 1) def_step in for i = 0 to r1-1 do - r := next !r; + r := next !r; traceq.(i) <- step_to_coq !r; done; trace.(q) <- mkArray (step, traceq) diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml index e7f842c..bfa1949 100644 --- a/src/zchaff/zchaff.ml +++ b/src/zchaff/zchaff.ml @@ -31,7 +31,7 @@ open SmtMisc let rec is_trivial cl = match cl with - | l :: cl -> + | l :: cl -> let nl = Form.neg l in List.exists (fun l' -> Form.equal nl l') cl || is_trivial cl | [] -> false @@ -50,19 +50,19 @@ let string_of_op = function | Fite -> "ite" | Fnot2 i -> "!"^string_of_int i -let rec pp_form fmt l = +let rec pp_form fmt l = Format.fprintf fmt "(#%i %a %a)" (Form.to_lit l)pp_sign l pp_pform (Form.pform l) -and pp_sign fmt l = - if Form.is_pos l then () +and pp_sign fmt l = + if Form.is_pos l then () else Format.fprintf fmt "-" -and pp_pform fmt p = +and pp_pform fmt p = match p with | Fatom x -> Format.fprintf fmt "x%i" x | Fapp(op,args) -> Format.fprintf fmt "%s" (string_of_op op); Array.iter (fun a -> Format.fprintf fmt "%a " pp_form a) args -let pp_value fmt c = +let pp_value fmt c = match c.value with | Some cl -> Format.fprintf fmt "VAL = {"; @@ -71,16 +71,16 @@ let pp_value fmt c = | _ -> Format.fprintf fmt "Val = empty@." -let pp_kind fmt c = +let pp_kind fmt c = match c.kind with | Root -> Format.fprintf fmt "Root" - | Res res -> + | Res res -> Format.fprintf fmt "(Res %i %i " res.rc1.id res.rc2.id; List.iter (fun c -> Format.fprintf fmt "%i " c.id) res.rtail; Format.fprintf fmt ") " | Other other -> begin match other with - | ImmFlatten (c,l) -> + | ImmFlatten (c,l) -> Format.fprintf fmt "(ImmFlatten %i %a)" c.id pp_form l | True -> Format.fprintf fmt "True" @@ -95,18 +95,18 @@ let pp_kind fmt c = end | Same c -> Format.fprintf fmt "(Same %i)" c.id -let rec pp_trace fmt c = +let rec pp_trace fmt c = Format.fprintf fmt "%i = %a %a" c.id pp_kind c pp_value c; if c.next <> None then pp_trace fmt (next c) (******************************************************************************) (** Given a cnf (dimacs) files and a resolve_trace build *) -(* the corresponding object *) +(* the corresponding object *) (******************************************************************************) -let import_cnf filename = +let import_cnf filename = let nvars, first, last = CnfParser.parse_cnf filename in let reloc = Hashtbl.create 17 in let count = ref 0 in @@ -140,7 +140,7 @@ let import_cnf_trace reloc filename first last = let make_roots first last = let cint = Lazy.force cint in let roots = Array.make (last.id + 2) (Structures.mkArray (cint, Array.make 1 (mkInt 0))) in - let mk_elem l = + let mk_elem l = let x = match Form.pform l with | Fatom x -> x + 2 | _ -> assert false in @@ -151,7 +151,7 @@ let make_roots first last = let croot = Array.make (Array.length root + 1) (mkInt 0) in Array.iteri (fun i l -> croot.(i) <- mk_elem l) root; roots.(!r.id) <- Structures.mkArray (cint, croot); - r := next !r + r := next !r done; let root = Array.of_list (get_val !r) in let croot = Array.make (Array.length root + 1) (mkInt 0) in @@ -162,13 +162,13 @@ let make_roots first last = let interp_roots first last = let tbl = Hashtbl.create 17 in - let mk_elem l = + let mk_elem l = let x = match Form.pform l with | Fatom x -> x | _ -> assert false in let ph = x lsl 1 in let h = if Form.is_pos l then ph else ph lxor 1 in - try Hashtbl.find tbl h + try Hashtbl.find tbl h with Not_found -> let p = Term.mkApp (Term.mkRel 1, [|mkInt (x+1)|]) in let np = mklApp cnegb [|p|] in @@ -178,8 +178,8 @@ let interp_roots first last = let interp_root c = match get_val c with | [] -> Lazy.force cfalse - | l :: cl -> - List.fold_left (fun acc l -> mklApp corb [|acc; mk_elem l|]) + | l :: cl -> + List.fold_left (fun acc l -> mklApp corb [|acc; mk_elem l|]) (mk_elem l) cl in let res = ref (interp_root first) in if first.id <> last.id then begin @@ -194,7 +194,7 @@ let interp_roots first last = let sat_checker_modules = [ ["SMTCoq";"Trace";"Sat_Checker"] ] let certif_ops = CoqTerms.make_certif_ops sat_checker_modules None -let cCertif = gen_constant sat_checker_modules "Certif" +let cCertif = gen_constant sat_checker_modules "Certif" let parse_certif dimacs trace fdimacs ftrace = SmtTrace.clear (); @@ -205,8 +205,8 @@ let parse_certif dimacs trace fdimacs ftrace = let max_id, confl = import_cnf_trace reloc ftrace first last in let (tres,_,_) = SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl in - let certif = - mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in + let certif = + mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in let ce2 = Structures.mkUConst certif in let _ = declare_constant trace (DefinitionEntry ce2, IsDefinition Definition) in () @@ -225,11 +225,11 @@ let theorems interp name fdimacs ftrace = let (tres,_,_) = SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl in let certif = - mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in + mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in let theorem_concl = mklApp cnot [|mklApp cis_true [|interp d first last|] |] in let vtype = Term.mkProd(Names.Anonymous, Lazy.force cint, Lazy.force cbool) in - let theorem_type = + let theorem_type = Term.mkProd (mkName "v", vtype, theorem_concl) in let theorem_proof_cast = Term.mkCast ( @@ -278,35 +278,35 @@ let checker fdimacs ftrace = - + (******************************************************************************) (** Given a Coq formula build the proof *) (******************************************************************************) let export_clause fmt cl = - List.iter - (fun l -> Format.fprintf fmt "%s%i " + List.iter + (fun l -> Format.fprintf fmt "%s%i " (if Form.is_pos l then "" else "-") (Form.index l + 1)) cl; Format.fprintf fmt "0@\n" let export out_channel nvars first = - let fmt = Format.formatter_of_out_channel out_channel in + let fmt = Format.formatter_of_out_channel out_channel in let reloc = Hashtbl.create 17 in let count = ref 0 in (* count the number of non trivial clause *) let r = ref first in - let add_count c = + let add_count c = match c.value with | Some cl -> if not (is_trivial cl) then incr count | _ -> () in while !r.next <> None do add_count !r; r := next !r done; add_count !r; Format.fprintf fmt "p cnf %i %i@." nvars !count; - count := 0; r := first; + count := 0; r := first; (* ouput clause *) - let out c = + let out c = match c.value with - | Some cl -> + | Some cl -> if not (is_trivial cl) then begin Hashtbl.add reloc !count c; incr count; @@ -326,21 +326,21 @@ let call_zchaff nvars root = let resfilename = (Filename.chop_extension filename)^".zlog" in let reloc, last = export outchan nvars root in close_out outchan; - let command = "zchaff "^filename^" > "^resfilename in + let command = "zchaff " ^ filename ^ " > " ^ resfilename in Format.eprintf "%s@." command; let t0 = Sys.time () in let exit_code = Sys.command command in let t1 = Sys.time () in - Format.eprintf "Zchaff = %.5f@." (t1-.t0); - if exit_code <> 0 then - failwith ("Zchaff.call_zchaff: command "^command^ - " exited with code "^(string_of_int exit_code)); - let logfilename = (Filename.chop_extension filename)^".log" in + Format.eprintf "Zchaff = %.5f@." (t1-.t0); + if exit_code <> 0 then + failwith ("Zchaff.call_zchaff: command " ^ command ^ + " exited with code " ^ (string_of_int exit_code)); + let logfilename = (Filename.chop_extension filename) ^ ".log" in let command2 = "mv resolve_trace "^logfilename in let exit_code2 = Sys.command command2 in - if exit_code2 <> 0 then - failwith ("Zchaff.call_zchaff: command "^command2^ - " exited with code "^(string_of_int exit_code2)); + if exit_code2 <> 0 then + failwith ("Zchaff.call_zchaff: command " ^ command2 ^ + " exited with code " ^ (string_of_int exit_code2)); (* import_cnf_trace reloc logfilename root last *) (reloc, resfilename, logfilename, last) @@ -350,16 +350,16 @@ let call_zchaff nvars root = let cnf_checker_modules = [ ["SMTCoq";"Trace";"Cnf_Checker"] ] let certif_ops = CoqTerms.make_certif_ops cnf_checker_modules None -let ccertif = gen_constant cnf_checker_modules "certif" -let cCertif = gen_constant cnf_checker_modules "Certif" -let cchecker_b_correct = - gen_constant cnf_checker_modules "checker_b_correct" -let cchecker_b = gen_constant cnf_checker_modules "checker_b" -let cchecker_eq_correct = - gen_constant cnf_checker_modules "checker_eq_correct" -let cchecker_eq = gen_constant cnf_checker_modules "checker_eq" - -let build_body reify_atom reify_form l b (max_id, confl) = +let ccertif = gen_constant cnf_checker_modules "certif" +let cCertif = gen_constant cnf_checker_modules "Certif" +let cchecker_b_correct = + gen_constant cnf_checker_modules "checker_b_correct" +let cchecker_b = gen_constant cnf_checker_modules "checker_b" +let cchecker_eq_correct = + gen_constant cnf_checker_modules "checker_eq_correct" +let cchecker_eq = gen_constant cnf_checker_modules "checker_eq" + +let build_body reify_atom reify_form l b (max_id, confl) = let ntvar = mkName "t_var" in let ntform = mkName "t_form" in let nc = mkName "c" in @@ -399,7 +399,7 @@ let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) = let (tres,_,_) = SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl in let certif = - mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in + mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in let vtvar = Term.mkRel 3 in let vtform = Term.mkRel 2 in let vc = Term.mkRel 1 in @@ -420,7 +420,7 @@ let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) = in (proof_cast, proof_nocast) -let get_arguments concl = +let get_arguments concl = let f, args = Term.decompose_app concl in match args with | [ty;a;b] when (Term.eq_constr f (Lazy.force ceq)) && (Term.eq_constr ty (Lazy.force cbool)) -> a, b @@ -490,8 +490,8 @@ let check_unsat filename = let make_proof pform_tbl atom_tbl env reify_form l = let fl = Form.flatten reify_form l in let root = SmtTrace.mkRootV [l] in - let _ = - if Form.equal l fl then Cnf.make_cnf reify_form root + let _ = + if Form.equal l fl then Cnf.make_cnf reify_form root else let first_c = SmtTrace.mkOther (ImmFlatten(root,fl)) (Some [fl]) in SmtTrace.link root first_c; @@ -532,7 +532,7 @@ let core_tactic env sigma t = let atom_tbl = Atom.atom_tbl reify_atom in let pform_tbl = Form.pform_tbl reify_form in let max_id_confl = make_proof pform_tbl atom_tbl (Environ.push_rel_context forall_let env) reify_form l' in - build_body reify_atom reify_form (Form.to_coq l) b max_id_confl + build_body reify_atom reify_form (Form.to_coq l) b max_id_confl else let l1 = Form.of_coq (Atom.get reify_atom) reify_form a in let l2 = Form.of_coq (Atom.get reify_atom) reify_form b in @@ -540,7 +540,7 @@ let core_tactic env sigma t = let atom_tbl = Atom.atom_tbl reify_atom in let pform_tbl = Form.pform_tbl reify_form in let max_id_confl = make_proof pform_tbl atom_tbl (Environ.push_rel_context forall_let env) reify_form l in - build_body_eq reify_atom reify_form + build_body_eq reify_atom reify_form (Form.to_coq l1) (Form.to_coq l2) (Form.to_coq l) max_id_confl in diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v index 33df78b..827dc4b 100644 --- a/unit-tests/Tests_verit.v +++ b/unit-tests/Tests_verit.v @@ -5,7 +5,6 @@ Require Import Bool PArray Int63 List ZArith. Local Open Scope int63_scope. - (* First a tactic, to test the universe computation in an empty environment. *) @@ -610,7 +609,7 @@ Qed. (* (a ∨ b ∨ c) ∧ (¬a ∨ ¬b ∨ ¬c) ∧ (¬a ∨ b) ∧ (¬b ∨ c) ∧ (¬c ∨ a) = ⊥ *) Goal forall a b c, - (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false. + (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false. Proof. verit. Qed. @@ -619,10 +618,10 @@ Qed. (* The same, but with a, b and c being 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. + 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. verit. Qed. @@ -783,7 +782,7 @@ Qed. (* lia1.smt *) Goal forall x y z, implb ((x <=? 3) && ((y <=? 7) || (z <=? 9))) - ((x + y <=? 10) || (x + z <=? 12)) = true. + ((x + y <=? 10) || (x + z <=? 12)) = true. Proof. verit. Qed. @@ -812,7 +811,7 @@ Qed. (* lia5.smt *) Goal forall x y, ((x + y <=? - (3)) && (y >=? 0) - || (x <=? - (3))) && (x >=? 0) = false. + || (x <=? - (3))) && (x >=? 0) = false. Proof. verit. Qed. @@ -860,15 +859,15 @@ Qed. (* With let ... in ... *) Goal forall b, - let a := b in - a && (negb a) = false. + let a := b in + a && (negb a) = false. Proof. verit. Qed. Goal forall b, - let a := b in - a || (negb a) = true. + let a := b in + a || (negb a) = true. Proof. verit. Qed. @@ -884,15 +883,15 @@ Qed. (* With concrete terms *) Goal forall i j, - let a := i == j in - a && (negb a) = false. + let a := i == j in + a && (negb a) = false. Proof. verit. Qed. Goal forall i j, - let a := i == j in - a || (negb a) = true. + let a := i == j in + a || (negb a) = true. Proof. verit. Qed. @@ -926,8 +925,8 @@ Proof. Qed. -(* +(* Local Variables: coq-load-path: ((rec "../src" "SMTCoq")) - End: + End: *) |