aboutsummaryrefslogtreecommitdiffstats
path: root/src/verit/veritSyntax.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/verit/veritSyntax.ml')
-rw-r--r--src/verit/veritSyntax.ml427
1 files changed, 278 insertions, 149 deletions
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index a45fb63..c4427b7 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -1,13 +1,9 @@
(**************************************************************************)
(* *)
(* SMTCoq *)
-(* Copyright (C) 2011 - 2016 *)
+(* Copyright (C) 2011 - 2019 *)
(* *)
-(* Michaël Armand *)
-(* Benjamin Grégoire *)
-(* Chantal Keller *)
-(* *)
-(* Inria - École Polytechnique - Université Paris-Sud *)
+(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
@@ -24,7 +20,8 @@ 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 | Hole
+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 | Weak | 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 | Flat | Hole | Bbva | Bbconst | Bbeq | Bbdis | Bbop | Bbadd | Bbmul | Bbult | Bbslt | Bbnot | Bbneg | Bbconc | Bbextr | Bbzext | Bbsext | Bbshl | Bbshr | Row1 | Row2 | Exte
+
(* About equality *)
@@ -194,6 +191,23 @@ let mkDistinctElim old value =
Other (SplDistinctElim (old,find_res l1 value))
+(* Clause difference (wrt to their sets of literals) *)
+
+let clause_diff c1 c2 =
+ let r =
+ List.filter (fun t1 -> not (List.exists (SmtAtom.Form.equal t1) c2)) c1
+ in
+ Format.eprintf "[";
+ List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) c1;
+ Format.eprintf "] -- [";
+ List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) c2;
+ Format.eprintf "] ==\n [";
+ List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) r;
+ Format.eprintf "] @.";
+ r
+
+
+
(* Generating clauses *)
let clauses : (int,Form.t clause) Hashtbl.t = Hashtbl.create 17
@@ -211,7 +225,7 @@ let add_ref i j = Hashtbl.add ref_cl i j
let clear_ref () = Hashtbl.clear ref_cl
(* Recognizing and modifying clauses depending on a forall_inst clause. *)
-
+
let rec fins_lemma ids_params =
match ids_params with
[] -> raise Not_found
@@ -222,9 +236,9 @@ let rec fins_lemma ids_params =
let rec find_remove_lemma lemma ids_params =
let eq_lemma h = eq_clause lemma (get_clause h) in
- list_find_remove eq_lemma ids_params
+ list_find_remove eq_lemma ids_params
-(* Removes the lemma in a list of ids containing an instance of this lemma *)
+(* Removes the lemma in a list of ids containing an instance of this lemma *)
let rec merge ids_params =
let rest_opt = try let lemma = fins_lemma ids_params in
let _, rest = find_remove_lemma lemma ids_params in
@@ -235,136 +249,237 @@ let rec merge ids_params =
| Some r -> merge r
let to_add = ref []
-
+
let rec mk_clause (id,typ,value,ids_params) =
let kind =
match typ with
- | Tpbr ->
- begin match ids_params with
- | [id] ->
- Same (get_clause id)
- | _ -> failwith "unexpected form of tmp_betared" end
- | Tpqt ->
- begin match ids_params with
- | [id] ->
- Same (get_clause id)
- | _ -> failwith "unexpected form of tmp_qnt_tidy" end
- | Fins ->
- begin match value, ids_params with
- | [inst], [ref_th] ->
- let cl_th = get_clause ref_th in
- Other (Forall_inst (repr cl_th, inst))
- | _ -> failwith "unexpected form of forall_inst" end
- | Or ->
- (match ids_params with
- | [id_target] ->
- let cl_target = get_clause id_target in
- begin match cl_target.kind with
- | Other (Forall_inst _) -> Same cl_target
- | _ -> Other (ImmBuildDef cl_target) end
- | _ -> assert false)
- (* Resolution *)
- | Reso ->
- let ids_params = merge ids_params in
- (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
- | [fins_id] -> Same (get_clause fins_id)
- | [] -> 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 | 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"
- | 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"
- | 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"
- | 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"
+ (* 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 | Imp | Xor1 | Nxor1 | Equ2 | Nequ2 | Ite1 | Nite1 ->
+ (match ids_params with
+ | [id] -> Other (ImmBuildDef (get_clause id))
+ | _ -> assert false)
+ | Or ->
+ (match ids_params with
+ | [id_target] ->
+ let cl_target = get_clause id_target in
+ begin match cl_target.kind with
+ | Other (Forall_inst _) -> Same cl_target
+ | _ -> Other (ImmBuildDef cl_target) end
+ | _ -> 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 ->
+ let ids_params = merge ids_params in
+ (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
+ | [fins_id] -> Same (get_clause fins_id)
+ | [] -> assert false)
+ (* Clause weakening *)
+ | Weak ->
+ (match ids_params with
+ | [id] -> (* Other (Weaken (get_clause id, value)) *)
+ let cid = get_clause id in
+ (match cid.value with
+ | None -> Other (Weaken (cid, value))
+ | Some c -> Other (Weaken (cid, value))
+ (* need to add c, otherwise dosen't terminate or returns false,
+ we would like instead: clause_diff value c *)
+ )
+ | _ -> 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)
+ | Flat ->
+ (match ids_params, value with
+ | id::_, f :: _ -> Other (ImmFlatten(get_clause id, f))
+ | _ -> assert false)
+ (* Bit blasting *)
+ | Bbva ->
+ (match value with
+ | [f] -> Other (BBVar f)
+ | _ -> assert false)
+ | Bbconst ->
+ (match value with
+ | [f] -> Other (BBConst f)
+ | _ -> assert false)
+ | Bbeq ->
+ (match ids_params, value with
+ | [id1;id2], [f] -> Other (BBEq (get_clause id1, get_clause id2, f))
+ | _, _ -> assert false)
+ | Bbdis ->
+ (match value with
+ | [f] -> Other (BBDiseq f)
+ | __ -> assert false)
+ | Bbop ->
+ (match ids_params, value with
+ | [id1;id2], [f] -> Other (BBOp (get_clause id1, get_clause id2, f))
+ | _, _ -> assert false)
+ | Bbadd ->
+ (match ids_params, value with
+ | [id1;id2], [f] -> Other (BBAdd (get_clause id1, get_clause id2, f))
+ | _, _ -> assert false)
+ | Bbmul ->
+ (match ids_params, value with
+ | [id1;id2], [f] -> Other (BBMul (get_clause id1, get_clause id2, f))
+ | _, _ -> assert false)
+ | Bbult ->
+ (match ids_params, value with
+ | [id1;id2], [f] -> Other (BBUlt (get_clause id1, get_clause id2, f))
+ | _, _ -> assert false)
+ | Bbslt ->
+ (match ids_params, value with
+ | [id1;id2], [f] -> Other (BBSlt (get_clause id1, get_clause id2, f))
+ | _, _ -> assert false)
+ | Bbconc ->
+ (match ids_params, value with
+ | [id1;id2], [f] ->
+ Other (BBConc (get_clause id1, get_clause id2, f))
+ | _, _ -> assert false)
+ | Bbextr ->
+ (match ids_params, value with
+ | [id], [f] -> Other (BBExtr (get_clause id, f))
+ | _, _ -> assert false)
+ | Bbzext ->
+ (match ids_params, value with
+ | [id], [f] -> Other (BBZextn (get_clause id, f))
+ | _, _ -> assert false)
+ | Bbsext ->
+ (match ids_params, value with
+ | [id], [f] -> Other (BBSextn (get_clause id, f))
+ | _, _ -> assert false)
+ | Bbshl ->
+ (match ids_params, value with
+ | [id1;id2], [f] -> Other (BBShl (get_clause id1, get_clause id2, f))
+ | _, _ -> assert false)
+ | Bbshr ->
+ (match ids_params, value with
+ | [id1;id2], [f] -> Other (BBShr (get_clause id1, get_clause id2, f))
+ | _, _ -> assert false)
+ | Bbnot ->
+ (match ids_params, value with
+ | [id], [f] -> Other (BBNot (get_clause id, f))
+ | _, _ -> assert false)
+ | Bbneg ->
+ (match ids_params, value with
+ | [id], [f] -> Other (BBNeg (get_clause id, f))
+ | _, _ -> assert false)
+
+ | Row1 ->
+ (match value with
+ | [f] -> Other (RowEq f)
+ | _ -> assert false)
+
+ | Exte ->
+ (match value with
+ | [f] -> Other (Ext f)
+ | _ -> assert false)
+
+ | Row2 -> Other (RowNeq value)
+
+ (* Holes in proofs *)
+ | Hole -> Other (SmtCertif.Hole (List.map get_clause ids_params, value))
+
+ (* Quantifier instanciation *)
+ | Fins ->
+ begin match value, ids_params with
+ | [inst], [ref_th] ->
+ let cl_th = get_clause ref_th in
+ Other (Forall_inst (repr cl_th, inst))
+ | _ -> failwith "unexpected form of forall_inst" end
+ | Tpbr ->
+ begin match ids_params with
+ | [id] ->
+ Same (get_clause id)
+ | _ -> failwith "unexpected form of tmp_betared" end
+ | Tpqt ->
+ begin match ids_params with
+ | [id] ->
+ Same (get_clause id)
+ | _ -> failwith "unexpected form of tmp_qnt_tidy" end
+
+ (* Not implemented *)
+ | Deep -> failwith "VeritSyntax.ml: rule deep_res 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"
+ | 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"
+ | 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 *)
@@ -375,6 +490,12 @@ let rec mk_clause (id,typ,value,ids_params) =
id
+let mk_clause cl =
+ try mk_clause cl
+ with Failure f ->
+ Structures.error ("SMTCoq was not able to check the certificate \
+ for the following reason.\n"^f)
+
type atom_form_lit =
| Atom of SmtAtom.Atom.t
| Form of SmtAtom.Form.pform
@@ -396,16 +517,23 @@ let rec list_dec = function
| (decl_h, h) :: t ->
let decl_t, l_t = list_dec t in
decl_h && decl_t, h :: l_t
-
-let apply_dec_atom f = function
- | decl, Atom h -> decl, Atom (f decl h)
+
+let apply_dec_atom (f:?declare:bool -> SmtAtom.hatom -> SmtAtom.hatom) = function
+ | decl, Atom h -> decl, Atom (f ~declare:decl h)
| _ -> assert false
-let apply_bdec_atom f o1 o2 =
+let apply_bdec_atom (f:?declare:bool -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t) o1 o2 =
match o1, o2 with
| (decl1, Atom h1), (decl2, Atom h2) ->
let decl = decl1 && decl2 in
- decl, Atom (f decl h1 h2)
+ decl, Atom (f ~declare:decl h1 h2)
+ | _ -> assert false
+
+let apply_tdec_atom (f:?declare:bool -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t) o1 o2 o3 =
+ match o1, o2, o3 with
+ | (decl1, Atom h1), (decl2, Atom h2), (decl3, Atom h3) ->
+ let decl = decl1 && decl2 && decl3 in
+ decl, Atom (f ~declare:decl h1 h2 h3)
| _ -> assert false
@@ -428,6 +556,7 @@ let get_fun id =
try Hashtbl.find funs id
with | Not_found -> failwith ("VeritSyntax.get_fun : function symbol \""^id^"\" not found\n")
let add_fun id cl = Hashtbl.add funs id cl
+let remove_fun id = Hashtbl.remove funs id
let clear_funs () = Hashtbl.clear funs
let qvar_tbl : (string, SmtBtype.btype) Hashtbl.t = Hashtbl.create 10
@@ -436,9 +565,9 @@ let find_opt_qvar s = try Some (Hashtbl.find qvar_tbl s)
let add_qvar s bt = Hashtbl.add qvar_tbl s bt
let clear_qvar () = Hashtbl.clear qvar_tbl
-let string_hform = Form.to_string ~pi:true (Atom.to_string ~pi:true )
+let hform_to_smt = Form.to_smt ~pi:true Atom.to_smt
-(* Finding the index of a root in <lsmt> modulo the <re_hash> function.
+(* Finding the index of a root in <lsmt> modulo the <re_hash> function.
This function is used by SmtTrace.order_roots *)
let init_index lsmt re_hash =
let form_index_init_rank : (int, int) Hashtbl.t = Hashtbl.create 20 in
@@ -453,9 +582,9 @@ let init_index lsmt re_hash =
try find (Form.to_lit re_hf)
with Not_found ->
let oc = open_out "/tmp/input_not_found.log" in
- (List.map string_hform lsmt)
- |> List.iter (Printf.fprintf oc "%s\n");
- Printf.fprintf oc "\n%s\n" (string_hform re_hf);
+ let fmt = Format.formatter_of_out_channel oc in
+ List.iter (fun h -> Format.fprintf fmt "%a\n" hform_to_smt h) lsmt;
+ Format.fprintf fmt "\n%a\n" hform_to_smt re_hf;
flush oc; close_out oc;
failwith "not found: log available"
@@ -469,7 +598,7 @@ let qf_to_add lr =
(Other (Qf_lemma (r, l)), r.value, r) :: qf_lemmas t
| _::t -> qf_lemmas t in
qf_lemmas lr
-
+
let ra = Atom.create ()
let rf = Form.create ()
let ra' = Atom.create ()
@@ -477,7 +606,7 @@ let rf' = Form.create ()
let hlets : (string, atom_form_lit) Hashtbl.t = Hashtbl.create 17
-let clear_mk_clause () =
+let clear_mk_clause () =
to_add := [];
clear_ref ()
generated by cgit (git 2.34.1) at 2024-06-29 00:15:11 +0000