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

Modifications in progress....

Browse source
This commit is contained in:
Guillaume Bury 2014-12-12 17:14:06 +01:00
parent 8e8a592475
commit a0d6be1057
7 changed files with 270 additions and 145 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
mcsolver/expr_intf.ml
View file

@ -47,8 +47,5 @@ module type S = sig
(** Returns a 'normalized' form of the formula, possibly negated (in which case return true). (** Returns a 'normalized' form of the formula, possibly negated (in which case return true).
[norm] must be so that [a] and [neg a] normalises to the same formula. *) [norm] must be so that [a] and [neg a] normalises to the same formula. *)
val iter_pure : (Term.t -> unit) -> Formula.t -> bool
(** An iterator over the pure subterms of a formula *)
end end

173
mcsolver/mcsolver.ml
View file

@ -11,10 +11,10 @@
(**************************************************************************) (**************************************************************************)
module Make (E : Expr_intf.S) module Make (E : Expr_intf.S)
(Th : Plugin_intf.S with 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)
module Proof = Res.Make(St) (* module Proof = Res.Make(St) *)
open St open St
@ -30,6 +30,11 @@ module Make (E : Expr_intf.S)
ul_learnt : int; (* number of learnt clauses *) ul_learnt : int; (* number of learnt clauses *)
} }
(* Type for trail elements *)
type trail_elt =
| Semantic of semantic var
| Boolean of atom
(* Singleton type containing the current state *) (* Singleton type containing the current state *)
type env = { type env = {
@ -51,7 +56,7 @@ module Make (E : Expr_intf.S)
mutable var_inc : float; mutable var_inc : float;
(* increment for variables' activity *) (* increment for variables' activity *)
trail : atom Vec.t; trail : trail_elt Vec.t;
(* decision stack + propagated atoms *) (* decision stack + propagated atoms *)
trail_lim : int Vec.t; trail_lim : int Vec.t;
@ -111,7 +116,6 @@ module Make (E : Expr_intf.S)
mutable max_literals : int; mutable max_literals : int;
mutable tot_literals : int; mutable tot_literals : int;
mutable nb_init_clauses : int; mutable nb_init_clauses : int;
mutable model : var Vec.t;
mutable tenv_queue : Th.level Vec.t; mutable tenv_queue : Th.level Vec.t;
mutable tatoms_qhead : int; mutable tatoms_qhead : int;
} }
@ -123,7 +127,7 @@ module Make (E : Expr_intf.S)
learnts = Vec.make 0 dummy_clause; (*updated during parsing*) learnts = Vec.make 0 dummy_clause; (*updated during parsing*)
clause_inc = 1.; clause_inc = 1.;
var_inc = 1.; var_inc = 1.;
trail = Vec.make 601 dummy_atom; trail = Vec.make 601 (Boolean dummy_atom);
trail_lim = Vec.make 601 (-1); trail_lim = Vec.make 601 (-1);
user_levels = Vec.make 20 {ul_trail=0;ul_learnt=0;ul_clauses=0}; user_levels = Vec.make 20 {ul_trail=0;ul_learnt=0;ul_clauses=0};
qhead = 0; qhead = 0;
@ -149,7 +153,6 @@ module Make (E : Expr_intf.S)
max_literals = 0; max_literals = 0;
tot_literals = 0; tot_literals = 0;
nb_init_clauses = 0; nb_init_clauses = 0;
model = Vec.make 0 dummy_var;
tenv_queue = Vec.make 100 Th.dummy; tenv_queue = Vec.make 100 Th.dummy;
tatoms_qhead = 0; tatoms_qhead = 0;
} }
@ -158,16 +161,32 @@ module Make (E : Expr_intf.S)
let to_float i = float_of_int i let to_float i = float_of_int i
let to_int f = int_of_float f let to_int f = int_of_float f
let get_elt_weight = function
| Term v -> v.weight
| Formula v -> v.weight
let set_elt_weight e w = match e with
| Term v -> v.weight <- w
| Formula v -> v.weight <- w
let get_elt_level = function
| Term v -> v.level
| Formula v -> v.level
let f_weight i j = let f_weight i j =
(St.get_var j).weight < (St.get_var i).weight get_elt_weight (St.get_var j) < get_elt_weight (St.get_var i)
let f_filter i = let f_filter i =
(St.get_var i).level < 0 get_elt_level (St.get_var i) < 0
(* Var/clause activity *) (* Var/clause activity *)
let insert_var_order v = let rec insert_var_order = function
Iheap.insert f_weight env.order v.vid | Term v ->
Iheap.insert f_weight env.order v.vid
| Formula v ->
Iheap.insert f_weight env.order v.vid;
Th.iter_assignable
(fun t -> insert_var_order (Term (St.add_term t))) v.tag.pa.lit
let var_decay_activity () = let var_decay_activity () =
env.var_inc <- env.var_inc *. env.var_decay env.var_inc <- env.var_inc *. env.var_decay
@ -179,7 +198,7 @@ module Make (E : Expr_intf.S)
v.weight <- v.weight +. env.var_inc; v.weight <- v.weight +. env.var_inc;
if v.weight > 1e100 then begin if v.weight > 1e100 then begin
for i = 0 to (St.nb_vars ()) - 1 do for i = 0 to (St.nb_vars ()) - 1 do
(St.get_var i).weight <- (St.get_var i).weight *. 1e-100 set_elt_weight (St.get_var i) ((get_elt_weight (St.get_var i)) *. 1e-100)
done; done;
env.var_inc <- env.var_inc *. 1e-100; env.var_inc <- env.var_inc *. 1e-100;
end; end;
@ -244,13 +263,15 @@ module Make (E : Expr_intf.S)
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;
for c = Vec.size env.trail - 1 downto env.qhead do for c = Vec.size env.trail - 1 downto env.qhead do
let a = Vec.get env.trail c in match Vec.get env.trail c with
a.is_true <- false; | Boolean a ->
a.neg.is_true <- false; a.is_true <- false;
a.var.level <- -1; a.neg.is_true <- false;
a.var.reason <- None; a.var.level <- -1;
a.var.vpremise <- History []; a.var.tag.reason <- Bcp None;
insert_var_order a.var a.var.tag.vpremise <- History [];
insert_var_order (Formula a.var)
| Semantic a -> ()
done; done;
Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *) 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 ((Vec.size env.trail) - env.qhead);
@ -265,17 +286,22 @@ module Make (E : Expr_intf.S)
env.is_unsat <- true; env.is_unsat <- true;
raise Unsat raise Unsat
let enqueue a lvl reason = let enqueue_bool a lvl reason =
assert (not a.is_true && not a.neg.is_true && assert (not a.is_true && not a.neg.is_true && a.var.level < 0
a.var.level < 0 && a.var.reason = None && lvl >= 0); && a.var.tag.reason = Bcp None && lvl >= 0);
assert (lvl = decision_level ()); assert (lvl = decision_level ());
(* keep the reason for proof/unsat-core *) (* keep the reason for proof/unsat-core *)
(*let reason = if lvl = 0 then None else reason in*) (*let reason = if lvl = 0 then None else reason in*)
a.is_true <- true; a.is_true <- true;
a.var.level <- lvl; a.var.level <- lvl;
a.var.reason <- reason; a.var.tag.reason <- reason;
Log.debug 8 "Enqueue: %a" pp_atom a; Log.debug 8 "Enqueue: %a" pp_atom a;
Vec.push env.trail a Vec.push env.trail (Boolean a)
let enqueue_assign v value lvl =
v.tag.assigned <- Some value;
v.level <- lvl;
Vec.push env.trail (Semantic v)
(* conflict analysis *) (* conflict analysis *)
let analyze c_clause = let analyze c_clause =
@ -296,9 +322,9 @@ module Make (E : Expr_intf.S)
let q = Vec.get !c.atoms j in let q = Vec.get !c.atoms j in
(*printf "I visit %a@." D1.atom q;*) (*printf "I visit %a@." D1.atom q;*)
assert (q.is_true || q.neg.is_true && q.var.level >= 0); (* Pas sur *) 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 if not q.var.tag.seen && q.var.level > 0 then begin
var_bump_activity q.var; var_bump_activity q.var;
q.var.seen <- true; q.var.tag.seen <- true;
seen := q :: !seen; seen := q :: !seen;
if q.var.level >= decision_level () then begin if q.var.level >= decision_level () then begin
incr pathC incr pathC
@ -330,12 +356,12 @@ module Make (E : Expr_intf.S)
| [] -> assert false | [] -> assert false
| [fuip] -> | [fuip] ->
assert (blevel = 0); assert (blevel = 0);
fuip.var.vpremise <- history; fuip.var.tag.vpremise <- history;
let name = fresh_lname () in let name = fresh_lname () in
let uclause = make_clause name learnt size true history in let uclause = make_clause name learnt size true history in
Log.debug 2 "Unit clause learnt : %a" St.pp_clause uclause; Log.debug 2 "Unit clause learnt : %a" St.pp_clause uclause;
Vec.push env.learnts uclause; Vec.push env.learnts uclause;
enqueue fuip 0 (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 size true history in let lclause = make_clause name learnt size true history in
@ -343,7 +369,7 @@ module Make (E : Expr_intf.S)
Vec.push env.learnts lclause; Vec.push env.learnts lclause;
attach_clause lclause; attach_clause lclause;
clause_bump_activity lclause; clause_bump_activity lclause;
enqueue fuip blevel (Some lclause) enqueue_bool fuip blevel (Bcp (Some lclause))
end; end;
var_decay_activity (); var_decay_activity ();
clause_decay_activity () clause_decay_activity ()
@ -364,7 +390,7 @@ module Make (E : Expr_intf.S)
let aux (atoms, init) a = let aux (atoms, init) a =
if a.is_true then raise Trivial; if a.is_true then raise Trivial;
if a.neg.is_true then if a.neg.is_true then
match a.var.vpremise with match a.var.tag.vpremise with
| History v -> atoms, [init0] | History v -> atoms, [init0]
| Lemma p -> assert false | Lemma p -> assert false
else else
@ -381,7 +407,7 @@ module Make (E : Expr_intf.S)
if a.var.level = 0 then raise Trivial if a.var.level = 0 then raise Trivial
else (a::trues) @ unassigned @ falses @ r, init else (a::trues) @ unassigned @ falses @ r, init
else if a.neg.is_true then else if a.neg.is_true then
if a.var.level = 0 then match a.var.vpremise with if a.var.level = 0 then match a.var.tag.vpremise with
| History v -> | History v ->
partition_aux trues unassigned falses [init0] r partition_aux trues unassigned falses [init0] r
| Lemma _ -> assert false | Lemma _ -> assert false
@ -422,25 +448,15 @@ module Make (E : Expr_intf.S)
end else if b.neg.is_true && not a.is_true && not a.neg.is_true then begin 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 let lvl = List.fold_left (fun m a -> max m a.var.level) 0 atoms in
cancel_until lvl; cancel_until lvl;
enqueue a lvl (Some clause) enqueue_bool a lvl (Bcp (Some clause))
end end
| [a] -> | [a] ->
cancel_until 0; cancel_until 0;
a.var.vpremise <- history; a.var.tag.vpremise <- history;
enqueue a 0 (match init with [init0] -> Some init0 | _ -> None) enqueue_bool a 0 (Bcp (match init with [init0] -> Some init0 | _ -> None))
with Trivial -> () with Trivial -> ()
(* Decide on a new litteral *)
let rec pick_branch_lit () =
let max = Iheap.remove_min f_weight env.order in
let v = St.get_var max in
if v.level>= 0 then begin
assert (v.pa.is_true || v.na.is_true);
pick_branch_lit ()
end else
v
let progress_estimate () = let progress_estimate () =
let prg = ref 0. in let prg = ref 0. in
let nbv = to_float (nb_vars()) in let nbv = to_float (nb_vars()) in
@ -495,7 +511,7 @@ module Make (E : Expr_intf.S)
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; Log.debug 5 "Unit clause : %a" St.pp_clause c;
enqueue first (decision_level ()) (Some c) enqueue_bool first (decision_level ()) (Bcp (Some c))
end end
with Exit -> () with Exit -> ()
@ -520,12 +536,16 @@ module Make (E : Expr_intf.S)
(* Propagation (boolean and theory *) (* Propagation (boolean and theory *)
let _th_cnumber = ref 0 let _th_cnumber = ref 0
let slice_get i = (Vec.get env.trail i).lit let slice_get i = match (Vec.get env.trail i) with
| Boolean a -> Th.Lit a.lit
| Semantic {tag={term; assigned = Some v}} -> Th.Assign (term, v)
| _ -> assert false
let slice_push l lemma = let slice_push l lemma =
decr _th_cnumber; decr _th_cnumber;
let atoms = List.rev_map (fun x -> add_atom x) l in let atoms = List.rev_map (fun x -> add_atom x) l in
Iheap.grow_to_by_double env.order (St.nb_vars ()); Iheap.grow_to_by_double env.order (St.nb_vars ());
List.iter (fun a -> insert_var_order a.var) atoms; List.iter (fun a -> insert_var_order (Formula a.var)) atoms;
add_clause ~cnumber:!_th_cnumber atoms (Lemma lemma) add_clause ~cnumber:!_th_cnumber atoms (Lemma lemma)
let current_slice () = Th.({ let current_slice () = Th.({
@ -553,10 +573,12 @@ module Make (E : Expr_intf.S)
let num_props = ref 0 in let num_props = ref 0 in
let res = ref None in let res = ref None in
while env.qhead < Vec.size env.trail do while env.qhead < Vec.size env.trail do
let a = Vec.get env.trail env.qhead in match Vec.get env.trail env.qhead with
env.qhead <- env.qhead + 1; | Boolean a ->
incr num_props; env.qhead <- env.qhead + 1;
propagate_atom a res; incr num_props;
propagate_atom a res
| Semantic a -> ()
done; done;
env.propagations <- env.propagations + !num_props; env.propagations <- env.propagations + !num_props;
env.simpDB_props <- env.simpDB_props - !num_props; env.simpDB_props <- env.simpDB_props - !num_props;
@ -637,6 +659,34 @@ module Make (E : Expr_intf.S)
env.simpDB_props <- env.clauses_literals + env.learnts_literals; env.simpDB_props <- env.clauses_literals + env.learnts_literals;
end end
(* Decide on a new litteral *)
let rec pick_branch_lit () =
let max = Iheap.remove_min f_weight env.order in
match St.get_var max with
| Term v ->
let value = Th.assign v.tag.term in
env.decisions <- env.decisions + 1;
new_decision_level();
let current_level = decision_level () in
assert (v.level < 0);
(* Log.debug 5 "Assigning %a to %a" St.pp_atom v.tag.pa; *)
enqueue_assign v value current_level
| Formula 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
assert (v.level < 0);
Log.debug 5 "Deciding on %a" St.pp_atom v.tag.pa;
enqueue_bool v.tag.pa current_level (Bcp None)
| Th.Bool b ->
let a = if b then v.tag.pa else v.tag.na in
enqueue_bool a (decision_level ()) (Bcp None)
let search n_of_conflicts n_of_learnts = let search n_of_conflicts n_of_learnts =
let conflictC = ref 0 in let conflictC = ref 0 in
env.starts <- env.starts + 1; env.starts <- env.starts + 1;
@ -660,14 +710,7 @@ module Make (E : Expr_intf.S)
Vec.size env.learnts - nb_assigns() >= n_of_learnts then Vec.size env.learnts - nb_assigns() >= n_of_learnts then
reduce_db(); reduce_db();
env.decisions <- env.decisions + 1; pick_branch_lit ()
new_decision_level();
let next = pick_branch_lit () in
let current_level = decision_level () in
assert (next.level < 0);
Log.debug 5 "Deciding on %a" St.pp_atom next.pa;
enqueue next.pa current_level None
done done
let check_clause c = let check_clause c =
@ -682,11 +725,6 @@ module Make (E : Expr_intf.S)
let check_vec vec = let check_vec vec =
for i = 0 to Vec.size vec - 1 do check_clause (Vec.get vec i) done for i = 0 to Vec.size vec - 1 do check_clause (Vec.get vec i) done
(*
let check_model () =
check_vec env.clauses;
check_vec env.learnts
*)
(* fixpoint of propagation and decisions until a model is found, or a (* fixpoint of propagation and decisions until a model is found, or a
conflict is reached *) conflict is reached *)
@ -720,7 +758,6 @@ module Make (E : Expr_intf.S)
Iheap.grow_to_by_double env.order nbv; Iheap.grow_to_by_double env.order nbv;
(* List.iter (List.iter (fun a -> insert_var_order a.var)) cnf; *) (* List.iter (List.iter (fun a -> insert_var_order a.var)) cnf; *)
St.iter_vars insert_var_order; St.iter_vars insert_var_order;
Vec.grow_to_by_double env.model nbv;
Vec.grow_to_by_double env.clauses nbc; Vec.grow_to_by_double env.clauses nbc;
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;
@ -732,9 +769,9 @@ module Make (E : Expr_intf.S)
init_solver cnf ~cnumber init_solver cnf ~cnumber
let eval lit = let eval lit =
let var, negated = make_var lit in let var, negated = make_boolean_var lit in
assert (var.pa.is_true || var.na.is_true); assert (var.tag.pa.is_true || var.tag.na.is_true);
let truth = var.pa.is_true in let truth = var.tag.pa.is_true in
if negated then not truth else truth if negated then not truth else truth
let history () = env.learnts let history () = env.learnts

7
mcsolver/mcsolver.mli
View file

@ -12,19 +12,20 @@
(**************************************************************************) (**************************************************************************)
module Make (E : Expr_intf.S) module Make (E : Expr_intf.S)
(Th : Theory_intf.S with 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 SMT Solver parametrised by the atomic (** Functor to create a McSolver parametrised by the atomic formulas and a theory. *)
formulas and a theory. *)
exception Unsat exception Unsat
module St : Mcsolver_types.S module St : Mcsolver_types.S
with type formula = E.Formula.t with type formula = E.Formula.t
(*
module Proof : Res.S module Proof : Res.S
with type atom = St.atom with type atom = St.atom
and type clause = St.clause and type clause = St.clause
and type lemma = Th.proof and type lemma = Th.proof
*)
val solve : unit -> unit val solve : unit -> unit
(** Try and solves the current set of assumptions. (** Try and solves the current set of assumptions.

152
mcsolver/mcsolver_types.ml
View file

@ -15,23 +15,34 @@ open Printf
module type S = Mcsolver_types_intf.S module type S = Mcsolver_types_intf.S
module Make (E : Expr_intf.S)(Th : Theory_intf.S) = struct module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct
(* Types declarations *)
type term = E.Term.t
type formula = E.Formula.t type formula = E.Formula.t
type proof = Th.proof type proof = Th.proof
type var = type 'a var =
{ vid : int; { vid : int;
pa : atom; tag : 'a;
na : atom; mutable weight : float;
mutable weight : float; mutable level : int; }
mutable seen : bool;
mutable level : int; type semantic =
mutable reason: reason; { term : term;
mutable vpremise : premise} mutable assigned : term option; }
type boolean = {
pa : atom;
na : atom;
mutable seen : bool;
mutable reason : reason;
mutable vpremise : premise
}
and atom = and atom =
{ var : var; { var : boolean var;
lit : formula; lit : formula;
neg : atom; neg : atom;
mutable watched : clause Vec.t; mutable watched : clause Vec.t;
@ -46,23 +57,53 @@ module Make (E : Expr_intf.S)(Th : Theory_intf.S) = struct
learnt : bool; learnt : bool;
cpremise : premise } cpremise : premise }
and reason = clause option and reason =
| Semantic of int
| Bcp of clause option
and premise = and premise =
| History of clause list | History of clause list
| Lemma of proof | Lemma of proof
type elt =
| Term of semantic var
| Formula of boolean var
(* Accessors for variables *)
let get_elt_id = function
| Term v -> v.vid
| Formula v -> v.vid
let get_elt_weight = function
| Term v -> v.weight
| Formula v -> v.weight
let get_elt_level = function
| Term v -> v.level
| Formula v -> v.level
let set_elt_weight e w = match e with
| Term v -> v.weight <- w
| Formula v -> v.weight <- w
let set_elt_level e l = match e with
| Term v -> v.level <- l
| Formula v -> v.level <- l
(* Dummy values *)
let dummy_lit = E.dummy let dummy_lit = E.dummy
let rec dummy_var = let rec dummy_var =
{ vid = -101; { vid = -101;
pa = dummy_atom;
na = dummy_atom;
level = -1; level = -1;
reason = None;
weight = -1.; weight = -1.;
seen = false; tag = {
vpremise = History [] } pa = dummy_atom;
na = dummy_atom;
reason = None;
seen = false;
vpremise = History []; };
}
and dummy_atom = and dummy_atom =
{ var = dummy_var; { var = dummy_var;
lit = dummy_lit; lit = dummy_lit;
@ -72,7 +113,6 @@ module Make (E : Expr_intf.S)(Th : Theory_intf.S) = struct
neg = dummy_atom; neg = dummy_atom;
is_true = false; is_true = false;
aid = -102 } aid = -102 }
let dummy_clause = let dummy_clause =
{ name = ""; { name = "";
atoms = Vec.make_empty dummy_atom; atoms = Vec.make_empty dummy_atom;
@ -84,33 +124,36 @@ module Make (E : Expr_intf.S)(Th : Theory_intf.S) = struct
let () = let () =
dummy_atom.watched <- Vec.make_empty dummy_clause dummy_atom.watched <- Vec.make_empty dummy_clause
module MA = Map.Make(E.Formula) (* Constructors *)
module MF = Map.Make(E.Formula)
module MT = Map.Make(E.Term)
let normal_form = E.norm let f_map = ref MF.empty
let t_map = ref MT.empty
let ma = ref MA.empty
let vars = Vec.make 107 dummy_var
let vars = Vec.make 107 (Formula dummy_var)
let nb_vars () = Vec.size vars let nb_vars () = Vec.size vars
let get_var i = Vec.get vars i let get_var i = Vec.get vars i
let iter_vars f = Vec.iter f vars let iter_vars f = Vec.iter f vars
let cpt_mk_var = ref 0 let cpt_mk_var = ref 0
let make_var =
let make_boolean_var =
fun lit -> fun lit ->
let lit, negated = normal_form lit in let lit, negated = E.norm lit in
try MA.find lit !ma, negated try MF.find lit !f_map, negated
with Not_found -> with Not_found ->
let cpt_fois_2 = !cpt_mk_var lsl 1 in let cpt_fois_2 = !cpt_mk_var lsl 1 in
let rec var = let rec var =
{ vid = !cpt_mk_var; { vid = !cpt_mk_var;
pa = pa;
na = na;
level = -1; level = -1;
reason = None;
weight = 0.; weight = 0.;
seen = false; tag = {
vpremise = History []; pa = pa;
na = na;
reason = Bcp None;
seen = false;
vpremise = History [];};
} }
and pa = and pa =
{ var = var; { var = var;
@ -126,15 +169,32 @@ module Make (E : Expr_intf.S)(Th : Theory_intf.S) = struct
neg = pa; neg = pa;
is_true = false; is_true = false;
aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in
ma := MA.add lit var !ma; f_map := MF.add lit var !f_map;
incr cpt_mk_var; incr cpt_mk_var;
Vec.push vars var; Vec.push vars (Formula var);
assert (Vec.get vars var.vid == var && !cpt_mk_var = Vec.size vars);
var, negated var, negated
let make_semantic_var t =
try MT.find t !t_map
with Not_found ->
let res = {
vid = !cpt_mk_var;
weight = 0.;
level = -1;
tag = {
term = t;
assigned = None; };
} in
incr cpt_mk_var;
t_map := MT.add t res !t_map;
Vec.push vars (Term res);
res
let add_term t = make_semantic_var t
let add_atom lit = let add_atom lit =
let var, negated = make_var lit in let var, negated = make_boolean_var lit in
if negated then var.na else var.pa if negated then var.tag.na else var.tag.pa
let make_clause name ali sz_ali is_learnt premise = let make_clause name ali sz_ali is_learnt premise =
let atoms = Vec.from_list ali sz_ali dummy_atom in let atoms = Vec.from_list ali sz_ali dummy_atom in
@ -147,6 +207,7 @@ module Make (E : Expr_intf.S)(Th : Theory_intf.S) = struct
let empty_clause = make_clause "Empty" [] 0 false (History []) let empty_clause = make_clause "Empty" [] 0 false (History [])
(* Name generation *)
let fresh_lname = let fresh_lname =
let cpt = ref 0 in let cpt = ref 0 in
fun () -> incr cpt; "L" ^ (string_of_int !cpt) fun () -> incr cpt; "L" ^ (string_of_int !cpt)
@ -159,10 +220,6 @@ module Make (E : Expr_intf.S)(Th : Theory_intf.S) = struct
let cpt = ref 0 in let cpt = ref 0 in
fun () -> incr cpt; "C" ^ (string_of_int !cpt) fun () -> incr cpt; "C" ^ (string_of_int !cpt)
let clear () =
cpt_mk_var := 0;
ma := MA.empty
(* Pretty printing for atoms and clauses *) (* Pretty printing for atoms and clauses *)
let print_atom fmt a = E.Formula.print fmt a.lit let print_atom fmt a = E.Formula.print fmt a.lit
@ -178,15 +235,16 @@ module Make (E : Expr_intf.S)(Th : Theory_intf.S) = struct
Format.fprintf fmt "%s : %a" c.name print_atoms c.atoms Format.fprintf fmt "%s : %a" c.name print_atoms c.atoms
(* Complete debug printing *) (* 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 = 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 | n, _ when n < 0 -> assert false
| 0, Some c -> sprintf "->0/%s" c.name | 0, Bcp (Some c) -> sprintf "->0/%s" c.name
| 0, None -> "@0" | 0, Bcp None -> "@0"
| n, Some c -> sprintf "->%d/%s" n c.name | n, Bcp (Some c) -> sprintf "->%d/%s" n c.name
| n, None -> sprintf "@@%d" n | n, Bcp None -> sprintf "@@%d" n
| _ -> assert false
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)
@ -200,7 +258,7 @@ module Make (E : Expr_intf.S)(Th : Theory_intf.S) = struct
let pp_atom b a = let pp_atom b a =
bprintf b "%s%d%s [lit:%s] vpremise={{%a}}" bprintf b "%s%d%s [lit:%s] vpremise={{%a}}"
(sign a) (a.var.vid+1) (value a) (Log.on_fmt E.Formula.print a.lit) (sign a) (a.var.vid+1) (value a) (Log.on_fmt E.Formula.print a.lit)
pp_premise a.var.vpremise pp_premise a.var.tag.vpremise
let pp_atoms_vec b vec = let pp_atoms_vec b vec =
for i = 0 to Vec.size vec - 1 do for i = 0 to Vec.size vec - 1 do

6
mcsolver/mcsolver_types.mli
View file

@ -11,8 +11,8 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
module type S = Solver_types_intf.S module type S = Mcsolver_types_intf.S
module Make : functor (E : Expr_intf.S)(Th : Theory_intf.S) module Make : functor (E : Expr_intf.S)(Th : Plugin_intf.S)
-> S with type formula = E.Formula.t and type proof = Th.proof -> 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. *) (** Functor to instantiate the types of clauses for the Solver. *)

50
mcsolver/mcsolver_types_intf.ml
View file

@ -14,22 +14,31 @@
module type S = sig module type S = sig
(** The signatures of clauses used in the Solver. *) (** The signatures of clauses used in the Solver. *)
type term
type formula type formula
type proof type proof
type var = {
vid : int; 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; pa : atom;
na : atom; na : atom;
mutable weight : float;
mutable seen : bool; mutable seen : bool;
mutable level : int;
mutable reason : reason; mutable reason : reason;
mutable vpremise : premise mutable vpremise : premise
} }
and atom = { and atom = {
var : var; var : boolean var;
lit : formula; lit : formula;
neg : atom; neg : atom;
mutable watched : clause Vec.t; mutable watched : clause Vec.t;
@ -46,43 +55,46 @@ module type S = sig
cpremise : premise cpremise : premise
} }
and reason = clause option and reason =
| Semantic of int
| Bcp of clause option
and premise = and premise =
| History of clause list | History of clause list
| Lemma of proof | Lemma of proof
type elt =
| Term of semantic var
| Formula of boolean var
(** Recursive types for literals (atoms) and clauses *) (** Recursive types for literals (atoms) and clauses *)
val dummy_var : var val dummy_var : boolean var
val dummy_atom : atom val dummy_atom : atom
val dummy_clause : clause val dummy_clause : clause
(** Dummy values for use in vector dummys *) (** Dummy values for use in vector dummys *)
val empty_clause : clause val nb_vars : unit -> int
(** The empty clause *) val get_var : int -> elt
val iter_vars : (elt -> unit) -> unit
(** Read access to the vector of variables created *)
val add_atom : formula -> atom val add_atom : formula -> atom
(** Returns the atom associated with the given formula *) (** Returns the atom associated with the given formula *)
val add_term : term -> semantic var
val make_var : formula -> var * bool (** 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 (** Returns the variable linked with the given formula, and wether the atom associated with the formula
is [var.pa] or [var.na] *) is [var.pa] or [var.na] *)
val empty_clause : clause
(** The empty clause *)
val make_clause : string -> atom list -> int -> bool -> premise -> 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. *) (** [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_name : unit -> string
val fresh_lname : unit -> string val fresh_lname : unit -> string
val fresh_dname : unit -> string val fresh_dname : unit -> string
(** Fresh names for clauses *) (** Fresh names for clauses *)
val clear : unit -> unit
(** Forget all variables cretaed *)
val print_atom : Format.formatter -> atom -> unit val print_atom : Format.formatter -> atom -> unit
val print_clause : Format.formatter -> clause -> unit val print_clause : Format.formatter -> clause -> unit
(** Pretty printing functions for atoms and clauses *) (** Pretty printing functions for atoms and clauses *)

24
mcsolver/plugin_intf.ml
View file

@ -15,16 +15,23 @@
module type S = sig module type S = sig
(** Singature for theories to be given to the Solver. *) (** Singature for theories to be given to the Solver. *)
type term
(** The type of terms. Should be compatible with Expr_intf.Term.t*)
type formula type formula
(** The type of formulas. Should be compatble with Formula_intf.S *) (** The type of formulas. Should be compatble with Expr_intf.Formula.t *)
type proof type proof
(** A custom type for the proofs of lemmas produced by the theory. *) (** A custom type for the proofs of lemmas produced by the theory. *)
type assumption =
| Lit of formula
| Assign of term * term (* Assign(x, alpha) *)
type slice = { type slice = {
start : int; start : int;
length : int; length : int;
get : int -> formula; get : int -> assumption;
push : formula list -> proof -> unit; push : formula list -> proof -> unit;
} }
(** The type for a slice of litterals to assume/propagate in the theory. (** The type for a slice of litterals to assume/propagate in the theory.
@ -42,6 +49,10 @@ module type S = sig
| Sat of level | Sat of level
| Unsat of formula list * proof | Unsat of formula list * proof
type eval_res =
| Bool of bool
| Unknown
val dummy : level val dummy : level
(** A dummy level. *) (** A dummy level. *)
@ -57,5 +68,14 @@ module type S = sig
(** Backtrack to the given level. After a call to [backtrack l], the theory should be in the (** Backtrack to the given level. After a call to [backtrack l], the theory should be in the
same state as when it returned the value [l], *) same state as when it returned the value [l], *)
val assign : term -> term
(** Returns an assignment value for the given term. *)
val iter_assignable : (term -> unit) -> formula -> unit
(** An iterator over the subterms of a formula that should be assigned a value (usually the poure subterms) *)
val eval : formula -> eval_res
(** Returns the evaluation of the formula in the current assignment *)
end end