wip: preprocess/simplify as part of theories

src/base-term/Base_types.ml

@@ -594,6 +594,8 @@ module Term : sig
 
   val iter_dag : t -> t Iter.t
 
+  val map_shallow : state -> (t -> t) -> t -> t
+
   val pp : t Fmt.printer
 
   (** {6 Views} *)
@@ -745,6 +747,13 @@ end = struct
   let iter_dag t yield =
     let st = Iter_dag.create() in
     Iter_dag.iter_dag st t yield
+
+  let map_shallow (tst:state) f (t:t) : t =
+    match view t with
+    | Bool _ -> t
+    | App_fun (hd, a) -> app_fun tst hd (IArray.map f a)
+    | Not u -> not_ tst (f u)
+    | Eq (a,b) -> eq tst (f a) (f b)
 end
 
 module Lit : sig

src/core/Sidekick_core.ml

@@ -78,6 +78,9 @@ module type TERM = sig
     val bool : state -> bool -> t (* build true/false *)
     val as_bool : t -> bool option
 
+    val map_shallow : state -> (t -> t) -> t -> t
+    (** Map function on immediate subterms *)
+
     val iter_dag : t -> (t -> unit) -> unit
 
     module Tbl : Hashtbl.S with type key = t
@@ -312,13 +315,37 @@ module type SOLVER_INTERNAL = sig
       Its negation will become a conflict clause *)
   type conflict = lit list
 
-  (** {3 Actions available to theories} *)
-
   val tst : t -> term_state
 
   val cc : t -> CC.t
   (** Congruence closure for this solver *)
 
+  (** {3 Simplifiers} *)
+
+  module Simplify : sig
+    type t
+
+    val tst : t -> term_state
+
+    val clear : t -> unit
+    (** Reset internal cache, etc. *)
+
+    type hook = t -> term -> term option
+    (** Given a term, try to simplify it. Return [None] if it didn't change.
+        Can also add clauses to the simplifier. *)
+
+    val normalize : t -> term -> term
+    (** Normalize a term using all the hooks. *)
+  end
+
+  type simplify_hook = Simplify.hook
+
+  val add_simplifier : t -> Simplify.hook -> unit
+
+  val simplifier : t -> Simplify.t
+
+  val simp_t : t -> term -> term
+
   (** {3 hooks for the theory} *)
 
   type actions
@@ -398,6 +425,17 @@ module type SOLVER_INTERNAL = sig
       Must be complete (i.e. must raise a conflict if the set of literals is
       not satisfiable) and can be expensive. The function
       is given the whole trail. *)
+
+  (** {3 Preprocessors}
+      These preprocessors turn mixed, raw literals (possibly simplified) into
+      literals suitable for reasoning.
+      Typically some clauses are also added to the solver. *)
+
+  type preprocess_hook = t -> actions -> term -> term option
+  (** Given a term, try to preprocess it. Return [None] if it didn't change.
+      Can also add clauses to define new terms. *)
+
+  val add_preprocess : t -> preprocess_hook -> unit
 end
 
 (** Public view of the solver *)

src/msat-solver/Sidekick_msat_solver.ml

@@ -67,6 +67,43 @@ module Make(A : ARG)
 
     type actions = msat_acts
 
+    module Simplify = struct
+      type t = {
+        tst: term_state;
+        mutable hooks: hook list;
+        cache: T.t T.Tbl.t;
+      }
+      and hook = t -> term -> term option
+
+      let create tst : t = {tst; hooks=[]; cache=T.Tbl.create 32;}
+      let[@inline] tst self = self.tst
+      let add_hook self f = self.hooks <- f :: self.hooks
+      let clear self = T.Tbl.clear self.cache
+
+      let normalize (self:t) (t:T.t) : T.t =
+        (* compute and cache normal form of [t] *)
+        let rec aux t =
+          match T.Tbl.find self.cache t with
+          | u -> u
+          | exception Not_found ->
+            let u = aux_rec t self.hooks in
+            T.Tbl.add self.cache t u;
+            u
+        (* try each function in [hooks] successively, and rewrite subterms *)
+        and aux_rec t hooks = match hooks with
+          | [] ->
+            let u = T.map_shallow self.tst aux t in
+            if T.equal t u then t else aux u
+          | h :: hooks_tl ->
+            match h self t with
+            | None -> aux_rec t hooks_tl
+            | Some u when T.equal t u -> aux_rec t hooks_tl
+            | Some u -> aux u
+        in
+        aux t
+    end
+    type simplify_hook = Simplify.hook
+
     type t = {
       tst: T.state; (** state for managing terms *)
       cc: CC.t lazy_t; (** congruence closure *)
@@ -74,10 +111,15 @@ module Make(A : ARG)
       count_axiom: int Stat.counter;
       count_conflict: int Stat.counter;
       count_propagate: int Stat.counter;
+      simp: Simplify.t;
+      mutable preprocess: preprocess_hook list;
+      preprocess_cache: T.t T.Tbl.t;
       mutable th_states : th_states; (** Set of theories *)
       mutable on_partial_check: (t -> actions -> lit Iter.t -> unit) list;
       mutable on_final_check: (t -> actions -> lit Iter.t -> unit) list;
     }
