simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-11 21:48:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

wip: LIA theory

Browse source
This commit is contained in:
Simon Cruanes 2022-01-13 12:54:35 -05:00
parent 7f2e92fe88
commit 4b2afd7a05
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
8 changed files with 326 additions and 304 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
src/base-solver/sidekick_base_solver.ml
View file

@ -76,10 +76,29 @@ module Th_bool = Sidekick_th_bool_static.Make(struct
let lemma_ite_false = Proof.lemma_ite_false let lemma_ite_false = Proof.lemma_ite_false
end) 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 *) (** Theory of Linear Rational Arithmetic *)
module Th_lra = Sidekick_arith_lra.Make(struct module Th_lra = Sidekick_arith_lra.Make(struct
module S = Solver module S = Solver
module T = Term module T = Term
module Z = Sidekick_zarith.Int
module Q = Sidekick_zarith.Rational module Q = Sidekick_zarith.Rational
type term = S.T.Term.t type term = S.T.Term.t
type ty = S.T.Ty.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 has_ty_real t = Ty.equal (T.ty t) (Ty.real())
let lemma_lra = Proof.lemma_lra let lemma_lra = Proof.lemma_lra
module Gensym = Gensym
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
end) end)
module Th_lia = Sidekick_arith_lia.Make(struct module Th_lia = Sidekick_arith_lia.Make(struct
module S = Solver module S = Solver
module T = Term module T = Term
module Q = Sidekick_zarith.Rational
module Z = Sidekick_zarith.Int module Z = Sidekick_zarith.Int
module Q = Sidekick_zarith.Rational
type term = S.T.Term.t type term = S.T.Term.t
type ty = S.T.Ty.t type ty = S.T.Ty.t
module LRA = Th_lra
module LIA = Sidekick_arith_lia module LIA = Sidekick_arith_lia
let mk_eq = Form.eq 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 has_ty_int t = Ty.equal (T.ty t) (Ty.int())
let lemma_lia = Proof.lemma_lia let lemma_lia = Proof.lemma_lia
module Gensym = Gensym
end) end)
let th_bool : Solver.theory = Th_bool.theory let th_bool : Solver.theory = Th_bool.theory

72
src/base/Base_types.ml
View file

