From 28126eaebde7ce5cd9032f237376135042591edd Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 27 May 2019 17:03:05 -0500 Subject: [PATCH] refactor: functorize(th-bool) --- src/th-bool/Bool_intf.ml | 24 ------ src/th-bool/Bool_term.ml | 135 ------------------------------- src/th-bool/Bool_term.mli | 21 ----- src/th-bool/Sidekick_th_bool.ml | 137 ++++++++++++++++++++++++++++---- src/th-bool/Th_dyn_tseitin.ml | 104 ------------------------ src/th-bool/Th_dyn_tseitin.mli | 16 ---- src/th-bool/dune | 2 +- 7 files changed, 123 insertions(+), 316 deletions(-) delete mode 100644 src/th-bool/Bool_intf.ml delete mode 100644 src/th-bool/Bool_term.ml delete mode 100644 src/th-bool/Bool_term.mli delete mode 100644 src/th-bool/Th_dyn_tseitin.ml delete mode 100644 src/th-bool/Th_dyn_tseitin.mli diff --git a/src/th-bool/Bool_intf.ml b/src/th-bool/Bool_intf.ml deleted file mode 100644 index 7bef0b7a..00000000 --- a/src/th-bool/Bool_intf.ml +++ /dev/null @@ -1,24 +0,0 @@ - -(** {1 Signatures for booleans} *) - -type 'a view = - | B_not of 'a - | B_and of 'a IArray.t - | B_or of 'a IArray.t - | B_imply of 'a IArray.t * 'a - | B_atom of 'a - -(** {2 Interface for a representation of boolean terms} *) -module type BOOL_TERM = sig - type t - type state - - val equal : t -> t -> bool - val hash : t -> int - - val view_as_bool : t -> t view - (** View a term as a boolean formula *) - - val make : state -> t view -> t - (** Build a boolean term from a formula view *) -end diff --git a/src/th-bool/Bool_term.ml b/src/th-bool/Bool_term.ml deleted file mode 100644 index 22dd0c99..00000000 --- a/src/th-bool/Bool_term.ml +++ /dev/null @@ -1,135 +0,0 @@ - -module ID = Sidekick_smt.ID -module T = Sidekick_smt.Term -module Ty = Sidekick_smt.Ty -open Sidekick_smt.Solver_types - -open Bool_intf - -type term = T.t -type t = T.t -type state = T.state - -type 'a view = 'a Bool_intf.view - -exception Not_a_th_term - -let id_and = ID.make "and" -let id_or = ID.make "or" -let id_imply = ID.make "=>" - -let equal = T.equal -let hash = T.hash - -let view_id cst_id args = - if ID.equal cst_id id_and then ( - B_and args - ) else if ID.equal cst_id id_or then ( - B_or args - ) else if ID.equal cst_id id_imply && IArray.length args >= 2 then ( - (* conclusion is stored first *) - let len = IArray.length args in - B_imply (IArray.sub args 1 (len-1), IArray.get args 0) - ) else ( - raise_notrace Not_a_th_term - ) - -let view_as_bool (t:T.t) : T.t view = - match T.view t with - | Not u -> B_not u - | App_cst ({cst_id; _}, args) -> - (try view_id cst_id args with Not_a_th_term -> B_atom t) - | _ -> B_atom t - -module C = struct - - let get_ty _ _ = Ty.prop - - let abs ~self _a = - match T.view self with - | Not u -> u, false - | _ -> self, true - - let eval id args = - let module Value = Sidekick_smt.Value in - match view_id id args with - | B_not (V_bool b) -> Value.bool (not b) - | B_and a when IArray.for_all Value.is_true a -> Value.true_ - | B_and a when IArray.exists Value.is_false a -> Value.false_ - | B_or a when IArray.exists Value.is_true a -> Value.true_ - | B_or a when IArray.for_all Value.is_false a -> Value.false_ - | B_imply (_, V_bool true) -> Value.true_ - | B_imply (a,_) when IArray.exists Value.is_false a -> Value.true_ - | B_imply (a,b) when IArray.for_all Value.is_bool a && Value.is_bool b -> Value.false_ - | B_atom v -> v - | B_not _ | B_and _ | B_or _ | B_imply _ - -> Error.errorf "non boolean value in boolean connective" - - (* no congruence closure for boolean terms *) - let relevant _id _ _ = false - - let mk_cst ?(do_cc=false) id : cst = - {cst_id=id; - cst_view=Cst_def { - pp=None; abs; ty=get_ty; relevant; do_cc; eval=eval id; }; } - - let not = T.not_ - let and_ = mk_cst id_and - let or_ = mk_cst id_or - let imply = mk_cst id_imply -end - -let as_id id (t:T.t) : T.t IArray.t option = - match T.view t with - | App_cst ({cst_id; _}, args) when ID.equal id cst_id -> Some args - | _ -> None - -(* flatten terms of the given ID *) -let flatten_id op sign (l:T.t list) : T.t list = - CCList.flat_map - (fun t -> match as_id op t with - | Some args -> IArray.to_list args - | None when (sign && T.is_true t) || (not sign && T.is_false t) -> - [] (* idempotent *) - | None -> [t]) - l - -let and_l st l = - match flatten_id id_and true l with - | [] -> T.true_ st - | l when List.exists T.is_false l -> T.false_ st - | [x] -> x - | args -> T.app_cst st C.and_ (IArray.of_list args) - -let or_l st l = - match flatten_id id_or false l with - | [] -> T.false_ st - | l when List.exists T.is_true l -> T.true_ st - | [x] -> x - | args -> T.app_cst st C.or_ (IArray.of_list args) - -let and_ st a b = and_l st [a;b] -let or_ st a b = or_l st [a;b] -let and_a st a = and_l st (IArray.to_list a) -let or_a st a = or_l st (IArray.to_list a) -let eq = T.eq -let not_ = T.not_ - -let neq st a b = not_ st @@ eq st a b - -let imply_a st xs y = - if IArray.is_empty xs then y - else T.app_cst st C.imply (IArray.append (IArray.singleton y) xs) - -let imply_l st xs y = match xs with - | [] -> y - | _ -> T.app_cst st C.imply (IArray.of_list @@ y :: xs) - -let imply st a b = imply_a st (IArray.singleton a) b - -let make st = function - | B_atom t -> t - | B_and l -> and_a st l - | B_or l -> or_a st l - | B_imply (a,b) -> imply_a st a b - | B_not t -> not_ st t diff --git a/src/th-bool/Bool_term.mli b/src/th-bool/Bool_term.mli deleted file mode 100644 index 31eceb83..00000000 --- a/src/th-bool/Bool_term.mli +++ /dev/null @@ -1,21 +0,0 @@ - -type 'a view = 'a Bool_intf.view - -type term = Sidekick_smt.Term.t - -include Bool_intf.BOOL_TERM - with type t = term - and type state = Sidekick_smt.Term.state - -val and_ : state -> term -> term -> term -val or_ : state -> term -> term -> term -val not_ : state -> term -> term -val imply : state -> term -> term -> term -val imply_a : state -> term IArray.t -> term -> term -val imply_l : state -> term list -> term -> term -val eq : state -> term -> term -> term -val neq : state -> term -> term -> term -val and_a : state -> term IArray.t -> term -val and_l : state -> term list -> term -val or_a : state -> term IArray.t -> term -val or_l : state -> term list -> term diff --git a/src/th-bool/Sidekick_th_bool.ml b/src/th-bool/Sidekick_th_bool.ml index f2607f47..4e5bfb70 100644 --- a/src/th-bool/Sidekick_th_bool.ml +++ b/src/th-bool/Sidekick_th_bool.ml @@ -1,22 +1,129 @@ (** {1 Theory of Booleans} *) -type term = Sidekick_smt.Term.t +(** {2 Signatures for booleans} *) +module View = struct + type 'a t = + | B_not of 'a + | B_and of 'a IArray.t + | B_or of 'a IArray.t + | B_imply of 'a IArray.t * 'a + | B_atom of 'a +end -module Intf = Bool_intf -module Bool_term = Bool_term -module Th_dyn_tseitin = Th_dyn_tseitin +module type ARG = sig + module S : Sidekick_core.SOLVER -type 'a view = 'a Intf.view = - | B_not of 'a - | B_and of 'a IArray.t - | B_or of 'a IArray.t - | B_imply of 'a IArray.t * 'a - | B_atom of 'a + type term = S.A.Term.t -module type BOOL_TERM = Intf.BOOL_TERM + val view_as_bool : term -> term View.t + val mk_bool : S.A.Term.state -> term View.t -> term +end -(** Dynamic Tseitin transformation *) -let th_dynamic_tseitin = - let module Th = Th_dyn_tseitin.Make(Bool_term) in - Th.th +module type S = sig + module A : ARG + val theory : A.S.theory +end + +(** Theory with dynamic reduction to clauses *) +module Make_dyn_tseitin(A : ARG) +(* : S with module A = A *) += struct + (* TODO (long term): relevancy propagation *) + + (* TODO: Tseitin on the fly when a composite boolean term is asserted. + --> maybe, cache the clause inside the literal *) + + module A = A + module Solver = A.S.Internal + module T = Solver.A.Term + module Lit = Solver.A.Lit + + type term = T.t + + module T_tbl = CCHashtbl.Make(T) + + type t = { + expanded: unit T_tbl.t; (* set of literals already expanded *) + } + + let tseitin ~final (self:t) (solver:Solver.t) (lit:Lit.t) (lit_t:term) (v:term View.t) : unit = + Log.debugf 5 (fun k->k "(@[th_bool.tseitin@ %a@])" Lit.pp lit); + let expanded () = T_tbl.mem self.expanded lit_t in + let add_axiom c = + T_tbl.replace self.expanded lit_t (); + Solver.add_persistent_axiom solver c + in + match v with + | B_not _ -> assert false (* normalized *) + | B_atom _ -> () (* CC will manage *) + | B_and subs -> + if Lit.sign lit then ( + (* propagate [lit => subs_i] *) + IArray.iter + (fun sub -> + let sublit = Solver.mk_lit solver sub in + Solver.propagate_l solver sublit [lit]) + subs + ) else if final && not @@ expanded () then ( + (* axiom [¬lit => ∨_i ¬ subs_i] *) + let subs = IArray.to_list subs in + let c = Lit.neg lit :: List.map (Solver.mk_lit solver ~sign:false) subs in + add_axiom c + ) + | B_or subs -> + if not @@ Lit.sign lit then ( + (* propagate [¬lit => ¬subs_i] *) + IArray.iter + (fun sub -> + let sublit = Solver.mk_lit solver ~sign:false sub in + Solver.add_local_axiom solver [Lit.neg lit; sublit]) + subs + ) else if final && not @@ expanded () then ( + (* axiom [lit => ∨_i subs_i] *) + let subs = IArray.to_list subs in + let c = Lit.neg lit :: List.map (Solver.mk_lit solver ~sign:true) subs in + add_axiom c + ) + | B_imply (guard,concl) -> + if Lit.sign lit && final && not @@ expanded () then ( + (* axiom [lit => ∨_i ¬guard_i ∨ concl] *) + let guard = IArray.to_list guard in + let c = + Solver.mk_lit solver concl :: Lit.neg lit :: + List.map (Solver.mk_lit solver ~sign:false) guard in + add_axiom c + ) else if not @@ Lit.sign lit then ( + (* propagate [¬lit => ¬concl] *) + Solver.propagate_l solver (Solver.mk_lit solver ~sign:false concl) [lit]; + (* propagate [¬lit => ∧_i guard_i] *) + IArray.iter + (fun sub -> + let sublit = Solver.mk_lit solver ~sign:true sub in + Solver.propagate_l solver sublit [lit]) + guard + ) + + let check_ ~final self solver lits = + lits + (fun lit -> + let t = Lit.term lit in + match A.view_as_bool t with + | B_atom _ -> () + | v -> tseitin ~final self solver lit t v) + + let partial_check (self:t) acts (lits:Lit.t Iter.t) = + check_ ~final:false self acts lits + + let final_check (self:t) acts (lits:Lit.t Iter.t) = + check_ ~final:true self acts lits + + let create_and_setup (solver:Solver.t) : t = + let self = {expanded=T_tbl.create 24} in + Solver.on_final_check solver (final_check self); + Solver.on_partial_check solver (partial_check self); + self + + let theory = + A.S.mk_theory ~name:"boolean" ~create_and_setup () +end diff --git a/src/th-bool/Th_dyn_tseitin.ml b/src/th-bool/Th_dyn_tseitin.ml deleted file mode 100644 index a86fe8a2..00000000 --- a/src/th-bool/Th_dyn_tseitin.ml +++ /dev/null @@ -1,104 +0,0 @@ - -(* TODO (long term): relevancy propagation *) - -(* TODO: Tseitin on the fly when a composite boolean term is asserted. - --> maybe, cache the clause inside the literal *) - -module Theory = Sidekick_smt.Theory -open Bool_intf - -module type ARG = Bool_intf.BOOL_TERM - with type t = Sidekick_smt.Term.t - and type state = Sidekick_smt.Term.state - -module Make(Term : ARG) = struct - type term = Term.t - - module T_tbl = CCHashtbl.Make(Term) - module Lit = Sidekick_smt.Lit - - type t = { - tst: Term.state; - expanded: unit T_tbl.t; (* set of literals already expanded *) - } - - let tseitin ~final (self:t) (acts:Theory.actions) (lit:Lit.t) (lit_t:term) (v:term view) : unit = - let (module A) = acts in - Log.debugf 5 (fun k->k "(@[th_bool.tseitin@ %a@])" Lit.pp lit); - let expanded () = T_tbl.mem self.expanded lit_t in - let add_axiom c = - T_tbl.replace self.expanded lit_t (); - A.add_persistent_axiom c - in - match v with - | B_not _ -> assert false (* normalized *) - | B_atom _ -> () (* CC will manage *) - | B_and subs -> - if Lit.sign lit then ( - (* propagate [lit => subs_i] *) - IArray.iter - (fun sub -> - let sublit = Lit.atom self.tst sub in - A.propagate_l sublit [lit]) - subs - ) else if final && not @@ expanded () then ( - (* axiom [¬lit => ∨_i ¬ subs_i] *) - let subs = IArray.to_list subs in - let c = Lit.neg lit :: List.map (Lit.atom self.tst ~sign:false) subs in - add_axiom c - ) - | B_or subs -> - if not @@ Lit.sign lit then ( - (* propagate [¬lit => ¬subs_i] *) - IArray.iter - (fun sub -> - let sublit = Lit.atom self.tst ~sign:false sub in - A.add_local_axiom [Lit.neg lit; sublit]) - subs - ) else if final && not @@ expanded () then ( - (* axiom [lit => ∨_i subs_i] *) - let subs = IArray.to_list subs in - let c = Lit.neg lit :: List.map (Lit.atom self.tst ~sign:true) subs in - add_axiom c - ) - | B_imply (guard,concl) -> - if Lit.sign lit && final && not @@ expanded () then ( - (* axiom [lit => ∨_i ¬guard_i ∨ concl] *) - let guard = IArray.to_list guard in - let c = Lit.atom self.tst concl :: Lit.neg lit :: List.map (Lit.atom self.tst ~sign:false) guard in - add_axiom c - ) else if not @@ Lit.sign lit then ( - (* propagate [¬lit => ¬concl] *) - A.propagate_l (Lit.atom self.tst ~sign:false concl) [lit]; - (* propagate [¬lit => ∧_i guard_i] *) - IArray.iter - (fun sub -> - let sublit = Lit.atom self.tst ~sign:true sub in - A.propagate_l sublit [lit]) - guard - ) - - let check_ ~final self acts lits = - lits - (fun lit -> - let t = Lit.term lit in - match Term.view_as_bool t with - | B_atom _ -> () - | v -> tseitin ~final self acts lit t v) - - let partial_check (self:t) acts (lits:Lit.t Iter.t) = - check_ ~final:false self acts lits - - let final_check (self:t) acts (lits:Lit.t Iter.t) = - check_ ~final:true self acts lits - - let th = - Theory.make - ~partial_check - ~final_check - ~name:"boolean" - ~create:(fun tst -> {tst; expanded=T_tbl.create 24}) - ?mk_model:None (* entirely interpreted *) - () - -end diff --git a/src/th-bool/Th_dyn_tseitin.mli b/src/th-bool/Th_dyn_tseitin.mli deleted file mode 100644 index be131f8c..00000000 --- a/src/th-bool/Th_dyn_tseitin.mli +++ /dev/null @@ -1,16 +0,0 @@ - -(** {1 Dynamic Tseitin conversion} - - This theory performs the conversion of boolean terms into clauses, on - the fly, during the proof search. It is a true CDCL(T)-style theory. - *) - -module type ARG = Bool_intf.BOOL_TERM - with type t = Sidekick_smt.Term.t - and type state = Sidekick_smt.Term.state - -module Make(Term : ARG) : sig - type term = Term.t - - val th : Sidekick_smt.Theory.t -end diff --git a/src/th-bool/dune b/src/th-bool/dune index 8d8b3005..8ac7acad 100644 --- a/src/th-bool/dune +++ b/src/th-bool/dune @@ -1,6 +1,6 @@ (library (name Sidekick_th_bool) - (public_name sidekick.smt.th-bool) + (public_name sidekick.th-bool) (libraries containers sidekick.core sidekick.util) (flags :standard -open Sidekick_util))