From 90f100d9b178533b09614f6239d8c3f4a29ee079 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 27 Aug 2022 15:01:25 -0400 Subject: [PATCH] helpers to build terms and solvers --- src/base/ID.ml | 3 ++- src/base/ID.mli | 1 + src/base/LRA_term.ml | 10 ++++++++++ src/base/LRA_term.mli | 16 ++++++++++++++-- src/base/Ty.ml | 2 ++ src/base/Ty.mli | 1 + src/base/Uconst.ml | 3 +++ src/base/Uconst.mli | 1 + src/core-logic/term.ml | 1 + src/core-logic/term.mli | 1 + src/core/default_cc_view.ml | 3 ++- src/smt/solver.ml | 9 +++++++++ src/smt/solver.mli | 12 ++++++++++++ 13 files changed, 59 insertions(+), 4 deletions(-) diff --git a/src/base/ID.ml b/src/base/ID.ml index a1e5f808..c3c23053 100644 --- a/src/base/ID.ml +++ b/src/base/ID.ml @@ -16,8 +16,9 @@ let to_string id = id.name let equal a b = a.id = b.id let compare a b = CCInt.compare a.id b.id let hash a = CCHash.int a.id -let pp out a = Format.fprintf out "%s/%d" a.name a.id +let pp_full out a = Format.fprintf out "%s/%d" a.name a.id let pp_name out a = CCFormat.string out a.name +let pp = pp_name let to_string_full a = Printf.sprintf "%s/%d" a.name a.id module AsKey = struct diff --git a/src/base/ID.mli b/src/base/ID.mli index 0e96c3fa..d3929d2c 100644 --- a/src/base/ID.mli +++ b/src/base/ID.mli @@ -40,6 +40,7 @@ val to_string_full : t -> string include Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t val pp_name : t CCFormat.printer +val pp_full : t CCFormat.printer module Map : CCMap.S with type key = t module Set : CCSet.S with type elt = t diff --git a/src/base/LRA_term.ml b/src/base/LRA_term.ml index c7b3c7ec..db8c4811 100644 --- a/src/base/LRA_term.ml +++ b/src/base/LRA_term.ml @@ -49,11 +49,21 @@ let pred tst p t1 t2 : term = let p = Term.const tst (Const.make (Pred p) ops ~ty) in Term.app_l tst p [ t1; t2 ] +let leq tst a b = pred tst Pred.Leq a b +let lt tst a b = pred tst Pred.Lt a b +let geq tst a b = pred tst Pred.Geq a b +let gt tst a b = pred tst Pred.Gt a b +let eq tst a b = pred tst Pred.Eq a b +let neq tst a b = pred tst Pred.Neq a b + let op tst op t1 t2 : term = let ty = Term.(arrow_l tst [ real tst; real tst ] (real tst)) in let p = Term.const tst (Const.make (Op op) ops ~ty) in Term.app_l tst p [ t1; t2 ] +let plus tst a b = op tst Op.Plus a b +let minus tst a b = op tst Op.Minus a b + let view (t : term) : _ View.t = let f, args = Term.unfold_app t in match T.view f, args with diff --git a/src/base/LRA_term.mli b/src/base/LRA_term.mli index a6f7b5d3..f4188842 100644 --- a/src/base/LRA_term.mli +++ b/src/base/LRA_term.mli @@ -6,6 +6,7 @@ module View = Arith_types_.LRA_view type term = Term.t type ty = Term.t +val term_of_view : Term.store -> term View.t -> term val real : Term.store -> ty val has_ty_real : term -> bool val pred : Term.store -> Pred.t -> term -> term -> term @@ -13,7 +14,18 @@ val mult_by : Term.store -> Q.t -> term -> term val op : Term.store -> Op.t -> term -> term -> term val const : Term.store -> Q.t -> term +(** {2 Helpers} *) + +val leq : Term.store -> term -> term -> term +val lt : Term.store -> term -> term -> term +val geq : Term.store -> term -> term -> term +val gt : Term.store -> term -> term -> term +val eq : Term.store -> term -> term -> term +val neq : Term.store -> term -> term -> term +val plus : Term.store -> term -> term -> term +val minus : Term.store -> term -> term -> term + +(** {2 View} *) + val view : term -> term View.t (** View as LRA *) - -val term_of_view : Term.store -> term View.t -> term diff --git a/src/base/Ty.ml b/src/base/Ty.ml index 2e2f7cc8..1bd6e2d0 100644 --- a/src/base/Ty.ml +++ b/src/base/Ty.ml @@ -59,6 +59,8 @@ let is_int t = let uninterpreted tst id : t = mk_ty0 tst (Ty_uninterpreted { id; finite = false }) +let uninterpreted_str tst s : t = uninterpreted tst (ID.make s) + let is_uninterpreted (self : t) = match view self with | E_const { Const.c_view = Ty (Ty_uninterpreted _); _ } -> true diff --git a/src/base/Ty.mli b/src/base/Ty.mli index 1ac9ad8e..ccd701a9 100644 --- a/src/base/Ty.mli +++ b/src/base/Ty.mli @@ -13,6 +13,7 @@ val bool : store -> t val real : store -> t val int : store -> t val uninterpreted : store -> ID.t -> t +val uninterpreted_str : store -> string -> t val is_uninterpreted : t -> bool val is_real : t -> bool val is_int : t -> bool diff --git a/src/base/Uconst.ml b/src/base/Uconst.ml index 8a6cd14a..4c09220e 100644 --- a/src/base/Uconst.ml +++ b/src/base/Uconst.ml @@ -39,6 +39,9 @@ let uconst_of_id' tst id args ret = let ty = Term.arrow_l tst args ret in uconst_of_id tst id ty +let uconst_of_str tst name args ret : term = + uconst_of_id' tst (ID.make name) args ret + module As_key = struct type nonrec t = t diff --git a/src/base/Uconst.mli b/src/base/Uconst.mli index ed7faa59..8bd2787d 100644 --- a/src/base/Uconst.mli +++ b/src/base/Uconst.mli @@ -18,6 +18,7 @@ val make : ID.t -> ty -> t val uconst : Term.store -> t -> Term.t val uconst_of_id : Term.store -> ID.t -> ty -> Term.t val uconst_of_id' : Term.store -> ID.t -> ty list -> ty -> Term.t +val uconst_of_str : Term.store -> string -> ty list -> ty -> Term.t module Map : CCMap.S with type key = t module Tbl : CCHashtbl.S with type key = t diff --git a/src/core-logic/term.ml b/src/core-logic/term.ml index 33884ee3..e77a2cb6 100644 --- a/src/core-logic/term.ml +++ b/src/core-logic/term.ml @@ -168,6 +168,7 @@ module Store = struct (* TODO: use atomic? CCAtomic? *) let n = ref 0 + let size self = Hcons.size self.s_exprs let create ?(size = 256) () : t = (* store id, modulo 2^5 *) diff --git a/src/core-logic/term.mli b/src/core-logic/term.mli index 9bd8ec81..b9d2ac67 100644 --- a/src/core-logic/term.mli +++ b/src/core-logic/term.mli @@ -111,6 +111,7 @@ module Store : sig type t = store val create : ?size:int -> unit -> t + val size : t -> int end val type_ : store -> t diff --git a/src/core/default_cc_view.ml b/src/core/default_cc_view.ml index 84e0ad7e..4718ff5a 100644 --- a/src/core/default_cc_view.ml +++ b/src/core/default_cc_view.ml @@ -4,7 +4,8 @@ module View = CC_view let view_as_cc (t : Term.t) : _ CC_view.t = let f, args = Term.unfold_app t in match Term.view f, args with - | _, [ _; t; u ] when T_builtins.is_eq f -> View.Eq (t, u) + | Term.E_const { Const.c_view = T_builtins.C_eq; _ }, [ _; t; u ] -> + View.Eq (t, u) | Term.E_const { Const.c_view = T_builtins.C_ite; _ }, [ _ty; a; b; c ] -> View.If (a, b, c) | Term.E_const { Const.c_view = T_builtins.C_not; _ }, [ a ] -> View.Not a diff --git a/src/smt/solver.ml b/src/smt/solver.ml index d2157216..33b539b5 100644 --- a/src/smt/solver.ml +++ b/src/smt/solver.ml @@ -116,6 +116,15 @@ let create arg ?(stat = Stat.global) ?size ~proof ~theories tst () : t = (P.add_step self.proof @@ fun () -> Rule_.lemma_true t_true)); self +let default_arg = + (module struct + let view_as_cc = Default_cc_view.view_as_cc + let is_valid_literal _ = true + end : ARG) + +let create_default ?stat ?size ~proof ~theories tst () : t = + create default_arg ?stat ?size ~proof ~theories tst () + let[@inline] solver self = self.solver let[@inline] stats self = self.stat let[@inline] tst self = Solver_internal.tst self.si diff --git a/src/smt/solver.mli b/src/smt/solver.mli index d297cc6a..1d6f53a5 100644 --- a/src/smt/solver.mli +++ b/src/smt/solver.mli @@ -67,6 +67,18 @@ val create : @param theories theories to load from the start. Other theories can be added using {!add_theory}. *) +val create_default : + ?stat:Stat.t -> + ?size:[ `Big | `Tiny | `Small ] -> + (* TODO? ?config:Config.t -> *) + proof:proof_trace -> + theories:Theory.t list -> + Term.store -> + unit -> + t +(** Create a new solver with the default CC view, and where all boolean subterms + are mapped to boolean atoms. *) + val add_theory : t -> Theory.t -> unit (** Add a theory to the solver. This should be called before any call to {!solve} or to {!add_clause} and the likes (otherwise