@ -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_pred = Sidekick_arith_lra.Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq
type lra_op = Sidekick_arith_lra.op = Plus | Minus 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_pred of lra_pred * 'a * 'a
| Arith_op of lra_op * 'a * 'a | Arith_op of lra_op * 'a * 'a
| Arith_mult of 'num * 'a | Arith_mult of 'num * 'a
@ -20,10 +20,10 @@ type ('num, 'a) arith_view =
| Arith_to_real of 'a | Arith_to_real of 'a
(* after preprocessing *) (* 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 | 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 begin match l with
| Arith_pred (p, a, b) -> Arith_pred (p, f a, f b) | Arith_pred (p, a, b) -> Arith_pred (p, f a, f b)
| Arith_op (p, a, b) -> Arith_op (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_var x -> Arith_var (f x)
| Arith_to_real x -> Arith_to_real (f x) | Arith_to_real x -> Arith_to_real (f x)
| Arith_simplex_var v -> Arith_simplex_var (f v) | 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 end
let iter_arith_view f l : unit = let iter_arith_view f l : unit =
@ -64,8 +64,8 @@ and 'a term_view =
| Eq of 'a * 'a | Eq of 'a * 'a
| Not of 'a | Not of 'a
| Ite of 'a * 'a * 'a | Ite of 'a * 'a * 'a
| LRA of (Q.t, 'a) arith_view | LRA of (Q.t, Q.t, 'a) arith_view
| LIA of (Z.t, 'a) arith_view | LIA of (Z.t, Q.t, 'a) arith_view
and fun_ = { and fun_ = {
fun_id: ID.t; fun_id: ID.t;
@ -258,7 +258,7 @@ let string_of_lra_op = function
| Minus -> "-" | Minus -> "-"
let pp_lra_op out p = Fmt.string out (string_of_lra_op p) 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) -> | Arith_pred (p, a, b) ->
Fmt.fprintf out "(@[%s@ %a@ %a@])" (string_of_lra_pred p) pp_t a pp_t b Fmt.fprintf out "(@[%s@ %a@ %a@])" (string_of_lra_pred p) pp_t a pp_t b
| Arith_op (p, a, 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_var v -> pp_t out v
| Arith_simplex_pred (v, op, c) -> | Arith_simplex_pred (v, op, c) ->
Fmt.fprintf out "(@[%a@ %s %a@])" 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 let pp_term_view_gen ~pp_id ~pp_t out = function
| Bool true -> Fmt.string out "true" | 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 "(@[<hv>=@ %a@ %a@])" pp_t a pp_t b | Eq (a,b) -> Fmt.fprintf out "(@[<hv>=@ %a@ %a@])" pp_t a pp_t b
| Not u -> Fmt.fprintf out "(@[not@ %a@])" pp_t u | 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 | 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 | 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_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 pp_term_top ~ids out t =
let rec pp out t = let rec pp out t =
@ -604,8 +604,8 @@ module Term_cell : sig
| Eq of 'a * 'a | Eq of 'a * 'a
| Not of 'a | Not of 'a
| Ite of 'a * 'a * 'a | Ite of 'a * 'a * 'a
| LRA of (Q.t, 'a) arith_view | LRA of (Q.t, Q.t, 'a) arith_view
| LIA of (Z.t, 'a) arith_view | LIA of (Z.t, Q.t, 'a) arith_view
type t = term view type t = term view
@ -619,8 +619,8 @@ module Term_cell : sig
val eq : term -> term -> t val eq : term -> term -> t
val not_ : term -> t val not_ : term -> t
val ite : term -> term -> term -> t val ite : term -> term -> term -> t
val lra : (Q.t,term) arith_view -> t val lra : (Q.t,Q.t,term) arith_view -> t
val lia : (Z.t,term) arith_view -> t val lia : (Z.t,Q.t,term) arith_view -> t
val ty : t -> Ty.t val ty : t -> Ty.t
(** Compute the type of this term cell. Not totally free *) (** Compute the type of this term cell. Not totally free *)
@ -649,8 +649,8 @@ end = struct
| Eq of 'a * 'a | Eq of 'a * 'a
| Not of 'a | Not of 'a
| Ite of 'a * 'a * 'a | Ite of 'a * 'a * 'a
| LRA of (Q.t, 'a) arith_view | LRA of (Q.t, Q.t, 'a) arith_view
| LIA of (Z.t, 'a) arith_view | LIA of (Z.t, Q.t, 'a) arith_view
type t = term view type t = term view
@ -668,7 +668,7 @@ end = struct
let hash_q q = Hash.string (Q.to_string q) let hash_q q = Hash.string (Q.to_string q)
let hash_z = Z.hash let hash_z = Z.hash
let hash_arith ~hash_c = function let hash_arith ~hash_c ~hash_real = function
| Arith_pred (p, a, b) -> | Arith_pred (p, a, b) ->
Hash.combine4 81 (Hash.poly p) (sub_hash a) (sub_hash b) Hash.combine4 81 (Hash.poly p) (sub_hash a) (sub_hash b)
| Arith_op (p, a, b) -> | Arith_op (p, a, b) ->
@ -680,7 +680,7 @@ end = struct
| Arith_to_real x -> Hash.combine2 85 (sub_hash x) | Arith_to_real x -> Hash.combine2 85 (sub_hash x)
| Arith_simplex_var v -> Hash.combine2 99 (sub_hash v) | Arith_simplex_var v -> Hash.combine2 99 (sub_hash v)
| Arith_simplex_pred (v,op,q) -> | 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 let hash (t:A.t view) : int = match t with
| Bool b -> Hash.bool b | Bool b -> Hash.bool b
@ -689,10 +689,10 @@ end = struct
| Eq (a,b) -> Hash.combine3 12 (sub_hash a) (sub_hash b) | Eq (a,b) -> Hash.combine3 12 (sub_hash a) (sub_hash b)
| Not u -> Hash.combine2 70 (sub_hash u) | Not u -> Hash.combine2 70 (sub_hash u)
| Ite (a,b,c) -> Hash.combine4 80 (sub_hash a)(sub_hash b)(sub_hash c) | 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 | LRA l -> hash_arith ~hash_c:hash_q ~hash_real:hash_q l
| LIA l -> hash_arith ~hash_c:hash_z 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 begin match l1, l2 with
| Arith_pred (p1,a1,b1), Arith_pred (p2,a2,b2) -> | Arith_pred (p1,a1,b1), Arith_pred (p2,a2,b2) ->
p1 = p2 && sub_eq a1 a2 && sub_eq b1 b2 p1 = p2 && sub_eq a1 a2 && sub_eq b1 b2
@ -705,7 +705,7 @@ end = struct
-> sub_eq x1 x2 -> sub_eq x1 x2
| Arith_simplex_var v1, Arith_simplex_var v2 -> sub_eq v1 v2 | Arith_simplex_var v1, Arith_simplex_var v2 -> sub_eq v1 v2
| Arith_simplex_pred (v1,op1,q1), Arith_simplex_pred (v2,op2,q2) -> | 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_pred _ | Arith_op _ | Arith_const _ | Arith_simplex_var _
| Arith_mult _ | Arith_var _ | Arith_mult _ | Arith_var _
| Arith_to_real _ | Arith_simplex_pred _), _ -> false | Arith_to_real _ | Arith_simplex_pred _), _ -> false
@ -720,8 +720,8 @@ end = struct
| Not a, Not b -> sub_eq a b | Not a, Not b -> sub_eq a b
| Ite (a1,b1,c1), Ite (a2,b2,c2) -> | Ite (a1,b1,c1), Ite (a2,b2,c2) ->
sub_eq a1 a2 && sub_eq b1 b2 && sub_eq c1 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 | 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 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 _), _ | (Bool _ | App_fun _ | Eq _ | Not _ | Ite _ | LRA _ | LIA _), _
-> false -> false
@ -820,8 +820,8 @@ end = struct
| Not u -> Not (f u) | Not u -> Not (f u)
| Eq (a,b) -> Eq (f a, f b) | Eq (a,b) -> Eq (f a, f b)
| Ite (a,b,c) -> Ite (f a, f b, f c) | Ite (a,b,c) -> Ite (f a, f b, f c)
| LRA l -> LRA (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 l) | LIA l -> LIA (map_arith_view ~f_c:CCFun.id ~f_real:CCFun.id f l)
end end
(** Term creation and manipulation *) (** Term creation and manipulation *)
@ -838,8 +838,8 @@ module Term : sig
| Eq of 'a * 'a | Eq of 'a * 'a
| Not of 'a | Not of 'a
| Ite of 'a * 'a * 'a | Ite of 'a * 'a * 'a
| LRA of (Q.t,'a) arith_view | LRA of (Q.t, Q.t, 'a) arith_view
| LIA of (Z.t,'a) arith_view | LIA of (Z.t, Q.t, 'a) arith_view
val id : t -> int val id : t -> int
val view : t -> term view val view : t -> term view
@ -875,8 +875,8 @@ module Term : sig
val select : store -> select -> t -> t val select : store -> select -> t -> t
val app_cstor : store -> cstor -> t IArray.t -> t val app_cstor : store -> cstor -> t IArray.t -> t
val is_a : store -> cstor -> t -> t val is_a : store -> cstor -> t -> t
val lra : store -> (Q.t,t) arith_view -> t val lra : store -> (Q.t, Q.t, t) arith_view -> t
val lia : store -> (Z.t,t) arith_view -> t val lia : store -> (Z.t, Q.t, t) arith_view -> t
module type ARITH_HELPER = sig module type ARITH_HELPER = sig
type num type num
@ -948,8 +948,8 @@ end = struct
| Eq of 'a * 'a | Eq of 'a * 'a
| Not of 'a | Not of 'a
| Ite of 'a * 'a * 'a | Ite of 'a * 'a * 'a
| LRA of (Q.t,'a) arith_view | LRA of (Q.t, Q.t, 'a) arith_view
| LIA of (Z.t,'a) arith_view | LIA of (Z.t, Q.t, 'a) arith_view
let[@inline] id t = t.term_id let[@inline] id t = t.term_id
let[@inline] ty t = t.term_ty 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 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 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 match l with
| Arith_var x -> x (* normalize *) | Arith_var x -> x (* normalize *)
| _ -> make st (Term_cell.lra l) | _ -> 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 match l with
| Arith_var x -> x (* normalize *) | Arith_var x -> x (* normalize *)
| _ -> make st (Term_cell.lia l) | _ -> make st (Term_cell.lia l)
@ -1158,8 +1158,8 @@ end = struct
| Not u -> not_ tst (f u) | Not u -> not_ tst (f u)
| Eq (a,b) -> eq tst (f a) (f b) | Eq (a,b) -> eq tst (f a) (f b)
| Ite (a,b,c) -> ite tst (f a) (f b) (f c) | 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) | 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 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_size tst = H.size tst.tbl
let store_iter tst = H.to_iter tst.tbl let store_iter tst = H.to_iter tst.tbl

