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

Add unsat core explanations to the simplex

Browse source
This commit is contained in:
Guillaume Bury 2020-12-22 14:16:23 +01:00
parent a6f6a99fb3
commit 4be726db43
4 changed files with 99 additions and 52 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -253,7 +253,9 @@ module Make(A : ARG) : S with module A = A = struct
let open LE.Infix in let open LE.Infix in
let le = le - LE.monomial1 t in let le = le - LE.monomial1 t in
let c = LConstr.eq0 le in let c = LConstr.eq0 le in
SimpSolver.add_constr simplex c) let lit = assert false (* TODO: find the lit *) in
SimpSolver.add_constr simplex c lit
)
self.t_defs self.t_defs
end; end;
(* add trail *) (* add trail *)
@ -274,7 +276,7 @@ module Make(A : ARG) : S with module A = A = struct
) else ( ) else (
(* TODO: tag *) (* TODO: tag *)
let c = LConstr.of_expr LE.(a-b) pred in let c = LConstr.of_expr LE.(a-b) pred in
SimpSolver.add_constr simplex c; SimpSolver.add_constr simplex c lit;
) )
end) end)
end; end;
@ -283,17 +285,18 @@ module Make(A : ARG) : S with module A = A = struct
| SimpSolver.Solution _m -> | SimpSolver.Solution _m ->
Log.debug 5 "lra: solver returns SAT"; Log.debug 5 "lra: solver returns SAT";
() (* TODO: get a model + model combination *) () (* TODO: get a model + model combination *)
| SimpSolver.Unsatisfiable _cert -> | SimpSolver.Unsatisfiable cert ->
(* we tagged assertions with their lit, so the certificate being an begin match SimpSolver.check_cert simplex cert with
unsat core translates directly into a conflict clause *) | `Ok _unsat_core -> assert false (* TODO *)
assert false | _ -> assert false (* some kind of fatal error ? *)
(* TODO (* TODO
Log.debugf 5 (fun k->k"lra: solver returns UNSAT@ with cert %a" Log.debugf 5 (fun k->k"lra: solver returns UNSAT@ with cert %a"
(Fmt.Dump.list Lit.pp) lits); (Fmt.Dump.list Lit.pp) lits);
let confl = List.rev_map Lit.neg lits in let confl = List.rev_map Lit.neg lits in
(* TODO: produce and store a proper LRA resolution proof *) (* TODO: produce and store a proper LRA resolution proof *)
SI.raise_conflict si acts confl SI.P.default SI.raise_conflict si acts confl SI.P.default
*) *)
end
end; end;
() ()

110
src/arith/lra/simplex.ml
View file

@ -122,13 +122,18 @@ module Make_inner
let str_of_erat = Format.to_string Erat.pp let str_of_erat = Format.to_string Erat.pp
let str_of_q = Format.to_string Q.pp_print let str_of_q = Format.to_string Q.pp_print
type bound = {
value : Erat.t;
reason : lit option;
}
type t = { type t = {
param: param; param: param;
tab : Q.t Matrix.t; (* the matrix of coefficients *) tab : Q.t Matrix.t; (* the matrix of coefficients *)
basic : basic_var Vec.vector; (* basic variables *) basic : basic_var Vec.vector; (* basic variables *)
nbasic : nbasic_var Vec.vector; (* non basic variables *) nbasic : nbasic_var Vec.vector; (* non basic variables *)
mutable assign : Erat.t M.t; (* assignments *) mutable assign : Erat.t M.t; (* assignments *)
mutable bounds : (Erat.t * Erat.t) M.t; (* (lower, upper) bounds for variables *) mutable bounds : (bound * bound) M.t; (* (lower, upper) bounds for variables *)
mutable idx_basic : int M.t; (* basic var -> its index in [basic] *) mutable idx_basic : int M.t; (* basic var -> its index in [basic] *)
mutable idx_nbasic : int M.t; (* non basic var -> its index in [nbasic] *) mutable idx_nbasic : int M.t; (* non basic var -> its index in [nbasic] *)
} }
@ -136,7 +141,6 @@ module Make_inner
type cert = { type cert = {
cert_var: var; cert_var: var;
cert_expr: (Q.t * var) list; cert_expr: (Q.t * var) list;
cert_core: lit list;
} }
type res = type res =
@ -239,17 +243,23 @@ module Make_inner
with Not_found -> value_basic t x with Not_found -> value_basic t x
(* trivial bounds *) (* trivial bounds *)
let empty_bounds : Erat.t * Erat.t = Q.(Erat.make minus_inf zero, Erat.make inf zero) let empty_bounds : bound * bound =
{ value = Erat.make Q.minus_inf Q.zero; reason = None; },
{ value = Erat.make Q.inf Q.zero; reason = None; }
(* find bounds of [x] *) (* find bounds of [x] *)
let[@inline] get_bounds (t:t) (x:var) : Erat.t * Erat.t = let[@inline] get_bounds (t:t) (x:var) : bound * bound =
try M.find x t.bounds try M.find x t.bounds
with Not_found -> empty_bounds with Not_found -> empty_bounds
let[@inline] get_bounds_values (t:t) (x:var) : Erat.t * Erat.t =
let l, u = get_bounds t x in
l.value, u.value
(* is [value x] within the bounds for [x]? *) (* is [value x] within the bounds for [x]? *)
let is_within_bounds (t:t) (x:var) : bool * Erat.t = let is_within_bounds (t:t) (x:var) : bool * Erat.t =
let v = value t x in let v = value t x in
let low, upp = get_bounds t x in let low, upp = get_bounds_values t x in
if Erat.compare v low < 0 then if Erat.compare v low < 0 then
false, low false, low
else if Erat.compare v upp > 0 then else if Erat.compare v upp > 0 then
@ -313,15 +323,21 @@ module Make_inner
() ()
(* add bounds to [x] in [t] *) (* add bounds to [x] in [t] *)
let add_bound_aux (t:t) (x:var) (low:Erat.t) (upp:Erat.t) : unit = let add_bound_aux (t:t) (x:var)
(low:Erat.t) (low_reason:lit option)
(upp:Erat.t) (upp_reason:lit option) : unit =
add_vars t [x]; add_vars t [x];
let l, u = get_bounds t x in let l, u = get_bounds t x in
t.bounds <- M.add x (Erat.max l low, Erat.min u upp) t.bounds let l' = if Erat.lt low l.value then l else { value = low; reason = low_reason; } in
let u' = if Erat.gt upp u.value then u else { value = upp; reason = upp_reason; } in
t.bounds <- M.add x (l', u') t.bounds
let add_bounds (t:t) ?strict_lower:(slow=false) ?strict_upper:(supp=false) (x, l, u) : unit = let add_bounds (t:t)
?strict_lower:(slow=false) ?strict_upper:(supp=false)
?lower_reason ?upper_reason (x, l, u) : unit =
let e1 = if slow then Q.one else Q.zero in let e1 = if slow then Q.one else Q.zero in
let e2 = if supp then Q.neg Q.one else Q.zero in let e2 = if supp then Q.neg Q.one else Q.zero in
add_bound_aux t x (Erat.make l e1) (Erat.make u e2); add_bound_aux t x (Erat.make l e1) lower_reason (Erat.make u e2) upper_reason;
if mem_nbasic t x then ( if mem_nbasic t x then (
let b, v = is_within_bounds t x in let b, v = is_within_bounds t x in
if not b then ( if not b then (
@ -329,8 +345,11 @@ module Make_inner
) )
) )
let add_lower_bound t ?strict x l = add_bounds t ?strict_lower:strict (x,l,Q.inf) let add_lower_bound t ?strict ~reason x l =
let add_upper_bound t ?strict x u = add_bounds t ?strict_upper:strict (x,Q.minus_inf,u) add_bounds t ?strict_lower:strict ~lower_reason:reason (x,l,Q.inf)
let add_upper_bound t ?strict ~reason x u =
add_bounds t ?strict_upper:strict ~upper_reason:reason (x,Q.minus_inf,u)
(* full assignment *) (* full assignment *)
let full_assign (t:t) : (var * Erat.t) Iter.t = let full_assign (t:t) : (var * Erat.t) Iter.t =
@ -352,7 +371,8 @@ module Make_inner
let solve_epsilon (t:t) : Q.t = let solve_epsilon (t:t) : Q.t =
let emax = let emax =
M.fold M.fold
(fun x ({base=low;eps_factor=e_low}, {base=upp;eps_factor=e_upp}) emax -> (fun x ({ value = {base=low;eps_factor=e_low}; _},
{ value = {base=upp;eps_factor=e_upp}; _}) emax ->
let {base=v; eps_factor=e_v} = value t x in let {base=v; eps_factor=e_v} = value t x in
(* lower bound *) (* lower bound *)
let emax = let emax =
@ -396,7 +416,7 @@ module Make_inner
let test (y:nbasic_var) (a:Q.t) : bool = let test (y:nbasic_var) (a:Q.t) : bool =
assert (mem_nbasic t y); assert (mem_nbasic t y);
let v = value t y in let v = value t y in
let low, upp = get_bounds t y in let low, upp = get_bounds_values t y in
if b then ( if b then (
(Erat.lt v upp && Q.compare a Q.zero > 0) || (Erat.lt v upp && Q.compare a Q.zero > 0) ||
(Erat.gt v low && Q.compare a Q.zero < 0) (Erat.gt v low && Q.compare a Q.zero < 0)
@ -489,7 +509,7 @@ module Make_inner
(* check bounds *) (* check bounds *)
let check_bounds (t:t) : unit = let check_bounds (t:t) : unit =
M.iter (fun x (l, u) -> if Erat.gt l u then raise (AbsurdBounds x)) t.bounds M.iter (fun x (l, u) -> if Erat.gt l.value u.value then raise (AbsurdBounds x)) t.bounds
(* actual solving algorithm *) (* actual solving algorithm *)
let solve_aux (t:t) : unit = let solve_aux (t:t) : unit =
@ -534,9 +554,9 @@ module Make_inner
(Vec.to_list (find_expr_basic t x)) (Vec.to_list (find_expr_basic t x))
(Vec.to_list t.nbasic) (Vec.to_list t.nbasic)
in in
Unsatisfiable { cert_var=x; cert_expr; cert_core=[]; } (* FIXME *) Unsatisfiable { cert_var=x; cert_expr; } (* FIXME *)
| AbsurdBounds x -> | AbsurdBounds x ->
Unsatisfiable { cert_var=x; cert_expr=[]; cert_core=[]; } Unsatisfiable { cert_var=x; cert_expr=[]; }
(* add [c·x] to [m] *) (* add [c·x] to [m] *)
let add_expr_ (x:var) (c:Q.t) (m:Q.t M.t) = let add_expr_ (x:var) (c:Q.t) (m:Q.t M.t) =
@ -557,38 +577,54 @@ module Make_inner
!m !m
(* maybe invert bounds, if [c < 0] *) (* maybe invert bounds, if [c < 0] *)
let scale_bounds c (l,u) : erat * erat = let scale_bounds c (l,u) : bound * bound =
match Q.compare c Q.zero with match Q.compare c Q.zero with
| 0 -> Erat.zero, Erat.zero | 0 ->
| n when n<0 -> Erat.mul c u, Erat.mul c l let b = { value = Erat.zero; reason = None; } in
| _ -> Erat.mul c l, Erat.mul c u b, b
| n when n<0 ->
{ u with value = Erat.mul c u.value; },
{ l with value = Erat.mul c l.value; }
| _ ->
{ l with value = Erat.mul c l.value; },
{ u with value = Erat.mul c u.value; }
let add_to_unsat_core acc = function
| None -> acc
| Some reason -> reason :: acc
let check_cert (t:t) (c:cert) = let check_cert (t:t) (c:cert) =
let x = c.cert_var in let x = c.cert_var in
let low_x, up_x = get_bounds t x in let { value = low_x; reason = low_x_reason; },
{ value = up_x; reason = upp_x_reason; } = get_bounds t x in
begin match c.cert_expr with begin match c.cert_expr with
| [] -> | [] ->
if Erat.compare low_x up_x > 0 then `Ok if Erat.compare low_x up_x > 0
then `Ok (add_to_unsat_core (add_to_unsat_core [] low_x_reason) upp_x_reason)
else `Bad_bounds (str_of_erat low_x, str_of_erat up_x) else `Bad_bounds (str_of_erat low_x, str_of_erat up_x)
| expr -> | expr ->
let e0 = deref_var_ t x (Q.neg Q.one) M.empty in let e0 = deref_var_ t x (Q.neg Q.one) M.empty in
(* compute bounds for the expression [c.cert_expr], (* compute bounds for the expression [c.cert_expr],
and also compute [c.cert_expr - x] to check if it's 0] *) and also compute [c.cert_expr - x] to check if it's 0] *)
let low, up, expr_minus_x = let low, low_unsat_core, up, up_unsat_core, expr_minus_x =
List.fold_left List.fold_left
(fun (l,u,expr_minus_x) (c, y) -> (fun (l, luc, u, uuc, expr_minus_x) (c, y) ->
let ly, uy = scale_bounds c (get_bounds t y) in let ly, uy = scale_bounds c (get_bounds t y) in
assert (Erat.compare ly uy <= 0); assert (Erat.compare ly.value uy.value <= 0);
let expr_minus_x = deref_var_ t y c expr_minus_x in let expr_minus_x = deref_var_ t y c expr_minus_x in
Erat.sum l ly, Erat.sum u uy, expr_minus_x) let luc = add_to_unsat_core luc ly.reason in
(Erat.zero, Erat.zero, e0) let uuc = add_to_unsat_core uuc uy.reason in
Erat.sum l ly.value, luc, Erat.sum u uy.value, uuc, expr_minus_x)
(Erat.zero, [], Erat.zero, [], e0)
expr expr
in in
(* check that the expanded expression is [x], and that (* check that the expanded expression is [x], and that
one of the bounds on [x] is incompatible with bounds of [c.cert_expr] *) one of the bounds on [x] is incompatible with bounds of [c.cert_expr] *)
if M.is_empty expr_minus_x then ( if M.is_empty expr_minus_x then (
if Erat.compare low_x up > 0 || Erat.compare up_x low < 0 if Erat.compare low_x up > 0
then `Ok then `Ok (add_to_unsat_core up_unsat_core low_x_reason)
else if Erat.compare up_x low < 0
then `Ok (add_to_unsat_core low_unsat_core upp_x_reason)
else `Bad_bounds (str_of_erat low, str_of_erat up) else `Bad_bounds (str_of_erat low, str_of_erat up)
) else `Diff_not_0 expr_minus_x ) else `Diff_not_0 expr_minus_x
end end
@ -636,7 +672,7 @@ module Make_inner
let pp_bounds = let pp_bounds =
let open Format in let open Format in
let pp_pairs out (x,(l,u)) = let pp_pairs out (x,(l,u)) =
fprintf out "(@[%a =< %a =< %a@])" Erat.pp l Var.pp x Erat.pp u fprintf out "(@[%a =< %a =< %a@])" Erat.pp l.value Var.pp x Erat.pp u.value
in in
map Var_map.to_seq @@ within "(" ")" @@ hvbox @@ seq pp_pairs map Var_map.to_seq @@ within "(" ")" @@ hvbox @@ seq pp_pairs
@ -668,16 +704,18 @@ module Make_full_for_expr(V : VAR_GEN)
type constr = L.Constr.t type constr = L.Constr.t
(* add a constraint *) (* add a constraint *)
let add_constr (t:t) (c:constr) : unit = let add_constr (t:t) (c:constr) (reason:lit) : unit =
let (x:var) = V.Fresh.fresh t.param in let (x:var) = V.Fresh.fresh t.param in
let e, op, q = L.Constr.split c in let e, op, q = L.Constr.split c in
add_eq t (x, L.Comb.to_list e); add_eq t (x, L.Comb.to_list e);
begin match op with begin match op with
| Leq -> add_upper_bound t ~strict:false x q | Leq -> add_upper_bound t ~strict:false ~reason x q
| Geq -> add_lower_bound t ~strict:false x q | Geq -> add_lower_bound t ~strict:false ~reason x q
| Lt -> add_upper_bound t ~strict:true x q | Lt -> add_upper_bound t ~strict:true ~reason x q
| Gt -> add_lower_bound t ~strict:true x q | Gt -> add_lower_bound t ~strict:true ~reason x q
| Eq -> add_bounds t ~strict_lower:false ~strict_upper:false (x,q,q) | Eq -> add_bounds t (x,q,q)
~strict_lower:false ~strict_upper:false
~lower_reason:reason ~upper_reason:reason
| Neq -> assert false | Neq -> assert false
end end
end end

