diff options
-rw-r--r-- | src/verit/veritSyntax.ml | 16 | ||||
-rw-r--r-- | src/versions/standard/structures.ml | 4 | ||||
-rw-r--r-- | unit-tests/Tests_verit.v | 6 |
3 files changed, 13 insertions, 13 deletions
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml index c60d34f..3ff11e9 100644 --- a/src/verit/veritSyntax.ml +++ b/src/verit/veritSyntax.ml @@ -55,14 +55,14 @@ let is_eq l = let rec process_trans a b prem res = try - let (l,(c,c')) = List.find (fun (l,(a',b')) -> (a' = b || b' = b)) prem in - let prem = List.filter (fun l' -> l' <> (l,(c,c'))) prem in - let c = if c = b then c' else c in - if a = c + let (l,(c,c')) = List.find (fun (l,(a',b')) -> ((Atom.equal a' b) || (Atom.equal b' b))) prem in + let prem = List.filter (fun (l',(d,d')) -> (not (Form.equal l' l)) || (not (Atom.equal d c)) || (not (Atom.equal d' c'))) prem in + let c = if Atom.equal c b then c' else c in + if Atom.equal a c then List.rev (l::res) else process_trans a c prem (l::res) with - |Not_found -> if a = b then [] else assert false + |Not_found -> if Atom.equal a b then [] else assert false let mkTrans p = @@ -84,7 +84,7 @@ let rec process_congr a_args b_args prem res = (* if a = b *) (* then process_congr a_args b_args prem (None::res) *) (* else *) - let (l,(a',b')) = List.find (fun (l,(a',b')) -> (a = a' && b = b')||(a = b' && b = a')) prem in + 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" @@ -108,7 +108,7 @@ let mkCongr p = 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 a_f = b_f then + 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" @@ -131,7 +131,7 @@ let mkCongrPred p = 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 a_f = b_f then + 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" diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml index bd9e4f4..08451c9 100644 --- a/src/versions/standard/structures.ml +++ b/src/versions/standard/structures.ml @@ -85,11 +85,11 @@ let error = Errors.error let coqtype = Future.from_val Term.mkSet let declare_new_type t = - let _ = Command.declare_assumption false (Decl_kinds.Local, false, Decl_kinds.Definitional) (Future.force coqtype, Univ.ContextSet.empty) [] [] false Vernacexpr.NoInline (dummy_loc, t) in + let _ = Command.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Future.force coqtype, Univ.ContextSet.empty) [] [] false Vernacexpr.NoInline (dummy_loc, t) in Term.mkVar t let declare_new_variable v constr_t = - let _ = Command.declare_assumption false (Decl_kinds.Local, false, Decl_kinds.Definitional) (constr_t, Univ.ContextSet.empty) [] [] false Vernacexpr.NoInline (dummy_loc, v) in + let _ = Command.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Univ.ContextSet.empty) [] [] false Vernacexpr.NoInline (dummy_loc, v) in Term.mkVar v let extern_constr = Constrextern.extern_constr true Environ.empty_env Evd.empty diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v index 2be8752..53cb9fb 100644 --- a/unit-tests/Tests_verit.v +++ b/unit-tests/Tests_verit.v @@ -134,8 +134,8 @@ End Checker_Let2. Section Sat0. - Parse_certif_verit t_i1 t_func1 t_atom1 t_form1 root1 used_roots1 trace1 "sat1.smt2" "sat1.vtlog". - Compute Euf_Checker.checker t_i1 t_func1 t_atom1 t_form1 root1 used_roots1 trace1. + Parse_certif_verit t_i0 t_func0 t_atom0 t_form0 root0 used_roots0 trace0 "sat0.smt2" "sat0.vtlog". + Compute Euf_Checker.checker t_i0 t_func0 t_atom0 t_form0 root0 used_roots0 trace0. End Sat0. Section Sat1. @@ -287,7 +287,7 @@ End Let2. Section Theorem_Sat0. - Time Verit_Theorem theorem_sat1 "sat0.smt2" "sat0.vtlog". + Time Verit_Theorem theorem_sat0 "sat0.smt2" "sat0.vtlog". End Theorem_Sat0. Section Theorem_Sat1. |