simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-08 20:25:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Solver modules are paramtrized by log module

Browse source
This commit is contained in:
Guillaume Bury 2015-01-20 12:58:28 +01:00
parent 24b9362b30
commit d227d4c8b5
10 changed files with 49 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
msat.mlpack
View file

@ -1,4 +1,5 @@
# Solver Modules # Solver Modules
Log_intf
Formula_intf Formula_intf
Solver Solver
Solver_types Solver_types

1
msat.odocl
View file

@ -1,3 +1,4 @@
solver/Log_intf
solver/Formula_intf solver/Formula_intf
solver/Expr_intf solver/Expr_intf

2
sat/sat.ml
View file

@ -86,7 +86,7 @@ module Tsat = struct
end end
module Make(Dummy : sig end) = struct module Make(Dummy : sig end) = struct
module SatSolver = Solver.Make(Fsat)(Tsat) module SatSolver = Solver.Make(Log)(Fsat)(Tsat)
exception Bad_atom exception Bad_atom

2
smt/mcsat.ml
View file

@ -108,7 +108,7 @@ module Tsmt = struct
end end
module Make(Dummy:sig end) = struct module Make(Dummy:sig end) = struct
module SmtSolver = Mcsolver.Make(Fsmt)(Tsmt) module SmtSolver = Mcsolver.Make(Log)(Fsmt)(Tsmt)
type atom = Fsmt.t type atom = Fsmt.t
type clause = SmtSolver.St.clause type clause = SmtSolver.St.clause

2
smt/smt.ml
View file

@ -62,7 +62,7 @@ module Tsmt = struct
end end
module Make(Dummy:sig end) = struct module Make(Dummy:sig end) = struct
module SmtSolver = Solver.Make(Fsmt)(Tsmt) module SmtSolver = Solver.Make(Log)(Fsmt)(Tsmt)
type atom = Fsmt.t type atom = Fsmt.t
type clause = SmtSolver.St.clause type clause = SmtSolver.St.clause

6
solver/log_intf.ml Normal file
View file

