mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
fix more warnings; remove never completed LIA stuff
This commit is contained in:
Simon Cruanes
parent
fd500a3d7d
commit
e2b9b2874c
19 changed files with 21 additions and 1275 deletions
|
|
@ -1,9 +1,9 @@
|
|||
(library
|
||||
(name sidekick_base_solver)
|
||||
(public_name sidekick-base.solver)
|
||||
(synopsis "Instantiation of solver and theories for Sidekick_base")
|
||||
(libraries sidekick-base sidekick.core sidekick.smt-solver
|
||||
sidekick.th-bool-static
|
||||
sidekick.mini-cc sidekick.th-data
|
||||
sidekick.arith-lra sidekick.arith-lia sidekick.zarith)
|
||||
(flags :standard -warn-error -a+8 -safe-string -color always -open Sidekick_util))
|
||||
(name sidekick_base_solver)
|
||||
(public_name sidekick-base.solver)
|
||||
(synopsis "Instantiation of solver and theories for Sidekick_base")
|
||||
(libraries sidekick-base sidekick.core sidekick.smt-solver
|
||||
sidekick.th-bool-static sidekick.mini-cc sidekick.th-data
|
||||
sidekick.arith-lra sidekick.zarith)
|
||||
(flags :standard -warn-error -a+8 -safe-string -color always -open
|
||||
Sidekick_util))
|
||||
|
|
|
|||
|
|
@ -136,49 +136,6 @@ module Th_lra = Sidekick_arith_lra.Make(struct
|
|||
module Gensym = Gensym
|
||||
end)
|
||||
|
||||
module Th_lia = Sidekick_arith_lia.Make(struct
|
||||
module S = Solver
|
||||
module T = Term
|
||||
module Z = Sidekick_zarith.Int
|
||||
module Q = Sidekick_zarith.Rational
|
||||
type term = S.T.Term.t
|
||||
type ty = S.T.Ty.t
|
||||
|
||||
module LIA = Sidekick_arith_lia
|
||||
module LRA_solver = Th_lra
|
||||
|
||||
let mk_eq = Form.eq
|
||||
let mk_lia store l = match l with
|
||||
| LIA.LIA_other x -> x
|
||||
| LIA.LIA_pred (p, x, y) -> T.lia store (Pred(p,x,y))
|
||||
| LIA.LIA_op (op, x, y) -> T.lia store (Op(op,x,y))
|
||||
| LIA.LIA_const c -> T.lia store (Const c)
|
||||
| LIA.LIA_mult (c,x) -> T.lia store (Mult (c,x))
|
||||
let mk_bool = T.bool
|
||||
let mk_to_real store t = T.lra store (To_real t)
|
||||
|
||||
let view_as_lia t = match T.view t with
|
||||
| T.LIA l ->
|
||||
let module LIA = Sidekick_arith_lia in
|
||||
begin match l with
|
||||
| Const c -> LIA.LIA_const c
|
||||
| Pred (p,a,b) -> LIA.LIA_pred(p,a,b)
|
||||
| Op(op,a,b) -> LIA.LIA_op(op,a,b)
|
||||
| Mult (c,x) -> LIA.LIA_mult (c,x)
|
||||
| Var x -> LIA.LIA_other x
|
||||
end
|
||||
| T.Eq (a,b) when Ty.equal (T.ty a) (Ty.int()) ->
|
||||
LIA.LIA_pred (Eq, a, b)
|
||||
| _ -> LIA.LIA_other t
|
||||
|
||||
let ty_int _st = Ty.int()
|
||||
let has_ty_int t = Ty.equal (T.ty t) (Ty.int())
|
||||
|
||||
let lemma_lia = Proof.lemma_lia
|
||||
let lemma_relax_to_lra = Proof.lemma_relax_to_lra
|
||||
end)
|
||||
|
||||
let th_bool : Solver.theory = Th_bool.theory
|
||||
let th_data : Solver.theory = Th_data.theory
|
||||
let th_lra : Solver.theory = Th_lra.theory
|
||||
let th_lia : Solver.theory = Th_lia.theory
|
||||
|
|
|
|||
|
|
@ -1032,7 +1032,6 @@ end = struct
|
|||
|
||||
type store = {
|
||||
tbl : H.t;
|
||||
mutable n: int;
|
||||
true_ : t lazy_t;
|
||||
false_ : t lazy_t;
|
||||
}
|
||||
|
|
@ -1051,7 +1050,6 @@ end = struct
|
|||
|
||||
let create ?(size=1024) () : store =
|
||||
let rec st ={
|
||||
n=2;
|
||||
tbl=H.create ~size ();
|
||||
true_ = lazy (make st Term_cell.true_);
|
||||
false_ = lazy (make st Term_cell.false_);
|
||||
|
|
|
|||
|
|
@ -1,6 +0,0 @@
|
|||
(library
|
||||
(name sidekick_intsolver)
|
||||
(public_name sidekick.intsolver)
|
||||
(synopsis "Simple integer solver")
|
||||
(flags :standard -warn-error -a+8 -w -32 -open Sidekick_util)
|
||||
(libraries containers sidekick.core sidekick.arith))
|
||||
|
|
@ -1,633 +0,0 @@
|
|||
|
||||
module type ARG = sig
|
||||
module Z : Sidekick_arith.INT_FULL
|
||||
|
||||
type term
|
||||
type lit
|
||||
|
||||
val pp_term : term Fmt.printer
|
||||
val pp_lit : lit Fmt.printer
|
||||
|
||||
module T_map : CCMap.S with type key = term
|
||||
end
|
||||
|
||||
module type S = sig
|
||||
module A : ARG
|
||||
|
||||
module Op : sig
|
||||
type t =
|
||||
| Leq
|
||||
| Lt
|
||||
| Eq
|
||||
val pp : t Fmt.printer
|
||||
end
|
||||
|
||||
type t
|
||||
|
||||
val create : unit -> t
|
||||
|
||||
val push_level : t -> unit
|
||||
|
||||
val pop_levels : t -> int -> unit
|
||||
|
||||
val assert_ :
|
||||
t ->
|
||||
(A.Z.t * A.term) list -> Op.t -> A.Z.t ->
|
||||
lit:A.lit ->
|
||||
unit
|
||||
|
||||
val define :
|
||||
t ->
|
||||
A.term ->
|
||||
(A.Z.t * A.term) list ->
|
||||
unit
|
||||
|
||||
module Cert : sig
|
||||
type t
|
||||
val pp : t Fmt.printer
|
||||
|
||||
val lits : t -> A.lit Iter.t
|
||||
end
|
||||
|
||||
module Model : sig
|
||||
type t
|
||||
val pp : t Fmt.printer
|
||||
|
||||
val eval : t -> A.term -> A.Z.t option
|
||||
end
|
||||
|
||||
type result =
|
||||
| Sat of Model.t
|
||||
| Unsat of Cert.t
|
||||
|
||||
val pp_result : result Fmt.printer
|
||||
|
||||
val check : t -> result
|
||||
|
||||
(**/**)
|
||||
val _check_invariants : t -> unit
|
||||
(**/**)
|
||||
end
|
||||
|
||||
|
||||
|
||||
module Make(A : ARG)
|
||||
: S with module A = A
|
||||
= struct
|
||||
module BVec = Backtrack_stack
|
||||
module A = A
|
||||
open A
|
||||
|
||||
module ZTbl = CCHashtbl.Make(Z)
|
||||
|
||||
module Utils_ : sig
|
||||
type divisor = {
|
||||
prime : Z.t;
|
||||
power : int;
|
||||
}
|
||||
val is_prime : Z.t -> bool
|
||||
val prime_decomposition : Z.t -> divisor list
|
||||
val primes_leq : Z.t -> Z.t Iter.t
|
||||
end = struct
|
||||
|
||||
type divisor = {
|
||||
prime : Z.t;
|
||||
power : int;
|
||||
}
|
||||
|
||||
let two = Z.of_int 2
|
||||
|
||||
(* table from numbers to some of their divisor (if any) *)
|
||||
let _table = lazy (
|
||||
let t = ZTbl.create 256 in
|
||||
ZTbl.add t two None;
|
||||
t)
|
||||
|
||||
let _divisors n = ZTbl.find (Lazy.force _table) n
|
||||
|
||||
let _add_prime n =
|
||||
ZTbl.replace (Lazy.force _table) n None
|
||||
|
||||
(* add to the table the fact that [d] is a divisor of [n] *)
|
||||
let _add_divisor n d =
|
||||
assert (not (ZTbl.mem (Lazy.force _table) n));
|
||||
ZTbl.add (Lazy.force _table) n (Some d)
|
||||
|
||||
(* primality test, modifies _table *)
|
||||
let _is_prime n0 =
|
||||
let n = ref two in
|
||||
let bound = Z.succ (Z.sqrt n0) in
|
||||
let is_prime = ref true in
|
||||
while !is_prime && Z.(!n <= bound) do
|
||||
if Z.(rem n0 !n = zero)
|
||||
then begin
|
||||
is_prime := false;
|
||||
_add_divisor n0 !n;
|
||||
end;
|
||||
n := Z.succ !n;
|
||||
done;
|
||||
if !is_prime then _add_prime n0;
|
||||
!is_prime
|
||||
|
||||
let is_prime n =
|
||||
try
|
||||
begin match _divisors n with
|
||||
| None -> true
|
||||
| Some _ -> false
|
||||
end
|
||||
with Not_found ->
|
||||
if Z.probab_prime n && _is_prime n then (
|
||||
_add_prime n; true
|
||||
) else false
|
||||
|
||||
let rec _merge l1 l2 = match l1, l2 with
|
||||
| [], _ -> l2
|
||||
| _, [] -> l1
|
||||
| p1::l1', p2::l2' ->
|
||||
match Z.compare p1.prime p2.prime with
|
||||
| 0 ->
|
||||
{prime=p1.prime; power=p1.power+p2.power} :: _merge l1' l2'
|
||||
| n when n < 0 ->
|
||||
p1 :: _merge l1' l2
|
||||
| _ -> p2 :: _merge l1 l2'
|
||||
|
||||
let rec _decompose n =
|
||||
try
|
||||
begin match _divisors n with
|
||||
| None -> [{prime=n; power=1;}]
|
||||
| Some q1 ->
|
||||
let q2 = Z.divexact n q1 in
|
||||
_merge (_decompose q1) (_decompose q2)
|
||||
end
|
||||
with Not_found ->
|
||||
ignore (_is_prime n);
|
||||
_decompose n
|
||||
|
||||
let prime_decomposition n =
|
||||
if is_prime n
|
||||
then [{prime=n; power=1;}]
|
||||
else _decompose n
|
||||
|
||||
let primes_leq n0 k =
|
||||
let n = ref two in
|
||||
while Z.(!n <= n0) do
|
||||
if is_prime !n then k !n
|
||||
done
|
||||
end [@@warning "-60"]
|
||||
|
||||
|
||||
module Op = struct
|
||||
type t =
|
||||
| Leq
|
||||
| Lt
|
||||
| Eq
|
||||
|
||||
let pp out = function
|
||||
| Leq -> Fmt.string out "<="
|
||||
| Lt -> Fmt.string out "<"
|
||||
| Eq -> Fmt.string out "="
|
||||
end
|
||||
|
||||
module Linexp = struct
|
||||
type t = Z.t T_map.t
|
||||
let is_empty = T_map.is_empty
|
||||
let empty : t = T_map.empty
|
||||
|
||||
let pp out (self:t) : unit =
|
||||
let pp_pair out (t,z) =
|
||||
if Z.(z = one) then A.pp_term out t
|
||||
else Fmt.fprintf out "%a · %a" Z.pp z A.pp_term t in
|
||||
if is_empty self then Fmt.string out "0"
|
||||
else Fmt.fprintf out "(@[%a@])"
|
||||
Fmt.(iter ~sep:(return "@ + ") pp_pair) (T_map.to_iter self)
|
||||
|
||||
let iter = T_map.iter
|
||||
let return t : t = T_map.add t Z.one empty
|
||||
let neg self : t = T_map.map Z.neg self
|
||||
let mem self t : bool = T_map.mem t self
|
||||
let remove self t = T_map.remove t self
|
||||
let find_exn self t = T_map.find t self
|
||||
let mult n self =
|
||||
if Z.(n = zero) then empty
|
||||
else T_map.map (fun c -> Z.(c * n)) self
|
||||
|
||||
let add (self:t) (c:Z.t) (t:term) : t =
|
||||
let n = Z.(c + T_map.get_or ~default:Z.zero t self) in
|
||||
if Z.(n = zero)
|
||||
then T_map.remove t self
|
||||
else T_map.add t n self
|
||||
|
||||
let merge (self:t) (other:t) : t =
|
||||
T_map.fold
|
||||
(fun t c m -> add m c t)
|
||||
other self
|
||||
|
||||
let of_list l : t =
|
||||
List.fold_left (fun self (c,t) -> add self c t) empty l
|
||||
|
||||
(* map each term to a linexp *)
|
||||
let flat_map f (self:t) : t =
|
||||
T_map.fold
|
||||
(fun t c m ->
|
||||
let t_le = mult c (f t) in
|
||||
merge m t_le
|
||||
)
|
||||
self empty
|
||||
|
||||
let (+) = merge
|
||||
let ( * ) = mult
|
||||
let ( ~- ) = neg
|
||||
let (-) a b = a + ~- b
|
||||
end
|
||||
|
||||
module Cert = struct
|
||||
type t = unit
|
||||
let pp = Fmt.unit
|
||||
|
||||
let lits _ = Iter.empty (* TODO *)
|
||||
end
|
||||
|
||||
module Model = struct
|
||||
type t = {
|
||||
m: Z.t T_map.t;
|
||||
} [@@unboxed]
|
||||
|
||||
let pp out self =
|
||||
let pp_pair out (t,z) = Fmt.fprintf out "(@[%a := %a@])" A.pp_term t Z.pp z in
|
||||
Fmt.fprintf out "(@[model@ %a@])"
|
||||
Fmt.(iter ~sep:(return "@ ") pp_pair) (T_map.to_iter self.m)
|
||||
|
||||
let empty : t = {m=T_map.empty}
|
||||
|
||||
let eval (self:t) t : Z.t option = T_map.get t self.m
|
||||
end
|
||||
|
||||
module Constr = struct
|
||||
type t = {
|
||||
le: Linexp.t;
|
||||
const: Z.t;
|
||||
op: Op.t;
|
||||
lits: lit Bag.t;
|
||||
}
|
||||
|
||||
(* FIXME: need to simplify: compute gcd(le.coeffs), then divide by that
|
||||
and round const appropriately *)
|
||||
|
||||
let pp out self =
|
||||
Fmt.fprintf out "(@[%a@ %a %a@])" Linexp.pp self.le Op.pp self.op Z.pp self.const
|
||||
end
|
||||
|
||||
type t = {
|
||||
defs: (term * Linexp.t) BVec.t;
|
||||
cs: Constr.t BVec.t;
|
||||
}
|
||||
|
||||
let create() : t =
|
||||
{ defs=BVec.create();
|
||||
cs=BVec.create(); }
|
||||
|
||||
let push_level self =
|
||||
BVec.push_level self.defs;
|
||||
BVec.push_level self.cs;
|
||||
()
|
||||
|
||||
let pop_levels self n =
|
||||
BVec.pop_levels self.defs n ~f:(fun _ -> ());
|
||||
BVec.pop_levels self.cs n ~f:(fun _ -> ());
|
||||
()
|
||||
|
||||
type result =
|
||||
| Sat of Model.t
|
||||
| Unsat of Cert.t
|
||||
|
||||
let pp_result out = function
|
||||
| Sat m -> Fmt.fprintf out "(@[SAT@ %a@])" Model.pp m
|
||||
| Unsat cert -> Fmt.fprintf out "(@[UNSAT@ %a@])" Cert.pp cert
|
||||
|
||||
let assert_ (self:t) l op c ~lit : unit =
|
||||
let le = Linexp.of_list l in
|
||||
let c = {Constr.le; const=c; op; lits=Bag.return lit} in
|
||||
Log.debugf 15 (fun k->k "(@[sidekick.intsolver.assert@ %a@])" Constr.pp c);
|
||||
BVec.push self.cs c
|
||||
|
||||
(* TODO: check before hand that [t] occurs nowhere else *)
|
||||
let define (self:t) t l : unit =
|
||||
let le = Linexp.of_list l in
|
||||
BVec.push self.defs (t,le)
|
||||
|
||||
(* #### checking #### *)
|
||||
|
||||
module Check_ = struct
|
||||
module LE = Linexp
|
||||
|
||||
type op =
|
||||
| Leq
|
||||
| Eq
|
||||
| Eq_mod of {
|
||||
prime: Z.t;
|
||||
pow: int;
|
||||
} (* modulo prime^pow *)
|
||||
|
||||
let pp_op out = function
|
||||
| Leq -> Fmt.string out "<="
|
||||
| Eq -> Fmt.string out "="
|
||||
| Eq_mod {prime; pow} -> Fmt.fprintf out "%a^%d" Z.pp prime pow
|
||||
|
||||
type constr = {
|
||||
le: LE.t;
|
||||
const: Z.t;
|
||||
op: op;
|
||||
lits: lit Bag.t;
|
||||
}
|
||||
|
||||
let pp_constr out self =
|
||||
Fmt.fprintf out "(@[%a@ %a %a@])" Linexp.pp self.le pp_op self.op Z.pp self.const
|
||||
|
||||
type state = {
|
||||
mutable rw: LE.t T_map.t; (* rewrite rules *)
|
||||
mutable vars: int T_map.t; (* variables in at least one constraint *)
|
||||
mutable constrs: constr list;
|
||||
mutable ok: (unit, constr) Result.t;
|
||||
}
|
||||
(* main solving state. mutable, but copied for backtracking.
|
||||
invariant: variables in [rw] do not occur anywhere else
|
||||
*)
|
||||
|
||||
let[@inline] is_ok_ self = CCResult.is_ok self.ok
|
||||
|
||||
(* perform rewriting on the linear expression *)
|
||||
let rec norm_le (self:state) (le:LE.t) : LE.t =
|
||||
LE.flat_map
|
||||
(fun t ->
|
||||
begin match T_map.find t self.rw with
|
||||
| le -> norm_le self le
|
||||
| exception Not_found -> LE.return t
|
||||
end)
|
||||
le
|
||||
|
||||
let[@inline] count_v self t : int = T_map.get_or ~default:0 t self.vars
|
||||
|
||||
let[@inline] incr_v (self:state) (t:term) : unit =
|
||||
self.vars <- T_map.add t (1 + count_v self t) self.vars
|
||||
|
||||
(* GCD of the coefficients of this linear expression *)
|
||||
let gcd_coeffs (le:LE.t) : Z.t =
|
||||
match T_map.choose_opt le with
|
||||
| None -> Z.one
|
||||
| Some (_, z0) -> T_map.fold (fun _ z m -> Z.gcd z m) le z0
|
||||
|
||||
let decr_v (self:state) (t:term) : unit =
|
||||
let n = count_v self t - 1 in
|
||||
assert (n >= 0);
|
||||
self.vars <-
|
||||
(if n=0 then T_map.remove t self.vars
|
||||
else T_map.add t n self.vars)
|
||||
|
||||
let simplify_constr (c:constr) : (constr, unit) Result.t =
|
||||
let exception E_unsat in
|
||||
try
|
||||
match T_map.choose_opt c.le with
|
||||
| None -> Ok c
|
||||
| Some (_, z0) ->
|
||||
let c_gcd = T_map.fold (fun _ z m -> Z.gcd z m) c.le z0 in
|
||||
if Z.(c_gcd > one) then (
|
||||
let const = match c.op with
|
||||
| Leq ->
|
||||
(* round down, regardless of sign *)
|
||||
Z.ediv c.const c_gcd
|
||||
| Eq | Eq_mod _ ->
|
||||
if Z.equal (Z.rem c.const c_gcd) Z.zero then (
|
||||
(* compatible constant *)
|
||||
Z.(divexact c.const c_gcd)
|
||||
) else (
|
||||
raise E_unsat
|
||||
)
|
||||
in
|
||||
|
||||
let c' = {
|
||||
c with
|
||||
le=T_map.map (fun c -> Z.(c / c_gcd)) c.le;
|
||||
const;
|
||||
} in
|
||||
Log.debugf 50
|
||||
(fun k->k "(@[intsolver.simplify@ :from %a@ :into %a@])"
|
||||
pp_constr c pp_constr c');
|
||||
Ok c'
|
||||
) else Ok c
|
||||
with E_unsat ->
|
||||
Log.debugf 50 (fun k->k "(@[intsolver.simplify.unsat@ %a@])" pp_constr c);
|
||||
Error ()
|
||||
|
||||
let add_constr (self:state) (c:constr) : unit =
|
||||
if is_ok_ self then (
|
||||
let c = {c with le=norm_le self c.le } in
|
||||
match simplify_constr c with
|
||||
| Ok c ->
|
||||
Log.debugf 50 (fun k->k "(@[intsolver.add-constr@ %a@])" pp_constr c);
|
||||
LE.iter (fun t _ -> incr_v self t) c.le;
|
||||
self.constrs <- c :: self.constrs
|
||||
| Error () ->
|
||||
self.ok <- Error c
|
||||
)
|
||||
|
||||
let remove_constr (self:state) (c:constr) : unit =
|
||||
LE.iter (fun t _ -> decr_v self t) c.le
|
||||
|
||||
let create (self:t) : state =
|
||||
let state = {
|
||||
vars=T_map.empty;
|
||||
rw=T_map.empty;
|
||||
constrs=[];
|
||||
ok=Ok();
|
||||
} in
|
||||
BVec.iter self.defs
|
||||
~f:(fun (v,le) ->
|
||||
assert (not (T_map.mem v state.rw));
|
||||
(* normalize as much as we can now *)
|
||||
let le = norm_le state le in
|
||||
Log.debugf 50 (fun k->k "(@[intsolver.add-rw %a@ := %a@])" pp_term v LE.pp le);
|
||||
state.rw <- T_map.add v le state.rw);
|
||||
BVec.iter self.cs
|
||||
~f:(fun (c:Constr.t) ->
|
||||
let {Constr.le; op; const; lits} = c in
|
||||
let op, const = match op with
|
||||
| Op.Eq -> Eq, const
|
||||
| Op.Leq -> Leq, const
|
||||
| Op.Lt -> Leq, Z.pred const (* [x < t] is [x <= t-1] *)
|
||||
in
|
||||
let c = {le;const;lits;op} in
|
||||
add_constr state c
|
||||
);
|
||||
state
|
||||
|
||||
let rec solve_rec (self:state) : result =
|
||||
begin match T_map.choose_opt self.vars with
|
||||
| None ->
|
||||
let m = Model.empty in
|
||||
Sat m (* TODO: model *)
|
||||
|
||||
| Some (t, _) -> elim_var_ self t
|
||||
end
|
||||
|
||||
|
||||
and elim_var_ self (x:term) : result =
|
||||
Log.debugf 20
|
||||
(fun k->k "(@[@{<Yellow>intsolver.elim-var@}@ %a@ :remaining %d@])"
|
||||
A.pp_term x (T_map.cardinal self.vars));
|
||||
|
||||
assert (not (T_map.mem x self.rw)); (* would have been rewritten away *)
|
||||
self.vars <- T_map.remove x self.vars;
|
||||
|
||||
(* gather the sets *)
|
||||
let set_e = ref [] in (* eqns *)
|
||||
let set_l = ref [] in (* t <= … *)
|
||||
let set_g = ref [] in (* t >= … *)
|
||||
let set_m = ref [] in (* t = … [n] *)
|
||||
let others = ref [] in
|
||||
|
||||
let classify_constr (c:constr) =
|
||||
match T_map.get x c.le, c.op with
|
||||
| None, _ ->
|
||||
others := c :: !others;
|
||||
| Some n_t, Leq ->
|
||||
if Z.sign n_t > 0 then
|
||||
set_l := (n_t,c) :: !set_l
|
||||
else
|
||||
set_g := (n_t,c) :: !set_g
|
||||
| Some n_t, Eq ->
|
||||
set_e := (n_t,c) :: !set_e
|
||||
| Some n_t, Eq_mod _ ->
|
||||
set_m := (n_t,c) :: !set_m
|
||||
in
|
||||
|
||||
List.iter classify_constr self.constrs;
|
||||
self.constrs <- !others; (* remove all constraints involving [t] *)
|
||||
|
||||
Log.debugf 50
|
||||
(fun k->
|
||||
let pps = Fmt.Dump.(list @@ pair Z.pp pp_constr) in
|
||||
k "(@[intsolver.classify.for %a@ E=%a@ L=%a@ G=%a@ M=%a@])"
|
||||
A.pp_term x pps !set_e pps !set_l pps !set_g pps !set_m);
|
||||
|
||||
(* now apply the algorithm *)
|
||||
if !set_e <> [] then (
|
||||
(* case (a): eliminate via an equality. *)
|
||||
|
||||
(* pick an equality with a small coeff, if possible *)
|
||||
let coeff1, c1 =
|
||||
Iter.of_list !set_e
|
||||
|> Iter.min_exn ~lt:(fun (n1,_)(n2,_) -> Z.(abs n1 < abs n2))
|
||||
in
|
||||
|
||||
let le1 = LE.(neg @@ remove c1.le x) in
|
||||
|
||||
Log.debugf 30
|
||||
(fun k->k "(@[intsolver.case_a.eqn@ :coeff %a@ :c %a@])"
|
||||
Z.pp coeff1 pp_constr c1);
|
||||
|
||||
let elim_in_constr (coeff2, c2) =
|
||||
let le2 = LE.(neg @@ remove c2.le x) in
|
||||
|
||||
let gcd12 = Z.gcd coeff1 coeff2 in
|
||||
(* coeff1 × p1 = coeff2 × p2 = lcm = coeff1 × coeff2 / gcd,
|
||||
because coeff1 × coeff2 = lcm × gcd *)
|
||||
let lcm12 = Z.(abs coeff1 * abs coeff2 / gcd12) in
|
||||
let p1 = Z.(lcm12 / coeff1) in
|
||||
let p2 = Z.(lcm12 / coeff2) in
|
||||
Log.debugf 50
|
||||
(fun k->k "(@[intsolver.elim-in-constr@ %a@ :gcd %a :lcm %a@ :p1 %a :p2 %a@])"
|
||||
pp_constr c2 Z.pp gcd12 Z.pp lcm12 Z.pp p1 Z.pp p2);
|
||||
|
||||
let c' =
|
||||
let lits = Bag.append c1.lits c2.lits in
|
||||
if Z.sign coeff1 <> Z.sign coeff2 then (
|
||||
let le' = LE.(p1 * le1 + p2 * le2) in
|
||||
let const' = Z.(p1 * c1.const + p2 * c2.const) in
|
||||
{op=c2.op; le=le'; const=const'; lits}
|
||||
) else (
|
||||
let le' = LE.(p1 * le1 - p2 * le2) in
|
||||
let const' = Z.(p1 * c1.const - p2 * c2.const) in
|
||||
let le', const' =
|
||||
if Z.sign coeff1 < 0 then LE.neg le', Z.neg const'
|
||||
else le', const'
|
||||
in
|
||||
{op=c2.op; le=le'; const=const'; lits}
|
||||
)
|
||||
in
|
||||
add_constr self c'
|
||||
|
||||
(* also add a divisibility constraint if needed *)
|
||||
(* TODO:
|
||||
if Z.(p1 > one) then (
|
||||
let c' = {le=le2; op=Eq_mod p1; const=c2.const} in
|
||||
add_constr self c'
|
||||
)
|
||||
*)
|
||||
in
|
||||
List.iter elim_in_constr !set_l;
|
||||
List.iter elim_in_constr !set_g;
|
||||
List.iter elim_in_constr !set_m;
|
||||
|
||||
(* FIXME: handle the congruence *)
|
||||
) else if !set_l = [] || !set_g = [] then (
|
||||
(* case (b): no bound on at least one side *)
|
||||
assert (!set_e=[]);
|
||||
|
||||
() (* FIXME: handle the congruence *)
|
||||
) else (
|
||||
(* case (c): combine inequalities pairwise *)
|
||||
|
||||
let elim_pair (coeff1, c1) (coeff2, c2) : unit =
|
||||
assert (Z.sign coeff1 > 0 && Z.sign coeff2 < 0);
|
||||
|
||||
let le1 = LE.remove c1.le x in
|
||||
let le2 = LE.remove c2.le x in
|
||||
|
||||
let gcd12 = Z.gcd coeff1 coeff2 in
|
||||
let lcm12 = Z.(coeff1 * abs coeff2 / gcd12) in
|
||||
|
||||
let p1 = Z.(lcm12 / coeff1) in
|
||||
let p2 = Z.(lcm12 / Z.abs coeff2) in
|
||||
|
||||
Log.debugf 50
|
||||
(fun k->k "(@[intsolver.case-b.elim-pair@ L=%a@ G=%a@ \
|
||||
:gcd %a :lcm %a@ :p1 %a :p2 %a@])"
|
||||
pp_constr c1 pp_constr c2 Z.pp gcd12 Z.pp lcm12 Z.pp p1 Z.pp p2);
|
||||
|
||||
let new_ineq =
|
||||
let le = LE.(p2 * le1 - p1 * le2) in
|
||||
let const = Z.(p2 * c1.const - p1 * c2.const) in
|
||||
let lits = Bag.append c1.lits c2.lits in
|
||||
{op=Leq; le; const; lits}
|
||||
in
|
||||
|
||||
add_constr self new_ineq;
|
||||
(* TODO: handle modulo constraints *)
|
||||
|
||||
in
|
||||
|
||||
List.iter (fun x1 -> List.iter (elim_pair x1) !set_g) !set_l;
|
||||
);
|
||||
|
||||
(* now recurse *)
|
||||
solve_rec self
|
||||
end
|
||||
|
||||
let check (self:t) : result =
|
||||
|
||||
Log.debugf 10 (fun k->k "(@[@{<Yellow>intsolver.check@}@])");
|
||||
let state = Check_.create self in
|
||||
Log.debugf 10
|
||||
(fun k->k "(@[intsolver.check.stat@ :n-vars %d@ :n-constr %d@])"
|
||||
(T_map.cardinal state.vars) (List.length state.constrs));
|
||||
|
||||
match state.ok with
|
||||
| Ok () ->
|
||||
Check_.solve_rec state
|
||||
| Error c ->
|
||||
Log.debugf 10 (fun k->k "(@[insolver.unsat-constraint@ %a@])" Check_.pp_constr c);
|
||||
(* TODO proper certificate *)
|
||||
Unsat ()
|
||||
|
||||
let _check_invariants _ = ()
|
||||
end
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
|
||||
(library
|
||||
(name sidekick_test_intsolver)
|
||||
(libraries zarith sidekick.intsolver sidekick.util sidekick.zarith
|
||||
qcheck alcotest))
|
||||
|
|
@ -1,346 +0,0 @@
|
|||
|
||||
open CCMonomorphic
|
||||
|
||||
module Fmt = CCFormat
|
||||
module QC = QCheck
|
||||
module Log = Sidekick_util.Log
|
||||
let spf = Printf.sprintf
|
||||
|
||||
module ZarithZ = Z
|
||||
module Z = Sidekick_zarith.Int
|
||||
|
||||
module Var = struct
|
||||
include CCInt
|
||||
|
||||
let pp out x = Format.fprintf out "X_%d" x
|
||||
|
||||
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 Var_map = CCMap.Make(Var)
|
||||
|
||||
module Solver = Sidekick_intsolver.Make(struct
|
||||
module Z = Z
|
||||
type term = Var.t
|
||||
let pp_term = Var.pp
|
||||
type lit = Var.lit
|
||||
let pp_lit = Var.pp_lit
|
||||
module T_map = Var_map
|
||||
end)
|
||||
|
||||
let unwrap_opt_ msg = function
|
||||
| Some x -> x
|
||||
| None -> failwith msg
|
||||
|
||||
let rand_n low n : Z.t QC.arbitrary =
|
||||
QC.map ~rev:ZarithZ.to_int Z.of_int QC.(low -- n)
|
||||
|
||||
(* TODO: fudge *)
|
||||
let rand_z = rand_n (-15) 15
|
||||
|
||||
module Step = struct
|
||||
module G = QC.Gen
|
||||
|
||||
type linexp = (Z.t * Var.t) list
|
||||
|
||||
type t =
|
||||
| S_new_var of Var.t
|
||||
| S_define of Var.t * (Z.t * Var.t) list
|
||||
| S_leq of linexp * Z.t
|
||||
| S_lt of linexp * Z.t
|
||||
| S_eq of linexp * Z.t
|
||||
|
||||
let pp_le out (le:linexp) =
|
||||
let pp_pair out (n,x) =
|
||||
if Z.equal Z.one n then Var.pp out x
|
||||
else Fmt.fprintf out "%a . %a" Z.pp n Var.pp x in
|
||||
Fmt.fprintf out "(@[%a@])"
|
||||
Fmt.(list ~sep:(return " +@ ") pp_pair) le
|
||||
|
||||
let pp_ out = function
|
||||
| S_new_var v -> Fmt.fprintf out "(@[new-var %a@])" Var.pp v
|
||||
| S_define (v,le) -> Fmt.fprintf out "(@[define %a@ := %a@])" Var.pp v pp_le le
|
||||
| S_leq (le,n) -> Fmt.fprintf out "(@[upper %a <= %a@])" pp_le le Z.pp n
|
||||
| S_lt (le,n) -> Fmt.fprintf out "(@[upper %a < %a@])" pp_le le Z.pp n
|
||||
| S_eq (le,n) -> Fmt.fprintf out "(@[lower %a > %a@])" pp_le le Z.pp n
|
||||
|
||||
(* check that a sequence is well formed *)
|
||||
let well_formed (l:t list) : bool =
|
||||
let rec aux vars = function
|
||||
| [] -> true
|
||||
| S_new_var v :: tl ->
|
||||
not (List.mem v vars) && aux (v::vars) tl
|
||||
| (S_leq (le,_) | S_lt (le,_) | S_eq (le,_)) :: tl ->
|
||||
List.for_all (fun (_,x) -> List.mem x vars) le && aux vars tl
|
||||
| S_define (x,le) :: tl->
|
||||
not (List.mem x vars) &&
|
||||
List.for_all (fun (_,y) -> List.mem y vars) le &&
|
||||
aux (x::vars) tl
|
||||
in
|
||||
aux [] l
|
||||
|
||||
let shrink_step self =
|
||||
let module S = QC.Shrink in
|
||||
match self with
|
||||
| S_new_var _
|
||||
| S_leq _ | S_lt _ | S_eq _ -> QC.Iter.empty
|
||||
| S_define (x, le) ->
|
||||
let open QC.Iter in
|
||||
let* le = S.list le in
|
||||
if List.length le >= 2 then return (S_define (x,le)) else empty
|
||||
|
||||
let rand_steps (n:int) : t list QC.Gen.t =
|
||||
let open G in
|
||||
let rec aux n vars acc =
|
||||
if n<=0 then return (List.rev acc)
|
||||
else (
|
||||
let gen_linexp =
|
||||
let* vars' = G.shuffle_l vars in
|
||||
let* n = 1 -- (min 7 @@ List.length vars') in
|
||||
let vars' = CCList.take n vars' in
|
||||
assert (List.length vars' = n);
|
||||
let* coeffs = list_repeat n rand_z.gen in
|
||||
return (List.combine coeffs vars')
|
||||
in
|
||||
let* vars, proof_rule =
|
||||
frequency @@ List.flatten [
|
||||
(* add a constraint *)
|
||||
(match vars with
|
||||
| [] -> []
|
||||
| _ ->
|
||||
let gen =
|
||||
let+ le = gen_linexp
|
||||
and+ kind = frequencyl [5, `Leq; 5, `Lt; 3,`Eq]
|
||||
and+ n = rand_z.QC.gen in
|
||||
vars, (match kind with
|
||||
| `Lt -> S_lt(le,n)
|
||||
| `Leq -> S_leq(le,n)
|
||||
| `Eq -> S_eq(le,n)
|
||||
)
|
||||
in
|
||||
[6, gen]);
|
||||
(* make a new non-basic var *)
|
||||
(let gen =
|
||||
let v = List.length vars in
|
||||
return ((v::vars), S_new_var v)
|
||||
in
|
||||
[2, gen]);
|
||||
(* make a definition *)
|
||||
(if List.length vars>2
|
||||
then (
|
||||
let v = List.length vars in
|
||||
let gen =
|
||||
let+ le = gen_linexp in
|
||||
v::vars, S_define (v, le)
|
||||
in
|
||||
[5, gen]
|
||||
) else []);
|
||||
]
|
||||
in
|
||||
aux (n-1) vars (proof_rule::acc)
|
||||
)
|
||||
in
|
||||
aux n [] []
|
||||
|
||||
(* shrink a list but keep it well formed *)
|
||||
let shrink : t list QC.Shrink.t =
|
||||
QC.Shrink.(filter well_formed @@ list ~shrink:shrink_step)
|
||||
|
||||
let gen_for n1 n2 =
|
||||
let open G in
|
||||
assert (n1 < n2);
|
||||
let* n = n1 -- n2 in
|
||||
rand_steps n
|
||||
|
||||
let rand_for n1 n2 : t list QC.arbitrary =
|
||||
let print = Fmt.to_string (Fmt.Dump.list pp_) in
|
||||
QC.make ~shrink ~print (gen_for n1 n2)
|
||||
|
||||
let rand : t list QC.arbitrary = rand_for 1 15
|
||||
end
|
||||
|
||||
let on_propagate _ ~reason:_ = ()
|
||||
|
||||
(* add a single proof_rule to the solvere *)
|
||||
let add_step solver (s:Step.t) : unit =
|
||||
begin match s with
|
||||
| Step.S_new_var _v -> ()
|
||||
| Step.S_leq (le,n) ->
|
||||
Solver.assert_ solver le Solver.Op.Leq n ~lit:0
|
||||
| Step.S_lt (le,n) ->
|
||||
Solver.assert_ solver le Solver.Op.Lt n ~lit:0
|
||||
| Step.S_eq (le,n) ->
|
||||
Solver.assert_ solver le Solver.Op.Eq n ~lit:0
|
||||
| Step.S_define (x,le) ->
|
||||
Solver.define solver x le
|
||||
end
|
||||
|
||||
let add_steps ?(f=fun()->()) (solver:Solver.t) l : unit =
|
||||
f();
|
||||
List.iter
|
||||
(fun s -> add_step solver s; f())
|
||||
l
|
||||
|
||||
(* is this solver's state sat? *)
|
||||
let check_solver_is_sat solver : bool =
|
||||
match Solver.check solver with
|
||||
| Solver.Sat _ -> true
|
||||
| Solver.Unsat _ -> false
|
||||
|
||||
(* is this problem sat? *)
|
||||
let check_pb_is_sat pb : bool =
|
||||
let solver = Solver.create() in
|
||||
add_steps solver pb;
|
||||
check_solver_is_sat solver
|
||||
|
||||
(* basic debug printer for Q.t *)
|
||||
let str_z n = ZarithZ.to_string n
|
||||
|
||||
let prop_sound ?(inv=false) pb =
|
||||
let solver = Solver.create () in
|
||||
begin match
|
||||
add_steps solver pb;
|
||||
Solver.check solver
|
||||
with
|
||||
| Sat model ->
|
||||
|
||||
let get_val v =
|
||||
match Solver.Model.eval model v with
|
||||
| Some n -> n
|
||||
| None -> assert false
|
||||
in
|
||||
|
||||
let eval_le le =
|
||||
List.fold_left (fun s (n,y) -> Z.(s + n * get_val y)) Z.zero le
|
||||
in
|
||||
|
||||
let check_step s =
|
||||
(try
|
||||
if inv then Solver._check_invariants solver;
|
||||
match s with
|
||||
| Step.S_new_var _ -> ()
|
||||
| Step.S_define (x, le) ->
|
||||
let v_x = get_val x in
|
||||
let v_le = eval_le le in
|
||||
if Z.(v_x <> v_le) then (
|
||||
failwith (spf "bad def (X_%d): val(x)=%s, val(expr)=%s" x (str_z v_x)(str_z v_le))
|
||||
);
|
||||
| Step.S_lt (x, n) ->
|
||||
let v_x = eval_le x in
|
||||
if Z.(v_x >= n) then failwith (spf "val=%s, n=%s"(str_z v_x)(str_z n))
|
||||
| Step.S_leq (x, n) ->
|
||||
let v_x = eval_le x in
|
||||
if Z.(v_x > n) then failwith (spf "val=%s, n=%s"(str_z v_x)(str_z n))
|
||||
| Step.S_eq (x, n) ->
|
||||
let v_x = eval_le x in
|
||||
if Z.(v_x <> n) then failwith (spf "val=%s, n=%s"(str_z v_x)(str_z n))
|
||||
with e ->
|
||||
QC.Test.fail_reportf "proof_rule failed: %a@.exn:@.%s@."
|
||||
Step.pp_ s (Printexc.to_string e)
|
||||
);
|
||||
if inv then Solver._check_invariants solver;
|
||||
true
|
||||
in
|
||||
List.for_all check_step pb
|
||||
|
||||
| Solver.Unsat _cert ->
|
||||
(* FIXME:
|
||||
Solver._check_cert cert;
|
||||
*)
|
||||
true
|
||||
end
|
||||
|
||||
(* a bunch of useful stats for a problem *)
|
||||
let steps_stats = [
|
||||
"n-define", Step.(List.fold_left (fun n -> function S_define _ -> n+1 | _->n) 0);
|
||||
"n-bnd",
|
||||
Step.(List.fold_left
|
||||
(fun n -> function (S_leq _ | S_lt _ | S_eq _) -> n+1 | _->n) 0);
|
||||
"n-vars",
|
||||
Step.(List.fold_left
|
||||
(fun n -> function S_define _ | S_new_var _ -> n+1 | _ -> n) 0);
|
||||
]
|
||||
|
||||
let enable_stats =
|
||||
match Sys.getenv_opt "TEST_STAT" with Some("1"|"true") -> true | _ -> false
|
||||
|
||||
let set_stats_maybe ar =
|
||||
if enable_stats then QC.set_stats steps_stats ar else ar
|
||||
|
||||
let check_sound =
|
||||
let ar =
|
||||
Step.(rand_for 0 15)
|
||||
|> QC.set_collect (fun pb -> if check_pb_is_sat pb then "sat" else "unsat")
|
||||
|> set_stats_maybe
|
||||
in
|
||||
QC.Test.make ~long_factor:10 ~count:500 ~name:"solver2_sound" ar prop_sound
|
||||
|
||||
let prop_backtrack pb =
|
||||
let solver = Solver.create () in
|
||||
let stack = Stack.create() in
|
||||
let res = ref true in
|
||||
begin try
|
||||
List.iter
|
||||
(fun s ->
|
||||
let is_sat = check_solver_is_sat solver in
|
||||
Solver.push_level solver;
|
||||
Stack.push is_sat stack;
|
||||
if not is_sat then (res := false; raise Exit);
|
||||
add_step solver s;
|
||||
)
|
||||
pb;
|
||||
with Exit -> ()
|
||||
end;
|
||||
res := !res && check_solver_is_sat solver;
|
||||
Log.debugf 50 (fun k->k "res=%b, expected=%b" !res (check_pb_is_sat pb));
|
||||
assert CCBool.(equal !res (check_pb_is_sat pb));
|
||||
(* now backtrack and check at each level *)
|
||||
while not (Stack.is_empty stack) do
|
||||
let res = Stack.pop stack in
|
||||
Solver.pop_levels solver 1;
|
||||
assert CCBool.(equal res (check_solver_is_sat solver))
|
||||
done;
|
||||
true
|
||||
|
||||
let check_backtrack =
|
||||
let ar =
|
||||
Step.(rand_for 0 15)
|
||||
|> QC.set_collect (fun pb -> if check_pb_is_sat pb then "sat" else "unsat")
|
||||
|> set_stats_maybe
|
||||
in
|
||||
QC.Test.make
|
||||
~long_factor:10 ~count:200 ~name:"solver2_backtrack"
|
||||
ar prop_backtrack
|
||||
|
||||
let props = [
|
||||
(* FIXME: need to finish the implem, including model production
|
||||
check_sound;
|
||||
check_backtrack;
|
||||
*)
|
||||
]
|
||||
|
||||
(* regression tests *)
|
||||
|
||||
module Reg = struct
|
||||
let alco_mk name f = name, `Quick, f
|
||||
|
||||
let reg_prop_sound ?inv name l =
|
||||
alco_mk name @@ fun () ->
|
||||
if not (prop_sound ?inv l) then Alcotest.fail "fail";
|
||||
()
|
||||
|
||||
let reg_prop_backtrack name l =
|
||||
alco_mk name @@ fun () ->
|
||||
if not (prop_backtrack l) then Alcotest.fail "fail";
|
||||
()
|
||||
|
||||
open Step
|
||||
let tests = [
|
||||
]
|
||||
end
|
||||
|
||||
let tests =
|
||||
"solver", List.flatten [ Reg.tests ]
|
||||
|
|
@ -1,118 +0,0 @@
|
|||
|
||||
(** {1 Linear Integer Arithmetic} *)
|
||||
|
||||
(* Reference:
|
||||
http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_LIA *)
|
||||
|
||||
open Sidekick_core
|
||||
include Intf_lia
|
||||
|
||||
module Make(A : ARG) : S with module A = A = struct
|
||||
module A = A
|
||||
module Ty = A.S.T.Ty
|
||||
module T = A.S.T.Term
|
||||
module Lit = A.S.Solver_internal.Lit
|
||||
module SI = A.S.Solver_internal
|
||||
module N = A.S.Solver_internal.CC.N
|
||||
|
||||
module Q = A.Q
|
||||
module Z = A.Z
|
||||
|
||||
module LRA_solver = A.LRA_solver
|
||||
|
||||
type state = {
|
||||
stat: Stat.t;
|
||||
proof: A.S.P.t;
|
||||
tst: T.store;
|
||||
ty_st: Ty.store;
|
||||
lra_solver: LRA_solver.state;
|
||||
(* TODO: with intsolver
|
||||
encoded_eqs: unit T.Tbl.t; (* [a=b] gets clause [a = b <=> (a >= b /\ a <= b)] *)
|
||||
needs_th_combination: unit T.Tbl.t;
|
||||
stat_th_comb: int Stat.counter;
|
||||
*)
|
||||
}
|
||||
|
||||
let create ?(stat=Stat.create()) ~lra_solver proof tst ty_st : state =
|
||||
{ stat; proof; tst; ty_st;
|
||||
lra_solver;
|
||||
(*
|
||||
encoded_eqs=T.Tbl.create 16;
|
||||
needs_th_combination=T.Tbl.create 16;
|
||||
stat_th_comb=Stat.mk_int stat "lia.th-comb";
|
||||
*)
|
||||
}
|
||||
|
||||
let push_level _self =
|
||||
(*
|
||||
Backtrack_stack.push_level self.local_eqs;
|
||||
*)
|
||||
()
|
||||
|
||||
let pop_levels _self _n =
|
||||
(*
|
||||
Backtrack_stack.pop_levels self.local_eqs n ~f:(fun _ -> ());
|
||||
*)
|
||||
()
|
||||
|
||||
(* convert [t] to a real-typed term *)
|
||||
let rec conv_to_lra (self:state) (t:T.t) : T.t =
|
||||
let open Sidekick_arith_lra in
|
||||
let f = conv_to_lra self in
|
||||
let mklra = LRA_solver.A.mk_lra self.tst in
|
||||
match A.view_as_lia t with
|
||||
| LIA_const n ->
|
||||
mklra @@ LRA_const (Q.of_bigint n)
|
||||
| LIA_pred (p, a, b) ->
|
||||
mklra @@ LRA_pred (p, f a, f b)
|
||||
| LIA_op (op, a, b) ->
|
||||
mklra @@ LRA_op (op, f a, f b)
|
||||
| LIA_mult (c, x) ->
|
||||
mklra @@ LRA_mult (Q.of_bigint c, f x)
|
||||
| LIA_other t ->
|
||||
mklra @@ LRA_other (A.mk_to_real self.tst t)
|
||||
|
||||
(* preprocess linear expressions away *)
|
||||
let preproc_lia (self:state) si (module PA:SI.PREPROCESS_ACTS)
|
||||
(t:T.t) : unit =
|
||||
Log.debugf 50 (fun k->k "(@[lia.preprocess@ %a@])" T.pp t);
|
||||
|
||||
match A.view_as_lia t with
|
||||
| LIA_pred _ ->
|
||||
(* perform LRA relaxation *)
|
||||
let u = conv_to_lra self t in
|
||||
let pr =
|
||||
let lits = [Lit.atom ~sign:false self.tst t; Lit.atom self.tst u] in
|
||||
A.lemma_relax_to_lra Iter.(of_list lits) self.proof
|
||||
in
|
||||
|
||||
(* add [t => u] *)
|
||||
let cl = [PA.mk_lit ~sign:false t; PA.mk_lit u] in
|
||||
PA.add_clause cl pr;
|
||||
|
||||
| LIA_other t when A.has_ty_int t ->
|
||||
SI.declare_pb_is_incomplete si;
|
||||
| LIA_op _ | LIA_mult _ ->
|
||||
(* TODO: theory combination?*)
|
||||
SI.declare_pb_is_incomplete si;
|
||||
| LIA_const _ | LIA_other _ -> ()
|
||||
|
||||
let create_and_setup si =
|
||||
Log.debug 2 "(th-lia.setup)";
|
||||
let stat = SI.stats si in
|
||||
let lra = match SI.Registry.get (SI.registry si) LRA_solver.k_state with
|
||||
| None -> Error.errorf "LIA: cannot find LRA, is it registered?"
|
||||
| Some st -> st
|
||||
in
|
||||
let st = create ~stat ~lra_solver:lra
|
||||
(SI.proof si) (SI.tst si) (SI.ty_st si) in
|
||||
|
||||
SI.on_preprocess si (preproc_lia st);
|
||||
st
|
||||
|
||||
let theory =
|
||||
A.S.mk_theory
|
||||
~name:"th-lia"
|
||||
~create_and_setup ~push_level ~pop_levels
|
||||
()
|
||||
end
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
|
||||
|
||||
(** {1 Linear Rational Arithmetic} *)
|
||||
|
||||
(* Reference:
|
||||
http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_LIA *)
|
||||
|
||||
open Sidekick_core
|
||||
include module type of Intf_lia
|
||||
|
||||
module Make(A : ARG) : S with module A=A
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
(library
|
||||
(name sidekick_arith_lia)
|
||||
(public_name sidekick.arith-lia)
|
||||
(synopsis "Solver for LIA (integer arithmetic)")
|
||||
(flags :standard -warn-error -a+8 -w -32 -open Sidekick_util)
|
||||
(libraries containers sidekick.core sidekick.arith sidekick.arith-lra))
|
||||
|
|
@ -1,69 +0,0 @@
|
|||
|
||||
|
||||
module type RATIONAL = Sidekick_arith.RATIONAL
|
||||
module type INT = Sidekick_arith.INT
|
||||
|
||||
module S_op = Sidekick_simplex.Op
|
||||
type pred = Sidekick_simplex.Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq
|
||||
type op = Sidekick_simplex.Binary_op.t = Plus | Minus
|
||||
|
||||
type ('num, 'real, 'a) lia_view =
|
||||
| LIA_pred of pred * 'a * 'a
|
||||
| LIA_op of op * 'a * 'a
|
||||
| LIA_mult of 'num * 'a
|
||||
| LIA_const of 'num
|
||||
| LIA_other of 'a
|
||||
|
||||
let map_view f (l:_ lia_view) : _ lia_view =
|
||||
begin match l with
|
||||
| LIA_pred (p, a, b) -> LIA_pred (p, f a, f b)
|
||||
| LIA_op (p, a, b) -> LIA_op (p, f a, f b)
|
||||
| LIA_mult (n,a) -> LIA_mult (n, f a)
|
||||
| LIA_const q -> LIA_const q
|
||||
| LIA_other x -> LIA_other (f x)
|
||||
end
|
||||
|
||||
module type ARG = sig
|
||||
module S : Sidekick_core.SOLVER
|
||||
|
||||
module Z : INT
|
||||
module Q : RATIONAL with type bigint = Z.t
|
||||
|
||||
(* pass a LRA solver as parameter *)
|
||||
module LRA_solver :
|
||||
Sidekick_arith_lra.S
|
||||
with type A.Q.t = Q.t
|
||||
and module A.S = S
|
||||
|
||||
type term = S.T.Term.t
|
||||
type ty = S.T.Ty.t
|
||||
|
||||
val view_as_lia : term -> (Z.t, Q.t, term) lia_view
|
||||
(** Project the term into the theory view *)
|
||||
|
||||
val mk_bool : S.T.Term.store -> bool -> term
|
||||
|
||||
val mk_to_real : S.T.Term.store -> term -> term
|
||||
(** Wrap term into a [to_real] projector to rationals *)
|
||||
|
||||
val mk_lia : S.T.Term.store -> (Z.t, Q.t, term) lia_view -> term
|
||||
(** Make a term from the given theory view *)
|
||||
|
||||
val ty_int : S.T.Term.store -> ty
|
||||
|
||||
val mk_eq : S.T.Term.store -> term -> term -> term
|
||||
(** syntactic equality *)
|
||||
|
||||
val has_ty_int : term -> bool
|
||||
(** Does this term have the type [Int] *)
|
||||
|
||||
val lemma_lia : S.Lit.t Iter.t -> S.P.proof_rule
|
||||
|
||||
val lemma_relax_to_lra : S.Lit.t Iter.t -> S.P.proof_rule
|
||||
end
|
||||
|
||||
module type S = sig
|
||||
module A : ARG
|
||||
|
||||
val theory : A.S.theory
|
||||
end
|
||||
|
|
@ -115,17 +115,14 @@ module Make(A : ARG) : S with module A = A = struct
|
|||
|
||||
module Tag = struct
|
||||
type t =
|
||||
| By_def
|
||||
| Lit of Lit.t
|
||||
| CC_eq of N.t * N.t
|
||||
|
||||
let pp out = function
|
||||
| By_def -> Fmt.string out "by-def"
|
||||
| Lit l -> Fmt.fprintf out "(@[lit %a@])" Lit.pp l
|
||||
| CC_eq (n1,n2) -> Fmt.fprintf out "(@[cc-eq@ %a@ %a@])" N.pp n1 N.pp n2
|
||||
|
||||
let to_lits si = function
|
||||
| By_def -> []
|
||||
| Lit l -> [l]
|
||||
| CC_eq (n1,n2) ->
|
||||
let r = SI.CC.explain_eq (SI.cc si) n1 n2 in
|
||||
|
|
|
|||
|
|
@ -145,7 +145,6 @@ let main_smt () : _ result =
|
|||
Process.th_bool;
|
||||
Process.th_data;
|
||||
Process.th_lra;
|
||||
Process.th_lia;
|
||||
]
|
||||
in
|
||||
Process.Solver.create ~proof ~theories tst () ()
|
||||
|
|
|
|||
|
|
@ -109,7 +109,6 @@ module type S = sig
|
|||
(** Make sure the variable exists in the simplex. *)
|
||||
|
||||
val add_constraint :
|
||||
?keep_on_backtracking:bool ->
|
||||
?is_int:bool ->
|
||||
on_propagate:ev_on_propagate ->
|
||||
t -> Constraint.t -> V.lit -> unit
|
||||
|
|
@ -118,8 +117,6 @@ module type S = sig
|
|||
This is removed upon backtracking by default.
|
||||
@param is_int declares whether the constraint's variable is an integer
|
||||
@raise Unsat if it's immediately obvious that this is not satisfiable.
|
||||
@param keep_on_backtracking if true (default false), the bound is not
|
||||
backtrackable
|
||||
*)
|
||||
|
||||
val declare_bound : ?is_int:bool -> t -> Constraint.t -> V.lit -> unit
|
||||
|
|
@ -449,7 +446,6 @@ module Make(Arg: ARG)
|
|||
vars: var_state Vec.t; (* index -> var with this index *)
|
||||
mutable var_tbl: var_state V_map.t; (* var -> its state *)
|
||||
bound_stack: bound_assertion Backtrack_stack.t;
|
||||
bound_lvl0: bound_assertion Vec.t;
|
||||
undo_stack: (unit -> unit) Backtrack_stack.t;
|
||||
stat_check: int Stat.counter;
|
||||
stat_unsat: int Stat.counter;
|
||||
|
|
@ -809,7 +805,7 @@ module Make(Arg: ARG)
|
|||
self.vars;
|
||||
!map_res, !bounds
|
||||
|
||||
let add_constraint ?(keep_on_backtracking=false) ?(is_int=false)
|
||||
let add_constraint ?(is_int=false)
|
||||
~on_propagate (self:t) (c:Constraint.t) (lit:lit) : unit =
|
||||
let open Constraint in
|
||||
|
||||
|
|
@ -1056,7 +1052,6 @@ module Make(Arg: ARG)
|
|||
vars=Vec.create();
|
||||
var_tbl=V_map.empty;
|
||||
bound_stack=Backtrack_stack.create();
|
||||
bound_lvl0=Vec.create();
|
||||
undo_stack=Backtrack_stack.create();
|
||||
stat_check=Stat.mk_int stat "simplex.check";
|
||||
stat_unsat=Stat.mk_int stat "simplex.conflicts";
|
||||
|
|
|
|||
|
|
@ -308,7 +308,6 @@ module Make(A : ARG)
|
|||
delayed_actions: delayed_action Queue.t;
|
||||
mutable last_model: Model.t option;
|
||||
|
||||
mutable t_defs : (term*term) list; (* term definitions *)
|
||||
mutable th_states : th_states; (** Set of theories *)
|
||||
mutable level: int;
|
||||
mutable complete: bool;
|
||||
|
|
@ -805,7 +804,6 @@ module Make(A : ARG)
|
|||
count_preprocess_clause = Stat.mk_int stat "solver.preprocess-clause";
|
||||
count_propagate = Stat.mk_int stat "solver.th-propagations";
|
||||
count_conflict = Stat.mk_int stat "solver.th-conflicts";
|
||||
t_defs=[];
|
||||
on_partial_check=[];
|
||||
on_final_check=[];
|
||||
on_th_combination=[];
|
||||
|
|
|
|||
|
|
@ -351,9 +351,7 @@ let process_stmt
|
|||
module Th_data = SBS.Th_data
|
||||
module Th_bool = SBS.Th_bool
|
||||
module Th_lra = SBS.Th_lra
|
||||
module Th_lia = SBS.Th_lia
|
||||
|
||||
let th_bool : Solver.theory = Th_bool.theory
|
||||
let th_data : Solver.theory = Th_data.theory
|
||||
let th_lra : Solver.theory = Th_lra.theory
|
||||
let th_lia : Solver.theory = Th_lia.theory
|
||||
|
|
|
|||
|
|
@ -12,7 +12,6 @@ module Solver
|
|||
val th_bool : Solver.theory
|
||||
val th_data : Solver.theory
|
||||
val th_lra : Solver.theory
|
||||
val th_lia : Solver.theory
|
||||
|
||||
type 'a or_error = ('a, string) CCResult.t
|
||||
|
||||
|
|
|
|||
|
|
@ -1,11 +1,9 @@
|
|||
|
||||
(executable
|
||||
(name run_tests)
|
||||
(modules run_tests)
|
||||
(modes native)
|
||||
(libraries containers alcotest qcheck sidekick.util
|
||||
sidekick_test_simplex sidekick_test_intsolver
|
||||
sidekick_test_util sidekick_test_minicc)
|
||||
(libraries containers alcotest qcheck sidekick.util sidekick_test_simplex
|
||||
sidekick_test_util sidekick_test_minicc)
|
||||
(flags :standard -warn-error -a+8 -color always))
|
||||
|
||||
(alias
|
||||
|
|
@ -13,18 +11,21 @@
|
|||
(locks /test)
|
||||
(package sidekick)
|
||||
(action
|
||||
(progn
|
||||
(run ./run_tests.exe alcotest) ; run regressions first
|
||||
(run ./run_tests.exe qcheck --verbose))))
|
||||
(progn
|
||||
(run ./run_tests.exe alcotest) ; run regressions first
|
||||
(run ./run_tests.exe qcheck --verbose))))
|
||||
|
||||
(rule
|
||||
(targets basic.drup)
|
||||
(deps (:pb basic.cnf) (:solver ../main/main.exe))
|
||||
(action (run %{solver} %{pb} -t 2 -o %{targets})))
|
||||
(targets basic.drup)
|
||||
(deps
|
||||
(:pb basic.cnf)
|
||||
(:solver ../main/main.exe))
|
||||
(action
|
||||
(run %{solver} %{pb} -t 2 -o %{targets})))
|
||||
|
||||
(alias
|
||||
(name runtest)
|
||||
(locks /test)
|
||||
(package sidekick-bin)
|
||||
(action
|
||||
(diff basic.drup.expected basic.drup)))
|
||||
(diff basic.drup.expected basic.drup)))
|
||||
|
|
|
|||
|
|
@ -1,7 +1,6 @@
|
|||
|
||||
let tests : unit Alcotest.test list =
|
||||
List.flatten @@ [
|
||||
[Sidekick_test_intsolver.tests];
|
||||
[Sidekick_test_simplex.tests];
|
||||
[Sidekick_test_minicc.tests];
|
||||
Sidekick_test_util.tests;
|
||||
|
|
@ -10,7 +9,6 @@ let tests : unit Alcotest.test list =
|
|||
let props =
|
||||
List.flatten
|
||||
[
|
||||
Sidekick_test_intsolver.props;
|
||||
Sidekick_test_simplex.props;
|
||||
Sidekick_test_util.props;
|
||||
]
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue