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

first draft of replacing push/pop by assumptions

Browse source
This commit is contained in:
Simon Cruanes 2016-07-27 16:40:36 +02:00
parent 09166d0370
commit 563e9027e1
7 changed files with 182 additions and 340 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

70
src/core/external.ml
View file

@ -6,6 +6,29 @@ Copyright 2016 Simon Cruanes
module type S = Solver_intf.S module type S = Solver_intf.S
type ('term, 'form) sat_state = ('term, 'form) Solver_intf.sat_state = {
eval: 'form -> bool;
(** Returns the valuation of a formula in the current state
of the sat solver.
@raise UndecidedLit if the literal is not decided *)
eval_level: 'form -> bool * int;
(** Return the current assignement of the literals, as well as its
decision level. If the level is 0, then it is necessary for
the atom to have this value; otherwise it is due to choices
that can potentially be backtracked.
@raise UndecidedLit if the literal is not decided *)
model: unit -> ('term * 'term) list;
(** Returns the model found if the formula is satisfiable. *)
}
type ('clause, 'proof) unsat_state = ('clause, 'proof) Solver_intf.unsat_state = {
unsat_conflict : unit -> 'clause;
(** Returns the unsat clause found at the toplevel *)
get_proof : unit -> 'proof;
(** returns a persistent proof of the empty clause from the Unsat result. *)
}
module Make module Make
(St : Solver_types.S) (St : Solver_types.S)
(Th : Plugin_intf.S with type term = St.term (Th : Plugin_intf.S with type term = St.term
@ -25,36 +48,35 @@ module Make
type clause = St.clause type clause = St.clause
type proof = Proof.proof type proof = Proof.proof
type res = Sat | Unsat type res =
| Sat of (St.term,St.formula) sat_state
| Unsat of (St.clause,Proof.proof) unsat_state
let assume ?tag l = let assume ?tag l = S.assume ?tag l
try S.assume ?tag l
with S.Unsat -> ()
let solve () = let mk_sat () : _ sat_state =
{ model=S.model; eval=S.eval; eval_level=S.eval_level }
let mk_unsat () : _ unsat_state =
let unsat_conflict () = match S.unsat_conflict () with
| None -> assert false
| Some c -> c
in
let get_proof () =
let c = unsat_conflict() in
S.Proof.prove_unsat c
in
{ unsat_conflict; get_proof; }
let solve ?assumptions () =
try try
S.solve (); S.solve ?assumptions ();
Sat Sat (mk_sat())
with S.Unsat -> Unsat with S.Unsat ->
Unsat (mk_unsat())
let eval = S.eval
let eval_level = S.eval_level
let get_proof () =
match S.unsat_conflict () with
| None -> assert false
| Some c -> S.Proof.prove_unsat c
let unsat_core = S.Proof.unsat_core let unsat_core = S.Proof.unsat_core
let get_tag cl = St.(cl.tag) let get_tag cl = St.(cl.tag)
(* Push/pop operations *)
type level = S.level
let base_level = S.base_level
let current_level = S.current_level
let push = S.push
let pop = S.pop
let reset = S.reset
end end

318
src/core/internal.ml
View file

@ -22,16 +22,6 @@ module Make
exception Restart exception Restart
exception Conflict of clause exception Conflict of clause
(* a push/pop state *)
type user_level = {
(* User levels always refer to decision_level 0 *)
ul_elt_lvl : int; (* Number of atoms in trail at decision level 0 *)
ul_th_lvl : int; (* Number of atoms known by the theory at decision level 0 *)
ul_th_env : Plugin.level; (* Theory state at level 0 *)
ul_clauses : int; (* number of clauses *)
ul_learnt : int; (* number of learnt clauses *)
}
(* Singleton type containing the current state *) (* Singleton type containing the current state *)
type env = { type env = {
@ -49,7 +39,7 @@ module Make
mutable unsat_conflict : clause option; mutable unsat_conflict : clause option;
(* conflict clause at decision level 0, if any *) (* conflict clause at [base_level], if any *)
mutable next_decision : atom option; mutable next_decision : atom option;
(* When the last conflict was a semantic one, this stores the next decision to make *) (* When the last conflict was a semantic one, this stores the next decision to make *)
@ -61,8 +51,6 @@ module Make
(* decision levels in [trail] *) (* decision levels in [trail] *)
th_levels : Plugin.level Vec.t; th_levels : Plugin.level Vec.t;
(* theory states corresponding to elt_levels *) (* theory states corresponding to elt_levels *)
user_levels : user_level Vec.t;
(* user-defined levels, for {!push} and {!pop} *)
mutable th_head : int; mutable th_head : int;
(* Start offset in the queue {!elt_queue} of (* Start offset in the queue {!elt_queue} of
@ -71,6 +59,10 @@ module Make
(* Start offset in the queue {!elt_queue} of (* Start offset in the queue {!elt_queue} of
unit facts to propagate, within the trail *) unit facts to propagate, within the trail *)
mutable base_level: int;
(* the decision level under which we cannot backtrack, that is,
the one after we pushed local assumptions *)
(* invariant: (* invariant:
- during propagation, th_head <= elt_head - during propagation, th_head <= elt_head
- then, once elt_head reaches length elt_queue, Th.assume is - then, once elt_head reaches length elt_queue, Th.assume is
@ -140,14 +132,7 @@ module Make
elt_queue = Vec.make 601 (of_atom dummy_atom); elt_queue = Vec.make 601 (of_atom dummy_atom);
elt_levels = Vec.make 601 (-1); elt_levels = Vec.make 601 (-1);
th_levels = Vec.make 100 Plugin.dummy; th_levels = Vec.make 100 Plugin.dummy;
base_level = 0;
user_levels = Vec.make 20 {
ul_elt_lvl = 0;
ul_th_lvl = 0;
ul_learnt = 0;
ul_clauses = 0;
ul_th_env = Plugin.dummy;
};
order = Iheap.init 0; order = Iheap.init 0;
@ -193,49 +178,6 @@ module Make
| Some _ -> true | Some _ -> true
| None -> false | None -> false
(* Level for push/pop operations *)
type level = int
(* Push/Pop *)
let current_level () = Vec.size env.user_levels
let push () : level =
if is_unsat () then
(* When unsat, pushing does nothing, since adding more assumptions
can not make the proof disappear. *)
current_level ()
else begin
(* The assumptions are sat, or at least not yet detected unsat,
we need to save enough to be able to restore the current decision
level 0. *)
let res = current_level () in
(* To restore decision level 0, we need the solver queue, and theory state. *)
let ul_elt_lvl, ul_th_lvl =
if Vec.is_empty env.elt_levels then
env.elt_head, env.th_head
else (
let l = Vec.get env.elt_levels 0 in
l, l
)
and ul_th_env =
if Vec.is_empty env.th_levels
then Plugin.current_level ()
else Vec.get env.th_levels 0
in
(* Keep in mind what are the current assumptions. *)
let ul_clauses = Vec.size env.clauses_hyps in
let ul_learnt = Vec.size env.clauses_learnt in
Vec.push env.user_levels {ul_elt_lvl; ul_th_lvl; ul_th_env; ul_clauses; ul_learnt;};
res
end
(* To store info for level 0, it is easier to push at module
initialisation, when there are no assumptions. *)
let base_level =
let l = push () in
assert (l = 0);
l
(* Iteration over subterms. (* Iteration over subterms.
When incrementing activity, we want to be able to iterate over When incrementing activity, we want to be able to iterate over
all subterms of a formula. However, the function provided by the theory all subterms of a formula. However, the function provided by the theory
@ -345,8 +287,8 @@ module Make
if a.neg.is_true then begin if a.neg.is_true then begin
(* If a variable is false, we need to see why it is false. *) (* If a variable is false, we need to see why it is false. *)
match a.var.reason with match a.var.reason with
| None | Some Decision -> assert false | None | Some Decision | Some Assumption -> assert false
(* The var must have a reason, and it cannot be a decision, since we are (* The var must have a reason, and it cannot be a decision/assumption, since we are
at level 0. *) at level 0. *)
| Some (Bcp cl) -> atoms, cl :: history | Some (Bcp cl) -> atoms, cl :: history
(* The variable has been set to false because of another clause, (* The variable has been set to false because of another clause,
@ -598,10 +540,10 @@ module Make
a UIP ("Unique Implication Point") a UIP ("Unique Implication Point")
precond: the atom list is sorted by decreasing decision level *) precond: the atom list is sorted by decreasing decision level *)
let backtrack_lvl ~is_uip : atom list -> int = function let backtrack_lvl ~is_uip : atom list -> int = function
| [] -> 0 | [] -> env.base_level
| [a] -> | [a] ->
assert is_uip; assert is_uip;
0 env.base_level
| a :: b :: r -> | a :: b :: r ->
if is_uip then ( if is_uip then (
(* backtrack below [a], so we can propagate [not a] *) (* backtrack below [a], so we can propagate [not a] *)
@ -609,7 +551,7 @@ module Make
b.var.v_level b.var.v_level
) else ( ) else (
assert (a.var.v_level = b.var.v_level); assert (a.var.v_level = b.var.v_level);
max (a.var.v_level - 1) 0 max (a.var.v_level - 1) env.base_level
) )
(* result of conflict analysis, containing the learnt clause and some (* result of conflict analysis, containing the learnt clause and some
@ -644,7 +586,7 @@ module Make
try try
while true do while true do
let lvl, atoms = max_lvl_atoms !c in let lvl, atoms = max_lvl_atoms !c in
if lvl = 0 then raise Exit; if lvl = env.base_level then raise Exit;
match atoms with match atoms with
| [] | [_] -> | [] | [_] ->
is_uip := true; is_uip := true;
@ -670,7 +612,7 @@ module Make
c := res c := res
| _ -> assert false | _ -> assert false
end end
| None | Some Decision | Some Semantic _ -> () | None | Some Decision | Some Assumption | Some Semantic _ -> ()
end end
done; assert false done; assert false
with Exit -> with Exit ->
@ -692,7 +634,7 @@ module Make
(* conflict analysis for SAT (* conflict analysis for SAT
Same idea as the mcsat analyze function (without semantic propagations), Same idea as the mcsat analyze function (without semantic propagations),
except we look the the Last UIP (TODO: check ?), and do it in an imperative except we look the the Last UIP (TODO: check ?), and do it in an imperative
and eficient manner. *) and efficient manner. *)
let analyze_sat c_clause : conflict_res = let analyze_sat c_clause : conflict_res =
let pathC = ref 0 in let pathC = ref 0 in
let learnt = ref [] in let learnt = ref [] in
@ -707,14 +649,14 @@ module Make
while !cond do while !cond do
begin match !c.cpremise with begin match !c.cpremise with
| History _ -> clause_bump_activity !c | History _ -> clause_bump_activity !c
| Hyp _ | Lemma _ -> () | Hyp | Lemma _ -> ()
end; end;
history := !c :: !history; history := !c :: !history;
(* visit the current predecessors *) (* visit the current predecessors *)
for j = 0 to Array.length !c.atoms - 1 do for j = 0 to Array.length !c.atoms - 1 do
let q = !c.atoms.(j) in let q = !c.atoms.(j) in
assert (q.is_true || q.neg.is_true && q.var.v_level >= 0); (* unsure? *) assert (q.is_true || q.neg.is_true && q.var.v_level >= env.base_level); (* unsure? *)
if q.var.v_level = 0 then begin if q.var.v_level <= env.base_level then begin
assert (q.neg.is_true); assert (q.neg.is_true);
match q.var.reason with match q.var.reason with
| Some Bcp cl -> history := cl :: !history | Some Bcp cl -> history := cl :: !history
@ -723,7 +665,7 @@ module Make
if not q.var.seen then begin if not q.var.seen then begin
q.var.seen <- true; q.var.seen <- true;
seen := q :: !seen; seen := q :: !seen;
if q.var.v_level > 0 then begin if q.var.v_level > env.base_level then begin
var_bump_activity q.var; var_bump_activity q.var;
if q.var.v_level >= decision_level () then begin if q.var.v_level >= decision_level () then begin
incr pathC incr pathC
@ -799,7 +741,8 @@ module Make
let add_boolean_conflict (confl:clause): unit = let add_boolean_conflict (confl:clause): unit =
env.next_decision <- None; env.next_decision <- None;
env.conflicts <- env.conflicts + 1; env.conflicts <- env.conflicts + 1;
if decision_level() = 0 || Array_util.for_all (fun a -> a.var.v_level = 0) confl.atoms then if decision_level() = 0
|| Array_util.for_all (fun a -> a.var.v_level <= env.base_level) confl.atoms then
report_unsat confl; (* Top-level conflict *) report_unsat confl; (* Top-level conflict *)
let cr = analyze confl in let cr = analyze confl in
cancel_until cr.cr_backtrack_lvl; cancel_until cr.cr_backtrack_lvl;
@ -809,9 +752,8 @@ module Make
the clause is false in the current trail *) the clause is false in the current trail *)
let add_clause ?(force=false) (init:clause) : unit = let add_clause ?(force=false) (init:clause) : unit =
Log.debugf 90 "Adding clause:@[<hov>%a@]" (fun k -> k St.pp_clause init); Log.debugf 90 "Adding clause:@[<hov>%a@]" (fun k -> k St.pp_clause init);
assert (init.c_level <= current_level ());
let vec = match init.cpremise with let vec = match init.cpremise with
| Hyp _ -> env.clauses_hyps | Hyp -> env.clauses_hyps
| Lemma _ -> env.clauses_learnt | Lemma _ -> env.clauses_learnt
| History _ -> assert false | History _ -> assert false
in in
@ -862,8 +804,7 @@ module Make
env.nb_init_clauses <- nbc; env.nb_init_clauses <- nbc;
while not (Stack.is_empty env.clauses_to_add) do while not (Stack.is_empty env.clauses_to_add) do
let c = Stack.pop env.clauses_to_add in let c = Stack.pop env.clauses_to_add in
if c.c_level <= current_level () then add_clause c
add_clause c
done done
end end
@ -1119,41 +1060,6 @@ module Make
let check_vec vec = Vec.iter check_clause vec let check_vec vec = Vec.iter check_clause vec
(* fixpoint of propagation and decisions until a model is found, or a
conflict is reached *)
let solve (): unit =
if 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 ->
assert (env.elt_head = Vec.size env.elt_queue);
Plugin.if_sat (full_slice ());
flush_clauses();
if is_unsat () then raise Unsat
else if env.elt_head = Vec.size env.elt_queue (* sanity check *)
&& env.elt_head = St.nb_elt ()
(* this is the important test to know if the search is finished *)
then raise Sat
end
done
with
| Sat -> ()
let assume ?tag cnf =
List.iter (fun l ->
let atoms = List.rev_map atom l in
let c = make_clause ?tag (fresh_hname ()) atoms (Hyp (current_level ())) in
Stack.push c env.clauses_to_add
) cnf
let eval_level lit = let eval_level lit =
let var, negated = make_boolean_var lit in let var, negated = make_boolean_var lit in
if not var.pa.is_true && not var.na.is_true if not var.pa.is_true && not var.na.is_true
@ -1168,10 +1074,6 @@ module Make
let eval lit = fst (eval_level lit) let eval lit = fst (eval_level lit)
let hyps () = env.clauses_hyps
let history () = env.clauses_learnt
let unsat_conflict () = env.unsat_conflict let unsat_conflict () = env.unsat_conflict
let model () : (term * term) list = let model () : (term * term) list =
@ -1182,119 +1084,77 @@ module Make
| Atom _ -> acc) | Atom _ -> acc)
[] env.elt_queue [] env.elt_queue
(* Backtrack to decision_level 0, with trail_lim && theory env specified *) (* push a series of assumptions to the stack *)
let reset_until push_lvl (ul: user_level) = let push_assumptions =
Log.debug 1 "Resetting to decision level 0 (pop/forced)"; List.iter
env.th_head <- ul.ul_th_lvl ; (fun lit ->
env.elt_head <- ul.ul_elt_lvl; let a = atom lit in
for c = env.elt_head to Vec.size env.elt_queue - 1 do if a.is_true then ()
match Vec.get env.elt_queue c with else if a.neg.is_true then (
| Lit l -> (* conflict between assumptions: UNSAT *)
l.assigned <- None; let c = make_clause (fresh_hname ()) [a] Hyp in
l.l_level <- -1; add_boolean_conflict c;
insert_var_order (elt_of_lit l) assert false (* should raise Unsat *)
| Atom a -> ) else (
begin match a.var.reason with (* make a decision, propagate *)
| Some Bcp { c_level } when c_level > push_lvl -> new_decision_level();
a.is_true <- false; let level = decision_level() in
a.neg.is_true <- false; assert (env.base_level = level-1);
a.var.v_level <- -1; env.base_level <- level;
a.var.reason <- None; enqueue_bool a ~level Assumption;
insert_var_order (elt_of_var a.var) match propagate () with
| _ -> | Some confl -> (* Conflict *)
if a.var.v_level = 0 then begin add_boolean_conflict confl;
(* [a] is still true, so we move it to the current top position assert false (* should raise Unsat *)
of the trail, as if it was propagated again *) | None -> ()
Vec.set env.elt_queue env.elt_head (of_atom a); ))
env.elt_head <- env.elt_head + 1
end else begin (* clear assumptions *)
a.is_true <- false; let pop_assumptions (): unit =
a.neg.is_true <- false; cancel_until 0;
a.var.v_level <- -1; env.base_level <- 0;
a.var.reason <- None;
insert_var_order (elt_of_var a.var)
end
end
done;
Plugin.backtrack ul.ul_th_env; (* recover the right theory env *)
Vec.shrink env.elt_queue ((Vec.size env.elt_queue) - env.elt_head);
Vec.clear env.elt_levels;
Vec.clear env.th_levels;
assert (Vec.size env.elt_levels = Vec.size env.th_levels);
assert (env.elt_head = Vec.size env.elt_queue);
() ()
let pop l: unit = (* fixpoint of propagation and decisions until a model is found, or a
(* Check sanity of pop *) conflict is reached *)
if l > current_level () then invalid_arg "cannot pop to level, it is too high" let solve ?(assumptions=[]) (): unit =
else if l < current_level () then begin if env.base_level > 0 then pop_assumptions();
if is_unsat () then raise Unsat;
(* Filter the current buffer of clauses to remove potential assumptions let n_of_conflicts = ref (to_float env.restart_first) in
with too high a user level, let n_of_learnts = ref ((to_float (nb_clauses())) *. env.learntsize_factor) in
or else, with later pushes, these assumptions might be added. *) push_assumptions assumptions;
let cl = ref [] in assert (env.base_level <= List.length assumptions);
Stack.iter (fun c -> try
if c.c_level <= l then cl := c :: !cl) env.clauses_to_add; while true do
Stack.clear env.clauses_to_add; begin try
List.iter (fun c -> Stack.push c env.clauses_to_add) !cl; search (to_int !n_of_conflicts) (to_int !n_of_learnts)
with
(* Get back the user level *) | Restart ->
let ul = Vec.get env.user_levels l in n_of_conflicts := !n_of_conflicts *. env.restart_inc;
Vec.shrink env.user_levels (max 0 (Vec.size env.user_levels - l - 1)); n_of_learnts := !n_of_learnts *. env.learntsize_inc
| Sat ->
(* It is quite hard to check wether unsat status can be kept, so in doubt, we remove it *) assert (env.elt_head = Vec.size env.elt_queue);
env.unsat_conflict <- None; Plugin.if_sat (full_slice ());
flush_clauses();
(* Backtrack to the level 0 with appropriate settings *) if is_unsat () then raise Unsat
reset_until l ul; else if env.elt_head = Vec.size env.elt_queue (* sanity check *)
&& env.elt_head = St.nb_elt ()
(* Log current assumptions for debugging purposes *) (* this is the important test to know if the search is finished *)
Log.debugf 99 "@[<v2>Current trail:@ %a@]" then raise Sat
(fun k->
let pp out () =
for i = 0 to Vec.size env.elt_queue - 1 do
Format.fprintf out "%s%s%d -- %a@,"
(if i = ul.ul_elt_lvl then "*" else " ")
(if i = ul.ul_th_lvl then "*" else " ")
i (fun fmt e ->
match e with
| Lit l -> St.pp_lit fmt l
| Atom a -> St.pp_atom fmt a)
(Vec.get env.elt_queue i)
done
in
k pp ());
(* Clear hypothesis not valid anymore *)
for i = ul.ul_clauses to Vec.size env.clauses_hyps - 1 do
let c = Vec.get env.clauses_hyps i in
assert (c.c_level > l);
detach_clause c
done;
Vec.shrink env.clauses_hyps (Vec.size env.clauses_hyps - ul.ul_clauses);
(* Refresh the known tautologies simplified because of clauses that have been removed *)
let s = Stack.create () in
let new_sz = ref ul.ul_learnt in
for i = ul.ul_learnt to Vec.size env.clauses_learnt - 1 do
let c = Vec.get env.clauses_learnt i in
if c.c_level > l then begin
detach_clause c;
match c.cpremise with
| Lemma _ -> Stack.push c s
| History ({ cpremise = Lemma _ } as c' :: _ ) -> Stack.push c' s
| _ -> () (* Only simplified clauses can have a level > 0 *)
end else begin
Log.debugf 15 "Keeping intact clause %a" (fun k->k St.pp_clause c);
Vec.set env.clauses_learnt !new_sz c;
incr new_sz
end end
done; done
Vec.shrink env.clauses_learnt (Vec.size env.clauses_learnt - !new_sz); with Sat -> ()
Stack.iter (add_clause ~force:true) s
end
let reset () = pop base_level let assume ?tag cnf =
List.iter
(fun l ->
let atoms = List.rev_map atom l in
let c = make_clause ?tag (fresh_hname ()) atoms Hyp in
Stack.push c env.clauses_to_add)
cnf
let hyps () = env.clauses_hyps
let history () = env.clauses_learnt
end end

30
src/core/internal.mli
View file

@ -18,9 +18,14 @@ module Make
module Proof : Res.S with module St = St module Proof : Res.S with module St = St
val solve : unit -> unit val solve :
?assumptions:St.formula list ->
unit ->
unit
(** Try and solves the current set of assumptions. (** Try and solves the current set of assumptions.
@return () if the current set of clauses is satisfiable @return () if the current set of clauses is satisfiable
@param assumptions list of additional local assumptions to make,
removed after the callback returns a value
@raise Unsat if a toplevel conflict is found *) @raise Unsat if a toplevel conflict is found *)
val assume : ?tag:int -> St.formula list list -> unit val assume : ?tag:int -> St.formula list list -> unit
@ -53,28 +58,5 @@ module Make
val model : unit -> (St.term * St.term) list val model : unit -> (St.term * St.term) list
(** Returns the model found if the formula is satisfiable. *) (** Returns the model found if the formula is satisfiable. *)
(** {2 Backtracking facilities} *)
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 reset : unit -> unit
(** Return to level {!base_level} *)
end end

69
src/core/solver_intf.ml
View file

@ -4,6 +4,28 @@ Copyright 2016 Guillaume Bury
Copyright 2016 Simon Cruanes Copyright 2016 Simon Cruanes
*) *)
type ('term, 'form) sat_state = {
eval: 'form -> bool;
(** Returns the valuation of a formula in the current state
of the sat solver.
@raise UndecidedLit if the literal is not decided *)
eval_level: 'form -> bool * int;
(** Return the current assignement of the literals, as well as its
decision level. If the level is 0, then it is necessary for
the atom to have this value; otherwise it is due to choices
that can potentially be backtracked.
@raise UndecidedLit if the literal is not decided *)
model: unit -> ('term * 'term) list;
(** Returns the model found if the formula is satisfiable. *)
}
type ('clause, 'proof) unsat_state = {
unsat_conflict : unit -> 'clause;
(** Returns the unsat clause found at the toplevel *)
get_proof : unit -> 'proof;
(** returns a persistent proof of the empty clause from the Unsat result. *)
}
module type S = sig module type S = sig
(** {2 Internal modules} (** {2 Internal modules}
@ -19,7 +41,9 @@ module type S = sig
type atom = St.formula type atom = St.formula
(** The type of atoms given by the module argument for formulas *) (** The type of atoms given by the module argument for formulas *)
type res = Sat | Unsat type res =
| Sat of (St.term,St.formula) sat_state
| Unsat of (St.clause,Proof.proof) unsat_state
(** Result type for the solver *) (** Result type for the solver *)
exception UndecidedLit exception UndecidedLit
@ -32,26 +56,8 @@ module type S = sig
(** Add the list of clauses to the current set of assumptions. (** Add the list of clauses to the current set of assumptions.
Modifies the sat solver state in place. *) Modifies the sat solver state in place. *)
val solve : unit -> res val solve : ?assumptions:atom list -> unit -> res
(** Try and solves the current set of assumptions. (** 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 eval : atom -> bool
(** Returns the valuation of a formula in the current state
of the sat solver.
@raise UndecidedLit if the literal is not decided *)
val eval_level : atom -> bool * int
(** Return the current assignement of the literals, as well as its
decision level. If the level is 0, then it is necessary for
the atom to have this value; otherwise it is due to choices
that can potentially be backtracked.
@raise UndecidedLit if the literal is not decided *)
val get_proof : unit -> Proof.proof
(** If the last call to [solve] returned [Unsat], then returns a persistent
proof of the empty clause. *)
val unsat_core : Proof.proof -> St.clause list val unsat_core : Proof.proof -> St.clause list
(** Returns the unsat core of a given proof. *) (** Returns the unsat core of a given proof. *)
@ -59,26 +65,5 @@ module type S = sig
val get_tag : St.clause -> int option val get_tag : St.clause -> int option
(** Recover tag from a clause, if any *) (** Recover tag from a clause, if any *)
(** {2 Push/Pop operations} *)
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 reset : unit -> unit
(** Rest the state of the solver, i.e return to level {!base_level} *)
end end

15
src/core/solver_types.ml
View file

@ -58,7 +58,6 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
name : string; name : string;
tag : int option; tag : int option;
atoms : atom array; atoms : atom array;
c_level : int;
mutable cpremise : premise; mutable cpremise : premise;
mutable activity : float; mutable activity : float;
mutable attached : bool; mutable attached : bool;
@ -69,9 +68,10 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
| Decision | Decision
| Bcp of clause | Bcp of clause
| Semantic of int | Semantic of int
| Assumption
and premise = and premise =
| Hyp of int | Hyp
| Lemma of proof | Lemma of proof
| History of clause list | History of clause list
@ -106,7 +106,6 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
atoms = [| |]; atoms = [| |];
activity = -1.; activity = -1.;
attached = false; attached = false;
c_level = -1;
visited = false; visited = false;
cpremise = History [] } cpremise = History [] }
@ -187,18 +186,11 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
let make_clause ?tag name ali premise = let make_clause ?tag name ali premise =
let atoms = Array.of_list ali in let atoms = Array.of_list ali in
let level =
match premise with
| Hyp lvl -> lvl
| Lemma _ -> 0
| History l -> List.fold_left (fun lvl c -> max lvl c.c_level) 0 l
in
{ name = name; { name = name;
tag = tag; tag = tag;
atoms = atoms; atoms = atoms;
attached = false; attached = false;
visited = false; visited = false;
c_level = level;
activity = 0.; activity = 0.;
cpremise = premise} cpremise = premise}
@ -275,6 +267,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
| n, Some Decision -> sprintf "@@%d" n | n, Some Decision -> sprintf "@@%d" n
| n, Some Bcp c -> sprintf "->%d/%s" n c.name | n, Some Bcp c -> sprintf "->%d/%s" n c.name
| n, Some Semantic lvl -> sprintf "::%d/%d" n lvl | n, Some Semantic lvl -> sprintf "::%d/%d" n lvl
| n, Some Assumption -> sprintf "!%d" n
let value a = let value a =
if a.is_true then sprintf "[T%s]" (level a) if a.is_true then sprintf "[T%s]" (level a)
@ -282,7 +275,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
else "[]" else "[]"
let pp_premise out = function let pp_premise out = function
| Hyp _ -> Format.fprintf out "hyp" | Hyp -> Format.fprintf out "hyp"
| Lemma _ -> Format.fprintf out "th_lemma" | Lemma _ -> Format.fprintf out "th_lemma"
| History v -> List.iter (fun {name=name} -> Format.fprintf out "%s,@ " name) v | History v -> List.iter (fun {name=name} -> Format.fprintf out "%s,@ " name) v

4
src/core/solver_types_intf.ml
View file

@ -53,7 +53,6 @@ module type S = sig
name : string; name : string;
tag : int option; tag : int option;
atoms : atom array; atoms : atom array;
c_level : int;
mutable cpremise : premise; mutable cpremise : premise;
mutable activity : float; mutable activity : float;
mutable attached : bool; mutable attached : bool;
@ -64,9 +63,10 @@ module type S = sig
| Decision | Decision
| Bcp of clause | Bcp of clause
| Semantic of int | Semantic of int
| Assumption
and premise = and premise =
| Hyp of int | Hyp
| Lemma of proof | Lemma of proof
| History of clause list | History of clause list

16
src/main.ml
View file

@ -234,16 +234,16 @@ let main () =
let res = Smt.solve () in let res = Smt.solve () in
Gc.delete_alarm al; Gc.delete_alarm al;
begin match res with begin match res with
| Smt.Sat -> | Smt.Sat sat ->
let t = Sys.time () in let t = Sys.time () in
if !p_check then if !p_check then
if not (List.for_all (List.exists Smt.eval) cnf) then if not (List.for_all (List.exists sat.Solver_intf.eval) cnf) then
raise Incorrect_model; raise Incorrect_model;
print "Sat (%f/%f)" t (Sys.time () -. t) print "Sat (%f/%f)" t (Sys.time () -. t)
| Smt.Unsat -> | Smt.Unsat us ->
let t = Sys.time () in let t = Sys.time () in
if !p_check then begin if !p_check then begin
let p = Smt.get_proof () in let p = us.Solver_intf.get_proof () in
Smt.Proof.check p; Smt.Proof.check p;
print_proof p; print_proof p;
if !p_unsat_core then if !p_unsat_core then
@ -256,16 +256,16 @@ let main () =
let res = Mcsat.solve () in let res = Mcsat.solve () in
Gc.delete_alarm al; Gc.delete_alarm al;
begin match res with begin match res with
| Mcsat.Sat -> | Mcsat.Sat sat ->
let t = Sys.time () in let t = Sys.time () in
if !p_check then if !p_check then
if not (List.for_all (List.exists Mcsat.eval) cnf) then if not (List.for_all (List.exists sat.Solver_intf.eval) cnf) then
raise Incorrect_model; raise Incorrect_model;
print "Sat (%f/%f)" t (Sys.time () -. t) print "Sat (%f/%f)" t (Sys.time () -. t)
| Mcsat.Unsat -> | Mcsat.Unsat us ->
let t = Sys.time () in let t = Sys.time () in
if !p_check then begin if !p_check then begin
let p = Mcsat.get_proof () in let p = us.Solver_intf.get_proof () in
Mcsat.Proof.check p; Mcsat.Proof.check p;
print_mcproof p; print_mcproof p;
if !p_unsat_core then if !p_unsat_core then