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

First test (probably unsound)

Browse source
This commit is contained in:
Guillaume Bury 2015-10-19 22:04:15 +02:00
parent fa24d2da6f
commit ac5e8a9766
7 changed files with 77 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

91
solver/internal.ml
View file

@ -145,6 +145,9 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
tatoms_qhead = 0; tatoms_qhead = 0;
} }
(* Level for push/pop operations *)
let current_level () = Vec.size env.user_levels
(* Iteration over subterms *) (* Iteration over subterms *)
module Mi = Map.Make(struct type t = int let compare = Pervasives.compare end) module Mi = Map.Make(struct type t = int let compare = Pervasives.compare end)
let iter_map = ref Mi.empty let iter_map = ref Mi.empty
@ -349,6 +352,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
let is_uip = ref false in let is_uip = ref false in
let c = ref (Proof.to_list c_clause) in let c = ref (Proof.to_list c_clause) in
let history = ref [c_clause] in let history = ref [c_clause] in
let c_level = ref 0 in
clause_bump_activity c_clause; clause_bump_activity c_clause;
let is_semantic a = match a.var.reason with let is_semantic a = match a.var.reason with
| Semantic _ -> true | Semantic _ -> true
@ -380,6 +384,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
begin match tmp with begin match tmp with
| [] -> L.debug 15 "No lit to resolve over." | [] -> L.debug 15 "No lit to resolve over."
| [b] when b == a.var.pa -> | [b] when b == a.var.pa ->
c_level := max !c_level d.c_level;
clause_bump_activity d; clause_bump_activity d;
var_bump_activity a.var; var_bump_activity a.var;
history := d :: !history; history := d :: !history;
@ -392,7 +397,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
with Exit -> with Exit ->
let learnt = List.sort (fun a b -> Pervasives.compare b.var.level a.var.level) !c in let learnt = List.sort (fun a b -> Pervasives.compare b.var.level a.var.level) !c in
let blevel = backtrack_lvl !is_uip learnt in let blevel = backtrack_lvl !is_uip learnt in
blevel, learnt, !history, !is_uip blevel, learnt, !history, !is_uip, !c_level
let get_atom i = let get_atom i =
destruct (Vec.get env.trail i) destruct (Vec.get env.trail i)
@ -408,6 +413,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
let tr_ind = ref (Vec.size env.trail - 1) in let tr_ind = ref (Vec.size env.trail - 1) in
let size = ref 1 in let size = ref 1 in
let history = ref [] in let history = ref [] in
let c_level = ref 0 in
while !cond do while !cond do
if !c.learnt then clause_bump_activity !c; if !c.learnt then clause_bump_activity !c;
history := !c :: !history; history := !c :: !history;
@ -438,11 +444,13 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
| 0, _ -> | 0, _ ->
cond := false; cond := false;
learnt := p.neg :: (List.rev !learnt) learnt := p.neg :: (List.rev !learnt)
| n, Bcp Some cl -> c := cl | n, Bcp Some cl ->
c_level := max !c_level cl.c_level;
c := cl
| n, _ -> assert false | n, _ -> assert false
done; done;
List.iter (fun q -> q.var.seen <- false) !seen; List.iter (fun q -> q.var.seen <- false) !seen;
!blevel, !learnt, !history, true !blevel, !learnt, !history, true, !c_level
let analyze c_clause = let analyze c_clause =
if St.mcsat then if St.mcsat then
@ -450,7 +458,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
else else
analyze_sat c_clause analyze_sat c_clause
let record_learnt_clause confl blevel learnt history is_uip = let record_learnt_clause confl blevel learnt history is_uip lvl =
begin match learnt with begin match learnt with
| [] -> assert false | [] -> assert false
| [fuip] -> | [fuip] ->
@ -459,14 +467,14 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
report_unsat confl report_unsat confl
else begin else begin
let name = fresh_lname () in let name = fresh_lname () in
let uclause = make_clause name learnt (List.length learnt) true history in let uclause = make_clause name learnt (List.length learnt) true history lvl in
L.debug 1 "Unit clause learnt : %a" St.pp_clause uclause; L.debug 1 "Unit clause learnt : %a" St.pp_clause uclause;
Vec.push env.learnts uclause; Vec.push env.learnts uclause;
enqueue_bool fuip 0 (Bcp (Some uclause)) enqueue_bool fuip 0 (Bcp (Some uclause))
end end
| fuip :: _ -> | fuip :: _ ->
let name = fresh_lname () in let name = fresh_lname () in
let lclause = make_clause name learnt (List.length learnt) true history in let lclause = make_clause name learnt (List.length learnt) true history lvl in
L.debug 2 "New clause learnt : %a" St.pp_clause lclause; L.debug 2 "New clause learnt : %a" St.pp_clause lclause;
Vec.push env.learnts lclause; Vec.push env.learnts lclause;
attach_clause lclause; attach_clause lclause;
@ -486,55 +494,61 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
env.conflicts <- env.conflicts + 1; env.conflicts <- env.conflicts + 1;
if decision_level() = 0 || Vec.for_all (fun a -> a.var.level = 0) confl.atoms then if decision_level() = 0 || Vec.for_all (fun a -> a.var.level = 0) confl.atoms then
report_unsat confl; (* Top-level conflict *) report_unsat confl; (* Top-level conflict *)
let blevel, learnt, history, is_uip = analyze confl in let blevel, learnt, history, is_uip, lvl = analyze confl in
cancel_until blevel; cancel_until blevel;
record_learnt_clause confl blevel learnt (History history) is_uip record_learnt_clause confl blevel learnt (History history) is_uip lvl
(* Add a new clause *) (* Add a new clause *)
exception Trivial exception Trivial
let simplify_zero atoms init0 = let simplify_zero atoms level0 =
(* TODO: could be more efficient than [@] everywhere? *) (* TODO: could be more efficient than [@] everywhere? *)
assert (decision_level () = 0); assert (decision_level () = 0);
let aux (atoms, init) a = let aux (atoms, init, lvl) 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 begin
atoms, false match a.var.reason with
else | Bcp (Some cl) -> atoms, true, max lvl cl.c_level
a::atoms, init | _ -> assert false
end else
a::atoms, init, lvl
in in
let atoms, init = List.fold_left aux ([], true) atoms in let atoms, init, lvl = List.fold_left aux ([], false, level0) atoms in
List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init, lvl
let partition atoms init0 = let partition atoms init0 =
let rec partition_aux trues unassigned falses init = function let rec partition_aux trues unassigned falses init lvl = function
| [] -> trues @ unassigned @ falses, init | [] -> trues @ unassigned @ falses, init, lvl
| a :: r -> | a :: r ->
if a.is_true then if a.is_true then
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, lvl
else if a.neg.is_true then else if a.neg.is_true then
if a.var.level = 0 then if a.var.level = 0 then begin
partition_aux trues unassigned falses false r match a.var.reason with
else | Bcp (Some cl) ->
partition_aux trues unassigned (a::falses) init r partition_aux trues unassigned falses true (max lvl cl.c_level) r
| _ -> assert false
end else
partition_aux trues unassigned (a::falses) init lvl r
else else
partition_aux trues (a::unassigned) falses init r partition_aux trues (a::unassigned) falses init lvl r
in in
if decision_level () = 0 then if decision_level () = 0 then
simplify_zero atoms init0 simplify_zero atoms init0
else else
partition_aux [] [] [] true atoms partition_aux [] [] [] false init0 atoms
let add_clause ?tag name atoms history = let add_clause ?tag name atoms history =
if env.is_unsat then raise Unsat; (* is it necessary ? *) if env.is_unsat then raise Unsat; (* is it necessary ? *)
let init_name = name in let init_name = name in
let init0 = make_clause ?tag init_name atoms (List.length atoms) (history <> History []) history in let c_level = current_level () in
let init0 = make_clause ?tag init_name atoms (List.length atoms) (history <> History []) history c_level in
L.debug 10 "Adding clause : %a" St.pp_clause init0; L.debug 10 "Adding clause : %a" St.pp_clause init0;
try try
if Proof.has_been_proved init0 then raise Trivial; if Proof.has_been_proved init0 then raise Trivial;
assert (Proof.is_proven init0); (* Important side-effect, DO NOT REMOVE *) assert (Proof.is_proven init0); (* Important side-effect, DO NOT REMOVE *)
let atoms, init = partition atoms init0 in let atoms, init, level = partition atoms c_level in
let size = List.length atoms in let size = List.length atoms in
match atoms with match atoms with
| [] -> | [] ->
@ -542,7 +556,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
| a::b::_ -> | a::b::_ ->
let clause = let clause =
if init then init0 if init then init0
else make_clause ?tag (fresh_name ()) atoms size true (History [init0]) else make_clause ?tag (fresh_name ()) atoms size true (History [init0]) level
in in
L.debug 1 "New clause : %a" St.pp_clause clause; L.debug 1 "New clause : %a" St.pp_clause clause;
attach_clause clause; attach_clause clause;
@ -685,7 +699,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
let l = List.rev_map new_atom l in let l = List.rev_map new_atom l in
Iheap.grow_to_by_double env.order (St.nb_elt ()); Iheap.grow_to_by_double env.order (St.nb_elt ());
List.iter (fun a -> insert_var_order (elt_of_var a.var)) l; 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 let c = St.make_clause (St.fresh_tname ()) l (List.length l) true (Lemma p) (current_level ())in
Some c Some c
and propagate () = and propagate () =
@ -923,8 +937,6 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
let base_level = 0 let base_level = 0
let current_level () = Vec.size env.user_levels
let push () = let push () =
let ul_trail = if Vec.is_empty env.trail_lim let ul_trail = if Vec.is_empty env.trail_lim
then base_level then base_level
@ -938,17 +950,20 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
if l > current_level() if l > current_level()
then invalid_arg "cannot pop() to level, it is too high"; then invalid_arg "cannot pop() to level, it is too high";
let ul = Vec.get env.user_levels l in let ul = Vec.get env.user_levels l in
(* see whether we can reset [env.is_unsat] *) if env.is_unsat then begin
if env.is_unsat && not (Vec.is_empty env.trail_lim) then ( match env.unsat_conflict with
(* level at which the decision that lead to unsat was made *) | Some cl ->
let last = Vec.last env.trail_lim in if cl.c_level > l then begin
if ul.ul_trail < last then env.is_unsat <- false env.unsat_conflict <- None;
); env.is_unsat <- false
end
| _ -> assert false
end;
cancel_until ul.ul_trail; cancel_until ul.ul_trail;
Vec.shrink env.clauses ul.ul_clauses; Vec.shrink env.clauses ul.ul_clauses;
Vec.shrink env.learnts ul.ul_learnt; Vec.shrink env.learnts ul.ul_learnt;
() ()
let clear () = pop base_level let reset () = pop base_level
end end