@ -0,0 +1,6 @@
module type S = sig
val debug : int -> ('a, Buffer.t, unit, unit) format4 -> 'a
(** debug message *)
end

70
solver/mcsolver.ml
View file

@ -4,7 +4,7 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes Copyright 2014 Simon Cruanes
*) *)
module Make (E : Expr_intf.S) 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 (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) = struct
module St = Mcsolver_types.Make(E)(Th) module St = Mcsolver_types.Make(E)(Th)
@ -221,15 +221,15 @@ module Make (E : Expr_intf.S)
let new_decision_level() = let new_decision_level() =
Vec.push env.trail_lim (Vec.size env.trail); Vec.push env.trail_lim (Vec.size env.trail);
Vec.push env.tenv_queue (Th.current_level ()); (* save the current tenv *) Vec.push env.tenv_queue (Th.current_level ()); (* save the current tenv *)
Log.debug 5 "New decision level : %d (%d in env queue)(%d in trail)" 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); (Vec.size env.trail_lim) (Vec.size env.tenv_queue) (Vec.size env.trail);
() ()
let attach_clause c = let attach_clause c =
Vec.push (Vec.get c.atoms 0).neg.watched c; Vec.push (Vec.get c.atoms 0).neg.watched c;
Vec.push (Vec.get c.atoms 1).neg.watched c; Vec.push (Vec.get c.atoms 1).neg.watched c;
Log.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 0).neg St.pp_clause c;
Log.debug 8 "%a <-- %a" St.pp_atom (Vec.get c.atoms 1).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 if c.learnt then
env.learnts_literals <- env.learnts_literals + Vec.size c.atoms env.learnts_literals <- env.learnts_literals + Vec.size c.atoms
else else
@ -253,7 +253,7 @@ module Make (E : Expr_intf.S)
(* cancel down to [lvl] excluded *) (* cancel down to [lvl] excluded *)
let cancel_until lvl = let cancel_until lvl =
Log.debug 5 "Bactracking to decision level %d (excluded)" lvl; L.debug 5 "Bactracking to decision level %d (excluded)" lvl;
if decision_level () > lvl then begin if decision_level () > lvl then begin
env.qhead <- Vec.get env.trail_lim lvl; env.qhead <- Vec.get env.trail_lim lvl;
env.tatoms_qhead <- env.qhead; env.tatoms_qhead <- env.qhead;
@ -285,7 +285,7 @@ module Make (E : Expr_intf.S)
assert (Vec.size env.trail_lim = Vec.size env.tenv_queue) assert (Vec.size env.trail_lim = Vec.size env.tenv_queue)
let report_unsat ({atoms=atoms} as confl) = let report_unsat ({atoms=atoms} as confl) =
Log.debug 5 "Unsat conflict : %a" St.pp_clause confl; L.debug 5 "Unsat conflict : %a" St.pp_clause confl;
env.unsat_conflict <- Some confl; env.unsat_conflict <- Some confl;
env.is_unsat <- true; env.is_unsat <- true;
raise Unsat raise Unsat
@ -293,22 +293,22 @@ module Make (E : Expr_intf.S)
let enqueue_bool a lvl reason = let enqueue_bool a lvl reason =
assert (not a.neg.is_true); assert (not a.neg.is_true);
if a.is_true then if a.is_true then
Log.debug 10 "Litteral %a alreayd in queue" pp_atom a L.debug 10 "Litteral %a alreayd in queue" pp_atom a
else begin else begin
assert (a.var.level < 0 && a.var.tag.reason = Bcp None && lvl >= 0); assert (a.var.level < 0 && a.var.tag.reason = Bcp None && lvl >= 0);
a.is_true <- true; a.is_true <- true;
a.var.level <- lvl; a.var.level <- lvl;
a.var.tag.reason <- reason; a.var.tag.reason <- reason;
Log.debug 8 "Enqueue: %a" pp_atom a; L.debug 8 "Enqueue: %a" pp_atom a;
Vec.push env.trail (Either.mk_right a) Vec.push env.trail (Either.mk_right a)
end end
let enqueue_assign v value lvl = let enqueue_assign v value lvl =
v.tag.assigned <- Some value; v.tag.assigned <- Some value;
v.level <- lvl; v.level <- lvl;
Log.debug 5 "Enqueue: %a" St.pp_semantic_var v; L.debug 5 "Enqueue: %a" St.pp_semantic_var v;
Vec.push env.trail (Either.mk_left v); Vec.push env.trail (Either.mk_left v);
Log.debug 15 "Done." L.debug 15 "Done."
(* conflict analysis *) (* conflict analysis *)
let max_lvl_atoms l = let max_lvl_atoms l =
@ -340,28 +340,28 @@ module Make (E : Expr_intf.S)
in in
try while true do try while true do
let _, atoms = max_lvl_atoms !c in let _, atoms = max_lvl_atoms !c in
Log.debug 15 "Current conflict clause :"; L.debug 15 "Current conflict clause :";
List.iter (fun a -> Log.debug 15 " |- %a" St.pp_atom a) !c; List.iter (fun a -> L.debug 15 " |- %a" St.pp_atom a) !c;
match atoms with match atoms with
| [] | _ :: [] -> | [] | _ :: [] ->
Log.debug 15 "Found UIP clause"; L.debug 15 "Found UIP clause";
is_uip := true; is_uip := true;
raise Exit raise Exit
| _ when List.for_all is_semantic atoms -> | _ when List.for_all is_semantic atoms ->
Log.debug 15 "Found Semantic backtrack clause"; L.debug 15 "Found Semantic backtrack clause";
raise Exit raise Exit
| _ -> | _ ->
decr tr_ind; decr tr_ind;
Log.debug 20 "Looking at trail element %d" !tr_ind; L.debug 20 "Looking at trail element %d" !tr_ind;
Either.destruct (Vec.get env.trail !tr_ind) Either.destruct (Vec.get env.trail !tr_ind)
(fun v -> Log.debug 15 "%a" St.pp_semantic_var v) (fun v -> L.debug 15 "%a" St.pp_semantic_var v)
(fun a -> match a.var.tag.reason with (fun a -> match a.var.tag.reason with
| Bcp (Some d) -> | Bcp (Some d) ->
Log.debug 15 "Propagation : %a" St.pp_atom a; L.debug 15 "Propagation : %a" St.pp_atom a;
Log.debug 15 " |- %a" St.pp_clause d; L.debug 15 " |- %a" St.pp_clause d;
let tmp, res = Proof.resolve (Proof.merge !c (Proof.to_list d)) in let tmp, res = Proof.resolve (Proof.merge !c (Proof.to_list d)) in
begin match tmp with begin match tmp with
| [] -> Log.debug 15 "No lit to resolve over." | [] -> L.debug 15 "No lit to resolve over."
| [b] when b == a.var.tag.pa -> | [b] when b == a.var.tag.pa ->
clause_bump_activity d; clause_bump_activity d;
var_bump_activity a.var; var_bump_activity a.var;
@ -369,8 +369,8 @@ module Make (E : Expr_intf.S)
c := res c := res
| _ -> assert false | _ -> assert false
end end
| Bcp None -> Log.debug 15 "Decision : %a" St.pp_atom a | Bcp None -> L.debug 15 "Decision : %a" St.pp_atom a
| Semantic _ -> Log.debug 15 "Semantic propagation : %a" St.pp_atom a) | Semantic _ -> L.debug 15 "Semantic propagation : %a" St.pp_atom a)
done; assert false done; assert false
with Exit -> with Exit ->
let learnt = List.sort (fun a b -> Pervasives.compare b.var.level a.var.level) !c in let learnt = List.sort (fun a b -> Pervasives.compare b.var.level a.var.level) !c in
@ -423,13 +423,13 @@ module Make (E : Expr_intf.S)
fuip.var.tag.vpremise <- history; fuip.var.tag.vpremise <- history;
let name = fresh_lname () in let name = fresh_lname () in
let uclause = make_clause name learnt (List.length learnt) true history in let uclause = make_clause name learnt (List.length learnt) true history in
Log.debug 2 "Unit clause learnt : %a" St.pp_clause uclause; L.debug 2 "Unit clause learnt : %a" St.pp_clause uclause;
Vec.push env.learnts uclause; Vec.push env.learnts uclause;
enqueue_bool fuip 0 (Bcp (Some uclause)) enqueue_bool fuip 0 (Bcp (Some uclause))
| fuip :: _ -> | fuip :: _ ->
let name = fresh_lname () in let name = fresh_lname () in
let lclause = make_clause name learnt (List.length learnt) true history in let lclause = make_clause name learnt (List.length learnt) true history in
Log.debug 2 "New clause learnt : %a" St.pp_clause lclause; L.debug 2 "New clause learnt : %a" St.pp_clause lclause;
Vec.push env.learnts lclause; Vec.push env.learnts lclause;
attach_clause lclause; attach_clause lclause;
clause_bump_activity lclause; clause_bump_activity lclause;
@ -494,7 +494,7 @@ module Make (E : Expr_intf.S)
if env.is_unsat then raise Unsat; if env.is_unsat then raise Unsat;
let init_name = string_of_int cnumber in let init_name = string_of_int cnumber in
let init0 = make_clause init_name atoms (List.length atoms) (history <> History []) history in let init0 = make_clause init_name atoms (List.length atoms) (history <> History []) history in
Log.debug 10 "Adding clause : %a" St.pp_clause init0; L.debug 10 "Adding clause : %a" St.pp_clause init0;
try try
let atoms, init = partition atoms init0 in let atoms, init = partition atoms init0 in
let history = match init with let history = match init with
@ -508,7 +508,7 @@ module Make (E : Expr_intf.S)
| a::b::_ -> | a::b::_ ->
let name = fresh_name () in let name = fresh_name () in
let clause = make_clause name atoms size (history <> History []) history in let clause = make_clause name atoms size (history <> History []) history in
Log.debug 10 "New clause : %a" St.pp_clause init0; L.debug 10 "New clause : %a" St.pp_clause init0;
attach_clause clause; attach_clause clause;
Vec.push env.clauses clause; Vec.push env.clauses clause;
if a.neg.is_true then begin if a.neg.is_true then begin
@ -561,7 +561,7 @@ module Make (E : Expr_intf.S)
Vec.set atoms 1 ak; Vec.set atoms 1 ak;
Vec.set atoms k a.neg; Vec.set atoms k a.neg;
Vec.push ak.neg.watched c; Vec.push ak.neg.watched c;
Log.debug 8 "New watcher (%a) for clause : %a" St.pp_atom ak.neg St.pp_clause c; L.debug 8 "New watcher (%a) for clause : %a" St.pp_atom ak.neg St.pp_clause c;
raise Exit raise Exit
end end
done; done;
@ -573,23 +573,23 @@ module Make (E : Expr_intf.S)
Vec.set watched !new_sz (Vec.get watched k); Vec.set watched !new_sz (Vec.get watched k);
incr new_sz; incr new_sz;
done; done;
Log.debug 3 "Conflict found : %a" St.pp_clause c; L.debug 3 "Conflict found : %a" St.pp_clause c;
raise (Conflict c) raise (Conflict c)
end end
else begin else begin
(* clause is unit *) (* clause is unit *)
Vec.set watched !new_sz c; Vec.set watched !new_sz c;
incr new_sz; incr new_sz;
Log.debug 5 "Unit clause : %a" St.pp_clause c; L.debug 5 "Unit clause : %a" St.pp_clause c;
enqueue_bool first (decision_level ()) (Bcp (Some c)) enqueue_bool first (decision_level ()) (Bcp (Some c))
end end
with Exit -> () with Exit -> ()
let propagate_atom a res = let propagate_atom a res =
Log.debug 8 "Propagating %a" St.pp_atom a; L.debug 8 "Propagating %a" St.pp_atom a;
let watched = a.watched in let watched = a.watched in
Log.debug 10 "Watching %a :" St.pp_atom a; L.debug 10 "Watching %a :" St.pp_atom a;
Vec.iter (fun c -> Log.debug 10 " %a" St.pp_clause c) watched; Vec.iter (fun c -> L.debug 10 " %a" St.pp_clause c) watched;
let new_sz_w = ref 0 in let new_sz_w = ref 0 in
begin begin
try try
@ -752,7 +752,7 @@ module Make (E : Expr_intf.S)
env.decisions <- env.decisions + 1; env.decisions <- env.decisions + 1;
new_decision_level(); new_decision_level();
let current_level = decision_level () in let current_level = decision_level () in
Log.debug 5 "Deciding on %a" St.pp_semantic_var v; L.debug 5 "Deciding on %a" St.pp_semantic_var v;
enqueue_assign v value current_level enqueue_assign v value current_level
end) end)
(fun v -> (fun v ->
@ -764,7 +764,7 @@ module Make (E : Expr_intf.S)
env.decisions <- env.decisions + 1; env.decisions <- env.decisions + 1;
new_decision_level(); new_decision_level();
let current_level = decision_level () in let current_level = decision_level () in
Log.debug 5 "Deciding on %a" St.pp_atom v.tag.pa; L.debug 5 "Deciding on %a" St.pp_atom v.tag.pa;
enqueue_bool v.tag.pa current_level (Bcp None) enqueue_bool v.tag.pa current_level (Bcp None)
| Th.Valued (b, lvl) -> | Th.Valued (b, lvl) ->
let a = if b then v.tag.pa else v.tag.na in let a = if b then v.tag.pa else v.tag.na in
@ -845,8 +845,8 @@ module Make (E : Expr_intf.S)
Vec.grow_to_by_double env.learnts nbc; Vec.grow_to_by_double env.learnts nbc;
env.nb_init_clauses <- nbc; env.nb_init_clauses <- nbc;
St.iter_vars (fun e -> Either.destruct e St.iter_vars (fun e -> Either.destruct e
(fun v -> Log.debug 50 " -- %a" St.pp_semantic_var v) (fun v -> L.debug 50 " -- %a" St.pp_semantic_var v)
(fun a -> Log.debug 50 " -- %a" St.pp_atom a.tag.pa) (fun a -> L.debug 50 " -- %a" St.pp_atom a.tag.pa)
); );
add_clauses cnf ~cnumber add_clauses cnf ~cnumber

2
solver/mcsolver.mli
View file

@ -4,7 +4,7 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes Copyright 2014 Simon Cruanes
*) *)
module Make (E : Expr_intf.S) 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 (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 McSolver parametrised by the atomic formulas and a theory. *)

2
solver/solver.ml
View file

@ -10,7 +10,7 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
module Make (F : Formula_intf.S) module Make (L : Log_intf.S)(F : Formula_intf.S)
(Th : Theory_intf.S with type formula = F.t) = struct (Th : Theory_intf.S with type formula = F.t) = struct
module St = Solver_types.Make(F)(Th) module St = Solver_types.Make(F)(Th)

2
solver/solver.mli
View file

@ -11,7 +11,7 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
module Make (F : Formula_intf.S) module Make (L : Log_intf.S)(F : Formula_intf.S)
(Th : Theory_intf.S with type formula = F.t) : sig (Th : Theory_intf.S with type formula = F.t) : sig
(** Functor to create a SMT Solver parametrised by the atomic (** Functor to create a SMT Solver parametrised by the atomic
formulas and a theory. *) formulas and a theory. *)