diff --git a/_tags b/_tags index 11e609f7..4f131897 100644 --- a/_tags +++ b/_tags @@ -2,7 +2,7 @@ true: color(always) # optimization options -true: optimize(3), unbox_closures +true: optimize(3), unbox_closures, unbox_closures_factor(20) # Include paths : include diff --git a/solver/internal.ml b/solver/internal.ml index 74b42d89..6c87e7bf 100644 --- a/solver/internal.ml +++ b/solver/internal.ml @@ -23,11 +23,11 @@ module Make (* a push/pop state *) type user_level = { (* User levels always refer to decision_level 0 *) - ul_elt_lvl : int; (* Number of atoms in trail at decision level 0 *) - ul_th_lvl : int; (* Number of atoms known by the theory at decicion level 0 *) + ul_elt_lvl : int; (* Number of atoms in trail at decision level 0 *) + ul_th_lvl : int; (* Number of atoms known by the theory at decicion level 0 *) ul_th_env : Th.level; (* Theory state at level 0 *) - ul_clauses : int; (* number of clauses *) - ul_learnt : int; (* number of learnt clauses *) + ul_clauses : int; (* number of clauses *) + ul_learnt : int; (* number of learnt clauses *) } (* Singleton type containing the current state *) @@ -107,6 +107,7 @@ module Make mutable nb_init_clauses : int; } + (* Starting environment. *) let env = { unsat_conflict = None; next_decision = None; @@ -157,18 +158,40 @@ module Make nb_init_clauses = 0; } + (* Misc functions *) + let to_float i = float_of_int i + let to_int f = int_of_float f + + let nb_clauses () = Vec.size env.clauses_hyps + let nb_vars () = St.nb_elt () + let decision_level () = Vec.size env.elt_levels + + let f_weight i j = + get_elt_weight (St.get_elt j) < get_elt_weight (St.get_elt i) + + (* Is the assumptions currently unsat ? *) let is_unsat () = match env.unsat_conflict with | Some _ -> true | None -> false + (* Level for push/pop operations *) + type level = int + (* Push/Pop *) let current_level () = Vec.size env.user_levels - let push () = - if is_unsat () then current_level () + let push () : level = + if is_unsat () then + (* When unsat, pushing does nothing, since adding more assumptions + can not make the proof disappear. *) + current_level () else begin + (* The assumptions are sat, or at least not yet detected unsat, + we need to save enough to be able to restore the current decision + level 0. *) let res = current_level () in + (* To restore decision level 0, we need the stolver queue, and theory state. *) let ul_elt_lvl, ul_th_lvl = if Vec.is_empty env.elt_levels then env.elt_head, env.th_head @@ -179,58 +202,61 @@ module Make if Vec.is_empty env.th_levels then Th.current_level () else Vec.get env.th_levels 0 in + (* Keep in mind what are the current assumptions. *) let ul_clauses = Vec.size env.clauses_hyps in let ul_learnt = Vec.size env.clauses_learnt in Vec.push env.user_levels {ul_elt_lvl; ul_th_lvl; ul_th_env; ul_clauses; ul_learnt;}; res end - (* Level for push/pop operations *) - type level = int - + (* To store info for level 0, it is easier to push at module + initialisation, when there are no assumptions. *) let base_level = let l = push () in assert (l = 0); l - (* Iteration over subterms *) - module Mi = Map.Make(struct type t = int let compare = Pervasives.compare end) - let iter_map = ref Mi.empty + (* Iteration over subterms. + When incrementing activity, we want to be able to iterate over + all subterms of a formula. However, the function provided by the theory + may be costly (if it walks a tree-like structure, and does some processing + to ignore some subterms for instance), so we want to 'cache' to list + of subterms of each formula. To do so we use a hashtable from variable id to + list of subterms. *) + let iter_map = Hashtbl.create 1003 let iter_sub f v = try - List.iter f (Mi.find v.vid !iter_map) + List.iter f (Hashtbl.find iter_map v.vid) with Not_found -> let l = ref [] in Th.iter_assignable (fun t -> l := add_term t :: !l) v.pa.lit; - iter_map := Mi.add v.vid !l !iter_map; + Hashtbl.add iter_map v.vid !l; List.iter f !l - let atom lit = + (* When we have a new litteral, + we need to first create the list of its subterms. *) + let atom lit : atom = let res = add_atom lit in iter_sub ignore res.var; res - (* Misc functions *) - let to_float i = float_of_int i - let to_int f = int_of_float f - - (* Accessors for litterals *) - let f_weight i j = - get_elt_weight (St.get_elt j) < get_elt_weight (St.get_elt i) - - (* - let f_filter i = - get_elt_level (St.get_elt i) < 0 - *) - - (* Var/clause activity *) + (* Variable and litteral activity. + Activity is used to decide on which variable to decide when propagation + is done. Uses a heap (implemented in Iheap), to keep track of variable activity. + To be more general, the heap only stores the variable/litteral id (i.e an int). + When we add a variable (which wraps a formula), we also need to add all + its subterms. + *) let insert_var_order = function | Either.Left l -> Iheap.insert f_weight env.order l.lid | Either.Right v -> Iheap.insert f_weight env.order v.vid; iter_sub (fun t -> Iheap.insert f_weight env.order t.lid) v + (* Rather than iterate over all the heap when we want to decrease all the + variables/literals activity, we instead increase the value by which + we increase the activity of 'interesting' var/lits. *) let var_decay_activity () = env.var_incr <- env.var_incr *. env.var_decay @@ -273,33 +299,45 @@ module Make env.clause_incr <- env.clause_incr *. 1e-20 end - (* Convenient access *) - let decision_level () = Vec.size env.elt_levels + (* Simplification of clauses. + When adding new clauses, it is desirable to 'simplify' them, i.e: + - remove variables that are false at level 0, since it is a fact + that they cannot be true, and therefore can not help to satisfy the clause - let nb_clauses () = Vec.size env.clauses_hyps - let nb_vars () = St.nb_elt () - - (* Simplify clauses *) + Aditionally, since we can do push/pop on the assumptions, we need to + keep track of what assumptions were used to simplify a given clause. + *) exception Trivial let simplify_zero atoms level0 = - (* Eliminates dead litterals from clauses when at decision level 0 *) + (* Eliminates dead litterals from clauses when at decision level 0 (see above) *) assert (decision_level () = 0); let aux (atoms, history, lvl) a = if a.is_true then raise Trivial; + (* If a variable is true at level 0, then the clause is always satisfied *) if a.neg.is_true then begin + (* If a variable is false, we need to see why it is false. *) match a.var.reason with | None | Some Decision -> assert false + (* The var must have a reason, and it cannot be a decision, since we are + at level 0. *) | Some (Bcp cl) -> atoms, cl :: history, max lvl cl.c_level + (* The variable has been set to false because of another clause, + we then need to keep track of the assumption level used. *) | Some (Semantic 0) -> atoms, history, lvl + (* Semantic propagations at level 0 are, well not easy to deal with, + this shouldn't really happen actually (because semantic propagations + at level 0 currently lack a proof). *) | Some (Semantic _) -> Log.debugf 0 "Unexpected semantic propagation at level 0: %a" (fun k->k St.pp_atom a); assert false end else a::atoms, history, lvl + (* General case, we do not know the truth value of a, just let it be. *) in let atoms, init, lvl = List.fold_left aux ([], [], level0) atoms in + (* TODO: Why do we sort the atoms here ? *) List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init, lvl let partition atoms init0 = @@ -309,12 +347,17 @@ module Make | a :: r -> if a.is_true then if a.var.v_level = 0 then raise Trivial + (* Same as before, a var true at level 0 gives a trivially true clause *) else (a::trues) @ unassigned @ falses @ r, history, lvl + (* A var true at level > 0 does not change anything, but is unlikely + to be watched, so we put prefer to put them at the end. *) else if a.neg.is_true then if a.var.v_level = 0 then begin match a.var.reason with | Some (Bcp cl) -> partition_aux trues unassigned falses (cl :: history) (max lvl cl.c_level) r + (* Same as before, a var false at level 0 can be eliminated from the clause, + but we need to kepp in mind that we used another clause to simplify it. *) | Some (Semantic 0) -> partition_aux trues unassigned falses history lvl r | _ -> assert false @@ -328,7 +371,8 @@ module Make else partition_aux [] [] [] [] init0 atoms - (* Compute a progess estimate *) + (* Compute a progess estimate. + TODO: remove it or use it ? *) let progress_estimate () = let prg = ref 0. in let nbv = to_float (nb_vars()) in @@ -342,7 +386,13 @@ module Make !prg /. nbv - (* Manipulating decision levels *) + (* Making a decision. + Before actually creatig a new decision level, we check that + all propagations have been done and propagated to the theory, + i.e that the theoriy state indeed takes into account the whole + stack of litterals + i.e we have indeed reached a propagation fixpoint before making + a new decision *) let new_decision_level() = assert (env.th_head = Vec.size env.elt_queue); assert (env.elt_head = Vec.size env.elt_queue); @@ -350,10 +400,14 @@ module Make Vec.push env.th_levels (Th.current_level ()); (* save the current tenv *) () - (* Adding/removing clauses *) + (* Attach/Detach a clause. + Clauses that become satisfied are detached, i.e we remove + their watchers, while clauses that loose their satisfied status + have to be reattached, adding watchers. *) let attach_clause c = Vec.push (Vec.get c.atoms 0).neg.watched c; Vec.push (Vec.get c.atoms 1).neg.watched c; + (* TODO: Learnt litterals are not really used anymre, :p *) if c.learnt then env.learnts_literals <- env.learnts_literals + Vec.size c.atoms else @@ -362,36 +416,46 @@ module Make let detach_clause c = Log.debugf 10 "Removing clause @[%a@]" (fun k->k St.pp_clause c); c.removed <- true; - (* Not necessary, cleanup is done during propagation - Vec.remove (Vec.get c.atoms 0).neg.watched c; - Vec.remove (Vec.get c.atoms 1).neg.watched c; - *) if c.learnt then env.learnts_literals <- env.learnts_literals - Vec.size c.atoms else env.clauses_literals <- env.clauses_literals - Vec.size c.atoms - let remove_clause c = detach_clause c + (* Is a clause satisfied ? *) + let satisfied c = Vec.exists (fun atom -> atom.is_true) c.atoms - let satisfied c = - Vec.exists (fun atom -> atom.is_true) c.atoms - - (* cancel down to [lvl] excluded *) + (* Backtracking. + Used to backtrack, i.e cancel down to [lvl] excluded, + i.e we want to go back to the state the solver was in + when decision level [lvl] was created. *) let cancel_until lvl = + (* Nothing to do if we try to backtrack to a non-existent level. *) if decision_level () > lvl then begin + (* We set the head of the solver and theory queue to what it was. *) env.elt_head <- Vec.get env.elt_levels lvl; env.th_head <- env.elt_head; + (* Now we need to cleanup the vars that are not valid anymore + (i.e to the right of elt_head in the queue. *) for c = env.elt_head to Vec.size env.elt_queue - 1 do match (Vec.get env.elt_queue c) with + (* A literal is unassigned, we nedd to add it back to + the heap of potentially assignable literals. *) | Either.Left l -> l.assigned <- None; l.l_level <- -1; insert_var_order (elt_of_lit l) + (* A variable is not true/false anymore, one of two things can happen: *) | Either.Right a -> if a.var.v_level <= lvl then begin + (* It is a semantic propagation, which can be late, and has a level + lower than where we backtrack, so we just move it to the head + of the queue. *) Vec.set env.elt_queue env.elt_head (of_atom a); env.elt_head <- env.elt_head + 1 end else begin + (* it is a result of bolean propagation, or a semantic propagation + with a level higher than the level to which we backtrack, + in that case, we simply unset its value and reinsert it into the heap. *) a.is_true <- false; a.neg.is_true <- false; a.var.v_level <- -1; @@ -399,7 +463,9 @@ module Make insert_var_order (elt_of_var a.var) end done; - Th.backtrack (Vec.get env.th_levels lvl); (* recover the right tenv *) + (* Recover the right theory state. *) + Th.backtrack (Vec.get env.th_levels lvl); + (* Resize the vectors according to their new size. *) Vec.shrink env.elt_queue ((Vec.size env.elt_queue) - env.elt_head); Vec.shrink env.elt_levels ((Vec.size env.elt_levels) - lvl); Vec.shrink env.th_levels ((Vec.size env.th_levels) - lvl); @@ -407,24 +473,40 @@ module Make assert (Vec.size env.elt_levels = Vec.size env.th_levels); () + (* Unsatisfiability is signaled through an exception, since it can happen + in multiple places (adding new clauses, or solving for instance). *) let report_unsat ({atoms=atoms} as confl) = Log.debugf 5 "@[Unsat conflict: %a@]" (fun k -> k St.pp_clause confl); env.unsat_conflict <- Some confl; raise Unsat + (* Simplification of boolean propagation reasons. + When doing boolean propagation *at level 0*, it can happen + that the clause cl, which propagates a formula, also contains + other formulas, but has been simplified. in which case, we + need to rebuild a clause with correct history, in order to + be able to build a correct proof at the end of proof search. *) let simpl_reason = function | (Bcp cl) as r -> let l, history, c_lvl = partition (Vec.to_list cl.atoms) 0 in begin match l with | [ a ] -> if history = [] then r + (* no simplification has been done, so [cl] is actually a clause with only + [a], so it is a valid reason for propagating [a]. *) else + (* Clauses in [history] have been used to simplify [cl] into a clause [tmp_cl] + with only one formula (which is [a]). So we explicitly create that clause + and set it as the cause for the propagation of [a], that way we can + rebuild the whole resolution tree when we want to prove [a]. *) let tmp_cl = make_clause (fresh_tname ()) l 1 true (History (cl :: history)) c_lvl in Bcp tmp_cl | _ -> assert false end | r -> r + (* Boolean propagation. + Wrapper function for adding a new propagated formula. *) let enqueue_bool a lvl reason = if a.neg.is_true then begin Log.debugf 0 "Trying to enqueue a false litteral: %a" (fun k->k St.pp_atom a); @@ -610,7 +692,7 @@ module Make clause_bump_activity lclause; if is_uip then enqueue_bool fuip blevel (Bcp lclause) - else begin + else begin env.next_decision <- Some fuip.neg end end; @@ -790,10 +872,10 @@ module Make let res = ref None in while env.elt_head < Vec.size env.elt_queue do begin match Vec.get env.elt_queue env.elt_head with - | Either.Left _ -> () - | Either.Right a -> - incr num_props; - propagate_atom a res + | Either.Left _ -> () + | Either.Right a -> + incr num_props; + propagate_atom a res end; env.elt_head <- env.elt_head + 1; done; @@ -838,14 +920,14 @@ module Make for i = 0 to lim1 - 1 do let c = Vec.get env.learnts i in if Vec.size c.atoms > 2 && not (locked c) then - remove_clause c + detach_clause c else begin Vec.set env.learnts !j c; incr j end done; for i = lim1 to lim2 - 1 do let c = Vec.get env.learnts i in if Vec.size c.atoms > 2 && not (locked c) && c.activity < extra_lim then - remove_clause c + detach_clause c else begin Vec.set env.learnts !j c; incr j end done; @@ -857,7 +939,7 @@ module Make let remove_satisfied vec = for i = 0 to Vec.size vec - 1 do let c = Vec.get vec i in - if satisfied c then remove_clause c + if satisfied c then detach_clause c done let simplify () = @@ -961,8 +1043,8 @@ module Make add_clause c; (* Clauses can be added after search has begun (and thus we are not at level 0, so better not do anything at this point. - match propagate () with - | None -> () | Some confl -> report_unsat confl + match propagate () with + | None -> () | Some confl -> report_unsat confl *) in List.iter aux cnf @@ -1106,7 +1188,7 @@ module Make for i = ul.ul_clauses to Vec.size env.clauses_hyps - 1 do let c = Vec.get env.clauses_hyps i in assert (c.c_level > l); - remove_clause c + detach_clause c done; Vec.shrink env.clauses_hyps (Vec.size env.clauses_hyps - ul.ul_clauses); @@ -1116,7 +1198,7 @@ module Make for i = ul.ul_learnt to Vec.size env.clauses_learnt - 1 do let c = Vec.get env.clauses_learnt i in if c.c_level > l then begin - remove_clause c; + detach_clause c; match c.cpremise with | History ({ cpremise = Lemma _ } as c' :: _ ) -> Stack.push c' s | _ -> () (* Only simplified clauses can have a level > 0 *)