From e2b9b2874c12f10b83205fd2b373f737211c20d0 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 14 Jul 2022 22:01:23 -0400 Subject: [PATCH] fix more warnings; remove never completed LIA stuff --- src/base-solver/dune | 16 +- src/base-solver/sidekick_base_solver.ml | 43 -- src/base/Base_types.ml | 2 - src/intsolver/dune | 6 - src/intsolver/sidekick_intsolver.ml | 633 ------------------ src/intsolver/tests/dune | 5 - .../tests/sidekick_test_intsolver.ml | 346 ---------- src/lia/Sidekick_arith_lia.ml | 118 ---- src/lia/Sidekick_arith_lia.mli | 11 - src/lia/dune | 6 - src/lia/intf_lia.ml | 69 -- src/lra/sidekick_arith_lra.ml | 3 - src/main/main.ml | 1 - src/simplex/sidekick_simplex.ml | 7 +- src/smt-solver/Sidekick_smt_solver.ml | 2 - src/smtlib/Process.ml | 2 - src/smtlib/Process.mli | 1 - src/tests/dune | 23 +- src/tests/run_tests.ml | 2 - 19 files changed, 21 insertions(+), 1275 deletions(-) delete mode 100644 src/intsolver/dune delete mode 100644 src/intsolver/sidekick_intsolver.ml delete mode 100644 src/intsolver/tests/dune delete mode 100644 src/intsolver/tests/sidekick_test_intsolver.ml delete mode 100644 src/lia/Sidekick_arith_lia.ml delete mode 100644 src/lia/Sidekick_arith_lia.mli delete mode 100644 src/lia/dune delete mode 100644 src/lia/intf_lia.ml diff --git a/src/base-solver/dune b/src/base-solver/dune index 693fa02a..ab2c62ab 100644 --- a/src/base-solver/dune +++ b/src/base-solver/dune @@ -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)) diff --git a/src/base-solver/sidekick_base_solver.ml b/src/base-solver/sidekick_base_solver.ml index 6e05cc92..89c204ef 100644 --- a/src/base-solver/sidekick_base_solver.ml +++ b/src/base-solver/sidekick_base_solver.ml @@ -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 diff --git a/src/base/Base_types.ml b/src/base/Base_types.ml index 69c93293..47cfe4f9 100644 --- a/src/base/Base_types.ml +++ b/src/base/Base_types.ml @@ -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_); diff --git a/src/intsolver/dune b/src/intsolver/dune deleted file mode 100644 index 04779850..00000000 --- a/src/intsolver/dune +++ /dev/null @@ -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)) diff --git a/src/intsolver/sidekick_intsolver.ml b/src/intsolver/sidekick_intsolver.ml deleted file mode 100644 index dea33cc6..00000000 --- a/src/intsolver/sidekick_intsolver.ml +++ /dev/null @@ -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 "(@[@{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 "(@[@{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 diff --git a/src/intsolver/tests/dune b/src/intsolver/tests/dune deleted file mode 100644 index 969a9b4d..00000000 --- a/src/intsolver/tests/dune +++ /dev/null @@ -1,5 +0,0 @@ - -(library - (name sidekick_test_intsolver) - (libraries zarith sidekick.intsolver sidekick.util sidekick.zarith - qcheck alcotest)) diff --git a/src/intsolver/tests/sidekick_test_intsolver.ml b/src/intsolver/tests/sidekick_test_intsolver.ml deleted file mode 100644 index fecb8dd4..00000000 --- a/src/intsolver/tests/sidekick_test_intsolver.ml +++ /dev/null @@ -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 ] diff --git a/src/lia/Sidekick_arith_lia.ml b/src/lia/Sidekick_arith_lia.ml deleted file mode 100644 index 5fdaaa47..00000000 --- a/src/lia/Sidekick_arith_lia.ml +++ /dev/null @@ -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 diff --git a/src/lia/Sidekick_arith_lia.mli b/src/lia/Sidekick_arith_lia.mli deleted file mode 100644 index ddbdc9aa..00000000 --- a/src/lia/Sidekick_arith_lia.mli +++ /dev/null @@ -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 diff --git a/src/lia/dune b/src/lia/dune deleted file mode 100644 index 35103ce4..00000000 --- a/src/lia/dune +++ /dev/null @@ -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)) diff --git a/src/lia/intf_lia.ml b/src/lia/intf_lia.ml deleted file mode 100644 index 6719f237..00000000 --- a/src/lia/intf_lia.ml +++ /dev/null @@ -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 diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml index 72eb5be1..9edf4367 100644 --- a/src/lra/sidekick_arith_lra.ml +++ b/src/lra/sidekick_arith_lra.ml @@ -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 diff --git a/src/main/main.ml b/src/main/main.ml index 108ebe1e..dd5867d6 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -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 () () diff --git a/src/simplex/sidekick_simplex.ml b/src/simplex/sidekick_simplex.ml index df8caac2..c588c5f2 100644 --- a/src/simplex/sidekick_simplex.ml +++ b/src/simplex/sidekick_simplex.ml @@ -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"; diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml index c20e8554..eae905d8 100644 --- a/src/smt-solver/Sidekick_smt_solver.ml +++ b/src/smt-solver/Sidekick_smt_solver.ml @@ -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=[]; diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 5052c27b..96f9098f 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -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 diff --git a/src/smtlib/Process.mli b/src/smtlib/Process.mli index 07879ffc..2d07a8c9 100644 --- a/src/smtlib/Process.mli +++ b/src/smtlib/Process.mli @@ -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 diff --git a/src/tests/dune b/src/tests/dune index 72c80e8a..ead3d67e 100644 --- a/src/tests/dune +++ b/src/tests/dune @@ -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))) diff --git a/src/tests/run_tests.ml b/src/tests/run_tests.ml index b8119d40..037b99e3 100644 --- a/src/tests/run_tests.ml +++ b/src/tests/run_tests.ml @@ -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; ]