+    and preprocess_hook = t -> actions -> term -> term option
+
     type solver = t
 
     module Formula = struct
@@ -95,6 +137,12 @@ module Make(A : ARG)
     let[@inline] cc (t:t) = Lazy.force t.cc
     let[@inline] tst t = t.tst
 
+    let simplifier self = self.simp
+    let simp_t self (t:T.t) : T.t = Simplify.normalize self.simp t
+    let add_simplifier (self:t) f : unit = Simplify.add_hook self.simp f
+
+    let add_preprocess self f = self.preprocess <- f :: self.preprocess
+
     let[@inline] raise_conflict self acts c : 'a =
       Stat.incr self.count_conflict;
       acts.Msat.acts_raise_conflict c A.Proof.default
@@ -110,7 +158,31 @@ module Make(A : ARG)
       Stat.incr self.count_axiom;
       acts.Msat.acts_add_clause ~keep lits A.Proof.default
 
-    let[@inline] mk_lit self _acts ?sign t = Lit.atom self.tst ?sign t
+    let preprocess_lit_ (self:t) (acts:actions) (lit:lit) : lit =
+      (* compute and cache normal form of [t] *)
+      let rec aux t =
+        match T.Tbl.find self.preprocess_cache t with
+        | u -> u
+        | exception Not_found ->
+          (* first, map subterms *)
+          let u = T.map_shallow self.tst aux t in
+          (* then rewrite *)
+          let u = aux_rec u self.preprocess in
+          T.Tbl.add self.preprocess_cache t u;
+          u
+      (* try each function in [hooks] successively *)
+      and aux_rec t hooks = match hooks with
+        | [] -> t
+        | h :: hooks_tl ->
+          match h self acts t with
+          | None -> aux_rec t hooks_tl
+          | Some u -> aux u
+      in
+      let t = aux (Lit.term lit) in
+      Lit.atom self.tst ~sign:(Lit.sign lit) t
+
+    let[@inline] mk_lit self acts ?sign t =
+      preprocess_lit_ self acts @@ Lit.atom self.tst ?sign t
 
     let[@inline] add_clause_temp self acts lits : unit =
       add_sat_clause_ self acts ~keep:false lits
@@ -118,8 +190,7 @@ module Make(A : ARG)
     let[@inline] add_clause_permanent self acts lits : unit =
       add_sat_clause_ self acts ~keep:true lits
 
-    let[@inline] add_lit _self acts lit : unit =
+    let add_lit _self acts lit : unit = acts.Msat.acts_mk_lit lit
-      acts.Msat.acts_mk_lit lit
 
     let add_lit_t self acts ?sign t = add_lit self acts (mk_lit self acts ?sign t)
 
@@ -215,6 +286,9 @@ module Make(A : ARG)
         );
         th_states=Ths_nil;
         stat;
+        simp=Simplify.create tst;
+        preprocess=[];
+        preprocess_cache=T.Tbl.create 32;
         count_axiom = Stat.mk_int stat "th-axioms";
         count_propagate = Stat.mk_int stat "th-propagations";
         count_conflict = Stat.mk_int stat "th-conflicts";

src/smtlib/Process.ml

@@ -35,6 +35,7 @@ module Form =  struct
 
   let view_as_bool (t:T.t) : T.t bool_view =
     match T.view t with
+    | Bool b -> B_bool b
     | Not u -> B_not u
     | Eq (a, b) when Ty.is_bool (T.ty a) -> B_equiv (a,b)
     | App_fun ({fun_id; _}, args) ->
@@ -57,6 +58,7 @@ module Form =  struct
     let eval id args =
       let open Value in
       match view_id id args with
+      | B_bool b -> Value.bool b
       | B_not (V_bool b) -> Value.bool (not b)
       | B_and a when IArray.for_all Value.is_true a -> Value.true_
       | B_and a when IArray.exists Value.is_false a -> Value.false_