8
solver/internal.mli
View file

@ -8,6 +8,8 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
(Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof) : sig (Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof) : sig
(** Functor to create a solver parametrised by the atomic formulas and a theory. *) (** Functor to create a solver parametrised by the atomic formulas and a theory. *)
(** {2 Solving facilities} *)
exception Unsat exception Unsat
module Proof : Res.S with module St = St module Proof : Res.S with module St = St
@ -40,6 +42,9 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
val model : unit -> (St.term * St.term) list val model : unit -> (St.term * St.term) list
(** Returns the model found if the formula is satisfiable. *) (** Returns the model found if the formula is satisfiable. *)
(** {2 Backtracking facilities} *)
type level type level
(** Abstract notion of assumption level. *) (** Abstract notion of assumption level. *)
@ -56,7 +61,8 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
(** Go back to the given level, forgetting every assumption added since. (** Go back to the given level, forgetting every assumption added since.
@raise Invalid_argument if the current level is below the argument *) @raise Invalid_argument if the current level is below the argument *)
val clear : unit -> unit val reset : unit -> unit
(** Return to level {!base_level} *) (** Return to level {!base_level} *)
end end

2
solver/mcsolver.mli
View file

@ -62,7 +62,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
(** Go back to the given level, forgetting every assumption added since. (** Go back to the given level, forgetting every assumption added since.
@raise Invalid_argument if the current level is below the argument *) @raise Invalid_argument if the current level is below the argument *)
val clear : unit -> unit val reset : unit -> unit
(** Return to level {!base_level} *) (** Return to level {!base_level} *)
end end

