From c5819f465abd97cb7257508155221e636cc9e1cd Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 11 Jan 2024 16:54:27 +0100 Subject: [PATCH] Partial documentation of SatML --- src/lib/reasoners/satml.ml | 235 ++++++++++++++++++++++++---- src/lib/reasoners/satml.mli | 5 + src/lib/reasoners/satml_frontend.ml | 16 +- src/lib/structures/expr.mli | 6 + src/lib/structures/satml_types.ml | 60 ++++++- src/lib/structures/satml_types.mli | 151 +++++++++++++++--- 6 files changed, 415 insertions(+), 58 deletions(-) diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index 986a772bd..1fe2bc3b1 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -78,8 +78,15 @@ exception Stopped type conflict_origin = | C_none + (* No conflict. *) + | C_bool of Atom.clause + (* Conflict found during the boolean constraint propagation with + its conflict clause. *) + | C_theory of Ex.t + (* Conflict found during the theory constraint propagation. + The explanation is returned by the theory reasoner. *) (* not even the final one *) let vraie_form = E.vrai @@ -182,32 +189,78 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct (* un vecteur des variables du probleme *) mutable vars : Atom.var Vec.t; - (* la pile de decisions avec les faits impliques *) mutable trail : Atom.atom Vec.t; + (** Stack of the assigned atoms. An atom [a] is assigned if [a.is_true] + is [true]. + + An assigned atom [a] is decided or propagated: + - [a] is decided if we choose it but there is no constraint which + forces it to be [true]. + - [a] is propaged if we discover that [a] as to be [true] because + of boolean/theory constraints. + + Both have a decision level stored in [a.var.level]. The decision level + of an atom [a] is set as follows: + - if [a] is the only atom of a learnt clause, its decision level + is [0]; + + - if [a] is propagated during the BCP, its decision level is: + * The current decision level if [Options.get_minimal_bj ()] is + [false]. + * Otherwise, its decision level is the maximal decision level of + the atoms of the unit clause that constraints [a] to be [true]; + + - if [a] is an atom of maximal decision level among the atoms of + a conflict clause [C] discovered during BCP and all the other + atoms of [C] have a lower decision level than [a], we revert + the assignation of [a] and [a.neg] is propagated with the + decision level given by the second maximal decision level in the + clause [C]; + + - if [a] is the first atom of a new learnt clause [C] + (of size at least 2), we immediatly propagate this atom with the + decision level equals to: + * The current decision level if [Options.get_minimal_bj ()] is + [false]. + * Otherwise, its decision level is the maximal decision level of + the atoms of [C]. + + Note: in this trail, atoms aren't ordered in increasing decision + level but decided atoms are in order. *) - (* une pile qui pointe vers les niveaux de decision dans trail *) mutable trail_lim : int Vec.t; + (* Stack of decision's indexes in trail. + + The length of this stack is the current decision level. *) (* Tete de la File des faits unitaires a propager. C'est un index vers le trail *) mutable qhead : int; - (* Nombre des assignements top-level depuis la derniere - execution de 'simplify()' *) mutable simpDB_assigns : int; + (** Size of the trail at decision level 0 since the last call of + [simplify]. *) (* Nombre restant de propagations a faire avant la prochaine execution de 'simplify()' *) mutable simpDB_props : int; - (* Un tas ordone en fonction de l'activite des variables *) mutable order : Vheap.t; + (* Priority queue used to choose the next variable to decide in + [search]. The priorities of variables are given by a heuristic + based on the activities of clauses using these variables. + + Notice that the underlying variables of guards aren't present in + this queue. Instead these variables are decided first. *) (* estimation de progressions, mis a jour par 'search()' *) mutable progress_estimate : float; - (* *) remove_satisfied : bool; + (** If this flag is set to [true], assumed clauses at decision level + [0] are removed. * + + Currently, this flag is always [true]. *) (* inverse du facteur d'acitivte des variables, vaut 1/0.999 par defaut *) var_decay : float; @@ -237,27 +290,31 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct mutable starts : int; - mutable decisions : int; - - mutable propagations : int; - mutable conflicts : int; + (** Number of conflicts found. This field is unread. *) mutable clauses_literals : int; + (** Sum of the size of all the assumed clauses. + The size of a clause is given by its number of literals. *) mutable learnts_literals : int; + (** Sum of the size of all the learnt clauses. + The size of a clause is given by its number of literals. *) mutable max_literals : int; mutable tot_literals : int; mutable nb_init_clauses : int; + (** Number of assumed clauses. *) mutable tenv : Th.t; mutable unit_tenv : Th.t; + (* TODO: rename to tenv_stack. *) mutable tenv_queue : Th.t Vec.t; + (** Stack of the environments of Theory. *) mutable tatoms_queue : Atom.atom Queue.t; (** Queue of atoms that have been added to the [trail] through either @@ -384,8 +441,24 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct solver. *) mutable increm_guards : Atom.atom Vec.t; + (** Stack of incremental guards. After each push, a new guard is added + to this stack and assigned with the current decision level. + All the formulas [f] assumed at this assertion level has to be + prefixed by the guard: [g ==> f]. + + If the corresponding pop is performed, the guard [g] is disactivate + (the field [g.is_guard] is set to [false]) and the the negation of + [g] is propagated. + + Finally, if the negation of [g] is propagated before beging + desactivate, it means some clause asserted at the assertion level + of [g] can't be satisfy and the problem is unsatisfiable at the + level of assertion. *) mutable next_dec_guard : int; + (** Index in the trail of the next unassigned guard. + This index is used to ensure that we decide all the guards before + choosing other variables in [search]. *) } exception Conflict of Atom.clause @@ -444,10 +517,6 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct starts = 0; - decisions = 0; - - propagations = 0; - conflicts = 0; clauses_literals = 0; @@ -522,15 +591,14 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct env.clause_inc <- env.clause_inc *. 1e-20 end - let decision_level env = Vec.size env.trail_lim + let[@inline always] decision_level env = Vec.size env.trail_lim - let nb_assigns env = Vec.size env.trail - let nb_clauses env = Vec.size env.clauses + let[@inline always] nb_assigns env = Vec.size env.trail + let[@inline always] nb_clauses env = Vec.size env.clauses (* unused -- let nb_learnts env = Vec.size env.learnts *) - let nb_vars env = Vec.size env.vars + let[@inline always] nb_vars env = Vec.size env.vars let new_decision_level env = - env.decisions <- env.decisions + 1; Vec.push env.trail_lim (Vec.size env.trail); if Options.get_profiling() then Profiling.decision (decision_level env) ""; @@ -659,6 +727,9 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct assert (Options.get_minimal_bj () || (!repush == [])); List.iter (enqueue_assigned env) !repush + (* Select the next unassigned variable with the highest priority. + + @raise Sat if there is no more unassigned atom. *) let rec pick_branch_var env = if Vheap.size env.order = 0 then raise Sat; let v = Vheap.remove_min env.order in @@ -671,6 +742,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct let pick_branch_lit env = if env.next_dec_guard < Vec.size env.increm_guards then begin + (* Guards are always choosen first. *) let a = Vec.get env.increm_guards env.next_dec_guard in (assert (not (a.neg.is_guard || a.neg.is_true))); env.next_dec_guard <- env.next_dec_guard + 1; @@ -698,14 +770,27 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct max_lvl := max !max_lvl a.var.level) c.atoms; !max_lvl + (* Push in the trail the atom [a] with decision level [lvl] and reason + [reason]. + + Requires: the atoms [a] and [a.neg] are unassigned. + Ensures: the atom [a] is assigned to [true]. + + @raise Unsat if we try to push the negation of a guard which is still + active. *) let enqueue env (a : Atom.atom) lvl reason = assert (not a.is_true && not a.neg.is_true && a.var.level < 0 && a.var.reason == None && lvl >= 0); if a.neg.is_guard then begin - (* if the negation of a is (still) a guard, it should be forced to true - during the first decisions. - If the SAT tries to deduce that a.neg is true (ie. a is false), - then we have detected an inconsistency. *) + (* If the negation [g = a.neg] of [a] is still an active guard and we try + to decide [a], it means that there is a clause [c] asserted at + assertion level of [g] which is false in current trail (and so the + clause [~g \/ c] is unit, which is the reason of the propagation of + [~g]). But active guards are decided first. Thus the only reason for + which [g] cannot be decided + But [c] is a part of the problem (at the current assertion + level) and has to be true to answer `Sat`. Otherwise, the problem is + unsatisfiable. *) assert (a.var.level <= env.next_dec_guard); (* guards are necessarily decided/propagated before all other atoms *) raise (Unsat None); @@ -795,6 +880,8 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct end with Exit -> () + (* Propagate the boolean constraints implied by assuming [a]. + If a contradiction is discovered, its reason is stored in [res]. *) let propagate_atom env (a : Atom.atom) res = let watched = a.watched in let new_sz_w = ref 0 in @@ -950,6 +1037,8 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct "expensive_theory_propagate => Inconsistent@."; *) (* Some dep *) + (* Propagate the atoms assigned at level [0] in [lazy_q] to + the theory environment [env.tenv]. *) let unit_theory_propagate env _full_q lazy_q = let nb_f = ref 0 in let facts = @@ -1057,6 +1146,16 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct if Options.get_profiling() then Profiling.theory_conflict(); C_theory dep + (* Perform all the boolean constraint propagations implied by assuming + atoms in the queue stored at the top of [env.trail] (the head of + this queue is given by [env.qhead]). + + If we found a contradiction, the BCP stops and a conflict clause is + returned. + + The theory constraint propagation isn't perfom here. Instead, these + atoms are stored in the queue [env.tatoms_queue], which is processed + in [theory_propagate]. *) let propagate env = let num_props = ref 0 in let res = ref C_none in @@ -1070,7 +1169,6 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct propagate_atom env a res; Queue.push a env.tatoms_queue; done; - env.propagations <- env.propagations + !num_props; env.simpDB_props <- env.simpDB_props - !num_props; !res @@ -1121,6 +1219,8 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct Vec.shrink env.learnts !j true *) + (* Helper function that removes all the clauses of [vec] that + are satisfied at the decision level [0] in the environment [env]. *) let remove_satisfied env vec = let j = ref 0 in for i = 0 to Vec.size vec - 1 do @@ -1278,6 +1378,8 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct | C_bool c -> C_bool c | C_theory _ -> assert false | C_none -> + (* We don't find contradiction during the BCP, thus we + can perform the TCP. *) if Options.get_tableaux_cdcl () then C_none else @@ -1292,14 +1394,21 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct | C_theory dep -> report_t_unsat env dep | C_none -> () + (* Simplify the clause database by removing some satisfied clauses at + the decision level [0]. Notice that these clauses can still appear in + watched lists of atoms but we ignore them during the BCP. *) let simplify env = assert (decision_level env = 0); if env.is_unsat then raise (Unsat env.unsat_core); - (* report possible propagation conflict *) - report_conflict env (all_propagations env); if nb_assigns env <> env.simpDB_assigns && env.simpDB_props <= 0 then begin if Options.get_debug_sat () then Printer.print_dbg ~module_name:"Satml" ~function_name:"simplify" ""; + (* Before simplifying the clause database, we have to ensure it doesn't + contain unreported conflicts for sake of soundness. As the function + [simplify] is always called after [propagate_and_stabilize], we don't + need to call [all_propagations] here but we keep this call to enforce + this important requirement. *) + report_conflict env (all_propagations env); (*theory_simplify ();*) if Vec.size env.learnts > 0 then remove_satisfied env env.learnts; if env.remove_satisfied then remove_satisfied env env.clauses; @@ -1335,6 +1444,15 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct clause_decay_activity env end + (* The clause [c_clause] is a conflict clause. More precisely, + [c_clause] is a unit clause whose the negation of the first atom + have been decided or propagated at the current decision level. + + where [max_lvl] is the maximal level of decision among the + atoms of the clause [c_clause]. + + @return [(blevel, learnt, history)] where + - [blevel] is the backtrack level *) let conflict_analyze_aux env c_clause max_lvl = let pathC = ref 0 in let learnt = ref SA.empty in @@ -1344,6 +1462,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct let c : Atom.clause ref = ref c_clause in let tr_ind = ref (Vec.size env.trail -1) in let history = ref [] in + (* This loop terminates the second times [pathC] is [0]. *) while !cond do if !c.learnt then clause_bump_activity env !c; history := !c :: !history; @@ -1390,6 +1509,16 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct in bj_level, learnt, !history + (* Search in [confl] an atom of maximal decision level [lvl] such that there + is no other atom in [confl] whose the decision level is [lvl]. + + If such an atom [a] exists, the function returns the tuple + [(a, blvl, snd_max)] where: + - [blvl] is a backjump level (equal to [lvl - 1] here); + - [snd_max] is the second maximal decision level in [confl]. + + @requires all the atom of [confl] are assigned to [false] + (it's a conflict clause!). *) let fixable_with_simple_backjump (confl : Atom.clause) max_lvl lv = if not (Options.get_minimal_bj ()) then None else @@ -1467,6 +1596,13 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct cancel_until env blevel; record_learnt_clause env ~is_T_learn:false blevel learnt history | Some (a, blevel, propag_lvl) -> + (* We found an atom [a] in the conflict clause [c] whose the + decision level is bigger than all the other atoms of this clause. + + In this case, we backjump just before the decision of [a.neg] + (given by the backjump level [blevel]) and we propagate the atom [a] + with the decision level given by the second maximum decision level + of [c]. *) assert (a.neg.is_true); cancel_until env blevel; assert (not a.neg.is_true); @@ -1489,10 +1625,17 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct *) + (* Strategies to choose the next decision. *) type strat = | Auto + (* In this mode, we use the activity-based heuristic to choose + the next decision. *) + | Stop + (* We stop the search process. *) + | Interactive of Atom.atom + (* We force the decision of this atom. *) let find_uip_reason q = let res = ref SA.empty in @@ -1554,6 +1697,9 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct end else raise e + (* Produce a clause of the form [fuip \/ ~a1 \/ ... \/ ~an] where + the [a_i] are all the literals assigned by the SAT solver and involved + in the explanation [d]. *) let clause_of_dep d fuip = let cpt = ref 0 in let l = @@ -1568,6 +1714,24 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct in fuip :: l, !cpt + 1 + (* Check if the atom [a] or its negation is entailed by the current theory + environment [tenv]. + + if [a] is entailed by [tenv], the function returns a new + tautological clause of the form: + a \/ ~a1 \/ ... \/ ~an + where [ai] are all the atoms assigned by the SAT solver and involved in + the explanation produced by the theory reasoner. + + In other words, the formula [a1 /\ ... /\ an ==> a] is first-order + tautological (it's true in any first-order model but the underlying + proposition formula isn't necessary a tautology). + + For instance, if the atom [a] is [x < z] and the theory environment + [tenv] contains the facts [x < y] and [y < z]. Then the tautological + implication + x < y /\ y < z => x < y + can be discovered by this mechanism. *) let th_entailed tenv a = if Options.get_no_tcp () || not (Options.get_minimal_bj ()) then None else @@ -1605,6 +1769,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct Vec.size env.learnts - nb_assigns env >= n_of_learnts then reduce_db(); + (* We get an appropriate candidate for the next decision. *) let next = match !strat with | Auto -> pick_branch_lit env @@ -1613,18 +1778,34 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct strat := Stop; f in + (* We first check if the [next] literal has to be true according to the + theory. It is an heuristic to accelerate the exploration of the + decision tree by avoiding to perform BCP whose the conclusion can + already be discovered by the theory. *) match th_entailed env.tenv next with | None -> new_decision_level env; let current_level = decision_level env in env.cpt_current_propagations <- 0; + (* The variable [next.var] aren't already assigned as [pick_branch_lit] + guarantees it. *) assert (next.var.level < 0); if Options.get_debug_sat () then Printer.print_dbg "[satml] decide: %a" Atom.pr_atom next; enqueue env next current_level None | Some(c, _) -> + (* We discover a first-order tautology [c] of the form + [a1 /\ ... /\ an => next] or [a1 /\ ... /\ an => ~next]. + In this case, we learn the clause [c] discovered thanks to the + theory reasoner. + + We don't need to decide [next] as it's entailed or it's negation + is entailed by the theory and learning [c] will propagate this atom + later (if we don't backtrack before). + + The right decision level will be set inside + [record_learnt_clause]. *) record_learnt_clause env ~is_T_learn:true (decision_level env) c [] - (* right decision level will be set inside record_learnt_clause *) done (* unused -- diff --git a/src/lib/reasoners/satml.mli b/src/lib/reasoners/satml.mli index 40b5e6503..eafc15b7f 100644 --- a/src/lib/reasoners/satml.mli +++ b/src/lib/reasoners/satml.mli @@ -87,6 +87,11 @@ module type SAT_ML = sig val do_case_split : t -> Util.case_split_policy -> conflict_origin val decide : t -> Atom.atom -> unit + (** [decide env a] forces the decision of the atom [a] in the environment + [env]. + + @raise Unsat if the environment is already unsatisfiable. *) + val conflict_analyze_and_fix : t -> conflict_origin -> unit val push : t -> Satml_types.Atom.atom -> unit diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 434e9617e..5e4ffaf07 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -44,7 +44,10 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct type guards = { mutable current_guard: E.t; + (* Top element of the stack [stack_guard]. *) + stack_guard: E.t Stack.t; + (* Stack of the incremental guards. *) } type t = { @@ -54,14 +57,23 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct mutable last_forced_normal : int; mutable last_forced_greedy : int; mutable gamma : (int * FF.t option) ME.t; + (** Stack of assumed flat formulas. *) + mutable conj : (int * SE.t) FF.Map.t; mutable abstr_of_axs : (FF.t * Atom.atom) ME.t; + (** Map a lemma to the abstract literal used to represent it in the flat + formulas. *) + mutable axs_of_abstr : (E.t * Atom.atom) ME.t; + (** Inverse map of [abstr_of_axs]. *) + mutable proxies : (Atom.atom * Atom.atom list * bool) Util.MI.t; mutable inst : Inst.t; mutable skolems : E.gformula ME.t; (* key <-> f *) add_inst : E.t -> bool; guards : guards; + (* Stack of the incremental guards. *) + mutable last_saved_model : Models.t Lazy.t option; mutable last_saved_objectives : Objective.Model.t option; mutable unknown_reason : Sat_solver_sig.unknown_reason option; @@ -496,7 +508,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let ded = match E.neg f |> E.form_view with | E.Skolem q -> E.skolemize q | E.Unit _ | E.Clause _ | E.Literal _ | E.Lemma _ - | E.Let _ | E.Iff _ | E.Xor _ -> assert false + | E.Let _ | E.Iff _ | E.Xor _ -> + (* *) + assert false in (*XXX TODO: internal skolems*) let f = E.mk_or lat ded false in diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index 8ca71acbc..a69f98a32 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -308,6 +308,12 @@ val skolemize : quantified -> t val elim_let : recursive:bool -> letin -> t val elim_iff : t -> t -> with_conj:bool -> t +(** [elim ~with_conj e1 e2] produces a formula equivalent to [f1 <==> f2]. + - If [with_conj] is [true], the internal formula is of the form: + [f1 ==> f2 /\ f2 ==> f1] + + - Otherwise, the internal formula is of the form: + [(f1 /\ f2) \/ (~f1 /\ ~f2)]. *) (*val purify_literal : t -> t*) val purify_form : t -> t diff --git a/src/lib/structures/satml_types.ml b/src/lib/structures/satml_types.ml index be3993cee..64473bfe8 100644 --- a/src/lib/structures/satml_types.ml +++ b/src/lib/structures/satml_types.ml @@ -289,7 +289,13 @@ module Atom : ATOM = struct module HT = Hashtbl.Make(E) - type hcons_env = { tbl : var HT.t ; cpt : int ref } + type hcons_env = { + tbl : var HT.t; + (** Hashtable of positive literals to their atom. *) + + cpt : int ref + (** Number of keys of the hashtable [tbl]. *) + } let make_var = fun hcons lit acc -> @@ -438,7 +444,6 @@ module type FLAT_FORMULA = sig val equal : t -> t -> bool val compare : t -> t -> int val print : Format.formatter -> t -> unit - val print_stats : Format.formatter -> unit val vrai : t val faux : t val view : t -> view @@ -521,8 +526,6 @@ module Flat_Formula : FLAT_FORMULA = struct let print fmt f = cpt := 0; print fmt f - let print_stats _ = () - let compare f1 f2 = f1.tag - f2.tag let equal f1 f2 = f1.tag == f2.tag @@ -530,6 +533,8 @@ module Flat_Formula : FLAT_FORMULA = struct (* unused -- let tag f = f.tag *) let view f = f.view + (* Helper function used to ensure we don't store a flat formula and + its negation in the hconsing environment. *) let is_positive pos = match pos with | AND _ -> true | OR _ -> false @@ -570,8 +575,18 @@ module Flat_Formula : FLAT_FORMULA = struct eq_aux f1.view f2.view end) - type hcons_env = { tbl : t HT.t ; cpt : int ref ; - atoms : Atom.hcons_env} + type hcons_env = { + tbl : t HT.t; + (** Hash set of positive flat formulas. The notion of positive function + is only used to ensure we don't store a flat formula and its negation + in this hash set. *) + + cpt : int ref; + (** Cardinal of the set [tbl]. *) + + atoms : Atom.hcons_env + (** Hconsing environment for the construction of atoms. *) + } let make hcons pos neg = let is_pos = is_positive pos in @@ -600,7 +615,7 @@ module Flat_Formula : FLAT_FORMULA = struct let aaz a = assert (a.Atom.var.Atom.level = 0) - let complements f1 f2 = f1.tag == f2.neg.tag + let[@inline always] complements f1 f2 = f1.tag == f2.neg.tag let mk_lit hcons a acc = let at, acc = Atom.add_atom hcons.atoms a acc in @@ -636,8 +651,25 @@ module Flat_Formula : FLAT_FORMULA = struct let nb_made_vars hcons = Atom.nb_made_vars hcons.atoms + (* Helper function used in the smart constructors [mk_and] and [mk_or]. + Requires: + [l1] and [l2] are two [AND] gates, respectively two [OR] gates, whose + the elements are sorted in increasing order and without duplicates. + + Ensures: + If [l1 = A1 /\ ... /\ An] and [l2 = B1 /\ ... /\ Bm] then + the result of the function is an [AND] gate equivalent to + (A1 /\ .. /\ An) /\ (B1 /\ ... /\ Bm) + but the result gate is actually represented by a sorted list + without duplicates. + + The same goes for the [OR] case. + + @raise Exit if [l1] contains an element [A] and [l2] contains + its negation. *) let merge_and_check l1 l2 = let rec merge_rec l1 l2 hd = + (* Invariant: [hd] is the minimum of the heads of [l1] or [l2]. *) match l1, l2 with | [], l2 -> l2 | l1, [] -> l1 @@ -647,10 +679,16 @@ module Flat_Formula : FLAT_FORMULA = struct else if compare h1 h2 < 0 then begin + (* As the index of the negation of [hd] follows immediatly the + index of [hd], we have the guarantee that [t1] cannot + contain the negation of [hd]. *) if complements hd h1 then raise Exit; h1 :: merge_rec t1 l2 h1 end else begin + (* As the index of the negation of [hd] follows immediatly the + index of [hd], we have the guarantee that [t2] cannot + contain the negation of [hd]. *) if complements hd h2 then raise Exit; h2 :: merge_rec l1 t2 h2 end @@ -846,6 +884,11 @@ module Flat_Formula : FLAT_FORMULA = struct (* translation from E.t *) + (* Helper function used in [simplify] to create a fresh atom for + the lemmas embedded in an expression formula. + + Both [abstr] and [lem] ensure we won't create twice an abstraction + for the same lemma. *) let abstract_lemma hcons abstr (f: E.t) tl lem new_vars = try fst (abstr f) with Not_found -> @@ -866,7 +909,10 @@ module Flat_Formula : FLAT_FORMULA = struct xlit let simplify hcons f abstr new_vars = + (* Cache of the new lemmas discovered in [f]. These lemmas aren't + present in the internal cache of [abstr]. *) let lem = ref [] in + (* Accumulator of the new atoms. *) let new_vars = ref new_vars in let rec simp topl ~parent_disj f = match E.form_view f with diff --git a/src/lib/structures/satml_types.mli b/src/lib/structures/satml_types.mli index 37dc30379..d6c5cbf5a 100644 --- a/src/lib/structures/satml_types.mli +++ b/src/lib/structures/satml_types.mli @@ -34,33 +34,83 @@ module type ATOM = sig type var = { vid : int; pa : atom; + (* Pointer to the positive atom having this variable as + underlying variable. *) + na : atom; + (* Pointer to the nagative atom having this variable as + underlying variable. *) + mutable weight : float; mutable seen : bool; - mutable level : int; (* decision level *) - mutable index : int; (* position in the trail, debug only *) - mutable hindex : int; (* index in heap *) + mutable level : int; + (** Decision level. For more details, see the documention of the field + [trail] of the environment of SatML. *) + + mutable index : int; + (** Position in the trail, debug only. + + This position doesn't correspond to a propagation level, + see the documention of the field [trail] of the environment of + SatML. *) + + mutable hindex : int; + (** Index in heap. *) + mutable reason: reason; + (** If the value is [Some c], the clause [c] is the reason for + which [pa] or [na] have been assigned to be [true]. *) + mutable vpremise : premise} - and atom = - { var : var; - lit : Expr.t; - neg : atom; - mutable watched : clause Vec.t; - mutable is_true : bool; - mutable timp : int; - mutable is_guard : bool; - aid : int } - - and clause = - { name : string; - mutable atoms : atom Vec.t ; - mutable activity : float; - mutable removed : bool; - learnt : bool; - cpremise : premise; - form : Expr.t} + and atom = { + var : var; + (** The underlying variable. *) + + lit : Expr.t; + (** The underlying literal. *) + + neg : atom; + (** The negation of this atom. *) + + mutable watched : clause Vec.t; + (** List of clauses watched by this atom. *) + + mutable is_true : bool; + (** Determine if the atom is assigned. An atom [a] and its + negation [a.neg] cannot be both assigned. *) + + mutable timp : int; + mutable is_guard : bool; + (** Determine if the atom is used as an incremental guard. *) + + aid : int + } + + and clause = { + name : string; + mutable atoms : atom Vec.t; + (** Atoms of the clause. + + A clause has always at least two atoms and + the negations of the two first atoms watch the clause. *) + + mutable activity : float; + mutable removed : bool; + (** If this flag is set to [true], the clause is ignored during + the boolean constraint propagation. More precisely, if the clause + is watched by an atom [a], we don't propagate constraints in this + clause after assigned [a] to [true]. + + Satisfied clauses (that is clauses whose one of their atoms has been + decided at the level [0]) can be removed for sake of performance. *) + + learnt : bool; + (** This flag is set to [true] if the clause have been learnt by solver. *) + + cpremise : premise; + form : Expr.t + } and reason = clause option @@ -121,20 +171,63 @@ module Atom : ATOM module type FLAT_FORMULA = sig type t - type view = private UNIT of Atom.atom | AND of t list | OR of t list + (* Type of hconsed flat formula. *) + + type view = private + | UNIT of Atom.atom + (** [UNIT a] represents an atom. *) + + | AND of t list + (** [AND (A1, ..., An)] represents the n-ary [AND] gate + A1 /\ ... /\ An + with the following invariants: + - There are at least two elements; + - No duplicate; + - None of the [Ai] are [AND] gates; + - The elements are in increasing order for the function [compare]; + - The gate doesn't contain a contradiction. *) + + | OR of t list + (** [OR (A1, ..., An)]) represents the n-ary [OR] gate + A1 \/ ... \/ An + with the following invariants: + - There are at least two elements; + - No duplicate; + - None of the [Ai] are [OR] gates; + - The elements are in increasing order for the function [compare]; + - The gate doesn't contain tautology. *) + type hcons_env + (* Environment of the hconsing. *) val equal : t -> t -> bool + (** [equal f1 f2] checks the equality of the hashes of [f1] and [f2]. *) + val compare : t -> t -> int + (** [compare f1 f2] compares the two flat formulas [f1] and [f2] using hashes. + + By construction, the negation of a flat formula [f] is the immediate + successor or predecessor of [f] for this comparison function. + + [vrai] is the smallest element for this order and [faux] is + the second smallest element. *) + val print : Format.formatter -> t -> unit - val print_stats : Format.formatter -> unit val vrai : t val faux : t val view : t -> view val mk_lit : hcons_env -> Expr.t -> Atom.var list -> t * Atom.var list val mk_and : hcons_env -> t list -> t + (** [mk_and l] where [l = [f1; ...; fn]] is a flat formula equivalent to + [f1 /\ ... /\ fn]. *) + val mk_or : hcons_env -> t list -> t + (** [mk_or l] where [l = [f1; ...; fn]] is a flat formula equivalent to + [f1 \/ ... \/ fn]. *) + val mk_not : t -> t + (** [mk_not f] is a flat formula equivalent to the negation of [f]. *) + val empty_hcons_env : unit -> hcons_env val nb_made_vars : hcons_env -> int val get_atom : hcons_env -> Expr.t -> Atom.atom @@ -146,6 +239,18 @@ module type FLAT_FORMULA = sig Atom.var list -> t * (Expr.t * (t * Atom.atom)) list * Atom.var list + (** [simplify henv f abstr acc] creates a flat formula from the + expression formula [f] in the hconsing environment [henv]. + + The [abstr] function is used to hit a cache of abstract atoms used to + represent lemmas. + + @return [(ff, new_abstrs, new_vars)] where + - [ff] is the flat formula built from [f]. + - [new_abstrs] is the list of abstractions created for lemmas in [f]. + The internal cache of [abstr] has to be updated with the new + abstractions before recalling [simplify]. + - [new_vars] is an accumulator of all the new atoms. *) val get_proxy_of : t -> (Atom.atom * Atom.atom list * bool) Util.MI.t -> Atom.atom option