476
src/lia/Sidekick_arith_lia.ml
View file

@ -5,7 +5,9 @@
http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_LIA *) http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_LIA *)
open Sidekick_core 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 Make(A : ARG) : S with module A = A = struct
module A = A module A = A
@ -15,72 +17,6 @@ module Make(A : ARG) : S with module A = A = struct
module SI = A.S.Solver_internal module SI = A.S.Solver_internal
module N = A.S.Solver_internal.CC.N 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 module Tag = struct
type t = type t =
| By_def | By_def
@ -114,111 +50,139 @@ module Make(A : ARG) : S with module A = A = struct
| _ -> None | _ -> None
end end
module LE_ = Linear_expr.Make(A.Q)(SimpVar) module LE_ = Linear_expr.Make(A.Z)(SimpVar)
module LE = LE_.Expr 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 Subst = SimpSolver.Subst
module Comb_map = CCMap.Make(LE_.Comb) module Comb_map = CCMap.Make(LE_.Comb)
type state = { type state = {
stat: Stat.t;
proof: A.S.P.t;
tst: T.store; tst: T.store;
ty_st: Ty.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 *) 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; simplex: SimpSolver.t;
gensym: A.Gensym.t;
stat_th_comb: int Stat.counter; stat_th_comb: int Stat.counter;
} }
let create ?(stat=Stat.create()) proof tst ty_st : state = let create ?(stat=Stat.create()) proof tst ty_st : state =
{ tst; ty_st; { stat; proof; tst; ty_st;
proof; local_eqs=Backtrack_stack.create();
simps=T.Tbl.create 128;
gensym=A.Gensym.create tst;
encoded_eqs=T.Tbl.create 8;
needs_th_combination=T.Tbl.create 8;
encoded_le=Comb_map.empty; encoded_le=Comb_map.empty;
local_eqs = Backtrack_stack.create(); encoded_eqs=T.Tbl.create 16;
simplex=SimpSolver.create ~stat (); simplex=SimpSolver.create();
stat_th_comb=Stat.mk_int stat "lra.th-comb"; 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_term self ~pre ty = A.Gensym.fresh_term self.gensym ~pre ty
let fresh_lit (self:state) ~mk_lit ~pre : Lit.t = let fresh_lit (self:state) ~mk_lit ~pre : Lit.t =
let t = fresh_term ~pre self (Ty.bool self.ty_st) in let t = fresh_term ~pre self (Ty.bool self.ty_st) in
mk_lit t 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. *) (* turn the term into a linear expression. Apply [f] on leaves. *)
let rec as_linexp ~f (t:T.t) : LE.t = let rec as_linexp ~f (t:T.t) : LE.t =
let open LE.Infix in let open LE.Infix in
match A.view_as_lra t with match A.view_as_lia t with
| LRA_other _ -> LE.monomial1 (f t) | LIA_other _ -> LE.monomial1 (f t)
| LRA_pred _ | LRA_simplex_pred _ -> | LIA_pred _ | LIA_simplex_pred _ ->
Error.errorf "type error: in linexp, LRA predicate %a" T.pp t Error.errorf "type error: in linexp, LIA predicate %a" T.pp t
| LRA_op (op, t1, t2) -> | LIA_op (op, t1, t2) ->
let t1 = as_linexp ~f t1 in let t1 = as_linexp ~f t1 in
let t2 = as_linexp ~f t2 in let t2 = as_linexp ~f t2 in
begin match op with begin match op with
| Plus -> t1 + t2 | Plus -> t1 + t2
| Minus -> t1 - t2 | Minus -> t1 - t2
end end
| LRA_mult (n, x) -> | LIA_mult (n, x) ->
let t = as_linexp ~f x in let t = as_linexp ~f x in
LE.( n * t ) LE.( n * t )
| LRA_simplex_var v -> LE.monomial1 v | LIA_simplex_var v -> LE.monomial1 v
| LRA_const q -> LE.of_const q | LIA_const q -> LE.of_const q
let as_linexp_id = as_linexp ~f:CCFun.id 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. *) (* 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 = let var_encoding_comb ~pre self (le_comb:LE_.Comb.t) : T.t =
match LE_.Comb.as_singleton le_comb with 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 match Comb_map.find le_comb self.encoded_le with
| x -> x (* already encoded that *) | x -> x (* already encoded that *)
| exception Not_found -> | exception Not_found ->
(* new variable to represent [le_comb] *) (* 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 *) (* TODO: define proxy *)
self.encoded_le <- Comb_map.add le_comb proxy self.encoded_le; self.encoded_le <- Comb_map.add le_comb proxy self.encoded_le;
Log.debugf 50 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 *) (* it's actually 0 *)
if LE_.Comb.is_empty le_comb then ( if LE_.Comb.is_empty le_comb then (
Log.debug 50 "(lra.encode-le.is-trivially-0)"; Log.debug 50 "(lia.encode-le.is-trivially-0)";
SimpSolver.add_constraint self.simplex SimpSolver.add_constraint
self.simplex ~is_int:true
~on_propagate:(fun _ ~reason:_ -> ()) ~on_propagate:(fun _ ~reason:_ -> ())
(SimpSolver.Constraint.leq proxy A.Q.zero) Tag.By_def; (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:_ -> ()) ~on_propagate:(fun _ ~reason:_ -> ())
(SimpSolver.Constraint.geq proxy A.Q.zero) Tag.By_def; (SimpSolver.Constraint.geq proxy A.Q.zero) Tag.By_def;
) else ( ) else (
LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb; LE_.Comb.iter (fun v _ -> SimpSolver.add_var ~is_int:true self.simplex v) le_comb;
SimpSolver.define self.simplex proxy (LE_.Comb.to_list le_comb); SimpSolver.define self.simplex proxy (mk_le_q le_comb);
); );
proxy proxy
let add_clause_lra_ ?using (module PA:SI.PREPROCESS_ACTS) lits = let add_clause_lia_ ?using (module PA:SI.PREPROCESS_ACTS) lits =
let pr = A.lemma_lra (Iter.of_list lits) PA.proof in let pr = A.lemma_lia (Iter.of_list lits) PA.proof in
let pr = match using with let pr = match using with
| None -> pr | None -> pr
| Some using -> SI.P.lemma_rw_clause pr ~res:(Iter.of_list lits) ~using PA.proof in | Some using -> SI.P.lemma_rw_clause pr ~res:(Iter.of_list lits) ~using PA.proof in
PA.add_clause lits pr 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 *) (* 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 = (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 let tst = SI.tst si in
(* preprocess subterm *) (* preprocess subterm *)
@ -228,19 +192,24 @@ module Make(A : ARG) : S with module A = A = struct
u u
in 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 *) (* tell the CC this term exists *)
let declare_term_to_cc t = let declare_term_to_cc t =
Log.debugf 50 (fun k->k "(@[simplex2.declare-term-to-cc@ %a@])" T.pp 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); ignore (SI.CC.add_term (SI.cc si) t : SI.CC.N.t);
in in
match A.view_as_lra t with match A.view_as_lia t with
| LRA_pred ((Eq | Neq), t1, t2) -> | LIA_pred ((Eq | Neq), t1, t2) ->
(* the equality side. *) (* the equality side. *)
let t, _ = T.abs tst t in let t, _ = T.abs tst t in
if not (T.Tbl.mem self.encoded_eqs t) then ( if not (T.Tbl.mem self.encoded_eqs t) then (
let u1 = A.mk_lra tst (LRA_pred (Leq, t1, t2)) in let u1 = A.mk_lia tst (LIA_pred (Leq, t1, t2)) in
let u2 = A.mk_lra tst (LRA_pred (Geq, t1, t2)) in let u2 = A.mk_lia tst (LIA_pred (Geq, t1, t2)) in
T.Tbl.add self.encoded_eqs t (); 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_t = PA.mk_lit_nopreproc t in
let lit_u1 = PA.mk_lit_nopreproc u1 in let lit_u1 = PA.mk_lit_nopreproc u1 in
let lit_u2 = PA.mk_lit_nopreproc u2 in let lit_u2 = PA.mk_lit_nopreproc u2 in
add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u1]; add_clause_lia_ (module PA) [SI.Lit.neg lit_t; lit_u1];
add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u2]; add_clause_lia_ (module PA) [SI.Lit.neg lit_t; lit_u2];
add_clause_lra_ (module PA) add_clause_lia_ (module PA)
[SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t]; [SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t];
); );
None None
| LRA_pred (pred, t1, t2) -> | LIA_pred (pred, t1, t2) ->
let steps = ref [] in let steps = ref [] in
let l1 = as_linexp ~f:(preproc_t ~steps) t1 in let l1 = as_linexp ~f:(preproc_t ~steps) t1 in
let l2 = as_linexp ~f:(preproc_t ~steps) t2 in let l2 = as_linexp ~f:(preproc_t ~steps) t2 in
let le = LE.(l1 - l2) in let le = LE.(l1 - l2) in
let le_comb, le_const = LE.comb le, LE.const le 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 <pred> le_const] *) (* now we have [le_comb <pred> le_const] *)
begin match LE_.Comb.as_singleton le_comb, pred with 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 | Gt -> S_op.Gt
in 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 begin
let lit = PA.mk_lit_nopreproc new_t in let lit = PA.mk_lit_nopreproc new_t in
let constr = SimpSolver.Constraint.mk proxy op le_const 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; 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 (new_t, Iter.of_list !steps)
| Some (coeff, v), pred -> | Some (coeff, v), pred ->
(* [c . v <= const] becomes a direct simplex constraint [v <= const/c] *) (* [c . v <= const] becomes a direct (rational) simplex constraint [v <= const/c] *)
let q = A.Q.( le_const / coeff ) in let const' = A.Q.( le_const / of_bigint coeff) in
declare_term_to_cc v; declare_term_to_cc v;
let op = match pred with let op = match pred with
@ -304,23 +275,26 @@ module Make(A : ARG) : S with module A = A = struct
| Eq | Neq -> assert false | Eq | Neq -> assert false
in in
(* make sure to swap sides if multiplying with a negative coeff *) (* 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 begin
let lit = PA.mk_lit_nopreproc new_t in 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); SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
end; 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 (new_t, Iter.of_list !steps)
end end
| LRA_op _ | LRA_mult _ -> | LIA_op _ | LIA_mult _ ->
let steps = ref [] in let steps = ref [] in
let le = as_linexp ~f:(preproc_t ~steps) t 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_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 A.Q.(le_const = zero) then (
(* if there is no constant, define [proxy] as [proxy := le_comb] and (* 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; end;
let proxy2 = fresh_term self ~pre:"_le_diff" (T.ty t) in let proxy2 = fresh_term self ~pre:"_le_diff" (T.ty t) in
let pr_def2 = 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 in
SimpSolver.add_var self.simplex proxy; SimpSolver.add_var self.simplex proxy;
LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb; LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb;
SimpSolver.define self.simplex proxy2 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 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); LE_.Comb.pp le_comb T.pp proxy T.pp proxy2);
declare_term_to_cc proxy; declare_term_to_cc proxy;
declare_term_to_cc proxy2; declare_term_to_cc proxy2;
add_clause_lra_ ~using:Iter.(return pr_def2) (module PA) [ add_clause_lia_ ~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))) 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) [ add_clause_lia_ ~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))) PA.mk_lit_nopreproc (A.mk_lia tst (LIA_simplex_pred (proxy2, Geq, A.Q.neg le_const)))
]; ];
Some (proxy, Iter.of_list !steps) Some (proxy, Iter.of_list !steps)
) )
| LRA_other t when A.has_ty_real t -> None | LIA_other t when A.has_ty_int t -> None
| LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ -> | LIA_const _ | LIA_simplex_pred _ | LIA_simplex_var _ | LIA_other _ ->
None None
let simplify (self:state) (_recurse:_) (t:T.t) : (T.t * SI.proof_step Iter.t) option = let simplify (self:state) (_recurse:_) (t:T.t) : (T.t * SI.proof_step Iter.t) option =
let proof_eq t u = 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 (Iter.return (SI.Lit.atom self.tst (A.mk_eq self.tst t u))) self.proof
in in
let proof_bool t ~sign:b = let proof_bool t ~sign:b =
let lit = SI.Lit.atom ~sign:b self.tst t in 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 in
match A.view_as_lra t with match A.view_as_lia t with
| LRA_op _ | LRA_mult _ -> | LIA_op _ | LIA_mult _ ->
let le = as_linexp_id t in let le = as_linexp_id t in
if LE.is_const le then ( if LE.is_const le then (
let c = LE.const le in 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 let pr = proof_eq t u in
Some (u, Iter.return pr) Some (u, Iter.return pr)
) else None ) else None
| LRA_pred (pred, l1, l2) -> | LIA_pred (pred, l1, l2) ->
let le = LE.(as_linexp_id l1 - as_linexp_id l2) in let le = LE.(as_linexp_id l1 - as_linexp_id l2) in
if LE.is_const le then ( if LE.is_const le then (
let c = LE.const le in let c = LE.const le in
let is_true = match pred with let is_true = match pred with
| Leq -> A.Q.(c <= zero) | Leq -> A.Z.(c <= zero)
| Geq -> A.Q.(c >= zero) | Geq -> A.Z.(c >= zero)
| Lt -> A.Q.(c < zero) | Lt -> A.Z.(c < zero)
| Gt -> A.Q.(c > zero) | Gt -> A.Z.(c > zero)
| Eq -> A.Q.(c = zero) | Eq -> A.Z.(c = zero)
| Neq -> A.Q.(c <> zero) | Neq -> A.Z.(c <> zero)
in in
let u = A.mk_bool self.tst is_true in let u = A.mk_bool self.tst is_true in
let pr = proof_bool t ~sign: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 ) else None
| _ -> 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 *) (* raise conflict from certificate *)
let fail_with_cert si acts cert : 'a = 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) |> CCList.flat_map (Tag.to_lits si)
|> List.rev_map SI.Lit.neg |> List.rev_map SI.Lit.neg
in 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 SI.raise_conflict si acts confl pr
let on_propagate_ si acts lit ~reason = module Q_map = CCMap.Make(A.Q)
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)
| _ -> ()
let check_simplex_ self si acts : SimpSolver.Subst.t = let check_simplex_ self si acts : SimpSolver.Subst.t =
Log.debug 5 "(lra.check-simplex)"; Log.debug 5 "(lia.check-simplex)";
let res = let res =
Profile.with_ "simplex.solve" Profile.with_ "lia.simplex.solve"
(fun () -> (fun () ->
SimpSolver.check self.simplex SimpSolver.check self.simplex
~on_propagate:(on_propagate_ si acts)) ~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.Sat m -> m
| SimpSolver.Unsat cert -> | SimpSolver.Unsat cert ->
Log.debugf 10 Log.debugf 10
(fun k->k "(@[lra.check.unsat@ :cert %a@])" (fun k->k "(@[lia.check.unsat@ :cert %a@])"
SimpSolver.Unsat_cert.pp cert); SimpSolver.Unsat_cert.pp cert);
fail_with_cert si acts cert fail_with_cert si acts cert
end 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 = 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 t1 = N.term n1 in
let t2 = N.term n2 in let t2 = N.term n2 in
let t1, t2 = if T.compare t1 t2 > 0 then t2, t1 else t1, t2 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 = LE.(as_linexp_id t1 - as_linexp_id t2) in
let le_comb, le_const = LE.comb le, LE.const le 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 v = var_encoding_comb ~pre:"le_local_eq" self le_comb in
let lit = Tag.CC_eq (n1,n2) in let lit = Tag.CC_eq (n1,n2) in
begin begin
try try
let c1 = SimpSolver.Constraint.geq v le_const in let c1 = SimpSolver.Constraint.geq v (A.Q.of_bigint le_const) in
SimpSolver.add_constraint self.simplex c1 lit SimpSolver.add_constraint self.simplex ~is_int:true c1 lit
~on_propagate:(on_propagate_ si acts); ~on_propagate:(on_propagate_ si acts);
let c2 = SimpSolver.Constraint.leq v le_const in let c2 = SimpSolver.Constraint.leq v (A.Q.of_bigint le_const) in
SimpSolver.add_constraint self.simplex c2 lit SimpSolver.add_constraint self.simplex ~is_int:true c2 lit
~on_propagate:(on_propagate_ si acts); ~on_propagate:(on_propagate_ si acts);
with SimpSolver.E_unsat cert -> with SimpSolver.E_unsat cert ->
fail_with_cert si acts 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] (* theory combination: add decisions [t=u] whenever [t] and [u]
have the same value in [subst] and both occur under function symbols *) have the same value in [subst] and both occur under function symbols *)
let do_th_combination (self:state) si acts (subst:Subst.t) : unit = 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 let n_th_comb = T.Tbl.keys self.needs_th_combination |> Iter.length in
if n_th_comb > 0 then ( if n_th_comb > 0 then (
Log.debugf 5 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 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)); (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 |> List.iter
(fun (t1,t2) -> (fun (t1,t2) ->
Log.debugf 50 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); A.Q.pp _q T.pp t1 T.pp t2);
assert(SI.cc_mem_term si t1); assert(SI.cc_mem_term si t1);
assert(SI.cc_mem_term si t2); 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 closure, and are not equal in it yet, add [t1=t2] as
the next decision to do *) the next decision to do *)
if not (SI.cc_are_equal si t1 t2) then ( 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; 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 t = A.mk_eq (SI.tst si) t1 t2 in
let lit = SI.mk_lit si acts t 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; 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 = let final_check_ (self:state) si (acts:SI.theory_actions) (_trail:_ Iter.t) : unit =
Log.debug 5 "(th-lra.final-check)"; Log.debug 5 "(th-lia.final-check)";
Profile.with_ "lra.final-check" @@ fun () -> Profile.with_ "lia.final-check" @@ fun () ->
(* add congruence closure equalities *) (* add congruence closure equalities *)
Backtrack_stack.iter self.local_eqs 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 (* TODO: jiggle model to reduce the number of variables that
have the same value *) have the same value *)
let model = check_simplex_ self si acts in let model = check_simplex_ self si acts in
Log.debugf 20 (fun k->k "(@[lra.model@ %a@])" SimpSolver.Subst.pp model); Log.debugf 20 (fun k->k "(@[lia.model@ %a@])" SimpSolver.Subst.pp model);
Log.debug 5 "(lra: solver returns SAT)"; Log.debug 5 "(lia: solver returns SAT)";
do_th_combination self si acts model; do_th_combination self si acts model;
() ()
(* look for subterms of type Real, for they will need theory combination *) (* raise conflict from certificate *)
let on_subterm (self:state) _ (t:T.t) : unit = let fail_with_cert si acts cert : 'a =
Log.debugf 50 (fun k->k "(@[lra.cc-on-subterm@ %a@])" T.pp t); Profile.with1 "simplex.check-cert" SimpSolver._check_cert cert;
match A.view_as_lra t with let confl =
| LRA_other _ when not (A.has_ty_real t) -> () SimpSolver.Unsat_cert.lits cert
| _ -> |> CCList.flat_map (Tag.to_lits si)
if not (T.Tbl.mem self.needs_th_combination t) then ( |> List.rev_map SI.Lit.neg
Log.debugf 5 (fun k->k "(@[lra.needs-th-combination@ %a@])" T.pp t); in
T.Tbl.add self.needs_th_combination t () 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 end

2
src/lia/Sidekick_arith_lia.mli
View file

@ -6,6 +6,6 @@
http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_LIA *) http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_LIA *)
open Sidekick_core open Sidekick_core
include module type of Intf include module type of Intf_lia
module Make(A : ARG) : S with module A=A module Make(A : ARG) : S with module A=A