3
solver/res.ml
View file

@ -122,7 +122,8 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
| [] -> raise (Resolution_error "No literal to resolve over") | [] -> raise (Resolution_error "No literal to resolve over")
| [a] -> | [a] ->
H.add proof new_clause (Resolution (a, (c, cl_c), (d, cl_d))); H.add proof new_clause (Resolution (a, (c, cl_c), (d, cl_d)));
let new_c = St.make_clause (fresh_pcl_name ()) new_clause (List.length new_clause) true St.(History [c; d]) in let new_c = St.make_clause (fresh_pcl_name ()) new_clause (List.length new_clause)
true St.(History [c; d]) (max c.St.c_level d.St.c_level) in
L.debug 5 "New clause : %a" St.pp_clause new_c; L.debug 5 "New clause : %a" St.pp_clause new_c;
new_c, new_clause new_c, new_clause
| _ -> raise (Resolution_error "Resolved to a tautology") | _ -> raise (Resolution_error "Resolved to a tautology")

2
solver/solver.mli
View file

@ -65,7 +65,7 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
(** Go back to the given level, forgetting every assumption added since. (** Go back to the given level, forgetting every assumption added since.
@raise Invalid_argument if the current level is below the argument *) @raise Invalid_argument if the current level is below the argument *)
val clear : unit -> unit val reset : unit -> unit
(** Return to level {!base_level} *) (** Return to level {!base_level} *)
end end

