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

Removed special solver types module for pure SAT

Browse source 
This specialisation was there to have better performances,
but it doesn't seem to have any impact anymore.
This commit is contained in:
Guillaume Bury 2015-11-27 15:23:04 +01:00
parent 656b7d4fd7
commit f9f88e0767
1 changed files with 9 additions and 259 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

266
solver/solver_types.ml
View file

@ -20,6 +20,9 @@ module type S = Solver_types_intf.S
module McMake (L : Log_intf.S)(E : Expr_intf.S) = struct module McMake (L : Log_intf.S)(E : Expr_intf.S) = struct
(* Flag for Mcsat v.s Pure Sat *)
let mcsat = true
type term = E.Term.t type term = E.Term.t
type formula = E.Formula.t type formula = E.Formula.t
type proof = E.proof type proof = E.proof
@ -70,9 +73,6 @@ module McMake (L : Log_intf.S)(E : Expr_intf.S) = struct
| Lemma of proof | Lemma of proof
| History of clause list | History of clause list
(* Flag for Mcsat v.s Pure Sat *)
let mcsat = true
type elt = (lit, var) Either.t type elt = (lit, var) Either.t
(* Dummy values *) (* Dummy values *)
@ -302,262 +302,12 @@ end
(* ************************************************************************ *) (* ************************************************************************ *)
module SatMake (L : Log_intf.S)(E : Formula_intf.S) = struct module SatMake (L : Log_intf.S)(E : Formula_intf.S) = struct
include McMake(L)(struct
include E
module Term = E
module Formula = E
end)
type term = E.t
type formula = E.t
type proof = E.proof
type lit = {
lid : int;
term : term;
mutable level : int;
mutable weight : float;
mutable assigned : term option;
}
type var = {
vid : int;
pa : atom;
na : atom;
mutable seen : bool;
mutable level : int;
mutable weight : float;
mutable reason : reason;
}
and atom = {
aid : int;
var : var;
neg : atom;
lit : formula;
mutable is_true : bool;
mutable watched : clause Vec.t;
}
and clause = {
name : string;
tag : int option;
atoms : atom Vec.t;
learnt : bool;
cpremise : premise;
c_level : int;
mutable activity : float;
mutable removed : bool;
}
and reason =
| Semantic of int
| Bcp of clause option
and premise =
| Lemma of proof
| History of clause list
(* Flag for Mcsat v.s Pure Sat *)
let mcsat = false let mcsat = false
(* Types declarations *)
type elt = var
(* Dummy values *)
let dummy_lit = E.dummy
let rec dummy_var =
{ vid = -101;
pa = dummy_atom;
na = dummy_atom;
seen = false;
level = -1;
weight = -1.;
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 = "";
tag = None;
atoms = Vec.make_empty dummy_atom;
activity = -1.;
removed = false;
c_level = -1;
learnt = false;
cpremise = History [] }
let () =
dummy_atom.watched <- Vec.make_empty dummy_clause
(* Constructors *)
module MF = Hashtbl.Make(E)
let f_map = MF.create 4096
let vars = Vec.make 107 dummy_var
let nb_elt () = Vec.size vars
let get_elt i = Vec.get vars i
let iter_elt f = Vec.iter f vars
let cpt_mk_var = ref 0
let make_semantic_var _ = assert false
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;
pa = pa;
na = na;
seen = false;
level = -1;
weight = 0.;
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 var;
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.na else var.pa
let make_clause ?tag name ali sz_ali is_learnt premise lvl =
let atoms = Vec.from_list ali sz_ali dummy_atom in
{ name = name;
tag = tag;
atoms = atoms;
removed = false;
learnt = is_learnt;
c_level = lvl;
activity = 0.;
cpremise = premise}
let empty_clause = make_clause "Empty" [] 0 false (History []) 0
(* Decisions & propagations *)
type t = atom
let of_lit _ = assert false
let of_atom a = a
let destruct e _ f = f e
(* Elements *)
let elt_of_lit _ = assert false
let elt_of_var v = v
let destruct_elt v _ f = f v
let get_elt_id v = v.vid
let get_elt_level v = v.level
let get_elt_weight v = v.weight
let set_elt_level v lvl = v.level <- lvl
let set_elt_weight v w = v.weight <- w
(* 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 *)
let iter_sub _ _ = ()
(* Proof debug info *)
let proof_debug _ = "lemma", [], [], None
(* Pretty printing for atoms and clauses *)
let print_lit _ _ = assert false
let print_atom fmt a = E.print fmt a.lit
let print_atoms fmt v =
if Vec.size v = 0 then
Format.fprintf fmt "∅"
else begin
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
end 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.pa then "" else "-"
let level a =
match a.var.level, a.var.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 _ _ = ()
let pp_lit b v = bprintf b "%d [lit:()]" (v.lid+1)
let pp_atom b a =
bprintf b "%s%d%s[lit:%s]"
(sign a) (a.var.vid+1) (value a) (Log.on_fmt E.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