diff --git a/msat.mlpack b/msat.mlpack index 1abd2ef0..9aac5035 100644 --- a/msat.mlpack +++ b/msat.mlpack @@ -1,22 +1,24 @@ # Debug Log -# Solver Modules +# Interface definitions Log_intf Formula_intf -Solver -Solver_types Theory_intf -Expr_intf -Mcsolver -Mcsolver_types Plugin_intf +Expr_intf +Tseitin_intf +Res_intf + +# Solver Modules +Internal +Solver +Mcsolver +Solver_types # Auxiliary modules Res -Mcproof Tseitin -Tseitin_intf # Sat/Smt modules Expr diff --git a/solver/internal.ml b/solver/internal.ml new file mode 100644 index 00000000..dca67ce9 --- /dev/null +++ b/solver/internal.ml @@ -0,0 +1,936 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +module Make (L : Log_intf.S)(St : Solver_types.S) + (Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof) = struct + + open St + module Proof = Res.Make(L)(St) + + exception Sat + exception Unsat + exception Restart + exception Conflict of clause + + (* a push/pop state *) + type user_level = { + ul_trail : int; (* height of the decision trail *) + ul_clauses : int; (* number of clauses *) + ul_learnt : int; (* number of learnt clauses *) + } + + (* Singleton type containing the current state *) + type env = { + + mutable is_unsat : bool; + (* if [true], constraints are already false *) + + mutable unsat_conflict : clause option; + (* conflict clause at decision level 0, if any *) + + clauses : clause Vec.t; + (* all currently active clauses *) + + learnts : clause Vec.t; + (* learnt clauses *) + + mutable clause_inc : float; + (* increment for clauses' activity *) + + mutable var_inc : float; + (* increment for variables' activity *) + + trail : (semantic var, atom) Either.t Vec.t; + (* decision stack + propagated atoms *) + + trail_lim : int Vec.t; + (* decision levels in [trail] *) + + user_levels : user_level Vec.t; + (* user-defined levels, for {!push} and {!pop} *) + + mutable qhead : int; + (* Start offset in the queue of unit facts to propagate, within the trail *) + + mutable simpDB_assigns : int; + (* number of toplevel assignments since last call to [simplify ()] *) + + mutable simpDB_props : int; + (* remaining number of propagations before the next call to [simplify ()] *) + + order : Iheap.t; + (* Heap ordered by variable activity *) + + mutable progress_estimate : float; + (* progression estimate, updated by [search ()] *) + + remove_satisfied : bool; + + var_decay : float; + (* inverse of the activity factor for variables. Default 1/0.999 *) + + clause_decay : float; + (* inverse of the activity factor for clauses. Default 1/0.95 *) + + mutable restart_first : int; + (* intial restart limit, default 100 *) + + restart_inc : float; + (* multiplicative factor for restart limit, default 1.5 *) + + mutable learntsize_factor : float; + (* initial limit for the number of learnt clauses, 1/3 of initial + number of clauses by default *) + + learntsize_inc : float; + (* multiplicative factor for [learntsize_factor] at each restart, default 1.1 *) + + expensive_ccmin : bool; + (* control minimization of conflict clause, default true *) + + polarity_mode : bool; + (* default polarity for decision *) + + mutable starts : int; + mutable decisions : int; + mutable propagations : int; + mutable conflicts : int; + mutable clauses_literals : int; + mutable learnts_literals : int; + mutable max_literals : int; + mutable tot_literals : int; + mutable nb_init_clauses : int; + mutable tenv_queue : Th.level Vec.t; + mutable tatoms_qhead : int; + } + + let env = { + is_unsat = false; + unsat_conflict = None; + clauses = Vec.make 0 dummy_clause; (*updated during parsing*) + learnts = Vec.make 0 dummy_clause; (*updated during parsing*) + clause_inc = 1.; + var_inc = 1.; + trail = Vec.make 601 (Either.mk_right dummy_atom); + trail_lim = Vec.make 601 (-1); + user_levels = Vec.make 20 {ul_trail=0;ul_learnt=0;ul_clauses=0}; + qhead = 0; + simpDB_assigns = -1; + simpDB_props = 0; + order = Iheap.init 0; (* updated in solve *) + progress_estimate = 0.; + remove_satisfied = true; + var_decay = 1. /. 0.95; + clause_decay = 1. /. 0.999; + restart_first = 100; + restart_inc = 1.5; + learntsize_factor = 1. /. 3. ; + learntsize_inc = 1.1; + expensive_ccmin = true; + polarity_mode = false; + starts = 0; + decisions = 0; + propagations = 0; + conflicts = 0; + clauses_literals = 0; + learnts_literals = 0; + max_literals = 0; + tot_literals = 0; + nb_init_clauses = 0; + tenv_queue = Vec.make 100 Th.dummy; + tatoms_qhead = 0; + } + + (* Misc functions *) + let to_float i = float_of_int i + let to_int f = int_of_float f + + (* Accessors for variables *) + let get_var_id v = v.vid + let get_var_level v = v.level + let get_var_weight v = v.weight + + let set_var_weight v w = v.weight <- w + let set_var_level v l = v.level <- l + + let get_elt_id e = Either.destruct e get_var_id get_var_id + let get_elt_weight e = Either.destruct e get_var_weight get_var_weight + let get_elt_level e = Either.destruct e get_var_level get_var_level + + let set_elt_weight e = Either.destruct e set_var_weight set_var_weight + let set_elt_level e = Either.destruct e set_var_level set_var_level + + let f_weight i j = + get_elt_weight (St.get_var j) < get_elt_weight (St.get_var i) + + let f_filter i = + get_elt_level (St.get_var i) < 0 + + (* Var/clause activity *) + let insert_var_order e = Either.destruct e + (fun v -> Iheap.insert f_weight env.order v.vid) + (fun v -> + Iheap.insert f_weight env.order v.vid; + iter_sub (fun t -> Iheap.insert f_weight env.order t.vid) v + ) + + let var_decay_activity () = + env.var_inc <- env.var_inc *. env.var_decay + + let clause_decay_activity () = + env.clause_inc <- env.clause_inc *. env.clause_decay + + let var_bump_activity_aux v = + v.weight <- v.weight +. env.var_inc; + if v.weight > 1e100 then begin + for i = 0 to (St.nb_vars ()) - 1 do + set_elt_weight (St.get_var i) ((get_elt_weight (St.get_var i)) *. 1e-100) + done; + env.var_inc <- env.var_inc *. 1e-100; + end; + if Iheap.in_heap env.order v.vid then + Iheap.decrease f_weight env.order v.vid + + let var_bump_activity v = + var_bump_activity_aux v; + iter_sub (fun t -> var_bump_activity_aux t) v + + let clause_bump_activity c = + c.activity <- c.activity +. env.clause_inc; + if c.activity > 1e20 then begin + for i = 0 to (Vec.size env.learnts) - 1 do + (Vec.get env.learnts i).activity <- + (Vec.get env.learnts i).activity *. 1e-20; + done; + env.clause_inc <- env.clause_inc *. 1e-20 + end + + (* Convenient access *) + let decision_level () = Vec.size env.trail_lim + + let nb_assigns () = Vec.size env.trail + let nb_clauses () = Vec.size env.clauses + let nb_learnts () = Vec.size env.learnts + let nb_vars () = St.nb_vars () + + let new_decision_level() = + Vec.push env.trail_lim (Vec.size env.trail); + Vec.push env.tenv_queue (Th.current_level ()); (* save the current tenv *) + L.debug 5 "New decision level : %d (%d in env queue)(%d in trail)" + (Vec.size env.trail_lim) (Vec.size env.tenv_queue) (Vec.size env.trail); + () + + let attach_clause c = + Vec.push (Vec.get c.atoms 0).neg.watched c; + Vec.push (Vec.get c.atoms 1).neg.watched c; + L.debug 8 "%a <-- %a" St.pp_atom (Vec.get c.atoms 0).neg St.pp_clause c; + L.debug 8 "%a <-- %a" St.pp_atom (Vec.get c.atoms 1).neg St.pp_clause 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 detach_clause c = + c.removed <- true; + (* + 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 + + let satisfied c = + Vec.exists (fun atom -> atom.is_true) c.atoms + + (* cancel down to [lvl] excluded *) + let cancel_until lvl = + L.debug 1 "Backtracking to decision level %d (excluded)" lvl; + if decision_level () > lvl then begin + env.qhead <- Vec.get env.trail_lim lvl; + env.tatoms_qhead <- env.qhead; + for c = env.qhead to Vec.size env.trail - 1 do + Either.destruct (Vec.get env.trail c) + (fun v -> + v.tag.assigned <- None; + v.level <- -1; + insert_var_order (Either.mk_left v) + ) + (fun a -> + if a.var.level <= lvl then begin + Vec.set env.trail env.qhead (Either.mk_right a); + env.qhead <- env.qhead + 1 + end else begin + a.is_true <- false; + a.neg.is_true <- false; + a.var.level <- -1; + a.var.tag.reason <- Bcp None; + insert_var_order (Either.mk_right a.var) + end) + done; + Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *) + Vec.shrink env.trail ((Vec.size env.trail) - env.qhead); + Vec.shrink env.trail_lim ((Vec.size env.trail_lim) - lvl); + Vec.shrink env.tenv_queue ((Vec.size env.tenv_queue) - lvl); + end; + assert (Vec.size env.trail_lim = Vec.size env.tenv_queue) + + let report_unsat ({atoms=atoms} as confl) = + L.debug 5 "Unsat conflict : %a" St.pp_clause confl; + env.unsat_conflict <- Some confl; + env.is_unsat <- true; + raise Unsat + + let enqueue_bool a lvl reason = + assert (not a.neg.is_true); + if a.is_true then + L.debug 10 "Litteral %a already in queue" pp_atom a + else begin + assert (a.var.level < 0 && a.var.tag.reason = Bcp None && lvl >= 0); + a.is_true <- true; + a.var.level <- lvl; + a.var.tag.reason <- reason; + Vec.push env.trail (Either.mk_right a); + L.debug 2 "Enqueue (%d): %a" (nb_assigns ()) pp_atom a + end + + let enqueue_assign (v: semantic var) value lvl = + v.tag.assigned <- Some value; + v.level <- lvl; + Vec.push env.trail (Either.mk_left v); + L.debug 2 "Enqueue (%d): %a" (nb_assigns ()) St.pp_semantic_var v + + let th_eval a = + if a.is_true || a.neg.is_true then None + else match Th.eval a.lit with + | Th.Unknown -> None + | Th.Valued (b, lvl) -> + let atom = if b then a else a.neg in + enqueue_bool atom lvl (Semantic lvl); + Some b + + (* conflict analysis *) + let max_lvl_atoms l = + List.fold_left (fun (max_lvl, acc) a -> + if a.var.level = max_lvl then (max_lvl, a :: acc) + else if a.var.level > max_lvl then (a.var.level, [a]) + else (max_lvl, acc)) (0, []) l + + let backtrack_lvl is_uip = function + | [] -> 0 + | a :: r when not is_uip -> max (a.var.level - 1) 0 + | a :: [] -> 0 + | a :: b :: r -> assert(a.var.level <> b.var.level); b.var.level + + let analyze_mcsat c_clause = + let tr_ind = ref (Vec.size env.trail) in + let is_uip = ref false in + let c = ref (Proof.to_list c_clause) in + let history = ref [c_clause] in + clause_bump_activity c_clause; + let is_semantic a = match a.var.tag.reason with + | Semantic _ -> true + | _ -> false + in + try while true do + let lvl, atoms = max_lvl_atoms !c in + L.debug 15 "Current conflict clause :"; + List.iter (fun a -> L.debug 15 " |- %a" St.pp_atom a) !c; + if lvl = 0 then raise Exit; + match atoms with + | [] | _ :: [] -> + L.debug 15 "Found UIP clause"; + is_uip := true; + raise Exit + | _ when List.for_all is_semantic atoms -> + L.debug 15 "Found Semantic backtrack clause"; + raise Exit + | _ -> + decr tr_ind; + L.debug 20 "Looking at trail element %d" !tr_ind; + Either.destruct (Vec.get env.trail !tr_ind) + (fun v -> L.debug 15 "%a" St.pp_semantic_var v) + (fun a -> match a.var.tag.reason with + | Bcp (Some d) -> + L.debug 15 "Propagation : %a" St.pp_atom a; + L.debug 15 " |- %a" St.pp_clause d; + let tmp, res = Proof.resolve (Proof.merge !c (Proof.to_list d)) in + begin match tmp with + | [] -> L.debug 15 "No lit to resolve over." + | [b] when b == a.var.tag.pa -> + clause_bump_activity d; + var_bump_activity a.var; + history := d :: !history; + c := res + | _ -> assert false + end + | Bcp None -> L.debug 15 "Decision : %a" St.pp_atom a + | Semantic _ -> L.debug 15 "Semantic propagation : %a" St.pp_atom a) + done; assert false + with Exit -> + let learnt = List.sort (fun a b -> Pervasives.compare b.var.level a.var.level) !c in + let blevel = backtrack_lvl !is_uip learnt in + blevel, learnt, !history, !is_uip + + let get_atom i = + Either.destruct (Vec.get env.trail i) + (fun _ -> assert false) (fun x -> x) + + let analyze_sat c_clause = + let pathC = ref 0 in + let learnt = ref [] in + let cond = ref true in + let blevel = ref 0 in + let seen = ref [] in + let c = ref c_clause in + let tr_ind = ref (Vec.size env.trail - 1) in + let size = ref 1 in + let history = ref [] in + while !cond do + if !c.learnt then clause_bump_activity !c; + history := !c :: !history; + (* visit the current predecessors *) + for j = 0 to Vec.size !c.atoms - 1 do + let q = Vec.get !c.atoms j in + (*printf "I visit %a@." D1.atom q;*) + assert (q.is_true || q.neg.is_true && q.var.level >= 0); (* Pas sur *) + if not q.var.seen && q.var.level > 0 then begin + var_bump_activity q.var; + q.var.seen <- true; + seen := q :: !seen; + if q.var.level >= decision_level () then begin + incr pathC + end else begin + learnt := q :: !learnt; + incr size; + blevel := max !blevel q.var.level + end + end + done; + + (* look for the next node to expand *) + while not (get_atom !tr_ind).var.seen do decr tr_ind done; + decr pathC; + let p = get_atom !tr_ind in + decr tr_ind; + match !pathC, p.var.tag.reason with + | 0, _ -> + cond := false; + learnt := p.neg :: (List.rev !learnt) + | n, Bcp Some cl -> c := cl + | n, _ -> assert false + done; + List.iter (fun q -> q.var.seen <- false) !seen; + !blevel, !learnt, !history, true + + let analyze c_clause = if St.mcsat then analyze_mcsat c_clause else analyze_sat c_clause + + let record_learnt_clause confl blevel learnt history is_uip = + begin match learnt with + | [] -> assert false + | [fuip] -> + assert (blevel = 0); + if fuip.neg.is_true then + report_unsat confl + else begin + let name = fresh_lname () in + let uclause = make_clause name learnt (List.length learnt) true history in + L.debug 1 "Unit clause learnt : %a" St.pp_clause uclause; + Vec.push env.learnts uclause; + enqueue_bool fuip 0 (Bcp (Some uclause)) + end + | fuip :: _ -> + let name = fresh_lname () in + let lclause = make_clause name learnt (List.length learnt) true history in + L.debug 2 "New clause learnt : %a" St.pp_clause lclause; + Vec.push env.learnts lclause; + attach_clause lclause; + clause_bump_activity lclause; + if is_uip then + enqueue_bool fuip blevel (Bcp (Some lclause)) + else begin + env.decisions <- env.decisions + 1; + new_decision_level(); + enqueue_bool fuip.neg (decision_level ()) (Bcp None) + end + end; + var_decay_activity (); + clause_decay_activity () + + let add_boolean_conflict confl = + env.conflicts <- env.conflicts + 1; + if decision_level() = 0 || Vec.for_all (fun a -> a.var.level = 0) confl.atoms then + report_unsat confl; (* Top-level conflict *) + let blevel, learnt, history, is_uip = analyze confl in + cancel_until blevel; + record_learnt_clause confl blevel learnt (History history) is_uip + + (* Add a new clause *) + exception Trivial + + let simplify_zero atoms init0 = + (* TODO: could be more efficient than [@] everywhere? *) + assert (decision_level () = 0); + let aux (atoms, init) a = + if a.is_true then raise Trivial; + if a.neg.is_true then + atoms, false + else + a::atoms, init + in + let atoms, init = List.fold_left aux ([], true) atoms in + List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init + + let partition atoms init0 = + let rec partition_aux trues unassigned falses init = function + | [] -> trues @ unassigned @ falses, init + | a :: r -> + if a.is_true then + if a.var.level = 0 then raise Trivial + else (a::trues) @ unassigned @ falses @ r, init + else if a.neg.is_true then + if a.var.level = 0 then + partition_aux trues unassigned falses false r + else + partition_aux trues unassigned (a::falses) init r + else + partition_aux trues (a::unassigned) falses init r + in + if decision_level () = 0 then + simplify_zero atoms init0 + else + partition_aux [] [] [] true atoms + + let add_clause ?tag name atoms history = + if env.is_unsat then raise Unsat; (* is it necessary ? *) + let init_name = name in + let init0 = make_clause ?tag init_name atoms (List.length atoms) (history <> History []) history in + L.debug 10 "Adding clause : %a" St.pp_clause init0; + try + if Proof.has_been_proved init0 then raise Trivial; + assert (Proof.is_proven init0); (* Important side-effect, DO NOT REMOVE *) + let atoms, init = partition atoms init0 in + let size = List.length atoms in + match atoms with + | [] -> + report_unsat init0; + | a::b::_ -> + let name = fresh_name () in + let clause = + if init then init0 + else make_clause ?tag name atoms size true (History [init0]) + in + L.debug 1 "New clause : %a" St.pp_clause clause; + attach_clause clause; + Vec.push env.clauses clause; + if a.neg.is_true then begin + let lvl = List.fold_left (fun m a -> max m a.var.level) 0 atoms in + cancel_until lvl; + add_boolean_conflict clause + end else if b.neg.is_true && not a.is_true && not a.neg.is_true then begin + let lvl = List.fold_left (fun m a -> max m a.var.level) 0 atoms in + cancel_until lvl; + enqueue_bool a lvl (Bcp (Some clause)) + end + | [a] -> + cancel_until 0; + enqueue_bool a 0 (Bcp (Some init0)) + with Trivial -> () + + let progress_estimate () = + let prg = ref 0. in + let nbv = to_float (nb_vars()) in + let lvl = decision_level () in + let _F = 1. /. nbv in + for i = 0 to lvl do + let _beg = if i = 0 then 0 else Vec.get env.trail_lim (i-1) in + let _end = if i=lvl then Vec.size env.trail else Vec.get env.trail_lim i in + prg := !prg +. _F**(to_float i) *. (to_float (_end - _beg)) + done; + !prg /. nbv + + let propagate_in_clause a c i watched new_sz = + let atoms = c.atoms in + let first = Vec.get atoms 0 in + if first == a.neg then begin (* false lit must be at index 1 *) + Vec.set atoms 0 (Vec.get atoms 1); + Vec.set atoms 1 first + end; + let first = Vec.get atoms 0 in + if first.is_true then begin + (* true clause, keep it in watched *) + Vec.set watched !new_sz c; + incr new_sz; + end + else + try (* look for another watch lit *) + for k = 2 to Vec.size atoms - 1 do + let ak = Vec.get atoms k in + if not (ak.neg.is_true) then begin + (* watch lit found: update and exit *) + Vec.set atoms 1 ak; + Vec.set atoms k a.neg; + Vec.push ak.neg.watched c; + L.debug 8 "New watcher (%a) for clause : %a" St.pp_atom ak.neg St.pp_clause c; + raise Exit + end + done; + (* no watch lit found *) + if first.neg.is_true || (th_eval first = Some false) then begin + (* clause is false *) + env.qhead <- Vec.size env.trail; + for k = i to Vec.size watched - 1 do + Vec.set watched !new_sz (Vec.get watched k); + incr new_sz; + done; + L.debug 3 "Conflict found : %a" St.pp_clause c; + raise (Conflict c) + end else begin + (* clause is unit *) + Vec.set watched !new_sz c; + incr new_sz; + L.debug 5 "Unit clause : %a" St.pp_clause c; + enqueue_bool first (decision_level ()) (Bcp (Some c)) + end + with Exit -> () + + let propagate_atom a res = + L.debug 8 "Propagating %a" St.pp_atom a; + let watched = a.watched in + L.debug 10 "Watching %a :" St.pp_atom a; + Vec.iter (fun c -> L.debug 10 " %a" St.pp_clause c) watched; + let new_sz_w = ref 0 in + begin + try + for i = 0 to Vec.size watched - 1 do + let c = Vec.get watched i in + if not c.removed then propagate_in_clause a c i watched new_sz_w + done; + with Conflict c -> + assert (!res = None); + res := Some c + end; + let dead_part = Vec.size watched - !new_sz_w in + Vec.shrink watched dead_part + + (* Propagation (boolean and theory) *) + let new_atom f = + let a = add_atom f in + L.debug 10 "New atom : %a" St.pp_atom a; + ignore (th_eval a); + a + + let slice_get i = Either.destruct (Vec.get env.trail i) + (function {level; tag={term; assigned = Some v}} -> Th.Assign (term, v), level | _ -> assert false) + (fun a -> Th.Lit a.lit, a.var.level) + + let slice_push l lemma = + let atoms = List.rev_map (fun x -> new_atom x) l in + Iheap.grow_to_by_double env.order (St.nb_vars ()); + List.iter (fun a -> insert_var_order (Either.mk_right a.var)) atoms; + add_clause (fresh_tname ()) atoms (Lemma lemma) + + let slice_propagate f lvl = + let a = add_atom f in + Iheap.grow_to_by_double env.order (St.nb_vars ()); + enqueue_bool a lvl (Semantic lvl) + + let current_slice () = Th.({ + start = env.tatoms_qhead; + length = (Vec.size env.trail) - env.tatoms_qhead; + get = slice_get; + push = slice_push; + propagate = slice_propagate; + }) + + let full_slice tag = Th.({ + start = 0; + length = Vec.size env.trail; + get = slice_get; + push = (fun cl proof -> tag := true; slice_push cl proof); + propagate = (fun _ -> assert false); + }) + + let rec theory_propagate () = + let slice = current_slice () in + env.tatoms_qhead <- nb_assigns (); + match Th.assume slice with + | Th.Sat -> + propagate () + | Th.Unsat (l, p) -> + let l = List.rev_map new_atom l in + Iheap.grow_to_by_double env.order (St.nb_vars ()); + List.iter (fun a -> insert_var_order (Either.mk_right a.var)) l; + let c = St.make_clause (St.fresh_tname ()) l (List.length l) true (Lemma p) in + Some c + + and propagate () = + if env.qhead = Vec.size env.trail then + None + else begin + let num_props = ref 0 in + let res = ref None in + while env.qhead < Vec.size env.trail do + Either.destruct (Vec.get env.trail env.qhead) + (fun a -> ()) + (fun a -> + incr num_props; + propagate_atom a res); + env.qhead <- env.qhead + 1 + done; + env.propagations <- env.propagations + !num_props; + env.simpDB_props <- env.simpDB_props - !num_props; + match !res with + | None -> theory_propagate () + | _ -> !res + end + + (* heuristic comparison between clauses, by their size (unary/binary or not) + and activity *) + let f_sort_db c1 c2 = + let sz1 = Vec.size c1.atoms in + let sz2 = Vec.size c2.atoms in + let c = compare c1.activity c2.activity in + if sz1 = sz2 && c = 0 then 0 + else + if sz1 > 2 && (sz2 = 2 || c < 0) then -1 + else 1 + +(* returns true if the clause is used as a reason for a propagation, + and therefore can be needed in case of conflict. In this case + the clause can't be forgotten *) + let locked c = false (* + Vec.exists + (fun v -> match v.reason with + | Some c' -> c ==c' + | _ -> false + ) env.vars + *) + + (* remove some learnt clauses *) + let reduce_db () = () (* + let extra_lim = env.clause_inc /. (to_float (Vec.size env.learnts)) in + Vec.sort env.learnts f_sort_db; + let lim2 = Vec.size env.learnts in + let lim1 = lim2 / 2 in + let j = ref 0 in + 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 + 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 + else + begin Vec.set env.learnts !j c; incr j end + done; + Vec.shrink env.learnts (lim2 - !j) + *) + + (* remove from [vec] the clauses that are satisfied in the current trail *) + 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 + done + + module HUC = Hashtbl.Make + (struct type t = clause let equal = (==) let hash = Hashtbl.hash end) + + let simplify () = + assert (decision_level () = 0); + if env.is_unsat then raise Unsat; + begin + match propagate () with + | Some confl -> report_unsat confl + | None -> () + end; + if nb_assigns() <> env.simpDB_assigns && env.simpDB_props <= 0 then begin + if Vec.size env.learnts > 0 then remove_satisfied env.learnts; + if env.remove_satisfied then remove_satisfied env.clauses; + (*Iheap.filter env.order f_filter f_weight;*) + env.simpDB_assigns <- nb_assigns (); + env.simpDB_props <- env.clauses_literals + env.learnts_literals; + end + + (* Decide on a new litteral *) + let rec pick_branch_lit () = + let max = Iheap.remove_min f_weight env.order in + Either.destruct (St.get_var max) + (fun v -> + if v.level >= 0 then + pick_branch_lit () + else begin + let value = Th.assign v.tag.term in + env.decisions <- env.decisions + 1; + new_decision_level(); + let current_level = decision_level () in + L.debug 5 "Deciding on %a" St.pp_semantic_var v; + enqueue_assign v value current_level + end) + (fun v -> + if v.level >= 0 then begin + assert (v.tag.pa.is_true || v.tag.na.is_true); + pick_branch_lit () + end else match Th.eval v.tag.pa.lit with + | Th.Unknown -> + env.decisions <- env.decisions + 1; + new_decision_level(); + let current_level = decision_level () in + L.debug 5 "Deciding on %a" St.pp_atom v.tag.pa; + enqueue_bool v.tag.pa current_level (Bcp None) + | Th.Valued (b, lvl) -> + let a = if b then v.tag.pa else v.tag.na in + enqueue_bool a lvl (Semantic lvl)) + + let search n_of_conflicts n_of_learnts = + let conflictC = ref 0 in + env.starts <- env.starts + 1; + while (true) do + match propagate () with + | Some confl -> (* Conflict *) + incr conflictC; + add_boolean_conflict confl + + | None -> (* No Conflict *) + if nb_assigns() = St.nb_vars () (* env.nb_init_vars *) then raise Sat; + if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then begin + L.debug 1 "Restarting..."; + env.progress_estimate <- progress_estimate(); + cancel_until 0; + raise Restart + end; + if decision_level() = 0 then simplify (); + + if n_of_learnts >= 0 && + Vec.size env.learnts - nb_assigns() >= n_of_learnts then + reduce_db(); + + pick_branch_lit () + done + + let check_clause c = + let b = ref false in + let atoms = c.atoms in + for i = 0 to Vec.size atoms - 1 do + let a = Vec.get atoms i in + b := !b || a.is_true + done; + assert (!b) + + let check_vec vec = + for i = 0 to Vec.size vec - 1 do check_clause (Vec.get vec i) done + + let add_clauses ?tag cnf = + let aux cl = + add_clause ?tag (fresh_hname ()) cl (History []); + match propagate () with + | None -> () | Some confl -> report_unsat confl + in + List.iter aux cnf + + (* fixpoint of propagation and decisions until a model is found, or a + conflict is reached *) + let solve () = + if env.is_unsat then raise Unsat; + let n_of_conflicts = ref (to_float env.restart_first) in + let n_of_learnts = ref ((to_float (nb_clauses())) *. env.learntsize_factor) in + try + while true do + begin try + search (to_int !n_of_conflicts) (to_int !n_of_learnts) + with + | Restart -> + n_of_conflicts := !n_of_conflicts *. env.restart_inc; + n_of_learnts := !n_of_learnts *. env.learntsize_inc + | Sat -> + let tag = ref false in + Th.if_sat (full_slice tag); + if not !tag then raise Sat + end + done + with + | Sat -> () + + let init_solver ?tag cnf = + let nbv = St.nb_vars () in + let nbc = env.nb_init_clauses + List.length cnf in + Iheap.grow_to_by_double env.order nbv; + (* List.iter (List.iter (fun a -> insert_var_order a.var)) cnf; *) + St.iter_vars insert_var_order; + Vec.grow_to_by_double env.clauses nbc; + Vec.grow_to_by_double env.learnts nbc; + env.nb_init_clauses <- nbc; + St.iter_vars (fun e -> Either.destruct e + (fun v -> L.debug 50 " -- %a" St.pp_semantic_var v) + (fun a -> L.debug 50 " -- %a" St.pp_atom a.tag.pa) + ); + add_clauses ?tag cnf + + let assume ?tag cnf = + let cnf = List.rev_map (List.rev_map St.add_atom) cnf in + init_solver ?tag cnf + + let eval lit = + let var, negated = make_boolean_var lit in + assert (var.tag.pa.is_true || var.tag.na.is_true); + let truth = var.tag.pa.is_true in + if negated then not truth else truth + + let hyps () = env.clauses + + let history () = env.learnts + + let unsat_conflict () = env.unsat_conflict + + let model () = + let opt = function Some a -> a | None -> assert false in + Vec.fold (fun acc e -> Either.destruct e + (fun (v: semantic var) -> (v.tag.term, opt v.tag.assigned) :: acc) + (fun _ -> acc) + ) [] env.trail + + (* Push/Pop *) + type level = int + + let base_level = 0 + + let current_level () = Vec.size env.user_levels + + let push () = + let ul_trail = if Vec.is_empty env.trail_lim + then base_level + else Vec.last env.trail_lim + and ul_clauses = Vec.size env.clauses + and ul_learnt = Vec.size env.learnts in + Vec.push env.user_levels {ul_trail; ul_clauses;ul_learnt}; + Vec.size env.user_levels + + let pop l = + if l > current_level() + then invalid_arg "cannot pop() to level, it is too high"; + let ul = Vec.get env.user_levels l in + (* see whether we can reset [env.is_unsat] *) + if env.is_unsat && not (Vec.is_empty env.trail_lim) then ( + (* level at which the decision that lead to unsat was made *) + let last = Vec.last env.trail_lim in + if ul.ul_trail < last then env.is_unsat <- false + ); + cancel_until ul.ul_trail; + Vec.shrink env.clauses ul.ul_clauses; + Vec.shrink env.learnts ul.ul_learnt; + () + + let clear () = pop base_level +end + diff --git a/solver/internal.mli b/solver/internal.mli new file mode 100644 index 00000000..6e640f8a --- /dev/null +++ b/solver/internal.mli @@ -0,0 +1,65 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +module Make (L : Log_intf.S)(St : Solver_types.S) + (Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof) : sig + (** Functor to create a solver parametrised by the atomic formulas and a theory. *) + + exception Unsat + + module Proof : Res.S + with type atom = St.atom + and type clause = St.clause + and type lemma = Th.proof + + val solve : unit -> unit + (** Try and solves the current set of assumptions. + @return () if the current set of clauses is satisfiable + @raise Unsat if a toplevel conflict is found *) + + val assume : ?tag:int -> St.formula list list -> unit + (** Add the list of clauses to the current set of assumptions. + Modifies the sat solver state in place. + @raise Unsat if a conflict is detect when adding the clauses *) + + val eval : St.formula -> bool + (** Returns the valuation of a formula in the current state + of the sat solver. *) + + val hyps : unit -> St.clause Vec.t + (** Returns the vector of assumptions used by the solver. May be slightly different + from the clauses assumed because of top-level simplification of clauses. *) + + val history : unit -> St.clause Vec.t + (** Returns the history of learnt clauses, in the right order. *) + + val unsat_conflict : unit -> St.clause option + (** Returns the unsat clause found at the toplevel, if it exists (i.e if + [solve] has raised [Unsat]) *) + + val model : unit -> (St.term * St.term) list + (** Returns the model found if the formula is satisfiable. *) + + type level + (** Abstract notion of assumption level. *) + + val base_level : level + (** Level with no assumption at all, corresponding to the empty solver *) + + val current_level : unit -> level + (** The current level *) + + val push : unit -> level + (** Create a new level that extends the previous one. *) + + val pop : level -> unit + (** Go back to the given level, forgetting every assumption added since. + @raise Invalid_argument if the current level is below the argument *) + + val clear : unit -> unit + (** Return to level {!base_level} *) +end + diff --git a/solver/mcproof.ml b/solver/mcproof.ml deleted file mode 100644 index 10cd3380..00000000 --- a/solver/mcproof.ml +++ /dev/null @@ -1,365 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module type S = Res_intf.S - -module Make(L : Log_intf.S)(St : Mcsolver_types.S) = struct - - (* Type definitions *) - type lemma = St.proof - type clause = St.clause - type atom = St.atom - type int_cl = clause * St.atom list - - type node = - | Assumption - | Lemma of lemma - | Resolution of atom * int_cl * int_cl - (* lits, c1, c2 with lits the literals used to resolve c1 and c2 *) - - exception Insuficient_hyps - exception Resolution_error of string - - (* Proof graph *) - let hash_cl cl = - Hashtbl.hash (List.map (fun a -> St.(a.aid)) cl) - - let equal_cl cl_c cl_d = - try - List.for_all2 (==) cl_c cl_d - with Invalid_argument _ -> - false - - module H = Hashtbl.Make(struct - type t = St.atom list - let hash = hash_cl - let equal = equal_cl - end) - let proof : node H.t = H.create 1007;; - - (* Misc functions *) - let equal_atoms a b = St.(a.aid) = St.(b.aid) - let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid) - - let merge = List.merge compare_atoms - - let _c = ref 0 - let fresh_pcl_name () = incr _c; "P" ^ (string_of_int !_c) - - (* Printing functions *) - let rec print_cl fmt = function - | [] -> Format.fprintf fmt "[]" - | [a] -> St.print_atom fmt a - | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" St.print_atom a print_cl r - - (* Compute resolution of 2 clauses *) - let resolve l = - let rec aux resolved acc = function - | [] -> resolved, acc - | [a] -> resolved, a :: acc - | a :: b :: r -> - if equal_atoms a b then - aux resolved (a :: acc) r - else if equal_atoms St.(a.neg) b then - aux (St.(a.var.tag.pa) :: resolved) acc r - else - aux resolved (a :: acc) (b :: r) - in - let resolved, new_clause = aux [] [] l in - resolved, List.rev new_clause - - (* List.sort_uniq is only since 4.02.0 *) - let sort_uniq compare l = - let rec aux = function - | x :: ((y :: _) as r) -> if compare x y = 0 then aux r else x :: aux r - | l -> l - in - aux (List.sort compare l) - - let to_list c = - let v = St.(c.atoms) in - let l = ref [] in - for i = 0 to Vec.size v - 1 do - l := (Vec.get v i) :: !l - done; - let res = sort_uniq compare_atoms !l in - let l, _ = resolve res in - if l <> [] then - L.debug 3 "Input clause is a tautology"; - res - - (* Adding hyptoheses *) - let has_been_proved c = H.mem proof (to_list c) - - let is_proved (c, cl) = - if H.mem proof cl then - true - else if not St.(c.learnt) then begin - H.add proof cl Assumption; - true - end else match St.(c.cpremise) with - | St.Lemma p -> H.add proof cl (Lemma p); true - | St.History _ -> false - - let is_proven c = is_proved (c, to_list c) - - let add_res (c, cl_c) (d, cl_d) = - L.debug 7 " Resolving clauses :"; - L.debug 7 " %a" St.pp_clause c; - L.debug 7 " %a" St.pp_clause d; - assert (is_proved (c, cl_c)); - assert (is_proved (d, cl_d)); - let l = merge cl_c cl_d in - let resolved, new_clause = resolve l in - match resolved with - | [] -> raise (Resolution_error "No literal to resolve over") - | [a] -> - H.add proof new_clause (Resolution (a, (c, cl_c), (d, cl_d))); - let new_c = St.make_clause (fresh_pcl_name ()) new_clause (List.length new_clause) true St.(History [c; d]) in - L.debug 5 "New clause : %a" St.pp_clause new_c; - new_c, new_clause - | _ -> raise (Resolution_error "Resolved to a tautology") - - let rec diff_learnt acc l l' = - match l, l' with - | [], _ -> l' @ acc - | a :: r, b :: r' -> - if equal_atoms a b then - diff_learnt acc r r' - else - diff_learnt (b :: acc) l r' - | _ -> raise (Resolution_error "Impossible to derive correct clause") - - let clause_unit a = match St.(a.var.level, a.var.tag.reason) with - | 0, St.Bcp Some c -> c, to_list c - | _ -> - raise (Resolution_error "Could not find a reason needed to resolve") - - let need_clause (c, cl) = - if is_proved (c, cl) then - [] - else - match St.(c.cpremise) with - | St.History l -> l - | St.Lemma _ -> assert false - - let rec add_clause c cl l = (* We assume that all clauses in l are already proved ! *) - match l with - | a :: r -> - L.debug 5 "Resolving (with history) %a" St.pp_clause c; - let temp_c, temp_cl = List.fold_left add_res a r in - L.debug 10 " Switching to unit resolutions"; - let new_c, new_cl = (ref temp_c, ref temp_cl) in - while not (equal_cl cl !new_cl) do - let unit_to_use = diff_learnt [] cl !new_cl in - let unit_r = List.map (fun a -> clause_unit a) unit_to_use in - do_clause (List.map fst unit_r); - let temp_c, temp_cl = List.fold_left add_res (!new_c, !new_cl) unit_r in - new_c := temp_c; - new_cl := temp_cl; - done - | _ -> assert false - - and do_clause = function - | [] -> () - | c :: r -> - let cl = to_list c in - match need_clause (c, cl) with - | [] -> do_clause r - | history -> - let history_cl = List.rev_map (fun c -> c, to_list c) history in - let to_prove = List.filter (fun (c, cl) -> not (is_proved (c, cl))) history_cl in - let to_prove = (List.rev_map fst to_prove) in - begin match to_prove with - | [] -> - add_clause c cl history_cl; - do_clause r - | _ -> do_clause (to_prove @ (c :: r)) - end - - let prove c = - L.debug 3 "Proving : %a" St.pp_clause c; - do_clause [c]; - L.debug 3 "Proved : %a" St.pp_clause c - - let rec prove_unsat_cl (c, cl) = match cl with - | [] -> true - | a :: r -> - L.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c; - let d = match St.(a.var.level, a.var.tag.reason) with - | 0, St.Bcp Some d -> d - | _ -> raise Exit - in - prove d; - let cl_d = to_list d in - prove_unsat_cl (add_res (c, cl) (d, cl_d)) - - let prove_unsat_cl c = - try - prove_unsat_cl c - with Exit -> - false - - let learn v = - Vec.iter (fun c -> L.debug 15 "history : %a" St.pp_clause c) v; - Vec.iter prove v - - let assert_can_prove_unsat c = - L.debug 1 "=================== Proof ====================="; - prove c; - if not (prove_unsat_cl (c, to_list c)) then - raise Insuficient_hyps - - (* Interface exposed *) - type proof_node = { - conclusion : clause; - step : step; - } - and proof = unit -> proof_node - and step = - | Hypothesis - | Lemma of lemma - | Resolution of proof * proof * atom - - let rec return_proof (c, cl) () = - L.debug 8 "Returning proof for : %a" St.pp_clause c; - let st = match H.find proof cl with - | Assumption -> Hypothesis - | Lemma l -> Lemma l - | Resolution (a, cl_c, cl_d) -> - Resolution (return_proof cl_c, return_proof cl_d, a) - in - { conclusion = c; step = st } - - let prove_unsat c = - assert_can_prove_unsat c; - return_proof (St.empty_clause, []) - - (* Compute unsat-core *) - let compare_cl c d = - let rec aux = function - | [], [] -> 0 - | a :: r, a' :: r' -> begin match compare_atoms a a' with - | 0 -> aux (r, r') - | x -> x - end - | _ :: _ , [] -> -1 - | [], _ :: _ -> 1 - in - aux (to_list c, to_list d) - - let unsat_core proof = - let rec aux acc proof = - let p = proof () in - match p.step with - | Hypothesis | Lemma _ -> p.conclusion :: acc - | Resolution (proof1, proof2, _) -> - aux (aux acc proof1) proof2 - in - sort_uniq compare_cl (aux [] proof) - - (* Print proof graph *) - let _i = ref 0 - let new_id () = incr _i; "id_" ^ (string_of_int !_i) - - let ids : (clause, (bool * string)) Hashtbl.t = Hashtbl.create 1007;; - let c_id c = - try - snd (Hashtbl.find ids c) - with Not_found -> - let id = new_id () in - Hashtbl.add ids c (false, id); - id - - let clear_ids () = - Hashtbl.iter (fun c (_, id) -> Hashtbl.replace ids c (false, id)) ids - - let is_drawn c = - ignore (c_id c); - fst (Hashtbl.find ids c) - - let has_drawn c = - if not (is_drawn c) then - let b, id = Hashtbl.find ids c in - Hashtbl.replace ids c (true, id) - else - () - - (* We use a custom function instead of the functions in Solver_type, - so that atoms are sorted before printing. *) - let print_clause fmt c = print_cl fmt (to_list c) - - let print_dot_rule opt f arg fmt cl = - Format.fprintf fmt "%s [shape=plaintext, label=<%a
>];@\n" - (c_id cl) "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\"" opt f arg - - let print_dot_edge id_c fmt id_d = - Format.fprintf fmt "%s -> %s;@\n" id_c id_d - - let print_res_atom id fmt a = - Format.fprintf fmt "%s [label=\"%a\"]" id St.print_atom a - - let print_res_node concl p1 p2 fmt atom = - let id = new_id () in - Format.fprintf fmt "%a;@\n%a%a%a" - (print_res_atom id) atom - (print_dot_edge (c_id concl)) id - (print_dot_edge id) (c_id p1) - (print_dot_edge id) (c_id p2) - - let color s = match s.[0] with - | 'E' -> "BGCOLOR=\"GREEN\"" - | 'L' -> "BGCOLOR=\"GREEN\"" - | _ -> "BGCOLOR=\"GREY\"" - - let rec print_dot_proof fmt p = - if not (is_drawn p.conclusion) then begin - has_drawn p.conclusion; - match p.step with - | Hypothesis -> - let aux fmt () = - Format.fprintf fmt "%aHypothesis%s" - print_clause p.conclusion St.(p.conclusion.name) - in - print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion - | Lemma proof -> - let name, f_args, t_args, color = St.proof_debug proof in - let color = match color with None -> "YELLOW" | Some c -> c in - let aux fmt () = - Format.fprintf fmt "%a%s" - print_clause p.conclusion color (max (List.length f_args + List.length t_args) 1) name; - if f_args <> [] then - Format.fprintf fmt "%a%a%a" St.print_atom (List.hd f_args) - (fun fmt -> List.iter (fun a -> Format.fprintf fmt "%a" St.print_atom a)) (List.tl f_args) - (fun fmt -> List.iter (fun v -> Format.fprintf fmt "%a" St.print_semantic_var v)) t_args - else if t_args <> [] then - Format.fprintf fmt "%a%a" St.print_semantic_var (List.hd t_args) - (fun fmt -> List.iter (fun v -> Format.fprintf fmt "%a" St.print_semantic_var v)) (List.tl t_args) - else - Format.fprintf fmt "" - in - print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion - | Resolution (proof1, proof2, a) -> - let aux fmt () = - Format.fprintf fmt "%a%s%s" - print_clause p.conclusion - "Resolution" St.(p.conclusion.name) - in - let p1 = proof1 () in - let p2 = proof2 () in - Format.fprintf fmt "%a%a%a%a" - (print_dot_rule (color p.conclusion.St.name) aux ()) p.conclusion - (print_res_node p.conclusion p1.conclusion p2.conclusion) a - print_dot_proof p1 - print_dot_proof p2 - end - - let print_dot fmt proof = - clear_ids (); - Format.fprintf fmt "digraph proof {@\n%a@\n}@." print_dot_proof (proof ()) - -end - diff --git a/solver/mcproof.mli b/solver/mcproof.mli deleted file mode 100644 index cb7b2167..00000000 --- a/solver/mcproof.mli +++ /dev/null @@ -1,13 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module type S = Res_intf.S - -module Make : - functor (L : Log_intf.S) -> - functor (St : Mcsolver_types.S) -> - S with type atom = St.atom and type clause = St.clause and type lemma = St.proof -(** Functor to create a module building proofs from a sat-solver unsat trace. *) diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index bce4b6bc..5e63946d 100644 --- a/solver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -7,917 +7,13 @@ Copyright 2014 Simon Cruanes module Make (L : Log_intf.S)(E : Expr_intf.S) (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) = struct - module St = Mcsolver_types.Make(L)(E)(Th) - module Proof = Mcproof.Make(L)(St) + module St = Solver_types.Make(L)(E)(Th) - open St + module M = Internal.Make(L)(St)(Th) - exception Sat - exception Unsat - exception Restart - exception Conflict of clause + include St - (* a push/pop state *) - type user_level = { - ul_trail : int; (* height of the decision trail *) - ul_clauses : int; (* number of clauses *) - ul_learnt : int; (* number of learnt clauses *) - } + include M - (* Singleton type containing the current state *) - type env = { - - mutable is_unsat : bool; - (* if [true], constraints are already false *) - - mutable unsat_conflict : clause option; - (* conflict clause at decision level 0, if any *) - - clauses : clause Vec.t; - (* all currently active clauses *) - - learnts : clause Vec.t; - (* learnt clauses *) - - mutable clause_inc : float; - (* increment for clauses' activity *) - - mutable var_inc : float; - (* increment for variables' activity *) - - trail : (semantic var, atom) Either.t Vec.t; - (* decision stack + propagated atoms *) - - trail_lim : int Vec.t; - (* decision levels in [trail] *) - - user_levels : user_level Vec.t; - (* user-defined levels, for {!push} and {!pop} *) - - mutable qhead : int; - (* Start offset in the queue of unit facts to propagate, within the trail *) - - mutable simpDB_assigns : int; - (* number of toplevel assignments since last call to [simplify ()] *) - - mutable simpDB_props : int; - (* remaining number of propagations before the next call to [simplify ()] *) - - order : Iheap.t; - (* Heap ordered by variable activity *) - - mutable progress_estimate : float; - (* progression estimate, updated by [search ()] *) - - remove_satisfied : bool; - - var_decay : float; - (* inverse of the activity factor for variables. Default 1/0.999 *) - - clause_decay : float; - (* inverse of the activity factor for clauses. Default 1/0.95 *) - - mutable restart_first : int; - (* intial restart limit, default 100 *) - - restart_inc : float; - (* multiplicative factor for restart limit, default 1.5 *) - - mutable learntsize_factor : float; - (* initial limit for the number of learnt clauses, 1/3 of initial - number of clauses by default *) - - learntsize_inc : float; - (* multiplicative factor for [learntsize_factor] at each restart, default 1.1 *) - - expensive_ccmin : bool; - (* control minimization of conflict clause, default true *) - - polarity_mode : bool; - (* default polarity for decision *) - - mutable starts : int; - mutable decisions : int; - mutable propagations : int; - mutable conflicts : int; - mutable clauses_literals : int; - mutable learnts_literals : int; - mutable max_literals : int; - mutable tot_literals : int; - mutable nb_init_clauses : int; - mutable tenv_queue : Th.level Vec.t; - mutable tatoms_qhead : int; - } - - let env = { - is_unsat = false; - unsat_conflict = None; - clauses = Vec.make 0 dummy_clause; (*updated during parsing*) - learnts = Vec.make 0 dummy_clause; (*updated during parsing*) - clause_inc = 1.; - var_inc = 1.; - trail = Vec.make 601 (Either.mk_right dummy_atom); - trail_lim = Vec.make 601 (-1); - user_levels = Vec.make 20 {ul_trail=0;ul_learnt=0;ul_clauses=0}; - qhead = 0; - simpDB_assigns = -1; - simpDB_props = 0; - order = Iheap.init 0; (* updated in solve *) - progress_estimate = 0.; - remove_satisfied = true; - var_decay = 1. /. 0.95; - clause_decay = 1. /. 0.999; - restart_first = 100; - restart_inc = 1.5; - learntsize_factor = 1. /. 3. ; - learntsize_inc = 1.1; - expensive_ccmin = true; - polarity_mode = false; - starts = 0; - decisions = 0; - propagations = 0; - conflicts = 0; - clauses_literals = 0; - learnts_literals = 0; - max_literals = 0; - tot_literals = 0; - nb_init_clauses = 0; - tenv_queue = Vec.make 100 Th.dummy; - tatoms_qhead = 0; - } - - (* Misc functions *) - let to_float i = float_of_int i - let to_int f = int_of_float f - - (* Accessors for variables *) - let get_var_id v = v.vid - let get_var_level v = v.level - let get_var_weight v = v.weight - - let set_var_weight v w = v.weight <- w - let set_var_level v l = v.level <- l - - let get_elt_id e = Either.destruct e get_var_id get_var_id - let get_elt_weight e = Either.destruct e get_var_weight get_var_weight - let get_elt_level e = Either.destruct e get_var_level get_var_level - - let set_elt_weight e = Either.destruct e set_var_weight set_var_weight - let set_elt_level e = Either.destruct e set_var_level set_var_level - - let f_weight i j = - get_elt_weight (St.get_var j) < get_elt_weight (St.get_var i) - - let f_filter i = - get_elt_level (St.get_var i) < 0 - - (* Var/clause activity *) - let insert_var_order e = Either.destruct e - (fun v -> Iheap.insert f_weight env.order v.vid) - (fun v -> - Iheap.insert f_weight env.order v.vid; - iter_sub (fun t -> Iheap.insert f_weight env.order t.vid) v - ) - - let var_decay_activity () = - env.var_inc <- env.var_inc *. env.var_decay - - let clause_decay_activity () = - env.clause_inc <- env.clause_inc *. env.clause_decay - - let var_bump_activity_aux v = - v.weight <- v.weight +. env.var_inc; - if v.weight > 1e100 then begin - for i = 0 to (St.nb_vars ()) - 1 do - set_elt_weight (St.get_var i) ((get_elt_weight (St.get_var i)) *. 1e-100) - done; - env.var_inc <- env.var_inc *. 1e-100; - end; - if Iheap.in_heap env.order v.vid then - Iheap.decrease f_weight env.order v.vid - - let var_bump_activity v = - var_bump_activity_aux v; - iter_sub (fun t -> var_bump_activity_aux t) v - - let clause_bump_activity c = - c.activity <- c.activity +. env.clause_inc; - if c.activity > 1e20 then begin - for i = 0 to (Vec.size env.learnts) - 1 do - (Vec.get env.learnts i).activity <- - (Vec.get env.learnts i).activity *. 1e-20; - done; - env.clause_inc <- env.clause_inc *. 1e-20 - end - - (* Convenient access *) - let decision_level () = Vec.size env.trail_lim - - let nb_assigns () = Vec.size env.trail - let nb_clauses () = Vec.size env.clauses - let nb_learnts () = Vec.size env.learnts - let nb_vars () = St.nb_vars () - - let new_decision_level() = - Vec.push env.trail_lim (Vec.size env.trail); - Vec.push env.tenv_queue (Th.current_level ()); (* save the current tenv *) - L.debug 5 "New decision level : %d (%d in env queue)(%d in trail)" - (Vec.size env.trail_lim) (Vec.size env.tenv_queue) (Vec.size env.trail); - () - - let attach_clause c = - Vec.push (Vec.get c.atoms 0).neg.watched c; - Vec.push (Vec.get c.atoms 1).neg.watched c; - L.debug 8 "%a <-- %a" St.pp_atom (Vec.get c.atoms 0).neg St.pp_clause c; - L.debug 8 "%a <-- %a" St.pp_atom (Vec.get c.atoms 1).neg St.pp_clause 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 detach_clause c = - c.removed <- true; - (* - 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 - - let satisfied c = - Vec.exists (fun atom -> atom.is_true) c.atoms - - (* cancel down to [lvl] excluded *) - let cancel_until lvl = - L.debug 1 "Backtracking to decision level %d (excluded)" lvl; - if decision_level () > lvl then begin - env.qhead <- Vec.get env.trail_lim lvl; - env.tatoms_qhead <- env.qhead; - for c = env.qhead to Vec.size env.trail - 1 do - Either.destruct (Vec.get env.trail c) - (fun v -> - v.tag.assigned <- None; - v.level <- -1; - insert_var_order (Either.mk_left v) - ) - (fun a -> - if a.var.level <= lvl then begin - Vec.set env.trail env.qhead (Either.mk_right a); - env.qhead <- env.qhead + 1 - end else begin - a.is_true <- false; - a.neg.is_true <- false; - a.var.level <- -1; - a.var.tag.reason <- Bcp None; - insert_var_order (Either.mk_right a.var) - end) - done; - Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *) - Vec.shrink env.trail ((Vec.size env.trail) - env.qhead); - Vec.shrink env.trail_lim ((Vec.size env.trail_lim) - lvl); - Vec.shrink env.tenv_queue ((Vec.size env.tenv_queue) - lvl); - end; - assert (Vec.size env.trail_lim = Vec.size env.tenv_queue) - - let report_unsat ({atoms=atoms} as confl) = - L.debug 5 "Unsat conflict : %a" St.pp_clause confl; - env.unsat_conflict <- Some confl; - env.is_unsat <- true; - raise Unsat - - let enqueue_bool a lvl reason = - assert (not a.neg.is_true); - if a.is_true then - L.debug 10 "Litteral %a already in queue" pp_atom a - else begin - assert (a.var.level < 0 && a.var.tag.reason = Bcp None && lvl >= 0); - a.is_true <- true; - a.var.level <- lvl; - a.var.tag.reason <- reason; - Vec.push env.trail (Either.mk_right a); - L.debug 2 "Enqueue (%d): %a" (nb_assigns ()) pp_atom a - end - - let enqueue_assign v value lvl = - v.tag.assigned <- Some value; - v.level <- lvl; - Vec.push env.trail (Either.mk_left v); - L.debug 2 "Enqueue (%d): %a" (nb_assigns ()) St.pp_semantic_var v - - let th_eval a = - if a.is_true || a.neg.is_true then None - else match Th.eval a.lit with - | Th.Unknown -> None - | Th.Valued (b, lvl) -> - let atom = if b then a else a.neg in - enqueue_bool atom lvl (Semantic lvl); - Some b - - (* conflict analysis *) - let max_lvl_atoms l = - List.fold_left (fun (max_lvl, acc) a -> - if a.var.level = max_lvl then (max_lvl, a :: acc) - else if a.var.level > max_lvl then (a.var.level, [a]) - else (max_lvl, acc)) (0, []) l - - let backtrack_lvl is_uip = function - | [] -> 0 - | a :: r when not is_uip -> max (a.var.level - 1) 0 - | a :: [] -> 0 - | a :: b :: r -> assert(a.var.level <> b.var.level); b.var.level - - let analyze c_clause = - let tr_ind = ref (Vec.size env.trail) in - let is_uip = ref false in - let c = ref (Proof.to_list c_clause) in - let history = ref [c_clause] in - clause_bump_activity c_clause; - let is_semantic a = match a.var.tag.reason with - | Semantic _ -> true - | _ -> false - in - try while true do - let lvl, atoms = max_lvl_atoms !c in - L.debug 15 "Current conflict clause :"; - List.iter (fun a -> L.debug 15 " |- %a" St.pp_atom a) !c; - if lvl = 0 then raise Exit; - match atoms with - | [] | _ :: [] -> - L.debug 15 "Found UIP clause"; - is_uip := true; - raise Exit - | _ when List.for_all is_semantic atoms -> - L.debug 15 "Found Semantic backtrack clause"; - raise Exit - | _ -> - decr tr_ind; - L.debug 20 "Looking at trail element %d" !tr_ind; - Either.destruct (Vec.get env.trail !tr_ind) - (fun v -> L.debug 15 "%a" St.pp_semantic_var v) - (fun a -> match a.var.tag.reason with - | Bcp (Some d) -> - L.debug 15 "Propagation : %a" St.pp_atom a; - L.debug 15 " |- %a" St.pp_clause d; - let tmp, res = Proof.resolve (Proof.merge !c (Proof.to_list d)) in - begin match tmp with - | [] -> L.debug 15 "No lit to resolve over." - | [b] when b == a.var.tag.pa -> - clause_bump_activity d; - var_bump_activity a.var; - history := d :: !history; - c := res - | _ -> assert false - end - | Bcp None -> L.debug 15 "Decision : %a" St.pp_atom a - | Semantic _ -> L.debug 15 "Semantic propagation : %a" St.pp_atom a) - done; assert false - with Exit -> - let learnt = List.sort (fun a b -> Pervasives.compare b.var.level a.var.level) !c in - let blevel = backtrack_lvl !is_uip learnt in - blevel, learnt, !history, !is_uip - - (* - while !cond do - if !c.learnt then clause_bump_activity !c; - history := !c :: !history; - (* visit the current predecessors *) - for j = 0 to Vec.size !c.atoms - 1 do - let q = Vec.get !c.atoms j in - (*printf "I visit %a@." D1.atom q;*) - assert (q.is_true || q.neg.is_true && q.var.level >= 0); (* Pas sur *) - if not q.var.tag.seen && q.var.level > 0 then begin - var_bump_activity q.var; - q.var.tag.seen <- true; - seen := q :: !seen; - if q.var.level >= decision_level () then begin - incr pathC - end else begin - learnt := q :: !learnt; - incr size; - blevel := max !blevel q.var.level - end - end - done; - - (* look for the next node to expand *) - while not (Vec.get env.trail !tr_ind).var.seen do decr tr_ind done; - decr pathC; - let p = Vec.get env.trail !tr_ind in - decr tr_ind; - match !pathC, p.var.reason with - | 0, _ -> - cond := false; - learnt := p.neg :: (List.rev !learnt) - | n, None -> assert false - | n, Some cl -> c := cl - done; - List.iter (fun q -> q.var.seen <- false) !seen; - *) - - let record_learnt_clause confl blevel learnt history is_uip = - begin match learnt with - | [] -> assert false - | [fuip] -> - assert (blevel = 0); - if fuip.neg.is_true then - report_unsat confl - else begin - let name = fresh_lname () in - let uclause = make_clause name learnt (List.length learnt) true history in - L.debug 1 "Unit clause learnt : %a" St.pp_clause uclause; - Vec.push env.learnts uclause; - enqueue_bool fuip 0 (Bcp (Some uclause)) - end - | fuip :: _ -> - let name = fresh_lname () in - let lclause = make_clause name learnt (List.length learnt) true history in - L.debug 2 "New clause learnt : %a" St.pp_clause lclause; - Vec.push env.learnts lclause; - attach_clause lclause; - clause_bump_activity lclause; - if is_uip then - enqueue_bool fuip blevel (Bcp (Some lclause)) - else begin - env.decisions <- env.decisions + 1; - new_decision_level(); - enqueue_bool fuip.neg (decision_level ()) (Bcp None) - end - end; - var_decay_activity (); - clause_decay_activity () - - let add_boolean_conflict confl = - env.conflicts <- env.conflicts + 1; - if decision_level() = 0 || Vec.for_all (fun a -> a.var.level = 0) confl.atoms then - report_unsat confl; (* Top-level conflict *) - let blevel, learnt, history, is_uip = analyze confl in - cancel_until blevel; - record_learnt_clause confl blevel learnt (History history) is_uip - - (* Add a new clause *) - exception Trivial - - let simplify_zero atoms init0 = - (* TODO: could be more efficient than [@] everywhere? *) - assert (decision_level () = 0); - let aux (atoms, init) a = - if a.is_true then raise Trivial; - if a.neg.is_true then - atoms, false - else - a::atoms, init - in - let atoms, init = List.fold_left aux ([], true) atoms in - List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init - - let partition atoms init0 = - let rec partition_aux trues unassigned falses init = function - | [] -> trues @ unassigned @ falses, init - | a :: r -> - if a.is_true then - if a.var.level = 0 then raise Trivial - else (a::trues) @ unassigned @ falses @ r, init - else if a.neg.is_true then - if a.var.level = 0 then - partition_aux trues unassigned falses false r - else - partition_aux trues unassigned (a::falses) init r - else - partition_aux trues (a::unassigned) falses init r - in - if decision_level () = 0 then - simplify_zero atoms init0 - else - partition_aux [] [] [] true atoms - - let add_clause name atoms history = - if env.is_unsat then raise Unsat; (* is it necessary ? *) - let init_name = name in - let init0 = make_clause init_name atoms (List.length atoms) (history <> History []) history in - L.debug 10 "Adding clause : %a" St.pp_clause init0; - try - if Proof.has_been_proved init0 then raise Trivial; - assert (Proof.is_proven init0); (* Important side-effect, DO NOT REMOVE *) - let atoms, init = partition atoms init0 in - let size = List.length atoms in - match atoms with - | [] -> - report_unsat init0; - | a::b::_ -> - let name = fresh_name () in - let clause = - if init then init0 - else make_clause name atoms size true (History [init0]) - in - L.debug 1 "New clause : %a" St.pp_clause clause; - attach_clause clause; - Vec.push env.clauses clause; - if a.neg.is_true then begin - let lvl = List.fold_left (fun m a -> max m a.var.level) 0 atoms in - cancel_until lvl; - add_boolean_conflict clause - end else if b.neg.is_true && not a.is_true && not a.neg.is_true then begin - let lvl = List.fold_left (fun m a -> max m a.var.level) 0 atoms in - cancel_until lvl; - enqueue_bool a lvl (Bcp (Some clause)) - end - | [a] -> - cancel_until 0; - enqueue_bool a 0 (Bcp (Some init0)) - with Trivial -> () - - let progress_estimate () = - let prg = ref 0. in - let nbv = to_float (nb_vars()) in - let lvl = decision_level () in - let _F = 1. /. nbv in - for i = 0 to lvl do - let _beg = if i = 0 then 0 else Vec.get env.trail_lim (i-1) in - let _end = if i=lvl then Vec.size env.trail else Vec.get env.trail_lim i in - prg := !prg +. _F**(to_float i) *. (to_float (_end - _beg)) - done; - !prg /. nbv - - let propagate_in_clause a c i watched new_sz = - let atoms = c.atoms in - let first = Vec.get atoms 0 in - if first == a.neg then begin (* false lit must be at index 1 *) - Vec.set atoms 0 (Vec.get atoms 1); - Vec.set atoms 1 first - end; - let first = Vec.get atoms 0 in - if first.is_true then begin - (* true clause, keep it in watched *) - Vec.set watched !new_sz c; - incr new_sz; - end - else - try (* look for another watch lit *) - for k = 2 to Vec.size atoms - 1 do - let ak = Vec.get atoms k in - if not (ak.neg.is_true) then begin - (* watch lit found: update and exit *) - Vec.set atoms 1 ak; - Vec.set atoms k a.neg; - Vec.push ak.neg.watched c; - L.debug 8 "New watcher (%a) for clause : %a" St.pp_atom ak.neg St.pp_clause c; - raise Exit - end - done; - (* no watch lit found *) - if first.neg.is_true || (th_eval first = Some false) then begin - (* clause is false *) - env.qhead <- Vec.size env.trail; - for k = i to Vec.size watched - 1 do - Vec.set watched !new_sz (Vec.get watched k); - incr new_sz; - done; - L.debug 3 "Conflict found : %a" St.pp_clause c; - raise (Conflict c) - end else begin - (* clause is unit *) - Vec.set watched !new_sz c; - incr new_sz; - L.debug 5 "Unit clause : %a" St.pp_clause c; - enqueue_bool first (decision_level ()) (Bcp (Some c)) - end - with Exit -> () - - let propagate_atom a res = - L.debug 8 "Propagating %a" St.pp_atom a; - let watched = a.watched in - L.debug 10 "Watching %a :" St.pp_atom a; - Vec.iter (fun c -> L.debug 10 " %a" St.pp_clause c) watched; - let new_sz_w = ref 0 in - begin - try - for i = 0 to Vec.size watched - 1 do - let c = Vec.get watched i in - if not c.removed then propagate_in_clause a c i watched new_sz_w - done; - with Conflict c -> - assert (!res = None); - res := Some c - end; - let dead_part = Vec.size watched - !new_sz_w in - Vec.shrink watched dead_part - - (* Propagation (boolean and theory) *) - let new_atom f = - let a = add_atom f in - L.debug 10 "New atom : %a" St.pp_atom a; - ignore (th_eval a); - a - - let slice_get i = Either.destruct (Vec.get env.trail i) - (function {level; tag={term; assigned = Some v}} -> Th.Assign (term, v), level | _ -> assert false) - (fun a -> Th.Lit a.lit, a.var.level) - - let slice_push l lemma = - let atoms = List.rev_map (fun x -> new_atom x) l in - Iheap.grow_to_by_double env.order (St.nb_vars ()); - List.iter (fun a -> insert_var_order (Either.mk_right a.var)) atoms; - add_clause (fresh_tname ()) atoms (Lemma lemma) - - let slice_propagate f lvl = - let a = add_atom f in - Iheap.grow_to_by_double env.order (St.nb_vars ()); - enqueue_bool a lvl (Semantic lvl) - - let current_slice () = Th.({ - start = env.tatoms_qhead; - length = (Vec.size env.trail) - env.tatoms_qhead; - get = slice_get; - push = slice_push; - propagate = slice_propagate; - }) - - let full_slice tag = Th.({ - start = 0; - length = Vec.size env.trail; - get = slice_get; - push = (fun cl proof -> tag := true; slice_push cl proof); - propagate = (fun _ -> assert false); - }) - - let rec theory_propagate () = - let slice = current_slice () in - env.tatoms_qhead <- nb_assigns (); - match Th.assume slice with - | Th.Sat -> - propagate () - | Th.Unsat (l, p) -> - let l = List.rev_map new_atom l in - Iheap.grow_to_by_double env.order (St.nb_vars ()); - List.iter (fun a -> insert_var_order (Either.mk_right a.var)) l; - let c = St.make_clause (St.fresh_tname ()) l (List.length l) true (Lemma p) in - Some c - - and propagate () = - if env.qhead = Vec.size env.trail then - None - else begin - let num_props = ref 0 in - let res = ref None in - while env.qhead < Vec.size env.trail do - Either.destruct (Vec.get env.trail env.qhead) - (fun a -> ()) - (fun a -> - incr num_props; - propagate_atom a res); - env.qhead <- env.qhead + 1 - done; - env.propagations <- env.propagations + !num_props; - env.simpDB_props <- env.simpDB_props - !num_props; - match !res with - | None -> theory_propagate () - | _ -> !res - end - - (* heuristic comparison between clauses, by their size (unary/binary or not) - and activity *) - let f_sort_db c1 c2 = - let sz1 = Vec.size c1.atoms in - let sz2 = Vec.size c2.atoms in - let c = compare c1.activity c2.activity in - if sz1 = sz2 && c = 0 then 0 - else - if sz1 > 2 && (sz2 = 2 || c < 0) then -1 - else 1 - -(* returns true if the clause is used as a reason for a propagation, - and therefore can be needed in case of conflict. In this case - the clause can't be forgotten *) - let locked c = false (* - Vec.exists - (fun v -> match v.reason with - | Some c' -> c ==c' - | _ -> false - ) env.vars - *) - - (* remove some learnt clauses *) - let reduce_db () = () (* - let extra_lim = env.clause_inc /. (to_float (Vec.size env.learnts)) in - Vec.sort env.learnts f_sort_db; - let lim2 = Vec.size env.learnts in - let lim1 = lim2 / 2 in - let j = ref 0 in - 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 - 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 - else - begin Vec.set env.learnts !j c; incr j end - done; - Vec.shrink env.learnts (lim2 - !j) - *) - - (* remove from [vec] the clauses that are satisfied in the current trail *) - 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 - done - - module HUC = Hashtbl.Make - (struct type t = clause let equal = (==) let hash = Hashtbl.hash end) - - let simplify () = - assert (decision_level () = 0); - if env.is_unsat then raise Unsat; - begin - match propagate () with - | Some confl -> report_unsat confl - | None -> () - end; - if nb_assigns() <> env.simpDB_assigns && env.simpDB_props <= 0 then begin - if Vec.size env.learnts > 0 then remove_satisfied env.learnts; - if env.remove_satisfied then remove_satisfied env.clauses; - (*Iheap.filter env.order f_filter f_weight;*) - env.simpDB_assigns <- nb_assigns (); - env.simpDB_props <- env.clauses_literals + env.learnts_literals; - end - - (* Decide on a new litteral *) - let rec pick_branch_lit () = - let max = Iheap.remove_min f_weight env.order in - Either.destruct (St.get_var max) - (fun v -> - if v.level >= 0 then - pick_branch_lit () - else begin - let value = Th.assign v.tag.term in - env.decisions <- env.decisions + 1; - new_decision_level(); - let current_level = decision_level () in - L.debug 5 "Deciding on %a" St.pp_semantic_var v; - enqueue_assign v value current_level - end) - (fun v -> - if v.level >= 0 then begin - assert (v.tag.pa.is_true || v.tag.na.is_true); - pick_branch_lit () - end else match Th.eval v.tag.pa.lit with - | Th.Unknown -> - env.decisions <- env.decisions + 1; - new_decision_level(); - let current_level = decision_level () in - L.debug 5 "Deciding on %a" St.pp_atom v.tag.pa; - enqueue_bool v.tag.pa current_level (Bcp None) - | Th.Valued (b, lvl) -> - let a = if b then v.tag.pa else v.tag.na in - enqueue_bool a lvl (Semantic lvl)) - - let search n_of_conflicts n_of_learnts = - let conflictC = ref 0 in - env.starts <- env.starts + 1; - while (true) do - match propagate () with - | Some confl -> (* Conflict *) - incr conflictC; - add_boolean_conflict confl - - | None -> (* No Conflict *) - if nb_assigns() = St.nb_vars () (* env.nb_init_vars *) then raise Sat; - if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then begin - L.debug 1 "Restarting..."; - env.progress_estimate <- progress_estimate(); - cancel_until 0; - raise Restart - end; - if decision_level() = 0 then simplify (); - - if n_of_learnts >= 0 && - Vec.size env.learnts - nb_assigns() >= n_of_learnts then - reduce_db(); - - pick_branch_lit () - done - - let check_clause c = - let b = ref false in - let atoms = c.atoms in - for i = 0 to Vec.size atoms - 1 do - let a = Vec.get atoms i in - b := !b || a.is_true - done; - assert (!b) - - let check_vec vec = - for i = 0 to Vec.size vec - 1 do check_clause (Vec.get vec i) done - - let add_clauses cnf = - let aux cl = - add_clause (fresh_hname ()) cl (History []); - match propagate () with - | None -> () | Some confl -> report_unsat confl - in - List.iter aux cnf - - (* fixpoint of propagation and decisions until a model is found, or a - conflict is reached *) - let solve () = - if env.is_unsat then raise Unsat; - let n_of_conflicts = ref (to_float env.restart_first) in - let n_of_learnts = ref ((to_float (nb_clauses())) *. env.learntsize_factor) in - try - while true do - begin try - search (to_int !n_of_conflicts) (to_int !n_of_learnts) - with - | Restart -> - n_of_conflicts := !n_of_conflicts *. env.restart_inc; - n_of_learnts := !n_of_learnts *. env.learntsize_inc - | Sat -> - let tag = ref false in - Th.if_sat (full_slice tag); - if not !tag then raise Sat - end - done - with - | Sat -> () - - let init_solver cnf = - let nbv = St.nb_vars () in - let nbc = env.nb_init_clauses + List.length cnf in - Iheap.grow_to_by_double env.order nbv; - (* List.iter (List.iter (fun a -> insert_var_order a.var)) cnf; *) - St.iter_vars insert_var_order; - Vec.grow_to_by_double env.clauses nbc; - Vec.grow_to_by_double env.learnts nbc; - env.nb_init_clauses <- nbc; - St.iter_vars (fun e -> Either.destruct e - (fun v -> L.debug 50 " -- %a" St.pp_semantic_var v) - (fun a -> L.debug 50 " -- %a" St.pp_atom a.tag.pa) - ); - add_clauses cnf - - let assume cnf = - let cnf = List.rev_map (List.rev_map St.add_atom) cnf in - init_solver cnf - - let eval lit = - let var, negated = make_boolean_var lit in - assert (var.tag.pa.is_true || var.tag.na.is_true); - let truth = var.tag.pa.is_true in - if negated then not truth else truth - - let hyps () = env.clauses - - let history () = env.learnts - - let unsat_conflict () = env.unsat_conflict - - let model () = - let opt = function Some a -> a | None -> assert false in - Vec.fold (fun acc e -> Either.destruct e - (fun v -> (v.tag.term, opt v.tag.assigned) :: acc) - (fun _ -> acc) - ) [] env.trail - - (* Push/Pop *) - type level = int - - let base_level = 0 - - let current_level () = Vec.size env.user_levels - - let push () = - let ul_trail = if Vec.is_empty env.trail_lim - then base_level - else Vec.last env.trail_lim - and ul_clauses = Vec.size env.clauses - and ul_learnt = Vec.size env.learnts in - Vec.push env.user_levels {ul_trail; ul_clauses;ul_learnt}; - Vec.size env.user_levels - - let pop l = - if l > current_level() - then invalid_arg "cannot pop() to level, it is too high"; - let ul = Vec.get env.user_levels l in - (* see whether we can reset [env.is_unsat] *) - if env.is_unsat && not (Vec.is_empty env.trail_lim) then ( - (* level at which the decision that lead to unsat was made *) - let last = Vec.last env.trail_lim in - if ul.ul_trail < last then env.is_unsat <- false - ); - cancel_until ul.ul_trail; - Vec.shrink env.clauses ul.ul_clauses; - Vec.shrink env.learnts ul.ul_learnt; - () - - let clear () = pop base_level end diff --git a/solver/mcsolver.mli b/solver/mcsolver.mli index d0e657dd..58ac31cc 100644 --- a/solver/mcsolver.mli +++ b/solver/mcsolver.mli @@ -6,11 +6,11 @@ Copyright 2014 Simon Cruanes module Make (L : Log_intf.S)(E : Expr_intf.S) (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) : sig - (** Functor to create a McSolver parametrised by the atomic formulas and a theory. *) + (** Functor to create a solver parametrised by the atomic formulas and a theory. *) exception Unsat - module St : Mcsolver_types.S + module St : Solver_types.S with type term = E.Term.t and type formula = E.Formula.t @@ -24,7 +24,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) @return () if the current set of clauses is satisfiable @raise Unsat if a toplevel conflict is found *) - val assume : E.Formula.t list list -> unit + val assume : ?tag:int -> E.Formula.t list list -> unit (** Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place. @raise Unsat if a conflict is detect when adding the clauses *) diff --git a/solver/mcsolver_types.ml b/solver/mcsolver_types.ml deleted file mode 100644 index 0d5765bd..00000000 --- a/solver/mcsolver_types.ml +++ /dev/null @@ -1,275 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -open Printf - -module type S = Mcsolver_types_intf.S - -module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with - type formula = E.Formula.t and type term = E.Term.t) = struct - - (* Types declarations *) - - type term = E.Term.t - type formula = E.Formula.t - type proof = Th.proof - - type 'a var = - { vid : int; - tag : 'a; - mutable weight : float; - mutable level : int; } - - type semantic = - { term : term; - mutable assigned : term option; } - - type boolean = { - pa : atom; - na : atom; - mutable reason : reason; - } - - and atom = - { var : boolean var; - lit : formula; - neg : atom; - mutable watched : clause Vec.t; - mutable is_true : bool; - aid : int } - - and clause = - { name : string; - atoms : atom Vec.t ; - mutable activity : float; - mutable removed : bool; - learnt : bool; - cpremise : premise } - - and reason = - | Semantic of int - | Bcp of clause option - - and premise = - | History of clause list - | Lemma of proof - - type elt = (semantic var, boolean var) Either.t - - (* Dummy values *) - let dummy_lit = E.dummy - - let rec dummy_var = - { vid = -101; - level = -1; - weight = -1.; - tag = { - pa = dummy_atom; - na = dummy_atom; - reason = Bcp None; }; - } - and dummy_atom = - { var = dummy_var; - lit = dummy_lit; - watched = Obj.magic 0; - (* should be [Vec.make_empty dummy_clause] - but we have to break the cycle *) - neg = dummy_atom; - is_true = false; - aid = -102 } - let dummy_clause = - { name = ""; - atoms = Vec.make_empty dummy_atom; - activity = -1.; - removed = false; - learnt = false; - cpremise = History [] } - - let () = - dummy_atom.watched <- Vec.make_empty dummy_clause - - (* Constructors *) - module MF = Hashtbl.Make(E.Formula) - module MT = Hashtbl.Make(E.Term) - - let f_map = MF.create 4096 - let t_map = MT.create 4096 - - let vars = Vec.make 107 (Either.mk_right dummy_var) - let nb_vars () = Vec.size vars - let get_var i = Vec.get vars i - let iter_vars f = Vec.iter f vars - - let cpt_mk_var = ref 0 - - let make_semantic_var t = - try MT.find t_map t - with Not_found -> - let res = { - vid = !cpt_mk_var; - weight = 1.; - level = -1; - tag = { - term = t; - assigned = None; }; - } in - incr cpt_mk_var; - MT.add t_map t res; - Vec.push vars (Either.mk_left res); - res - - let make_boolean_var = - fun lit -> - let lit, negated = E.norm lit in - try MF.find f_map lit, negated - with Not_found -> - let cpt_fois_2 = !cpt_mk_var lsl 1 in - let rec var = - { vid = !cpt_mk_var; - level = -1; - weight = 0.; - tag = { - pa = pa; - na = na; - reason = Bcp None;}; - } - and pa = - { var = var; - lit = lit; - watched = Vec.make 10 dummy_clause; - neg = na; - is_true = false; - aid = cpt_fois_2 (* aid = vid*2 *) } - and na = - { var = var; - lit = E.neg lit; - watched = Vec.make 10 dummy_clause; - neg = pa; - is_true = false; - aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in - MF.add f_map lit var; - incr cpt_mk_var; - Vec.push vars (Either.mk_right var); - Th.iter_assignable (fun t -> ignore (make_semantic_var t)) lit; - var, negated - - let add_term t = make_semantic_var t - - let add_atom lit = - let var, negated = make_boolean_var lit in - if negated then var.tag.na else var.tag.pa - - let make_clause name ali sz_ali is_learnt premise = - let atoms = Vec.from_list ali sz_ali dummy_atom in - { name = name; - atoms = atoms; - removed = false; - learnt = is_learnt; - activity = 0.; - cpremise = premise} - - let empty_clause = make_clause "Empty" [] 0 false (History []) - - (* Name generation *) - let fresh_lname = - let cpt = ref 0 in - fun () -> incr cpt; "L" ^ (string_of_int !cpt) - - let fresh_hname = - let cpt = ref 0 in - fun () -> incr cpt; "H" ^ (string_of_int !cpt) - - let fresh_tname = - let cpt = ref 0 in - fun () -> incr cpt; "T" ^ (string_of_int !cpt) - - let fresh_name = - let cpt = ref 0 in - fun () -> incr cpt; "C" ^ (string_of_int !cpt) - - (* Iteration over subterms *) - module Mi = Map.Make(struct type t = int let compare= Pervasives.compare end) - let iter_map = ref Mi.empty - - let iter_sub f v = - try - List.iter f (Mi.find v.vid !iter_map) - with Not_found -> - let l = ref [] in - Th.iter_assignable (fun t -> l := add_term t :: !l) v.tag.pa.lit; - iter_map := Mi.add v.vid !l !iter_map; - List.iter f !l - - (* Proof debug info *) - let proof_debug p = - let name, l, l', color = Th.proof_debug p in - name, (List.map add_atom l), (List.map add_term l'), color - - (* Pretty printing for atoms and clauses *) - let print_semantic_var fmt v = E.Term.print fmt v.tag.term - - let print_atom fmt a = E.Formula.print fmt a.lit - - let print_atoms fmt v = - print_atom fmt (Vec.get v 0); - if (Vec.size v) > 1 then begin - for i = 1 to (Vec.size v) - 1 do - Format.fprintf fmt " ∨ %a" print_atom (Vec.get v i) - done - end - - let print_clause fmt c = - Format.fprintf fmt "%s : %a" c.name print_atoms c.atoms - - (* Complete debug printing *) - let sign a = if a==a.var.tag.pa then "" else "-" - - let level a = - match a.var.level, a.var.tag.reason with - | n, _ when n < 0 -> assert false - | 0, Bcp (Some c) -> sprintf "->0/%s" c.name - | 0, Bcp None -> "@0" - | n, Bcp (Some c) -> sprintf "->%d/%s" n c.name - | n, Bcp None -> sprintf "@@%d" n - | n, Semantic lvl -> sprintf "::%d/%d" n lvl - - let value a = - if a.is_true then sprintf "[T%s]" (level a) - else if a.neg.is_true then sprintf "[F%s]" (level a) - else "[]" - - let pp_premise b = function - | History v -> List.iter (fun {name=name} -> bprintf b "%s," name) v - | Lemma _ -> bprintf b "th_lemma" - - let pp_assign b = function - | None -> () - | Some t -> bprintf b "[assignment: %s]" (Log.on_fmt E.Term.print t) - - let pp_semantic_var b v = - bprintf b "%d [lit:%s]%a" - (v.vid+1) (Log.on_fmt E.Term.print v.tag.term) pp_assign v.tag.assigned - - let pp_atom b a = - bprintf b "%s%d%s[lit:%s]" - (sign a) (a.var.vid+1) (value a) (Log.on_fmt E.Formula.print a.lit) - - let pp_atoms_vec b vec = - for i = 0 to Vec.size vec - 1 do - bprintf b "%a ; " pp_atom (Vec.get vec i) - done - - let pp_clause b {name=name; atoms=arr; cpremise=cp; learnt=learnt} = - bprintf b "%s%s{ %a} cpremise={{%a}}" name (if learnt then "!" else ":") pp_atoms_vec arr pp_premise cp - -end diff --git a/solver/mcsolver_types.mli b/solver/mcsolver_types.mli deleted file mode 100644 index a10ae5f5..00000000 --- a/solver/mcsolver_types.mli +++ /dev/null @@ -1,21 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -module type S = Mcsolver_types_intf.S - -module Make : - functor (L : Log_intf.S) -> - functor (E : Expr_intf.S) -> - functor (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) -> - S with type term = E.Term.t and type formula = E.Formula.t and type proof = Th.proof -(** Functor to instantiate the types of clauses for the Solver. *) diff --git a/solver/mcsolver_types_intf.ml b/solver/mcsolver_types_intf.ml deleted file mode 100644 index f22b8256..00000000 --- a/solver/mcsolver_types_intf.ml +++ /dev/null @@ -1,112 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -module type S = sig - (** The signatures of clauses used in the Solver. *) - - type term - type formula - type proof - - type 'a var = - { vid : int; - tag : 'a; - mutable weight : float; - mutable level : int; } - - type semantic = - { term : term; - mutable assigned : term option; } - - type boolean = { - pa : atom; - na : atom; - mutable reason : reason; - } - - and atom = { - var : boolean var; - lit : formula; - neg : atom; - mutable watched : clause Vec.t; - mutable is_true : bool; - aid : int - } - - and clause = { - name : string; - atoms : atom Vec.t; - mutable activity : float; - mutable removed : bool; - learnt : bool; - cpremise : premise - } - - and reason = - | Semantic of int - | Bcp of clause option - and premise = - | History of clause list - | Lemma of proof - - type elt = (semantic var, boolean var) Either.t - (** Recursive types for literals (atoms) and clauses *) - - val dummy_var : boolean var - val dummy_atom : atom - val dummy_clause : clause - (** Dummy values for use in vector dummys *) - - val nb_vars : unit -> int - val get_var : int -> elt - val iter_vars : (elt -> unit) -> unit - (** Read access to the vector of variables created *) - - val add_atom : formula -> atom - (** Returns the atom associated with the given formula *) - val add_term : term -> semantic var - (** Returns the variable associated with the term *) - val make_boolean_var : formula -> boolean var * bool - (** Returns the variable linked with the given formula, and wether the atom associated with the formula - is [var.pa] or [var.na] *) - - val iter_sub : (semantic var -> unit) -> boolean var -> unit - (** Iterates over the semantic var corresponding to subterms of the fiven literal, according - to Th.iter_assignable *) - - val empty_clause : clause - (** The empty clause *) - val make_clause : string -> atom list -> int -> bool -> premise -> clause - (** [make_clause name atoms size learnt premise] creates a clause with the given attributes. *) - - val fresh_name : unit -> string - val fresh_lname : unit -> string - val fresh_tname : unit -> string - val fresh_hname : unit -> string - (** Fresh names for clauses *) - - val proof_debug : proof -> string * (atom list) * (semantic var list) * (string option) - (** Debugging info for proofs (see Plugin_intf). *) - - val print_atom : Format.formatter -> atom -> unit - val print_semantic_var : Format.formatter -> semantic var -> unit - val print_clause : Format.formatter -> clause -> unit - (** Pretty printing functions for atoms and clauses *) - - val pp_atom : Buffer.t -> atom -> unit - val pp_semantic_var : Buffer.t -> semantic var -> unit - val pp_clause : Buffer.t -> clause -> unit - (** Debug function for atoms and clauses (very verbose) *) - -end - diff --git a/solver/res.ml b/solver/res.ml index f8615def..84a3594c 100644 --- a/solver/res.ml +++ b/solver/res.ml @@ -64,7 +64,7 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct if equal_atoms a b then aux resolved (a :: acc) r else if equal_atoms St.(a.neg) b then - aux (St.(a.var.pa) :: resolved) acc r + aux (St.(a.var.tag.pa) :: resolved) acc r else aux resolved (a :: acc) (b :: r) in @@ -85,9 +85,10 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct for i = 0 to Vec.size v - 1 do l := (Vec.get v i) :: !l done; - let l, res = resolve (sort_uniq compare_atoms !l) in + let res = sort_uniq compare_atoms !l in + let l, _ = resolve res in if l <> [] then - raise (Resolution_error "Input clause is a tautology"); + L.debug 3 "Input clause is a tautology"; res (* Adding hyptoheses *) @@ -132,8 +133,8 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct diff_learnt (b :: acc) l r' | _ -> raise (Resolution_error "Impossible to derive correct clause") - let clause_unit a = match St.(a.var.level, a.var.reason) with - | 0, Some c -> c, to_list c + let clause_unit a = match St.(a.var.level, a.var.tag.reason) with + | 0, St.Bcp Some c -> c, to_list c | _ -> raise (Resolution_error "Could not find a reason needed to resolve") @@ -188,8 +189,8 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct | [] -> true | a :: r -> L.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c; - let d = match St.(a.var.level, a.var.reason) with - | 0, Some d -> d + let d = match St.(a.var.level, a.var.tag.reason) with + | 0, St.Bcp Some d -> d | _ -> raise Exit in prove d; @@ -324,10 +325,21 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct print_clause p.conclusion St.(p.conclusion.name) in print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion - | Lemma _ -> + | Lemma proof -> + let name, f_args, t_args, color = St.proof_debug proof in + let color = match color with None -> "YELLOW" | Some c -> c in let aux fmt () = - Format.fprintf fmt "%aLemma%s" - print_clause p.conclusion St.(p.conclusion.name) + Format.fprintf fmt "%a%s" + print_clause p.conclusion color (max (List.length f_args + List.length t_args) 1) name; + if f_args <> [] then + Format.fprintf fmt "%a%a%a" St.print_atom (List.hd f_args) + (fun fmt -> List.iter (fun a -> Format.fprintf fmt "%a" St.print_atom a)) (List.tl f_args) + (fun fmt -> List.iter (fun v -> Format.fprintf fmt "%a" St.print_semantic_var v)) t_args + else if t_args <> [] then + Format.fprintf fmt "%a%a" St.print_semantic_var (List.hd t_args) + (fun fmt -> List.iter (fun v -> Format.fprintf fmt "%a" St.print_semantic_var v)) (List.tl t_args) + else + Format.fprintf fmt "" in print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion | Resolution (proof1, proof2, a) -> diff --git a/solver/res.mli b/solver/res.mli index 306a724d..657937e7 100644 --- a/solver/res.mli +++ b/solver/res.mli @@ -9,5 +9,5 @@ module type S = Res_intf.S module Make : functor (L : Log_intf.S) -> functor (St : Solver_types.S) -> - S with type atom= St.atom and type clause = St.clause and type lemma = St.proof + S with type atom = St.atom and type clause = St.clause and type lemma = St.proof (** Functor to create a module building proofs from a sat-solver unsat trace. *) diff --git a/solver/solver.ml b/solver/solver.ml index c40ee0f0..59c42889 100644 --- a/solver/solver.ml +++ b/solver/solver.ml @@ -10,6 +10,84 @@ (* *) (**************************************************************************) +module Make (L : Log_intf.S)(E : Formula_intf.S) + (Th : Theory_intf.S with type formula = E.t) = struct + + module Expr = struct + module Term = E + module Formula = E + include E + end + + module Plugin = struct + type term = E.t + type formula = E.t + type proof = Th.proof + + type assumption = + | Lit of formula + | Assign of term * term + + type slice = { + start : int; + length : int; + get : int -> assumption * int; + push : formula list -> proof -> unit; + propagate : formula -> int -> unit; + } + + type level = Th.level + + type res = + | Sat + | Unsat of formula list * proof + + type eval_res = + | Valued of bool * int + | Unknown + + let dummy = Th.dummy + + let current_level = Th.current_level + + let assume s = match Th.assume { + Th.start = s.start; + Th.length = s.length; + Th.get = (function i -> match s.get i with + | Lit f, _ -> f | _ -> assert false); + Th.push = s.push; + } with + | Th.Sat _ -> Sat + | Th.Unsat (l, p) -> Unsat (l, p) + + let backtrack = Th.backtrack + + let assign t = + Format.printf "Error : %a@." Expr.Term.print t; + assert false + + let iter_assignable _ _ = () + + let eval _ = Unknown + + let if_sat _ = () + + let proof_debug _ = assert false + end + + module St = struct + module M = Solver_types.Make(L)(Expr)(Plugin) + include M + let mcsat = false + end + + module S = Internal.Make(L)(St)(Plugin) + + include S + +end + +(* module Make (L : Log_intf.S)(F : Formula_intf.S) (Th : Theory_intf.S with type formula = F.t) = struct @@ -775,4 +853,4 @@ module Make (L : Log_intf.S)(F : Formula_intf.S) let clear () = pop base_level end - +*) diff --git a/solver/solver_types.ml b/solver/solver_types.ml index 974ced65..24a869bc 100644 --- a/solver/solver_types.ml +++ b/solver/solver_types.ml @@ -15,23 +15,38 @@ open Printf module type S = Solver_types_intf.S -module Make (F : Formula_intf.S)(Th : Theory_intf.S) = struct +module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with + type formula = E.Formula.t and type term = E.Term.t) = struct - type formula = F.t + (* Flag for Mcsat v.s Pure Sat *) + let mcsat = true + + (* Types declarations *) + + type term = E.Term.t + type formula = E.Formula.t type proof = Th.proof - type var = - { vid : int; - pa : atom; - na : atom; - mutable weight : float; - mutable seen : bool; - mutable level : int; - mutable reason: reason; - mutable vpremise : premise} + type 'a var = + { vid : int; + tag : 'a; + mutable weight : float; + mutable level : int; + mutable seen : bool; + } + + type semantic = + { term : term; + mutable assigned : term option; } + + type boolean = { + pa : atom; + na : atom; + mutable reason : reason; + } and atom = - { var : var; + { var : boolean var; lit : formula; neg : atom; mutable watched : clause Vec.t; @@ -47,23 +62,29 @@ module Make (F : Formula_intf.S)(Th : Theory_intf.S) = struct learnt : bool; cpremise : premise } - and reason = clause option + and reason = + | Semantic of int + | Bcp of clause option and premise = | History of clause list | Lemma of proof - let dummy_lit = F.dummy + type elt = (semantic var, boolean var) Either.t + + (* Dummy values *) + let dummy_lit = E.dummy let rec dummy_var = { vid = -101; - pa = dummy_atom; - na = dummy_atom; level = -1; - reason = None; weight = -1.; seen = false; - vpremise = History [] } + tag = { + pa = dummy_atom; + na = dummy_atom; + reason = Bcp None; }; + } and dummy_atom = { var = dummy_var; lit = dummy_lit; @@ -73,7 +94,6 @@ module Make (F : Formula_intf.S)(Th : Theory_intf.S) = struct neg = dummy_atom; is_true = false; aid = -102 } - let dummy_clause = { name = ""; tag = None; @@ -86,33 +106,52 @@ module Make (F : Formula_intf.S)(Th : Theory_intf.S) = struct let () = dummy_atom.watched <- Vec.make_empty dummy_clause - module MA = Map.Make(F) + (* Constructors *) + module MF = Hashtbl.Make(E.Formula) + module MT = Hashtbl.Make(E.Term) - let normal_form = F.norm - - let ma = ref MA.empty - let vars = Vec.make 107 dummy_var + let f_map = MF.create 4096 + let t_map = MT.create 4096 + let vars = Vec.make 107 (Either.mk_right dummy_var) let nb_vars () = Vec.size vars let get_var i = Vec.get vars i let iter_vars f = Vec.iter f vars let cpt_mk_var = ref 0 - let make_var = + + let make_semantic_var t = + try MT.find t_map t + with Not_found -> + let res = { + vid = !cpt_mk_var; + weight = 1.; + level = -1; + seen = false; + tag = { + term = t; + assigned = None; }; + } in + incr cpt_mk_var; + MT.add t_map t res; + Vec.push vars (Either.mk_left res); + res + + let make_boolean_var = fun lit -> - let lit, negated = normal_form lit in - try MA.find lit !ma, negated + let lit, negated = E.norm lit in + try MF.find f_map lit, negated with Not_found -> let cpt_fois_2 = !cpt_mk_var lsl 1 in let rec var = { vid = !cpt_mk_var; - pa = pa; - na = na; level = -1; - reason = None; weight = 0.; seen = false; - vpremise = History []; + tag = { + pa = pa; + na = na; + reason = Bcp None;}; } and pa = { var = var; @@ -123,20 +162,22 @@ module Make (F : Formula_intf.S)(Th : Theory_intf.S) = struct aid = cpt_fois_2 (* aid = vid*2 *) } and na = { var = var; - lit = F.neg lit; + lit = E.neg lit; watched = Vec.make 10 dummy_clause; neg = pa; is_true = false; aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in - ma := MA.add lit var !ma; + MF.add f_map lit var; incr cpt_mk_var; - Vec.push vars var; - assert (Vec.get vars var.vid == var && !cpt_mk_var = Vec.size vars); + Vec.push vars (Either.mk_right var); + Th.iter_assignable (fun t -> ignore (make_semantic_var t)) lit; var, negated + let add_term t = make_semantic_var t + let add_atom lit = - let var, negated = make_var lit in - if negated then var.na else var.pa + let var, negated = make_boolean_var lit in + if negated then var.tag.na else var.tag.pa let make_clause ?tag name ali sz_ali is_learnt premise = let atoms = Vec.from_list ali sz_ali dummy_atom in @@ -150,24 +191,45 @@ module Make (F : Formula_intf.S)(Th : Theory_intf.S) = struct let empty_clause = make_clause "Empty" [] 0 false (History []) + (* Name generation *) let fresh_lname = let cpt = ref 0 in fun () -> incr cpt; "L" ^ (string_of_int !cpt) - let fresh_dname = + let fresh_hname = let cpt = ref 0 in - fun () -> incr cpt; "D" ^ (string_of_int !cpt) + fun () -> incr cpt; "H" ^ (string_of_int !cpt) + + let fresh_tname = + let cpt = ref 0 in + fun () -> incr cpt; "T" ^ (string_of_int !cpt) let fresh_name = let cpt = ref 0 in fun () -> incr cpt; "C" ^ (string_of_int !cpt) - let clear () = - cpt_mk_var := 0; - ma := MA.empty + (* Iteration over subterms *) + module Mi = Map.Make(struct type t = int let compare= Pervasives.compare end) + let iter_map = ref Mi.empty + + let iter_sub f v = + try + List.iter f (Mi.find v.vid !iter_map) + with Not_found -> + let l = ref [] in + Th.iter_assignable (fun t -> l := add_term t :: !l) v.tag.pa.lit; + iter_map := Mi.add v.vid !l !iter_map; + List.iter f !l + + (* Proof debug info *) + let proof_debug p = + let name, l, l', color = Th.proof_debug p in + name, (List.map add_atom l), (List.map add_term l'), color (* Pretty printing for atoms and clauses *) - let print_atom fmt a = F.print fmt a.lit + let print_semantic_var fmt (v: semantic var) = E.Term.print fmt v.tag.term + + let print_atom fmt a = E.Formula.print fmt a.lit let print_atoms fmt v = print_atom fmt (Vec.get v 0); @@ -181,29 +243,37 @@ module Make (F : Formula_intf.S)(Th : Theory_intf.S) = struct Format.fprintf fmt "%s : %a" c.name print_atoms c.atoms (* Complete debug printing *) - let sign a = if a==a.var.pa then "" else "-" + let sign a = if a==a.var.tag.pa then "" else "-" let level a = - match a.var.level, a.var.reason with + match a.var.level, a.var.tag.reason with | n, _ when n < 0 -> assert false - | 0, Some c -> sprintf "->0/%s" c.name - | 0, None -> "@0" - | n, Some c -> sprintf "->%d/%s" n c.name - | n, None -> sprintf "@@%d" n + | 0, Bcp (Some c) -> sprintf "->0/%s" c.name + | 0, Bcp None -> "@0" + | n, Bcp (Some c) -> sprintf "->%d/%s" n c.name + | n, Bcp None -> sprintf "@@%d" n + | n, Semantic lvl -> sprintf "::%d/%d" n lvl let value a = if a.is_true then sprintf "[T%s]" (level a) else if a.neg.is_true then sprintf "[F%s]" (level a) - else "" + else "[]" let pp_premise b = function - | History v -> List.iter (fun {name=name} -> bprintf b "%s," name) v - | Lemma _ -> bprintf b "th_lemma" + | History v -> List.iter (fun {name=name} -> bprintf b "%s," name) v + | Lemma _ -> bprintf b "th_lemma" + + let pp_assign b = function + | None -> () + | Some t -> bprintf b "[assignment: %s]" (Log.on_fmt E.Term.print t) + + let pp_semantic_var b v = + bprintf b "%d [lit:%s]%a" + (v.vid+1) (Log.on_fmt E.Term.print v.tag.term) pp_assign v.tag.assigned let pp_atom b a = - bprintf b "%s%d%s [lit:%s] vpremise={{%a}}" - (sign a) (a.var.vid+1) (value a) (Log.on_fmt F.print a.lit) - pp_premise a.var.vpremise + bprintf b "%s%d%s[lit:%s]" + (sign a) (a.var.vid+1) (value a) (Log.on_fmt E.Formula.print a.lit) let pp_atoms_vec b vec = for i = 0 to Vec.size vec - 1 do diff --git a/solver/solver_types.mli b/solver/solver_types.mli index d4fa2200..658b3108 100644 --- a/solver/solver_types.mli +++ b/solver/solver_types.mli @@ -14,7 +14,9 @@ module type S = Solver_types_intf.S module Make : - functor (F : Formula_intf.S) -> - functor (Th : Theory_intf.S) -> - S with type formula = F.t and type proof = Th.proof -(** Functor to instantiate the types of clauses for the Solver. *) + functor (L : Log_intf.S) -> + functor (E : Expr_intf.S) -> + functor (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) -> + S with type term = E.Term.t and type formula = E.Formula.t and type proof = Th.proof +(** Functor to instantiate the types of clauses for a solver. *) + diff --git a/solver/solver_types_intf.ml b/solver/solver_types_intf.ml index 995df934..960d3743 100644 --- a/solver/solver_types_intf.ml +++ b/solver/solver_types_intf.ml @@ -14,22 +14,31 @@ module type S = sig (** The signatures of clauses used in the Solver. *) + val mcsat : bool + + type term type formula type proof - type var = { - vid : int; + type 'a var = + { vid : int; + tag : 'a; + mutable weight : float; + mutable level : int; + mutable seen : bool; } + + type semantic = + { term : term; + mutable assigned : term option; } + + type boolean = { pa : atom; na : atom; - mutable weight : float; - mutable seen : bool; - mutable level : int; mutable reason : reason; - mutable vpremise : premise } and atom = { - var : var; + var : boolean var; lit : formula; neg : atom; mutable watched : clause Vec.t; @@ -47,48 +56,59 @@ module type S = sig cpremise : premise } - and reason = clause option + and reason = + | Semantic of int + | Bcp of clause option and premise = | History of clause list | Lemma of proof + + type elt = (semantic var, boolean var) Either.t (** Recursive types for literals (atoms) and clauses *) - val dummy_var : var + val dummy_var : boolean var val dummy_atom : atom val dummy_clause : clause (** Dummy values for use in vector dummys *) - val empty_clause : clause - (** The empty clause *) + val nb_vars : unit -> int + val get_var : int -> elt + val iter_vars : (elt -> unit) -> unit + (** Read access to the vector of variables created *) val add_atom : formula -> atom (** Returns the atom associated with the given formula *) - - val make_var : formula -> var * bool + val add_term : term -> semantic var + (** Returns the variable associated with the term *) + val make_boolean_var : formula -> boolean var * bool (** Returns the variable linked with the given formula, and wether the atom associated with the formula is [var.pa] or [var.na] *) + val iter_sub : (semantic var -> unit) -> boolean var -> unit + (** Iterates over the semantic var corresponding to subterms of the fiven literal, according + to Th.iter_assignable *) + + val empty_clause : clause + (** The empty clause *) val make_clause : ?tag:int -> string -> atom list -> int -> bool -> premise -> clause (** [make_clause name atoms size learnt premise] creates a clause with the given attributes. *) - val nb_vars : unit -> int - val get_var : int -> var - val iter_vars : (var -> unit) -> unit - (** Read access to the vector of variables created *) - val fresh_name : unit -> string val fresh_lname : unit -> string - val fresh_dname : unit -> string + val fresh_tname : unit -> string + val fresh_hname : unit -> string (** Fresh names for clauses *) - val clear : unit -> unit - (** Forget all variables cretaed *) + val proof_debug : proof -> string * (atom list) * (semantic var list) * (string option) + (** Debugging info for proofs (see Plugin_intf). *) val print_atom : Format.formatter -> atom -> unit + val print_semantic_var : Format.formatter -> semantic var -> unit val print_clause : Format.formatter -> clause -> unit (** Pretty printing functions for atoms and clauses *) val pp_atom : Buffer.t -> atom -> unit + val pp_semantic_var : Buffer.t -> semantic var -> unit val pp_clause : Buffer.t -> clause -> unit (** Debug function for atoms and clauses (very verbose) *)