From 4875b07d0b04d23d38bf5f3810b3f39072525498 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 30 Oct 2019 15:41:52 -0500 Subject: [PATCH] feat: add `Ite` constructor in base-term, handle it in mini-cc --- src/base-term/Base_types.ml | 19 ++++++++++++++++++- src/base-term/Model.ml | 6 ++++++ src/mini-cc/Sidekick_mini_cc.ml | 9 ++++----- src/mini-cc/tests/tests.ml | 20 ++++++++++++++++++++ 4 files changed, 48 insertions(+), 6 deletions(-) diff --git a/src/base-term/Base_types.ml b/src/base-term/Base_types.ml index 7d45cf3b..42b285a5 100644 --- a/src/base-term/Base_types.ml +++ b/src/base-term/Base_types.ml @@ -17,6 +17,7 @@ and 'a term_view = | App_fun of fun_ * 'a IArray.t (* full, first-order application *) | Eq of 'a * 'a | Not of 'a + | Ite of 'a * 'a * 'a and fun_ = { fun_id: ID.t; @@ -140,6 +141,7 @@ let pp_term_view_gen ~pp_id ~pp_t out = function Fmt.fprintf out "(@[<1>%a@ %a@])" pp_id (id_of_fun f) (Util.pp_iarray pp_t) l | Eq (a,b) -> Fmt.fprintf out "(@[=@ %a@ %a@])" pp_t a pp_t b | Not u -> Fmt.fprintf out "(@[not@ %a@])" pp_t u + | Ite (a,b,c) -> Fmt.fprintf out "(@[ite@ %a@ %a@ %a@])" pp_t a pp_t b pp_t c let pp_term_top ~ids out t = let rec pp out t = @@ -384,6 +386,7 @@ module Term_cell : sig | App_fun of fun_ * 'a IArray.t | Eq of 'a * 'a | Not of 'a + | Ite of 'a * 'a * 'a type t = term view @@ -396,6 +399,7 @@ module Term_cell : sig val app_fun : fun_ -> term IArray.t -> t val eq : term -> term -> t val not_ : term -> t + val ite : term -> term -> term -> t val ty : t -> Ty.t (** Compute the type of this term cell. Not totally free *) @@ -423,6 +427,7 @@ end = struct | App_fun of fun_ * 'a IArray.t | Eq of 'a * 'a | Not of 'a + | Ite of 'a * 'a * 'a type t = term view @@ -443,6 +448,7 @@ end = struct Hash.combine3 4 (Fun.hash f) (Hash.iarray sub_hash l) | Eq (a,b) -> Hash.combine3 12 (sub_hash a) (sub_hash b) | Not u -> Hash.combine2 70 (sub_hash u) + | Ite (a,b,c) -> Hash.combine4 80 (sub_hash a)(sub_hash b)(sub_hash c) (* equality that relies on physical equality of subterms *) let equal (a:A.t view) b : bool = match a, b with @@ -451,7 +457,7 @@ end = struct Fun.equal f1 f2 && IArray.equal sub_eq a1 a2 | Eq(a1,b1), Eq(a2,b2) -> sub_eq a1 a2 && sub_eq b1 b2 | Not a, Not b -> sub_eq a b - | Bool _, _ | App_fun _, _ | Eq _, _ | Not _, _ + | (Bool _ | App_fun _ | Eq _ | Not _ | Ite _), _ -> false let pp = pp_term_view_gen ~pp_id:ID.pp_name ~pp_t:A.pp @@ -484,8 +490,11 @@ end = struct | Not u -> u.term_view | _ -> Not t + let ite a b c = Ite (a,b,c) + let ty (t:t): Ty.t = match t with | Bool _ | Eq _ | Not _ -> Ty.bool + | Ite (_, b, _) -> b.term_ty | App_fun (f, args) -> begin match Fun.view f with | Fun_undef fty -> @@ -516,6 +525,7 @@ end = struct | App_fun (_,a) -> IArray.iter f a | Not u -> f u | Eq (a,b) -> f a; f b + | Ite (a,b,c) -> f a; f b; f c let map f view = match view with @@ -523,6 +533,7 @@ end = struct | App_fun (fu,a) -> App_fun (fu, IArray.map f a) | Not u -> Not (f u) | Eq (a,b) -> Eq (f a, f b) + | Ite (a,b,c) -> Ite (f a, f b, f c) module Tbl = CCHashtbl.Make(struct type t = term view @@ -543,6 +554,7 @@ module Term : sig | App_fun of fun_ * 'a IArray.t | Eq of 'a * 'a | Not of 'a + | Ite of 'a * 'a * 'a val id : t -> int val view : t -> term view @@ -563,6 +575,7 @@ module Term : sig val app_fun : state -> fun_ -> t IArray.t -> t val eq : state -> t -> t -> t val not_ : state -> t -> t + val ite : state -> t -> t -> t -> t (** Obtain unsigned version of [t], + the sign as a boolean *) val abs : state -> t -> t * bool @@ -608,6 +621,7 @@ end = struct | App_fun of fun_ * 'a IArray.t | Eq of 'a * 'a | Not of 'a + | Ite of 'a * 'a * 'a let[@inline] id t = t.term_id let[@inline] ty t = t.term_ty @@ -663,6 +677,7 @@ end = struct let[@inline] const st c = app_fun st c IArray.empty let[@inline] eq st a b = make st (Term_cell.eq a b) let[@inline] not_ st a = make st (Term_cell.not_ a) + let ite st a b c : t = make st (Term_cell.ite a b c) (* might need to tranfer the negation from [t] to [sign] *) let abs tst t : t * bool = match view t with @@ -687,6 +702,7 @@ end = struct | App_fun (f,args) -> C.App_fun (f, IArray.to_seq args) | Eq (a,b) -> C.Eq (a, b) | Not u -> C.Not u + | Ite (a,b,c) -> C.If (a,b,c) module As_key = struct type t = term @@ -735,6 +751,7 @@ end = struct | 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) + | Ite (a,b,c) -> ite tst (f a) (f b) (f c) end module Value : sig diff --git a/src/base-term/Model.ml b/src/base-term/Model.ml index 039540ea..6cac8f4c 100644 --- a/src/base-term/Model.ml +++ b/src/base-term/Model.ml @@ -143,6 +143,12 @@ let eval (m:t) (t:Term.t) : Value.t option = | V_bool b -> V_bool (not b) | v -> Error.errorf "@[Model: wrong value@ for boolean %a@ :val %a@]" Term.pp a Value.pp v end + | Ite (a,b,c) -> + begin match aux a with + | V_bool true -> aux b + | V_bool false -> aux c + | v -> Error.errorf "@[Model: wrong value@ for boolean %a@ :val %a@]" Term.pp a Value.pp v + end | Eq(a,b) -> let a = aux a in let b = aux b in diff --git a/src/mini-cc/Sidekick_mini_cc.ml b/src/mini-cc/Sidekick_mini_cc.ml index 4e431765..557beda7 100644 --- a/src/mini-cc/Sidekick_mini_cc.ml +++ b/src/mini-cc/Sidekick_mini_cc.ml @@ -184,11 +184,6 @@ module Make(A: ARG) = struct try T_tbl.find self.tbl t |> Node.root with Not_found -> Error.errorf "mini-cc.find_t: no node for %a" T.pp t - (* does this list contain a duplicate? *) - let has_dups (l:node list) : bool = - Iter.diagonal (Iter.of_list l) - |> Iter.exists (fun (n1,n2) -> Node.equal n1 n2) - exception E_unsat let compute_sig (self:t) (n:node) : Signature.t option = @@ -226,6 +221,10 @@ module Make(A: ARG) = struct self.combine <- (n,self.false_) :: self.combine | Some (Not u) when Node.equal u self.false_ -> self.combine <- (n,self.true_) :: self.combine + | Some (If (a,b,_)) when Node.equal a self.true_ -> + self.combine <- (n,b) :: self.combine + | Some (If (a,_,c)) when Node.equal a self.false_ -> + self.combine <- (n,c) :: self.combine | Some s -> Log.debugf 5 (fun k->k "(@[mini-cc.update-sig@ %a@])" Signature.pp s); match Sig_tbl.find self.sig_tbl s with diff --git a/src/mini-cc/tests/tests.ml b/src/mini-cc/tests/tests.ml index 751e944b..c9307a63 100644 --- a/src/mini-cc/tests/tests.ml +++ b/src/mini-cc/tests/tests.ml @@ -20,6 +20,8 @@ module Setup() = struct let fun_a = Fun.mk_undef_const (ID.make "a") ty_i let fun_b = Fun.mk_undef_const (ID.make "b") ty_i let fun_c = Fun.mk_undef_const (ID.make "c") ty_i + let fun_d1 = Fun.mk_undef_const (ID.make "d1") ty_i + let fun_d2 = Fun.mk_undef_const (ID.make "d2") ty_i let true_ = Term.true_ tst let false_ = Term.false_ tst @@ -29,9 +31,12 @@ module Setup() = struct let not_ x = Term.not_ tst x let eq a b = Term.eq tst a b let neq a b = Term.not_ tst (eq a b) + let ite a b c = Term.ite tst a b c let a = const fun_a let b = const fun_b let c = const fun_c + let d1 = const fun_d1 + let d2 = const fun_d2 let f t1 = app_l fun_f [t1] let g t1 t2 = app_l fun_g [t1;t2] let p t1 = app_l fun_p [t1] @@ -127,5 +132,20 @@ let () = mk_test "test_not_false" @@ fun () -> A.(check bool) "is-sat" (CC.check_sat cc) true; () +let () = mk_test "test_ite" @@ fun () -> + let module S = Setup() in + let cc = CC.create S.tst in + for _i = 0 to 10 do + CC.add_lit cc S.(eq a b) true; + CC.add_lit cc S.(p (ite (eq a c) d1 d2)) true; + CC.add_lit cc S.(not_ (p d1)) true; + CC.add_lit cc S.(p d2) true; + A.(check bool) "is-sat" (CC.check_sat cc) true; + CC.add_lit cc S.(eq b c) true; (* force (p d1) *) + A.(check bool) "is-unsat" (CC.check_sat cc) false; + CC.clear cc; + done; + () + (* run alcotest *) let () = Alcotest.run "mini-cc-tests" ["mini-cc", List.rev !l]