14
solver/solver_types.ml
View file

@ -57,6 +57,7 @@ module McMake (L : Log_intf.S)(E : Expr_intf.S) = struct
atoms : atom Vec.t; atoms : atom Vec.t;
learnt : bool; learnt : bool;
cpremise : premise; cpremise : premise;
c_level : int;
mutable activity : float; mutable activity : float;
mutable removed : bool; mutable removed : bool;
} }
@ -101,6 +102,7 @@ module McMake (L : Log_intf.S)(E : Expr_intf.S) = struct
atoms = Vec.make_empty dummy_atom; atoms = Vec.make_empty dummy_atom;
activity = -1.; activity = -1.;
removed = false; removed = false;
c_level = -1;
learnt = false; learnt = false;
cpremise = History [] } cpremise = History [] }
@ -177,17 +179,18 @@ module McMake (L : Log_intf.S)(E : Expr_intf.S) = struct
let var, negated = make_boolean_var lit in let var, negated = make_boolean_var lit in
if negated then var.na else var.pa if negated then var.na else var.pa
let make_clause ?tag name ali sz_ali is_learnt premise = let make_clause ?tag name ali sz_ali is_learnt premise lvl =
let atoms = Vec.from_list ali sz_ali dummy_atom in let atoms = Vec.from_list ali sz_ali dummy_atom in
{ name = name; { name = name;
tag = tag; tag = tag;
atoms = atoms; atoms = atoms;
removed = false; removed = false;
learnt = is_learnt; learnt = is_learnt;
c_level = lvl;
activity = 0.; activity = 0.;
cpremise = premise} cpremise = premise}
let empty_clause = make_clause "Empty" [] 0 false (History []) let empty_clause = make_clause "Empty" [] 0 false (History []) 0
(* Decisions & propagations *) (* Decisions & propagations *)
type t = (lit, atom) Either.t type t = (lit, atom) Either.t
@ -337,6 +340,7 @@ module SatMake (L : Log_intf.S)(E : Formula_intf.S) = struct
atoms : atom Vec.t; atoms : atom Vec.t;
learnt : bool; learnt : bool;
cpremise : premise; cpremise : premise;
c_level : int;
mutable activity : float; mutable activity : float;
mutable removed : bool; mutable removed : bool;
} }
@ -382,6 +386,7 @@ module SatMake (L : Log_intf.S)(E : Formula_intf.S) = struct
atoms = Vec.make_empty dummy_atom; atoms = Vec.make_empty dummy_atom;
activity = -1.; activity = -1.;
removed = false; removed = false;
c_level = -1;
learnt = false; learnt = false;
cpremise = History [] } cpremise = History [] }
@ -442,17 +447,18 @@ module SatMake (L : Log_intf.S)(E : Formula_intf.S) = struct
let var, negated = make_boolean_var lit in let var, negated = make_boolean_var lit in
if negated then var.na else var.pa if negated then var.na else var.pa
let make_clause ?tag name ali sz_ali is_learnt premise = let make_clause ?tag name ali sz_ali is_learnt premise lvl =
let atoms = Vec.from_list ali sz_ali dummy_atom in let atoms = Vec.from_list ali sz_ali dummy_atom in
{ name = name; { name = name;
tag = tag; tag = tag;
atoms = atoms; atoms = atoms;
removed = false; removed = false;
learnt = is_learnt; learnt = is_learnt;
c_level = lvl;
activity = 0.; activity = 0.;
cpremise = premise} cpremise = premise}
let empty_clause = make_clause "Empty" [] 0 false (History []) let empty_clause = make_clause "Empty" [] 0 false (History []) 0
(* Decisions & propagations *) (* Decisions & propagations *)
type t = atom type t = atom

5
solver/solver_types_intf.ml
View file

@ -55,6 +55,7 @@ module type S = sig
atoms : atom Vec.t; atoms : atom Vec.t;
learnt : bool; learnt : bool;
cpremise : premise; cpremise : premise;
c_level : int;
mutable activity : float; mutable activity : float;
mutable removed : bool; mutable removed : bool;
} }
@ -115,8 +116,8 @@ module type S = sig
val empty_clause : clause val empty_clause : clause
(** The empty clause *) (** The empty clause *)
val make_clause : ?tag:int -> string -> atom list -> int -> bool -> premise -> clause val make_clause : ?tag:int -> string -> atom list -> int -> bool -> premise -> int -> clause
(** [make_clause name atoms size learnt premise] creates a clause with the given attributes. *) (** [make_clause name atoms size learnt premise level] creates a clause with the given attributes. *)
(** {2 Proof management} *) (** {2 Proof management} *)