mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-07 11:45:41 -05:00
Added some abstraction to allow for more direct types int the pure SAT
solver
This commit is contained in:
Guillaume Bury
parent
ce05d8fe62
commit
e7140d6897
7 changed files with 382 additions and 856 deletions
|
|
@ -46,11 +46,8 @@ module Tsmt = struct
|
|||
Log.debug 10 "Propagating in th : %s" (Log.on_fmt Fsmt.print (s.get i));
|
||||
match s.get i with
|
||||
| Fsmt.Prop _ -> ()
|
||||
| Fsmt.Equal (i, j) as f ->
|
||||
env := CC.add_eq !env i j
|
||||
| Fsmt.Distinct (i, j) as f ->
|
||||
env := CC.add_neq !env i j
|
||||
| _ -> assert false
|
||||
| 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 ())
|
||||
with CC.Unsat x ->
|
||||
|
|
@ -84,7 +81,6 @@ module Make(Dummy:sig end) = struct
|
|||
with SmtSolver.Unsat -> ()
|
||||
|
||||
let get_proof () =
|
||||
(* SmtSolver.Proof.learn (SmtSolver.history ()); *)
|
||||
match SmtSolver.unsat_conflict () with
|
||||
| None -> assert false
|
||||
| Some c -> SmtSolver.Proof.prove_unsat c
|
||||
|
|
|
|||
|
|
@ -43,7 +43,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
|
|||
mutable var_inc : float;
|
||||
(* increment for variables' activity *)
|
||||
|
||||
trail : (lit, atom) Either.t Vec.t;
|
||||
trail : t Vec.t;
|
||||
(* decision stack + propagated atoms *)
|
||||
|
||||
trail_lim : int Vec.t;
|
||||
|
|
@ -114,7 +114,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
|
|||
learnts = Vec.make 0 dummy_clause; (*updated during parsing*)
|
||||
clause_inc = 1.;
|
||||
var_inc = 1.;
|
||||
trail = Vec.make 601 (Either.mk_right dummy_atom);
|
||||
trail = Vec.make 601 (of_atom dummy_atom);
|
||||
trail_lim = Vec.make 601 (-1);
|
||||
user_levels = Vec.make 20 {ul_trail=0;ul_learnt=0;ul_clauses=0};
|
||||
qhead = 0;
|
||||
|
|
@ -148,35 +148,15 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
|
|||
let to_float i = float_of_int i
|
||||
let to_int f = int_of_float f
|
||||
|
||||
(* Accessors for variables *)
|
||||
let get_var_id v = v.vid
|
||||
let get_var_level v = v.level
|
||||
let get_var_weight v = v.weight
|
||||
let set_var_weight v w = v.weight <- w
|
||||
let set_var_level v l = v.level <- l
|
||||
|
||||
(* Accessors for litterals *)
|
||||
let get_lit_id v = v.lid
|
||||
let get_lit_level (v : lit) = v.level
|
||||
let get_lit_weight (v : lit) = v.weight
|
||||
let set_lit_weight (v : lit) w = v.weight <- w
|
||||
let set_lit_level (v : lit) l = v.level <- l
|
||||
|
||||
let get_elt_id e = Either.destruct e get_lit_id get_var_id
|
||||
let get_elt_weight e = Either.destruct e get_lit_weight get_var_weight
|
||||
let get_elt_level e = Either.destruct e get_lit_level get_var_level
|
||||
|
||||
let set_elt_weight e = Either.destruct e set_lit_weight set_var_weight
|
||||
let set_elt_level e = Either.destruct e set_lit_level set_var_level
|
||||
|
||||
let f_weight i j =
|
||||
get_elt_weight (St.get_var j) < get_elt_weight (St.get_var i)
|
||||
get_elt_weight (St.get_elt j) < get_elt_weight (St.get_elt i)
|
||||
|
||||
let f_filter i =
|
||||
get_elt_level (St.get_var i) < 0
|
||||
get_elt_level (St.get_elt i) < 0
|
||||
|
||||
(* Var/clause activity *)
|
||||
let insert_var_order e = Either.destruct e
|
||||
let insert_var_order e = destruct_elt e
|
||||
(fun v -> Iheap.insert f_weight env.order v.lid)
|
||||
(fun v ->
|
||||
Iheap.insert f_weight env.order v.vid;
|
||||
|
|
@ -192,8 +172,8 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
|
|||
let var_bump_activity_aux v =
|
||||
v.weight <- v.weight +. env.var_inc;
|
||||
if v.weight > 1e100 then begin
|
||||
for i = 0 to (St.nb_vars ()) - 1 do
|
||||
set_elt_weight (St.get_var i) ((get_elt_weight (St.get_var i)) *. 1e-100)
|
||||
for i = 0 to (St.nb_elt ()) - 1 do
|
||||
set_elt_weight (St.get_elt i) ((get_elt_weight (St.get_elt i)) *. 1e-100)
|
||||
done;
|
||||
env.var_inc <- env.var_inc *. 1e-100;
|
||||
end;
|
||||
|
|
@ -203,8 +183,8 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
|
|||
let lit_bump_activity_aux (v : lit) =
|
||||
v.weight <- v.weight +. env.var_inc;
|
||||
if v.weight > 1e100 then begin
|
||||
for i = 0 to (St.nb_vars ()) - 1 do
|
||||
set_elt_weight (St.get_var i) ((get_elt_weight (St.get_var i)) *. 1e-100)
|
||||
for i = 0 to (St.nb_elt ()) - 1 do
|
||||
set_elt_weight (St.get_elt i) ((get_elt_weight (St.get_elt i)) *. 1e-100)
|
||||
done;
|
||||
env.var_inc <- env.var_inc *. 1e-100;
|
||||
end;
|
||||
|
|
@ -231,7 +211,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
|
|||
let nb_assigns () = Vec.size env.trail
|
||||
let nb_clauses () = Vec.size env.clauses
|
||||
let nb_learnts () = Vec.size env.learnts
|
||||
let nb_vars () = St.nb_vars ()
|
||||
let nb_vars () = St.nb_elt ()
|
||||
|
||||
let new_decision_level() =
|
||||
Vec.push env.trail_lim (Vec.size env.trail);
|
||||
|
|
@ -273,22 +253,22 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
|
|||
env.qhead <- Vec.get env.trail_lim lvl;
|
||||
env.tatoms_qhead <- env.qhead;
|
||||
for c = env.qhead to Vec.size env.trail - 1 do
|
||||
Either.destruct (Vec.get env.trail c)
|
||||
destruct (Vec.get env.trail c)
|
||||
(fun v ->
|
||||
v.assigned <- None;
|
||||
v.level <- -1;
|
||||
insert_var_order (Either.mk_left v)
|
||||
insert_var_order (elt_of_lit v)
|
||||
)
|
||||
(fun a ->
|
||||
if a.var.level <= lvl then begin
|
||||
Vec.set env.trail env.qhead (Either.mk_right a);
|
||||
Vec.set env.trail env.qhead (of_atom a);
|
||||
env.qhead <- env.qhead + 1
|
||||
end else begin
|
||||
a.is_true <- false;
|
||||
a.neg.is_true <- false;
|
||||
a.var.level <- -1;
|
||||
a.var.reason <- Bcp None;
|
||||
insert_var_order (Either.mk_right a.var)
|
||||
insert_var_order (elt_of_var a.var)
|
||||
end)
|
||||
done;
|
||||
Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *)
|
||||
|
|
@ -313,14 +293,14 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
|
|||
a.is_true <- true;
|
||||
a.var.level <- lvl;
|
||||
a.var.reason <- reason;
|
||||
Vec.push env.trail (Either.mk_right a);
|
||||
Vec.push env.trail (of_atom a);
|
||||
L.debug 2 "Enqueue (%d): %a" (nb_assigns ()) pp_atom a
|
||||
end
|
||||
|
||||
let enqueue_assign v value lvl =
|
||||
v.assigned <- Some value;
|
||||
v.level <- lvl;
|
||||
Vec.push env.trail (Either.mk_left v);
|
||||
Vec.push env.trail (of_lit v);
|
||||
L.debug 2 "Enqueue (%d): %a" (nb_assigns ()) St.pp_lit v
|
||||
|
||||
let th_eval a =
|
||||
|
|
@ -371,7 +351,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
|
|||
| _ ->
|
||||
decr tr_ind;
|
||||
L.debug 20 "Looking at trail element %d" !tr_ind;
|
||||
Either.destruct (Vec.get env.trail !tr_ind)
|
||||
destruct (Vec.get env.trail !tr_ind)
|
||||
(fun v -> L.debug 15 "%a" St.pp_lit v)
|
||||
(fun a -> match a.var.reason with
|
||||
| Bcp (Some d) ->
|
||||
|
|
@ -396,7 +376,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
|
|||
blevel, learnt, !history, !is_uip
|
||||
|
||||
let get_atom i =
|
||||
Either.destruct (Vec.get env.trail i)
|
||||
destruct (Vec.get env.trail i)
|
||||
(fun _ -> assert false) (fun x -> x)
|
||||
|
||||
let analyze_sat c_clause =
|
||||
|
|
@ -647,19 +627,19 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
|
|||
ignore (th_eval a);
|
||||
a
|
||||
|
||||
let slice_get i = Either.destruct (Vec.get env.trail i)
|
||||
let slice_get i = destruct (Vec.get env.trail i)
|
||||
(function {level; term; assigned = Some v} -> Th.Assign (term, v), level | _ -> assert false)
|
||||
(fun a -> Th.Lit a.lit, a.var.level)
|
||||
|
||||
let slice_push l lemma =
|
||||
let atoms = List.rev_map (fun x -> new_atom x) l in
|
||||
Iheap.grow_to_by_double env.order (St.nb_vars ());
|
||||
List.iter (fun a -> insert_var_order (Either.mk_right a.var)) atoms;
|
||||
Iheap.grow_to_by_double env.order (St.nb_elt ());
|
||||
List.iter (fun a -> insert_var_order (elt_of_var a.var)) atoms;
|
||||
add_clause (fresh_tname ()) atoms (Lemma lemma)
|
||||
|
||||
let slice_propagate f lvl =
|
||||
let a = add_atom f in
|
||||
Iheap.grow_to_by_double env.order (St.nb_vars ());
|
||||
Iheap.grow_to_by_double env.order (St.nb_elt ());
|
||||
enqueue_bool a lvl (Semantic lvl)
|
||||
|
||||
let current_slice () = Th.({
|
||||
|
|
@ -686,8 +666,8 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
|
|||
propagate ()
|
||||
| Th.Unsat (l, p) ->
|
||||
let l = List.rev_map new_atom l in
|
||||
Iheap.grow_to_by_double env.order (St.nb_vars ());
|
||||
List.iter (fun a -> insert_var_order (Either.mk_right a.var)) l;
|
||||
Iheap.grow_to_by_double env.order (St.nb_elt ());
|
||||
List.iter (fun a -> insert_var_order (elt_of_var a.var)) l;
|
||||
let c = St.make_clause (St.fresh_tname ()) l (List.length l) true (Lemma p) in
|
||||
Some c
|
||||
|
||||
|
|
@ -698,7 +678,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
|
|||
let num_props = ref 0 in
|
||||
let res = ref None in
|
||||
while env.qhead < Vec.size env.trail do
|
||||
Either.destruct (Vec.get env.trail env.qhead)
|
||||
destruct (Vec.get env.trail env.qhead)
|
||||
(fun a -> ())
|
||||
(fun a ->
|
||||
incr num_props;
|
||||
|
|
@ -787,7 +767,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
|
|||
(* Decide on a new litteral *)
|
||||
let rec pick_branch_lit () =
|
||||
let max = Iheap.remove_min f_weight env.order in
|
||||
Either.destruct (St.get_var max)
|
||||
destruct_elt (St.get_elt max)
|
||||
(fun v ->
|
||||
if v.level >= 0 then
|
||||
pick_branch_lit ()
|
||||
|
|
@ -824,7 +804,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
|
|||
add_boolean_conflict confl
|
||||
|
||||
| None -> (* No Conflict *)
|
||||
if nb_assigns() = St.nb_vars () (* env.nb_init_vars *) then raise Sat;
|
||||
if nb_assigns() = St.nb_elt () (* env.nb_init_vars *) then raise Sat;
|
||||
if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then begin
|
||||
L.debug 1 "Restarting...";
|
||||
env.progress_estimate <- progress_estimate();
|
||||
|
|
@ -884,15 +864,15 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
|
|||
| Sat -> ()
|
||||
|
||||
let init_solver ?tag cnf =
|
||||
let nbv = St.nb_vars () in
|
||||
let nbv = St.nb_elt () in
|
||||
let nbc = env.nb_init_clauses + List.length cnf in
|
||||
Iheap.grow_to_by_double env.order nbv;
|
||||
(* List.iter (List.iter (fun a -> insert_var_order a.var)) cnf; *)
|
||||
St.iter_vars insert_var_order;
|
||||
St.iter_elt insert_var_order;
|
||||
Vec.grow_to_by_double env.clauses nbc;
|
||||
Vec.grow_to_by_double env.learnts nbc;
|
||||
env.nb_init_clauses <- nbc;
|
||||
St.iter_vars (fun e -> Either.destruct e
|
||||
St.iter_elt (fun e -> destruct_elt e
|
||||
(fun v -> L.debug 50 " -- %a" St.pp_lit v)
|
||||
(fun a -> L.debug 50 " -- %a" St.pp_atom a.pa)
|
||||
);
|
||||
|
|
@ -916,7 +896,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
|
|||
|
||||
let model () =
|
||||
let opt = function Some a -> a | None -> assert false in
|
||||
Vec.fold (fun acc e -> Either.destruct e
|
||||
Vec.fold (fun acc e -> destruct e
|
||||
(fun v -> (v.term, opt v.assigned) :: acc)
|
||||
(fun _ -> acc)
|
||||
) [] env.trail
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ Copyright 2014 Simon Cruanes
|
|||
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
|
||||
|
||||
module St = Solver_types.Make(L)(E)(Th)
|
||||
module St = Solver_types.McMake(L)(E)(Th)
|
||||
|
||||
module M = Internal.Make(L)(St)(Th)
|
||||
|
||||
|
|
|
|||
798
solver/solver.ml
798
solver/solver.ml
|
|
@ -50,21 +50,22 @@ module Make (L : Log_intf.S)(E : Formula_intf.S)
|
|||
|
||||
let current_level = Th.current_level
|
||||
|
||||
let assume s = match Th.assume {
|
||||
Th.start = s.start;
|
||||
Th.length = s.length;
|
||||
Th.get = (function i -> match s.get i with
|
||||
| Lit f, _ -> f | _ -> assert false);
|
||||
Th.push = s.push;
|
||||
} with
|
||||
| Th.Sat _ -> Sat
|
||||
| Th.Unsat (l, p) -> Unsat (l, p)
|
||||
let assume_get s i = match s.get i with
|
||||
| Lit f, _ -> f | _ -> assert false
|
||||
|
||||
let assume s =
|
||||
match Th.assume {
|
||||
Th.start = s.start;
|
||||
Th.length = s.length;
|
||||
Th.get = assume_get s;
|
||||
Th.push = s.push;
|
||||
} with
|
||||
| Th.Sat _ -> Sat
|
||||
| Th.Unsat (l, p) -> Unsat (l, p)
|
||||
|
||||
let backtrack = Th.backtrack
|
||||
|
||||
let assign t =
|
||||
Format.printf "Error : %a@." Expr.Term.print t;
|
||||
assert false
|
||||
let assign _ = assert false
|
||||
|
||||
let iter_assignable _ _ = ()
|
||||
|
||||
|
|
@ -75,11 +76,7 @@ module Make (L : Log_intf.S)(E : Formula_intf.S)
|
|||
let proof_debug _ = assert false
|
||||
end
|
||||
|
||||
module St = struct
|
||||
module M = Solver_types.Make(L)(Expr)(Plugin)
|
||||
include M
|
||||
let mcsat = false
|
||||
end
|
||||
module St = Solver_types.SatMake(L)(E)(Th)
|
||||
|
||||
module S = Internal.Make(L)(St)(Plugin)
|
||||
|
||||
|
|
@ -87,770 +84,3 @@ module Make (L : Log_intf.S)(E : Formula_intf.S)
|
|||
|
||||
end
|
||||
|
||||
(*
|
||||
module Make (L : Log_intf.S)(F : Formula_intf.S)
|
||||
(Th : Theory_intf.S with type formula = F.t) = struct
|
||||
|
||||
module St = Solver_types.Make(F)(Th)
|
||||
module Proof = Res.Make(L)(St)
|
||||
|
||||
open St
|
||||
|
||||
exception Sat
|
||||
exception Unsat
|
||||
exception Restart
|
||||
exception Conflict of clause
|
||||
|
||||
(* a push/pop state *)
|
||||
type user_level = {
|
||||
ul_trail : int; (* height of the decision trail *)
|
||||
ul_clauses : int; (* number of clauses *)
|
||||
ul_learnt : int; (* number of learnt clauses *)
|
||||
}
|
||||
|
||||
(* Singleton type containing the current state *)
|
||||
type env = {
|
||||
|
||||
mutable is_unsat : bool;
|
||||
(* if [true], constraints are already false *)
|
||||
|
||||
mutable unsat_conflict : clause option;
|
||||
(* conflict clause at decision level 0, if any *)
|
||||
|
||||
clauses : clause Vec.t;
|
||||
(* all currently active clauses *)
|
||||
|
||||
learnts : clause Vec.t;
|
||||
(* learnt clauses *)
|
||||
|
||||
mutable clause_inc : float;
|
||||
(* increment for clauses' activity *)
|
||||
|
||||
mutable var_inc : float;
|
||||
(* increment for variables' activity *)
|
||||
|
||||
trail : atom Vec.t;
|
||||
(* decision stack + propagated atoms *)
|
||||
|
||||
trail_lim : int Vec.t;
|
||||
(* decision levels in [trail] *)
|
||||
|
||||
user_levels : user_level Vec.t;
|
||||
(* user-defined levels, for {!push} and {!pop} *)
|
||||
|
||||
mutable qhead : int;
|
||||
(* Start offset in the queue of unit facts to propagate, within the trail *)
|
||||
|
||||
mutable simpDB_assigns : int;
|
||||
(* number of toplevel assignments since last call to [simplify ()] *)
|
||||
|
||||
mutable simpDB_props : int;
|
||||
(* remaining number of propagations before the next call to [simplify ()] *)
|
||||
|
||||
order : Iheap.t;
|
||||
(* Heap ordered by variable activity *)
|
||||
|
||||
mutable progress_estimate : float;
|
||||
(* progression estimate, updated by [search ()] *)
|
||||
|
||||
remove_satisfied : bool;
|
||||
|
||||
var_decay : float;
|
||||
(* inverse of the activity factor for variables. Default 1/0.999 *)
|
||||
|
||||
clause_decay : float;
|
||||
(* inverse of the activity factor for clauses. Default 1/0.95 *)
|
||||
|
||||
mutable restart_first : int;
|
||||
(* intial restart limit, default 100 *)
|
||||
|
||||
restart_inc : float;
|
||||
(* multiplicative factor for restart limit, default 1.5 *)
|
||||
|
||||
mutable learntsize_factor : float;
|
||||
(* initial limit for the number of learnt clauses, 1/3 of initial
|
||||
number of clauses by default *)
|
||||
|
||||
learntsize_inc : float;
|
||||
(* multiplicative factor for [learntsize_factor] at each restart, default 1.1 *)
|
||||
|
||||
expensive_ccmin : bool;
|
||||
(* control minimization of conflict clause, default true *)
|
||||
|
||||
polarity_mode : bool;
|
||||
(* default polarity for decision *)
|
||||
|
||||
mutable starts : int;
|
||||
mutable decisions : int;
|
||||
mutable propagations : int;
|
||||
mutable conflicts : int;
|
||||
mutable clauses_literals : int;
|
||||
mutable learnts_literals : int;
|
||||
mutable max_literals : int;
|
||||
mutable tot_literals : int;
|
||||
mutable nb_init_clauses : int;
|
||||
mutable model : var Vec.t;
|
||||
mutable tenv_queue : Th.level Vec.t;
|
||||
mutable tatoms_qhead : int;
|
||||
}
|
||||
|
||||
let env = {
|
||||
is_unsat = false;
|
||||
unsat_conflict = None;
|
||||
clauses = Vec.make 0 dummy_clause; (*updated during parsing*)
|
||||
learnts = Vec.make 0 dummy_clause; (*updated during parsing*)
|
||||
clause_inc = 1.;
|
||||
var_inc = 1.;
|
||||
trail = Vec.make 601 dummy_atom;
|
||||
trail_lim = Vec.make 601 (-1);
|
||||
user_levels = Vec.make 20 {ul_trail=0;ul_learnt=0;ul_clauses=0};
|
||||
qhead = 0;
|
||||
simpDB_assigns = -1;
|
||||
simpDB_props = 0;
|
||||
order = Iheap.init 0; (* updated in solve *)
|
||||
progress_estimate = 0.;
|
||||
remove_satisfied = true;
|
||||
var_decay = 1. /. 0.95;
|
||||
clause_decay = 1. /. 0.999;
|
||||
restart_first = 100;
|
||||
restart_inc = 1.5;
|
||||
learntsize_factor = 1. /. 3. ;
|
||||
learntsize_inc = 1.1;
|
||||
expensive_ccmin = true;
|
||||
polarity_mode = false;
|
||||
starts = 0;
|
||||
decisions = 0;
|
||||
propagations = 0;
|
||||
conflicts = 0;
|
||||
clauses_literals = 0;
|
||||
learnts_literals = 0;
|
||||
max_literals = 0;
|
||||
tot_literals = 0;
|
||||
nb_init_clauses = 0;
|
||||
model = Vec.make 0 dummy_var;
|
||||
tenv_queue = Vec.make 100 Th.dummy;
|
||||
tatoms_qhead = 0;
|
||||
}
|
||||
|
||||
(* Misc functions *)
|
||||
let to_float i = float_of_int i
|
||||
let to_int f = int_of_float f
|
||||
|
||||
let f_weight i j =
|
||||
(St.get_var j).weight < (St.get_var i).weight
|
||||
|
||||
let f_filter i =
|
||||
(St.get_var i).level < 0
|
||||
|
||||
|
||||
(* Var/clause activity *)
|
||||
let insert_var_order v =
|
||||
Iheap.insert f_weight env.order v.vid
|
||||
|
||||
let var_decay_activity () =
|
||||
env.var_inc <- env.var_inc *. env.var_decay
|
||||
|
||||
let clause_decay_activity () =
|
||||
env.clause_inc <- env.clause_inc *. env.clause_decay
|
||||
|
||||
let var_bump_activity v =
|
||||
v.weight <- v.weight +. env.var_inc;
|
||||
if v.weight > 1e100 then begin
|
||||
for i = 0 to (St.nb_vars ()) - 1 do
|
||||
(St.get_var i).weight <- (St.get_var i).weight *. 1e-100
|
||||
done;
|
||||
env.var_inc <- env.var_inc *. 1e-100;
|
||||
end;
|
||||
if Iheap.in_heap env.order v.vid then
|
||||
Iheap.decrease f_weight env.order v.vid
|
||||
|
||||
let clause_bump_activity c =
|
||||
c.activity <- c.activity +. env.clause_inc;
|
||||
if c.activity > 1e20 then begin
|
||||
for i = 0 to (Vec.size env.learnts) - 1 do
|
||||
(Vec.get env.learnts i).activity <-
|
||||
(Vec.get env.learnts i).activity *. 1e-20;
|
||||
done;
|
||||
env.clause_inc <- env.clause_inc *. 1e-20
|
||||
end
|
||||
|
||||
(* Convenient access *)
|
||||
let decision_level () = Vec.size env.trail_lim
|
||||
|
||||
let nb_assigns () = Vec.size env.trail
|
||||
let nb_clauses () = Vec.size env.clauses
|
||||
let nb_learnts () = Vec.size env.learnts
|
||||
let nb_vars () = St.nb_vars ()
|
||||
|
||||
let new_decision_level() =
|
||||
Vec.push env.trail_lim (Vec.size env.trail);
|
||||
Vec.push env.tenv_queue (Th.current_level ()); (* save the current tenv *)
|
||||
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);
|
||||
()
|
||||
|
||||
let attach_clause c =
|
||||
Vec.push (Vec.get c.atoms 0).neg.watched c;
|
||||
Vec.push (Vec.get c.atoms 1).neg.watched c;
|
||||
L.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 1).neg St.pp_clause c;
|
||||
if c.learnt then
|
||||
env.learnts_literals <- env.learnts_literals + Vec.size c.atoms
|
||||
else
|
||||
env.clauses_literals <- env.clauses_literals + Vec.size c.atoms
|
||||
|
||||
let detach_clause c =
|
||||
c.removed <- true;
|
||||
(*
|
||||
Vec.remove (Vec.get c.atoms 0).neg.watched c;
|
||||
Vec.remove (Vec.get c.atoms 1).neg.watched c;
|
||||
*)
|
||||
if c.learnt then
|
||||
env.learnts_literals <- env.learnts_literals - Vec.size c.atoms
|
||||
else
|
||||
env.clauses_literals <- env.clauses_literals - Vec.size c.atoms
|
||||
|
||||
let remove_clause c = detach_clause c
|
||||
|
||||
let satisfied c =
|
||||
Vec.exists (fun atom -> atom.is_true) c.atoms
|
||||
|
||||
(* cancel down to [lvl] excluded *)
|
||||
let cancel_until lvl =
|
||||
L.debug 5 "Bactracking to decision level %d (excluded)" lvl;
|
||||
if decision_level () > lvl then begin
|
||||
env.qhead <- Vec.get env.trail_lim lvl;
|
||||
env.tatoms_qhead <- env.qhead;
|
||||
for c = Vec.size env.trail - 1 downto env.qhead do
|
||||
let a = Vec.get env.trail c in
|
||||
a.is_true <- false;
|
||||
a.neg.is_true <- false;
|
||||
a.var.level <- -1;
|
||||
a.var.reason <- None;
|
||||
a.var.vpremise <- History [];
|
||||
insert_var_order a.var
|
||||
done;
|
||||
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_lim ((Vec.size env.trail_lim) - lvl);
|
||||
Vec.shrink env.tenv_queue ((Vec.size env.tenv_queue) - lvl)
|
||||
end;
|
||||
assert (Vec.size env.trail_lim = Vec.size env.tenv_queue)
|
||||
|
||||
let report_unsat ({atoms=atoms} as confl) =
|
||||
L.debug 5 "Unsat conflict : %a" St.pp_clause confl;
|
||||
env.unsat_conflict <- Some confl;
|
||||
env.is_unsat <- true;
|
||||
raise Unsat
|
||||
|
||||
let enqueue a lvl reason =
|
||||
assert (not a.is_true && not a.neg.is_true &&
|
||||
a.var.level < 0 && a.var.reason = None && lvl >= 0);
|
||||
assert (lvl = decision_level ());
|
||||
(* keep the reason for proof/unsat-core *)
|
||||
(*let reason = if lvl = 0 then None else reason in*)
|
||||
a.is_true <- true;
|
||||
a.var.level <- lvl;
|
||||
a.var.reason <- reason;
|
||||
L.debug 8 "Enqueue: %a" pp_atom a;
|
||||
Vec.push env.trail a
|
||||
|
||||
(* conflict analysis *)
|
||||
let analyze c_clause =
|
||||
let pathC = ref 0 in
|
||||
let learnt = ref [] in
|
||||
let cond = ref true in
|
||||
let blevel = ref 0 in
|
||||
let seen = ref [] in
|
||||
let c = ref c_clause in
|
||||
let tr_ind = ref (Vec.size env.trail - 1) in
|
||||
let size = ref 1 in
|
||||
let history = ref [] in
|
||||
while !cond do
|
||||
if !c.learnt then clause_bump_activity !c;
|
||||
history := !c :: !history;
|
||||
(* visit the current predecessors *)
|
||||
for j = 0 to Vec.size !c.atoms - 1 do
|
||||
let q = Vec.get !c.atoms j in
|
||||
(*printf "I visit %a@." D1.atom q;*)
|
||||
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
|
||||
var_bump_activity q.var;
|
||||
q.var.seen <- true;
|
||||
seen := q :: !seen;
|
||||
if q.var.level >= decision_level () then begin
|
||||
incr pathC
|
||||
end else begin
|
||||
learnt := q :: !learnt;
|
||||
incr size;
|
||||
blevel := max !blevel q.var.level
|
||||
end
|
||||
end
|
||||
done;
|
||||
|
||||
(* look for the next node to expand *)
|
||||
while not (Vec.get env.trail !tr_ind).var.seen do decr tr_ind done;
|
||||
decr pathC;
|
||||
let p = Vec.get env.trail !tr_ind in
|
||||
decr tr_ind;
|
||||
match !pathC, p.var.reason with
|
||||
| 0, _ ->
|
||||
cond := false;
|
||||
learnt := p.neg :: (List.rev !learnt)
|
||||
| n, None -> assert false
|
||||
| n, Some cl -> c := cl
|
||||
done;
|
||||
List.iter (fun q -> q.var.seen <- false) !seen;
|
||||
!blevel, !learnt, !history, !size
|
||||
|
||||
let record_learnt_clause blevel learnt history size =
|
||||
begin match learnt with
|
||||
| [] -> assert false
|
||||
| [fuip] ->
|
||||
assert (blevel = 0);
|
||||
fuip.var.vpremise <- history;
|
||||
let name = fresh_lname () in
|
||||
let uclause = make_clause name learnt size true history in
|
||||
L.debug 2 "Unit clause learnt : %a" St.pp_clause uclause;
|
||||
Vec.push env.learnts uclause;
|
||||
enqueue fuip 0 (Some uclause)
|
||||
| fuip :: _ ->
|
||||
let name = fresh_lname () in
|
||||
let lclause = make_clause name learnt size true history in
|
||||
L.debug 2 "New clause learnt : %a" St.pp_clause lclause;
|
||||
Vec.push env.learnts lclause;
|
||||
attach_clause lclause;
|
||||
clause_bump_activity lclause;
|
||||
enqueue fuip blevel (Some lclause)
|
||||
end;
|
||||
var_decay_activity ();
|
||||
clause_decay_activity ()
|
||||
|
||||
let add_boolean_conflict confl =
|
||||
env.conflicts <- env.conflicts + 1;
|
||||
if decision_level() = 0 then report_unsat confl; (* Top-level conflict *)
|
||||
let blevel, learnt, history, size = analyze confl in
|
||||
cancel_until blevel;
|
||||
record_learnt_clause blevel learnt (History history) size
|
||||
|
||||
(* Add a new clause *)
|
||||
exception Trivial
|
||||
|
||||
let simplify_zero atoms init0 =
|
||||
(* TODO: could be more efficient than [@] everywhere? *)
|
||||
assert (decision_level () = 0);
|
||||
let aux (atoms, init) a =
|
||||
if a.is_true then raise Trivial;
|
||||
if a.neg.is_true then
|
||||
match a.var.vpremise with
|
||||
| History _ -> atoms, false
|
||||
| Lemma _ -> assert false
|
||||
else
|
||||
a::atoms, init
|
||||
in
|
||||
let atoms, init = List.fold_left aux ([], true) atoms in
|
||||
List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init
|
||||
|
||||
let partition atoms init0 =
|
||||
let rec partition_aux trues unassigned falses init = function
|
||||
| [] -> trues @ unassigned @ falses, init
|
||||
| a::r ->
|
||||
if a.is_true then
|
||||
if a.var.level = 0 then raise Trivial
|
||||
else (a::trues) @ unassigned @ falses @ r, init
|
||||
else if a.neg.is_true then
|
||||
if a.var.level = 0 then match a.var.vpremise with
|
||||
| History v ->
|
||||
partition_aux trues unassigned falses false r
|
||||
| Lemma _ -> assert false
|
||||
else
|
||||
partition_aux trues unassigned (a::falses) init r
|
||||
else partition_aux trues (a::unassigned) falses init r
|
||||
in
|
||||
if decision_level () = 0 then
|
||||
simplify_zero atoms init0
|
||||
else
|
||||
partition_aux [] [] [] true atoms
|
||||
|
||||
let add_clause ?tag name atoms history =
|
||||
if env.is_unsat then raise Unsat;
|
||||
let init_name = name in
|
||||
let init0 = make_clause ?tag init_name atoms (List.length atoms) (history <> History []) history in
|
||||
L.debug 10 "Adding clause : %a" St.pp_clause init0;
|
||||
try
|
||||
if Proof.has_been_proved init0 then raise Trivial;
|
||||
assert (Proof.is_proven init0);
|
||||
let atoms, init = partition atoms init0 in
|
||||
let size = List.length atoms in
|
||||
match atoms with
|
||||
| [] ->
|
||||
report_unsat init0;
|
||||
| a::b::_ ->
|
||||
let name = fresh_name () in
|
||||
let clause =
|
||||
if init then init0
|
||||
else make_clause ?tag (init_name ^ "_" ^ name) atoms size true (History [init0])
|
||||
in
|
||||
L.debug 10 "New clause : %a" St.pp_clause init0;
|
||||
attach_clause clause;
|
||||
Vec.push env.clauses clause;
|
||||
if a.neg.is_true then begin
|
||||
let lvl = List.fold_left (fun m a -> max m a.var.level) 0 atoms in
|
||||
cancel_until lvl;
|
||||
add_boolean_conflict clause
|
||||
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
|
||||
cancel_until lvl;
|
||||
enqueue a lvl (Some clause)
|
||||
end
|
||||
| [a] ->
|
||||
cancel_until 0;
|
||||
a.var.vpremise <- History [init0];
|
||||
enqueue a 0 (Some init0)
|
||||
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 prg = ref 0. in
|
||||
let nbv = to_float (nb_vars()) in
|
||||
let lvl = decision_level () in
|
||||
let _F = 1. /. nbv in
|
||||
for i = 0 to lvl do
|
||||
let _beg = if i = 0 then 0 else Vec.get env.trail_lim (i-1) in
|
||||
let _end = if i=lvl then Vec.size env.trail else Vec.get env.trail_lim i in
|
||||
prg := !prg +. _F**(to_float i) *. (to_float (_end - _beg))
|
||||
done;
|
||||
!prg /. nbv
|
||||
|
||||
let propagate_in_clause a c i watched new_sz =
|
||||
let atoms = c.atoms in
|
||||
let first = Vec.get atoms 0 in
|
||||
if first == a.neg then begin (* false lit must be at index 1 *)
|
||||
Vec.set atoms 0 (Vec.get atoms 1);
|
||||
Vec.set atoms 1 first
|
||||
end;
|
||||
let first = Vec.get atoms 0 in
|
||||
if first.is_true then begin
|
||||
(* true clause, keep it in watched *)
|
||||
Vec.set watched !new_sz c;
|
||||
incr new_sz;
|
||||
end
|
||||
else
|
||||
try (* look for another watch lit *)
|
||||
for k = 2 to Vec.size atoms - 1 do
|
||||
let ak = Vec.get atoms k in
|
||||
if not (ak.neg.is_true) then begin
|
||||
(* watch lit found: update and exit *)
|
||||
Vec.set atoms 1 ak;
|
||||
Vec.set atoms k a.neg;
|
||||
Vec.push ak.neg.watched c;
|
||||
L.debug 8 "New watcher (%a) for clause : %a" St.pp_atom ak.neg St.pp_clause c;
|
||||
raise Exit
|
||||
end
|
||||
done;
|
||||
(* no watch lit found *)
|
||||
if first.neg.is_true then begin
|
||||
(* clause is false *)
|
||||
env.qhead <- Vec.size env.trail;
|
||||
for k = i to Vec.size watched - 1 do
|
||||
Vec.set watched !new_sz (Vec.get watched k);
|
||||
incr new_sz;
|
||||
done;
|
||||
L.debug 3 "Conflict found : %a" St.pp_clause c;
|
||||
raise (Conflict c)
|
||||
end
|
||||
else begin
|
||||
(* clause is unit *)
|
||||
Vec.set watched !new_sz c;
|
||||
incr new_sz;
|
||||
L.debug 5 "Unit clause : %a" St.pp_clause c;
|
||||
enqueue first (decision_level ()) (Some c)
|
||||
end
|
||||
with Exit -> ()
|
||||
|
||||
let propagate_atom a res =
|
||||
L.debug 8 "Propagating %a" St.pp_atom a;
|
||||
let watched = a.watched in
|
||||
L.debug 10 "Watching %a :" St.pp_atom a;
|
||||
Vec.iter (fun c -> L.debug 10 " %a" St.pp_clause c) watched;
|
||||
let new_sz_w = ref 0 in
|
||||
begin
|
||||
try
|
||||
for i = 0 to Vec.size watched - 1 do
|
||||
let c = Vec.get watched i in
|
||||
if not c.removed then propagate_in_clause a c i watched new_sz_w
|
||||
done;
|
||||
with Conflict c ->
|
||||
assert (!res = None);
|
||||
res := Some c
|
||||
end;
|
||||
let dead_part = Vec.size watched - !new_sz_w in
|
||||
Vec.shrink watched dead_part
|
||||
|
||||
(* Propagation (boolean and theory *)
|
||||
let _th_cnumber = ref 0
|
||||
let slice_get i = (Vec.get env.trail i).lit
|
||||
let slice_push l lemma =
|
||||
decr _th_cnumber;
|
||||
let atoms = List.rev_map (fun x -> add_atom x) l in
|
||||
Iheap.grow_to_by_double env.order (St.nb_vars ());
|
||||
List.iter (fun a -> insert_var_order a.var) atoms;
|
||||
add_clause "lemma" atoms (Lemma lemma)
|
||||
|
||||
let current_slice () = Th.({
|
||||
start = env.tatoms_qhead;
|
||||
length = (Vec.size env.trail) - env.tatoms_qhead;
|
||||
get = slice_get;
|
||||
push = slice_push;
|
||||
})
|
||||
|
||||
let rec theory_propagate () =
|
||||
let head = Vec.size env.trail in
|
||||
match Th.assume (current_slice ()) with
|
||||
| Th.Sat _ ->
|
||||
env.tatoms_qhead <- head;
|
||||
propagate ()
|
||||
| Th.Unsat (l, p) ->
|
||||
let l = List.rev_map St.add_atom l in
|
||||
let c = St.make_clause (St.fresh_name ()) l (List.length l) true (Lemma p) in
|
||||
Some c
|
||||
|
||||
and propagate () =
|
||||
if env.qhead = Vec.size env.trail then
|
||||
None
|
||||
else begin
|
||||
let num_props = ref 0 in
|
||||
let res = ref None in
|
||||
while env.qhead < Vec.size env.trail do
|
||||
let a = Vec.get env.trail env.qhead in
|
||||
env.qhead <- env.qhead + 1;
|
||||
incr num_props;
|
||||
propagate_atom a res;
|
||||
done;
|
||||
env.propagations <- env.propagations + !num_props;
|
||||
env.simpDB_props <- env.simpDB_props - !num_props;
|
||||
match !res with
|
||||
| None -> theory_propagate ()
|
||||
| _ -> !res
|
||||
end
|
||||
|
||||
(* heuristic comparison between clauses, by their size (unary/binary or not)
|
||||
and activity *)
|
||||
let f_sort_db c1 c2 =
|
||||
let sz1 = Vec.size c1.atoms in
|
||||
let sz2 = Vec.size c2.atoms in
|
||||
let c = compare c1.activity c2.activity in
|
||||
if sz1 = sz2 && c = 0 then 0
|
||||
else
|
||||
if sz1 > 2 && (sz2 = 2 || c < 0) then -1
|
||||
else 1
|
||||
|
||||
(* returns true if the clause is used as a reason for a propagation,
|
||||
and therefore can be needed in case of conflict. In this case
|
||||
the clause can't be forgotten *)
|
||||
let locked c = false (*
|
||||
Vec.exists
|
||||
(fun v -> match v.reason with
|
||||
| Some c' -> c ==c'
|
||||
| _ -> false
|
||||
) env.vars
|
||||
*)
|
||||
|
||||
(* remove some learnt clauses *)
|
||||
let reduce_db () = () (*
|
||||
let extra_lim = env.clause_inc /. (to_float (Vec.size env.learnts)) in
|
||||
Vec.sort env.learnts f_sort_db;
|
||||
let lim2 = Vec.size env.learnts in
|
||||
let lim1 = lim2 / 2 in
|
||||
let j = ref 0 in
|
||||
for i = 0 to lim1 - 1 do
|
||||
let c = Vec.get env.learnts i in
|
||||
if Vec.size c.atoms > 2 && not (locked c) then
|
||||
remove_clause c
|
||||
else
|
||||
begin Vec.set env.learnts !j c; incr j end
|
||||
done;
|
||||
for i = lim1 to lim2 - 1 do
|
||||
let c = Vec.get env.learnts i in
|
||||
if Vec.size c.atoms > 2 && not (locked c) && c.activity < extra_lim then
|
||||
remove_clause c
|
||||
else
|
||||
begin Vec.set env.learnts !j c; incr j end
|
||||
done;
|
||||
Vec.shrink env.learnts (lim2 - !j)
|
||||
*)
|
||||
|
||||
(* remove from [vec] the clauses that are satisfied in the current trail *)
|
||||
let remove_satisfied vec =
|
||||
for i = 0 to Vec.size vec - 1 do
|
||||
let c = Vec.get vec i in
|
||||
if satisfied c then remove_clause c
|
||||
done
|
||||
|
||||
module HUC = Hashtbl.Make
|
||||
(struct type t = clause let equal = (==) let hash = Hashtbl.hash end)
|
||||
|
||||
let simplify () =
|
||||
assert (decision_level () = 0);
|
||||
if env.is_unsat then raise Unsat;
|
||||
begin
|
||||
match propagate () with
|
||||
| Some confl -> report_unsat confl
|
||||
| None -> ()
|
||||
end;
|
||||
if nb_assigns() <> env.simpDB_assigns && env.simpDB_props <= 0 then begin
|
||||
if Vec.size env.learnts > 0 then remove_satisfied env.learnts;
|
||||
if env.remove_satisfied then remove_satisfied env.clauses;
|
||||
(*Iheap.filter env.order f_filter f_weight;*)
|
||||
env.simpDB_assigns <- nb_assigns ();
|
||||
env.simpDB_props <- env.clauses_literals + env.learnts_literals;
|
||||
end
|
||||
|
||||
let search n_of_conflicts n_of_learnts =
|
||||
let conflictC = ref 0 in
|
||||
env.starts <- env.starts + 1;
|
||||
while (true) do
|
||||
match propagate () with
|
||||
| Some confl -> (* Conflict *)
|
||||
incr conflictC;
|
||||
add_boolean_conflict confl
|
||||
|
||||
| None -> (* No Conflict *)
|
||||
if nb_assigns() = St.nb_vars () (* env.nb_init_vars *) then raise Sat;
|
||||
if n_of_conflicts >= 0 && !conflictC >= n_of_conflicts then
|
||||
begin
|
||||
env.progress_estimate <- progress_estimate();
|
||||
cancel_until 0;
|
||||
raise Restart
|
||||
end;
|
||||
if decision_level() = 0 then simplify ();
|
||||
|
||||
if n_of_learnts >= 0 &&
|
||||
Vec.size env.learnts - nb_assigns() >= n_of_learnts then
|
||||
reduce_db();
|
||||
|
||||
env.decisions <- env.decisions + 1;
|
||||
|
||||
new_decision_level();
|
||||
let next = pick_branch_lit () in
|
||||
let current_level = decision_level () in
|
||||
assert (next.level < 0);
|
||||
L.debug 5 "Deciding on %a" St.pp_atom next.pa;
|
||||
enqueue next.pa current_level None
|
||||
done
|
||||
|
||||
let check_clause c =
|
||||
let b = ref false in
|
||||
let atoms = c.atoms in
|
||||
for i = 0 to Vec.size atoms - 1 do
|
||||
let a = Vec.get atoms i in
|
||||
b := !b || a.is_true
|
||||
done;
|
||||
assert (!b)
|
||||
|
||||
let check_vec vec =
|
||||
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
|
||||
conflict is reached *)
|
||||
let solve () =
|
||||
if env.is_unsat then raise Unsat;
|
||||
let n_of_conflicts = ref (to_float env.restart_first) in
|
||||
let n_of_learnts = ref ((to_float (nb_clauses())) *. env.learntsize_factor) in
|
||||
try
|
||||
while true do
|
||||
begin try
|
||||
search (to_int !n_of_conflicts) (to_int !n_of_learnts);
|
||||
with Restart -> ()
|
||||
end;
|
||||
n_of_conflicts := !n_of_conflicts *. env.restart_inc;
|
||||
n_of_learnts := !n_of_learnts *. env.learntsize_inc;
|
||||
done;
|
||||
with
|
||||
| Sat -> ()
|
||||
|
||||
let add_clauses ?tag cnf =
|
||||
let aux cl =
|
||||
add_clause ?tag "hyp" cl (History []);
|
||||
match propagate () with
|
||||
| None -> () | Some confl -> report_unsat confl
|
||||
in
|
||||
List.iter aux cnf
|
||||
|
||||
let init_solver ?tag cnf =
|
||||
let nbv = St.nb_vars () in
|
||||
let nbc = env.nb_init_clauses + List.length cnf in
|
||||
Iheap.grow_to_by_double env.order nbv;
|
||||
(* List.iter (List.iter (fun a -> insert_var_order a.var)) cnf; *)
|
||||
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.learnts nbc;
|
||||
env.nb_init_clauses <- nbc;
|
||||
add_clauses ?tag cnf
|
||||
|
||||
let assume ?tag cnf =
|
||||
let cnf = List.rev_map (List.rev_map St.add_atom) cnf in
|
||||
init_solver ?tag cnf
|
||||
|
||||
let eval lit =
|
||||
let var, negated = make_var lit in
|
||||
assert (var.pa.is_true || var.na.is_true);
|
||||
let truth = var.pa.is_true in
|
||||
if negated then not truth else truth
|
||||
|
||||
let hyps () = env.clauses
|
||||
|
||||
let history () = env.learnts
|
||||
|
||||
let unsat_conflict () = env.unsat_conflict
|
||||
|
||||
type level = int
|
||||
|
||||
let base_level = 0
|
||||
|
||||
let current_level () = Vec.size env.user_levels
|
||||
|
||||
let push () =
|
||||
let ul_trail = if Vec.is_empty env.trail_lim
|
||||
then base_level
|
||||
else Vec.last env.trail_lim
|
||||
and ul_clauses = Vec.size env.clauses
|
||||
and ul_learnt = Vec.size env.learnts in
|
||||
Vec.push env.user_levels {ul_trail; ul_clauses;ul_learnt};
|
||||
Vec.size env.user_levels
|
||||
|
||||
let pop l =
|
||||
if l > current_level()
|
||||
then invalid_arg "cannot pop() to level, it is too high";
|
||||
let ul = Vec.get env.user_levels l in
|
||||
(* see whether we can reset [env.is_unsat] *)
|
||||
if env.is_unsat && not (Vec.is_empty env.trail_lim) then (
|
||||
(* level at which the decision that lead to unsat was made *)
|
||||
let last = Vec.last env.trail_lim in
|
||||
if ul.ul_trail < last then env.is_unsat <- false
|
||||
);
|
||||
cancel_until ul.ul_trail;
|
||||
Vec.shrink env.clauses ul.ul_clauses;
|
||||
Vec.shrink env.learnts ul.ul_learnt;
|
||||
()
|
||||
|
||||
let clear () = pop base_level
|
||||
end
|
||||
*)
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@ open Printf
|
|||
|
||||
module type S = Solver_types_intf.S
|
||||
|
||||
module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
|
||||
module McMake (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
|
||||
type formula = E.Formula.t and type term = E.Term.t) = struct
|
||||
|
||||
(* Flag for Mcsat v.s Pure Sat *)
|
||||
|
|
@ -115,9 +115,9 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
|
|||
let t_map = MT.create 4096
|
||||
|
||||
let vars = Vec.make 107 (Either.mk_right dummy_var)
|
||||
let nb_vars () = Vec.size vars
|
||||
let get_var i = Vec.get vars i
|
||||
let iter_vars f = Vec.iter f vars
|
||||
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
|
||||
|
||||
|
|
@ -189,6 +189,31 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
|
|||
|
||||
let empty_clause = make_clause "Empty" [] 0 false (History [])
|
||||
|
||||
(* 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 destruct_elt = Either.destruct
|
||||
|
||||
let get_elt_id = function
|
||||
| Either.Left l -> l.lid | Either.Right v -> v.vid
|
||||
let get_elt_level = function
|
||||
| Either.Left (l :lit) -> l.level | Either.Right v -> v.level
|
||||
let get_elt_weight = function
|
||||
| Either.Left (l : lit) -> l.weight | Either.Right v -> v.weight
|
||||
|
||||
let set_elt_level e lvl = match e with
|
||||
| Either.Left (l : lit) -> l.level <- lvl | Either.Right v -> v.level <- lvl
|
||||
let set_elt_weight e w = match e with
|
||||
| Either.Left (l : lit) -> l.weight <- w | Either.Right v -> v.weight <- w
|
||||
|
||||
(* Name generation *)
|
||||
let fresh_lname =
|
||||
let cpt = ref 0 in
|
||||
|
|
@ -282,3 +307,259 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
|
|||
bprintf b "%s%s{ %a} cpremise={{%a}}" name (if learnt then "!" else ":") pp_atoms_vec arr pp_premise cp
|
||||
|
||||
end
|
||||
|
||||
module SatMake (L : Log_intf.S)(E : Formula_intf.S)
|
||||
(Th : Theory_intf.S with type formula = E.t ) = struct
|
||||
|
||||
(* Flag for Mcsat v.s Pure Sat *)
|
||||
let mcsat = false
|
||||
|
||||
(* Types declarations *)
|
||||
|
||||
type term = E.t
|
||||
type formula = E.t
|
||||
type proof = Th.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;
|
||||
mutable activity : float;
|
||||
mutable removed : bool;
|
||||
}
|
||||
|
||||
and reason =
|
||||
| Semantic of int
|
||||
| Bcp of clause option
|
||||
|
||||
and premise =
|
||||
| History of clause list
|
||||
| Lemma of proof
|
||||
|
||||
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;
|
||||
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 =
|
||||
let atoms = Vec.from_list ali sz_ali dummy_atom in
|
||||
{ name = name;
|
||||
tag = tag;
|
||||
atoms = atoms;
|
||||
removed = false;
|
||||
learnt = is_learnt;
|
||||
activity = 0.;
|
||||
cpremise = premise}
|
||||
|
||||
let empty_clause = make_clause "Empty" [] 0 false (History [])
|
||||
|
||||
(* 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 _ = assert false
|
||||
|
||||
(* 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 =
|
||||
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
|
||||
|
||||
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
|
||||
|
|
|
|||
|
|
@ -13,10 +13,17 @@
|
|||
|
||||
module type S = Solver_types_intf.S
|
||||
|
||||
module Make :
|
||||
module McMake :
|
||||
functor (L : Log_intf.S) ->
|
||||
functor (E : Expr_intf.S) ->
|
||||
functor (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) ->
|
||||
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 a solver. *)
|
||||
|
||||
module SatMake :
|
||||
functor (L : Log_intf.S) ->
|
||||
functor (E : Formula_intf.S) ->
|
||||
functor (Th : Theory_intf.S with type formula = E.t) ->
|
||||
S with type term = E.t and type formula = E.t and type proof = Th.proof
|
||||
(** Functor to instantiate the types of clauses for a solver. *)
|
||||
|
||||
|
|
|
|||
|
|
@ -16,6 +16,9 @@ module type S = sig
|
|||
|
||||
val mcsat : bool
|
||||
|
||||
|
||||
(** {2 Type definitions} *)
|
||||
|
||||
type term
|
||||
type formula
|
||||
type proof
|
||||
|
|
@ -65,23 +68,48 @@ module type S = sig
|
|||
| History of clause list
|
||||
| Lemma of proof
|
||||
|
||||
type elt = (lit, var) Either.t
|
||||
(** Recursive types for literals (atoms) and clauses *)
|
||||
(** {2 Decisions and propagations} *)
|
||||
type t
|
||||
(** Either a lit of an atom *)
|
||||
|
||||
val of_lit : lit -> t
|
||||
val of_atom : atom -> t
|
||||
val destruct : t -> (lit -> 'a) -> (atom -> 'a) -> 'a
|
||||
(** Constructors and destructors *)
|
||||
|
||||
(** {2 Elements} *)
|
||||
|
||||
type elt
|
||||
(** Either a lit of a var *)
|
||||
|
||||
val nb_elt : unit -> int
|
||||
val get_elt : int -> elt
|
||||
val iter_elt : (elt -> unit) -> unit
|
||||
(** Read access to the vector of variables created *)
|
||||
|
||||
val elt_of_lit : lit -> elt
|
||||
val elt_of_var : var -> elt
|
||||
val destruct_elt : elt -> (lit -> 'a) -> (var -> 'a) -> 'a
|
||||
(** Constructors & destructor for elements *)
|
||||
|
||||
val get_elt_id : elt -> int
|
||||
val get_elt_level : elt -> int
|
||||
val get_elt_weight : elt -> float
|
||||
val set_elt_level : elt -> int -> unit
|
||||
val set_elt_weight : elt -> float -> unit
|
||||
(** Accessors for elements *)
|
||||
|
||||
(** {2 Variables, Litterals & Clauses } *)
|
||||
|
||||
val dummy_var : var
|
||||
val dummy_atom : atom
|
||||
val dummy_clause : clause
|
||||
(** Dummy values for use in vector dummys *)
|
||||
|
||||
val nb_vars : unit -> int
|
||||
val get_var : int -> elt
|
||||
val iter_vars : (elt -> unit) -> unit
|
||||
(** Read access to the vector of variables created *)
|
||||
|
||||
val add_atom : formula -> atom
|
||||
(** Returns the atom associated with the given formula *)
|
||||
val add_term : term -> lit
|
||||
(** Returns the variable associated with the term *)
|
||||
val add_atom : formula -> atom
|
||||
(** Returns the atom associated with the given formula *)
|
||||
val make_boolean_var : formula -> var * bool
|
||||
(** Returns the variable linked with the given formula, and wether the atom associated with the formula
|
||||
is [var.pa] or [var.na] *)
|
||||
|
|
@ -95,6 +123,8 @@ module type S = sig
|
|||
val make_clause : ?tag:int -> string -> atom list -> int -> bool -> premise -> clause
|
||||
(** [make_clause name atoms size learnt premise] creates a clause with the given attributes. *)
|
||||
|
||||
(** {2 Proof management} *)
|
||||
|
||||
val fresh_name : unit -> string
|
||||
val fresh_lname : unit -> string
|
||||
val fresh_tname : unit -> string
|
||||
|
|
@ -104,6 +134,8 @@ module type S = sig
|
|||
val proof_debug : proof -> string * (atom list) * (lit list) * (string option)
|
||||
(** Debugging info for proofs (see Plugin_intf). *)
|
||||
|
||||
(** {2 Printing} *)
|
||||
|
||||
val print_lit : Format.formatter -> lit -> unit
|
||||
val print_atom : Format.formatter -> atom -> unit
|
||||
val print_clause : Format.formatter -> clause -> unit
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue