From 80b08e03cb56cb3a21894ff1dcbe7d729f3053c7 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 31 Aug 2022 00:41:42 -0400 Subject: [PATCH] feat(const): add `opaque_to_cc` property, to control CC --- examples/sudoku/sudoku_solve.ml | 2 ++ src/base/Data_ty.ml | 2 ++ src/base/Form.ml | 2 ++ src/base/LRA_term.ml | 2 ++ src/base/Ty.ml | 2 ++ src/base/Uconst.ml | 2 ++ src/core-logic/const.ml | 1 + src/core-logic/const.mli | 1 + src/core-logic/str_const.ml | 2 ++ src/core-logic/t_builtins.ml | 2 ++ src/core-logic/types_.ml | 7 +++++++ src/core/default_cc_view.ml | 5 +++++ src/core/gensym.ml | 11 +++++++++-- src/core/gensym.mli | 2 +- src/main/pure_sat_solver.ml | 3 +++ 15 files changed, 43 insertions(+), 3 deletions(-) diff --git a/examples/sudoku/sudoku_solve.ml b/examples/sudoku/sudoku_solve.ml index 8e177a31..0638b6a1 100644 --- a/examples/sudoku/sudoku_solve.ml +++ b/examples/sudoku/sudoku_solve.ml @@ -165,6 +165,8 @@ end = struct | Cell_is a, Cell_is b -> a.x = b.x && a.y = b.y && Cell.equal a.value b.value | _ -> false + + let opaque_to_cc _ = false end : Const.DYN_OPS) module Sat = Sidekick_sat diff --git a/src/base/Data_ty.ml b/src/base/Data_ty.ml index 29a9d533..26e87dd8 100644 --- a/src/base/Data_ty.ml +++ b/src/base/Data_ty.ml @@ -103,6 +103,8 @@ let ops = | Select s -> Hash.combine2 594 (Select.hash s) | Is_a c -> Hash.combine2 595 (Cstor.hash c) | _ -> assert false + + let opaque_to_cc _ = false end : Const.DYN_OPS) let data tst d : Term.t = diff --git a/src/base/Form.ml b/src/base/Form.ml index 2bfa3788..add55281 100644 --- a/src/base/Form.ml +++ b/src/base/Form.ml @@ -36,6 +36,8 @@ let ops : Const.ops = | C_or -> Hash.int 426 | C_imply -> Hash.int 427 | _ -> assert false + + let opaque_to_cc _ = true end) (* ### view *) diff --git a/src/base/LRA_term.ml b/src/base/LRA_term.ml index 423abfc7..527fdedc 100644 --- a/src/base/LRA_term.ml +++ b/src/base/LRA_term.ml @@ -113,6 +113,8 @@ let ops : Const.ops = | Op o -> Op.hash o | Mult_by q -> Hash.(combine2 135 (Sidekick_zarith.Rational.hash q)) | _ -> assert false + + let opaque_to_cc _ = true end) let real tst = Ty.real tst diff --git a/src/base/Ty.ml b/src/base/Ty.ml index 1bd6e2d0..4a5f4dd3 100644 --- a/src/base/Ty.ml +++ b/src/base/Ty.ml @@ -34,6 +34,8 @@ let ops_ty : Const.ops = | Ty_int -> Hash.int 3 | Ty_uninterpreted u -> Hash.combine2 10 (ID.hash u.id)) | _ -> assert false + + let opaque_to_cc _ = true end) open struct diff --git a/src/base/Uconst.ml b/src/base/Uconst.ml index 4c09220e..e7d5ad34 100644 --- a/src/base/Uconst.ml +++ b/src/base/Uconst.ml @@ -26,6 +26,8 @@ let ops = let hash = function | Uconst c -> Hash.combine2 522660 (hash c) | _ -> assert false + + let opaque_to_cc _ = false end : Const.DYN_OPS) let[@inline] make uc_id uc_ty : t = { uc_id; uc_ty } diff --git a/src/core-logic/const.ml b/src/core-logic/const.ml index c7004f70..0ca300b4 100644 --- a/src/core-logic/const.ml +++ b/src/core-logic/const.ml @@ -6,6 +6,7 @@ module type DYN_OPS = sig val pp : view Fmt.printer val equal : view -> view -> bool val hash : view -> int + val opaque_to_cc : view -> bool end type ops = (module DYN_OPS) diff --git a/src/core-logic/const.mli b/src/core-logic/const.mli index 8fe1838d..69fc210d 100644 --- a/src/core-logic/const.mli +++ b/src/core-logic/const.mli @@ -10,6 +10,7 @@ module type DYN_OPS = sig val pp : view Fmt.printer val equal : view -> view -> bool val hash : view -> int + val opaque_to_cc : view -> bool end type ops = (module DYN_OPS) diff --git a/src/core-logic/str_const.ml b/src/core-logic/str_const.ml index ea92d85d..119976b0 100644 --- a/src/core-logic/str_const.ml +++ b/src/core-logic/str_const.ml @@ -16,6 +16,8 @@ let ops : Const.ops = let hash = function | Str s -> CCHash.string s | _ -> assert false + + let opaque_to_cc _ = false end) let make name ~ty : Const.t = Const.make (Str name) ops ~ty diff --git a/src/core-logic/t_builtins.ml b/src/core-logic/t_builtins.ml index fe80d7eb..86265e7a 100644 --- a/src/core-logic/t_builtins.ml +++ b/src/core-logic/t_builtins.ml @@ -33,6 +33,8 @@ let ops : const_ops = | C_true -> Fmt.string out "true" | C_false -> Fmt.string out "false" | _ -> assert false + + let opaque_to_cc _ = false end) let bool store = const store @@ Const.make C_bool ops ~ty:(type_ store) diff --git a/src/core-logic/types_.ml b/src/core-logic/types_.ml index 112e4153..6464fdce 100644 --- a/src/core-logic/types_.ml +++ b/src/core-logic/types_.ml @@ -4,8 +4,15 @@ type const_view = .. module type DYN_CONST_OPS = sig val pp : const_view Fmt.printer + (** Pretty-print constant *) val equal : const_view -> const_view -> bool + (** Equality of constant with any other constant *) val hash : const_view -> int + (** Hash constant *) + val opaque_to_cc : const_view -> bool + (** If true, congruence closure will not apply for applications of this + constant. In other words, [c t1…tn] will appear to the congruence + closure as a single opaque term with no subterms. *) end type const_ops = (module DYN_CONST_OPS) diff --git a/src/core/default_cc_view.ml b/src/core/default_cc_view.ml index 4718ff5a..0e10b00e 100644 --- a/src/core/default_cc_view.ml +++ b/src/core/default_cc_view.ml @@ -9,9 +9,14 @@ let view_as_cc (t : Term.t) : _ CC_view.t = | Term.E_const { Const.c_view = T_builtins.C_ite; _ }, [ _ty; a; b; c ] -> View.If (a, b, c) | Term.E_const { Const.c_view = T_builtins.C_not; _ }, [ a ] -> View.Not a + | Term.E_const { Const.c_ops = (module OP); c_view; _ }, _ + when OP.opaque_to_cc c_view -> + (* this constant hides its arguments *) + View.Opaque t | _ -> (match Term.view t with | Term.E_app (f, a) -> View.App_ho (f, a) | Term.E_const { Const.c_view = T_builtins.C_true; _ } -> View.Bool true | Term.E_const { Const.c_view = T_builtins.C_false; _ } -> View.Bool false + | Term.E_app_fold _ -> View.Opaque t | _ -> View.Opaque t) diff --git a/src/core/gensym.ml b/src/core/gensym.ml index f4b8abd1..09bc2f6e 100644 --- a/src/core/gensym.ml +++ b/src/core/gensym.ml @@ -9,6 +9,7 @@ type Const.view += gensym_id: int; (** Id of the gensym *) pre: string; (** Printing prefix *) ty: ty; + opaque_to_cc: bool; } let ops = @@ -26,6 +27,10 @@ let ops = let pp out = function | Fresh { id; pre; _ } -> Fmt.fprintf out "$%s[%d]" pre id | _ -> assert false + + let opaque_to_cc = function + | Fresh f -> f.opaque_to_cc + | _ -> assert false end : Const.DYN_OPS) type t = { tst: Term.store; self_id: int; mutable fresh: int } @@ -38,11 +43,13 @@ let create tst : t = incr id_; { tst; self_id; fresh = 0 } -let fresh_term (self : t) ~pre (ty : ty) : Term.t = +let fresh_term ?(opaque_to_cc = false) (self : t) ~pre (ty : ty) : Term.t = let id = self.fresh in self.fresh <- 1 + self.fresh; let c = Term.const self.tst - @@ Const.make (Fresh { id; gensym_id = self.self_id; pre; ty }) ops ~ty + @@ Const.make + (Fresh { id; gensym_id = self.self_id; pre; ty; opaque_to_cc }) + ops ~ty in c diff --git a/src/core/gensym.mli b/src/core/gensym.mli index 05a42b20..00fcd5a8 100644 --- a/src/core/gensym.mli +++ b/src/core/gensym.mli @@ -15,5 +15,5 @@ type t val create : Term.store -> t (** New (stateful) generator instance. *) -val fresh_term : t -> pre:string -> ty -> term +val fresh_term : ?opaque_to_cc:bool -> t -> pre:string -> ty -> term (** Make a fresh term of the given type *) diff --git a/src/main/pure_sat_solver.ml b/src/main/pure_sat_solver.ml index 7e183a25..5c3f3895 100644 --- a/src/main/pure_sat_solver.ml +++ b/src/main/pure_sat_solver.ml @@ -177,6 +177,9 @@ end = struct let pp out = function | I i -> Fmt.int out i | _ -> assert false + + (* irrelevant *) + let opaque_to_cc _ = true end : Const.DYN_OPS) let make tst i : Lit.t =