From 4b2afd7a05520161e5761cec2425583979ef7ee1 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 13 Jan 2022 12:54:35 -0500 Subject: [PATCH] wip: LIA theory --- src/base-solver/sidekick_base_solver.ml | 41 +- src/base/Base_types.ml | 72 ++-- src/lia/Sidekick_arith_lia.ml | 476 ++++++++++++------------ src/lia/Sidekick_arith_lia.mli | 2 +- src/lia/dune | 2 +- src/lia/{intf.ml => intf_lia.ml} | 31 +- src/lra/sidekick_arith_lra.ml | 4 +- src/smtlib/Typecheck.ml | 2 +- 8 files changed, 326 insertions(+), 304 deletions(-) rename src/lia/{intf.ml => intf_lia.ml} (67%) diff --git a/src/base-solver/sidekick_base_solver.ml b/src/base-solver/sidekick_base_solver.ml index 6cfba728..76bc9f08 100644 --- a/src/base-solver/sidekick_base_solver.ml +++ b/src/base-solver/sidekick_base_solver.ml @@ -76,10 +76,29 @@ module Th_bool = Sidekick_th_bool_static.Make(struct let lemma_ite_false = Proof.lemma_ite_false end) + +module Gensym = struct + type t = { + tst: Term.store; + mutable fresh: int; + } + + let create tst : t = {tst; fresh=0} + let tst self = self.tst + let copy s = {s with tst=s.tst} + + let fresh_term (self:t) ~pre (ty:Ty.t) : Term.t = + let name = Printf.sprintf "_sk_lra_%s%d" pre self.fresh in + self.fresh <- 1 + self.fresh; + let id = ID.make name in + Term.const self.tst @@ Fun.mk_undef_const id ty +end + (** Theory of Linear Rational Arithmetic *) module Th_lra = Sidekick_arith_lra.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 @@ -120,34 +139,17 @@ module Th_lra = Sidekick_arith_lra.Make(struct let has_ty_real t = Ty.equal (T.ty t) (Ty.real()) let lemma_lra = Proof.lemma_lra - - module Gensym = struct - type t = { - tst: T.store; - mutable fresh: int; - } - - let create tst : t = {tst; fresh=0} - let tst self = self.tst - let copy s = {s with tst=s.tst} - - let fresh_term (self:t) ~pre (ty:Ty.t) : T.t = - let name = Printf.sprintf "_sk_lra_%s%d" pre self.fresh in - self.fresh <- 1 + self.fresh; - let id = ID.make name in - Term.const self.tst @@ Fun.mk_undef_const id ty - end + module Gensym = Gensym end) module Th_lia = Sidekick_arith_lia.Make(struct module S = Solver module T = Term - module Q = Sidekick_zarith.Rational module Z = Sidekick_zarith.Int + module Q = Sidekick_zarith.Rational type term = S.T.Term.t type ty = S.T.Ty.t - module LRA = Th_lra module LIA = Sidekick_arith_lia let mk_eq = Form.eq @@ -184,6 +186,7 @@ module Th_lia = Sidekick_arith_lia.Make(struct let has_ty_int t = Ty.equal (T.ty t) (Ty.int()) let lemma_lia = Proof.lemma_lia + module Gensym = Gensym end) let th_bool : Solver.theory = Th_bool.theory diff --git a/src/base/Base_types.ml b/src/base/Base_types.ml index d7df7c1a..5bb82858 100644 --- a/src/base/Base_types.ml +++ b/src/base/Base_types.ml @@ -11,7 +11,7 @@ module Storage = Sidekick_base_proof_trace.Storage type lra_pred = Sidekick_arith_lra.Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq type lra_op = Sidekick_arith_lra.op = Plus | Minus -type ('num, 'a) arith_view = +type ('num, 'real, 'a) arith_view = | Arith_pred of lra_pred * 'a * 'a | Arith_op of lra_op * 'a * 'a | Arith_mult of 'num * 'a @@ -20,10 +20,10 @@ type ('num, 'a) arith_view = | Arith_to_real of 'a (* after preprocessing *) - | Arith_simplex_pred of 'a * Sidekick_arith_lra.S_op.t * 'num + | Arith_simplex_pred of 'a * Sidekick_arith_lra.S_op.t * 'real | Arith_simplex_var of 'a -let map_arith_view ~f_c f (l:_ arith_view) : _ arith_view = +let map_arith_view ~f_c ~f_real f (l:_ arith_view) : _ arith_view = begin match l with | Arith_pred (p, a, b) -> Arith_pred (p, f a, f b) | Arith_op (p, a, b) -> Arith_op (p, f a, f b) @@ -32,7 +32,7 @@ let map_arith_view ~f_c f (l:_ arith_view) : _ arith_view = | Arith_var x -> Arith_var (f x) | Arith_to_real x -> Arith_to_real (f x) | Arith_simplex_var v -> Arith_simplex_var (f v) - | Arith_simplex_pred (v, op, c) -> Arith_simplex_pred (f v, op, f_c c) + | Arith_simplex_pred (v, op, c) -> Arith_simplex_pred (f v, op, f_real c) end let iter_arith_view f l : unit = @@ -64,8 +64,8 @@ and 'a term_view = | Eq of 'a * 'a | Not of 'a | Ite of 'a * 'a * 'a - | LRA of (Q.t, 'a) arith_view - | LIA of (Z.t, 'a) arith_view + | LRA of (Q.t, Q.t, 'a) arith_view + | LIA of (Z.t, Q.t, 'a) arith_view and fun_ = { fun_id: ID.t; @@ -258,7 +258,7 @@ let string_of_lra_op = function | Minus -> "-" let pp_lra_op out p = Fmt.string out (string_of_lra_op p) -let pp_arith_gen ~pp_c ~pp_t out = function +let pp_arith_gen ~pp_c ~pp_real ~pp_t out = function | Arith_pred (p, a, b) -> Fmt.fprintf out "(@[%s@ %a@ %a@])" (string_of_lra_pred p) pp_t a pp_t b | Arith_op (p, a, b) -> @@ -271,7 +271,7 @@ let pp_arith_gen ~pp_c ~pp_t out = function | Arith_simplex_var v -> pp_t out v | Arith_simplex_pred (v, op, c) -> Fmt.fprintf out "(@[%a@ %s %a@])" - pp_t v (Sidekick_arith_lra.S_op.to_string op) pp_c c + pp_t v (Sidekick_arith_lra.S_op.to_string op) pp_real c let pp_term_view_gen ~pp_id ~pp_t out = function | Bool true -> Fmt.string out "true" @@ -284,8 +284,8 @@ let pp_term_view_gen ~pp_id ~pp_t out = function | Eq (a,b) -> Fmt.fprintf out "(@[=@ %a@ %a@])" pp_t a pp_t b | Not u -> Fmt.fprintf out "(@[not@ %a@])" pp_t u | Ite (a,b,c) -> Fmt.fprintf out "(@[ite@ %a@ %a@ %a@])" pp_t a pp_t b pp_t c - | LRA l -> pp_arith_gen ~pp_c:Q.pp_print ~pp_t out l - | LIA l -> pp_arith_gen ~pp_c:Z.pp_print ~pp_t out l + | LRA l -> pp_arith_gen ~pp_c:Q.pp_print ~pp_real:Q.pp_print ~pp_t out l + | LIA l -> pp_arith_gen ~pp_c:Z.pp_print ~pp_real:Q.pp_print ~pp_t out l let pp_term_top ~ids out t = let rec pp out t = @@ -604,8 +604,8 @@ module Term_cell : sig | Eq of 'a * 'a | Not of 'a | Ite of 'a * 'a * 'a - | LRA of (Q.t, 'a) arith_view - | LIA of (Z.t, 'a) arith_view + | LRA of (Q.t, Q.t, 'a) arith_view + | LIA of (Z.t, Q.t, 'a) arith_view type t = term view @@ -619,8 +619,8 @@ module Term_cell : sig val eq : term -> term -> t val not_ : term -> t val ite : term -> term -> term -> t - val lra : (Q.t,term) arith_view -> t - val lia : (Z.t,term) arith_view -> t + val lra : (Q.t,Q.t,term) arith_view -> t + val lia : (Z.t,Q.t,term) arith_view -> t val ty : t -> Ty.t (** Compute the type of this term cell. Not totally free *) @@ -649,8 +649,8 @@ end = struct | Eq of 'a * 'a | Not of 'a | Ite of 'a * 'a * 'a - | LRA of (Q.t, 'a) arith_view - | LIA of (Z.t, 'a) arith_view + | LRA of (Q.t, Q.t, 'a) arith_view + | LIA of (Z.t, Q.t, 'a) arith_view type t = term view @@ -668,7 +668,7 @@ end = struct let hash_q q = Hash.string (Q.to_string q) let hash_z = Z.hash - let hash_arith ~hash_c = function + let hash_arith ~hash_c ~hash_real = function | Arith_pred (p, a, b) -> Hash.combine4 81 (Hash.poly p) (sub_hash a) (sub_hash b) | Arith_op (p, a, b) -> @@ -680,7 +680,7 @@ end = struct | Arith_to_real x -> Hash.combine2 85 (sub_hash x) | Arith_simplex_var v -> Hash.combine2 99 (sub_hash v) | Arith_simplex_pred (v,op,q) -> - Hash.combine4 120 (sub_hash v) (Hash.poly op) (hash_c q) + Hash.combine4 120 (sub_hash v) (Hash.poly op) (hash_real q) let hash (t:A.t view) : int = match t with | Bool b -> Hash.bool b @@ -689,10 +689,10 @@ end = struct | Eq (a,b) -> Hash.combine3 12 (sub_hash a) (sub_hash b) | Not u -> Hash.combine2 70 (sub_hash u) | Ite (a,b,c) -> Hash.combine4 80 (sub_hash a)(sub_hash b)(sub_hash c) - | LRA l -> hash_arith ~hash_c:hash_q l - | LIA l -> hash_arith ~hash_c:hash_z l + | LRA l -> hash_arith ~hash_c:hash_q ~hash_real:hash_q l + | LIA l -> hash_arith ~hash_c:hash_z ~hash_real:hash_q l - let equal_arith ~eq_c l1 l2 = + let equal_arith ~eq_c ~eq_real l1 l2 = begin match l1, l2 with | Arith_pred (p1,a1,b1), Arith_pred (p2,a2,b2) -> p1 = p2 && sub_eq a1 a2 && sub_eq b1 b2 @@ -705,7 +705,7 @@ end = struct -> sub_eq x1 x2 | Arith_simplex_var v1, Arith_simplex_var v2 -> sub_eq v1 v2 | Arith_simplex_pred (v1,op1,q1), Arith_simplex_pred (v2,op2,q2) -> - sub_eq v1 v2 && (op1==op2) && eq_c q1 q2 + sub_eq v1 v2 && (op1==op2) && eq_real q1 q2 | (Arith_pred _ | Arith_op _ | Arith_const _ | Arith_simplex_var _ | Arith_mult _ | Arith_var _ | Arith_to_real _ | Arith_simplex_pred _), _ -> false @@ -720,8 +720,8 @@ end = struct | Not a, Not b -> sub_eq a b | Ite (a1,b1,c1), Ite (a2,b2,c2) -> sub_eq a1 a2 && sub_eq b1 b2 && sub_eq c1 c2 - | LRA l1, LRA l2 -> equal_arith ~eq_c:Q.equal l1 l2 - | LIA l1, LIA l2 -> equal_arith ~eq_c:Z.equal l1 l2 + | LRA l1, LRA l2 -> equal_arith ~eq_c:Q.equal ~eq_real:Q.equal l1 l2 + | LIA l1, LIA l2 -> equal_arith ~eq_c:Z.equal ~eq_real:Q.equal l1 l2 | (Bool _ | App_fun _ | Eq _ | Not _ | Ite _ | LRA _ | LIA _), _ -> false @@ -820,8 +820,8 @@ end = struct | Not u -> Not (f u) | Eq (a,b) -> Eq (f a, f b) | Ite (a,b,c) -> Ite (f a, f b, f c) - | LRA l -> LRA (map_arith_view ~f_c:CCFun.id f l) - | LIA l -> LIA (map_arith_view ~f_c:CCFun.id f l) + | LRA l -> LRA (map_arith_view ~f_c:CCFun.id ~f_real:CCFun.id f l) + | LIA l -> LIA (map_arith_view ~f_c:CCFun.id ~f_real:CCFun.id f l) end (** Term creation and manipulation *) @@ -838,8 +838,8 @@ module Term : sig | Eq of 'a * 'a | Not of 'a | Ite of 'a * 'a * 'a - | LRA of (Q.t,'a) arith_view - | LIA of (Z.t,'a) arith_view + | LRA of (Q.t, Q.t, 'a) arith_view + | LIA of (Z.t, Q.t, 'a) arith_view val id : t -> int val view : t -> term view @@ -875,8 +875,8 @@ module Term : sig val select : store -> select -> t -> t val app_cstor : store -> cstor -> t IArray.t -> t val is_a : store -> cstor -> t -> t - val lra : store -> (Q.t,t) arith_view -> t - val lia : store -> (Z.t,t) arith_view -> t + val lra : store -> (Q.t, Q.t, t) arith_view -> t + val lia : store -> (Z.t, Q.t, t) arith_view -> t module type ARITH_HELPER = sig type num @@ -948,8 +948,8 @@ end = struct | Eq of 'a * 'a | Not of 'a | Ite of 'a * 'a * 'a - | LRA of (Q.t,'a) arith_view - | LIA of (Z.t,'a) arith_view + | LRA of (Q.t, Q.t, 'a) arith_view + | LIA of (Z.t, Q.t, 'a) arith_view let[@inline] id t = t.term_id let[@inline] ty t = t.term_ty @@ -1012,12 +1012,12 @@ end = struct let is_a st c t : t = app_fun st (Fun.is_a c) (IArray.singleton t) let app_cstor st c args : t = app_fun st (Fun.cstor c) args - let[@inline] lra (st:store) (l:(Q.t,t) arith_view) : t = + let[@inline] lra (st:store) (l:(Q.t,Q.t,t) arith_view) : t = match l with | Arith_var x -> x (* normalize *) | _ -> make st (Term_cell.lra l) - let[@inline] lia (st:store) (l:(Z.t,t) arith_view) : t = + let[@inline] lia (st:store) (l:(Z.t,Q.t,t) arith_view) : t = match l with | Arith_var x -> x (* normalize *) | _ -> make st (Term_cell.lia l) @@ -1158,8 +1158,8 @@ end = struct | Not u -> not_ tst (f u) | Eq (a,b) -> eq tst (f a) (f b) | Ite (a,b,c) -> ite tst (f a) (f b) (f c) - | LRA l -> lra tst (map_arith_view ~f_c:CCFun.id f l) - | LIA l -> lia tst (map_arith_view ~f_c:CCFun.id f l) + | LRA l -> lra tst (map_arith_view ~f_c:CCFun.id ~f_real:CCFun.id f l) + | LIA l -> lia tst (map_arith_view ~f_c:CCFun.id ~f_real:CCFun.id f l) let store_size tst = H.size tst.tbl let store_iter tst = H.to_iter tst.tbl diff --git a/src/lia/Sidekick_arith_lia.ml b/src/lia/Sidekick_arith_lia.ml index 5dbdee0b..e6031787 100644 --- a/src/lia/Sidekick_arith_lia.ml +++ b/src/lia/Sidekick_arith_lia.ml @@ -5,7 +5,9 @@ http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_LIA *) open Sidekick_core -include Intf +include Intf_lia + +module Linear_expr = Sidekick_simplex.Linear_expr module Make(A : ARG) : S with module A = A = struct module A = A @@ -15,72 +17,6 @@ module Make(A : ARG) : S with module A = A = struct module SI = A.S.Solver_internal module N = A.S.Solver_internal.CC.N - type state = { - stat: Stat.t; - proof: A.S.P.t; - tst: T.store; - ty_st: Ty.store; - local_eqs: (N.t * N.t) Backtrack_stack.t; (* inferred by the congruence closure *) - } - - let create ?(stat=Stat.create()) proof tst ty_st : state = - { stat; proof; tst; ty_st; - local_eqs=Backtrack_stack.create(); - } - - 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 _ -> ()); - () - - let create_and_setup si = - Log.debug 2 "(th-lia.setup)"; - let stat = SI.stats si in - let st = create ~stat (SI.proof si) (SI.tst si) (SI.ty_st si) in - - SI.on_preprocess si (fun _si _ t -> - let is_int_const t = match A.view_as_lia t with - | LIA_const _ -> true | _ -> false in - if A.has_ty_int t && not (is_int_const t) then ( - Log.debugf 10 (fun k->k "lia: has ty int %a" T.pp t); - SI.declare_pb_is_incomplete si; (* TODO: remove *) - - - ); None); - - SI.on_cc_post_merge si - (fun _ _ n1 n2 -> - if A.has_ty_int (N.term n1) then ( - Backtrack_stack.push st.local_eqs (n1, n2) - )); - st - - (* TODO - let stat = SI.stats si in - let st = create ~stat (SI.proof si) (SI.tst si) (SI.ty_st si) in - SI.add_simplifier si (simplify st); - SI.on_preprocess si (preproc_lra st); - SI.on_final_check si (final_check_ st); - SI.on_partial_check si (partial_check_ st); - SI.on_cc_is_subterm si (on_subterm st); - SI.on_cc_post_merge si - (fun _ _ n1 n2 -> - if A.has_ty_real (N.term n1) then ( - Backtrack_stack.push st.local_eqs (n1, n2) - )); - st - *) - - let theory = - A.S.mk_theory - ~name:"th-lia" - ~create_and_setup ~push_level ~pop_levels - () - - (* module Tag = struct type t = | By_def @@ -114,111 +50,139 @@ module Make(A : ARG) : S with module A = A = struct | _ -> None end - module LE_ = Linear_expr.Make(A.Q)(SimpVar) + module LE_ = Linear_expr.Make(A.Z)(SimpVar) module LE = LE_.Expr - module SimpSolver = Simplex2.Make(A.Q)(SimpVar) + module SimpSolver = Sidekick_simplex.Make(struct + module Z = A.Z + module Q = A.Q + module Var = SimpVar + let mk_lit _ _ _ = assert false + end) module Subst = SimpSolver.Subst module Comb_map = CCMap.Make(LE_.Comb) type state = { + stat: Stat.t; + proof: A.S.P.t; tst: T.store; ty_st: Ty.store; - proof: SI.P.t; - simps: T.t T.Tbl.t; (* cache *) - gensym: A.Gensym.t; - encoded_eqs: unit T.Tbl.t; (* [a=b] gets clause [a = b <=> (a >= b /\ a <= b)] *) - needs_th_combination: unit T.Tbl.t; (* terms that require theory combination *) - mutable encoded_le: T.t Comb_map.t; (* [le] -> var encoding [le] *) local_eqs: (N.t * N.t) Backtrack_stack.t; (* inferred by the congruence closure *) + mutable encoded_le: T.t Comb_map.t; (* [le] -> var encoding [le] *) + encoded_eqs: unit T.Tbl.t; (* [a=b] gets clause [a = b <=> (a >= b /\ a <= b)] *) + needs_th_combination: unit T.Tbl.t; simplex: SimpSolver.t; + gensym: A.Gensym.t; stat_th_comb: int Stat.counter; } let create ?(stat=Stat.create()) proof tst ty_st : state = - { tst; ty_st; - proof; - simps=T.Tbl.create 128; - gensym=A.Gensym.create tst; - encoded_eqs=T.Tbl.create 8; - needs_th_combination=T.Tbl.create 8; + { stat; proof; tst; ty_st; + local_eqs=Backtrack_stack.create(); encoded_le=Comb_map.empty; - local_eqs = Backtrack_stack.create(); - simplex=SimpSolver.create ~stat (); - stat_th_comb=Stat.mk_int stat "lra.th-comb"; + encoded_eqs=T.Tbl.create 16; + simplex=SimpSolver.create(); + needs_th_combination=T.Tbl.create 16; + stat_th_comb=Stat.mk_int stat "lia.th-comb"; + gensym=A.Gensym.create tst; } + 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 _ -> ()); + () + let fresh_term self ~pre ty = A.Gensym.fresh_term self.gensym ~pre ty let fresh_lit (self:state) ~mk_lit ~pre : Lit.t = let t = fresh_term ~pre self (Ty.bool self.ty_st) in mk_lit t - let pp_pred_def out (p,l1,l2) : unit = - Fmt.fprintf out "(@[%a@ :l1 %a@ :l2 %a@])" Predicate.pp p LE.pp l1 LE.pp l2 - (* turn the term into a linear expression. Apply [f] on leaves. *) let rec as_linexp ~f (t:T.t) : LE.t = let open LE.Infix in - match A.view_as_lra t with - | LRA_other _ -> LE.monomial1 (f t) - | LRA_pred _ | LRA_simplex_pred _ -> - Error.errorf "type error: in linexp, LRA predicate %a" T.pp t - | LRA_op (op, t1, t2) -> + match A.view_as_lia t with + | LIA_other _ -> LE.monomial1 (f t) + | LIA_pred _ | LIA_simplex_pred _ -> + Error.errorf "type error: in linexp, LIA predicate %a" T.pp t + | LIA_op (op, t1, t2) -> let t1 = as_linexp ~f t1 in let t2 = as_linexp ~f t2 in begin match op with | Plus -> t1 + t2 | Minus -> t1 - t2 end - | LRA_mult (n, x) -> + | LIA_mult (n, x) -> let t = as_linexp ~f x in LE.( n * t ) - | LRA_simplex_var v -> LE.monomial1 v - | LRA_const q -> LE.of_const q - + | LIA_simplex_var v -> LE.monomial1 v + | LIA_const q -> LE.of_const q let as_linexp_id = as_linexp ~f:CCFun.id + let mk_le_q (le:LE_.Comb.t) : _ list = + LE_.Comb.to_list le + |> List.rev_map (fun (c,x) -> A.Q.of_bigint c, x) + (* return a variable that is equal to [le_comb] in the simplex. *) let var_encoding_comb ~pre self (le_comb:LE_.Comb.t) : T.t = match LE_.Comb.as_singleton le_comb with - | Some (c, x) when A.Q.(c = one) -> x (* trivial linexp *) + | Some (c, x) when A.Z.(c = one) -> x (* trivial linexp *) | _ -> match Comb_map.find le_comb self.encoded_le with | x -> x (* already encoded that *) | exception Not_found -> (* new variable to represent [le_comb] *) - let proxy = fresh_term self ~pre (A.ty_lra self.tst) in + let proxy = fresh_term self ~pre (A.ty_int self.tst) in (* TODO: define proxy *) self.encoded_le <- Comb_map.add le_comb proxy self.encoded_le; Log.debugf 50 - (fun k->k "(@[lra.encode-le@ `%a`@ :into-var %a@])" LE_.Comb.pp le_comb T.pp proxy); + (fun k->k "(@[lia.encode-le@ `%a`@ :into-var %a@])" LE_.Comb.pp le_comb T.pp proxy); (* it's actually 0 *) if LE_.Comb.is_empty le_comb then ( - Log.debug 50 "(lra.encode-le.is-trivially-0)"; - SimpSolver.add_constraint self.simplex + Log.debug 50 "(lia.encode-le.is-trivially-0)"; + SimpSolver.add_constraint + self.simplex ~is_int:true ~on_propagate:(fun _ ~reason:_ -> ()) (SimpSolver.Constraint.leq proxy A.Q.zero) Tag.By_def; - SimpSolver.add_constraint self.simplex + SimpSolver.add_constraint + self.simplex ~is_int:true ~on_propagate:(fun _ ~reason:_ -> ()) (SimpSolver.Constraint.geq proxy A.Q.zero) Tag.By_def; ) else ( - LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb; - SimpSolver.define self.simplex proxy (LE_.Comb.to_list le_comb); + LE_.Comb.iter (fun v _ -> SimpSolver.add_var ~is_int:true self.simplex v) le_comb; + SimpSolver.define self.simplex proxy (mk_le_q le_comb); ); proxy - let add_clause_lra_ ?using (module PA:SI.PREPROCESS_ACTS) lits = - let pr = A.lemma_lra (Iter.of_list lits) PA.proof in + let add_clause_lia_ ?using (module PA:SI.PREPROCESS_ACTS) lits = + let pr = A.lemma_lia (Iter.of_list lits) PA.proof in let pr = match using with | None -> pr | Some using -> SI.P.lemma_rw_clause pr ~res:(Iter.of_list lits) ~using PA.proof in PA.add_clause lits pr + (* look for subterms of type Real, for they will need theory combination *) + let on_subterm (self:state) _ (t:T.t) : unit = + Log.debugf 50 (fun k->k "(@[lia.cc-on-subterm@ %a@])" T.pp t); + match A.view_as_lia t with + | LIA_other _ when not (A.has_ty_int t) -> () + | _ -> + if not (T.Tbl.mem self.needs_th_combination t) then ( + Log.debugf 5 (fun k->k "(@[lia.needs-th-combination@ %a@])" T.pp t); + T.Tbl.add self.needs_th_combination t () + ) + + let is_int_const t = match A.view_as_lia t with + | LIA_const _ -> true + | _ -> false + (* preprocess linear expressions away *) - let preproc_lra (self:state) si (module PA:SI.PREPROCESS_ACTS) + let preproc_lia (self:state) si (module PA:SI.PREPROCESS_ACTS) (t:T.t) : (T.t * SI.proof_step Iter.t) option = - Log.debugf 50 (fun k->k "(@[lra.preprocess@ %a@])" T.pp t); + Log.debugf 50 (fun k->k "(@[lia.preprocess@ %a@])" T.pp t); let tst = SI.tst si in (* preprocess subterm *) @@ -228,19 +192,24 @@ module Make(A : ARG) : S with module A = A = struct u in + if A.has_ty_int t && not (is_int_const t) then ( + Log.debugf 10 (fun k->k "(@[lia.has-int-ty@ %a@])" T.pp t); + SI.declare_pb_is_incomplete si; (* TODO: remove *) + ); + (* tell the CC this term exists *) let declare_term_to_cc t = Log.debugf 50 (fun k->k "(@[simplex2.declare-term-to-cc@ %a@])" T.pp t); ignore (SI.CC.add_term (SI.cc si) t : SI.CC.N.t); in - match A.view_as_lra t with - | LRA_pred ((Eq | Neq), t1, t2) -> + match A.view_as_lia t with + | LIA_pred ((Eq | Neq), t1, t2) -> (* the equality side. *) let t, _ = T.abs tst t in if not (T.Tbl.mem self.encoded_eqs t) then ( - let u1 = A.mk_lra tst (LRA_pred (Leq, t1, t2)) in - let u2 = A.mk_lra tst (LRA_pred (Geq, t1, t2)) in + let u1 = A.mk_lia tst (LIA_pred (Leq, t1, t2)) in + let u2 = A.mk_lia tst (LIA_pred (Geq, t1, t2)) in T.Tbl.add self.encoded_eqs t (); @@ -248,20 +217,20 @@ module Make(A : ARG) : S with module A = A = struct let lit_t = PA.mk_lit_nopreproc t in let lit_u1 = PA.mk_lit_nopreproc u1 in let lit_u2 = PA.mk_lit_nopreproc u2 in - add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u1]; - add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u2]; - add_clause_lra_ (module PA) + add_clause_lia_ (module PA) [SI.Lit.neg lit_t; lit_u1]; + add_clause_lia_ (module PA) [SI.Lit.neg lit_t; lit_u2]; + add_clause_lia_ (module PA) [SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t]; ); None - | LRA_pred (pred, t1, t2) -> + | LIA_pred (pred, t1, t2) -> let steps = ref [] in let l1 = as_linexp ~f:(preproc_t ~steps) t1 in let l2 = as_linexp ~f:(preproc_t ~steps) t2 in let le = LE.(l1 - l2) in let le_comb, le_const = LE.comb le, LE.const le in - let le_const = A.Q.neg le_const in + let le_const = A.Q.(neg @@ of_bigint le_const) in (* now we have [le_comb le_const] *) begin match LE_.Comb.as_singleton le_comb, pred with @@ -281,19 +250,21 @@ module Make(A : ARG) : S with module A = A = struct | Gt -> S_op.Gt in - let new_t = A.mk_lra tst (LRA_simplex_pred (proxy, op, le_const)) in + let new_t = A.mk_lia tst (LIA_simplex_pred (proxy, op, le_const)) in begin let lit = PA.mk_lit_nopreproc new_t in let constr = SimpSolver.Constraint.mk proxy op le_const in - SimpSolver.declare_bound self.simplex constr (Tag.Lit lit); + SimpSolver.declare_bound + self.simplex ~is_int:true + constr (Tag.Lit lit); end; - Log.debugf 10 (fun k->k "(@[lra.preprocess:@ %a@ :into %a@])" T.pp t T.pp new_t); + Log.debugf 10 (fun k->k "(@[lia.preprocess:@ %a@ :into %a@])" T.pp t T.pp new_t); Some (new_t, Iter.of_list !steps) | Some (coeff, v), pred -> - (* [c . v <= const] becomes a direct simplex constraint [v <= const/c] *) - let q = A.Q.( le_const / coeff ) in + (* [c . v <= const] becomes a direct (rational) simplex constraint [v <= const/c] *) + let const' = A.Q.( le_const / of_bigint coeff) in declare_term_to_cc v; let op = match pred with @@ -304,23 +275,26 @@ module Make(A : ARG) : S with module A = A = struct | Eq | Neq -> assert false in (* make sure to swap sides if multiplying with a negative coeff *) - let op = if A.Q.(coeff < zero) then S_op.neg_sign op else op in + let op = if A.Z.(coeff < zero) then S_op.neg_sign op else op in - let new_t = A.mk_lra tst (LRA_simplex_pred (v, op, q)) in + (* normalize to get an integer coeff *) + + let new_t = A.mk_lia tst (LIA_simplex_pred (v, op, const')) in begin let lit = PA.mk_lit_nopreproc new_t in - let constr = SimpSolver.Constraint.mk v op q in + let constr = SimpSolver.Constraint.mk v op const' in SimpSolver.declare_bound self.simplex constr (Tag.Lit lit); end; - Log.debugf 10 (fun k->k "lra.preprocess@ :%a@ :into %a" T.pp t T.pp new_t); + Log.debugf 10 (fun k->k "lia.preprocess@ :%a@ :into %a" T.pp t T.pp new_t); Some (new_t, Iter.of_list !steps) end - | LRA_op _ | LRA_mult _ -> + | LIA_op _ | LIA_mult _ -> let steps = ref [] in let le = as_linexp ~f:(preproc_t ~steps) t in let le_comb, le_const = LE.comb le, LE.const le in + let le_const = A.Q.of_bigint le_const in if A.Q.(le_const = zero) then ( (* if there is no constant, define [proxy] as [proxy := le_comb] and @@ -346,67 +320,66 @@ module Make(A : ARG) : S with module A = A = struct end; let proxy2 = fresh_term self ~pre:"_le_diff" (T.ty t) in let pr_def2 = - SI.P.define_term proxy (A.mk_lra tst (LRA_op (Minus, t, proxy))) PA.proof + SI.P.define_term proxy (A.mk_lia tst (LIA_op (Minus, t, proxy))) PA.proof in SimpSolver.add_var self.simplex proxy; LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb; SimpSolver.define self.simplex proxy2 - ((A.Q.minus_one, proxy) :: LE_.Comb.to_list le_comb); + ((A.Q.minus_one, proxy) :: mk_le_q le_comb); Log.debugf 50 - (fun k->k "(@[lra.encode-le.with-offset@ %a@ :var %a@ :diff-var %a@])" + (fun k->k "(@[lia.encode-le.with-offset@ %a@ :var %a@ :diff-var %a@])" LE_.Comb.pp le_comb T.pp proxy T.pp proxy2); declare_term_to_cc proxy; declare_term_to_cc proxy2; - add_clause_lra_ ~using:Iter.(return pr_def2) (module PA) [ - PA.mk_lit_nopreproc (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const))) + add_clause_lia_ ~using:Iter.(return pr_def2) (module PA) [ + PA.mk_lit_nopreproc (A.mk_lia tst (LIA_simplex_pred (proxy2, Leq, A.Q.neg le_const))) ]; - add_clause_lra_ ~using:Iter.(return pr_def2) (module PA) [ - PA.mk_lit_nopreproc (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const))) + add_clause_lia_ ~using:Iter.(return pr_def2) (module PA) [ + PA.mk_lit_nopreproc (A.mk_lia tst (LIA_simplex_pred (proxy2, Geq, A.Q.neg le_const))) ]; Some (proxy, Iter.of_list !steps) ) - | LRA_other t when A.has_ty_real t -> None - | LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ -> + | LIA_other t when A.has_ty_int t -> None + | LIA_const _ | LIA_simplex_pred _ | LIA_simplex_var _ | LIA_other _ -> None let simplify (self:state) (_recurse:_) (t:T.t) : (T.t * SI.proof_step Iter.t) option = - let proof_eq t u = - A.lemma_lra + A.lemma_lia (Iter.return (SI.Lit.atom self.tst (A.mk_eq self.tst t u))) self.proof in let proof_bool t ~sign:b = let lit = SI.Lit.atom ~sign:b self.tst t in - A.lemma_lra (Iter.return lit) self.proof + A.lemma_lia (Iter.return lit) self.proof in - match A.view_as_lra t with - | LRA_op _ | LRA_mult _ -> + match A.view_as_lia t with + | LIA_op _ | LIA_mult _ -> let le = as_linexp_id t in if LE.is_const le then ( let c = LE.const le in - let u = A.mk_lra self.tst (LRA_const c) in + let u = A.mk_lia self.tst (LIA_const c) in let pr = proof_eq t u in Some (u, Iter.return pr) ) else None - | LRA_pred (pred, l1, l2) -> + | LIA_pred (pred, l1, l2) -> let le = LE.(as_linexp_id l1 - as_linexp_id l2) in if LE.is_const le then ( let c = LE.const le in let is_true = match pred with - | Leq -> A.Q.(c <= zero) - | Geq -> A.Q.(c >= zero) - | Lt -> A.Q.(c < zero) - | Gt -> A.Q.(c > zero) - | Eq -> A.Q.(c = zero) - | Neq -> A.Q.(c <> zero) + | Leq -> A.Z.(c <= zero) + | Geq -> A.Z.(c >= zero) + | Lt -> A.Z.(c < zero) + | Gt -> A.Z.(c > zero) + | Eq -> A.Z.(c = zero) + | Neq -> A.Z.(c <> zero) in let u = A.mk_bool self.tst is_true in let pr = proof_bool t ~sign:is_true in @@ -414,7 +387,16 @@ module Make(A : ARG) : S with module A = A = struct ) else None | _ -> None - module Q_map = CCMap.Make(A.Q) + let on_propagate_ si acts lit ~reason = + match lit with + | Tag.Lit lit -> + (* TODO: more detailed proof certificate *) + SI.propagate si acts lit + ~reason:(fun() -> + let lits = CCList.flat_map (Tag.to_lits si) reason in + let pr = A.lemma_lia Iter.(cons lit (of_list lits)) (SI.proof si) in + CCList.flat_map (Tag.to_lits si) reason, pr) + | _ -> () (* raise conflict from certificate *) let fail_with_cert si acts cert : 'a = @@ -424,24 +406,15 @@ module Make(A : ARG) : S with module A = A = struct |> CCList.flat_map (Tag.to_lits si) |> List.rev_map SI.Lit.neg in - let pr = A.lemma_lra (Iter.of_list confl) (SI.proof si) in + let pr = A.lemma_lia (Iter.of_list confl) (SI.proof si) in SI.raise_conflict si acts confl pr - let on_propagate_ si acts lit ~reason = - match lit with - | Tag.Lit lit -> - (* TODO: more detailed proof certificate *) - SI.propagate si acts lit - ~reason:(fun() -> - let lits = CCList.flat_map (Tag.to_lits si) reason in - let pr = A.lemma_lra Iter.(cons lit (of_list lits)) (SI.proof si) in - CCList.flat_map (Tag.to_lits si) reason, pr) - | _ -> () + module Q_map = CCMap.Make(A.Q) let check_simplex_ self si acts : SimpSolver.Subst.t = - Log.debug 5 "(lra.check-simplex)"; + Log.debug 5 "(lia.check-simplex)"; let res = - Profile.with_ "simplex.solve" + Profile.with_ "lia.simplex.solve" (fun () -> SimpSolver.check self.simplex ~on_propagate:(on_propagate_ si acts)) @@ -450,32 +423,75 @@ module Make(A : ARG) : S with module A = A = struct | SimpSolver.Sat m -> m | SimpSolver.Unsat cert -> Log.debugf 10 - (fun k->k "(@[lra.check.unsat@ :cert %a@])" + (fun k->k "(@[lia.check.unsat@ :cert %a@])" SimpSolver.Unsat_cert.pp cert); fail_with_cert si acts cert end - (* TODO: trivial propagations *) + (* partial checks is where we add literals from the trail to the + simplex. *) + let partial_check_ self si acts trail : unit = + Profile.with_ "lia.partial-check" @@ fun () -> + + let changed = ref false in + trail + (fun lit -> + let sign = SI.Lit.sign lit in + let lit_t = SI.Lit.term lit in + Log.debugf 50 (fun k->k "(@[lia.partial-check.add@ :lit %a@ :lit-t %a@])" + SI.Lit.pp lit T.pp lit_t); + match A.view_as_lia lit_t with + | LIA_simplex_pred (v, op, q) -> + + (* need to account for the literal's sign *) + let op = if sign then op else S_op.not_ op in + + (* assert new constraint to Simplex *) + let constr = SimpSolver.Constraint.mk v op q in + Log.debugf 10 + (fun k->k "(@[lia.partial-check.assert@ %a@])" + SimpSolver.Constraint.pp constr); + begin + changed := true; + try + SimpSolver.add_var self.simplex v; + SimpSolver.add_constraint + self.simplex ~is_int:true + constr (Tag.Lit lit) + ~on_propagate:(on_propagate_ si acts); + with SimpSolver.E_unsat cert -> + Log.debugf 10 + (fun k->k "(@[lia.partial-check.unsat@ :cert %a@])" + SimpSolver.Unsat_cert.pp cert); + fail_with_cert si acts cert + end + | _ -> ()); + + (* incremental check *) + if !changed then ( + ignore (check_simplex_ self si acts : SimpSolver.Subst.t); + ); + () let add_local_eq (self:state) si acts n1 n2 : unit = - Log.debugf 20 (fun k->k "(@[lra.add-local-eq@ %a@ %a@])" N.pp n1 N.pp n2); + Log.debugf 20 (fun k->k "(@[lia.add-local-eq@ %a@ %a@])" N.pp n1 N.pp n2); let t1 = N.term n1 in let t2 = N.term n2 in let t1, t2 = if T.compare t1 t2 > 0 then t2, t1 else t1, t2 in let le = LE.(as_linexp_id t1 - as_linexp_id t2) in let le_comb, le_const = LE.comb le, LE.const le in - let le_const = A.Q.neg le_const in + let le_const = A.Z.neg le_const in let v = var_encoding_comb ~pre:"le_local_eq" self le_comb in let lit = Tag.CC_eq (n1,n2) in begin try - let c1 = SimpSolver.Constraint.geq v le_const in - SimpSolver.add_constraint self.simplex c1 lit + let c1 = SimpSolver.Constraint.geq v (A.Q.of_bigint le_const) in + SimpSolver.add_constraint self.simplex ~is_int:true c1 lit ~on_propagate:(on_propagate_ si acts); - let c2 = SimpSolver.Constraint.leq v le_const in - SimpSolver.add_constraint self.simplex c2 lit + let c2 = SimpSolver.Constraint.leq v (A.Q.of_bigint le_const) in + SimpSolver.add_constraint self.simplex ~is_int:true c2 lit ~on_propagate:(on_propagate_ si acts); with SimpSolver.E_unsat cert -> fail_with_cert si acts cert @@ -485,13 +501,13 @@ module Make(A : ARG) : S with module A = A = struct (* theory combination: add decisions [t=u] whenever [t] and [u] have the same value in [subst] and both occur under function symbols *) let do_th_combination (self:state) si acts (subst:Subst.t) : unit = - Log.debug 5 "(lra.do-th-combinations)"; + Log.debug 5 "(lia.do-th-combinations)"; let n_th_comb = T.Tbl.keys self.needs_th_combination |> Iter.length in if n_th_comb > 0 then ( Log.debugf 5 - (fun k->k "(@[LRA.needs-th-combination@ :n-lits %d@])" n_th_comb); + (fun k->k "(@[lia.needs-th-combination@ :n-lits %d@])" n_th_comb); Log.debugf 50 - (fun k->k "(@[LRA.needs-th-combination@ :terms [@[%a@]]@])" + (fun k->k "(@[lia.needs-th-combination@ :terms [@[%a@]]@])" (Util.pp_iter @@ Fmt.within "`" "`" T.pp) (T.Tbl.keys self.needs_th_combination)); ); @@ -518,7 +534,7 @@ module Make(A : ARG) : S with module A = A = struct |> List.iter (fun (t1,t2) -> Log.debugf 50 - (fun k->k "(@[LRA.th-comb.check-pair[val=%a]@ %a@ %a@])" + (fun k->k "(@[lia.th-comb.check-pair[val=%a]@ %a@ %a@])" A.Q.pp _q T.pp t1 T.pp t2); assert(SI.cc_mem_term si t1); assert(SI.cc_mem_term si t2); @@ -526,9 +542,9 @@ module Make(A : ARG) : S with module A = A = struct closure, and are not equal in it yet, add [t1=t2] as the next decision to do *) if not (SI.cc_are_equal si t1 t2) then ( - Log.debug 50 "LRA.th-comb.must-decide-equal"; + Log.debug 50 "lia.th-comb.must-decide-equal"; Stat.incr self.stat_th_comb; - Profile.instant "lra.th-comb-assert-eq"; + Profile.instant "lia.th-comb-assert-eq"; let t = A.mk_eq (SI.tst si) t1 t2 in let lit = SI.mk_lit si acts t in @@ -541,52 +557,9 @@ module Make(A : ARG) : S with module A = A = struct end; () - (* partial checks is where we add literals from the trail to the - simplex. *) - let partial_check_ self si acts trail : unit = - Profile.with_ "lra.partial-check" @@ fun () -> - - let changed = ref false in - trail - (fun lit -> - let sign = SI.Lit.sign lit in - let lit_t = SI.Lit.term lit in - Log.debugf 50 (fun k->k "(@[lra.partial-check.add@ :lit %a@ :lit-t %a@])" - SI.Lit.pp lit T.pp lit_t); - match A.view_as_lra lit_t with - | LRA_simplex_pred (v, op, q) -> - - (* need to account for the literal's sign *) - let op = if sign then op else S_op.not_ op in - - (* assert new constraint to Simplex *) - let constr = SimpSolver.Constraint.mk v op q in - Log.debugf 10 - (fun k->k "(@[lra.partial-check.assert@ %a@])" - SimpSolver.Constraint.pp constr); - begin - changed := true; - try - SimpSolver.add_var self.simplex v; - SimpSolver.add_constraint self.simplex constr (Tag.Lit lit) - ~on_propagate:(on_propagate_ si acts); - with SimpSolver.E_unsat cert -> - Log.debugf 10 - (fun k->k "(@[lra.partial-check.unsat@ :cert %a@])" - SimpSolver.Unsat_cert.pp cert); - fail_with_cert si acts cert - end - | _ -> ()); - - (* incremental check *) - if !changed then ( - ignore (check_simplex_ self si acts : SimpSolver.Subst.t); - ); - () - let final_check_ (self:state) si (acts:SI.theory_actions) (_trail:_ Iter.t) : unit = - Log.debug 5 "(th-lra.final-check)"; - Profile.with_ "lra.final-check" @@ fun () -> + Log.debug 5 "(th-lia.final-check)"; + Profile.with_ "lia.final-check" @@ fun () -> (* add congruence closure equalities *) Backtrack_stack.iter self.local_eqs @@ -595,20 +568,53 @@ module Make(A : ARG) : S with module A = A = struct (* TODO: jiggle model to reduce the number of variables that have the same value *) let model = check_simplex_ self si acts in - Log.debugf 20 (fun k->k "(@[lra.model@ %a@])" SimpSolver.Subst.pp model); - Log.debug 5 "(lra: solver returns SAT)"; + Log.debugf 20 (fun k->k "(@[lia.model@ %a@])" SimpSolver.Subst.pp model); + Log.debug 5 "(lia: solver returns SAT)"; do_th_combination self si acts model; () - (* look for subterms of type Real, for they will need theory combination *) - let on_subterm (self:state) _ (t:T.t) : unit = - Log.debugf 50 (fun k->k "(@[lra.cc-on-subterm@ %a@])" T.pp t); - match A.view_as_lra t with - | LRA_other _ when not (A.has_ty_real t) -> () - | _ -> - if not (T.Tbl.mem self.needs_th_combination t) then ( - Log.debugf 5 (fun k->k "(@[lra.needs-th-combination@ %a@])" T.pp t); - T.Tbl.add self.needs_th_combination t () - ) - *) + (* raise conflict from certificate *) + let fail_with_cert si acts cert : 'a = + Profile.with1 "simplex.check-cert" SimpSolver._check_cert cert; + let confl = + SimpSolver.Unsat_cert.lits cert + |> CCList.flat_map (Tag.to_lits si) + |> List.rev_map SI.Lit.neg + in + let pr = A.lemma_lia (Iter.of_list confl) (SI.proof si) in + SI.raise_conflict si acts confl pr + + let on_propagate_ si acts lit ~reason = + match lit with + | Tag.Lit lit -> + (* TODO: more detailed proof certificate *) + SI.propagate si acts lit + ~reason:(fun() -> + let lits = CCList.flat_map (Tag.to_lits si) reason in + let pr = A.lemma_lia Iter.(cons lit (of_list lits)) (SI.proof si) in + CCList.flat_map (Tag.to_lits si) reason, pr) + | _ -> () + + let create_and_setup si = + Log.debug 2 "(th-lia.setup)"; + let stat = SI.stats si in + let st = create ~stat (SI.proof si) (SI.tst si) (SI.ty_st si) in + + SI.add_simplifier si (simplify st); + SI.on_preprocess si (preproc_lia st); + SI.on_cc_is_subterm si (on_subterm st); + SI.on_final_check si (final_check_ st); + SI.on_partial_check si (partial_check_ st); + SI.on_cc_post_merge si + (fun _ _ n1 n2 -> + if A.has_ty_int (N.term n1) then ( + Backtrack_stack.push st.local_eqs (n1, n2) + )); + 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 index 0880740e..ddbdc9aa 100644 --- a/src/lia/Sidekick_arith_lia.mli +++ b/src/lia/Sidekick_arith_lia.mli @@ -6,6 +6,6 @@ http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_LIA *) open Sidekick_core -include module type of Intf +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 index 35103ce4..bca33df2 100644 --- a/src/lia/dune +++ b/src/lia/dune @@ -3,4 +3,4 @@ (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)) + (libraries containers sidekick.core sidekick.arith sidekick.simplex)) diff --git a/src/lia/intf.ml b/src/lia/intf_lia.ml similarity index 67% rename from src/lia/intf.ml rename to src/lia/intf_lia.ml index edac658f..df7268e5 100644 --- a/src/lia/intf.ml +++ b/src/lia/intf_lia.ml @@ -4,17 +4,17 @@ open Sidekick_core module type RATIONAL = Sidekick_arith.RATIONAL module type INT = Sidekick_arith.INT -module S_op = Sidekick_arith_lra.S_op -type pred = Sidekick_arith_lra.pred = Leq | Geq | Lt | Gt | Eq | Neq -type op = Sidekick_arith_lra.op = Plus | Minus +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, 'a) lia_view = +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_simplex_var of 'a (* an opaque variable *) - | LIA_simplex_pred of 'a * S_op.t * 'num (* an atomic constraint *) + | LIA_simplex_pred of 'a * S_op.t * 'real (* an atomic constraint *) | LIA_other of 'a let map_view f (l:_ lia_view) : _ lia_view = @@ -31,15 +31,13 @@ let map_view f (l:_ lia_view) : _ lia_view = module type ARG = sig module S : Sidekick_core.SOLVER - module Q : RATIONAL module Z : INT - - module LRA : Sidekick_arith_lra.S + module Q : RATIONAL with type bigint = Z.t type term = S.T.Term.t type ty = S.T.Ty.t - val view_as_lia : term -> (Z.t, term) lia_view + 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 @@ -47,7 +45,7 @@ module type ARG = sig 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, term) lia_view -> term + 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 @@ -59,6 +57,19 @@ module type ARG = sig (** Does this term have the type [Int] *) val lemma_lia : S.Lit.t Iter.t -> S.P.proof_rule + + module Gensym : sig + type t + + val create : S.T.Term.store -> t + + val tst : t -> S.T.Term.store + + val copy : t -> t + + val fresh_term : t -> pre:string -> S.T.Ty.t -> term + (** Make a fresh term of the given type *) + end end module type S = sig diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml index fa63fd98..78b082bc 100644 --- a/src/lra/sidekick_arith_lra.ml +++ b/src/lra/sidekick_arith_lra.ml @@ -40,7 +40,8 @@ let map_view f (l:_ lra_view) : _ lra_view = module type ARG = sig module S : Sidekick_core.SOLVER - module Q : RATIONAL + module Z : INT + module Q : RATIONAL with type bigint = Z.t type term = S.T.Term.t type ty = S.T.Ty.t @@ -154,6 +155,7 @@ module Make(A : ARG) : S with module A = A = struct module LE_ = Linear_expr.Make(A.Q)(SimpVar) module LE = LE_.Expr module SimpSolver = Sidekick_simplex.Make(struct + module Z = A.Z module Q = A.Q module Var = SimpVar let mk_lit _ _ _ = assert false diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index a138cd63..86b7e940 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -135,7 +135,7 @@ let cast_to_real (ctx:Ctx.t) (t:T.t) : T.t = T.lra ctx.tst (Arith_const (Q.of_bigint n)) | T.LIA l -> (* try to convert the whole structure to reals *) - let l = Base_types.map_arith_view ~f_c:Q.of_bigint conv l in + let l = Base_types.map_arith_view ~f_c:Q.of_bigint ~f_real:CCFun.id conv l in T.lra ctx.tst l | _ -> errorf_ctx ctx "cannot cast term to real@ :term %a" T.pp t