From b332e8ceb09e9ee154108bf532e3e281b6bb44d2 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 14 Jan 2020 20:23:23 -0600 Subject: [PATCH] fix: preprocess away "ite" --- src/core/Sidekick_core.ml | 3 +-- src/smtlib/Form.ml | 12 ++++-------- src/smtlib/Typecheck.ml | 2 +- src/th-bool-static/Sidekick_th_bool_static.ml | 18 +++++++++++++++--- 4 files changed, 21 insertions(+), 14 deletions(-) diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 165f025f..af28909e 100644 --- a/src/core/Sidekick_core.ml +++ b/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. - Can also add clauses to the simplifier. *) + (** Given a term, try to simplify it. Return [None] if it didn't change. *) val normalize : t -> term -> term (** Normalize a term using all the hooks. *) diff --git a/src/smtlib/Form.ml b/src/smtlib/Form.ml index e819171d..417fd943 100644 --- a/src/smtlib/Form.ml +++ b/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 = - if ID.equal id id_ite then T.ty (IArray.get args 1) - else Ty.bool + let get_ty _ _ = 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 diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index e5a565fc..4bc8b228 100644 --- a/src/smtlib/Typecheck.ml +++ b/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) -> diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 8bff46fb..7f729e11 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/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 _ -> - mk_lit t + | B_ite _ | B_eq _ -> 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)";