2
src/lia/dune
View file

@ -3,4 +3,4 @@
(public_name sidekick.arith-lia) (public_name sidekick.arith-lia)
(synopsis "Solver for LIA (integer arithmetic)") (synopsis "Solver for LIA (integer arithmetic)")
(flags :standard -warn-error -a+8 -w -32 -open Sidekick_util) (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))

31
src/lia/intf.ml → src/lia/intf_lia.ml
View file

@ -4,17 +4,17 @@ open Sidekick_core
module type RATIONAL = Sidekick_arith.RATIONAL module type RATIONAL = Sidekick_arith.RATIONAL
module type INT = Sidekick_arith.INT module type INT = Sidekick_arith.INT
module S_op = Sidekick_arith_lra.S_op module S_op = Sidekick_simplex.Op
type pred = Sidekick_arith_lra.pred = Leq | Geq | Lt | Gt | Eq | Neq type pred = Sidekick_simplex.Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq
type op = Sidekick_arith_lra.op = Plus | Minus 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_pred of pred * 'a * 'a
| LIA_op of op * 'a * 'a | LIA_op of op * 'a * 'a
| LIA_mult of 'num * 'a | LIA_mult of 'num * 'a
| LIA_const of 'num | LIA_const of 'num
| LIA_simplex_var of 'a (* an opaque variable *) | 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 | LIA_other of 'a
let map_view f (l:_ lia_view) : _ lia_view = 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 type ARG = sig
module S : Sidekick_core.SOLVER module S : Sidekick_core.SOLVER
module Q : RATIONAL
module Z : INT module Z : INT
module Q : RATIONAL with type bigint = Z.t
module LRA : Sidekick_arith_lra.S
type term = S.T.Term.t type term = S.T.Term.t
type ty = S.T.Ty.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 *) (** Project the term into the theory view *)
val mk_bool : S.T.Term.store -> bool -> term 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 val mk_to_real : S.T.Term.store -> term -> term
(** Wrap term into a [to_real] projector to rationals *) (** 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 *) (** Make a term from the given theory view *)
val ty_int : S.T.Term.store -> ty val ty_int : S.T.Term.store -> ty
@ -59,6 +57,19 @@ module type ARG = sig
(** Does this term have the type [Int] *) (** Does this term have the type [Int] *)
val lemma_lia : S.Lit.t Iter.t -> S.P.proof_rule 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 end
module type S = sig module type S = sig

4
src/lra/sidekick_arith_lra.ml
View file

@ -40,7 +40,8 @@ let map_view f (l:_ lra_view) : _ lra_view =
module type ARG = sig module type ARG = sig
module S : Sidekick_core.SOLVER 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 term = S.T.Term.t
type ty = S.T.Ty.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_ = Linear_expr.Make(A.Q)(SimpVar)
module LE = LE_.Expr module LE = LE_.Expr
module SimpSolver = Sidekick_simplex.Make(struct module SimpSolver = Sidekick_simplex.Make(struct
module Z = A.Z
module Q = A.Q module Q = A.Q
module Var = SimpVar module Var = SimpVar
let mk_lit _ _ _ = assert false let mk_lit _ _ _ = assert false

2
src/smtlib/Typecheck.ml
View file

@ -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.lra ctx.tst (Arith_const (Q.of_bigint n))
| T.LIA l -> | T.LIA l ->
(* try to convert the whole structure to reals *) (* 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 T.lra ctx.tst l
| _ -> | _ ->
errorf_ctx ctx "cannot cast term to real@ :term %a" T.pp t errorf_ctx ctx "cannot cast term to real@ :term %a" T.pp t