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

Moved some type def outside Plugins/Theories

Browse source
This commit is contained in:
Guillaume Bury 2016-07-08 14:29:45 +02:00
parent 46b621269c
commit eb2850caa6
6 changed files with 107 additions and 149 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

62
src/core/internal.ml
View file

@ -6,7 +6,9 @@ Copyright 2014 Simon Cruanes
module Make
(St : Solver_types.S)
(Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof)
(Plugin : Plugin_intf.S with type term = St.term
and type formula = St.formula
and type proof = St.proof)
(Dummy: sig end)
= struct
@ -25,7 +27,7 @@ module Make
(* 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 decicion level 0 *)
ul_th_env : Th.level; (* Theory state at 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 *)
}
@ -48,7 +50,7 @@ module Make
elt_levels : int Vec.t;
(* decision levels in [trail] *)
th_levels : Th.level Vec.t;
th_levels : Plugin.level Vec.t;
(* theory states corresponding to elt_levels *)
user_levels : user_level Vec.t;
(* user-defined levels, for {!push} and {!pop} *)
@ -120,14 +122,14 @@ module Make
elt_queue = Vec.make 601 (of_atom dummy_atom);
elt_levels = Vec.make 601 (-1);
th_levels = Vec.make 100 Th.dummy;
th_levels = Vec.make 100 Plugin.dummy;
user_levels = Vec.make 20 {
ul_elt_lvl = 0;
ul_th_lvl = 0;
ul_learnt = 0;
ul_clauses = 0;
ul_th_env = Th.dummy;
ul_th_env = Plugin.dummy;
};
order = Iheap.init 0;
@ -199,7 +201,7 @@ module Make
let l = Vec.get env.elt_levels 0 in
l, l
and ul_th_env =
if Vec.is_empty env.th_levels then Th.current_level ()
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. *)
@ -230,7 +232,7 @@ module Make
List.iter f (Hashtbl.find iter_map v.vid)
with Not_found ->
let l = ref [] in
Th.iter_assignable (fun t -> l := add_term t :: !l) v.pa.lit;
Plugin.iter_assignable (fun t -> l := add_term t :: !l) v.pa.lit;
Hashtbl.add iter_map v.vid !l;
List.iter f !l
@ -397,7 +399,7 @@ module Make
assert (env.th_head = Vec.size env.elt_queue);
assert (env.elt_head = Vec.size env.elt_queue);
Vec.push env.elt_levels (Vec.size env.elt_queue);
Vec.push env.th_levels (Th.current_level ()); (* save the current tenv *)
Vec.push env.th_levels (Plugin.current_level ()); (* save the current tenv *)
()
(* Attach/Detach a clause.
@ -464,7 +466,7 @@ module Make
end
done;
(* Recover the right theory state. *)
Th.backtrack (Vec.get env.th_levels lvl);
Plugin.backtrack (Vec.get env.th_levels lvl);
(* Resize the vectors according to their new size. *)
Vec.shrink env.elt_queue ((Vec.size env.elt_queue) - env.elt_head);
Vec.shrink env.elt_levels ((Vec.size env.elt_levels) - lvl);
@ -534,9 +536,9 @@ module Make
let th_eval a =
if a.is_true || a.neg.is_true then None
else match Th.eval a.lit with
| Th.Unknown -> None
| Th.Valued (b, lvl) ->
else match Plugin.eval a.lit with
| Plugin_intf.Unknown -> None
| Plugin_intf.Valued (b, lvl) ->
let atom = if b then a else a.neg in
enqueue_bool atom lvl (Semantic lvl);
Some b
@ -812,8 +814,10 @@ module Make
let slice_get i =
match Vec.get env.elt_queue i with
| Either.Right a -> Th.Lit a.lit, a.var.v_level
| Either.Left {l_level; term; assigned = Some v} -> Th.Assign (term, v), l_level
| Either.Right a ->
Plugin_intf.Lit a.lit
| Either.Left {l_level; term; assigned = Some v} ->
Plugin_intf.Assign (term, v, l_level)
| Either.Left _ -> assert false
let slice_push l lemma =
@ -828,21 +832,21 @@ module Make
Iheap.grow_to_by_double env.order (St.nb_elt ());
enqueue_bool a lvl (Semantic lvl)
let current_slice () = Th.({
start = env.th_head;
let current_slice () = {
Plugin_intf.start = env.th_head;
length = (Vec.size env.elt_queue) - env.th_head;
get = slice_get;
push = slice_push;
propagate = slice_propagate;
})
}
let full_slice () = Th.({
start = 0;
let full_slice () = {
Plugin_intf.start = 0;
length = Vec.size env.elt_queue;
get = slice_get;
push = slice_push;
propagate = (fun _ -> assert false);
})
}
let rec theory_propagate () =
assert (env.elt_head = Vec.size env.elt_queue);
@ -851,10 +855,10 @@ module Make
else begin
let slice = current_slice () in
env.th_head <- env.elt_head;
match Th.assume slice with
| Th.Sat ->
match Plugin.assume slice with
| Plugin_intf.Sat ->
propagate ()
| Th.Unsat (l, p) ->
| Plugin_intf.Unsat (l, p) ->
let l = List.rev_map new_atom l in
Iheap.grow_to_by_double env.order (St.nb_elt ());
List.iter (fun a -> insert_var_order (elt_of_var a.var)) l;
@ -965,13 +969,13 @@ module Make
if v.v_level >= 0 then begin
assert (v.pa.is_true || v.na.is_true);
pick_branch_lit ()
end else match Th.eval atom.lit with
| Th.Unknown ->
end else match Plugin.eval atom.lit with
| Plugin_intf.Unknown ->
env.decisions <- env.decisions + 1;
new_decision_level();
let current_level = decision_level () in
enqueue_bool atom current_level Decision
| Th.Valued (b, lvl) ->
| Plugin_intf.Valued (b, lvl) ->
let a = if b then atom else atom.neg in
enqueue_bool a lvl (Semantic lvl)
@ -987,7 +991,7 @@ module Make
if l.l_level >= 0 then
pick_branch_lit ()
else begin
let value = Th.assign l.term in
let value = Plugin.assign l.term in
env.decisions <- env.decisions + 1;
new_decision_level();
let current_level = decision_level () in
@ -1064,7 +1068,7 @@ module Make
n_of_conflicts := !n_of_conflicts *. env.restart_inc;
n_of_learnts := !n_of_learnts *. env.learntsize_inc
| Sat ->
Th.if_sat (full_slice ());
Plugin.if_sat (full_slice ());
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
@ -1148,7 +1152,7 @@ module Make
end
end
done;
Th.backtrack th_env; (* recover the right theory env *)
Plugin.backtrack 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;

64
src/core/plugin_intf.ml
View file

@ -12,6 +12,39 @@
(* *)
(**************************************************************************)
type eval_res =
| Valued of bool * int
| Unknown
(** The type of evaluation results, either the given formula cannot be
evaluated, or it can thanks to assignment. In that case, the level
of the evaluation is the maximum of levels of assignemnts needed
to evaluate the given formula. *)
type ('formula, 'proof) res =
| Sat
| Unsat of 'formula list * 'proof
(** Type returned by the theory, either the current set of assumptions is satisfiable,
or it is not, in which case a tautological clause (hopefully minimal) is returned.
Formulas in the unsat clause must come from the current set of assumptions, i.e
must have been encountered in a slice. *)
type ('term, 'formula) assumption =
| Lit of 'formula
| Assign of 'term * 'term * int (* Assign(x, alpha) *)
(** Asusmptions made by the core SAT solver. Can be either a formula, or an assignment.
Assignemnt are given a level. *)
type ('term, 'formula, 'proof) slice = {
start : int;
length : int;
get : int -> ('term, 'formula) assumption;
push : 'formula list -> 'proof -> unit;
propagate : 'formula -> int -> unit;
}
(** The type for a slice of litterals to assume/propagate in the theory.
[get] operations should only be used for integers [ start <= i < start + length].
[push clause proof] allows to add a tautological clause to the sat solver. *)
module type S = sig
(** Signature for theories to be given to the Model Constructing Solver. *)
@ -24,36 +57,9 @@ module type S = sig
type proof
(** 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 = {
start : int;
length : int;
get : int -> assumption * int;
push : formula list -> proof -> unit;
propagate : formula -> int -> unit;
}
(** The type for a slice of litterals to assume/propagate in the theory.
[get] operations should only be used for integers [ start <= i < start + length].
[push clause proof] allows to add a tautological clause to the sat solver. *)
type level
(** The type for levels to allow backtracking. *)
(** Type returned by the theory, either the current set of assumptions is satisfiable,
or it is not, in which case a tautological clause (hopefully minimal) is returned.
Formulas in the unsat clause must come from the current set of assumptions, i.e
must have been encountered in a slice. *)
type res =
| Sat
| Unsat of formula list * proof
type eval_res =
| Valued of bool * int
| Unknown
val dummy : level
(** A dummy level. *)
@ -61,7 +67,7 @@ module type S = sig
(** Return the current level of the theory (either the empty/beginning state, or the
last level returned by the [assume] function). *)
val assume : slice -> res
val assume : (term, formula, proof) slice -> (formula, proof) res
(** Assume the formulas in the slice, possibly pushing new formulas to be propagated,
and returns the result of the new assumptions. *)
@ -78,7 +84,7 @@ module type S = sig
val eval : formula -> eval_res
(** Returns the evaluation of the formula in the current assignment *)
val if_sat : slice -> unit
val if_sat : (term, formula, proof) slice -> unit
(** Called at the end of the search in case a model has been found. If no new clause is
pushed, then 'sat' is returned, else search is resumed. *)

18
src/core/theory_intf.ml
View file

@ -12,6 +12,14 @@
(* *)
(**************************************************************************)
type ('formula, 'proof) res = ('formula, 'proof) Plugin_intf.res =
| Sat
| Unsat of 'formula list * 'proof
(** Type returned by the theory, either the current set of assumptions is satisfiable,
or it is not, in which case a tautological clause (hopefully minimal) is returned.
Formulas in the unsat clause must come from the current set of assumptions, i.e
must have been encountered in a slice. *)
type ('form, 'proof) slice = {
start : int;
length : int;
@ -34,14 +42,6 @@ module type S = sig
type level
(** The type for levels to allow backtracking. *)
(** Type returned by the theory, either the current set of assumptions is satisfiable,
or it is not, in which case a tautological clause (hopefully minimal) is returned.
Formulas in the unsat clause must come from the current set of assumptions, i.e
must have been encountered in a slice. *)
type res =
| Sat of level
| Unsat of formula list * proof
val dummy : level
(** A dummy level. *)
@ -49,7 +49,7 @@ module type S = sig
(** Return the current level of the theory (either the empty/beginning state, or the
last level returned by the [assume] function). *)
val assume : (formula, proof) slice -> res
val assume : (formula, proof) slice -> (formula, proof) res
(** Assume the formulas in the slice, possibly pushing new formulas to be propagated,
and returns the result of the new assumptions. *)

39
src/example/mcsat.ml
View file

@ -16,31 +16,11 @@ module Tsmt = struct
type formula = Fsmt.t
type proof = unit
type assumption =
| Lit of formula
| Assign of term * term
type slice = {
start : int;
length : int;
get : int -> assumption * int;
push : formula list -> proof -> unit;
propagate : formula -> int -> unit;
}
type level = {
cc : CC.t;
assign : (term * int) M.t;
}
type res =
| Sat
| Unsat of formula list * proof
type eval_res =
| Valued of bool * int
| Unknown
(* Functions *)
let dummy = { cc = CC.empty; assign = M.empty; }
@ -60,12 +40,13 @@ module Tsmt = struct
(Fsmt.mk_eq a b) :: (List.rev_map Fsmt.neg (aux [] l))
let assume s =
let open Plugin_intf in
try
for i = s.start to s.start + s.length - 1 do
match s.get i with
| (Assign (x, v)), lvl ->
| Assign (x, v, lvl) ->
env := { !env with assign = M.add x (v, lvl) !env.assign }
| Lit f, _ ->
| Lit f ->
Log.debugf 10 "Propagating in th :@ @[%a@]" (fun k->k Fsmt.print f);
match f with
| Fsmt.Prop _ -> ()
@ -91,19 +72,23 @@ module Tsmt = struct
let max (a: int) (b: int) = if a < b then b else a
let eval = function
| Fsmt.Prop _ -> Unknown
| Fsmt.Prop _ -> Plugin_intf.Unknown
| Fsmt.Equal (a, b) ->
begin try
let a', lvl_a = M.find a !env.assign in
let b', lvl_b = M.find b !env.assign in
Valued (Fsmt.Term.equal a' b', max lvl_a lvl_b)
with Not_found -> Unknown end
Plugin_intf.Valued (Fsmt.Term.equal a' b', max lvl_a lvl_b)
with Not_found ->
Plugin_intf.Unknown
end
| Fsmt.Distinct (a, b) ->
begin try
let a', lvl_a = M.find a !env.assign in
let b', lvl_b = M.find b !env.assign in
Valued (not (Fsmt.Term.equal a' b'), max lvl_a lvl_b)
with Not_found -> Unknown end
Plugin_intf.Valued (not (Fsmt.Term.equal a' b'), max lvl_a lvl_b)
with Not_found ->
Plugin_intf.Unknown
end
let if_sat _ = ()

14
src/example/smt.ml
View file

@ -5,7 +5,6 @@ Copyright 2014 Simon Cruanes
*)
module Fsmt = Expr
module ThI = Theory_intf
module Tsmt = struct
@ -15,10 +14,6 @@ module Tsmt = struct
type proof = unit
type level = CC.t
type res =
| Sat of level
| Unsat of formula list * proof
let dummy = CC.empty
let env = ref dummy
@ -37,15 +32,16 @@ module Tsmt = struct
(Fsmt.mk_eq a b) :: (List.rev_map Fsmt.neg (aux [] l))
let assume s =
let open Theory_intf in
try
for i = s.ThI.start to s.ThI.start + s.ThI.length - 1 do
Log.debugf 10 "Propagating in th :@ @[%a@]" (fun k->k Fsmt.print (s.ThI.get i));
match s.ThI.get i with
for i = s.start to s.start + s.length - 1 do
Log.debugf 10 "Propagating in th :@ @[%a@]" (fun k->k Fsmt.print (s.get i));
match s.get i with
| Fsmt.Prop _ -> ()
| Fsmt.Equal (i, j) -> env := CC.add_eq !env i j
| Fsmt.Distinct (i, j) -> env := CC.add_neq !env i j
done;
Sat (current_level ())
Sat
with CC.Unsat x ->
Log.debug 8 "Making explanation clause...";
Unsat (to_clause x, ())

59
src/solver/solver.ml
View file

@ -11,7 +11,6 @@
(**************************************************************************)
module type S = Solver_intf.S
module ThI = Theory_intf
module DummyTheory(F : Formula_intf.S) = struct
(* We don't have anything to do since the SAT Solver already
@ -21,20 +20,9 @@ module DummyTheory(F : Formula_intf.S) = struct
type proof = F.proof
type level = unit
type slice = {
start : int;
length : int;
get : int -> formula;
push : formula list -> proof -> unit;
}
type res =
| Sat of level
| Unsat of formula list * proof
let dummy = ()
let current_level () = ()
let assume _ = Sat ()
let assume _ = Theory_intf.Sat
let backtrack _ = ()
end
@ -44,46 +32,25 @@ module Plugin(E : Formula_intf.S)
type term = E.t
type formula = E.t
type proof = Th.proof
type assumption =
| Lit of formula
| Assign of term * term
type slice = {
start : int;
length : int;
get : int -> assumption * int;
push : formula list -> proof -> unit;
propagate : formula -> int -> unit;
}
type level = Th.level
type res =
| Sat
| Unsat of formula list * proof
type eval_res =
| Valued of bool * int
| Unknown
let dummy = Th.dummy
let current_level = Th.current_level
let assume_get s i = match s.get i with
| Lit f, _ -> f | _ -> assert false
let assume_get s i =
match s.Plugin_intf.get i with
| Plugin_intf.Lit f -> f
| _ -> assert false
let assume s =
match Th.assume {
ThI.
start = s.start;
length = s.length;
get = assume_get s;
push = s.push;
} with
| Th.Sat _ -> Sat
| Th.Unsat (l, p) -> Unsat (l, p)
let slice = {
Theory_intf.start = s.Plugin_intf.start;
length = s.Plugin_intf.length;
get = assume_get s;
push = s.Plugin_intf.push;
} in
Th.assume slice
let backtrack = Th.backtrack
@ -91,7 +58,7 @@ module Plugin(E : Formula_intf.S)
let iter_assignable _ _ = ()
let eval _ = Unknown
let eval _ = Plugin_intf.Unknown
let if_sat _ = ()