Merge branch 'master' of github.com:c-cube/sidekick

src/smtlib/Process.ml

@@ -75,6 +75,7 @@ module Form =  struct
         else Error.errorf "non boolean value %a in ite" Value.pp a
       | B_equiv (a,b) | B_eq(a,b) -> Value.bool (Value.equal a b)
       | B_atom v -> v
+      | B_opaque_bool t -> Error.errorf "cannot evaluate opaque bool %a" pp t
       | B_not _ | B_and _ | B_or _ | B_imply _
         -> Error.errorf "non boolean value in boolean connective"
 
@@ -169,6 +170,7 @@ module Form =  struct
     | B_equiv (a,b) -> equiv st a b
     | B_eq (a,b) -> T.eq st a b
     | B_not t -> not_ st t
+    | B_opaque_bool t -> t
 
   module Gensym = struct
     type t = {

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -9,6 +9,7 @@ type 'a bool_view =
   | B_equiv of 'a * 'a
   | B_eq of 'a * 'a
   | B_ite of 'a * 'a * 'a
+  | B_opaque_bool of 'a (* do not enter *)
   | B_atom of 'a
 
 module type ARG = sig
@@ -86,6 +87,7 @@ module Make(A : ARG) : S with module A = A = struct
     | 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_opaque_bool _ -> None
     | B_and a ->
       if IArray.exists is_false a then Some (T.bool tst false)
       else if IArray.for_all is_true a then Some (T.bool tst true)
@@ -129,6 +131,7 @@ module Make(A : ARG) : S with module A = A = struct
     let rec get_lit (t:T.t) : Lit.t =
       match A.view_as_bool t with
       | B_bool b -> mk_lit (T.bool self.tst b)
+      | B_opaque_bool t -> mk_lit t
       | B_not u ->
         let lit = get_lit u in
         Lit.neg lit