mirror of
https://github.com/c-cube/sidekick.git
synced 2026-01-23 18:06:41 -05:00
refactor(bool): bool-view of terms, functorized theory
This commit is contained in:
Simon Cruanes
parent
1f68753121
commit
e878907f4b
9 changed files with 384 additions and 286 deletions
|
|
@ -114,9 +114,10 @@ let main () =
|
|||
let solver =
|
||||
let theories = match syn with
|
||||
| Dimacs ->
|
||||
[Sidekick_th_bool.th]
|
||||
(* TODO: eager CNF conversion *)
|
||||
[Sidekick_th_bool.th_dynamic_tseitin]
|
||||
| Smtlib ->
|
||||
[Sidekick_th_bool.th] (* TODO: more theories *)
|
||||
[Sidekick_th_bool.th_dynamic_tseitin] (* TODO: more theories *)
|
||||
in
|
||||
Sidekick_smt.Solver.create ~store_proof:!check ~theories ()
|
||||
in
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ type 'a or_error = ('a, string) CCResult.t
|
|||
|
||||
module E = CCResult
|
||||
module A = Ast
|
||||
module Form = Sidekick_th_bool
|
||||
module Form = Sidekick_th_bool.Bool_term
|
||||
module Fmt = CCFormat
|
||||
module Dot = Msat_backend.Dot.Make(Solver.Sat_solver)(Msat_backend.Dot.Default(Solver.Sat_solver))
|
||||
|
||||
|
|
@ -125,7 +125,7 @@ module Conv = struct
|
|||
begin match List.rev l with
|
||||
| [] -> Term.true_ tst
|
||||
| ret :: hyps ->
|
||||
Form.imply tst hyps ret
|
||||
Form.imply_l tst hyps ret
|
||||
end
|
||||
| A.Op (A.Eq, l) ->
|
||||
let l = List.map (aux subst) l in
|
||||
|
|
@ -137,7 +137,7 @@ module Conv = struct
|
|||
in
|
||||
Form.and_l tst (curry_eq l)
|
||||
| A.Op (A.Distinct, l) ->
|
||||
Form.distinct tst @@ List.map (aux subst) l
|
||||
Form.distinct_l tst @@ List.map (aux subst) l
|
||||
| A.Not f -> Form.not_ tst (aux subst f)
|
||||
| A.Bool true -> Term.true_ tst
|
||||
| A.Bool false -> Term.false_ tst
|
||||
|
|
|
|||
26
src/th-bool/Bool_intf.ml
Normal file
26
src/th-bool/Bool_intf.ml
Normal file
|
|
@ -0,0 +1,26 @@
|
|||
|
||||
(** {1 Signatures for booleans} *)
|
||||
|
||||
type 'a view =
|
||||
| B_not of 'a
|
||||
| B_eq of 'a * 'a
|
||||
| B_and of 'a IArray.t
|
||||
| B_or of 'a IArray.t
|
||||
| B_imply of 'a IArray.t * 'a
|
||||
| B_distinct of 'a IArray.t
|
||||
| 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
|
||||
171
src/th-bool/Bool_term.ml
Normal file
171
src/th-bool/Bool_term.ml
Normal file
|
|
@ -0,0 +1,171 @@
|
|||
|
||||
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_not = ID.make "not"
|
||||
let id_and = ID.make "and"
|
||||
let id_or = ID.make "or"
|
||||
let id_imply = ID.make "=>"
|
||||
let id_distinct = ID.make "distinct"
|
||||
|
||||
let equal = T.equal
|
||||
let hash = T.hash
|
||||
|
||||
let view_id cst_id args =
|
||||
if ID.equal cst_id id_not && IArray.length args=1 then (
|
||||
B_not (IArray.get args 0)
|
||||
) else 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 if ID.equal cst_id id_distinct then (
|
||||
B_distinct args
|
||||
) else (
|
||||
raise_notrace Not_a_th_term
|
||||
)
|
||||
|
||||
let view_as_bool (t:T.t) : T.t view =
|
||||
match T.view t with
|
||||
| Eq (a,b) -> B_eq (a,b)
|
||||
| App_cst ({cst_id; _}, args) ->
|
||||
begin try view_id cst_id args with Not_a_th_term -> B_atom t end
|
||||
| _ -> B_atom t
|
||||
|
||||
module C = struct
|
||||
|
||||
let get_ty _ _ = Ty.prop
|
||||
|
||||
let abs ~self _a =
|
||||
match T.view self with
|
||||
| App_cst ({cst_id;_}, args) when ID.equal cst_id id_not && IArray.length args=1 ->
|
||||
(* [not a] --> [a, false] *)
|
||||
IArray.get args 0, 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_eq (a,b) -> Value.bool @@ Value.equal a b
|
||||
| B_atom v -> v
|
||||
| B_distinct a ->
|
||||
if
|
||||
Sequence.diagonal (IArray.to_seq a)
|
||||
|> Sequence.for_all (fun (x,y) -> not @@ Value.equal x y)
|
||||
then Value.true_
|
||||
else Value.false_
|
||||
| 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; is_value=false; do_cc; eval=eval id; }; }
|
||||
|
||||
let not = mk_cst id_not
|
||||
let and_ = mk_cst id_and
|
||||
let or_ = mk_cst id_or
|
||||
let imply = mk_cst id_imply
|
||||
let distinct = mk_cst id_distinct
|
||||
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_ st a =
|
||||
match as_id id_not a, T.view a with
|
||||
| _, Bool false -> T.true_ st
|
||||
| _, Bool true -> T.false_ st
|
||||
| Some args, _ ->
|
||||
assert (IArray.length args = 1);
|
||||
IArray.get args 0
|
||||
| None, _ -> T.app_cst st C.not (IArray.singleton a)
|
||||
|
||||
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 distinct st a =
|
||||
if IArray.length a <= 1
|
||||
then T.true_ st
|
||||
else T.app_cst st C.distinct a
|
||||
|
||||
let distinct_l st = function
|
||||
| [] | [_] -> T.true_ st
|
||||
| xs -> distinct st (IArray.of_list xs)
|
||||
|
||||
let make st = function
|
||||
| B_atom t -> t
|
||||
| B_eq (a,b) -> T.eq st a b
|
||||
| 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
|
||||
| B_distinct l -> distinct st l
|
||||
23
src/th-bool/Bool_term.mli
Normal file
23
src/th-bool/Bool_term.mli
Normal file
|
|
@ -0,0 +1,23 @@
|
|||
|
||||
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 distinct : state -> term IArray.t -> term
|
||||
val distinct_l : state -> term list -> 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,23 +1,13 @@
|
|||
|
||||
(** {1 Theory of Booleans} *)
|
||||
|
||||
open Sidekick_smt
|
||||
open Solver_types
|
||||
type term = Sidekick_smt.Term.t
|
||||
|
||||
type term = Term.t
|
||||
module Intf = Bool_intf
|
||||
module Bool_term = Bool_term
|
||||
module Th_dyn_tseitin = Th_dyn_tseitin
|
||||
|
||||
(* TODO (long term): relevancy propagation *)
|
||||
|
||||
(* TODO: Tseitin on the fly when a composite boolean term is asserted.
|
||||
--> maybe, cache the clause inside the literal *)
|
||||
|
||||
let id_not = ID.make "not"
|
||||
let id_and = ID.make "and"
|
||||
let id_or = ID.make "or"
|
||||
let id_imply = ID.make "=>"
|
||||
let id_distinct = ID.make "distinct"
|
||||
|
||||
type 'a view =
|
||||
type 'a view = 'a Intf.view =
|
||||
| B_not of 'a
|
||||
| B_eq of 'a * 'a
|
||||
| B_and of 'a IArray.t
|
||||
|
|
@ -26,235 +16,9 @@ type 'a view =
|
|||
| B_distinct of 'a IArray.t
|
||||
| B_atom of 'a
|
||||
|
||||
exception Not_a_th_term
|
||||
module type BOOL_TERM = Intf.BOOL_TERM
|
||||
|
||||
let view_id cst_id args =
|
||||
if ID.equal cst_id id_not && IArray.length args=1 then (
|
||||
B_not (IArray.get args 0)
|
||||
) else 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 if ID.equal cst_id id_distinct then (
|
||||
B_distinct args
|
||||
) else (
|
||||
raise_notrace Not_a_th_term
|
||||
)
|
||||
|
||||
let view (t:Term.t) : term view =
|
||||
match Term.view t with
|
||||
| Eq (a,b) -> B_eq (a,b)
|
||||
| App_cst ({cst_id; _}, args) ->
|
||||
begin try view_id cst_id args with Not_a_th_term -> B_atom t end
|
||||
| _ -> B_atom t
|
||||
|
||||
|
||||
module C = struct
|
||||
|
||||
let get_ty _ _ = Ty.prop
|
||||
|
||||
let abs ~self _a =
|
||||
match Term.view self with
|
||||
| App_cst ({cst_id;_}, args) when ID.equal cst_id id_not && IArray.length args=1 ->
|
||||
(* [not a] --> [a, false] *)
|
||||
IArray.get args 0, false
|
||||
| _ -> self, true
|
||||
|
||||
let eval id args = 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_eq (a,b) -> Value.bool @@ Value.equal a b
|
||||
| B_atom v -> v
|
||||
| B_distinct a ->
|
||||
if
|
||||
Sequence.diagonal (IArray.to_seq a)
|
||||
|> Sequence.for_all (fun (x,y) -> not @@ Value.equal x y)
|
||||
then Value.true_
|
||||
else Value.false_
|
||||
| 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.t =
|
||||
{cst_id=id;
|
||||
cst_view=Cst_def {
|
||||
pp=None; abs; ty=get_ty; relevant; is_value=false; do_cc; eval=eval id; }; }
|
||||
|
||||
let not = mk_cst id_not
|
||||
let and_ = mk_cst id_and
|
||||
let or_ = mk_cst id_or
|
||||
let imply = mk_cst id_imply
|
||||
let distinct = mk_cst id_distinct
|
||||
end
|
||||
|
||||
let as_id id (t:Term.t) : Term.t IArray.t option =
|
||||
match Term.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:Term.t list) : Term.t list =
|
||||
CCList.flat_map
|
||||
(fun t -> match as_id op t with
|
||||
| Some args -> IArray.to_list args
|
||||
| None when (sign && Term.is_true t) || (not sign && Term.is_false t) ->
|
||||
[] (* idempotent *)
|
||||
| None -> [t])
|
||||
l
|
||||
|
||||
let and_l st l =
|
||||
match flatten_id id_and true l with
|
||||
| [] -> Term.true_ st
|
||||
| l when List.exists Term.is_false l -> Term.false_ st
|
||||
| [x] -> x
|
||||
| args -> Term.app_cst st C.and_ (IArray.of_list args)
|
||||
|
||||
let or_l st l =
|
||||
match flatten_id id_or false l with
|
||||
| [] -> Term.false_ st
|
||||
| l when List.exists Term.is_true l -> Term.true_ st
|
||||
| [x] -> x
|
||||
| args -> Term.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 eq = Term.eq
|
||||
|
||||
let not_ st a =
|
||||
match as_id id_not a, Term.view a with
|
||||
| _, Bool false -> Term.true_ st
|
||||
| _, Bool true -> Term.false_ st
|
||||
| Some args, _ ->
|
||||
assert (IArray.length args = 1);
|
||||
IArray.get args 0
|
||||
| None, _ -> Term.app_cst st C.not (IArray.singleton a)
|
||||
|
||||
let neq st a b = not_ st @@ eq st a b
|
||||
|
||||
let imply st xs y = match xs with
|
||||
| [] -> y
|
||||
| _ -> Term.app_cst st C.imply (IArray.of_list @@ y :: xs)
|
||||
|
||||
let distinct st = function
|
||||
| [] | [_] -> Term.true_ st
|
||||
| xs -> Term.app_cst st C.distinct (IArray.of_list xs)
|
||||
|
||||
module Lit = struct
|
||||
include Lit
|
||||
let eq tst a b = Lit.atom ~sign:true (eq tst a b)
|
||||
let neq tst a b = neg @@ eq tst a b
|
||||
end
|
||||
|
||||
type t = {
|
||||
tst: Term.state;
|
||||
expanded: unit Term.Tbl.t; (* set of literals already expanded *)
|
||||
}
|
||||
|
||||
let pp_c out c = Fmt.fprintf out "(@[<hv>%a@])" (Util.pp_list Lit.pp) c
|
||||
|
||||
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 () = Term.Tbl.mem self.expanded lit_t in
|
||||
let add_axiom c =
|
||||
Term.Tbl.replace self.expanded lit_t ();
|
||||
A.add_persistent_axiom c
|
||||
in
|
||||
match v with
|
||||
| B_not _ -> assert false (* normalized *)
|
||||
| B_atom _ | B_eq _ -> () (* CC will manage *)
|
||||
| B_distinct l ->
|
||||
let l = IArray.to_list l in
|
||||
if Lit.sign lit then (
|
||||
A.propagate_distinct l ~neq:lit_t lit
|
||||
) else if final && not @@ expanded () then (
|
||||
(* add clause [distinct t1…tn ∨ ∨_{i,j>i} t_i=j] *)
|
||||
let c =
|
||||
Sequence.diagonal_l l
|
||||
|> Sequence.map (fun (t,u) -> Lit.eq self.tst t u)
|
||||
|> Sequence.to_rev_list
|
||||
in
|
||||
let c = Lit.neg lit :: c in
|
||||
Log.debugf 5 (fun k->k "(@[tseitin.distinct.case-split@ %a@])" pp_c c);
|
||||
add_axiom c
|
||||
)
|
||||
| B_and subs ->
|
||||
if Lit.sign lit then (
|
||||
(* propagate [lit => subs_i] *)
|
||||
IArray.iter
|
||||
(fun sub ->
|
||||
let sublit = Lit.atom sub in
|
||||
A.propagate 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 ~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 ~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 ~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 concl :: Lit.neg lit :: List.map (Lit.atom ~sign:false) guard in
|
||||
add_axiom c
|
||||
) else if not @@ Lit.sign lit then (
|
||||
(* propagate [¬lit => ¬concl] *)
|
||||
A.propagate (Lit.atom ~sign:false concl) [lit];
|
||||
(* propagate [¬lit => ∧_i guard_i] *)
|
||||
IArray.iter
|
||||
(fun sub ->
|
||||
let sublit = Lit.atom ~sign:true sub in
|
||||
A.propagate sublit [lit])
|
||||
guard
|
||||
)
|
||||
|
||||
let check_ ~final self acts lits =
|
||||
lits
|
||||
(fun lit ->
|
||||
let t = Lit.term lit in
|
||||
match view t with
|
||||
| B_atom _ | B_eq _ -> ()
|
||||
| v -> tseitin ~final self acts lit t v)
|
||||
|
||||
let partial_check (self:t) acts (lits:Lit.t Sequence.t) =
|
||||
check_ ~final:false self acts lits
|
||||
|
||||
let final_check (self:t) acts (lits:Lit.t Sequence.t) =
|
||||
check_ ~final:true self acts lits
|
||||
|
||||
let th =
|
||||
Theory.make
|
||||
~partial_check
|
||||
~final_check
|
||||
~name:"boolean"
|
||||
~create:(fun tst -> {tst; expanded=Term.Tbl.create 24})
|
||||
?mk_model:None (* entirely interpreted *)
|
||||
()
|
||||
(** Dynamic Tseitin transformation *)
|
||||
let th_dynamic_tseitin =
|
||||
let module Th = Th_dyn_tseitin.Make(Bool_term) in
|
||||
Th.th
|
||||
|
|
|
|||
|
|
@ -1,35 +0,0 @@
|
|||
|
||||
(** {1 Theory of Booleans} *)
|
||||
|
||||
open Sidekick_smt
|
||||
|
||||
type term = Term.t
|
||||
|
||||
type 'a view = private
|
||||
| B_not of 'a
|
||||
| B_eq of 'a * 'a
|
||||
| B_and of 'a IArray.t
|
||||
| B_or of 'a IArray.t
|
||||
| B_imply of 'a IArray.t * 'a
|
||||
| B_distinct of 'a IArray.t
|
||||
| B_atom of 'a
|
||||
|
||||
val view : term -> term view
|
||||
|
||||
val and_ : Term.state -> term -> term -> term
|
||||
val or_ : Term.state -> term -> term -> term
|
||||
val not_ : Term.state -> term -> term
|
||||
val imply : Term.state -> term list -> term -> term
|
||||
val eq : Term.state -> term -> term -> term
|
||||
val neq : Term.state -> term -> term -> term
|
||||
val distinct : Term.state -> term list -> term
|
||||
val and_l : Term.state -> term list -> term
|
||||
val or_l : Term.state -> term list -> term
|
||||
|
||||
module Lit : sig
|
||||
type t = Lit.t
|
||||
val eq : Term.state -> term -> term -> t
|
||||
val neq : Term.state -> term -> term -> t
|
||||
end
|
||||
|
||||
val th : Sidekick_smt.Theory.t
|
||||
126
src/th-bool/Th_dyn_tseitin.ml
Normal file
126
src/th-bool/Th_dyn_tseitin.ml
Normal file
|
|
@ -0,0 +1,126 @@
|
|||
|
||||
(* 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 = struct
|
||||
include Sidekick_smt.Lit
|
||||
let eq tst a b = atom ~sign:true (Term.make tst (B_eq (a,b)))
|
||||
let neq tst a b = neg @@ eq tst a b
|
||||
end
|
||||
|
||||
let pp_c out c = Fmt.fprintf out "(@[<hv>%a@])" (Util.pp_list Lit.pp) c
|
||||
|
||||
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 _ | B_eq _ -> () (* CC will manage *)
|
||||
| B_distinct l ->
|
||||
let l = IArray.to_list l in
|
||||
if Lit.sign lit then (
|
||||
A.propagate_distinct l ~neq:lit_t lit
|
||||
) else if final && not @@ expanded () then (
|
||||
(* add clause [distinct t1…tn ∨ ∨_{i,j>i} t_i=j] *)
|
||||
let c =
|
||||
Sequence.diagonal_l l
|
||||
|> Sequence.map (fun (t,u) -> Lit.eq self.tst t u)
|
||||
|> Sequence.to_rev_list
|
||||
in
|
||||
let c = Lit.neg lit :: c in
|
||||
Log.debugf 5 (fun k->k "(@[tseitin.distinct.case-split@ %a@])" pp_c c);
|
||||
add_axiom c
|
||||
)
|
||||
| B_and subs ->
|
||||
if Lit.sign lit then (
|
||||
(* propagate [lit => subs_i] *)
|
||||
IArray.iter
|
||||
(fun sub ->
|
||||
let sublit = Lit.atom sub in
|
||||
A.propagate 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 ~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 ~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 ~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 concl :: Lit.neg lit :: List.map (Lit.atom ~sign:false) guard in
|
||||
add_axiom c
|
||||
) else if not @@ Lit.sign lit then (
|
||||
(* propagate [¬lit => ¬concl] *)
|
||||
A.propagate (Lit.atom ~sign:false concl) [lit];
|
||||
(* propagate [¬lit => ∧_i guard_i] *)
|
||||
IArray.iter
|
||||
(fun sub ->
|
||||
let sublit = Lit.atom ~sign:true sub in
|
||||
A.propagate 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 _ | B_eq _ -> ()
|
||||
| v -> tseitin ~final self acts lit t v)
|
||||
|
||||
let partial_check (self:t) acts (lits:Lit.t Sequence.t) =
|
||||
check_ ~final:false self acts lits
|
||||
|
||||
let final_check (self:t) acts (lits:Lit.t Sequence.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
|
||||
22
src/th-bool/Th_dyn_tseitin.mli
Normal file
22
src/th-bool/Th_dyn_tseitin.mli
Normal file
|
|
@ -0,0 +1,22 @@
|
|||
|
||||
(** {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
|
||||
|
||||
module Lit : sig
|
||||
type t = Sidekick_smt.Lit.t
|
||||
val eq : Term.state -> term -> term -> t
|
||||
val neq : Term.state -> term -> term -> t
|
||||
end
|
||||
|
||||
val th : Sidekick_smt.Theory.t
|
||||
end
|
||||
Loading…
Add table
Reference in a new issue