helpers to build terms and solvers

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

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

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

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

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

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

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
 

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

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 *)

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

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

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

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