mirror of
https://github.com/c-cube/sidekick.git
synced 2026-01-23 01:46:43 -05:00
refactor: functorize(th-bool)
This commit is contained in:
Simon Cruanes
parent
c36092d217
commit
28126eaebd
7 changed files with 123 additions and 316 deletions
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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))
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue