fix: preprocess away "ite"

src/core/Sidekick_core.ml

@@ -366,8 +366,7 @@ module type SOLVER_INTERNAL = sig
     (** Reset internal cache, etc. *)
 
     type hook = t -> term -> term option
-    (** Given a term, try to simplify it. Return [None] if it didn't change.
+    (** 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. *)

src/smtlib/Form.ml

@@ -7,7 +7,6 @@ exception Not_a_th_term
 let id_and = ID.make "and"
 let id_or = ID.make "or"
 let id_imply = ID.make "=>"
-let id_ite = ID.make "ite"
 
 let view_id fid args =
   if ID.equal fid id_and then (
@@ -18,8 +17,6 @@ let view_id fid args =
     (* conclusion is stored first *)
     let len = IArray.length args in
     B_imply (IArray.sub args 1 (len-1), IArray.get args 0)
-  ) else if ID.equal fid id_ite && IArray.length args = 3 then (
-    B_ite (IArray.get args 0, IArray.get args 1, IArray.get args 2)
   ) else (
     raise_notrace Not_a_th_term
   )
@@ -29,14 +26,13 @@ let view_as_bool (t:T.t) : T.t bool_view =
   | Bool b -> B_bool b
   | Not u -> B_not u
   | Eq (a, b) when Ty.is_bool (T.ty a) -> B_equiv (a,b)
+  | Ite (a,b,c) -> B_ite(a,b,c)
   | App_fun ({fun_id; _}, args) ->
     (try view_id fun_id args with Not_a_th_term -> B_atom t)
   | _ -> B_atom t
 
 module Funs = struct
-  let get_ty id args =
+  let get_ty _ _ = Ty.bool
-    if ID.equal id id_ite then T.ty (IArray.get args 1)
-    else Ty.bool
 
   let abs ~self _a =
     match T.view self with
@@ -76,7 +72,7 @@ module Funs = struct
   let and_ = mk_fun id_and
   let or_ = mk_fun id_or
   let imply = mk_fun id_imply
-  let ite = mk_fun id_ite
+  let ite = Term.ite
 end
 
 let as_id id (t:T.t) : T.t IArray.t option =
@@ -117,7 +113,7 @@ let not_ = T.not_
 
 let ite st a b c = match T.view a with
   | T.Bool ba -> if ba then b else c
-  | _ -> T.app_fun st Funs.ite (IArray.of_array_unsafe [| a;b;c |])
+  | _ -> T.ite st a b c
 
 let equiv st a b =
   if T.equal a b then T.true_ st

src/smtlib/Typecheck.ml

@@ -144,7 +144,7 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
     let a = conv_term ctx a in
     let b = conv_term ctx b in
     let c = conv_term ctx c in
-    T.ite tst a b c
+    Form.ite tst a b c
   | PA.Fun _ | PA.Forall _ | PA.Exists _ ->
     errorf_ctx ctx "cannot process lambda/quantifiers in %a" PA.pp_term t
   | PA.Let (vbs, body) ->

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -115,7 +115,8 @@ module Make(A : ARG) : S with module A = A = struct
       begin match A.view_as_bool a with
         | B_bool true -> Some b
         | B_bool false -> Some c
-        | _ -> None
+        | _ ->
+          None
       end
     | B_equiv (a,b) when is_true a -> Some b
     | B_equiv (a,b) when is_false a -> Some (not_ tst b)
@@ -131,6 +132,17 @@ module Make(A : ARG) : S with module A = A = struct
     let t = fresh_term ~pre self Ty.bool in
     mk_lit t
 
+  (* preprocess "ite" away *)
+  let preproc_ite self _si ~mk_lit ~add_clause (t:T.t) : T.t option =
+    match A.view_as_bool t with
+    | B_ite (a,b,c) ->
+      let t_a = fresh_term self ~pre:"ite" (T.ty b) in
+      let lit_a = mk_lit a in
+      add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_a b)];
+      add_clause [lit_a; mk_lit (eq self.tst t_a c)];
+      Some t_a
+    | _ -> None
+
   (* TODO: polarity? *)
   let cnf (self:state) (_si:SI.t) ~mk_lit ~add_clause (t:T.t) : T.t option =
     let rec get_lit (t:T.t) : Lit.t =
@@ -173,8 +185,7 @@ module Make(A : ARG) : S with module A = A = struct
           or_a self.tst @@
           IArray.append (IArray.map (not_ self.tst) args) (IArray.singleton u) in
         get_lit t'
-      | B_ite _ | B_eq _ ->
+      | B_ite _ | B_eq _ -> mk_lit t
-        mk_lit t
       | B_equiv (a,b) ->
         let a = get_lit a in
         let b = get_lit b in
@@ -225,6 +236,7 @@ module Make(A : ARG) : S with module A = A = struct
     Log.debug 2 "(th-bool.setup)";
     let st = create (SI.tst si) in
     SI.add_simplifier si (simplify st);
+    SI.add_preprocess si (preproc_ite st);
     SI.add_preprocess si (cnf st);
     if A.check_congruence_classes then (
       Log.debug 5 "(th-bool.add-final-check)";