16
src/arith/lra/simplex_intf.ml
View file

@ -35,7 +35,6 @@ module type S = sig
type cert = { type cert = {
cert_var: var; cert_var: var;
cert_expr: (Q.t * var) list; cert_expr: (Q.t * var) list;
cert_core: lit list;
} }
(** Generic type returned when solving the simplex. A solution is a list of (** Generic type returned when solving the simplex. A solution is a list of
@ -66,11 +65,14 @@ module type S = sig
[Q.inf]. [Q.inf].
Optional parameters allow to make the the bounds strict. Defaults to false, Optional parameters allow to make the the bounds strict. Defaults to false,
so that bounds are large by default. *) so that bounds are large by default. *)
val add_bounds : t -> ?strict_lower:bool -> ?strict_upper:bool -> var * Q.t * Q.t -> unit val add_bounds : t ->
?strict_lower:bool -> ?strict_upper:bool ->
?lower_reason:lit -> ?upper_reason:lit ->
var * Q.t * Q.t -> unit
val add_lower_bound : t -> ?strict:bool -> var -> Q.t -> unit val add_lower_bound : t -> ?strict:bool -> reason:lit -> var -> Q.t -> unit
val add_upper_bound : t -> ?strict:bool -> var -> Q.t -> unit val add_upper_bound : t -> ?strict:bool -> reason:lit -> var -> Q.t -> unit
(** {3 Simplex solving} *) (** {3 Simplex solving} *)
@ -85,10 +87,10 @@ module type S = sig
val check_cert : val check_cert :
t -> t ->
cert -> cert ->
[`Ok | `Bad_bounds of string * string | `Diff_not_0 of Q.t Var_map.t] [`Ok of lit list | `Bad_bounds of string * string | `Diff_not_0 of Q.t Var_map.t]
(** checks that the certificat indeed yields to a contradiction (** checks that the certificat indeed yields to a contradiction
in the current state of the simplex. in the current state of the simplex.
@return [`Ok] if the certificate is valid. *) @return [`Ok unsat_core] if the certificate is valid. *)
(* TODO: push/pop? at least on bounds *) (* TODO: push/pop? at least on bounds *)
@ -119,6 +121,6 @@ module type S_FULL = sig
type constr = L.Constr.t type constr = L.Constr.t
val add_constr : t -> constr -> unit val add_constr : t -> constr -> lit -> unit
(** Add a constraint to a simplex state. *) (** Add a constraint to a simplex state. *)
end end

8
src/arith/tests/test_simplex.ml
View file

@ -107,7 +107,11 @@ module Problem = struct
QC.list_of_size QC.Gen.(m -- n) @@ Constr.rand 10 QC.list_of_size QC.Gen.(m -- n) @@ Constr.rand 10
end end
let add_problem (t:Spl.t) (pb:Problem.t) : unit = List.iter (Spl.add_constr t) pb let add_problem (t:Spl.t) (pb:Problem.t) : unit =
(* TODO: use an arbitrary litteral if the tests do not check the unsat core,
or else add litterals to the generated problem. *)
let lit = assert false in
List.iter (fun constr -> Spl.add_constr t constr lit) pb
let pp_subst : subst Fmt.printer = let pp_subst : subst Fmt.printer =
Fmt.(map Spl.L.Var_map.to_seq @@ Fmt.(map Spl.L.Var_map.to_seq @@
@ -150,7 +154,7 @@ let check_sound =
) )
| Spl.Unsatisfiable cert -> | Spl.Unsatisfiable cert ->
begin match Spl.check_cert simplex cert with begin match Spl.check_cert simplex cert with
| `Ok -> true | `Ok _ -> true
| `Bad_bounds (low, up) -> | `Bad_bounds (low, up) ->
QC.Test.fail_reportf QC.Test.fail_reportf
"(@[<hv>bad-certificat@ :problem %a@ :cert %a@ :low %s :up %s@ :simplex-after %a@ :simplex-before %a@])" "(@[<hv>bad-certificat@ :problem %a@ :cert %a@ :low %s :up %s@ :simplex-after %a@ :simplex-before %a@])"