From f0041f9daee80ec94286a0eacf13688b6e6123b3 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 26 Aug 2022 22:17:02 -0400 Subject: [PATCH] feat: reinstate LRA theory and terms --- src/base/Form.ml | 4 - src/base/LRA_term.ml | 10 ++ src/base/LRA_term.mli | 3 + src/base/Sidekick_base.ml | 28 +---- src/base/th_lra.ml | 61 +++------- src/main/main.ml | 3 +- src/smtlib/Process.ml | 8 +- src/smtlib/Process.mli | 4 +- src/smtlib/Typecheck.ml | 199 ++++++++++++++++++--------------- src/th-lra/intf.ml | 16 +-- src/th-lra/proof_rules.ml | 3 + src/th-lra/proof_rules.mli | 5 + src/th-lra/sidekick_th_lra.ml | 50 +++++---- src/th-lra/sidekick_th_lra.mli | 26 ++++- 14 files changed, 207 insertions(+), 213 deletions(-) create mode 100644 src/th-lra/proof_rules.ml create mode 100644 src/th-lra/proof_rules.mli diff --git a/src/base/Form.ml b/src/base/Form.ml index 6173d171..2bfa3788 100644 --- a/src/base/Form.ml +++ b/src/base/Form.ml @@ -1,8 +1,6 @@ -open Types_ open Sidekick_core module T = Term -type ty = Term.t type term = Term.t type 'a view = 'a Sidekick_core.Bool_view.t = @@ -42,8 +40,6 @@ let ops : Const.ops = (* ### view *) -exception Not_a_th_term - let view (t : T.t) : T.t view = let hd, args = T.unfold_app t in match T.view hd, args with diff --git a/src/base/LRA_term.ml b/src/base/LRA_term.ml index eea25db2..c7b3c7ec 100644 --- a/src/base/LRA_term.ml +++ b/src/base/LRA_term.ml @@ -34,6 +34,7 @@ let ops : Const.ops = end) let real tst = Ty.real tst +let has_ty_real t = Ty.is_real (T.ty t) let const tst q : term = Term.const tst (Const.make (Const q) ops ~ty:(real tst)) @@ -56,8 +57,17 @@ let op tst op t1 t2 : term = let view (t : term) : _ View.t = let f, args = Term.unfold_app t in match T.view f, args with + | T.E_const { Const.c_view = T.C_eq; _ }, [ _; a; b ] when has_ty_real a -> + View.LRA_pred (Pred.Eq, a, b) | T.E_const { Const.c_view = Const q; _ }, [] -> View.LRA_const q | T.E_const { Const.c_view = Pred p; _ }, [ a; b ] -> View.LRA_pred (p, a, b) | T.E_const { Const.c_view = Op op; _ }, [ a; b ] -> View.LRA_op (op, a, b) | T.E_const { Const.c_view = Mult_by q; _ }, [ a ] -> View.LRA_mult (q, a) | _ -> View.LRA_other t + +let term_of_view store = function + | View.LRA_const q -> const store q + | View.LRA_mult (n, t) -> mult_by store n t + | View.LRA_pred (p, a, b) -> pred store p a b + | View.LRA_op (o, a, b) -> op store o a b + | View.LRA_other x -> x diff --git a/src/base/LRA_term.mli b/src/base/LRA_term.mli index 396f3b8c..a6f7b5d3 100644 --- a/src/base/LRA_term.mli +++ b/src/base/LRA_term.mli @@ -7,6 +7,7 @@ type term = Term.t type ty = Term.t val real : Term.store -> ty +val has_ty_real : term -> bool val pred : Term.store -> Pred.t -> term -> term -> term val mult_by : Term.store -> Q.t -> term -> term val op : Term.store -> Op.t -> term -> term -> term @@ -14,3 +15,5 @@ val const : Term.store -> Q.t -> term val view : term -> term View.t (** View as LRA *) + +val term_of_view : Term.store -> term View.t -> term diff --git a/src/base/Sidekick_base.ml b/src/base/Sidekick_base.ml index d0b03630..6ce130f6 100644 --- a/src/base/Sidekick_base.ml +++ b/src/base/Sidekick_base.ml @@ -33,35 +33,11 @@ module Config = Config module LRA_term = LRA_term module Th_data = Th_data module Th_bool = Th_bool -(* FIXME - module Th_lra = Th_lra -*) +module Th_lra = Th_lra let k_th_bool_config = Th_bool.k_config let th_bool = Th_bool.theory let th_bool_dyn : Solver.theory = Th_bool.theory_dyn let th_bool_static : Solver.theory = Th_bool.theory_static let th_data : Solver.theory = Th_data.theory - -(* FIXME - let th_lra : Solver.theory = Th_lra.theory -*) - -(* TODO - - module Value = Value - module Statement = Statement - module Data = Data - module Select = Select - - module LRA_view = Types_.LRA_view - module LRA_pred = Base_types.LRA_pred - module LRA_op = Base_types.LRA_op - module LIA_view = Base_types.LIA_view - module LIA_pred = Base_types.LIA_pred - module LIA_op = Base_types.LIA_op -*) - -(* -module Proof_quip = Proof_quip -*) +let th_lra : Solver.theory = Th_lra.theory diff --git a/src/base/th_lra.ml b/src/base/th_lra.ml index 29e29d19..933b482e 100644 --- a/src/base/th_lra.ml +++ b/src/base/th_lra.ml @@ -1,48 +1,21 @@ -(* TODO +(** Theory of Linear Rational Arithmetic *) +open Sidekick_core +module T = Term +module Q = Sidekick_zarith.Rational +open LRA_term - (** 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 +let mk_eq = Form.eq +let mk_bool = T.bool - type term = S.T.Term.t - type ty = S.T.Ty.t +let theory : Solver.theory = + Sidekick_th_lra.theory + (module struct + module Z = Sidekick_zarith.Int + module Q = Sidekick_zarith.Rational - module LRA = Sidekick_arith_lra - - let mk_eq = Form.eq - - let mk_lra store l = - match l with - | LRA.LRA_other x -> x - | LRA.LRA_pred (p, x, y) -> T.lra store (Pred (p, x, y)) - | LRA.LRA_op (op, x, y) -> T.lra store (Op (op, x, y)) - | LRA.LRA_const c -> T.lra store (Const c) - | LRA.LRA_mult (c, x) -> T.lra store (Mult (c, x)) - - let mk_bool = T.bool - - let rec view_as_lra t = - match T.view t with - | T.LRA l -> - let module LRA = Sidekick_arith_lra in - (match l with - | Const c -> LRA.LRA_const c - | Pred (p, a, b) -> LRA.LRA_pred (p, a, b) - | Op (op, a, b) -> LRA.LRA_op (op, a, b) - | Mult (c, x) -> LRA.LRA_mult (c, x) - | To_real x -> view_as_lra x - | Var x -> LRA.LRA_other x) - | T.Eq (a, b) when Ty.equal (T.ty a) (Ty.real ()) -> LRA.LRA_pred (Eq, a, b) - | _ -> LRA.LRA_other t - - let ty_lra _st = Ty.real () - let has_ty_real t = Ty.equal (T.ty t) (Ty.real ()) - let lemma_lra = Proof.lemma_lra - - module Gensym = Gensym - end) -*) + let ty_real = LRA_term.real + let has_ty_real = LRA_term.has_ty_real + let view_as_lra = LRA_term.view + let mk_lra = LRA_term.term_of_view + end : Sidekick_th_lra.ARG) diff --git a/src/main/main.ml b/src/main/main.ml index 769ec595..679e4d8d 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -178,8 +178,7 @@ let main_smt ~config () : _ result = Log.debugf 1 (fun k -> k "(@[main.th-bool.pick@ %S@])" (Sidekick_smt_solver.Theory.name th_bool)); - Sidekick_smt_solver.Theory. - [ th_bool; Process.th_data (* FIXME Process.th_lra *) ] + Sidekick_smt_solver.Theory.[ th_bool; Process.th_data; Process.th_lra ] in Process.Solver.create_default ~proof ~theories tst in diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index b530f465..1dea0d39 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -338,14 +338,10 @@ let process_stmt ?gc ?restarts ?(pp_cnf = false) ?proof_file ?pp_model module Th_data = Sidekick_base.Th_data module Th_bool = Sidekick_base.Th_bool -(* FIXME - module Th_lra = Sidekick_base.Th_lra -*) +module Th_lra = Sidekick_base.Th_lra let th_bool = Th_bool.theory let th_bool_dyn : Solver.theory = Th_bool.theory_dyn let th_bool_static : Solver.theory = Th_bool.theory_static let th_data : Solver.theory = Th_data.theory -(* FIXME - let th_lra : Solver.theory = Th_lra.theory -*) +let th_lra : Solver.theory = Th_lra.theory diff --git a/src/smtlib/Process.mli b/src/smtlib/Process.mli index 25e83add..2046c224 100644 --- a/src/smtlib/Process.mli +++ b/src/smtlib/Process.mli @@ -7,9 +7,7 @@ val th_bool_dyn : Solver.theory val th_bool_static : Solver.theory val th_bool : Config.t -> Solver.theory val th_data : Solver.theory -(* FIXME - val th_lra : Solver.theory -*) +val th_lra : Solver.theory type 'a or_error = ('a, string) CCResult.t diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index 7322b604..46ef5259 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -113,59 +113,84 @@ let string_as_q (s : string) : Q.t option = Some x with _ -> None -(* TODO - let t_as_q t = - match Term.view t with - | T.LRA (Const n) -> Some n - | T.LIA (Const n) -> Some (Q.of_bigint n) - | _ -> None +let t_as_q t = + match LRA_term.view t with + | LRA_term.View.LRA_const n -> Some n + (* + | T.LIA (Const n) -> Some (Q.of_bigint n) + *) + | _ -> None +(* TODO let t_as_z t = match Term.view t with | T.LIA (Const n) -> Some n | _ -> None +*) - let is_real = Ty.is_real +let is_real = Ty.is_real - (* convert [t] to a real term *) - let cast_to_real (ctx : Ctx.t) (t : T.t) : T.t = - let rec conv t = - match T.view t with - | T.LRA _ -> t - | _ when Ty.equal (T.ty t) (Ty.real ()) -> t +(* convert [t] to a real term *) +let cast_to_real (ctx : Ctx.t) (t : T.t) : T.t = + let conv t = + match T.view t with + | _ when Ty.is_real (T.ty t) -> t + (* FIXME | T.LIA (Const n) -> T.lra ctx.tst (Const (Q.of_bigint n)) | T.LIA l -> (* convert the whole structure to reals *) let l = LIA_view.to_lra conv l in T.lra ctx.tst l | T.Ite (a, b, c) -> T.ite ctx.tst a (conv b) (conv c) - | _ -> errorf_ctx ctx "cannot cast term to real@ :term %a" T.pp t - in - conv t + *) + | _ -> errorf_ctx ctx "cannot cast term to real@ :term %a" T.pp t + in + conv t - let conv_arith_op (ctx : Ctx.t) t (op : PA.arith_op) (l : T.t list) : T.t = - let tst = ctx.Ctx.tst in +let conv_arith_op (ctx : Ctx.t) (t : PA.term) (op : PA.arith_op) (l : T.t list) + : T.t = + let tst = ctx.Ctx.tst in - let mk_pred p a b = + let mk_pred p a b = + LRA_term.pred tst p (cast_to_real ctx a) (cast_to_real ctx b) + (* TODO + if is_real a || is_real b then + LRA_term.pred tst p (cast_to_real ctx a) (cast_to_real ctx b) + else + Error.errorf "cannot handle LIA term %a" PA.pp_term t + T.lia tst (Pred (p, a, b)) + *) + and mk_op o a b = + LRA_term.op tst o (cast_to_real ctx a) (cast_to_real ctx b) + (* TODO if is_real a || is_real b then - T.lra tst (Pred (p, cast_to_real ctx a, cast_to_real ctx b)) + LRA_term.op tst o (cast_to_real ctx a) (cast_to_real ctx b) else - T.lia tst (Pred (p, a, b)) - and mk_op o a b = - if is_real a || is_real b then - T.lra tst (Op (o, cast_to_real ctx a, cast_to_real ctx b)) - else - T.lia tst (Op (o, a, b)) - in + Error.errorf "cannot handle LIA term %a" PA.pp_term t + T.lia tst (Op (o, a, b)) + *) + in - match op, l with - | PA.Leq, [ a; b ] -> mk_pred Leq a b - | PA.Lt, [ a; b ] -> mk_pred Lt a b - | PA.Geq, [ a; b ] -> mk_pred Geq a b - | PA.Gt, [ a; b ] -> mk_pred Gt a b - | PA.Add, [ a; b ] -> mk_op Plus a b - | PA.Add, a :: l -> List.fold_left (fun a b -> mk_op Plus a b) a l - | PA.Minus, [ a ] -> + match op, l with + | PA.Leq, [ a; b ] -> mk_pred Leq a b + | PA.Lt, [ a; b ] -> mk_pred Lt a b + | PA.Geq, [ a; b ] -> mk_pred Geq a b + | PA.Gt, [ a; b ] -> mk_pred Gt a b + | PA.Add, [ a; b ] -> mk_op Plus a b + | PA.Add, a :: l -> List.fold_left (fun a b -> mk_op Plus a b) a l + | PA.Minus, [ a ] -> + (match t_as_q a with + | Some q -> LRA_term.const tst (Q.neg q) + | None -> + let zero = + if is_real a then + LRA_term.const tst Q.zero + else + Error.errorf "cannot handle non-rat %a" PA.pp_term t + (* T.lia tst (Const Z.zero) *) + in + mk_op Minus zero a) + (* (match t_as_q a, t_as_z a with | _, Some n -> T.lia tst (Const (Z.neg n)) | Some q, None -> T.lra tst (Const (Q.neg q)) @@ -176,57 +201,52 @@ let string_as_q (s : string) : Q.t option = else T.lia tst (Const Z.zero) in - mk_op Minus zero a) - | PA.Minus, [ a; b ] -> mk_op Minus a b - | PA.Minus, a :: l -> List.fold_left (fun a b -> mk_op Minus a b) a l - | PA.Mult, [ a; b ] when is_real a || is_real b -> - (match t_as_q a, t_as_q b with - | Some a, Some b -> T.lra tst (Const (Q.mul a b)) - | Some a, _ -> T.lra tst (Mult (a, b)) - | _, Some b -> T.lra tst (Mult (b, a)) - | None, None -> - errorf_ctx ctx "cannot handle non-linear mult %a" PA.pp_term t) - | PA.Mult, [ a; b ] -> - (match t_as_z a, t_as_z b with - | Some a, Some b -> T.lia tst (Const (Z.mul a b)) - | Some a, _ -> T.lia tst (Mult (a, b)) - | _, Some b -> T.lia tst (Mult (b, a)) - | None, None -> - errorf_ctx ctx "cannot handle non-linear mult %a" PA.pp_term t) - | PA.Div, [ a; b ] when is_real a || is_real b -> - (match t_as_q a, t_as_q b with - | Some a, Some b -> T.lra tst (Const (Q.div a b)) - | _, Some b -> T.lra tst (Mult (Q.inv b, a)) - | _, None -> errorf_ctx ctx "cannot handle non-linear div %a" PA.pp_term t) - | PA.Div, [ a; b ] -> - (* becomes a real *) - (match t_as_q a, t_as_q b with - | Some a, Some b -> T.lra tst (Const (Q.div a b)) - | _, Some b -> - let a = cast_to_real ctx a in - T.lra tst (Mult (Q.inv b, a)) - | _, None -> errorf_ctx ctx "cannot handle non-linear div %a" PA.pp_term t) - | _ -> errorf_ctx ctx "cannot handle arith construct %a" PA.pp_term t -*) + *) + | PA.Minus, [ a; b ] -> mk_op Minus a b + | PA.Minus, a :: l -> List.fold_left (fun a b -> mk_op Minus a b) a l + | PA.Mult, [ a; b ] -> + (match t_as_q a, t_as_q b with + | Some a, Some b -> LRA_term.const tst (Q.mul a b) + | Some a, _ -> LRA_term.mult_by tst a b + | _, Some b -> LRA_term.mult_by tst b a + | None, None -> + errorf_ctx ctx "cannot handle non-linear mult %a" PA.pp_term t) + (* TODO + | PA.Mult, [ _a; _b ] -> + (match t_as_z a, t_as_z b with + | Some a, Some b -> T.lia tst (Const (Z.mul a b)) + | Some a, _ -> T.lia tst (Mult (a, b)) + | _, Some b -> T.lia tst (Mult (b, a)) + | None, None -> + errorf_ctx ctx "cannot handle non-linear mult %a" PA.pp_term t) + errorf_ctx ctx "cannot handle non-linear mult %a" PA.pp_term t + *) + | PA.Div, [ a; b ] -> + (match t_as_q a, t_as_q b with + | Some a, Some b -> LRA_term.const tst (Q.div a b) + | _, Some b -> + let a = cast_to_real ctx a in + LRA_term.mult_by tst (Q.inv b) a + | _, None -> errorf_ctx ctx "cannot handle non-linear div %a" PA.pp_term t) + | _ -> errorf_ctx ctx "cannot handle arith construct %a" PA.pp_term t (* conversion of terms *) let rec conv_term (ctx : Ctx.t) (t : PA.term) : T.t = let tst = ctx.Ctx.tst in match t with | PA.True -> T.true_ tst - | PA.False -> - T.false_ tst - (* FIXME - | PA.Const s when is_num s -> - (match string_as_z s, ctx.default_num with - | Some n, `Int -> T.lia tst (Const n) - | Some n, `Real -> T.lra tst (Const (Q.of_bigint n)) - | None, _ -> - (match string_as_q s with - | Some n -> T.lra tst (Const n) - | None -> errorf_ctx ctx "expected a number for %a" PA.pp_term t)) - *) + | PA.False -> T.false_ tst + | PA.Const s when is_num s -> + (match string_as_z s, ctx.default_num with + | Some n, `Real -> LRA_term.const tst (Q.of_bigint n) + | Some n, `Int -> + Error.errorf "cannot handle integer constant %a yet" Z.pp_print n + (* TODO T.lia tst (Const n) *) + | None, _ -> + (match string_as_q s with + | Some n -> LRA_term.const tst n + | None -> errorf_ctx ctx "expected a number for %a" PA.pp_term t)) | PA.Const f | PA.App (f, []) -> (* lookup in `let` table, then in type defs *) (match StrTbl.find ctx.Ctx.lets f with @@ -276,12 +296,12 @@ let rec conv_term (ctx : Ctx.t) (t : PA.term) : T.t = | PA.Eq (a, b) -> let a = conv_term ctx a in let b = conv_term ctx b in - (* FIXME - if is_real a || is_real b then - Form.eq tst (cast_to_real ctx a) (cast_to_real ctx b) - else - *) - Form.eq tst a b + if is_real a || is_real b then + (* Form.eq tst (cast_to_real ctx a) (cast_to_real ctx b) *) + LRA_term.pred tst LRA_term.Pred.Eq (cast_to_real ctx a) + (cast_to_real ctx b) + else + Form.eq tst a b | PA.Imply (a, b) -> let a = conv_term ctx a in let b = conv_term ctx b in @@ -371,12 +391,9 @@ let rec conv_term (ctx : Ctx.t) (t : PA.term) : T.t = in A.match_ lhs cases *) - - (* FIXME - | PA.Arith (op, l) -> - let l = List.map (conv_term ctx) l in - conv_arith_op ctx t op l - *) + | PA.Arith (op, l) -> + let l = List.map (conv_term ctx) l in + conv_arith_op ctx t op l | PA.Cast (t, ty_expect) -> let t = conv_term ctx t in let ty_expect = conv_ty ctx ty_expect in diff --git a/src/th-lra/intf.ml b/src/th-lra/intf.ml index d1cdc516..5e3f5672 100644 --- a/src/th-lra/intf.ml +++ b/src/th-lra/intf.ml @@ -39,21 +39,9 @@ module type ARG = sig val mk_lra : Term.store -> (Q.t, Term.t) lra_view -> Term.t (** Make a Term.t from the given theory view *) - val ty_lra : Term.store -> ty + val ty_real : Term.store -> ty + (** Build the type Q *) val has_ty_real : Term.t -> bool (** Does this term have the type [Real] *) - - val lemma_lra : Lit.t list -> Proof_term.t - - module Gensym : sig - type t - - val create : Term.store -> t - val tst : t -> Term.store - val copy : t -> t - - val fresh_term : t -> pre:string -> ty -> term - (** Make a fresh term of the given type *) - end end diff --git a/src/th-lra/proof_rules.ml b/src/th-lra/proof_rules.ml new file mode 100644 index 00000000..72087162 --- /dev/null +++ b/src/th-lra/proof_rules.ml @@ -0,0 +1,3 @@ +open Sidekick_core + +let lemma_lra lits : Proof_term.t = Proof_term.apply_rule "lra.lemma" ~lits diff --git a/src/th-lra/proof_rules.mli b/src/th-lra/proof_rules.mli new file mode 100644 index 00000000..26a2688a --- /dev/null +++ b/src/th-lra/proof_rules.mli @@ -0,0 +1,5 @@ +open Sidekick_core + +val lemma_lra : Lit.t list -> Proof_term.t +(** List of literals [l1…ln] where [¬l1 /\ … /\ ¬ln] is LRA-unsat *) + diff --git a/src/th-lra/sidekick_th_lra.ml b/src/th-lra/sidekick_th_lra.ml index ec9f9188..918466d0 100644 --- a/src/th-lra/sidekick_th_lra.ml +++ b/src/th-lra/sidekick_th_lra.ml @@ -126,7 +126,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct type state = { tst: Term.store; proof: Proof_trace.t; - gensym: A.Gensym.t; + gensym: Gensym.t; in_model: unit Term.Tbl.t; (* terms to add to model *) encoded_eqs: unit Term.Tbl.t; (* [a=b] gets clause [a = b <=> (a >= b /\ a <= b)] *) @@ -140,6 +140,8 @@ module Make (A : ARG) = (* : S with module A = A *) struct mutable encoded_le: Term.t Comb_map.t; (* [le] -> var encoding [le] *) simplex: SimpSolver.t; mutable last_res: SimpSolver.result option; + n_propagate: int Stat.counter; + n_conflict: int Stat.counter; } let create (si : SI.t) : state = @@ -151,7 +153,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct proof; in_model = Term.Tbl.create 8; st_exprs = ST_exprs.create_and_setup (SI.cc si); - gensym = A.Gensym.create tst; + gensym = Gensym.create tst; simp_preds = Term.Tbl.create 32; simp_defined = Term.Tbl.create 16; encoded_eqs = Term.Tbl.create 8; @@ -159,6 +161,8 @@ module Make (A : ARG) = (* : S with module A = A *) struct encoded_le = Comb_map.empty; simplex = SimpSolver.create ~stat (); last_res = None; + n_propagate = Stat.mk_int stat "th.lra.propagate"; + n_conflict = Stat.mk_int stat "th.lra.conflicts"; } let[@inline] reset_res_ (self : state) : unit = self.last_res <- None @@ -175,7 +179,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct SimpSolver.pop_levels self.simplex n; () - let fresh_term self ~pre ty = A.Gensym.fresh_term self.gensym ~pre ty + let fresh_term self ~pre ty = Gensym.fresh_term self.gensym ~pre ty let fresh_lit (self : state) ~mk_lit ~pre : Lit.t = let t = fresh_term ~pre self (Term.bool self.tst) in @@ -239,7 +243,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct | 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_real self.tst) in (* TODO: define proxy *) self.encoded_le <- Comb_map.add le_comb proxy self.encoded_le; Log.debugf 50 (fun k -> @@ -251,7 +255,9 @@ module Make (A : ARG) = (* : S with module A = A *) struct proxy) let add_clause_lra_ ?using (module PA : SI.PREPROCESS_ACTS) lits = - let pr = Proof_trace.add_step PA.proof @@ fun () -> A.lemma_lra lits in + let pr = + Proof_trace.add_step PA.proof @@ fun () -> Proof_rules.lemma_lra lits + in let pr = match using with | None -> pr @@ -281,7 +287,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct (match Comb_map.get le_comb self.encoded_le with | Some x -> x, A.Q.one (* already encoded that *) | None -> - let proxy = fresh_term self ~pre:"_le_comb" (A.ty_lra self.tst) in + let proxy = fresh_term self ~pre:"_le_comb" (A.ty_real self.tst) in self.encoded_le <- Comb_map.add le_comb proxy self.encoded_le; LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb; @@ -400,11 +406,11 @@ module Make (A : ARG) = (* : S with module A = A *) struct (Term.t * Proof_step.id Iter.t) option = let proof_eq t u = Proof_trace.add_step self.proof @@ fun () -> - A.lemma_lra [ Lit.atom self.tst (Term.eq self.tst t u) ] + Proof_rules.lemma_lra [ Lit.atom self.tst (Term.eq self.tst t u) ] in let proof_bool t ~sign:b = let lit = Lit.atom ~sign:b self.tst t in - Proof_trace.add_step self.proof @@ fun () -> A.lemma_lra [ lit ] + Proof_trace.add_step self.proof @@ fun () -> Proof_rules.lemma_lra [ lit ] in match A.view_as_lra t with @@ -462,7 +468,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct | _ -> None (* raise conflict from certificate *) - let fail_with_cert si acts cert : 'a = + let fail_with_cert (self : state) si acts cert : 'a = Profile.with1 "lra.simplex.check-cert" SimpSolver._check_cert cert; let confl = SimpSolver.Unsat_cert.lits cert @@ -470,19 +476,22 @@ module Make (A : ARG) = (* : S with module A = A *) struct |> List.rev_map Lit.neg in let pr = - Proof_trace.add_step (SI.proof si) @@ fun () -> A.lemma_lra confl + Proof_trace.add_step (SI.proof si) @@ fun () -> + Proof_rules.lemma_lra confl in + Stat.incr self.n_conflict; SI.raise_conflict si acts confl pr - let on_propagate_ si acts lit ~reason = + let on_propagate_ self si acts lit ~reason = match lit with | Tag.Lit lit -> (* TODO: more detailed proof certificate *) + Stat.incr self.n_propagate; SI.propagate si acts lit ~reason:(fun () -> let lits = CCList.flat_map (Tag.to_lits si) reason in let pr = Proof_trace.add_step (SI.proof si) @@ fun () -> - A.lemma_lra (lit :: lits) + Proof_rules.lemma_lra (lit :: lits) in CCList.flat_map (Tag.to_lits si) reason, pr) | _ -> () @@ -495,7 +504,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct (SimpSolver.n_rows self.simplex)); let res = Profile.with_ "lra.simplex.solve" @@ fun () -> - SimpSolver.check self.simplex ~on_propagate:(on_propagate_ si acts) + SimpSolver.check self.simplex ~on_propagate:(on_propagate_ self si acts) in Log.debug 5 "(lra.check-simplex.done)"; self.last_res <- Some res; @@ -504,7 +513,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct | SimpSolver.Unsat cert -> Log.debugf 10 (fun k -> k "(@[lra.check.unsat@ :cert %a@])" SimpSolver.Unsat_cert.pp cert); - fail_with_cert si acts cert + fail_with_cert self si acts cert (* TODO: trivial propagations *) @@ -528,7 +537,8 @@ module Make (A : ARG) = (* : S with module A = A *) struct (* [c=0] when [c] is not 0 *) let lit = Lit.atom ~sign:false self.tst @@ Term.eq self.tst t1 t2 in let pr = - Proof_trace.add_step self.proof @@ fun () -> A.lemma_lra [ lit ] + Proof_trace.add_step self.proof @@ fun () -> + Proof_rules.lemma_lra [ lit ] in SI.add_clause_permanent si acts [ lit ] pr ) @@ -537,11 +547,11 @@ module Make (A : ARG) = (* : S with module A = A *) struct try let c1 = SimpSolver.Constraint.geq v le_const in SimpSolver.add_constraint self.simplex c1 tag - ~on_propagate:(on_propagate_ si acts); + ~on_propagate:(on_propagate_ self si acts); let c2 = SimpSolver.Constraint.leq v le_const in SimpSolver.add_constraint self.simplex c2 tag - ~on_propagate:(on_propagate_ si acts) - with SimpSolver.E_unsat cert -> fail_with_cert si acts cert + ~on_propagate:(on_propagate_ self si acts) + with SimpSolver.E_unsat cert -> fail_with_cert self si acts cert ) let add_local_eq (self : state) si acts n1 n2 : unit = @@ -627,12 +637,12 @@ module Make (A : ARG) = (* : S with module A = A *) struct (try SimpSolver.add_var self.simplex v; SimpSolver.add_constraint self.simplex constr (Tag.Lit lit) - ~on_propagate:(on_propagate_ si acts) + ~on_propagate:(on_propagate_ self 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) + fail_with_cert self si acts cert) | None, LRA_pred (Eq, t1, t2) when sign -> add_local_eq_t self si acts t1 t2 ~tag:(Tag.Lit lit) | None, LRA_pred (Neq, t1, t2) when not sign -> diff --git a/src/th-lra/sidekick_th_lra.mli b/src/th-lra/sidekick_th_lra.mli index 11ee0b4c..3f7d897e 100644 --- a/src/th-lra/sidekick_th_lra.mli +++ b/src/th-lra/sidekick_th_lra.mli @@ -1,10 +1,30 @@ (** Linear Rational Arithmetic *) +open Sidekick_core module Intf = Intf +module Predicate = Intf.Predicate +module SMT = Sidekick_smt_solver -include module type of struct - include Intf -end +module type INT = Intf.INT +module type RATIONAL = Intf.RATIONAL + +module S_op = Sidekick_simplex.Op + +type term = Term.t +type ty = Term.t +type pred = Intf.pred = Leq | Geq | Lt | Gt | Eq | Neq +type op = Intf.op = Plus | Minus + +type ('num, 'a) lra_view = ('num, 'a) Intf.lra_view = + | LRA_pred of pred * 'a * 'a + | LRA_op of op * 'a * 'a + | LRA_mult of 'num * 'a + | LRA_const of 'num + | LRA_other of 'a + +val map_view : ('a -> 'b) -> ('c, 'a) lra_view -> ('c, 'b) lra_view + +module type ARG = Intf.ARG (* TODO type state