simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-22 01:06:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Big refactoring of code. Some performances were lost on pure SAT Solving.

Browse source
This commit is contained in:
Guillaume Bury 2015-06-25 15:34:39 +02:00
parent 23f627cae3
commit 6f384fb80b
16 changed files with 1292 additions and 1797 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
msat.mlpack
View file

@ -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

936
solver/internal.ml Normal file
View file

@ -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

65
solver/internal.mli Normal file
View file

@ -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

365
solver/mcproof.ml
View file

@ -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=<<TABLE %s %s>%a</TABLE>>];@\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 "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD>Hypothesis</TD><TD>%s</TD></TR>"
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 "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD BGCOLOR=\"%s\" rowspan=\"%d\">%s</TD>"
print_clause p.conclusion color (max (List.length f_args + List.length t_args) 1) name;
if f_args <> [] then
Format.fprintf fmt "<TD>%a</TD></TR>%a%a" St.print_atom (List.hd f_args)
(fun fmt -> List.iter (fun a -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_atom a)) (List.tl f_args)
(fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_semantic_var v)) t_args
else if t_args <> [] then
Format.fprintf fmt "<TD>%a</TD></TR>%a" St.print_semantic_var (List.hd t_args)
(fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_semantic_var v)) (List.tl t_args)
else
Format.fprintf fmt "<TD></TD></TR>"
in
print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion
| Resolution (proof1, proof2, a) ->
let aux fmt () =
Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD>%s</TD><TD>%s</TD></TR>"
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

13
solver/mcproof.mli
View file

@ -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. *)

912
solver/mcsolver.ml
View file

@ -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

6
solver/mcsolver.mli
View file

@ -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 *)

275
solver/mcsolver_types.ml
View file

@ -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

21
solver/mcsolver_types.mli
View file

@ -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. *)

112
solver/mcsolver_types_intf.ml
View file

@ -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

32
solver/res.ml
View file

@ -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 "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD BGCOLOR=\"YELLOW\">Lemma</TD><TD>%s</TD></TR>"
print_clause p.conclusion St.(p.conclusion.name)
Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD BGCOLOR=\"%s\" rowspan=\"%d\">%s</TD>"
print_clause p.conclusion color (max (List.length f_args + List.length t_args) 1) name;
if f_args <> [] then
Format.fprintf fmt "<TD>%a</TD></TR>%a%a" St.print_atom (List.hd f_args)
(fun fmt -> List.iter (fun a -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_atom a)) (List.tl f_args)
(fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_semantic_var v)) t_args
else if t_args <> [] then
Format.fprintf fmt "<TD>%a</TD></TR>%a" St.print_semantic_var (List.hd t_args)
(fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_semantic_var v)) (List.tl t_args)
else
Format.fprintf fmt "<TD></TD></TR>"
in
print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion
| Resolution (proof1, proof2, a) ->

2
solver/res.mli
View file

@ -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. *)

80
solver/solver.ml
View file

@ -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
*)

180
solver/solver_types.ml
View file

@ -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

10
solver/solver_types.mli
View file

@ -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. *)

62
solver/solver_types_intf.ml
View file

@ -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) *)