@@ -156,6 +158,7 @@ module Form =  struct
       and_l tst cs
 
   let mk_bool st = function
+    | B_bool b -> T.bool st b
     | B_atom t -> t
     | B_and l -> and_a st l
     | B_or l -> or_a st l
@@ -165,19 +168,6 @@ module Form =  struct
     | B_eq (a,b) -> T.eq st a b
     | B_not t -> not_ st t
 
-  let view_as_non_bool t =
-    match T.view t with
-    | T.App_fun (f, args) ->
-      begin match view_id (Fun.id f) args with
-        | exception Not_a_th_term ->
-          NB_functor(args, fun tst args -> T.app_fun tst f args)
-        | B_ite (a,b,c) -> NB_ite(a,b,c)
-        | _ -> NB_bool t
-      end
-    | T.Bool _ | T.Eq _ | T.Not _ -> NB_bool t
-
-  let mk_ite = ite
-
   module Gensym = struct
     type t = {
       tst: T.state;
@@ -508,8 +498,6 @@ let solve
       Format.printf "Unknown (:reason %a)" Solver.Unknown.pp reas
   end
 
-(* NOTE: hack for testing with dimacs. Proper treatment should go into
-   scoping in Ast, or having theory-specific state in `Term.state` *)
 (* process a single statement *)
 let process_stmt
     ?hyps

src/smtlib/Typecheck.ml

@@ -16,11 +16,7 @@ let pp_loc_opt = Loc.pp_opt
 
 (** {2 Parsing} *)
 
-module StrTbl = CCHashtbl.Make(struct
+module StrTbl = CCHashtbl.Make(CCString)
-    type t = string
-    let equal = CCString.equal
-    let hash = CCString.hash
-  end)
 
 module Ctx = struct
   type kind =
@@ -324,13 +320,6 @@ let rec conv_term ctx (t:PA.term) : A.term = match t with
   | _ ->
     errorf_ctx ctx "unsupported term %a" PA.pp_term t
 
-let find_file_ name ~dir : string option =
-  Log.debugf 2 (fun k->k "search %s in %s" name dir);
-  let abs_path = Filename.concat dir name in
-  if Sys.file_exists abs_path
-  then Some abs_path
-  else None
-
 let conv_fun_decl ctx f : string * A.Ty.t =
   if f.PA.fun_ty_vars <> [] then (
     errorf_ctx ctx "cannot convert polymorphic function@ %a"

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -1,6 +1,7 @@
 (** {2 Signatures for booleans} *)
 
 type 'a bool_view =
+  | B_bool of bool
   | B_not of 'a
   | B_and of 'a IArray.t
   | B_or of 'a IArray.t
@@ -10,11 +11,6 @@ type 'a bool_view =
   | B_ite of 'a * 'a * 'a
   | B_atom of 'a
 
-type ('tst,'a) non_bool_view =
-  | NB_ite of 'a * 'a * 'a
-  | NB_functor of 'a IArray.t * ('tst -> 'a IArray.t -> 'a)
-  | NB_bool of 'a (* boolean subterm *)
-
 module type ARG = sig
   module S : Sidekick_core.SOLVER
 
@@ -23,14 +19,9 @@ module type ARG = sig
   val view_as_bool : term -> term bool_view
   (** Project the term into the boolean view *)
 
-  val view_as_non_bool : term -> (S.A.Term.state,term) non_bool_view
-  (** Project the term into the boolean view *)
-
   val mk_bool : S.A.Term.state -> term bool_view -> term
   (** Make a term from the given boolean view *)
 
-  val mk_ite : S.A.Term.state -> term -> term -> term -> term
-
   module Gensym : sig
     type t
 
@@ -44,15 +35,16 @@ end
 module type S = sig
   module A : ARG
   module T = A.S.A.Term
+  module SI = A.S.Solver_internal
 
   type state
 
   val create : T.state -> state
 
-  val simplify : state -> T.t -> T.t
+  val simplify : state -> SI.simplify_hook
   (** Simplify given term *)
 
-  val cnf : state -> T.t -> A.S.A.Lit.t list Vec.t
+  val cnf : state -> SI.preprocess_hook
   (** add clauses for the booleans within the term. *)
 
   val theory : A.S.theory
@@ -63,6 +55,7 @@ module Make(A : ARG) : S with module A = A = struct
   module Ty = A.S.A.Ty
   module T = A.S.A.Term
   module Lit = A.S.A.Lit
+  module SI = A.S.Solver_internal
 
   type state = {
     tst: T.state;
@@ -88,118 +81,85 @@ module Make(A : ARG) : S with module A = A = struct
   let is_true t = match T.as_bool t with Some true -> true | _ -> false
   let is_false t = match T.as_bool t with Some false -> true | _ -> false
     
-  let simplify (self:state) (t:T.t) : T.t =
+  let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : T.t option =
-    let rec aux t =
     let tst = self.tst in
-      match T.Tbl.find self.simps t with
-      | u -> u
-      | exception Not_found ->
-        let u, cache =
     match A.view_as_bool t with
-          | B_not u -> not_ tst (aux u), false
+    | B_bool _ -> None
+    | B_not u when is_true u -> Some (T.bool tst false)
+    | B_not u when is_false u -> Some (T.bool tst true)
+    | B_not _ -> None
     | B_and a ->
-            let a = IArray.map aux a in
+      if IArray.exists is_false a then Some (T.bool tst false)
-            let u = 
+      else if IArray.for_all is_true a then Some (T.bool tst true)
-              if IArray.exists is_false a then T.bool tst false
+      else None
-              else if IArray.for_all is_true a then T.bool tst true
-              else and_a tst a
-            in
-            u, true
     | B_or a ->
-            let a = IArray.map aux a in
+      if IArray.exists is_true a then Some (T.bool tst true)
-            let u = 
+      else if IArray.for_all is_false a then Some (T.bool tst false)
-              if IArray.exists is_true a then T.bool tst true
+      else None
-              else if IArray.for_all is_false a then T.bool tst false
-              else or_a tst a
-            in
-            u, true
     | B_imply (args, u) ->
       (* turn into a disjunction *)
       let u =
-              aux @@ or_a tst @@
+        or_a tst @@
         IArray.append (IArray.map (not_ tst) args) (IArray.singleton u)
       in
-            u, true
+      Some u
     | B_ite (a,b,c) ->
-            let a = aux a in
+      (* directly simplify [a] so that maybe we never will simplify one
-            begin match T.as_bool a with
+         of the branches *)
-              | Some true -> aux b
+      let a = SI.Simplify.normalize simp a in
-              | Some false -> aux c
+      begin match A.view_as_bool a with
-              | _ -> ite tst a (aux b) (aux c)
+        | B_bool true -> Some b
-            end, true
+        | B_bool false -> Some c
-          | B_equiv (a,b) ->
+        | _ -> None
-            let u = equiv tst (aux a) (aux b) in
-            u, true
-          | B_eq (a,b) ->
-            let u = eq tst (aux a) (aux b) in
-            u, true
-          | B_atom a ->
-            begin match A.view_as_non_bool a with
-              | NB_bool _ -> assert false
-              | NB_ite (a,b,c) ->
-                A.mk_ite tst (aux a) (aux b) (aux c), true
-              | NB_functor (args, mk) ->
-                mk tst (IArray.map aux args), true
       end
-        in
+    | B_equiv (a,b) when is_true a -> Some b
-        if cache then (
+    | B_equiv (a,b) when is_false a -> Some (not_ tst b)
-          T.Tbl.add self.simps t u; (* cache rewriting step *)
+    | B_equiv (a,b) when is_true b -> Some a
-        );
+    | B_equiv (a,b) when is_false b -> Some (not_ tst a)
-        u
+    | B_equiv _ -> None
-    in
+    | B_eq (a,b) when T.equal a b -> Some (T.bool tst true)
-    let u = aux t in
+    | B_eq _ -> None
-    if not (T.equal t u) then (
+    | B_atom _ -> None
-      Log.debugf 5
-        (fun k->k "(@[th-bool.simplified@ :from %a@ :to %a@])" T.pp t T.pp u);
-    );
-    u
 
   let fresh_term self ~pre ty = A.Gensym.fresh_term self.gensym ~pre ty
   let fresh_lit (self:state) ~pre : Lit.t =
     let t = fresh_term ~pre self Ty.bool in
     Lit.atom self.tst t
 
-  (* TODO: polarity *)
+  (* TODO: polarity? *)
-  let cnf (self:state) (t:T.t) : Lit.t list Vec.t =
+  let cnf (self:state) (solver:SI.t) (acts:SI.actions) (t:T.t) : T.t option =
-    let cs: Lit.t list Vec.t = Vec.create() in
+    let add_clause lits = SI.add_clause_permanent solver acts lits in
-    let add_clause lits = Vec.push cs lits in
+    let rec get_lit (t:T.t) : Lit.t =
-    let rec aux_bool (t:T.t) : Lit.t =
-      let tst = self.tst in
-      match T.Tbl.find self.cnf t with
-      | u -> u
-      | exception Not_found ->
-        let lit, cache =
       match A.view_as_bool t with
+      | B_bool b -> Lit.atom self.tst ~sign:b (T.bool self.tst true)
       | B_not u ->
-            let lit = aux_bool u in
+        let lit = get_lit u in
-            Lit.neg lit, false
+        Lit.neg lit
       | B_and l ->
-            let subs = IArray.to_list_map aux_bool l in
+        let subs = IArray.to_list_map get_lit l in
         let proxy = fresh_lit ~pre:"and_" self in
         (* add clauses *)
         List.iter (fun u -> add_clause [Lit.neg proxy; u]) subs;
         add_clause (proxy :: List.map Lit.neg subs);
-            proxy, true
+        proxy
       | B_or l ->
-            let subs = IArray.to_list_map aux_bool l in
+        let subs = IArray.to_list_map get_lit l in
         let proxy = fresh_lit ~pre:"or_" self in
         (* add clauses *)
         List.iter (fun u -> add_clause [Lit.neg u; proxy]) subs;
         add_clause (Lit.neg proxy :: subs);
-            proxy, true
+        proxy
       | B_imply (args, u) ->
         let t' =
-              or_a tst @@
+          or_a self.tst @@
-              IArray.append (IArray.map (not_ tst) args) (IArray.singleton u) in
+          IArray.append (IArray.map (not_ self.tst) args) (IArray.singleton u) in
-            aux_bool t', true
+        get_lit t'
-          | B_ite _ ->
+      | B_ite _ | B_eq _ ->
-            Lit.atom tst (aux_t t), true
+        Lit.atom self.tst t
-          | B_eq _ ->
-            Lit.atom tst (aux_t t), true
       | B_equiv (a,b) ->
         Format.printf "@[cnf: equiv@ %a@ and %a@]@." T.pp a T.pp b;
-            let a = aux_bool a in
+        let a = get_lit a in
-            let b = aux_bool b in
+        let b = get_lit b in
         let proxy = fresh_lit ~pre:"equiv_" self in
         (* proxy => a<=> b,
            ¬proxy => a xor b *)
@@ -207,50 +167,19 @@ module Make(A : ARG) : S with module A = A = struct
         add_clause [Lit.neg proxy; Lit.neg b; a];
         add_clause [proxy; a; b];
         add_clause [proxy; Lit.neg a; Lit.neg b];
-            proxy, true
-          | B_atom u ->
-            Lit.atom tst (aux_t u), false
-        in
-        if cache then (
-          T.Tbl.add self.cnf t lit; (* cache rewriting step *)
-        );
-        lit
-
-    and aux_t (t:T.t) : T.t =
-      let tst = self.tst in
-      match A.view_as_non_bool t with
-      | NB_ite (a,b,c) ->
-        begin match T.Tbl.find self.cnf_ite t with
-          | u -> u
-          | exception Not_found ->
-            let a = aux_bool a in
-            let b = aux_t b in
-            let c = aux_t c in
-            let proxy = fresh_term ~pre:"ite_" self (T.ty b) in
-            T.Tbl.add self.cnf_ite t proxy;
-            (* add clauses: [a => proxy=b], [¬a => proxy=c] *)
-            add_clause [Lit.neg a; Lit.atom tst (eq tst proxy b)];
-            add_clause [a; Lit.atom tst (eq tst proxy c)];
         proxy
-        end
+      | B_atom u -> Lit.atom self.tst u
-      | NB_bool _ -> Lit.term (aux_bool t)
-      | NB_functor (args, mk) ->
-        (* pass through *)
-        let args = IArray.map aux_t args in
-        mk tst args
     in
-    (* traverse [t] to produce clauses *)
+    let lit = get_lit t in
-    if Ty.is_bool (T.ty t) then (
+    let u = Lit.term lit in
-      let top = aux_bool t in
+    if T.equal u t then None else Some u
-      add_clause [top]; (* also add a clause standing for [t = true] *)
-    ) else (
-      ignore (aux_t t: T.t);
-    );
-    cs
 
-  (* TODO: register [cnf] as a clausifier, register [simplify] as a
+  let create_and_setup si =
-     preprocessor *)
+    Log.debug 2 "(th-bool.setup)";
-  let create_and_setup _si = ()
+    let st = create (SI.tst si) in
+    SI.add_simplifier si (simplify st);
+    SI.add_preprocess si (cnf st);
+    st
 
   let theory =
     A.S.mk_theory