simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-21 16:56:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

wip: perf(lra): implement basic propagations

Browse source
This commit is contained in:
Simon Cruanes 2021-02-22 14:28:44 -05:00
parent 7bf6b18bc0
commit 3fedca069d
4 changed files with 130 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/arith/lra/linear_expr_intf.ml
View file

@ -55,6 +55,8 @@ module type VAR = sig
type lit
val pp_lit : lit Fmt.printer
val not_lit : lit -> lit option
end
type bool_op = Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq

38
src/arith/lra/sidekick_arith_lra.ml
View file

@ -120,6 +120,9 @@ module Make(A : ARG) : S with module A = A = struct
let compare = A.S.T.Term.compare
type lit = Tag.t
let pp_lit = Tag.pp
let not_lit = function
| Tag.Lit l -> Some (Tag.Lit (Lit.neg l))
| _ -> None
end
module LE_ = Linear_expr.Make(struct include Q let pp=pp_print end)(SimpVar)
@ -213,8 +216,10 @@ module Make(A : ARG) : S with module A = A = struct
if LE_.Comb.is_empty le_comb then (
Log.debug 50 "(lra.encode-le.is-trivially-0)";
SimpSolver.add_constraint self.simplex
~on_propagate:(fun _ ~reason:_ -> ())
(SimpSolver.Constraint.leq proxy Q.zero) Tag.By_def;
SimpSolver.add_constraint self.simplex
~on_propagate:(fun _ ~reason:_ -> ())
(SimpSolver.Constraint.geq proxy Q.zero) Tag.By_def;
) else (
LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb;
@ -280,6 +285,11 @@ module Make(A : ARG) : S with module A = A = struct
in
let new_t = A.mk_lra tst (LRA_simplex_pred (proxy, op, le_const)) in
begin
let lit = mk_lit new_t in
let constr = SimpSolver.Constraint.mk proxy op le_const in
SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
end;
Log.debugf 10 (fun k->k "lra.preprocess:@ %a@ :into %a" T.pp t T.pp new_t);
Some new_t
@ -300,6 +310,11 @@ module Make(A : ARG) : S with module A = A = struct
let op = if Q.(coeff < zero) then S_op.neg_sign op else op in
let new_t = A.mk_lra tst (LRA_simplex_pred (v, op, q)) in
begin
let lit = mk_lit new_t in
let constr = SimpSolver.Constraint.mk v op q in
SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
end;
Log.debugf 10 (fun k->k "lra.preprocess@ :%a@ :into %a" T.pp t T.pp new_t);
Some new_t
@ -387,9 +402,21 @@ module Make(A : ARG) : S with module A = A = struct
in
SI.raise_conflict si acts confl SI.P.default
let on_propagate_ si acts lit ~reason =
match lit with
| Tag.Lit lit ->
SI.propagate si acts lit
(fun() -> CCList.flat_map (Tag.to_lits si) reason)
| _ -> ()
let check_simplex_ self si acts : SimpSolver.Subst.t =
Log.debug 5 "lra: call arith solver";
let res = Profile.with1 "simplex.solve" SimpSolver.check self.simplex in
let res =
Profile.with_ "simplex.solve"
(fun () ->
SimpSolver.check self.simplex
~on_propagate:(on_propagate_ si acts))
in
begin match res with
| SimpSolver.Sat m -> m
| SimpSolver.Unsat cert ->
@ -416,9 +443,11 @@ module Make(A : ARG) : S with module A = A = struct
begin
try
let c1 = SimpSolver.Constraint.geq v le_const in
SimpSolver.add_constraint self.simplex c1 lit;
SimpSolver.add_constraint self.simplex c1 lit
~on_propagate:(on_propagate_ si acts);
let c2 = SimpSolver.Constraint.leq v le_const in
SimpSolver.add_constraint self.simplex c2 lit;
SimpSolver.add_constraint self.simplex c2 lit
~on_propagate:(on_propagate_ si acts);
with SimpSolver.E_unsat cert ->
fail_with_cert si acts cert
end;
@ -492,6 +521,8 @@ module Make(A : ARG) : S with module A = A = struct
(fun lit ->
let sign = SI.Lit.sign lit in
let lit_t = SI.Lit.term lit in
Log.debugf 50 (fun k->k "(@[lra.partial-check.add@ :lit %a@ :lit-t %a@])"
SI.Lit.pp lit T.pp lit_t);
match A.view_as_lra lit_t with
| LRA_simplex_pred (v, op, q) ->
@ -508,6 +539,7 @@ module Make(A : ARG) : S with module A = A = struct
try
SimpSolver.add_var self.simplex v;
SimpSolver.add_constraint self.simplex constr (Tag.Lit lit)
~on_propagate:(on_propagate_ si acts);
with SimpSolver.E_unsat cert ->
Log.debugf 10
(fun k->k "(@[lra.partial-check.unsat@ :cert %a@])"

87
src/arith/lra/simplex2.ml
View file

@ -93,22 +93,37 @@ module type S = sig
exception E_unsat of Unsat_cert.t
type ev_on_propagate = V.lit -> reason:V.lit list -> unit
val add_var : t -> V.t -> unit
(** Make sure the variable exists in the simplex. *)
val add_constraint : t -> Constraint.t -> V.lit -> unit
val add_constraint :
on_propagate:ev_on_propagate ->
t -> Constraint.t -> V.lit -> unit
(** Add a constraint to the simplex.
@raise Unsat if it's immediately obvious that this is not satisfiable. *)
val check_exn : t -> unit
val declare_bound : t -> Constraint.t -> V.lit -> unit
(** Declare that this constraint exists, so we can possibly propagate it.
Unlike {!add_constraint} this does {b NOT} assert that the constraint
is true *)
val check_exn :
on_propagate:(V.lit -> reason:V.lit list -> unit) ->
t -> unit
(** Check the whole simplex for satisfiability.
@param on_propagate is called with arguments [lit, reason] whenever
[reason => lit] is found to be true by the simplex.
@raise Unsat if the constraints are not satisfiable. *)
type result =
| Sat of Subst.t
| Unsat of Unsat_cert.t
val check : t -> result
val check :
on_propagate:(V.lit -> reason:V.lit list -> unit) ->
t -> result
(** Call {!check_exn} and return a model or a proof of unsat. *)
(**/**)
@ -218,6 +233,7 @@ module Make(Var: VAR)
b_lit: Var.lit;
}
type is_lower = bool
type var_state = {
var: V.t;
mutable value: erat;
@ -225,6 +241,7 @@ module Make(Var: VAR)
mutable basic_idx: int; (* index of the row in the matrix, if any. -1 otherwise *)
mutable l_bound: bound option;
mutable u_bound: bound option;
mutable all_bound_lits : (is_lower * bound) list; (* all known literals on this var *)
}
(** {2 Matrix}
@ -375,6 +392,7 @@ module Make(Var: VAR)
stat_check: int Stat.counter;
stat_unsat: int Stat.counter;
stat_define: int Stat.counter;
stat_propagate: int Stat.counter;
}
let push_level self : unit =
@ -462,6 +480,7 @@ module Make(Var: VAR)
basic_idx=row_idx;
l_bound=None;
u_bound=None;
all_bound_lits=[];
})
in
Log.debugf 5 (fun k->k "(@[simplex.define@ @[v%d :var %a@]@ :linexpr %a@])"
@ -516,6 +535,7 @@ module Make(Var: VAR)
l_bound=None;
u_bound=None;
value=Erat.zero;
all_bound_lits=[];
} in
assert (Var_state.is_n_basic vs);
self.var_tbl <- V_map.add x vs self.var_tbl;
@ -666,11 +686,13 @@ module Make(Var: VAR)
exception E_unsat of Unsat_cert.t
type ev_on_propagate = V.lit -> reason:V.lit list -> unit
let add_var self (v:V.t) : unit =
ignore (find_or_create_n_basic_var_ self v : var_state);
()
let add_constraint (self:t) (c:Constraint.t) (lit:V.lit) : unit =
let add_constraint ~on_propagate (self:t) (c:Constraint.t) (lit:V.lit) : unit =
let open Constraint in
let vs = find_or_create_n_basic_var_ self c.lhs in
@ -700,6 +722,23 @@ module Make(Var: VAR)
Backtrack_stack.push self.bound_stack (vs, `Lower, vs.l_bound);
vs.l_bound <- Some new_bnd;
(* propagate *)
List.iter
(fun (is_lower', bnd) ->
if is_lower' && Erat.(bnd.b_val < new_bnd.b_val) then (
(* subsumed *)
Stat.incr self.stat_propagate;
on_propagate (bnd.b_lit) ~reason:[new_bnd.b_lit];
) else if not is_lower' && Erat.(bnd.b_val < new_bnd.b_val) then (
(* incompatible upper bound *)
match V.not_lit bnd.b_lit with
| Some l' ->
Stat.incr self.stat_propagate;
on_propagate l' ~reason:[new_bnd.b_lit];
| None -> ()
)
) vs.all_bound_lits;
if Var_state.is_n_basic vs &&
Erat.(vs.value < new_bnd.b_val) then (
(* line 5: need to update non-basic variable *)
@ -719,6 +758,23 @@ module Make(Var: VAR)
Backtrack_stack.push self.bound_stack (vs, `Upper, vs.u_bound);
vs.u_bound <- Some new_bnd;
(* propagate *)
List.iter
(fun (is_lower', bnd) ->
if not is_lower' && Erat.(bnd.b_val > new_bnd.b_val) then (
(* subsumed *)
Stat.incr self.stat_propagate;
on_propagate (bnd.b_lit) ~reason:[new_bnd.b_lit];
) else if is_lower' && Erat.(bnd.b_val > new_bnd.b_val) then (
(* incompatible lower bound *)
match V.not_lit bnd.b_lit with
| Some l' ->
Stat.incr self.stat_propagate;
on_propagate l' ~reason:[new_bnd.b_lit];
| None -> ()
)
) vs.all_bound_lits;
if Var_state.is_n_basic vs &&
Erat.(vs.value > new_bnd.b_val) then (
(* line 5: need to update non-basic variable *)
@ -727,6 +783,22 @@ module Make(Var: VAR)
end
)
let declare_bound (self:t) (c:Constraint.t) (lit:V.lit) : unit =
let vs = find_or_create_n_basic_var_ self c.lhs in
Log.debugf 10
(fun k->k "(@[simplex2.declare-bound@ %a@ :lit %a@])"
Constraint.pp c V.pp_lit lit);
let is_lower_bnd, new_bnd_val =
match c.op with
| Leq -> false, Erat.make_q c.rhs
| Lt -> false, Erat.make c.rhs Q.minus_one
| Geq -> true, Erat.make_q c.rhs
| Gt -> true, Erat.make c.rhs Q.one
in
let new_bnd = is_lower_bnd, {b_val=new_bnd_val; b_lit=lit} in
vs.all_bound_lits <- new_bnd :: vs.all_bound_lits
(* try to find basic variable that doesn't respect one of its bounds *)
let find_basic_var_ (self:t) : (var_state * [`Lower | `Upper] * bound) option =
let n = Matrix.n_rows self.matrix in
@ -815,7 +887,7 @@ module Make(Var: VAR)
(* main satisfiability check.
page 15, figure 3.2 *)
let check_exn (self:t) : unit =
let check_exn ~on_propagate:_ (self:t) : unit =
let exception Stop in
Log.debugf 20 (fun k->k "(@[simplex2.check@ %a@])" pp_stats self);
Stat.incr self.stat_check;
@ -894,6 +966,7 @@ module Make(Var: VAR)
stat_check=Stat.mk_int stat "simplex.check";
stat_unsat=Stat.mk_int stat "simplex.unsat";
stat_define=Stat.mk_int stat "simplex.define";
stat_propagate=Stat.mk_int stat "simplex.propagate";
} in
self
@ -987,9 +1060,9 @@ module Make(Var: VAR)
(fun k->k "(@[simplex2.model@ %a@])" Subst.pp subst);
subst
let check (self:t) : result =
let check ~on_propagate (self:t) : result =
try
check_exn self;
check_exn ~on_propagate self;
let m = model_ self in
Sat m
with E_unsat c -> Unsat c

23
src/arith/tests/test_simplex2.ml
View file

@ -14,6 +14,7 @@ module Var = struct
let rand n : t QC.arbitrary = QC.make ~print:(Fmt.to_string pp) @@ QC.Gen.(0--n)
type lit = int
let pp_lit = Fmt.int
let not_lit i = Some (- i)
end
module Spl = Sidekick_arith_lra.Simplex2.Make(Var)
@ -155,18 +156,20 @@ module Step = struct
let rand : t list QC.arbitrary = rand_for 1 100
end
let on_propagate _ ~reason:_ = ()
(* add a single step to the simplexe *)
let add_step simplex (s:Step.t) : unit =
begin match s with
| Step.S_new_var v -> Spl.add_var simplex v
| Step.S_leq (v,n) ->
Spl.add_constraint simplex (Spl.Constraint.leq v n) 0
Spl.add_constraint simplex (Spl.Constraint.leq v n) 0 ~on_propagate
| Step.S_lt (v,n) ->
Spl.add_constraint simplex (Spl.Constraint.lt v n) 0
Spl.add_constraint simplex (Spl.Constraint.lt v n) 0 ~on_propagate
| Step.S_geq (v,n) ->
Spl.add_constraint simplex (Spl.Constraint.geq v n) 0
Spl.add_constraint simplex (Spl.Constraint.geq v n) 0 ~on_propagate
| Step.S_gt (v,n) ->
Spl.add_constraint simplex (Spl.Constraint.gt v n) 0
Spl.add_constraint simplex (Spl.Constraint.gt v n) 0 ~on_propagate
| Step.S_define (x,le) ->
Spl.define simplex x le
end
@ -179,18 +182,18 @@ let add_steps ?(f=fun()->()) (simplex:Spl.t) l : unit =
(* is this simplex's state sat? *)
let check_simplex_is_sat simplex : bool =
(try Spl.check_exn simplex; true
(try Spl.check_exn ~on_propagate simplex; true
with Spl.E_unsat _ -> false)
(* is this problem sat? *)
let check_pb_is_sat pb : bool =
let simplex = Spl.create() in
(try add_steps simplex pb; Spl.check_exn simplex; true
(try add_steps simplex pb; Spl.check_exn ~on_propagate simplex; true
with Spl.E_unsat _ -> false)
let check_steps l : bool =
let simplex = Spl.create () in
try add_steps simplex l; Spl.check_exn simplex; true
try add_steps simplex l; Spl.check_exn ~on_propagate simplex; true
with _ -> false
(* basic debug printer for Q.t *)
@ -200,7 +203,7 @@ let prop_sound ?(inv=false) pb =
let simplex = Spl.create () in
begin match
add_steps simplex pb;
Spl.check simplex
Spl.check ~on_propagate simplex
with
| Sat subst ->
@ -279,7 +282,7 @@ let prop_invariants pb =
let simplex = Spl.create () in
(try
add_steps simplex pb ~f:(fun () -> Spl._check_invariants simplex);
Spl.check_exn simplex
Spl.check_exn ~on_propagate simplex
with Spl.E_unsat _ -> ());
Spl._check_invariants simplex;
true
@ -337,7 +340,7 @@ let check_scalable =
let simplex = Spl.create () in
(try
add_steps simplex pb;
Spl.check_exn simplex
Spl.check_exn ~on_propagate simplex
with _ -> ());
true
in