mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 11:15:43 -05:00
f88a5dd514
This ensures that the same solver_types module is not reused for two different solvers, which would be problematic. Marked minor because of the low use of multiple instances of a solver.
309 lines
8.2 KiB
OCaml
309 lines
8.2 KiB
OCaml
(**************************************************************************)
|
||
(* *)
|
||
(* 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 = Solver_types_intf.S
|
||
|
||
(* Solver types for McSat Solving *)
|
||
(* ************************************************************************ *)
|
||
|
||
module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
|
||
|
||
(* Flag for Mcsat v.s Pure Sat *)
|
||
let mcsat = true
|
||
|
||
type term = E.Term.t
|
||
type formula = E.Formula.t
|
||
type proof = E.proof
|
||
|
||
type lit = {
|
||
lid : int;
|
||
term : term;
|
||
mutable l_level : int;
|
||
mutable l_weight : float;
|
||
mutable assigned : term option;
|
||
}
|
||
|
||
type var = {
|
||
vid : int;
|
||
pa : atom;
|
||
na : atom;
|
||
mutable seen : bool;
|
||
mutable v_level : int;
|
||
mutable v_weight : float;
|
||
mutable reason : reason option;
|
||
}
|
||
|
||
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;
|
||
c_level : int;
|
||
mutable cpremise : premise;
|
||
mutable activity : float;
|
||
mutable removed : bool;
|
||
}
|
||
|
||
and reason =
|
||
| Decision
|
||
| Bcp of clause
|
||
| Semantic of int
|
||
|
||
and premise =
|
||
| Lemma of proof
|
||
| History of clause list
|
||
|
||
type elt = (lit, var) Either.t
|
||
|
||
(* Dummy values *)
|
||
let dummy_lit = E.dummy
|
||
|
||
let rec dummy_var =
|
||
{ vid = -101;
|
||
pa = dummy_atom;
|
||
na = dummy_atom;
|
||
seen = false;
|
||
v_level = -1;
|
||
v_weight = -1.;
|
||
reason = 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.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_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 t =
|
||
try MT.find t_map t
|
||
with Not_found ->
|
||
let res = {
|
||
lid = !cpt_mk_var;
|
||
term = t;
|
||
l_weight = 1.;
|
||
l_level = -1;
|
||
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;
|
||
pa = pa;
|
||
na = na;
|
||
seen = false;
|
||
v_level = -1;
|
||
v_weight = 0.;
|
||
reason = 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);
|
||
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 = (lit, atom) Either.t
|
||
|
||
let of_lit = Either.mk_left
|
||
let of_atom = Either.mk_right
|
||
let destruct = Either.destruct
|
||
|
||
(* Elements *)
|
||
let elt_of_lit = Either.mk_left
|
||
let elt_of_var = Either.mk_right
|
||
|
||
let get_elt_id = function
|
||
| Either.Left l -> l.lid | Either.Right v -> v.vid
|
||
let get_elt_level = function
|
||
| Either.Left l -> l.l_level | Either.Right v -> v.v_level
|
||
let get_elt_weight = function
|
||
| Either.Left l -> l.l_weight | Either.Right v -> v.v_weight
|
||
|
||
let set_elt_level e lvl = match e with
|
||
| Either.Left l -> l.l_level <- lvl | Either.Right v -> v.v_level <- lvl
|
||
let set_elt_weight e w = match e with
|
||
| Either.Left l -> l.l_weight <- w | Either.Right v -> v.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)
|
||
|
||
(* Pretty printing for atoms and clauses *)
|
||
let print_lit fmt v = E.Term.print fmt v.term
|
||
|
||
let print_atom fmt a = E.Formula.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
|
||
|
||
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.v_level, a.var.reason with
|
||
| n, _ when n < 0 -> sprintf "%%"
|
||
| n, None -> sprintf "%d" n
|
||
| n, Some Decision -> sprintf "@@%d" n
|
||
| n, Some Bcp c -> sprintf "->%d/%s" n c.name
|
||
| n, Some 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 out = function
|
||
| History v -> List.iter (fun {name=name} -> Format.fprintf out "%s,@," name) v
|
||
| Lemma _ -> Format.fprintf out "th_lemma"
|
||
|
||
let pp_assign out = function
|
||
| None -> ()
|
||
| Some t -> Format.fprintf out "[assignment: %a]" E.Term.print t
|
||
|
||
let pp_lit out v =
|
||
Format.fprintf out "%d [lit:%a]%a"
|
||
(v.lid+1) E.Term.print v.term pp_assign v.assigned
|
||
|
||
let pp_atom out a =
|
||
Format.fprintf out "%s%d%s[lit:%a]"
|
||
(sign a) (a.var.vid+1) (value a) E.Formula.print a.lit
|
||
|
||
let pp_atoms_vec out vec =
|
||
Vec.print ~sep:"; " pp_atom out vec
|
||
|
||
let pp_clause out {name=name; atoms=arr; cpremise=cp; learnt=learnt} =
|
||
Format.fprintf out "%s%s{ %a} cpremise={{%a}}"
|
||
name (if learnt then "!" else ":") pp_atoms_vec arr pp_premise cp
|
||
|
||
end
|
||
|
||
|
||
(* Solver types for pure SAT Solving *)
|
||
(* ************************************************************************ *)
|
||
|
||
module SatMake (E : Formula_intf.S)(Dummy : sig end) = struct
|
||
include McMake(struct
|
||
include E
|
||
module Term = E
|
||
module Formula = E
|
||
end)(struct end)
|
||
|
||
let mcsat = false
|
||
end
|
||
|