Merge branch 'wip-refactor' back

This commit is contained in:
Simon Cruanes 2019-06-07 16:35:39 -05:00
commit 81e7953261
94 changed files with 4209 additions and 4611 deletions

View file

@ -20,12 +20,6 @@ build: build-install
build-dev:
@dune build $(OPTS)
enable_log:
cd src/core; ln -sf log_real.ml log.ml
disable_log:
cd src/core; ln -sf log_dummy.ml log.ml
clean:
@dune clean
@ -42,7 +36,6 @@ logitest-quick:
--meta `git rev-parse HEAD` --summary snapshots/quick-$(DATE).txt \
--csv snapshots/quick-$(DATE).csv
install: build-install
@dune install
@ -54,19 +47,13 @@ doc:
reinstall: | uninstall install
ocp-indent:
@which ocp-indent > /dev/null || { \
echo 'ocp-indent not found; please run `opam install ocp-indent`'; \
exit 1 ; \
}
reindent: ocp-indent
@find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 echo "reindenting: "
@find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 ocp-indent -i
WATCH=build
WATCH=@install
watch:
@dune build @install -w
@dune build $(WATCH) -w
#@dune build @all -w # TODO: once tests pass
.PHONY: clean doc all bench install uninstall remove reinstall enable_log disable_log bin test
.PHONY: clean doc all bench install uninstall remove reinstall bin test

View file

@ -1,2 +1,3 @@
(lang dune 1.1)
(using menhir 1.0)
(using fmt 1.1)

881
src/base-term/Base_types.ml Normal file
View file

@ -0,0 +1,881 @@
module Vec = Msat.Vec
module Log = Msat.Log
module Fmt = CCFormat
module CC_view = Sidekick_core.CC_view
(* main term cell. *)
type term = {
mutable term_id: int; (* unique ID *)
mutable term_ty: ty;
term_view : term term_view;
}
(* term shallow structure *)
and 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a IArray.t (* full, first-order application *)
| Eq of 'a * 'a
| Not of 'a
(* boolean literal *)
and lit = {
lit_term: term;
lit_sign: bool;
}
and fun_ = {
fun_id: ID.t;
fun_view: fun_view;
}
and fun_view =
| Fun_undef of fun_ty (* simple undefined constant *)
| Fun_def of {
pp : 'a. ('a Fmt.printer -> 'a IArray.t Fmt.printer) option;
abs : self:term -> term IArray.t -> term * bool; (* remove the sign? *)
do_cc: bool; (* participate in congruence closure? *)
relevant : 'a. ID.t -> 'a IArray.t -> int -> bool; (* relevant argument? *)
ty : ID.t -> term IArray.t -> ty; (* compute type *)
eval: value IArray.t -> value; (* evaluate term *)
}
(** Methods on the custom term view whose arguments are ['a].
Terms must be printable, and provide some additional theory handles.
- [relevant] must return a subset of [args] (possibly the same set).
The terms it returns will be activated and evaluated whenever possible.
Terms in [args \ relevant args] are considered for
congruence but not for evaluation.
*)
(** Function type *)
and fun_ty = {
fun_ty_args: ty list;
fun_ty_ret: ty;
}
(** Hashconsed type *)
and ty = {
mutable ty_id: int;
ty_view: ty_view;
}
and ty_view =
| Ty_bool
| Ty_atomic of {
def: ty_def;
args: ty list;
card: ty_card lazy_t;
}
and ty_def =
| Ty_uninterpreted of ID.t
| Ty_def of {
id: ID.t;
pp: ty Fmt.printer -> ty list Fmt.printer;
default_val: value list -> value; (* default value of this type *)
card: ty list -> ty_card;
}
and ty_card =
| Finite
| Infinite
(** Semantic values, used for models (and possibly model-constructing calculi) *)
and value =
| V_bool of bool
| V_element of {
id: ID.t;
ty: ty;
} (** a named constant, distinct from any other constant *)
| V_custom of {
view: value_custom_view;
pp: value_custom_view Fmt.printer;
eq: value_custom_view -> value_custom_view -> bool;
hash: value_custom_view -> int;
} (** Custom value *)
and value_custom_view = ..
let[@inline] term_equal_ (a:term) b = a==b
let[@inline] term_hash_ a = a.term_id
let[@inline] term_cmp_ a b = CCInt.compare a.term_id b.term_id
let cmp_lit a b =
let c = CCBool.compare a.lit_sign b.lit_sign in
if c<>0 then c
else term_cmp_ a.lit_term b.lit_term
let fun_compare a b = ID.compare a.fun_id b.fun_id
let hash_lit a =
let sign = a.lit_sign in
Hash.combine3 2 (Hash.bool sign) (term_hash_ a.lit_term)
let pp_fun out a = ID.pp out a.fun_id
let id_of_fun a = a.fun_id
let[@inline] eq_ty a b = a.ty_id = b.ty_id
let eq_value a b = match a, b with
| V_bool a, V_bool b -> a=b
| V_element e1, V_element e2 ->
ID.equal e1.id e2.id && eq_ty e1.ty e2.ty
| V_custom x1, V_custom x2 ->
x1.eq x1.view x2.view
| V_bool _, _ | V_element _, _ | V_custom _, _
-> false
let hash_value a = match a with
| V_bool a -> Hash.bool a
| V_element e -> ID.hash e.id
| V_custom x -> x.hash x.view
let pp_value out = function
| V_bool b -> Fmt.bool out b
| V_element e -> ID.pp out e.id
| V_custom c -> c.pp out c.view
let pp_db out (i,_) = Format.fprintf out "%%%d" i
let rec pp_ty out t = match t.ty_view with
| Ty_bool -> Fmt.string out "Bool"
| Ty_atomic {def=Ty_uninterpreted id; args=[]; _} -> ID.pp out id
| Ty_atomic {def=Ty_uninterpreted id; args; _} ->
Fmt.fprintf out "(@[%a@ %a@])" ID.pp id (Util.pp_list pp_ty) args
| Ty_atomic {def=Ty_def def; args; _} -> def.pp pp_ty out args
let pp_term_view_gen ~pp_id ~pp_t out = function
| Bool true -> Fmt.string out "true"
| Bool false -> Fmt.string out "false"
| App_fun ({fun_view=Fun_def {pp=Some pp_custom;_};_},l) -> pp_custom pp_t out l
| App_fun (c, a) when IArray.is_empty a ->
pp_id out (id_of_fun c)
| App_fun (f,l) ->
Fmt.fprintf out "(@[<1>%a@ %a@])" pp_id (id_of_fun f) (Util.pp_iarray pp_t) l
| Eq (a,b) -> Fmt.fprintf out "(@[<hv>=@ %a@ %a@])" pp_t a pp_t b
| Not u -> Fmt.fprintf out "(@[not@ %a@])" pp_t u
let pp_term_top ~ids out t =
let rec pp out t =
pp_rec out t;
(* FIXME if Config.pp_hashcons then Format.fprintf out "/%d" t.term_id; *)
and pp_rec out t = pp_term_view_gen ~pp_id ~pp_t:pp_rec out t.term_view
and pp_id = if ids then ID.pp else ID.pp_name in
pp out t
let pp_term = pp_term_top ~ids:false
let pp_term_view = pp_term_view_gen ~pp_id:ID.pp_name ~pp_t:pp_term
let pp_lit out l =
if l.lit_sign then pp_term out l.lit_term
else Format.fprintf out "(@[@<1>¬@ %a@])" pp_term l.lit_term
module Ty_card : sig
type t = ty_card = Finite | Infinite
val (+) : t -> t -> t
val ( * ) : t -> t -> t
val ( ^ ) : t -> t -> t
val finite : t
val infinite : t
val sum : t list -> t
val product : t list -> t
val equal : t -> t -> bool
val compare : t -> t -> int
val pp : t CCFormat.printer
end = struct
type t = ty_card = Finite | Infinite
let (+) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite
let ( * ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite
let ( ^ ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite
let finite = Finite
let infinite = Infinite
let sum = List.fold_left (+) Finite
let product = List.fold_left ( * ) Finite
let equal = (=)
let compare = Pervasives.compare
let pp out = function
| Finite -> CCFormat.string out "finite"
| Infinite -> CCFormat.string out "infinite"
end
module Ty : sig
type t = ty
type view = ty_view
type def = ty_def
val id : t -> int
val view : t -> view
val bool : t
val atomic : def -> t list -> t
val atomic_uninterpreted : ID.t -> t
val card : t -> ty_card
val is_bool : t -> bool
val is_uninterpreted : t -> bool
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pp : t CCFormat.printer
module Tbl : CCHashtbl.S with type key = t
module Fun : sig
type t = fun_ty
val args : t -> ty list
val ret : t -> ty
val arity : t -> int
val unfold : t -> ty list * ty
val mk : ty list -> ty -> t
val pp : t CCFormat.printer
end
end = struct
type t = ty
type view = ty_view
type def = ty_def
let[@inline] id t = t.ty_id
let[@inline] view t = t.ty_view
let equal = eq_ty
let[@inline] compare a b = CCInt.compare a.ty_id b.ty_id
let[@inline] hash a = a.ty_id
let equal_def d1 d2 = match d1, d2 with
| Ty_uninterpreted id1, Ty_uninterpreted id2 -> ID.equal id1 id2
| Ty_def d1, Ty_def d2 -> ID.equal d1.id d2.id
| Ty_uninterpreted _, _ | Ty_def _, _
-> false
module H = Hashcons.Make(struct
type t = ty
let equal a b = match a.ty_view, b.ty_view with
| Ty_bool, Ty_bool -> true
| Ty_atomic a1, Ty_atomic a2 ->
equal_def a1.def a2.def && CCList.equal equal a1.args a2.args
| Ty_bool, _ | Ty_atomic _, _
-> false
let hash t = match t.ty_view with
| Ty_bool -> 1
| Ty_atomic {def=Ty_uninterpreted id; args; _} ->
Hash.combine3 10 (ID.hash id) (Hash.list hash args)
| Ty_atomic {def=Ty_def d; args; _} ->
Hash.combine3 20 (ID.hash d.id) (Hash.list hash args)
let set_id ty id =
assert (ty.ty_id < 0);
ty.ty_id <- id
end)
(* build a type *)
let make_ : ty_view -> t =
let tbl : H.t = H.create ~size:128 () in
fun[@inline] c ->
let ty = {ty_id= -1; ty_view=c; } in
H.hashcons tbl ty
let card t = match view t with
| Ty_bool -> Finite
| Ty_atomic {card=lazy c; _} -> c
let bool = make_ Ty_bool
let atomic def args : t =
let card = lazy (
match def with
| Ty_uninterpreted _ ->
if List.for_all (fun sub -> card sub = Finite) args then Finite else Infinite
| Ty_def d -> d.card args
) in
make_ (Ty_atomic {def; args; card})
let atomic_uninterpreted id = atomic (Ty_uninterpreted id) []
let is_bool t =
match t.ty_view with | Ty_bool -> true | _ -> false
let is_uninterpreted t =
match t.ty_view with | Ty_atomic {def=Ty_uninterpreted _; _} -> true | _ -> false
let pp = pp_ty
module Tbl = CCHashtbl.Make(struct
type t = ty
let equal = equal
let hash = hash
end)
module Fun = struct
type t = fun_ty
let[@inline] args f = f.fun_ty_args
let[@inline] ret f = f.fun_ty_ret
let[@inline] arity f = List.length @@ args f
let[@inline] mk args ret : t = {fun_ty_args=args; fun_ty_ret=ret}
let[@inline] unfold t = args t, ret t
let pp out f : unit =
match args f with
| [] -> pp out (ret f)
| args ->
Format.fprintf out "(@[(@[%a@])@ %a@])" (Util.pp_list pp) args pp (ret f)
end
end
module Fun : sig
type view = fun_view
type t = fun_
val id : t -> ID.t
val view : t -> view
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val as_undefined : t -> (t * Ty.Fun.t) option
val as_undefined_exn : t -> t * Ty.Fun.t
val is_undefined : t -> bool
val do_cc : t -> bool
val mk_undef : ID.t -> Ty.Fun.t -> t
val mk_undef_const : ID.t -> Ty.t -> t
val pp : t CCFormat.printer
module Map : CCMap.S with type key = t
module Tbl : CCHashtbl.S with type key = t
end = struct
type view = fun_view
type t = fun_
let[@inline] id t = t.fun_id
let[@inline] view t = t.fun_view
let[@inline] make fun_id fun_view = {fun_id; fun_view}
let as_undefined (c:t) = match view c with
| Fun_undef ty -> Some (c,ty)
| Fun_def _ -> None
let[@inline] is_undefined c = match view c with Fun_undef _ -> true | _ -> false
let as_undefined_exn (c:t) = match as_undefined c with
| Some tup -> tup
| None -> assert false
let[@inline] mk_undef id ty = make id (Fun_undef ty)
let[@inline] mk_undef_const id ty = mk_undef id (Ty.Fun.mk [] ty)
let[@inline] do_cc (c:t) : bool = match view c with
| Fun_undef _ -> true
| Fun_def {do_cc;_} -> do_cc
let equal a b = ID.equal a.fun_id b.fun_id
let compare a b = ID.compare a.fun_id b.fun_id
let hash t = ID.hash t.fun_id
let pp out a = ID.pp out a.fun_id
module As_key = struct
type nonrec t = t
let compare = compare
let equal = equal
let hash = hash
end
module Map = CCMap.Make(As_key)
module Tbl = CCHashtbl.Make(As_key)
end
module Term_cell : sig
type 'a view = 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a IArray.t
| Eq of 'a * 'a
| Not of 'a
type t = term view
val equal : t -> t -> bool
val hash : t -> int
val true_ : t
val false_ : t
val const : fun_ -> t
val app_fun : fun_ -> term IArray.t -> t
val eq : term -> term -> t
val not_ : term -> t
val ty : t -> Ty.t
(** Compute the type of this term cell. Not totally free *)
val pp : t Fmt.printer
val map : ('a -> 'b) -> 'a view -> 'b view
val iter : ('a -> unit) -> 'a view -> unit
module type ARG = sig
type t
val hash : t -> int
val equal : t -> t -> bool
val pp : t Fmt.printer
end
module Make_eq(X : ARG) : sig
val equal : X.t view -> X.t view -> bool
val hash : X.t view -> int
val pp : X.t view Fmt.printer
end
end = struct
type 'a view = 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a IArray.t
| Eq of 'a * 'a
| Not of 'a
type t = term view
module type ARG = sig
type t
val hash : t -> int
val equal : t -> t -> bool
val pp : t Fmt.printer
end
module Make_eq(A : ARG) = struct
let sub_hash = A.hash
let sub_eq = A.equal
let hash (t:A.t view) : int = match t with
| Bool b -> Hash.bool b
| App_fun (f,l) ->
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)
(* equality that relies on physical equality of subterms *)
let equal (a:A.t view) b : bool = match a, b with
| Bool b1, Bool b2 -> CCBool.equal b1 b2
| App_fun (f1, a1), App_fun (f2, a2) ->
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 _, _
-> false
let pp = pp_term_view_gen ~pp_id:ID.pp_name ~pp_t:A.pp
end[@@inline]
include Make_eq(struct
type t = term
let equal (t1:t) t2 = t1==t2
let hash (t:term): int = CCHash.int t.term_id
let pp = pp_term
end)
let true_ = Bool true
let false_ = Bool false
let app_fun f a = App_fun (f, a)
let const c = App_fun (c, IArray.empty)
let eq a b =
if term_equal_ a b then (
Bool true
) else (
(* canonize *)
let a,b = if a.term_id > b.term_id then b, a else a, b in
Eq (a,b)
)
let not_ t =
match t.term_view with
| Bool b -> Bool (not b)
| Not u -> u.term_view
| _ -> Not t
let ty (t:t): Ty.t = match t with
| Bool _ | Eq _ | Not _ -> Ty.bool
| App_fun (f, args) ->
begin match Fun.view f with
| Fun_undef fty ->
let ty_args, ty_ret = Ty.Fun.unfold fty in
(* check arity *)
if List.length ty_args <> IArray.length args then (
Error.errorf "Term_cell.apply: expected %d args, got %d@ in %a"
(List.length ty_args) (IArray.length args) pp t
);
(* check types *)
List.iteri
(fun i ty_a ->
let a = IArray.get args i in
if not @@ Ty.equal a.term_ty ty_a then (
Error.errorf "Term_cell.apply: %d-th argument mismatch:@ \
%a does not have type %a@ in %a"
i pp_term a Ty.pp ty_a pp t
))
ty_args;
ty_ret
| Fun_def def -> def.ty f.fun_id args
end
let iter f view =
match view with
| Bool _ -> ()
| App_fun (_,a) -> IArray.iter f a
| Not u -> f u
| Eq (a,b) -> f a; f b
let map f view =
match view with
| Bool b -> Bool b
| App_fun (fu,a) -> App_fun (fu, IArray.map f a)
| Not u -> Not (f u)
| Eq (a,b) -> Eq (f a, f b)
module Tbl = CCHashtbl.Make(struct
type t = term view
let equal = equal
let hash = hash
end)
end
module Term : sig
type t = term = {
mutable term_id : int;
mutable term_ty : ty;
term_view : t term_view;
}
type 'a view = 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a IArray.t
| Eq of 'a * 'a
| Not of 'a
val id : t -> int
val view : t -> term view
val ty : t -> Ty.t
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
type state
val create : ?size:int -> unit -> state
val make : state -> t view -> t
val true_ : state -> t
val false_ : state -> t
val bool : state -> bool -> t
val const : state -> fun_ -> t
val app_fun : state -> fun_ -> t IArray.t -> t
val eq : state -> t -> t -> t
val not_ : state -> t -> t
(** Obtain unsigned version of [t], + the sign as a boolean *)
val abs : state -> t -> t * bool
module Iter_dag : sig
type t
val create : unit -> t
val iter_dag : t -> term -> term Iter.t
end
val iter_dag : t -> t Iter.t
val map_shallow : state -> (t -> t) -> t -> t
val pp : t Fmt.printer
(** {6 Views} *)
val is_true : t -> bool
val is_false : t -> bool
val is_const : t -> bool
val cc_view : t -> (fun_,t,t Iter.t) CC_view.t
(* return [Some] iff the term is an undefined constant *)
val as_fun_undef : t -> (fun_ * Ty.Fun.t) option
val as_bool : t -> bool option
(** {6 Containers} *)
module Tbl : CCHashtbl.S with type key = t
module Map : CCMap.S with type key = t
module Set : CCSet.S with type elt = t
end = struct
type t = term = {
mutable term_id : int;
mutable term_ty : ty;
term_view : t term_view;
}
type 'a view = 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a IArray.t
| Eq of 'a * 'a
| Not of 'a
let[@inline] id t = t.term_id
let[@inline] ty t = t.term_ty
let[@inline] view t = t.term_view
let equal = term_equal_
let hash = term_hash_
let compare a b = CCInt.compare a.term_id b.term_id
module H = Hashcons.Make(struct
type t = term
let equal t1 t2 = Term_cell.equal t1.term_view t2.term_view
let hash t = Term_cell.hash t.term_view
let set_id t id =
assert (t.term_id < 0);
t.term_id <- id
end)
type state = {
tbl : H.t;
mutable n: int;
true_ : t lazy_t;
false_ : t lazy_t;
}
let[@inline] make st (c:t term_view) : t =
let t = {term_id= -1; term_ty=Ty.bool; term_view=c} in
let t' = H.hashcons st.tbl t in
if t == t' then (
t'.term_ty <- Term_cell.ty c;
);
t'
let[@inline] true_ st = Lazy.force st.true_
let[@inline] false_ st = Lazy.force st.false_
let bool st b = if b then true_ st else false_ st
let create ?(size=1024) () : state =
let rec st ={
n=2;
tbl=H.create ~size ();
true_ = lazy (make st Term_cell.true_);
false_ = lazy (make st Term_cell.false_);
} in
ignore (Lazy.force st.true_);
ignore (Lazy.force st.false_); (* not true *)
st
let app_fun st f a =
let cell = Term_cell.app_fun f a in
make st cell
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)
(* might need to tranfer the negation from [t] to [sign] *)
let abs tst t : t * bool = match view t with
| Bool false -> true_ tst, false
| Not u -> u, false
| App_fun ({fun_view=Fun_def def; _}, args) ->
def.abs ~self:t args (* TODO: pass state *)
| _ -> t, true
let[@inline] is_true t = match view t with Bool true -> true | _ -> false
let[@inline] is_false t = match view t with Bool false -> true | _ -> false
let[@inline] is_const t = match view t with
| App_fun (_, a) -> IArray.is_empty a
| _ -> false
let cc_view (t:t) =
let module C = CC_view in
match view t with
| Bool b -> C.Bool b
| App_fun (f,_) when not (Fun.do_cc f) -> C.Opaque t (* skip *)
| App_fun (f,args) -> C.App_fun (f, IArray.to_seq args)
| Eq (a,b) -> C.Eq (a, b)
| Not u -> C.Not u
module As_key = struct
type t = term
let compare = compare
let equal = equal
let hash = hash
end
module Map = CCMap.Make(As_key)
module Set = CCSet.Make(As_key)
module Tbl = CCHashtbl.Make(As_key)
(* return [Some] iff the term is an undefined constant *)
let as_fun_undef (t:term): (fun_ * Ty.Fun.t) option =
match view t with
| App_fun (c, a) when IArray.is_empty a -> Fun.as_undefined c
| _ -> None
let as_bool t = match view t with
| Bool b -> Some b
| _ -> None
let pp = pp_term
module Iter_dag = struct
type t = unit Tbl.t
let create () : t = Tbl.create 16
let iter_dag (self:t) t yield =
let rec aux t =
if not @@ Tbl.mem self t then (
Tbl.add self t ();
yield t;
Term_cell.iter aux (view t)
)
in
aux t
end
let iter_dag t yield =
let st = Iter_dag.create() in
Iter_dag.iter_dag st t yield
let map_shallow (tst:state) f (t:t) : t =
match view t with
| Bool _ -> t
| 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)
end
module Lit : sig
type t = lit = {
lit_term: term;
lit_sign : bool
}
val neg : t -> t
val abs : t -> t
val sign : t -> bool
val term : t -> term
val as_atom : t -> term * bool
val atom : Term.state -> ?sign:bool -> term -> t
val hash : t -> int
val compare : t -> t -> int
val equal : t -> t -> bool
val print : t Fmt.printer
val pp : t Fmt.printer
val apply_sign : t -> bool -> t
val norm_sign : t -> t * bool
val norm : t -> t * Msat.negated
module Set : CCSet.S with type elt = t
module Tbl : CCHashtbl.S with type key = t
end = struct
type t = lit = {
lit_term: term;
lit_sign : bool
}
let[@inline] neg l = {l with lit_sign=not l.lit_sign}
let[@inline] sign t = t.lit_sign
let[@inline] term (t:t): term = t.lit_term
let[@inline] abs t: t = {t with lit_sign=true}
let make ~sign t = {lit_sign=sign; lit_term=t}
let atom tst ?(sign=true) (t:term) : t =
let t, sign' = Term.abs tst t in
let sign = if not sign' then not sign else sign in
make ~sign t
let[@inline] as_atom (lit:t) = lit.lit_term, lit.lit_sign
let hash = hash_lit
let compare = cmp_lit
let[@inline] equal a b = compare a b = 0
let pp = pp_lit
let print = pp
let apply_sign t s = if s then t else neg t
let norm_sign l = if l.lit_sign then l, true else neg l, false
let norm l = let l, sign = norm_sign l in l, if sign then Msat.Same_sign else Msat.Negated
module Set = CCSet.Make(struct type t = lit let compare=compare end)
module Tbl = CCHashtbl.Make(struct type t = lit let equal=equal let hash=hash end)
end
module Value : sig
type t = value =
| V_bool of bool
| V_element of {id: ID.t; ty: ty}
| V_custom of {
view: value_custom_view;
pp: value_custom_view Fmt.printer;
eq: value_custom_view -> value_custom_view -> bool;
hash: value_custom_view -> int;
}
val true_ : t
val false_ : t
val bool : bool -> t
val mk_elt : ID.t -> Ty.t -> t
val is_bool : t -> bool
val is_true : t -> bool
val is_false : t -> bool
val fresh : Term.t -> t
val hash : t -> int
val equal : t -> t -> bool
val pp : t Fmt.printer
end = struct
type t = value =
| V_bool of bool
| V_element of {id: ID.t; ty: ty}
| V_custom of {
view: value_custom_view;
pp: value_custom_view Fmt.printer;
eq: value_custom_view -> value_custom_view -> bool;
hash: value_custom_view -> int;
}
let true_ = V_bool true
let false_ = V_bool false
let[@inline] bool v = if v then true_ else false_
let mk_elt id ty : t = V_element {id; ty}
let[@inline] is_bool = function V_bool _ -> true | _ -> false
let[@inline] is_true = function V_bool true -> true | _ -> false
let[@inline] is_false = function V_bool false -> true | _ -> false
let equal = eq_value
let hash = hash_value
let pp = pp_value
let fresh (t:term) : t =
mk_elt (ID.makef "v_%d" t.term_id) t.term_ty
end
module Proof = struct
type t = Default
let default = Default
end
module type CC_ACTIONS = sig
val raise_conflict : Lit.t list -> Proof.t -> 'a
val propagate : Lit.t -> reason:(unit -> Lit.t list) -> Proof.t -> unit
end
type cc_actions = (module CC_ACTIONS)

View file

@ -1,9 +1,8 @@
(* This file is free software. See file "license" for more details. *)
(** {1 Model} *)
open Solver_types
open Base_types
module Val_map = struct
module M = CCIntMap
@ -50,12 +49,12 @@ end
type t = {
values: Value.t Term.Map.t;
funs: Fun_interpretation.t Cst.Map.t;
funs: Fun_interpretation.t Fun.Map.t;
}
let empty : t = {
values=Term.Map.empty;
funs=Cst.Map.empty;
funs=Fun.Map.empty;
}
(* FIXME: ues this to allocate a default value for each sort
@ -91,10 +90,10 @@ let add t v m : t =
{m with values=Term.Map.add t v m.values}
let add_fun c v m : t =
match Cst.Map.find c m.funs with
| _ -> Error.errorf "@[Model: function %a already has an interpretation@]" Cst.pp c
match Fun.Map.find c m.funs with
| _ -> Error.errorf "@[Model: function %a already has an interpretation@]" Fun.pp c
| exception Not_found ->
{m with funs=Cst.Map.add c v m.funs}
{m with funs=Fun.Map.add c v m.funs}
(* merge two models *)
let merge m1 m2 : t =
@ -108,11 +107,11 @@ let merge m1 m2 : t =
Term.pp t Value.pp v1 Value.pp v2
))
and funs =
Cst.Map.merge_safe m1.funs m2.funs
Fun.Map.merge_safe m1.funs m2.funs
~f:(fun c o -> match o with
| `Left v | `Right v -> Some v
| `Both _ ->
Error.errorf "cannot merge the two interpretations of function %a" Cst.pp c)
Error.errorf "cannot merge the two interpretations of function %a" Fun.pp c)
in
{values; funs}
@ -124,14 +123,14 @@ let pp out {values; funs} =
let pp_fun_entry out (vals,ret) =
Format.fprintf out "(@[%a@ := %a@])" (Fmt.Dump.list Value.pp) vals Value.pp ret
in
let pp_fun out (c, fi: Cst.t * FI.t) =
let pp_fun out (c, fi: Fun.t * FI.t) =
Format.fprintf out "(@[<hov>%a :default %a@ %a@])"
Cst.pp c Value.pp fi.FI.default
Fun.pp c Value.pp fi.FI.default
(Fmt.list ~sep:(Fmt.return "@ ") pp_fun_entry) (FI.cases_list fi)
in
Fmt.fprintf out "(@[model@ @[:terms (@[<hv>%a@])@]@ @[:funs (@[<hv>%a@])@]@])"
(Fmt.seq ~sep:Fmt.(return "@ ") pp_tv) (Term.Map.to_seq values)
(Fmt.seq ~sep:Fmt.(return "@ ") pp_fun) (Cst.Map.to_seq funs)
(Fmt.seq ~sep:Fmt.(return "@ ") pp_fun) (Fun.Map.to_seq funs)
exception No_value
@ -139,12 +138,6 @@ let eval (m:t) (t:Term.t) : Value.t option =
let module FI = Fun_interpretation in
let rec aux t = match Term.view t with
| Bool b -> Value.bool b
| If (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@ %a@]" Term.pp a Value.pp v
end
| Not a ->
begin match aux a with
| V_bool b -> V_bool (not b)
@ -154,16 +147,16 @@ let eval (m:t) (t:Term.t) : Value.t option =
let a = aux a in
let b = aux b in
if Value.equal a b then Value.true_ else Value.false_
| App_cst (c, args) ->
match Cst.view c with
| Cst_def udef ->
| App_fun (c, args) ->
match Fun.view c with
| Fun_def udef ->
(* use builtin interpretation function *)
let args = IArray.map aux args in
udef.eval args
| Cst_undef _ ->
| Fun_undef _ ->
try Term.Map.find t m.values
with Not_found ->
begin match Cst.Map.find c m.funs with
begin match Fun.Map.find c m.funs with
| fi ->
let args = IArray.map aux args |> IArray.to_list in
begin match Val_map.find args fi.FI.cases with
@ -176,3 +169,45 @@ let eval (m:t) (t:Term.t) : Value.t option =
in
try Some (aux t)
with No_value -> None
(* TODO: get model from each theory, then complete it as follows based on types
let mk_model (cc:t) (m:A.Model.t) : A.Model.t =
let module Model = A.Model in
let module Value = A.Value in
Log.debugf 15 (fun k->k "(@[cc.mk-model@ %a@])" pp_full cc);
let t_tbl = N_tbl.create 32 in
(* populate [repr -> value] table *)
T_tbl.values cc.tbl
(fun r ->
if N.is_root r then (
(* find a value in the class, if any *)
let v =
N.iter_class r
|> Iter.find_map (fun n -> Model.eval m n.n_term)
in
let v = match v with
| Some v -> v
| None ->
if same_class r (true_ cc) then Value.true_
else if same_class r (false_ cc) then Value.false_
else Value.fresh r.n_term
in
N_tbl.add t_tbl r v
));
(* now map every term to its representative's value *)
let pairs =
T_tbl.values cc.tbl
|> Iter.map
(fun n ->
let r = find_ n in
let v =
try N_tbl.find t_tbl r
with Not_found ->
Error.errorf "didn't allocate a value for repr %a" N.pp r
in
n.n_term, v)
in
let m = Iter.fold (fun m (t,v) -> Model.add t v m) m pairs in
Log.debugf 5 (fun k->k "(@[cc.model@ %a@])" Model.pp m);
m
*)

View file

@ -1,8 +1,9 @@
(* This file is free software. See file "license" for more details. *)
(** {1 Model} *)
open Base_types
module Val_map : sig
type key = Value.t list
type 'a t
@ -30,7 +31,7 @@ end
type t = {
values: Value.t Term.Map.t;
funs: Fun_interpretation.t Cst.Map.t;
funs: Fun_interpretation.t Fun.Map.t;
}
val empty : t

View file

@ -0,0 +1,24 @@
module Base_types = Base_types
module ID = ID
module Ty_card = Base_types.Ty_card
module Fun = Base_types.Fun
module Stat = Stat
module Model = Model
module Term = Base_types.Term
module Value = Base_types.Value
module Term_cell = Base_types.Term_cell
module Ty = Base_types.Ty
module Lit = Base_types.Lit
module Arg
: Sidekick_core.TERM_LIT
with type Term.t = Term.t
and type Lit.t = Lit.t
and type Fun.t = Fun.t
and type Ty.t = Ty.t
= struct
module Term = Term
module Lit = Lit
module Fun = Fun
module Ty = Ty
end

7
src/base-term/dune Normal file
View file

@ -0,0 +1,7 @@
(library
(name sidekick_base_term)
(public_name sidekick.base-term)
(synopsis "Basic term definitions for the standalone SMT solver")
(libraries containers containers.data
sidekick.core sidekick.util zarith)
(flags :standard -w -32 -open Sidekick_util))

View file

@ -1,115 +0,0 @@
(** {1 Types used by the congruence closure} *)
type ('f, 't, 'ts) view =
| Bool of bool
| App_fun of 'f * 'ts
| App_ho of 't * 'ts
| If of 't * 't * 't
| Eq of 't * 't
| Not of 't
| Opaque of 't (* do not enter *)
let[@inline] map_view ~f_f ~f_t ~f_ts (v:_ view) : _ view =
match v with
| Bool b -> Bool b
| App_fun (f, args) -> App_fun (f_f f, f_ts args)
| App_ho (f, args) -> App_ho (f_t f, f_ts args)
| Not t -> Not (f_t t)
| If (a,b,c) -> If (f_t a, f_t b, f_t c)
| Eq (a,b) -> Eq (f_t a, f_t b)
| Opaque t -> Opaque (f_t t)
let iter_view ~f_f ~f_t ~f_ts (v:_ view) : unit =
match v with
| Bool _ -> ()
| App_fun (f, args) -> f_f f; f_ts args
| App_ho (f, args) -> f_t f; f_ts args
| Not t -> f_t t
| If (a,b,c) -> f_t a; f_t b; f_t c;
| Eq (a,b) -> f_t a; f_t b
| Opaque t -> f_t t
module type TERM = sig
module Fun : sig
type t
val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
end
module Term : sig
type t
val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
type state
val bool : state -> bool -> t
(** View the term through the lens of the congruence closure *)
val cc_view : t -> (Fun.t, t, t Iter.t) view
end
end
module type TERM_LIT = sig
include TERM
module Lit : sig
type t
val neg : t -> t
val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
val sign : t -> bool
val term : t -> Term.t
end
end
module type FULL = sig
include TERM_LIT
module Proof : sig
type t
val pp : t Fmt.printer
val default : t
(* TODO: to give more details
val cc_lemma : unit -> t
*)
end
module Ty : sig
type t
val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
end
module Value : sig
type t
val pp : t Fmt.printer
val fresh : Term.t -> t
val true_ : t
val false_ : t
end
module Model : sig
type t
val pp : t Fmt.printer
val eval : t -> Term.t -> Value.t option
(** Evaluate the term in the current model *)
val add : Term.t -> Value.t -> t -> t
end
end
(* TODO: micro theory *)

File diff suppressed because it is too large Load diff

View file

@ -1,16 +0,0 @@
(** {2 Congruence Closure} *)
module type ARG = Congruence_closure_intf.ARG
module type S = Congruence_closure_intf.S
module type THEORY_KEY = Congruence_closure_intf.THEORY_KEY
module Key : THEORY_KEY
module Make(A: ARG)
: S with type term = A.Term.t
and type lit = A.Lit.t
and type fun_ = A.Fun.t
and type term_state = A.Term.state
and type proof = A.Proof.t
and type model = A.Model.t
and module Key = Key

View file

@ -1,221 +0,0 @@
module type ARG = CC_types.FULL
module type THEORY_KEY = sig
type ('term,'lit,'a) t
(** An access key for theories which have per-class data ['a] *)
val create :
?pp:'a Fmt.printer ->
name:string ->
eq:('a -> 'a -> bool) ->
merge:('a -> 'a -> 'a) ->
unit ->
('term,'lit,'a) t
(** Generative creation of keys for the given theory data.
@param eq : Equality. This is used to optimize backtracking info.
@param merge :
[merge d1 d2] is called when merging classes with data [d1] and [d2]
respectively. The theory should already have checked that the merge
is compatible, and this produces the combined data for terms in the
merged class.
@param name name of the theory which owns this data
@param pp a printer for the data
*)
val equal : ('t,'lit,_) t -> ('t,'lit,_) t -> bool
(** Checks if two keys are equal (generatively) *)
val pp : _ t Fmt.printer
(** Prints the name of the key. *)
end
module type S = sig
type term_state
type term
type fun_
type lit
type proof
type model
(** Implementation of theory keys *)
module Key : THEORY_KEY
type t
(** Global state of the congruence closure *)
(** An equivalence class is a set of terms that are currently equal
in the partial model built by the solver.
The class is represented by a collection of nodes, one of which is
distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored
in this representative's node.
When two classes become equal (are "merged"), one of the two
representatives is picked as the representative of the new class.
The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the
representative. This information can be used when two classes are
merged, to detect conflicts and solve equations à la Shostak.
*)
module N : sig
type t
val term : t -> term
val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
val is_root : t -> bool
(** Is the node a root (ie the representative of its class)? *)
val iter_class : t -> t Iter.t
(** Traverse the congruence class.
Invariant: [is_root n] (see {!find} below) *)
val iter_parents : t -> t Iter.t
(** Traverse the parents of the class.
Invariant: [is_root n] (see {!find} below) *)
end
module Expl : sig
type t
val pp : t Fmt.printer
val mk_merge : N.t -> N.t -> t
val mk_lit : lit -> t
val mk_list : t list -> t
end
type node = N.t
(** A node of the congruence closure *)
type repr = N.t
(** Node that is currently a representative *)
type explanation = Expl.t
type conflict = lit list
(** Accessors *)
val term_state : t -> term_state
val find : t -> node -> repr
(** Current representative *)
val add_term : t -> term -> node
(** Add the term to the congruence closure, if not present already.
Will be backtracked. *)
(** Actions available to the theory *)
type sat_actions = (Msat.void, lit, Msat.void, proof) Msat.acts
module Theory : sig
type cc = t
type t
type 'a key = (term,lit,'a) Key.t
val raise_conflict : cc -> Expl.t -> unit
(** Raise a conflict with the given explanation
it must be a theory tautology that [expl ==> absurd].
To be used in theories. *)
val merge : cc -> N.t -> N.t -> Expl.t -> unit
(** Merge these two nodes given this explanation.
It must be a theory tautology that [expl ==> n1 = n2].
To be used in theories. *)
val add_term : cc -> term -> N.t
(** Add/retrieve node for this term.
To be used in theories *)
val get_data : cc -> N.t -> 'a key -> 'a option
(** Get data information for this particular representative *)
val add_data : cc -> N.t -> 'a key -> 'a -> unit
(** Add data to this particular representative. Will be backtracked. *)
val make :
key:'a key ->
on_merge:(cc -> N.t -> 'a -> N.t -> 'a -> Expl.t -> unit) ->
on_new_term:(cc -> N.t -> term -> 'a option) ->
unit ->
t
(** Build a micro theory. It can use the callbacks above. *)
end
val create :
?stat:Stat.t ->
?th:Theory.t list ->
?on_merge:(t -> N.t -> N.t -> Expl.t -> unit) list ->
?size:[`Small | `Big] ->
term_state ->
t
(** Create a new congruence closure. *)
val add_th : t -> Theory.t -> unit
(** Add a (micro) theory to the congruence closure.
@raise Error.Error if there is already a theory with
the same key. *)
val on_merge : t -> (t -> N.t -> N.t -> Expl.t -> unit) -> unit
(** Add a function to be called when two classes are merged *)
val set_as_lit : t -> N.t -> lit -> unit
(** map the given node to a literal. *)
val find_t : t -> term -> repr
(** Current representative of the term.
@raise Not_found if the term is not already {!add}-ed. *)
val add_seq : t -> term Iter.t -> unit
(** Add a sequence of terms to the congruence closure *)
val all_classes : t -> repr Iter.t
(** All current classes. This is costly, only use if there is no other solution *)
val assert_lit : t -> lit -> unit
(** Given a literal, assume it in the congruence closure and propagate
its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor *)
val assert_lits : t -> lit Iter.t -> unit
(** Addition of many literals *)
val assert_eq : t -> term -> term -> lit list -> unit
(** merge the given terms with some explanations *)
(* TODO: remove and move into its own library as a micro theory
val assert_distinct : t -> term list -> neq:term -> lit -> unit
(** [assert_distinct l ~neq:u e] asserts all elements of [l] are distinct
because [lit] is true
precond: [u = distinct l] *)
*)
val check : t -> sat_actions -> unit
(** Perform all pending operations done via {!assert_eq}, {!assert_lit}, etc.
Will use the [sat_actions] to propagate literals, declare conflicts, etc. *)
val push_level : t -> unit
(** Push backtracking level *)
val pop_levels : t -> int -> unit
(** Restore to state [n] calls to [push_level] earlier. Used during backtracking. *)
val mk_model : t -> model -> model
(** Enrich a model by mapping terms to their representative's value,
if any. Otherwise map the representative to a fresh value *)
(**/**)
val check_invariants : t -> unit
val pp_full : t Fmt.printer
(**/**)
end

View file

@ -1,5 +1,6 @@
module View = Sidekick_core.CC_view
type ('f, 't, 'ts) view = ('f, 't, 'ts) CC_types.view =
type ('f, 't, 'ts) view = ('f, 't, 'ts) View.t =
| Bool of bool
| App_fun of 'f * 'ts
| App_ho of 't * 'ts
@ -8,16 +9,848 @@ type ('f, 't, 'ts) view = ('f, 't, 'ts) CC_types.view =
| Not of 't
| Opaque of 't (* do not enter *)
module CC_types = CC_types
module type ARG = Sidekick_core.CC_ARG
module type S = Sidekick_core.CC_S
(** Parameter for the congruence closure *)
module type TERM_LIT = CC_types.TERM_LIT
module type FULL = CC_types.FULL
module type S = Congruence_closure.S
module Make(CC_A: ARG) = struct
module CC_A = CC_A
module A = CC_A.A
type term = A.Term.t
type term_state = A.Term.state
type lit = A.Lit.t
type fun_ = A.Fun.t
type proof = A.Proof.t
type actions = CC_A.Actions.t
module Mini_cc = Mini_cc
module Congruence_closure = Congruence_closure
module Key = Congruence_closure.Key
module T = A.Term
module Fun = A.Fun
module Lit = A.Lit
module Make = Congruence_closure.Make
module Bits = CCBitField.Make()
(* TODO: give theories the possibility to allocate new bits in nodes *)
let field_is_pending = Bits.mk_field()
(** true iff the node is in the [cc.pending] queue *)
let field_marked_explain = Bits.mk_field()
(** used to mark traversed nodes when looking for a common ancestor *)
(** A node of the congruence closure.
An equivalence class is represented by its "root" element,
the representative. *)
type node = {
n_term: term;
mutable n_sig0: signature option; (* initial signature *)
mutable n_bits: Bits.t; (* bitfield for various properties *)
mutable n_parents: node Bag.t; (* parent terms of this node *)
mutable n_root: node; (* representative of congruence class (itself if a representative) *)
mutable n_next: node; (* pointer to next element of congruence class *)
mutable n_size: int; (* size of the class *)
mutable n_as_lit: lit option; (* TODO: put into payload? and only in root? *)
mutable n_expl: explanation_forest_link; (* the rooted forest for explanations *)
}
and signature = (fun_, node, node list) view
and explanation_forest_link =
| FL_none
| FL_some of {
next: node;
expl: explanation;
}
(* atomic explanation in the congruence closure *)
and explanation =
| E_reduction (* by pure reduction, tautologically equal *)
| E_lit of lit (* because of this literal *)
| E_merge of node * node
| E_merge_t of term * term
| E_congruence of node * node (* caused by normal congruence *)
| E_and of explanation * explanation
type repr = node
module N = struct
type t = node
let[@inline] equal (n1:t) n2 = n1 == n2
let[@inline] hash n = T.hash n.n_term
let[@inline] term n = n.n_term
let[@inline] pp out n = T.pp out n.n_term
let[@inline] as_lit n = n.n_as_lit
let make (t:term) : t =
let rec n = {
n_term=t;
n_sig0= None;
n_bits=Bits.empty;
n_parents=Bag.empty;
n_as_lit=None; (* TODO: provide a method to do it *)
n_root=n;
n_expl=FL_none;
n_next=n;
n_size=1;
} in
n
let[@inline] is_root (n:node) : bool = n.n_root == n
(* traverse the equivalence class of [n] *)
let iter_class_ (n:node) : node Iter.t =
fun yield ->
let rec aux u =
yield u;
if u.n_next != n then aux u.n_next
in
aux n
let[@inline] iter_class n =
assert (is_root n);
iter_class_ n
let[@inline] iter_parents (n:node) : node Iter.t =
assert (is_root n);
Bag.to_seq n.n_parents
let[@inline] get_field f t = Bits.get f t.n_bits
let[@inline] set_field f b t = t.n_bits <- Bits.set f b t.n_bits
end
module N_tbl = CCHashtbl.Make(N)
module Expl = struct
type t = explanation
let rec pp out (e:explanation) = match e with
| E_reduction -> Fmt.string out "reduction"
| E_lit lit -> Lit.pp out lit
| E_congruence (n1,n2) -> Fmt.fprintf out "(@[congruence@ %a@ %a@])" N.pp n1 N.pp n2
| E_merge (a,b) -> Fmt.fprintf out "(@[merge@ %a@ %a@])" N.pp a N.pp b
| E_merge_t (a,b) -> Fmt.fprintf out "(@[merge@ %a@ %a@])" T.pp a T.pp b
| E_and (a,b) ->
Format.fprintf out "(@[<hv1>and@ %a@ %a@])" pp a pp b
let mk_reduction : t = E_reduction
let[@inline] mk_congruence n1 n2 : t = E_congruence (n1,n2)
let[@inline] mk_merge a b : t = if N.equal a b then mk_reduction else E_merge (a,b)
let[@inline] mk_merge_t a b : t = if T.equal a b then mk_reduction else E_merge_t (a,b)
let[@inline] mk_lit l : t = E_lit l
let rec mk_list l =
match l with
| [] -> mk_reduction
| [x] -> x
| E_reduction :: tl -> mk_list tl
| x :: y ->
match mk_list y with
| E_reduction -> x
| y' -> E_and (x,y')
end
(** A signature is a shallow term shape where immediate subterms
are representative *)
module Signature = struct
type t = signature
let equal (s1:t) s2 : bool =
match s1, s2 with
| Bool b1, Bool b2 -> b1=b2
| App_fun (f1,[]), App_fun (f2,[]) -> Fun.equal f1 f2
| App_fun (f1,l1), App_fun (f2,l2) ->
Fun.equal f1 f2 && CCList.equal N.equal l1 l2
| App_ho (f1,l1), App_ho (f2,l2) ->
N.equal f1 f2 && CCList.equal N.equal l1 l2
| Not a, Not b -> N.equal a b
| If (a1,b1,c1), If (a2,b2,c2) ->
N.equal a1 a2 && N.equal b1 b2 && N.equal c1 c2
| Eq (a1,b1), Eq (a2,b2) ->
N.equal a1 a2 && N.equal b1 b2
| Opaque u1, Opaque u2 -> N.equal u1 u2
| Bool _, _ | App_fun _, _ | App_ho _, _ | If _, _
| Eq _, _ | Opaque _, _ | Not _, _
-> false
let hash (s:t) : int =
let module H = CCHash in
match s with
| Bool b -> H.combine2 10 (H.bool b)
| App_fun (f, l) -> H.combine3 20 (Fun.hash f) (H.list N.hash l)
| App_ho (f, l) -> H.combine3 30 (N.hash f) (H.list N.hash l)
| Eq (a,b) -> H.combine3 40 (N.hash a) (N.hash b)
| Opaque u -> H.combine2 50 (N.hash u)
| If (a,b,c) -> H.combine4 60 (N.hash a)(N.hash b)(N.hash c)
| Not u -> H.combine2 70 (N.hash u)
let pp out = function
| Bool b -> Fmt.bool out b
| App_fun (f, []) -> Fun.pp out f
| App_fun (f, l) -> Fmt.fprintf out "(@[%a@ %a@])" Fun.pp f (Util.pp_list N.pp) l
| App_ho (f, []) -> N.pp out f
| App_ho (f, l) -> Fmt.fprintf out "(@[%a@ %a@])" N.pp f (Util.pp_list N.pp) l
| Opaque t -> N.pp out t
| Not u -> Fmt.fprintf out "(@[not@ %a@])" N.pp u
| Eq (a,b) -> Fmt.fprintf out "(@[=@ %a@ %a@])" N.pp a N.pp b
| If (a,b,c) -> Fmt.fprintf out "(@[ite@ %a@ %a@ %a@])" N.pp a N.pp b N.pp c
end
module Sig_tbl = CCHashtbl.Make(Signature)
module T_tbl = CCHashtbl.Make(T)
type combine_task =
| CT_merge of node * node * explanation
type t = {
tst: term_state;
tbl: node T_tbl.t;
(* internalization [term -> node] *)
signatures_tbl : node Sig_tbl.t;
(* map a signature to the corresponding node in some equivalence class.
A signature is a [term_cell] in which every immediate subterm
that participates in the congruence/evaluation relation
is normalized (i.e. is its own representative).
The critical property is that all members of an equivalence class
that have the same "shape" (including head symbol)
have the same signature *)
pending: node Vec.t;
combine: combine_task Vec.t;
undo: (unit -> unit) Backtrack_stack.t;
mutable on_merge: ev_on_merge list;
mutable on_new_term: ev_on_new_term list;
mutable on_conflict: ev_on_conflict list;
mutable on_propagate: ev_on_propagate list;
(* pairs to explain *)
true_ : node lazy_t;
false_ : node lazy_t;
stat: Stat.t;
count_conflict: int Stat.counter;
count_props: int Stat.counter;
count_merge: int Stat.counter;
}
(* TODO: an additional union-find to keep track, for each term,
of the terms they are known to be equal to, according
to the current explanation. That allows not to prove some equality
several times.
See "fast congruence closure and extensions", Nieuwenhis&al, page 14 *)
and ev_on_merge = t -> actions -> N.t -> N.t -> Expl.t -> unit
and ev_on_new_term = t -> N.t -> term -> unit
and ev_on_conflict = t -> lit list -> unit
and ev_on_propagate = t -> lit -> (unit -> lit list) -> unit
let[@inline] size_ (r:repr) = r.n_size
let[@inline] true_ cc = Lazy.force cc.true_
let[@inline] false_ cc = Lazy.force cc.false_
let[@inline] term_state cc = cc.tst
let[@inline] on_backtrack cc f : unit =
Backtrack_stack.push_if_nonzero_level cc.undo f
(* check if [t] is in the congruence closure.
Invariant: [in_cc t do_cc t => forall u subterm t, in_cc u] *)
let[@inline] mem (cc:t) (t:term): bool = T_tbl.mem cc.tbl t
(* non-recursive, inlinable function for [find] *)
let[@inline] find_ (n:node) : repr =
let n2 = n.n_root in
assert (N.is_root n2);
n2
let[@inline] same_class (n1:node)(n2:node): bool =
N.equal (find_ n1) (find_ n2)
let[@inline] find _ n = find_ n
(* print full state *)
let pp_full out (cc:t) : unit =
let pp_next out n =
Fmt.fprintf out "@ :next %a" N.pp n.n_next in
let pp_root out n =
if N.is_root n then Fmt.string out " :is-root" else Fmt.fprintf out "@ :root %a" N.pp n.n_root in
let pp_expl out n = match n.n_expl with
| FL_none -> ()
| FL_some e ->
Fmt.fprintf out " (@[:forest %a :expl %a@])" N.pp e.next Expl.pp e.expl
in
let pp_n out n =
Fmt.fprintf out "(@[%a%a%a%a@])" T.pp n.n_term pp_root n pp_next n pp_expl n
and pp_sig_e out (s,n) =
Fmt.fprintf out "(@[<1>%a@ ~~> %a%a@])" Signature.pp s N.pp n pp_root n
in
Fmt.fprintf out
"(@[@{<yellow>cc.state@}@ (@[<hv>:nodes@ %a@])@ (@[<hv>:sig-tbl@ %a@])@])"
(Util.pp_seq ~sep:" " pp_n) (T_tbl.values cc.tbl)
(Util.pp_seq ~sep:" " pp_sig_e) (Sig_tbl.to_seq cc.signatures_tbl)
(* compute up-to-date signature *)
let update_sig (s:signature) : Signature.t =
View.map_view s
~f_f:(fun x->x)
~f_t:find_
~f_ts:(List.map find_)
(* find whether the given (parent) term corresponds to some signature
in [signatures_] *)
let[@inline] find_signature cc (s:signature) : repr option =
Sig_tbl.get cc.signatures_tbl s
(* add to signature table. Assume it's not present already *)
let add_signature cc (s:signature) (n:node) : unit =
assert (not @@ Sig_tbl.mem cc.signatures_tbl s);
Log.debugf 15
(fun k->k "(@[cc.add-sig@ %a@ ~~> %a@])" Signature.pp s N.pp n);
on_backtrack cc (fun () -> Sig_tbl.remove cc.signatures_tbl s);
Sig_tbl.add cc.signatures_tbl s n
let push_pending cc t : unit =
if not @@ N.get_field field_is_pending t then (
Log.debugf 5 (fun k->k "(@[<hv1>cc.push_pending@ %a@])" N.pp t);
N.set_field field_is_pending true t;
Vec.push cc.pending t
)
let merge_classes cc t u e : unit =
Log.debugf 5
(fun k->k "(@[<hv1>cc.push_combine@ %a ~@ %a@ :expl %a@])"
N.pp t N.pp u Expl.pp e);
Vec.push cc.combine @@ CT_merge (t,u,e)
(* re-root the explanation tree of the equivalence class of [n]
so that it points to [n].
postcondition: [n.n_expl = None] *)
let[@unroll 2] rec reroot_expl (cc:t) (n:node): unit =
begin match n.n_expl with
| FL_none -> () (* already root *)
| FL_some {next=u; expl=e_n_u} ->
(* reroot to [u], then invert link between [u] and [n] *)
reroot_expl cc u;
u.n_expl <- FL_some {next=n; expl=e_n_u};
n.n_expl <- FL_none;
end
let raise_conflict (cc:t) (acts:actions) (e:lit list) : _ =
(* clear tasks queue *)
Vec.iter (N.set_field field_is_pending false) cc.pending;
Vec.clear cc.pending;
Vec.clear cc.combine;
List.iter (fun f -> f cc e) cc.on_conflict;
Stat.incr cc.count_conflict;
CC_A.Actions.raise_conflict acts e A.Proof.default
let[@inline] all_classes cc : repr Iter.t =
T_tbl.values cc.tbl
|> Iter.filter N.is_root
(* find the closest common ancestor of [a] and [b] in the proof forest.
Precond:
- [a] and [b] are in the same class
- no node has the flag [field_marked_explain] on
Invariants:
- if [n] is marked, then all the predecessors of [n]
from [a] or [b] are marked too.
*)
let find_common_ancestor (a:node) (b:node) : node =
(* catch up to the other node *)
let rec find1 a =
if N.get_field field_marked_explain a then a
else (
match a.n_expl with
| FL_none -> assert false
| FL_some r -> find1 r.next
)
in
let rec find2 a b =
if N.equal a b then a
else if N.get_field field_marked_explain a then a
else if N.get_field field_marked_explain b then b
else (
N.set_field field_marked_explain true a;
N.set_field field_marked_explain true b;
match a.n_expl, b.n_expl with
| FL_some r1, FL_some r2 -> find2 r1.next r2.next
| FL_some r, FL_none -> find1 r.next
| FL_none, FL_some r -> find1 r.next
| FL_none, FL_none -> assert false (* no common ancestor *)
)
in
(* cleanup tags on nodes traversed in [find2] *)
let rec cleanup_ n =
if N.get_field field_marked_explain n then (
N.set_field field_marked_explain false n;
match n.n_expl with
| FL_none -> ()
| FL_some {next;_} -> cleanup_ next;
)
in
let n = find2 a b in
cleanup_ a;
cleanup_ b;
n
(* decompose explanation [e] into a list of literals added to [acc] *)
let rec explain_decompose cc (acc:lit list) (e:explanation) : _ list =
Log.debugf 5 (fun k->k "(@[cc.decompose_expl@ %a@])" Expl.pp e);
match e with
| E_reduction -> acc
| E_congruence (n1, n2) ->
begin match n1.n_sig0, n2.n_sig0 with
| Some (App_fun (f1, a1)), Some (App_fun (f2, a2)) ->
assert (Fun.equal f1 f2);
assert (List.length a1 = List.length a2);
List.fold_left2 (explain_pair cc) acc a1 a2
| Some (App_ho (f1, a1)), Some (App_ho (f2, a2)) ->
assert (List.length a1 = List.length a2);
let acc = explain_pair cc acc f1 f2 in
List.fold_left2 (explain_pair cc) acc a1 a2
| Some (If (a1,b1,c1)), Some (If (a2,b2,c2)) ->
let acc = explain_pair cc acc a1 a2 in
let acc = explain_pair cc acc b1 b2 in
explain_pair cc acc c1 c2
| _ ->
assert false
end
| E_lit lit -> lit :: acc
| E_merge (a,b) -> explain_pair cc acc a b
| E_merge_t (a,b) ->
(* find nodes for [a] and [b] on the fly *)
begin match T_tbl.find cc.tbl a, T_tbl.find cc.tbl b with
| a, b -> explain_pair cc acc a b
| exception Not_found ->
Error.errorf "expl: cannot find node(s) for %a, %a" T.pp a T.pp b
end
| E_and (a,b) ->
let acc = explain_decompose cc acc a in
explain_decompose cc acc b
and explain_pair (cc:t) (acc:lit list) (a:node) (b:node) : _ list =
Log.debugf 5
(fun k->k "(@[cc.explain_loop.at@ %a@ =?= %a@])" N.pp a N.pp b);
assert (N.equal (find_ a) (find_ b));
let ancestor = find_common_ancestor a b in
let acc = explain_along_path cc acc a ancestor in
explain_along_path cc acc b ancestor
(* explain why [a = parent_a], where [a -> ... -> target] in the
proof forest *)
and explain_along_path cc acc (a:node) (target:node) : _ list =
let rec aux acc n =
if n == target then acc
else (
match n.n_expl with
| FL_none -> assert false
| FL_some {next=next_n; expl=expl} ->
let acc = explain_decompose cc acc expl in
(* now prove [next_n = target] *)
aux acc next_n
)
in aux acc a
(* add a term *)
let [@inline] rec add_term_rec_ cc t : node =
try T_tbl.find cc.tbl t
with Not_found -> add_new_term_ cc t
(* add [t] to [cc] when not present already *)
and add_new_term_ cc (t:term) : node =
assert (not @@ mem cc t);
Log.debugf 15 (fun k->k "(@[cc.add-term@ %a@])" T.pp t);
let n = N.make t in
(* register sub-terms, add [t] to their parent list, and return the
corresponding initial signature *)
let sig0 = compute_sig0 cc n in
n.n_sig0 <- sig0;
(* remove term when we backtrack *)
on_backtrack cc
(fun () ->
Log.debugf 15 (fun k->k "(@[cc.remove-term@ %a@])" T.pp t);
T_tbl.remove cc.tbl t);
(* add term to the table *)
T_tbl.add cc.tbl t n;
if CCOpt.is_some sig0 then (
(* [n] might be merged with other equiv classes *)
push_pending cc n;
);
List.iter (fun f -> f cc n t) cc.on_new_term;
n
(* compute the initial signature of the given node *)
and compute_sig0 (self:t) (n:node) : Signature.t option =
(* add sub-term to [cc], and register [n] to its parents.
Note that we return the exact sub-term, to get proper
explanations, but we add to the sub-term's root's parent list. *)
let deref_sub (u:term) : node =
let sub = add_term_rec_ self u in
(* add [n] to [sub.root]'s parent list *)
begin
let sub_r = find_ sub in
let old_parents = sub_r.n_parents in
on_backtrack self (fun () -> sub_r.n_parents <- old_parents);
sub_r.n_parents <- Bag.cons n sub_r.n_parents;
end;
sub
in
let[@inline] return x = Some x in
match CC_A.cc_view n.n_term with
| Bool _ | Opaque _ -> None
| Eq (a,b) ->
let a = deref_sub a in
let b = deref_sub b in
return @@ Eq (a,b)
| Not u -> return @@ Not (deref_sub u)
| App_fun (f, args) ->
let args = args |> Iter.map deref_sub |> Iter.to_list in
if args<>[] then (
return @@ App_fun (f, args)
) else None
| App_ho (f, args) ->
let args = args |> Iter.map deref_sub |> Iter.to_list in
return @@ App_ho (deref_sub f, args)
| If (a,b,c) ->
return @@ If (deref_sub a, deref_sub b, deref_sub c)
let[@inline] add_term cc t : node = add_term_rec_ cc t
let set_as_lit cc (n:node) (lit:lit) : unit =
match n.n_as_lit with
| Some _ -> ()
| None ->
Log.debugf 15 (fun k->k "(@[cc.set-as-lit@ %a@ %a@])" N.pp n Lit.pp lit);
on_backtrack cc (fun () -> n.n_as_lit <- None);
n.n_as_lit <- Some lit
let n_is_bool (self:t) n : bool =
N.equal n (true_ self) || N.equal n (false_ self)
(* main CC algo: add terms from [pending] to the signature table,
check for collisions *)
let rec update_tasks (cc:t) (acts:actions) : unit =
while not (Vec.is_empty cc.pending && Vec.is_empty cc.combine) do
while not @@ Vec.is_empty cc.pending do
task_pending_ cc (Vec.pop cc.pending);
done;
while not @@ Vec.is_empty cc.combine do
task_combine_ cc acts (Vec.pop cc.combine);
done;
done
and task_pending_ cc (n:node) : unit =
N.set_field field_is_pending false n;
(* check if some parent collided *)
begin match n.n_sig0 with
| None -> () (* no-op *)
| Some (Eq (a,b)) ->
(* if [a=b] is now true, merge [(a=b)] and [true] *)
if same_class a b then (
let expl = Expl.mk_merge a b in
Log.debugf 5
(fun k->k "(pending.eq@ %a@ :r1 %a@ :r2 %a@])" N.pp n N.pp a N.pp b);
merge_classes cc n (true_ cc) expl
)
| Some (Not u) ->
(* [u = bool ==> not u = not bool] *)
let r_u = find_ u in
if N.equal r_u (true_ cc) then (
let expl = Expl.mk_merge u (true_ cc) in
merge_classes cc n (false_ cc) expl
) else if N.equal r_u (false_ cc) then (
let expl = Expl.mk_merge u (false_ cc) in
merge_classes cc n (true_ cc) expl
)
| Some s0 ->
(* update the signature by using [find] on each sub-node *)
let s = update_sig s0 in
match find_signature cc s with
| None ->
(* add to the signature table [sig(n) --> n] *)
add_signature cc s n
| Some u when N.equal n u -> ()
| Some u ->
(* [t1] and [t2] must be applications of the same symbol to
arguments that are pairwise equal *)
assert (n != u);
let expl = Expl.mk_congruence n u in
merge_classes cc n u expl
end
and[@inline] task_combine_ cc acts = function
| CT_merge (a,b,e_ab) -> task_merge_ cc acts a b e_ab
(* main CC algo: merge equivalence classes in [st.combine].
@raise Exn_unsat if merge fails *)
and task_merge_ cc acts a b e_ab : unit =
let ra = find_ a in
let rb = find_ b in
if not @@ N.equal ra rb then (
assert (N.is_root ra);
assert (N.is_root rb);
Stat.incr cc.count_merge;
(* check we're not merging [true] and [false] *)
if (N.equal ra (true_ cc) && N.equal rb (false_ cc)) ||
(N.equal rb (true_ cc) && N.equal ra (false_ cc)) then (
Log.debugf 5
(fun k->k "(@[<hv>cc.merge.true_false_conflict@ \
@[:r1 %a@ :t1 %a@]@ @[:r2 %a@ :t2 %a@]@ :e_ab %a@])"
N.pp ra N.pp a N.pp rb N.pp b Expl.pp e_ab);
let lits = explain_decompose cc [] e_ab in
let lits = explain_pair cc lits a ra in
let lits = explain_pair cc lits b rb in
raise_conflict cc acts (List.rev_map Lit.neg lits)
);
(* We will merge [r_from] into [r_into].
we try to ensure that [size ra <= size rb] in general, but always
keep values as representative *)
let r_from, r_into =
if n_is_bool cc ra then rb, ra
else if n_is_bool cc rb then ra, rb
else if size_ ra > size_ rb then rb, ra
else ra, rb
in
(* when merging terms with [true] or [false], possibly propagate them to SAT *)
let merge_bool r1 t1 r2 t2 =
if N.equal r1 (true_ cc) then (
propagate_bools cc acts r2 t2 r1 t1 e_ab true
) else if N.equal r1 (false_ cc) then (
propagate_bools cc acts r2 t2 r1 t1 e_ab false
)
in
merge_bool ra a rb b;
merge_bool rb b ra a;
(* perform [union r_from r_into] *)
Log.debugf 15 (fun k->k "(@[cc.merge@ :from %a@ :into %a@])" N.pp r_from N.pp r_into);
(* call [on_merge] functions, and merge theory data items *)
begin
(* explanation is [a=ra & e_ab & b=rb] *)
let expl = Expl.mk_list [e_ab; Expl.mk_merge a ra; Expl.mk_merge b rb] in
List.iter (fun f -> f cc acts r_into r_from expl) cc.on_merge;
end;
begin
(* parents might have a different signature, check for collisions *)
N.iter_parents r_from
(fun parent -> push_pending cc parent);
(* for each node in [r_from]'s class, make it point to [r_into] *)
N.iter_class r_from
(fun u ->
assert (u.n_root == r_from);
u.n_root <- r_into);
(* capture current state *)
let r_into_old_next = r_into.n_next in
let r_from_old_next = r_from.n_next in
let r_into_old_parents = r_into.n_parents in
(* swap [into.next] and [from.next], merging the classes *)
r_into.n_next <- r_from_old_next;
r_from.n_next <- r_into_old_next;
r_into.n_parents <- Bag.append r_into.n_parents r_from.n_parents;
r_into.n_size <- r_into.n_size + r_from.n_size;
(* on backtrack, unmerge classes and restore the pointers to [r_from] *)
on_backtrack cc
(fun () ->
Log.debugf 15
(fun k->k "(@[cc.undo_merge@ :from %a :into %a@])"
N.pp r_from N.pp r_into);
r_into.n_next <- r_into_old_next;
r_from.n_next <- r_from_old_next;
r_into.n_parents <- r_into_old_parents;
(* NOTE: this must come after the restoration of [next] pointers,
otherwise we'd iterate on too big a class *)
N.iter_class_ r_from (fun u -> u.n_root <- r_from);
r_into.n_size <- r_into.n_size - r_from.n_size;
);
end;
(* update explanations (a -> b), arbitrarily.
Note that here we merge the classes by adding a bridge between [a]
and [b], not their roots. *)
begin
reroot_expl cc a;
assert (a.n_expl = FL_none);
(* on backtracking, link may be inverted, but we delete the one
that bridges between [a] and [b] *)
on_backtrack cc
(fun () -> match a.n_expl, b.n_expl with
| FL_some e, _ when N.equal e.next b -> a.n_expl <- FL_none
| _, FL_some e when N.equal e.next a -> b.n_expl <- FL_none
| _ -> assert false);
a.n_expl <- FL_some {next=b; expl=e_ab};
end;
)
(* we are merging [r1] with [r2==Bool(sign)], so propagate each term [u1]
in the equiv class of [r1] that is a known literal back to the SAT solver
and which is not the one initially merged.
We can explain the propagation with [u1 = t1 =e= t2 = r2==bool] *)
and propagate_bools cc acts r1 t1 r2 t2 (e_12:explanation) sign : unit =
(* explanation for [t1 =e= t2 = r2] *)
let half_expl = lazy (
let lits = explain_decompose cc [] e_12 in
explain_pair cc lits r2 t2
) in
(* TODO: flag per class, `or`-ed on merge, to indicate if the class
contains at least one lit *)
N.iter_class r1
(fun u1 ->
(* propagate if:
- [u1] is a proper literal
- [t2 != r2], because that can only happen
after an explicit merge (no way to obtain that by propagation)
*)
match N.as_lit u1 with
| Some lit when not (N.equal r2 t2) ->
let lit = if sign then lit else Lit.neg lit in (* apply sign *)
Log.debugf 5 (fun k->k "(@[cc.bool_propagate@ %a@])" Lit.pp lit);
(* complete explanation with the [u1=t1] chunk *)
let reason =
let e = lazy (explain_pair cc (Lazy.force half_expl) u1 t1) in
fun () -> Lazy.force e
in
List.iter (fun f -> f cc lit reason) cc.on_propagate;
Stat.incr cc.count_props;
CC_A.Actions.propagate acts lit ~reason CC_A.A.Proof.default
| _ -> ())
let check_invariants_ (cc:t) =
Log.debug 5 "(cc.check-invariants)";
Log.debugf 15 (fun k-> k "%a" pp_full cc);
assert (T.equal (T.bool cc.tst true) (true_ cc).n_term);
assert (T.equal (T.bool cc.tst false) (false_ cc).n_term);
assert (not @@ same_class (true_ cc) (false_ cc));
assert (Vec.is_empty cc.combine);
assert (Vec.is_empty cc.pending);
(* check that subterms are internalized *)
T_tbl.iter
(fun t n ->
assert (T.equal t n.n_term);
assert (not @@ N.get_field field_is_pending n);
assert (N.equal n.n_root n.n_next.n_root);
(* check proper signature.
note that some signatures in the sig table can be obsolete (they
were not removed) but there must be a valid, up-to-date signature for
each term *)
begin match CCOpt.map update_sig n.n_sig0 with
| None -> ()
| Some s ->
Log.debugf 15 (fun k->k "(@[cc.check-sig@ %a@ :sig %a@])" T.pp t Signature.pp s);
(* add, but only if not present already *)
begin match Sig_tbl.find cc.signatures_tbl s with
| exception Not_found -> assert false
| repr_s -> assert (same_class n repr_s)
end
end;
)
cc.tbl;
()
module Debug_ = struct
let[@inline] check_invariants (cc:t) : unit =
if Util._CHECK_INVARIANTS then check_invariants_ cc
let pp out _ = Fmt.string out "cc"
end
let add_seq cc seq =
seq (fun t -> ignore @@ add_term_rec_ cc t);
()
let[@inline] push_level (self:t) : unit =
Backtrack_stack.push_level self.undo
let pop_levels (self:t) n : unit =
Vec.iter (N.set_field field_is_pending false) self.pending;
Vec.clear self.pending;
Vec.clear self.combine;
Log.debugf 15
(fun k->k "(@[cc.pop-levels %d@ :n-lvls %d@])" n (Backtrack_stack.n_levels self.undo));
Backtrack_stack.pop_levels self.undo n ~f:(fun f -> f());
()
(* TODO:
CC.set_as_lit cc n (Lit.abs lit);
*)
(* assert that this boolean literal holds.
if a lit is [= a b], merge [a] and [b];
otherwise merge the atom with true/false *)
let assert_lit cc lit : unit =
let t = Lit.term lit in
Log.debugf 5 (fun k->k "(@[cc.assert_lit@ %a@])" Lit.pp lit);
let sign = Lit.sign lit in
begin match CC_A.cc_view t with
| Eq (a,b) when sign ->
let a = add_term cc a in
let b = add_term cc b in
(* merge [a] and [b] *)
merge_classes cc a b (Expl.mk_lit lit)
| _ ->
(* equate t and true/false *)
let rhs = if sign then true_ cc else false_ cc in
let n = add_term cc t in
(* TODO: ensure that this is O(1).
basically, just have [n] point to true/false and thus acquire
the corresponding value, so its superterms (like [ite]) can evaluate
properly *)
(* TODO: use oriented merge (force direction [n -> rhs]) *)
merge_classes cc n rhs (Expl.mk_lit lit)
end
let[@inline] assert_lits cc lits : unit =
Iter.iter (assert_lit cc) lits
(* raise a conflict *)
let raise_conflict_from_expl cc (acts:actions) expl =
Log.debugf 5
(fun k->k "(@[cc.theory.raise-conflict@ :expl %a@])" Expl.pp expl);
let lits = explain_decompose cc [] expl in
let lits = List.rev_map Lit.neg lits in
raise_conflict cc acts lits
let merge cc n1 n2 expl =
Log.debugf 5
(fun k->k "(@[cc.theory.merge@ :n1 %a@ :n2 %a@ :expl %a@])" N.pp n1 N.pp n2 Expl.pp expl);
merge_classes cc n1 n2 expl
let on_merge cc f = cc.on_merge <- f :: cc.on_merge
let on_new_term cc f = cc.on_new_term <- f :: cc.on_new_term
let on_conflict cc f = cc.on_conflict <- f :: cc.on_conflict
let on_propagate cc f = cc.on_propagate <- f :: cc.on_propagate
let create ?(stat=Stat.global)
?(on_merge=[]) ?(on_new_term=[]) ?(on_conflict=[]) ?(on_propagate=[])
?(size=`Big)
(tst:term_state) : t =
let size = match size with `Small -> 128 | `Big -> 2048 in
let rec cc = {
tst;
tbl = T_tbl.create size;
signatures_tbl = Sig_tbl.create size;
on_merge;
on_new_term;
on_conflict;
on_propagate;
pending=Vec.create();
combine=Vec.create();
undo=Backtrack_stack.create();
true_;
false_;
stat;
count_conflict=Stat.mk_int stat "cc.conflicts";
count_props=Stat.mk_int stat "cc.propagations";
count_merge=Stat.mk_int stat "cc.merges";
} and true_ = lazy (
add_term cc (T.bool tst true)
) and false_ = lazy (
add_term cc (T.bool tst false)
)
in
ignore (Lazy.force true_ : node);
ignore (Lazy.force false_ : node);
cc
let[@inline] find_t cc t : repr =
let n = T_tbl.find cc.tbl t in
find_ n
let[@inline] check cc acts : unit =
Log.debug 5 "(cc.check)";
update_tasks cc acts
(* model: return all the classes *)
let get_model (cc:t) : repr Iter.t Iter.t =
all_classes cc |> Iter.map N.iter_class
end

6
src/cc/Sidekick_cc.mli Normal file
View file

@ -0,0 +1,6 @@
(** {2 Congruence Closure} *)
module type ARG = Sidekick_core.CC_ARG
module type S = Sidekick_core.CC_S
module Make(CC_A: ARG) : S with module CC_A = CC_A

View file

@ -3,8 +3,5 @@
(library
(name Sidekick_cc)
(public_name sidekick.cc)
(libraries containers containers.data msat iter sidekick.util)
(flags :standard -warn-error -a+8
-color always -safe-string -short-paths -open Sidekick_util)
(ocamlopt_flags :standard -O3 -color always
-unbox-closures -unbox-closures-factor 20))
(libraries containers containers.data iter sidekick.core sidekick.util)
(flags :standard -open Sidekick_util))

623
src/core/Sidekick_core.ml Normal file
View file

@ -0,0 +1,623 @@
(** {1 Main Environment}
Theories and concrete solvers rely on an environment that defines
several important types:
- sorts
- terms (to represent logic expressions and formulas)
- a congruence closure instance
*)
module Fmt = CCFormat
module type MERGE_PP = sig
type t
val merge : t -> t -> t
val pp : t Fmt.printer
end
module CC_view = struct
type ('f, 't, 'ts) t =
| Bool of bool
| App_fun of 'f * 'ts
| App_ho of 't * 'ts
| If of 't * 't * 't
| Eq of 't * 't
| Not of 't
| Opaque of 't (* do not enter *)
let map_view ~f_f ~f_t ~f_ts (v:_ t) : _ t =
match v with
| Bool b -> Bool b
| App_fun (f, args) -> App_fun (f_f f, f_ts args)
| App_ho (f, args) -> App_ho (f_t f, f_ts args)
| Not t -> Not (f_t t)
| If (a,b,c) -> If (f_t a, f_t b, f_t c)
| Eq (a,b) -> Eq (f_t a, f_t b)
| Opaque t -> Opaque (f_t t)
let iter_view ~f_f ~f_t ~f_ts (v:_ t) : unit =
match v with
| Bool _ -> ()
| App_fun (f, args) -> f_f f; f_ts args
| App_ho (f, args) -> f_t f; f_ts args
| Not t -> f_t t
| If (a,b,c) -> f_t a; f_t b; f_t c;
| Eq (a,b) -> f_t a; f_t b
| Opaque t -> f_t t
end
module type TERM = sig
module Fun : sig
type t
val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
end
module Ty : sig
type t
val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
val bool : t
val is_bool : t -> bool
end
module Term : sig
type t
val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
type state
val ty : t -> Ty.t
val bool : state -> bool -> t (* build true/false *)
val as_bool : t -> bool option
val map_shallow : state -> (t -> t) -> t -> t
(** Map function on immediate subterms *)
val iter_dag : t -> (t -> unit) -> unit
module Tbl : CCHashtbl.S with type key = t
end
end
module type TERM_LIT = sig
include TERM
module Lit : sig
type t
val neg : t -> t
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pp : t Fmt.printer
val term : t -> Term.t
val sign : t -> bool
val abs : t -> t
val apply_sign : t -> bool -> t
val norm_sign : t -> t * bool
(** Invariant: if [u, sign = norm_sign t] then [apply_sign u sign = t] *)
val atom : Term.state -> ?sign:bool -> Term.t -> t
end
end
module type TERM_LIT_PROOF = sig
include TERM_LIT
module Proof : sig
type t
val pp : t Fmt.printer
val default : t
(* TODO: to give more details? or make this extensible?
or have a generative function for new proof cstors?
val cc_lemma : unit -> t
*)
end
end
module type CC_ARG = sig
module A : TERM_LIT_PROOF
val cc_view : A.Term.t -> (A.Fun.t, A.Term.t, A.Term.t Iter.t) CC_view.t
(** View the term through the lens of the congruence closure *)
module Actions : sig
type t
val raise_conflict : t -> A.Lit.t list -> A.Proof.t -> 'a
val propagate : t -> A.Lit.t -> reason:(unit -> A.Lit.t list) -> A.Proof.t -> unit
end
end
module type CC_S = sig
module CC_A : CC_ARG
module A = CC_A.A
type term_state = A.Term.state
type term = A.Term.t
type fun_ = A.Fun.t
type lit = A.Lit.t
type proof = A.Proof.t
type actions = CC_A.Actions.t
type t
(** Global state of the congruence closure *)
(** An equivalence class is a set of terms that are currently equal
in the partial model built by the solver.
The class is represented by a collection of nodes, one of which is
distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored
in this representative's node.
When two classes become equal (are "merged"), one of the two
representatives is picked as the representative of the new class.
The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the
representative. This information can be used when two classes are
merged, to detect conflicts and solve equations à la Shostak.
*)
module N : sig
type t
val term : t -> term
val equal : t -> t -> bool
val hash : t -> int
val pp : t Fmt.printer
val is_root : t -> bool
(** Is the node a root (ie the representative of its class)? *)
val iter_class : t -> t Iter.t
(** Traverse the congruence class.
Precondition: [is_root n] (see {!find} below) *)
val iter_parents : t -> t Iter.t
(** Traverse the parents of the class.
Precondition: [is_root n] (see {!find} below) *)
end
module Expl : sig
type t
val pp : t Fmt.printer
val mk_merge : N.t -> N.t -> t
val mk_merge_t : term -> term -> t
val mk_lit : lit -> t
val mk_list : t list -> t
end
type node = N.t
(** A node of the congruence closure *)
type repr = N.t
(** Node that is currently a representative *)
type explanation = Expl.t
(** Accessors *)
val term_state : t -> term_state
val find : t -> node -> repr
(** Current representative *)
val add_term : t -> term -> node
(** Add the term to the congruence closure, if not present already.
Will be backtracked. *)
type ev_on_merge = t -> actions -> N.t -> N.t -> Expl.t -> unit
type ev_on_new_term = t -> N.t -> term -> unit
type ev_on_conflict = t -> lit list -> unit
type ev_on_propagate = t -> lit -> (unit -> lit list) -> unit
val create :
?stat:Stat.t ->
?on_merge:ev_on_merge list ->
?on_new_term:ev_on_new_term list ->
?on_conflict:ev_on_conflict list ->
?on_propagate:ev_on_propagate list ->
?size:[`Small | `Big] ->
term_state ->
t
(** Create a new congruence closure. *)
(* TODO: remove? this is managed by the solver anyway? *)
val on_merge : t -> ev_on_merge -> unit
(** Add a function to be called when two classes are merged *)
val on_new_term : t -> ev_on_new_term -> unit
(** Add a function to be called when a new node is created *)
val on_conflict : t -> ev_on_conflict -> unit
(** Called when the congruence closure finds a conflict *)
val on_propagate : t -> ev_on_propagate -> unit
(** Called when the congruence closure propagates a literal *)
val set_as_lit : t -> N.t -> lit -> unit
(** map the given node to a literal. *)
val find_t : t -> term -> repr
(** Current representative of the term.
@raise Not_found if the term is not already {!add}-ed. *)
val add_seq : t -> term Iter.t -> unit
(** Add a sequence of terms to the congruence closure *)
val all_classes : t -> repr Iter.t
(** All current classes. This is costly, only use if there is no other solution *)
val assert_lit : t -> lit -> unit
(** Given a literal, assume it in the congruence closure and propagate
its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor *)
val assert_lits : t -> lit Iter.t -> unit
(** Addition of many literals *)
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'a
(** Raise a conflict with the given explanation
it must be a theory tautology that [expl ==> absurd].
To be used in theories. *)
val merge : t -> N.t -> N.t -> Expl.t -> unit
(** Merge these two nodes given this explanation.
It must be a theory tautology that [expl ==> n1 = n2].
To be used in theories. *)
val check : t -> actions -> unit
(** Perform all pending operations done via {!assert_eq}, {!assert_lit}, etc.
Will use the {!actions} to propagate literals, declare conflicts, etc. *)
val push_level : t -> unit
(** Push backtracking level *)
val pop_levels : t -> int -> unit
(** Restore to state [n] calls to [push_level] earlier. Used during backtracking. *)
val get_model : t -> N.t Iter.t Iter.t
(** get all the equivalence classes so they can be merged in the model *)
(**/**)
module Debug_ : sig
val check_invariants : t -> unit
val pp : t Fmt.printer
end
(**/**)
end
(** A view of the solver from a theory's point of view *)
module type SOLVER_INTERNAL = sig
module A : TERM_LIT_PROOF
module CC_A : CC_ARG with module A = A
module CC : CC_S with module CC_A = CC_A
type ty = A.Ty.t
type lit = A.Lit.t
type term = A.Term.t
type term_state = A.Term.state
type proof = A.Proof.t
(** {3 Main type for a solver} *)
type t
type solver = t
module Expl = CC.Expl
module N = CC.N
val tst : t -> term_state
val cc : t -> CC.t
(** Congruence closure for this solver *)
(** {3 Simplifiers} *)
module Simplify : sig
type t
val tst : t -> term_state
val clear : t -> unit
(** Reset internal cache, etc. *)
type hook = t -> term -> term option
(** Given a term, try to simplify it. Return [None] if it didn't change.
Can also add clauses to the simplifier. *)
val normalize : t -> term -> term
(** Normalize a term using all the hooks. *)
end
type simplify_hook = Simplify.hook
val add_simplifier : t -> Simplify.hook -> unit
val simplifier : t -> Simplify.t
val simp_t : t -> term -> term
(** {3 hooks for the theory} *)
type actions
val propagate : t -> actions -> lit -> reason:(unit -> lit list) -> A.Proof.t -> unit
val raise_conflict : t -> actions -> lit list -> A.Proof.t -> 'a
(** Give a conflict clause to the solver *)
val propagate: t -> actions -> lit -> (unit -> lit list) -> unit
(** Propagate a boolean using a unit clause.
[expl => lit] must be a theory lemma, that is, a T-tautology *)
val propagate_l: t -> actions -> lit -> lit list -> unit
(** Propagate a boolean using a unit clause.
[expl => lit] must be a theory lemma, that is, a T-tautology *)
val add_clause_temp : t -> actions -> lit list -> unit
(** Add local clause to the SAT solver. This clause will be
removed when the solver backtracks. *)
val add_clause_permanent : t -> actions -> lit list -> unit
(** Add toplevel clause to the SAT solver. This clause will
not be backtracked. *)
val mk_lit : t -> actions -> ?sign:bool -> term -> lit
(** Create a literal *)
val add_lit : t -> actions -> lit -> unit
(** Add the given literal to the SAT solver, so it gets assigned
a boolean value *)
val add_lit_t : t -> actions -> ?sign:bool -> term -> unit
(** Add the given (signed) bool term to the SAT solver, so it gets assigned
a boolean value *)
val cc_raise_conflict_expl : t -> actions -> Expl.t -> 'a
(** Raise a conflict with the given congruence closure explanation.
it must be a theory tautology that [expl ==> absurd].
To be used in theories. *)
val cc_find : t -> N.t -> N.t
(** Find representative of the node *)
val cc_merge : t -> actions -> N.t -> N.t -> Expl.t -> unit
(** Merge these two nodes in the congruence closure, given this explanation.
It must be a theory tautology that [expl ==> n1 = n2].
To be used in theories. *)
val cc_merge_t : t -> actions -> term -> term -> Expl.t -> unit
(** Merge these two terms in the congruence closure, given this explanation.
See {!cc_merge} *)
val cc_add_term : t -> term -> N.t
(** Add/retrieve congruence closure node for this term.
To be used in theories *)
val on_cc_merge : t -> (CC.t -> actions -> N.t -> N.t -> Expl.t -> unit) -> unit
(** Callback for when two classes containing data for this key are merged *)
val on_cc_new_term : t -> (CC.t -> N.t -> term -> unit) -> unit
(** Callback to add data on terms when they are added to the congruence
closure *)
val on_cc_conflict : t -> (CC.t -> lit list -> unit) -> unit
(** Callback called on every CC conflict *)
val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list) -> unit) -> unit
(** Callback called on every CC propagation *)
val on_partial_check : t -> (t -> actions -> lit Iter.t -> unit) -> unit
(** Register callbacked to be called with the slice of literals
newly added on the trail.
This is called very often and should be efficient. It doesn't have
to be complete, only correct. It's given only the slice of
the trail consisting in new literals. *)
val on_final_check: t -> (t -> actions -> lit Iter.t -> unit) -> unit
(** Register callback to be called during the final check.
Must be complete (i.e. must raise a conflict if the set of literals is
not satisfiable) and can be expensive. The function
is given the whole trail. *)
(** {3 Preprocessors}
These preprocessors turn mixed, raw literals (possibly simplified) into
literals suitable for reasoning.
Typically some clauses are also added to the solver. *)
type preprocess_hook = t -> add_clause:(lit list -> unit) -> term -> term option
(** Given a term, try to preprocess it. Return [None] if it didn't change.
Can also add clauses to define new terms. *)
val add_preprocess : t -> preprocess_hook -> unit
end
(** Public view of the solver *)
module type SOLVER = sig
module A : TERM_LIT_PROOF
module CC_A : CC_ARG with module A = A
module Solver_internal : SOLVER_INTERNAL with module A = A and module CC_A = CC_A
(** Internal solver, available to theories. *)
type t
type solver = t
type term = A.Term.t
type ty = A.Ty.t
type lit = A.Lit.t
type lemma = A.Proof.t
(** {3 A theory}
Theories are abstracted over the concrete implementation of the solver,
so they can work with any implementation.
Typically a theory should be a functor taking an argument containing
a [SOLVER_INTERNAL] and some additional views on terms, literals, etc.
that are specific to the theory (e.g. to map terms to linear
expressions).
The theory can then be instantiated on any kind of solver for any
term representation that also satisfies the additional theory-specific
requirements. Instantiated theories (ie values of type {!SOLVER.theory})
can be added to the solver.
*)
module type THEORY = sig
type t
(** The theory's state *)
val name : string
(** Name of the theory *)
val create_and_setup : Solver_internal.t -> t
(** Instantiate the theory's state for the given (internal) solver,
register callbacks, create keys, etc. *)
val push_level : t -> unit
(** Push backtracking level *)
val pop_levels : t -> int -> unit
(** Pop backtracking levels, restoring the theory to its former state *)
end
type theory = (module THEORY)
(** A theory that can be used for this particular solver. *)
val mk_theory :
name:string ->
create_and_setup:(Solver_internal.t -> 'th) ->
?push_level:('th -> unit) ->
?pop_levels:('th -> int -> unit) ->
unit ->
theory
(** Helper to create a theory *)
(** {3 Boolean Atoms} *)
module Atom : sig
type t
val equal : t -> t -> bool
val hash : t -> int
val pp : t CCFormat.printer
end
(** {3 Semantic values} *)
module Value : sig
type t
val equal : t -> t -> bool
val hash : t -> int
val ty : t -> ty
val pp : t Fmt.printer
end
module Model : sig
type t
val empty : t
val mem : term -> t -> bool
val find : term -> t -> Value.t option
val eval : t -> term -> Value.t option
val pp : t Fmt.printer
end
module Unknown : sig
type t
val pp : t CCFormat.printer
(*
type unknown =
| U_timeout
| U_incomplete
*)
end
module Proof : sig
type t
val check : t -> unit
val pp_dot : t Fmt.printer
end
type proof = Proof.t
(** {3 Main API} *)
val stats : t -> Stat.t
val tst : t -> A.Term.state
val create :
?stat:Stat.t ->
?size:[`Big | `Tiny | `Small] ->
(* TODO? ?config:Config.t -> *)
?store_proof:bool ->
theories:theory list ->
A.Term.state ->
unit ->
t
(** Create a new solver.
@param theories theories to load from the start. *)
val add_theory : t -> theory -> unit
(** Add a theory to the solver. This should be called before
any call to {!solve} or to {!add_clause} and the likes (otherwise
the theory will have a partial view of the problem). *)
val mk_atom_lit : t -> lit -> Atom.t
val mk_atom_t : t -> ?sign:bool -> term -> Atom.t
val add_clause_lits : t -> lit IArray.t -> unit
val add_clause_lits_l : t -> lit list -> unit
val add_clause : t -> Atom.t IArray.t -> unit
val add_clause_l : t -> Atom.t list -> unit
type res =
| Sat of Model.t
| Unsat of {
proof: proof option;
unsat_core: Atom.t list lazy_t;
}
| Unknown of Unknown.t
(** Result of solving for the current set of clauses *)
val solve :
?on_exit:(unit -> unit) list ->
?check:bool ->
assumptions:Atom.t list ->
t ->
res
(** [solve s] checks the satisfiability of the statement added so far to [s]
@param check if true, the model is checked before returning
@param assumptions a set of atoms held to be true. The unsat core,
if any, will be a subset of [assumptions].
@param on_exit functions to be run before this returns *)
val pp_term_graph: t CCFormat.printer
val pp_stats : t CCFormat.printer
(**/**)
module Debug_ : sig
val check_invariants : t -> unit
end
(**/**)
end

6
src/core/dune Normal file
View file

@ -0,0 +1,6 @@
(library
(name Sidekick_core)
(public_name sidekick.core)
(flags :standard -open Sidekick_util)
(libraries containers iter sidekick.util))

View file

@ -1,22 +0,0 @@
(* Copyright 2005 INRIA *)
{
open Sidekick_util
open Parser
}
let number = ['1' - '9'] ['0' - '9']*
rule token = parse
| eof { EOF }
| "c" { comment lexbuf }
| [' ' '\t' '\r'] { token lexbuf }
| 'p' { P }
| "cnf" { CNF }
| '\n' { Lexing.new_line lexbuf; token lexbuf }
| '0' { ZERO }
| '-'? number { LIT (int_of_string (Lexing.lexeme lexbuf)) }
| _ { Error.errorf "dimacs.lexer: unexpected char `%s`" (Lexing.lexeme lexbuf) }
and comment = parse
| '\n' { Lexing.new_line lexbuf; token lexbuf }
| [^'\n'] { comment lexbuf }

View file

@ -1,43 +0,0 @@
/* Copyright 2005 INRIA */
%{
open Sidekick_util
let lnum pos = pos.Lexing.pos_lnum
let cnum pos = pos.Lexing.pos_cnum - pos.Lexing.pos_bol
let pp_pos out (start,stop) =
Format.fprintf out "(at %d:%d - %d:%d)"
(lnum start) (cnum start) (lnum stop) (cnum stop)
%}
%token <int> LIT
%token ZERO
%token P CNF EOF
%start file
%type <int list list> file
%%
/* DIMACS syntax */
prelude:
| P CNF LIT LIT { () }
| error
{
Error.errorf "expected prelude %a" pp_pos ($startpos,$endpos)
}
clauses:
| l=clause* { l }
| error
{
Error.errorf "expected list of clauses %a"
pp_pos ($startpos,$endpos)
}
file:
| prelude l=clauses EOF { l }
clause:
| l=LIT+ ZERO { l }

View file

@ -1,15 +0,0 @@
(** {1 Main for dimacs} *)
type 'a or_error = ('a, string) CCResult.t
let parse file : int list list or_error =
try
CCIO.with_in file
(fun ic ->
let lexbuf = Lexing.from_channel ic in
Parser.file Lexer.token lexbuf)
|> CCResult.return
with e ->
CCResult.of_exn_trace e

View file

@ -1,13 +0,0 @@
(** {1 Main for dimacs} *)
(** This library provides a parser for DIMACS files, to represent
SAT problems.
http://www.satcompetition.org/2009/format-benchmarks2009.html
*)
type 'a or_error = ('a, string) CCResult.t
val parse : string -> int list list or_error
(** Parse a file into a list of clauses. *)

View file

@ -1,14 +0,0 @@
; main binary
(library
(name sidekick_dimacs)
(public_name sidekick.dimacs)
(optional) ; only if deps present
(libraries containers sidekick.util)
(flags :standard -w +a-4-42-44-48-50-58-32-60@8)
(ocamlopt_flags :standard -O3 -color always -bin-annot
-unbox-closures -unbox-closures-factor 20)
)
(menhir (modules Parser))
(ocamllex (modules Lexer))

View file

@ -1,14 +1,12 @@
; main binary
(executable
(name main)
(public_name sidekick)
(package sidekick)
(libraries containers iter result msat sidekick.smt sidekick.smtlib
sidekick.smt.th-ite sidekick.dimacs)
(flags :standard -w +a-4-42-44-48-50-58-32-60@8
-safe-string -color always -open Sidekick_util)
(ocamlopt_flags :standard -O3 -color always
-unbox-closures -unbox-closures-factor 20)
)
(executable
(name main)
(public_name sidekick)
(package sidekick)
(libraries containers iter result msat sidekick.core sidekick.base-term
sidekick.msat-solver sidekick.smtlib)
(flags :standard -w +a-4-42-44-48-50-58-32-60@8 -safe-string -color always
-open Sidekick_util)
(ocamlopt_flags :standard -O3 -color always -unbox-closures
-unbox-closures-factor 20))

View file

@ -8,9 +8,9 @@ open CCResult.Infix
module E = CCResult
module Fmt = CCFormat
module Term = Sidekick_smt.Term
module Ast = Sidekick_smt.Ast
module Solver = Sidekick_smt.Solver
module Term = Sidekick_base_term.Term
module Ast = Sidekick_smtlib.Ast
module Solver = Sidekick_smtlib.Solver
module Process = Sidekick_smtlib.Process
module Vec = Msat.Vec
@ -24,7 +24,7 @@ let p_cnf = ref false
let p_dot_proof = ref ""
let p_proof_print = ref false
let p_model = ref false
let check = ref true
let check = ref false
let time_limit = ref 300.
let size_limit = ref 1000_000_000.
let restarts = ref true
@ -62,34 +62,26 @@ let input_file = fun s -> file := s
let usage = "Usage : main [options] <file>"
let argspec = Arg.align [
"-bt", Arg.Unit (fun () -> Printexc.record_backtrace true), " enable stack traces";
"-cnf", Arg.Set p_cnf, " prints the cnf used.";
"-check", Arg.Set check, " build, check and print the proof (if output is set), if unsat";
"-no-check", Arg.Clear check, " inverse of -check";
"-gc", Arg.Set gc, " enable garbage collection";
"-no-gc", Arg.Clear gc, " disable garbage collection";
"-restarts", Arg.Set restarts, " enable restarts";
"-no-restarts", Arg.Clear restarts, " disable restarts";
"-dot", Arg.Set_string p_dot_proof, " if provided, print the dot proof in the given file";
"-stat", Arg.Set p_stat, " print statistics";
"-model", Arg.Set p_model, " print model";
"-no-model", Arg.Clear p_model, " do not print model";
"-gc-stat", Arg.Set p_gc_stat, " outputs statistics about the GC";
"--bt", Arg.Unit (fun () -> Printexc.record_backtrace true), " enable stack traces";
"--cnf", Arg.Set p_cnf, " prints the cnf used.";
"--check", Arg.Set check, " build, check and print the proof (if output is set), if unsat";
"--no-check", Arg.Clear check, " inverse of -check";
"--gc", Arg.Set gc, " enable garbage collection";
"--no-gc", Arg.Clear gc, " disable garbage collection";
"--restarts", Arg.Set restarts, " enable restarts";
"--no-restarts", Arg.Clear restarts, " disable restarts";
"--dot", Arg.Set_string p_dot_proof, " if provided, print the dot proof in the given file";
"--stat", Arg.Set p_stat, " print statistics";
"--model", Arg.Set p_model, " print model";
"--no-model", Arg.Clear p_model, " do not print model";
"--gc-stat", Arg.Set p_gc_stat, " outputs statistics about the GC";
"-p", Arg.Set p_progress, " print progress bar";
"-no-p", Arg.Clear p_progress, " no progress bar";
"-size", Arg.String (int_arg size_limit), " <s>[kMGT] sets the size limit for the sat solver";
"-time", Arg.String (int_arg time_limit), " <t>[smhd] sets the time limit for the sat solver";
"-v", Arg.Int Sidekick_smt.Log.set_debug, "<lvl> sets the debug verbose level";
"--no-p", Arg.Clear p_progress, " no progress bar";
"--size", Arg.String (int_arg size_limit), " <s>[kMGT] sets the size limit for the sat solver";
"--time", Arg.String (int_arg time_limit), " <t>[smhd] sets the time limit for the sat solver";
"-v", Arg.Int Msat.Log.set_debug, "<lvl> sets the debug verbose level";
]
type syntax =
| Dimacs
| Smtlib
let syntax_of_file file =
if CCString.suffix ~suf:".cnf" file then Dimacs
else Smtlib
(* Limits alarm *)
let check_limits () =
let t = Sys.time () in
@ -109,33 +101,21 @@ let main () =
exit 2
);
let al = Gc.create_alarm check_limits in
let syn = syntax_of_file !file in
Util.setup_gc();
let tst = Term.create ~size:4_096 () in
let solver =
let theories = match syn with
| Dimacs ->
(* TODO: eager CNF conversion *)
[Sidekick_th_bool.th_dynamic_tseitin]
| Smtlib ->
[ Sidekick_th_bool.th_dynamic_tseitin;
Sidekick_th_distinct.th;
Sidekick_th_ite.th;
] (* TODO: more theories *)
let theories = [
Process.th_bool ;
] (* TODO: more theories *)
in
Sidekick_smt.Solver.create ~store_proof:!check ~theories ()
Process.Solver.create ~store_proof:!check ~theories tst ()
in
if !check then (
(* might have to check conflicts *)
Solver.add_theory solver Process.Check_cc.theory;
);
let dot_proof = if !p_dot_proof = "" then None else Some !p_dot_proof in
begin match syn with
| Smtlib ->
(* parse pb *)
Sidekick_smtlib.parse !file
| Dimacs ->
Sidekick_dimacs.parse !file >|= fun cs ->
List.rev_append
(List.rev_map (fun c -> Ast.Assert_bool c) cs)
[Ast.CheckSat]
end
>>= fun input ->
Sidekick_smtlib.parse !file >>= fun input ->
(* process statements *)
let res =
try

View file

@ -1,9 +1,10 @@
module CC_view = Sidekick_core.CC_view
type res =
| Sat
| Unsat
module type ARG = sig
include Sidekick_core.TERM
module type TERM = CC_types.TERM
val cc_view : Term.t -> (Fun.t, Term.t, Term.t Iter.t) CC_view.t
end
module type S = sig
type term
@ -17,12 +18,13 @@ module type S = sig
val add_lit : t -> term -> bool -> unit
val distinct : t -> term list -> unit
val check : t -> res
val check_sat : t -> bool
val classes : t -> term Iter.t Iter.t
end
module Make(A: TERM) = struct
open CC_types
module Make(A: ARG) = struct
open CC_view
module Fun = A.Fun
module T = A.Term
@ -35,28 +37,29 @@ module Make(A: TERM) = struct
type node = {
n_t: term;
mutable n_next: node; (* next in class *)
mutable n_size: int; (* size of parent list *)
mutable n_size: int; (* size of class *)
mutable n_parents: node list;
mutable n_root: node;
mutable n_root: node; (* root of the class *)
}
type signature = (fun_, node, node list) view
type signature = (fun_, node, node list) CC_view.t
module Node = struct
type t = node
let[@inline] equal (n1:t) n2 = T.equal n1.n_t n2.n_t
let[@inline] hash (n:t) = T.hash n.n_t
let[@inline] size (n:t) = n.n_size
let[@inline] is_root n = n == n.n_root
let[@inline] root n = n.n_root
let[@inline] term n = n.n_t
let pp out n = T.pp out n.n_t
let add_parent (self:t) ~p : unit =
self.n_parents <- p :: self.n_parents;
self.n_size <- 1 + self.n_size;
()
self.n_parents <- p :: self.n_parents
let make (t:T.t) : t =
let rec n = {
n_t=t; n_size=0; n_next=n;
n_t=t; n_size=1; n_next=n;
n_parents=[]; n_root=n;
} in
n
@ -145,7 +148,7 @@ module Make(A: TERM) = struct
self
let sub_ t k : unit =
match T.cc_view t with
match A.cc_view t with
| Bool _ | Opaque _ -> ()
| App_fun (_, args) -> args k
| App_ho (f, args) -> k f; args k
@ -158,28 +161,19 @@ module Make(A: TERM) = struct
| n -> n
| exception Not_found ->
let node = Node.make t in
T_tbl.add self.tbl t node;
(* add sub-terms, and add [t] to their parent list *)
sub_ t
(fun u ->
let n_u = add_t self u in
let n_u = Node.root @@ add_t self u in
Node.add_parent n_u ~p:node);
T_tbl.add self.tbl t node;
(* need to compute signature *)
Vec.push self.pending node;
node
(* find representative *)
let[@inline] find_ (n:node) : node =
let r = n.n_root in
assert (Node.equal r.n_root r);
r
let find_t_ (self:t) (t:term): node =
let n =
try T_tbl.find self.tbl t
with Not_found -> Error.errorf "minicc.find_t: no node for %a" T.pp t
in
find_ n
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 =
@ -191,13 +185,13 @@ module Make(A: TERM) = struct
let check_distinct_ self : unit =
Vec.iter
(fun r ->
r := List.map find_ !r;
r := List.rev_map Node.root !r;
if has_dups !r then raise_notrace E_unsat)
self.distinct
let compute_sig (self:t) (n:node) : Signature.t option =
let[@inline] return x = Some x in
match T.cc_view n.n_t with
match A.cc_view n.n_t with
| Bool _ | Opaque _ -> None
| Eq (a,b) ->
let a = find_t_ self a in
@ -223,17 +217,17 @@ module Make(A: TERM) = struct
(* reduce to [true] *)
let n2 = self.true_ in
Log.debugf 5
(fun k->k "(@[minicc.congruence-by-eq@ %a@ %a@])" Node.pp n Node.pp n2);
(fun k->k "(@[mini-cc.congruence-by-eq@ %a@ %a@])" Node.pp n Node.pp n2);
Vec.push self.combine (n,n2)
)
| Some s ->
Log.debugf 5 (fun k->k "(@[minicc.update-sig@ %a@])" Signature.pp s);
Log.debugf 5 (fun k->k "(@[mini-cc.update-sig@ %a@])" Signature.pp s);
match Sig_tbl.find self.sig_tbl s with
| n2 when Node.equal n n2 -> ()
| n2 ->
(* collision, merge *)
Log.debugf 5
(fun k->k "(@[minicc.congruence-by-sig@ %a@ %a@])" Node.pp n Node.pp n2);
(fun k->k "(@[mini-cc.congruence-by-sig@ %a@ %a@])" Node.pp n Node.pp n2);
Vec.push self.combine (n,n2)
| exception Not_found ->
Sig_tbl.add self.sig_tbl s n
@ -242,8 +236,8 @@ module Make(A: TERM) = struct
(* merge the two classes *)
let merge_ self (n1,n2) : unit =
let n1 = find_ n1 in
let n2 = find_ n2 in
let n1 = Node.root n1 in
let n2 = Node.root n2 in
if not @@ Node.equal n1 n2 then (
(* merge into largest class, or into a boolean *)
let n1, n2 =
@ -251,10 +245,10 @@ module Make(A: TERM) = struct
else if is_bool self n2 then n2, n1
else if Node.size n1 > Node.size n2 then n1, n2
else n2, n1 in
Log.debugf 5 (fun k->k "(@[minicc.merge@ :into %a@ %a@])" Node.pp n1 Node.pp n2);
Log.debugf 5 (fun k->k "(@[mini-cc.merge@ :into %a@ %a@])" Node.pp n1 Node.pp n2);
if is_bool self n1 && is_bool self n2 then (
Log.debugf 5 (fun k->k "(minicc.conflict.merge-true-false)");
Log.debugf 5 (fun k->k "(mini-cc.conflict.merge-true-false)");
self.ok <- false;
raise E_unsat
);
@ -267,9 +261,14 @@ module Make(A: TERM) = struct
(* update root pointer in [n2.class] *)
Node.iter_cls n2 (fun n -> n.n_root <- n1);
(* merge classes [next] pointers *)
let n1_next = n1.n_next in
n1.n_next <- n2.n_next;
n2.n_next <- n1_next;
)
let check_ok_ self =
let[@inline] check_ok_ self =
if not self.ok then raise_notrace E_unsat
(* fixpoint of the congruence closure *)
@ -288,7 +287,7 @@ module Make(A: TERM) = struct
(* API *)
let add_lit (self:t) (p:T.t) (sign:bool) : unit =
match T.cc_view p with
match A.cc_view p with
| Eq (t1,t2) when sign ->
let n1 = add_t self t1 in
let n2 = add_t self t2 in
@ -300,17 +299,22 @@ module Make(A: TERM) = struct
Vec.push self.combine (n,n2)
let distinct (self:t) l =
begin match l with
| [] | [_] -> invalid_arg "distinct: need at least 2 terms"
| _ -> ()
end;
let l = List.map (add_t self) l in
Vec.push self.distinct (ref l)
match l with
| [] | [_] -> () (* trivial *)
| _ ->
let l = List.rev_map (add_t self) l in
Vec.push self.distinct (ref l)
let check (self:t) : res =
try fixpoint self; Sat
let check_sat (self:t) : bool =
try fixpoint self; true
with E_unsat ->
self.ok <- false;
Unsat
false
let classes self : _ Iter.t =
T_tbl.values self.tbl
|> Iter.filter Node.is_root
|> Iter.map
(fun n -> Node.iter_cls n |> Iter.map Node.term)
end

View file

@ -1,4 +1,3 @@
(** {1 Mini congruence closure}
This implementation is as simple as possible, and doesn't provide
@ -6,11 +5,13 @@
It just decides the satisfiability of a set of (dis)equations.
*)
type res =
| Sat
| Unsat
module CC_view = Sidekick_core.CC_view
module type TERM = CC_types.TERM
module type ARG = sig
include Sidekick_core.TERM
val cc_view : Term.t -> (Fun.t, Term.t, Term.t Iter.t) CC_view.t
end
module type S = sig
type term
@ -27,10 +28,16 @@ module type S = sig
val distinct : t -> term list -> unit
(** [distinct cc l] asserts that all terms in [l] are distinct *)
val check : t -> res
val check_sat : t -> bool
(** [check_sat cc] returns [true] if the current state is satisfiable, [false]
if it's unsatisfiable *)
val classes : t -> term Iter.t Iter.t
(** Traverse the set of classes in the congruence closure.
This should be called only if {!check} returned [Sat]. *)
end
module Make(A: TERM)
module Make(A: ARG)
: S with type term = A.Term.t
and type fun_ = A.Fun.t
and type term_state = A.Term.state

7
src/mini-cc/dune Normal file
View file

@ -0,0 +1,7 @@
(library
(name Sidekick_mini_cc)
(public_name sidekick.mini-cc)
(libraries containers iter sidekick.core sidekick.util)
(flags :standard -open Sidekick_util))

View file

@ -0,0 +1,567 @@
(** {1 Implementation of a Solver using Msat} *)
module Vec = Msat.Vec
module Log = Msat.Log
module IM = Util.Int_map
module type ARG = sig
include Sidekick_core.TERM_LIT_PROOF
val cc_view : Term.t -> (Fun.t, Term.t, Term.t Iter.t) Sidekick_core.CC_view.t
end
module type S = Sidekick_core.SOLVER
module Make(A : ARG)
: S with module A = A
= struct
module A = A
module T = A.Term
module Lit = A.Lit
module Ty = A.Ty
type lit = Lit.t
type term = T.t
type ty = Ty.t
type lemma = A.Proof.t
(* actions from msat *)
type msat_acts = (Msat.void, Lit.t, Msat.void, A.Proof.t) Msat.acts
(* the full argument to the congruence closure *)
module CC_A = struct
module A = A
let cc_view = A.cc_view
module Actions = struct
type t = msat_acts
let[@inline] raise_conflict a lits pr =
a.Msat.acts_raise_conflict lits pr
let[@inline] propagate a lit ~reason pr =
let reason = Msat.Consequence (fun () -> reason(), pr) in
a.Msat.acts_propagate lit reason
end
end
module CC = Sidekick_cc.Make(CC_A)
module Expl = CC.Expl
module N = CC.N
(** Internal solver, given to theories and to Msat *)
module Solver_internal = struct
module A = A
module CC_A = CC_A
module CC = CC
module N = CC.N
type term = T.t
type ty = Ty.t
type lit = Lit.t
type term_state = T.state
type th_states =
| Ths_nil
| Ths_cons : {
st: 'a;
push_level: 'a -> unit;
pop_levels: 'a -> int -> unit;
next: th_states;
} -> th_states
type actions = msat_acts
module Simplify = struct
type t = {
tst: term_state;
mutable hooks: hook list;
cache: T.t T.Tbl.t;
}
and hook = t -> term -> term option
let create tst : t = {tst; hooks=[]; cache=T.Tbl.create 32;}
let[@inline] tst self = self.tst
let add_hook self f = self.hooks <- f :: self.hooks
let clear self = T.Tbl.clear self.cache
let normalize (self:t) (t:T.t) : T.t =
(* compute and cache normal form of [t] *)
let rec aux t =
match T.Tbl.find self.cache t with
| u -> u
| exception Not_found ->
let u = aux_rec t self.hooks in
T.Tbl.add self.cache t u;
u
(* try each function in [hooks] successively, and rewrite subterms *)
and aux_rec t hooks = match hooks with
| [] ->
let u = T.map_shallow self.tst aux t in
if T.equal t u then t else aux u
| h :: hooks_tl ->
match h self t with
| None -> aux_rec t hooks_tl
| Some u when T.equal t u -> aux_rec t hooks_tl
| Some u -> aux u
in
aux t
end
type simplify_hook = Simplify.hook
type t = {
tst: T.state; (** state for managing terms *)
cc: CC.t lazy_t; (** congruence closure *)
stat: Stat.t;
count_axiom: int Stat.counter;
count_preprocess_clause: int Stat.counter;
count_conflict: int Stat.counter;
count_propagate: int Stat.counter;
simp: Simplify.t;
mutable preprocess: preprocess_hook list;
preprocess_cache: T.t T.Tbl.t;
mutable th_states : th_states; (** Set of theories *)
mutable on_partial_check: (t -> actions -> lit Iter.t -> unit) list;
mutable on_final_check: (t -> actions -> lit Iter.t -> unit) list;
}
and preprocess_hook = t -> add_clause:(lit list -> unit) -> term -> term option
type solver = t
module Formula = struct
include Lit
let norm lit =
let lit', sign = norm_sign lit in
lit', if sign then Msat.Same_sign else Msat.Negated
end
module Eq_class = CC.N
module Expl = CC.Expl
type proof = A.Proof.t
let[@inline] cc (t:t) = Lazy.force t.cc
let[@inline] tst t = t.tst
let simplifier self = self.simp
let simp_t self (t:T.t) : T.t = Simplify.normalize self.simp t
let add_simplifier (self:t) f : unit = Simplify.add_hook self.simp f
let add_preprocess self f = self.preprocess <- f :: self.preprocess
let[@inline] raise_conflict self acts c : 'a =
Stat.incr self.count_conflict;
acts.Msat.acts_raise_conflict c A.Proof.default
let[@inline] propagate self acts p cs : unit =
Stat.incr self.count_propagate;
acts.Msat.acts_propagate p (Msat.Consequence (fun () -> cs(), A.Proof.default))
let[@inline] propagate_l self acts p cs : unit =
propagate self acts p (fun()->cs)
let add_sat_clause_ self acts ~keep lits : unit =
Stat.incr self.count_axiom;
acts.Msat.acts_add_clause ~keep lits A.Proof.default
let preprocess_lit_ (self:t) ~add_clause (lit:lit) : lit =
(* compute and cache normal form of [t] *)
let rec aux t =
match T.Tbl.find self.preprocess_cache t with
| u -> u
| exception Not_found ->
(* first, map subterms *)
let u = T.map_shallow self.tst aux t in
(* then rewrite *)
let u = aux_rec u self.preprocess in
T.Tbl.add self.preprocess_cache t u;
u
(* try each function in [hooks] successively *)
and aux_rec t hooks = match hooks with
| [] -> t
| h :: hooks_tl ->
match h self ~add_clause t with
| None -> aux_rec t hooks_tl
| Some u ->
Log.debugf 30
(fun k->k "(@[msat-solver.preprocess.step@ :from %a@ :to %a@])"
T.pp t T.pp u);
aux u
in
let t = Lit.term lit |> simp_t self |> aux in
let lit' = Lit.atom self.tst ~sign:(Lit.sign lit) t in
Log.debugf 10
(fun k->k "(@[msat-solver.preprocess@ :lit %a@ :into %a@])" Lit.pp lit Lit.pp lit');
lit'
let[@inline] mk_lit self acts ?sign t =
let add_clause lits =
Stat.incr self.count_preprocess_clause;
add_sat_clause_ self acts ~keep:true lits
in
preprocess_lit_ self ~add_clause @@ Lit.atom self.tst ?sign t
let[@inline] add_clause_temp self acts lits : unit =
add_sat_clause_ self acts ~keep:false lits
let[@inline] add_clause_permanent self acts lits : unit =
add_sat_clause_ self acts ~keep:true lits
let add_lit _self acts lit : unit = acts.Msat.acts_mk_lit lit
let add_lit_t self acts ?sign t = add_lit self acts (mk_lit self acts ?sign t)
let on_final_check self f = self.on_final_check <- f :: self.on_final_check
let on_partial_check self f = self.on_partial_check <- f :: self.on_partial_check
let on_cc_new_term self f = CC.on_new_term (cc self) f
let on_cc_merge self f = CC.on_merge (cc self) f
let on_cc_conflict self f = CC.on_conflict (cc self) f
let on_cc_propagate self f = CC.on_propagate (cc self) f
let cc_add_term self t = CC.add_term (cc self) t
let cc_find self n = CC.find (cc self) n
let cc_merge self _acts n1 n2 e = CC.merge (cc self) n1 n2 e
let cc_merge_t self acts t1 t2 e =
cc_merge self acts (cc_add_term self t1) (cc_add_term self t2) e
let cc_raise_conflict_expl self acts e =
CC.raise_conflict_from_expl (cc self) acts e
(** {2 Interface with the SAT solver} *)
let rec push_lvl_ = function
| Ths_nil -> ()
| Ths_cons r -> r.push_level r.st; push_lvl_ r.next
let rec pop_lvls_ n = function
| Ths_nil -> ()
| Ths_cons r -> r.pop_levels r.st n; pop_lvls_ n r.next
let push_level (self:t) : unit =
CC.push_level (cc self);
push_lvl_ self.th_states
let pop_levels (self:t) n : unit =
CC.pop_levels (cc self) n;
pop_lvls_ n self.th_states
(* handle a literal assumed by the SAT solver *)
let assert_lits_ ~final (self:t) (acts:actions) (lits:Lit.t Iter.t) : unit =
Msat.Log.debugf 2
(fun k->k "(@[<hv1>@{<green>msat-solver.assume_lits@}%s@ %a@])"
(if final then "[final]" else "") (Util.pp_seq ~sep:"; " Lit.pp) lits);
(* transmit to CC *)
let cc = cc self in
if not final then (
CC.assert_lits cc lits;
);
(* transmit to theories. *)
CC.check cc acts;
if final then (
List.iter (fun f -> f self acts lits) self.on_final_check;
) else (
List.iter (fun f -> f self acts lits) self.on_partial_check;
);
()
let[@inline] iter_atoms_ acts : _ Iter.t =
fun f ->
acts.Msat.acts_iter_assumptions
(function
| Msat.Lit a -> f a
| Msat.Assign _ -> assert false)
(* propagation from the bool solver *)
let check_ ~final (self:t) (acts: msat_acts) =
let iter = iter_atoms_ acts in
(* TODO if Config.progress then print_progress(); *)
Msat.Log.debugf 5 (fun k->k "(msat-solver.assume :len %d)" (Iter.length iter));
assert_lits_ ~final self acts iter
(* propagation from the bool solver *)
let[@inline] partial_check (self:t) (acts:_ Msat.acts) : unit =
check_ ~final:false self acts
(* perform final check of the model *)
let[@inline] final_check (self:t) (acts:_ Msat.acts) : unit =
check_ ~final:true self acts
(* TODO
let mk_model (self:t) lits : Model.t =
let m =
Iter.fold
(fun m (Th_state ((module Th),st)) -> Th.mk_model st lits m)
Model.empty (theories self)
in
(* now complete model using CC *)
CC.mk_model (cc self) m
*)
let create ~stat (tst:A.Term.state) () : t =
let rec self = {
tst;
cc = lazy (
(* lazily tie the knot *)
CC.create ~size:`Big self.tst;
);
th_states=Ths_nil;
stat;
simp=Simplify.create tst;
preprocess=[];
preprocess_cache=T.Tbl.create 32;
count_axiom = Stat.mk_int stat "solver.th-axioms";
count_preprocess_clause = Stat.mk_int stat "solver.preprocess-clause";
count_propagate = Stat.mk_int stat "solver.th-propagations";
count_conflict = Stat.mk_int stat "solver.th-conflicts";
on_partial_check=[];
on_final_check=[];
} in
ignore (Lazy.force @@ self.cc : CC.t);
self
end
(** the parametrized SAT Solver *)
module Sat_solver = Msat.Make_cdcl_t(Solver_internal)
let[@inline] clause_of_mclause (c:Sat_solver.clause): Lit.t IArray.t =
Sat_solver.Clause.atoms c |> Array.map Sat_solver.Atom.formula |> IArray.of_array_unsafe
module Atom = Sat_solver.Atom
module Proof = struct
include Sat_solver.Proof
module Dot = Msat_backend.Dot.Make(Sat_solver)(Msat_backend.Dot.Default(Sat_solver))
let pp_dot = Dot.pp
end
type proof = Proof.t
(* main solver state *)
type t = {
si: Solver_internal.t;
solver: Sat_solver.t;
stat: Stat.t;
count_clause: int Stat.counter;
count_solve: int Stat.counter;
(* config: Config.t *)
}
type solver = t
module type THEORY = sig
type t
val name : string
val create_and_setup : Solver_internal.t -> t
val push_level : t -> unit
val pop_levels : t -> int -> unit
end
type theory = (module THEORY)
(** {2 Main} *)
let add_theory (self:t) (th:theory) : unit =
let (module Th) = th in
Log.debugf 2
(fun k-> k "(@[msat-solver.add-theory@ :name %S@])" Th.name);
let st = Th.create_and_setup self.si in
(* add push/pop to the internal solver *)
begin
let open Solver_internal in
self.si.th_states <- Ths_cons {
st;
push_level=Th.push_level;
pop_levels=Th.pop_levels;
next=self.si.th_states;
};
end;
()
let add_theory_l self = List.iter (add_theory self)
(* create a new solver *)
let create ?(stat=Stat.global) ?size ?store_proof ~theories tst () : t =
Log.debug 5 "msat-solver.create";
let si = Solver_internal.create ~stat tst () in
let self = {
si;
solver=Sat_solver.create ?store_proof ?size si;
stat;
count_clause=Stat.mk_int stat "solver.add-clause";
count_solve=Stat.mk_int stat "solver.solve";
} in
add_theory_l self theories;
(* assert [true] and [not false] *)
begin
let tst = Solver_internal.tst self.si in
Sat_solver.assume self.solver [
[Lit.atom tst @@ T.bool tst true];
] A.Proof.default;
end;
self
module Debug_ = struct
let check_invariants (self:t) =
if Util._CHECK_INVARIANTS then (
CC.Debug_.check_invariants (Solver_internal.cc self.si);
)
end
let[@inline] solver self = self.solver
let[@inline] cc self = Solver_internal.cc self.si
let stats self = self.stat
let[@inline] tst self = Solver_internal.tst self.si
let[@inline] mk_atom_lit_ self lit : Atom.t = Sat_solver.make_atom self.solver lit
let mk_atom_t_ self t : Atom.t =
let lit = Lit.atom (tst self) t in
mk_atom_lit_ self lit
(* map boolean subterms to literals *)
let add_bool_subterms_ (self:t) (t:T.t) : unit =
T.iter_dag t
|> Iter.filter (fun t -> Ty.is_bool @@ T.ty t)
|> Iter.filter
(fun t -> match A.cc_view t with
| Sidekick_core.CC_view.Not _ -> false (* will process the subterm just later *)
| _ -> true)
|> Iter.iter
(fun sub ->
Log.debugf 5 (fun k->k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" T.pp sub);
ignore (mk_atom_t_ self sub : Sat_solver.atom))
let rec mk_atom_lit self lit : Atom.t =
let lit =
Solver_internal.preprocess_lit_
~add_clause:(fun lits ->
(* recursively add these sub-literals, so they're also properly processed *)
Stat.incr self.si.count_preprocess_clause;
let atoms = List.map (mk_atom_lit self) lits in
Sat_solver.add_clause self.solver atoms A.Proof.default)
self.si lit in
add_bool_subterms_ self (Lit.term lit);
Sat_solver.make_atom self.solver lit
let[@inline] mk_atom_t self ?sign t : Atom.t =
let lit = Lit.atom (tst self) ?sign t in
mk_atom_lit self lit
(** {2 Result} *)
module Unknown = struct
type t =
| U_timeout
| U_max_depth
| U_incomplete
let pp out = function
| U_timeout -> Fmt.string out "timeout"
| U_max_depth -> Fmt.string out "max depth reached"
| U_incomplete -> Fmt.string out "incomplete fragment"
end [@@ocaml.warning "-37"]
(* TODO *)
module Value = struct
type t = unit
let equal _ _ = true
let hash _ = 0
let ty _ = Ty.bool
let pp out _ = Fmt.string out "<value>"
end
(* TODO *)
module Model = struct
type t = unit
let empty = ()
let mem _ _ = false
let find _ _ = None
let eval _ _ = None
let pp out _ = Fmt.string out "<model>"
end
(* TODO
type model = A.Model.t
let pp_model = Model.pp
*)
type res =
| Sat of Model.t
| Unsat of {
proof: proof option;
unsat_core: Atom.t list lazy_t;
}
| Unknown of Unknown.t
(** Result of solving for the current set of clauses *)
(** {2 Main} *)
(* print all terms reachable from watched literals *)
let pp_term_graph _out (_:t) =
() (* TODO *)
let pp_stats out (self:t) : unit =
Stat.pp_all out (Stat.all @@ stats self)
let add_clause (self:t) (c:Atom.t IArray.t) : unit =
Stat.incr self.count_clause;
Sat_solver.add_clause_a self.solver (c:> Atom.t array) A.Proof.default
let add_clause_l self c = add_clause self (IArray.of_list c)
let add_clause_lits (self:t) (c:Lit.t IArray.t) : unit =
let c = IArray.map (mk_atom_lit self) c in
add_clause self c
let add_clause_lits_l (self:t) (c:Lit.t list) : unit =
add_clause self (IArray.of_list_map (mk_atom_lit self) c)
(* TODO: remove? use a special constant + micro theory instead?
let[@inline] assume_distinct self l ~neq lit : unit =
CC.assert_distinct (cc self) l lit ~neq
*)
let check_model (_s:t) : unit =
Log.debug 1 "(smt.solver.check-model)";
(* TODO
Sat_solver.check_model s.solver
*)
()
let solve ?(on_exit=[]) ?(check=true) ~assumptions (self:t) : res =
let do_on_exit () =
List.iter (fun f->f()) on_exit;
in
let r = Sat_solver.solve ~assumptions (solver self) in
Stat.incr self.count_solve;
match r with
| Sat_solver.Sat st ->
Log.debugf 1 (fun k->k "SAT");
let _lits f = st.iter_trail f (fun _ -> ()) in
let m =
Model.empty (* TODO Theory_combine.mk_model (th_combine self) lits *)
in
do_on_exit ();
Sat m
(*
let env = Ast.env_empty in
let m = Model.make ~env in
Unknown U_incomplete (* TODO *)
*)
| Sat_solver.Unsat us ->
let proof =
try
let pr = us.get_proof () in
if check then Sat_solver.Proof.check pr;
Some pr
with Msat.Solver_intf.No_proof -> None
in
let unsat_core = lazy (us.Msat.unsat_assumptions ()) in
do_on_exit ();
Unsat {proof; unsat_core}
let mk_theory (type st)
~name ~create_and_setup
?(push_level=fun _ -> ()) ?(pop_levels=fun _ _ -> ())
() : theory =
let module Th = struct
type t = st
let name = name
let create_and_setup = create_and_setup
let push_level = push_level
let pop_levels = pop_levels
end in
(module Th : THEORY)
end

6
src/msat-solver/dune Normal file
View file

@ -0,0 +1,6 @@
(library
(name Sidekick_msat_solver)
(public_name sidekick.msat-solver)
(libraries containers containers.data iter sidekick.core sidekick.util
sidekick.cc msat msat.backend)
(flags :standard -open Sidekick_util))

View file

@ -0,0 +1,145 @@
module type S = sig
type ('term,'lit,'a) t
(** An access key for theories which have per-class data ['a] *)
val create :
?pp:'a Fmt.printer ->
name:string ->
eq:('a -> 'a -> bool) ->
merge:('a -> 'a -> 'a) ->
unit ->
('term,'lit,'a) t
(** Generative creation of keys for the given theory data.
@param eq : Equality. This is used to optimize backtracking info.
@param merge :
[merge d1 d2] is called when merging classes with data [d1] and [d2]
respectively. The theory should already have checked that the merge
is compatible, and this produces the combined data for terms in the
merged class.
@param name name of the theory which owns this data
@param pp a printer for the data
*)
val equal : ('t,'lit,_) t -> ('t,'lit,_) t -> bool
(** Checks if two keys are equal (generatively) *)
val pp : _ t Fmt.printer
(** Prints the name of the key. *)
end
(** Custom keys for theory data.
This imitates the classic tricks for heterogeneous maps
https://blog.janestreet.com/a-universal-type/
It needs to form a commutative monoid where values are persistent so
they can be restored during backtracking.
*)
module Key = struct
module type KEY_IMPL = sig
type term
type lit
type t
val id : int
val name : string
val pp : t Fmt.printer
val equal : t -> t -> bool
val merge : t -> t -> t
exception Store of t
end
type ('term,'lit,'a) t =
(module KEY_IMPL with type term = 'term and type lit = 'lit and type t = 'a)
let n_ = ref 0
let create (type term)(type lit)(type d)
?(pp=fun out _ -> Fmt.string out "<opaque>")
~name ~eq ~merge () : (term,lit,d) t =
let module K = struct
type nonrec term = term
type nonrec lit = lit
type t = d
let id = !n_
let name = name
let pp = pp
let merge = merge
let equal = eq
exception Store of d
end in
incr n_;
(module K)
let[@inline] id
: type term lit a. (term,lit,a) t -> int
= fun (module K) -> K.id
let[@inline] equal
: type term lit a b. (term,lit,a) t -> (term,lit,b) t -> bool
= fun (module K1) (module K2) -> K1.id = K2.id
let pp
: type term lit a. (term,lit,a) t Fmt.printer
= fun out (module K) -> Fmt.string out K.name
end
(*
(** Map for theory data associated with representatives *)
module K_map = struct
type 'a key = (term,lit,'a) Key.t
type pair = Pair : 'a key * exn -> pair
type t = pair IM.t
let empty = IM.empty
let[@inline] mem k t = IM.mem (Key.id k) t
let find (type a) (k : a key) (self:t) : a option =
let (module K) = k in
match IM.find K.id self with
| Pair (_, K.Store v) -> Some v
| _ -> None
| exception Not_found -> None
let add (type a) (k : a key) (v:a) (self:t) : t =
let (module K) = k in
IM.add K.id (Pair (k, K.Store v)) self
let remove (type a) (k: a key) self : t =
let (module K) = k in
IM.remove K.id self
let equal (m1:t) (m2:t) : bool =
IM.equal
(fun p1 p2 ->
let Pair ((module K1), v1) = p1 in
let Pair ((module K2), v2) = p2 in
assert (K1.id = K2.id);
match v1, v2 with K1.Store v1, K1.Store v2 -> K1.equal v1 v2 | _ -> false)
m1 m2
let merge ~f_both (m1:t) (m2:t) : t =
IM.merge
(fun _ p1 p2 ->
match p1, p2 with
| None, None -> None
| Some v, None
| None, Some v -> Some v
| Some (Pair ((module K1) as key1, pair1)), Some (Pair (_, pair2)) ->
match pair1, pair2 with
| K1.Store v1, K1.Store v2 ->
f_both K1.id pair1 pair2; (* callback for checking compat *)
let v12 = K1.merge v1 v2 in (* merge content *)
Some (Pair (key1, K1.Store v12))
| _ -> assert false
)
m1 m2
end
*)

View file

@ -1,18 +0,0 @@
module Arg = struct
module Fun = Cst
module Term = Term
module Lit = Lit
module Value = Value
module Ty = Ty
module Model = Model
module Proof = struct
type t = Solver_types.proof
let pp = Solver_types.pp_proof
let default = Solver_types.Proof_default
end
end
include Sidekick_cc.Make(Arg)
module Mini_cc = Sidekick_cc.Mini_cc.Make(Arg)

View file

@ -1,14 +0,0 @@
include Sidekick_cc.S
with type term = Term.t
and type model = Model.t
and type lit = Lit.t
and type fun_ = Cst.t
and type term_state = Term.state
and type proof = Solver_types.proof
and module Key = Sidekick_cc.Key
module Mini_cc : Sidekick_cc.Mini_cc.S
with type term = Term.t
and type fun_ = Cst.t
and type term_state = Term.state

View file

@ -1,41 +0,0 @@
open Solver_types
type view = cst_view
type t = cst
let[@inline] id t = t.cst_id
let[@inline] view t = t.cst_view
let[@inline] make cst_id cst_view = {cst_id; cst_view}
let as_undefined (c:t) = match view c with
| Cst_undef ty -> Some (c,ty)
| Cst_def _ -> None
let[@inline] is_undefined c = match view c with Cst_undef _ -> true | _ -> false
let as_undefined_exn (c:t) = match as_undefined c with
| Some tup -> tup
| None -> assert false
let[@inline] mk_undef id ty = make id (Cst_undef ty)
let[@inline] mk_undef_const id ty = mk_undef id (Ty.Fun.mk [] ty)
let[@inline] do_cc (c:t) : bool = match view c with
| Cst_undef _ -> true
| Cst_def {do_cc;_} -> do_cc
let equal a b = ID.equal a.cst_id b.cst_id
let compare a b = ID.compare a.cst_id b.cst_id
let hash t = ID.hash t.cst_id
let pp out a = ID.pp out a.cst_id
module Map = CCMap.Make(struct
type t = cst
let compare = compare
end)
module Tbl = CCHashtbl.Make(struct
type t = cst
let equal = equal
let hash = hash
end)

View file

@ -1,22 +0,0 @@
open Solver_types
type view = cst_view
type t = cst
val id : t -> ID.t
val view : t -> view
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val as_undefined : t -> (t * Ty.Fun.t) option
val as_undefined_exn : t -> t * Ty.Fun.t
val is_undefined : t -> bool
val do_cc : t -> bool
val mk_undef : ID.t -> Ty.Fun.t -> t
val mk_undef_const : ID.t -> Ty.t -> t
val pp : t Fmt.printer
module Map : CCMap.S with type key = t
module Tbl : CCHashtbl.S with type key = t

View file

@ -1,34 +0,0 @@
open Solver_types
type t = lit = {
lit_term: term;
lit_sign : bool
}
let[@inline] neg l = {l with lit_sign=not l.lit_sign}
let[@inline] sign t = t.lit_sign
let[@inline] term (t:t): term = t.lit_term
let[@inline] abs t: t = {t with lit_sign=true}
let make ~sign t = {lit_sign=sign; lit_term=t}
let atom tst ?(sign=true) (t:term) : t =
let t, sign' = Term.abs tst t in
let sign = if not sign' then not sign else sign in
make ~sign t
let[@inline] as_atom (lit:t) = lit.lit_term, lit.lit_sign
let hash = hash_lit
let compare = cmp_lit
let[@inline] equal a b = compare a b = 0
let pp = pp_lit
let print = pp
let norm l =
if l.lit_sign then l, Msat.Solver_intf.Same_sign else neg l, Msat.Solver_intf.Negated
module Set = CCSet.Make(struct type t = lit let compare=compare end)
module Tbl = CCHashtbl.Make(struct type t = lit let equal=equal let hash=hash end)

View file

@ -1,24 +0,0 @@
(** {2 Literals} *)
open Solver_types
type t = lit = {
lit_term: term;
lit_sign : bool
}
val neg : t -> t
val abs : t -> t
val sign : t -> bool
val term : t -> term
val as_atom : t -> term * bool
val atom : Term.state -> ?sign:bool -> term -> t
val hash : t -> int
val compare : t -> t -> int
val equal : t -> t -> bool
val print : t Fmt.printer
val pp : t Fmt.printer
val norm : t -> t * Msat.Solver_intf.negated
module Set : CCSet.S with type elt = t
module Tbl : CCHashtbl.S with type key = t

View file

@ -1,25 +0,0 @@
module ID = ID
module Ty_card = Ty_card
module Cst = Cst
module Stat = Stat
module Model = Model
module Ast = Ast
module Term = Term
module Value = Value
module Term_cell = Term_cell
module Ty = Ty
module Lit = Lit
module Theory_combine = Theory_combine
module Theory = Theory
module Solver = Solver
module CC = CC
module Solver_types = Solver_types
type theory = Theory.t
(**/**)
module Vec = Msat.Vec
module Log = Msat.Log
(**/**)

View file

@ -1,279 +0,0 @@
(* This file is free software. See file "license" for more details. *)
(** {1 Main Solver} *)
[@@@warning "-32"]
open Solver_types
let get_time : unit -> float = Sys.time
(** {2 The Main Solver} *)
module Sat_solver = Msat.Make_cdcl_t(Theory_combine)
let[@inline] clause_of_mclause (c:Sat_solver.clause): Lit.t IArray.t =
Sat_solver.Clause.atoms c |> Array.map Sat_solver.Atom.formula |> IArray.of_array_unsafe
module Atom = Sat_solver.Atom
module Proof = Sat_solver.Proof
(* main solver state *)
type t = {
solver: Sat_solver.t;
stat: Stat.t;
count_clause: int Stat.counter;
count_solve: int Stat.counter;
config: Config.t
}
let[@inline] solver self = self.solver
let[@inline] th_combine (self:t) : Theory_combine.t = Sat_solver.theory self.solver
let[@inline] add_theory self th = Theory_combine.add_theory (th_combine self) th
let[@inline] cc self = Theory_combine.cc (th_combine self)
let stats self = self.stat
let[@inline] tst self = Theory_combine.tst (th_combine self)
let[@inline] mk_atom_lit self lit : Atom.t = Sat_solver.make_atom self.solver lit
let[@inline] mk_atom_t self ?sign t : Atom.t =
let lit = Lit.atom (tst self) ?sign t in
mk_atom_lit self lit
let create ?(stat=Stat.global) ?size ?(config=Config.empty) ?store_proof ~theories () : t =
let th_combine = Theory_combine.create ~stat () in
let self = {
solver=Sat_solver.create ?store_proof ?size th_combine;
stat;
count_clause=Stat.mk_int stat "input-clauses";
count_solve=Stat.mk_int stat "solve";
config;
} in
(* now add the theories *)
Theory_combine.add_theory_l th_combine theories;
(* assert [true] and [not false] *)
let tst = tst self in
Sat_solver.assume self.solver [
[Lit.atom tst @@ Term.true_ tst];
] Proof_default;
self
(** {2 Toplevel Goals}
List of toplevel goals to satisfy. Mainly used for checking purpose
*)
module Top_goals: sig
val push : term -> unit
val to_seq : term Iter.t
val check: unit -> unit
end = struct
(* list of terms to fully evaluate *)
let toplevel_goals_ : term list ref = ref []
(* add [t] to the set of terms that must be evaluated *)
let push (t:term): unit =
toplevel_goals_ := t :: !toplevel_goals_;
()
let to_seq k = List.iter k !toplevel_goals_
(* FIXME
(* check that this term fully evaluates to [true] *)
let is_true_ (t:term): bool = match CC.normal_form t with
| None -> false
| Some (NF_bool b) -> b
| Some (NF_cstor _) -> assert false (* not a bool *)
let check () =
if not (List.for_all is_true_ !toplevel_goals_)
then (
if Config.progress then flush_progress();
Log.debugf 1
(fun k->
let pp_lit out t =
let nf = CC.normal_form t in
Format.fprintf out "(@[term: %a@ nf: %a@])"
Term.pp t (Fmt.opt pp_term_nf) nf
in
k "(@[<hv1>Top_goals.check@ (@[<v>%a@])@])"
(Util.pp_list pp_lit) !toplevel_goals_);
assert false;
)
*)
let check () : unit = ()
end
(** {2 Conversion} *)
(* list of constants we are interested in *)
let model_support_ : Cst.t list ref = ref []
let model_env_ : Ast.env ref = ref Ast.env_empty
let add_cst_support_ (c:cst): unit =
CCList.Ref.push model_support_ c
let add_ty_support_ (_ty:Ty.t): unit = ()
(** {2 Result} *)
type unknown =
| U_timeout
| U_max_depth
| U_incomplete
let pp_unknown out = function
| U_timeout -> Fmt.string out "timeout"
| U_max_depth -> Fmt.string out "max depth reached"
| U_incomplete -> Fmt.string out "incomplete fragment"
type model = Model.t
let pp_model = Model.pp
type res =
| Sat of model
| Unsat of Proof.t option
| Unknown of unknown
(** {2 Main} *)
(* convert unsat-core *)
let clauses_of_unsat_core (core:Sat_solver.clause list): Lit.t IArray.t Iter.t =
Iter.of_list core
|> Iter.map clause_of_mclause
(* print all terms reachable from watched literals *)
let pp_term_graph _out (_:t) =
()
let pp_stats out (self:t) : unit =
Stat.pp_all out (Stat.all @@ stats self)
let do_on_exit ~on_exit =
List.iter (fun f->f()) on_exit;
()
(* map boolean subterms to literals *)
let add_bool_subterms_ (self:t) (t:Term.t) : unit =
Term.iter_dag t
|> Iter.filter (fun t -> Ty.is_prop @@ Term.ty t)
|> Iter.filter
(fun t -> match Term.view t with
| Term.Not _ -> false (* will process the subterm just later *)
| _ -> true)
|> Iter.iter
(fun sub ->
Log.debugf 5 (fun k->k "(@[solver.map-to-lit@ :subterm %a@])" Term.pp sub);
ignore (mk_atom_t self sub : Sat_solver.atom))
let assume (self:t) (c:Lit.t IArray.t) : unit =
let sat = solver self in
IArray.iter (fun lit -> add_bool_subterms_ self @@ Lit.term lit) c;
let c = IArray.to_array_map (Sat_solver.make_atom sat) c in
Stat.incr self.count_clause;
Sat_solver.add_clause_a sat c Proof_default
(* TODO: remove? use a special constant + micro theory instead?
let[@inline] assume_distinct self l ~neq lit : unit =
CC.assert_distinct (cc self) l lit ~neq
*)
let check_model (_s:t) : unit =
Log.debug 1 "(smt.solver.check-model)";
(* TODO
Sat_solver.check_model s.solver
*)
()
(* TODO: main loop with iterative deepening of the unrolling limit
(not the value depth limit) *)
let solve ?(on_exit=[]) ?(check=true) ~assumptions (self:t) : res =
let r = Sat_solver.solve ~assumptions (solver self) in
Stat.incr self.count_solve;
match r with
| Sat_solver.Sat st ->
Log.debugf 1 (fun k->k "SAT");
let lits f = st.iter_trail f (fun _ -> ()) in
let m = Theory_combine.mk_model (th_combine self) lits in
do_on_exit ~on_exit;
Sat m
(*
let env = Ast.env_empty in
let m = Model.make ~env in
Unknown U_incomplete (* TODO *)
*)
| Sat_solver.Unsat us ->
let pr =
try
let pr = us.get_proof () in
if check then Sat_solver.Proof.check pr;
Some pr
with Msat.Solver_intf.No_proof -> None
in
do_on_exit ~on_exit;
Unsat pr
(* FIXME:
(* TODO: max_depth should actually correspond to the maximum depth
of un-expanded terms (expand in body of t --> depth = depth(t)+1),
so it corresponds to unfolding call graph to some depth *)
let solve ?(on_exit=[]) ?(check=true) () =
let n_iter = ref 0 in
let rec check_cc (): res =
assert (Backtrack.at_level_0 ());
if !n_iter > Config.max_depth then Unknown U_max_depth (* exceeded limit *)
else begin match CC.check () with
| CC.Unsat _ -> Unsat (* TODO proof *)
| CC.Sat lemmas ->
add_cc_lemmas lemmas;
check_solver()
end
and check_solver (): res =
(* assume all literals [expanded t] are false *)
let assumptions =
Terms_to_expand.to_seq
|> Iter.map (fun {Terms_to_expand.lit; _} -> Lit.neg lit)
|> Iter.to_rev_list
in
incr n_iter;
Log.debugf 2
(fun k->k
"(@[<1>@{<Yellow>solve@}@ @[:with-assumptions@ (@[%a@])@ n_iter: %d]@])"
(Util.pp_list Lit.pp) assumptions !n_iter);
begin match M.solve ~assumptions() with
| M.Sat _ ->
Log.debugf 1 (fun k->k "@{<Yellow>** found SAT@}");
do_on_exit ~on_exit;
let m = Model_build.make () in
if check then Model_build.check m;
Sat m
| M.Unsat us ->
let p = us.SI.get_proof () in
Log.debugf 4 (fun k->k "proof: @[%a@]@." pp_proof p);
let core = p |> M.unsat_core in
(* check if unsat because of assumptions *)
expand_next core
end
(* pick a term to expand, or UNSAT *)
and expand_next (core:unsat_core) =
begin match find_to_expand core with
| None -> Unsat (* TODO proof *)
| Some to_expand ->
let t = to_expand.Terms_to_expand.term in
Log.debugf 2 (fun k->k "(@[<1>@{<green>expand_next@}@ :term %a@])" Term.pp t);
CC.expand_term t;
Terms_to_expand.remove t;
Clause.push_new (Clause.make [to_expand.Terms_to_expand.lit]);
Backtrack.backtrack_to_level_0 ();
check_cc () (* recurse *)
end
in
check_cc()
*)

View file

@ -1,77 +0,0 @@
(* This file is free software. See file "license" for more details. *)
(** {1 Solver}
The solving algorithm, based on MCSat *)
module Sat_solver : Msat.S
with type Formula.t = Lit.t
and type theory = Theory_combine.t
and type lemma = Theory_combine.proof
(** {2 Result} *)
type model = Model.t
module Atom = Sat_solver.Atom
module Proof : sig
type t = Sat_solver.Proof.t
val check : t -> unit
end
type unknown =
| U_timeout
| U_max_depth
| U_incomplete
type res =
| Sat of Model.t
| Unsat of Proof.t option
| Unknown of unknown
(** {2 Main} *)
type t
(** Solver state *)
val create :
?stat:Stat.t ->
?size:[`Big | `Tiny | `Small] ->
?config:Config.t ->
?store_proof:bool ->
theories:Theory.t list ->
unit -> t
val solver : t -> Sat_solver.t
val th_combine : t -> Theory_combine.t
val add_theory : t -> Theory.t -> unit
val cc : t -> CC.t
val stats : t -> Stat.t
val tst : t -> Term.state
val mk_atom_lit : t -> Lit.t -> Atom.t
val mk_atom_t : t -> ?sign:bool -> Term.t -> Atom.t
val assume : t -> Lit.t IArray.t -> unit
(* TODO: use the theory instead
val assume_distinct : t -> Term.t list -> neq:Term.t -> Lit.t -> unit
*)
val solve :
?on_exit:(unit -> unit) list ->
?check:bool ->
assumptions:Atom.t list ->
t ->
res
(** [solve s] checks the satisfiability of the statement added so far to [s]
@param check if true, the model is checked before returning
@param on_exit functions to be run before this returns *)
val check_model : t -> unit
val pp_term_graph: t CCFormat.printer
val pp_stats : t CCFormat.printer
val pp_unknown : unknown CCFormat.printer

View file

@ -1,187 +0,0 @@
module Vec = Msat.Vec
module Log = Msat.Log
module Fmt = CCFormat
(* for objects that are expanded on demand only *)
type 'a lazily_expanded =
| Lazy_some of 'a
| Lazy_none
(* main term cell. *)
type term = {
mutable term_id: int; (* unique ID *)
mutable term_ty: ty;
term_view : term term_view;
}
(* term shallow structure *)
and 'a term_view =
| Bool of bool
| App_cst of cst * 'a IArray.t (* full, first-order application *)
| Eq of 'a * 'a
| If of 'a * 'a * 'a
| Not of 'a
(* boolean literal *)
and lit = {
lit_term: term;
lit_sign: bool;
}
and cst = {
cst_id: ID.t;
cst_view: cst_view;
}
and cst_view =
| Cst_undef of fun_ty (* simple undefined constant *)
| Cst_def of {
pp : 'a. ('a Fmt.printer -> 'a IArray.t Fmt.printer) option;
abs : self:term -> term IArray.t -> term * bool; (* remove the sign? *)
do_cc: bool; (* participate in congruence closure? *)
relevant : 'a. ID.t -> 'a IArray.t -> int -> bool; (* relevant argument? *)
ty : ID.t -> term IArray.t -> ty; (* compute type *)
eval: value IArray.t -> value; (* evaluate term *)
}
(** Methods on the custom term view whose arguments are ['a].
Terms must be printable, and provide some additional theory handles.
- [relevant] must return a subset of [args] (possibly the same set).
The terms it returns will be activated and evaluated whenever possible.
Terms in [args \ relevant args] are considered for
congruence but not for evaluation.
*)
(** Function type *)
and fun_ty = {
fun_ty_args: ty list;
fun_ty_ret: ty;
}
(** Hashconsed type *)
and ty = {
mutable ty_id: int;
ty_view: ty_view;
}
and ty_view =
| Ty_prop
| Ty_atomic of {
def: ty_def;
args: ty list;
card: ty_card lazy_t;
}
and ty_def =
| Ty_uninterpreted of ID.t
| Ty_def of {
id: ID.t;
pp: ty Fmt.printer -> ty list Fmt.printer;
default_val: value list -> value; (* default value of this type *)
card: ty list -> ty_card;
}
and ty_card =
| Finite
| Infinite
(** Semantic values, used for models (and possibly model-constructing calculi) *)
and value =
| V_bool of bool
| V_element of {
id: ID.t;
ty: ty;
} (** a named constant, distinct from any other constant *)
| V_custom of {
view: value_custom_view;
pp: value_custom_view Fmt.printer;
eq: value_custom_view -> value_custom_view -> bool;
hash: value_custom_view -> int;
} (** Custom value *)
and value_custom_view = ..
type proof = Proof_default
type sat_actions = (Msat.void, lit, Msat.void, proof) Msat.acts
let[@inline] term_equal_ (a:term) b = a==b
let[@inline] term_hash_ a = a.term_id
let[@inline] term_cmp_ a b = CCInt.compare a.term_id b.term_id
let cmp_lit a b =
let c = CCBool.compare a.lit_sign b.lit_sign in
if c<>0 then c
else term_cmp_ a.lit_term b.lit_term
let cst_compare a b = ID.compare a.cst_id b.cst_id
let hash_lit a =
let sign = a.lit_sign in
Hash.combine3 2 (Hash.bool sign) (term_hash_ a.lit_term)
let pp_cst out a = ID.pp out a.cst_id
let id_of_cst a = a.cst_id
let[@inline] eq_ty a b = a.ty_id = b.ty_id
let eq_value a b = match a, b with
| V_bool a, V_bool b -> a=b
| V_element e1, V_element e2 ->
ID.equal e1.id e2.id && eq_ty e1.ty e2.ty
| V_custom x1, V_custom x2 ->
x1.eq x1.view x2.view
| V_bool _, _ | V_element _, _ | V_custom _, _
-> false
let hash_value a = match a with
| V_bool a -> Hash.bool a
| V_element e -> ID.hash e.id
| V_custom x -> x.hash x.view
let pp_value out = function
| V_bool b -> Fmt.bool out b
| V_element e -> ID.pp out e.id
| V_custom c -> c.pp out c.view
let pp_db out (i,_) = Format.fprintf out "%%%d" i
let rec pp_ty out t = match t.ty_view with
| Ty_prop -> Fmt.string out "prop"
| Ty_atomic {def=Ty_uninterpreted id; args=[]; _} -> ID.pp out id
| Ty_atomic {def=Ty_uninterpreted id; args; _} ->
Fmt.fprintf out "(@[%a@ %a@])" ID.pp id (Util.pp_list pp_ty) args
| Ty_atomic {def=Ty_def def; args; _} -> def.pp pp_ty out args
let pp_term_view_gen ~pp_id ~pp_t out = function
| Bool true -> Fmt.string out "true"
| Bool false -> Fmt.string out "false"
| App_cst ({cst_view=Cst_def {pp=Some pp_custom;_};_},l) -> pp_custom pp_t out l
| App_cst (c, a) when IArray.is_empty a ->
pp_id out (id_of_cst c)
| App_cst (f,l) ->
Fmt.fprintf out "(@[<1>%a@ %a@])" pp_id (id_of_cst f) (Util.pp_iarray pp_t) l
| Eq (a,b) -> Fmt.fprintf out "(@[<hv>=@ %a@ %a@])" pp_t a pp_t b
| If (a, b, c) ->
Fmt.fprintf out "(@[if %a@ %a@ %a@])" pp_t a pp_t b pp_t c
| Not u -> Fmt.fprintf out "(@[not@ %a@])" pp_t u
let pp_term_top ~ids out t =
let rec pp out t =
pp_rec out t;
(* FIXME if Config.pp_hashcons then Format.fprintf out "/%d" t.term_id; *)
and pp_rec out t = pp_term_view_gen ~pp_id ~pp_t:pp_rec out t.term_view
and pp_id = if ids then ID.pp else ID.pp_name in
pp out t
let pp_term = pp_term_top ~ids:false
let pp_term_view = pp_term_view_gen ~pp_id:ID.pp_name ~pp_t:pp_term
let pp_lit out l =
if l.lit_sign then pp_term out l.lit_term
else Format.fprintf out "(@[@<1>¬@ %a@])" pp_term l.lit_term
let pp_proof out = function
| Proof_default -> Fmt.fprintf out "<default proof>"

View file

@ -1,147 +0,0 @@
open Solver_types
type t = term = {
mutable term_id : int;
mutable term_ty : ty;
term_view : t term_view;
}
type 'a view = 'a term_view =
| Bool of bool
| App_cst of cst * 'a IArray.t
| Eq of 'a * 'a
| If of 'a * 'a * 'a
| Not of 'a
let[@inline] id t = t.term_id
let[@inline] ty t = t.term_ty
let[@inline] view t = t.term_view
let equal = term_equal_
let hash = term_hash_
let compare a b = CCInt.compare a.term_id b.term_id
module H = Hashcons.Make(struct
type t = term
let equal t1 t2 = Term_cell.equal t1.term_view t2.term_view
let hash t = Term_cell.hash t.term_view
let set_id t id =
assert (t.term_id < 0);
t.term_id <- id
end)
type state = {
tbl : H.t;
mutable n: int;
true_ : t lazy_t;
false_ : t lazy_t;
}
let[@inline] make st (c:t term_view) : t =
let t = {term_id= -1; term_ty=Ty.prop; term_view=c} in
let t' = H.hashcons st.tbl t in
if t == t' then (
t'.term_ty <- Term_cell.ty c;
);
t'
let[@inline] true_ st = Lazy.force st.true_
let[@inline] false_ st = Lazy.force st.false_
let bool st b = if b then true_ st else false_ st
let create ?(size=1024) () : state =
let rec st ={
n=2;
tbl=H.create ~size ();
true_ = lazy (make st Term_cell.true_);
false_ = lazy (make st Term_cell.false_);
} in
ignore (Lazy.force st.true_);
ignore (Lazy.force st.false_); (* not true *)
st
let app_cst st f a =
let cell = Term_cell.app_cst f a in
make st cell
let[@inline] const st c = app_cst st c IArray.empty
let[@inline] if_ st a b c = make st (Term_cell.if_ a b c)
let[@inline] eq st a b = make st (Term_cell.eq a b)
let[@inline] not_ st a = make st (Not a)
(* "eager" and, evaluating [a] first *)
let and_eager st a b = if_ st a b (false_ st)
(* might need to tranfer the negation from [t] to [sign] *)
let abs tst t : t * bool = match view t with
| Bool false -> true_ tst, false
| Not u -> u, false
| App_cst ({cst_view=Cst_def def; _}, args) ->
def.abs ~self:t args (* TODO: pass state *)
| _ -> t, true
let[@inline] is_true t = match view t with Bool true -> true | _ -> false
let[@inline] is_false t = match view t with Bool false -> true | _ -> false
let[@inline] is_const t = match view t with
| App_cst (_, a) -> IArray.is_empty a
| _ -> false
let cc_view (t:t) =
let module C = Sidekick_cc in
match view t with
| Bool b -> C.Bool b
| App_cst (f,_) when not (Cst.do_cc f) -> C.Opaque t (* skip *)
| App_cst (f,args) -> C.App_fun (f, IArray.to_seq args)
| Eq (a,b) -> C.Eq (a, b)
| If (a,b,c) -> C.If (a,b,c)
| Not u -> C.Not u
module As_key = struct
type t = term
let compare = compare
let equal = equal
let hash = hash
end
module Map = CCMap.Make(As_key)
module Set = CCSet.Make(As_key)
module Tbl = CCHashtbl.Make(As_key)
(* return [Some] iff the term is an undefined constant *)
let as_cst_undef (t:term): (cst * Ty.Fun.t) option =
match view t with
| App_cst (c, a) when IArray.is_empty a -> Cst.as_undefined c
| _ -> None
let pp = Solver_types.pp_term
module Iter_dag = struct
type t = unit Tbl.t
let create () : t = Tbl.create 16
let iter_dag (self:t) t yield =
let rec aux t =
if not @@ Tbl.mem self t then (
Tbl.add self t ();
yield t;
Term_cell.iter aux (view t)
)
in
aux t
end
let iter_dag t yield =
let st = Iter_dag.create() in
Iter_dag.iter_dag st t yield
(* TODO
module T_arg = struct
module Fun = Cst
module Term = struct
include Term
let view = cc_view
end
end
module Mini_cc = Mini_cc.Make(T_arg)
*)

View file

@ -1,67 +0,0 @@
open Solver_types
type t = term = {
mutable term_id : int;
mutable term_ty : ty;
term_view : t term_view;
}
type 'a view = 'a term_view =
| Bool of bool
| App_cst of cst * 'a IArray.t
| Eq of 'a * 'a
| If of 'a * 'a * 'a
| Not of 'a
val id : t -> int
val view : t -> term view
val ty : t -> Ty.t
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
type state
val create : ?size:int -> unit -> state
val make : state -> t view -> t
val true_ : state -> t
val false_ : state -> t
val bool : state -> bool -> t
val const : state -> cst -> t
val app_cst : state -> cst -> t IArray.t -> t
val eq : state -> t -> t -> t
val if_: state -> t -> t -> t -> t
val and_eager : state -> t -> t -> t (* evaluate left argument first *)
val not_ : state -> t -> t
(** Obtain unsigned version of [t], + the sign as a boolean *)
val abs : state -> t -> t * bool
module Iter_dag : sig
type t
val create : unit -> t
val iter_dag : t -> term -> term Iter.t
end
val iter_dag : t -> t Iter.t
val pp : t Fmt.printer
(** {6 Views} *)
val is_true : t -> bool
val is_false : t -> bool
val is_const : t -> bool
val cc_view : t -> (cst,t,t Iter.t) Sidekick_cc.view
(* return [Some] iff the term is an undefined constant *)
val as_cst_undef : t -> (cst * Ty.Fun.t) option
(** {6 Containers} *)
module Tbl : CCHashtbl.S with type key = t
module Map : CCMap.S with type key = t
module Set : CCSet.S with type elt = t

View file

@ -1,120 +0,0 @@
open Solver_types
(* TODO: normalization of {!term_cell} for use in signatures? *)
type 'a view = 'a Solver_types.term_view =
| Bool of bool
| App_cst of cst * 'a IArray.t
| Eq of 'a * 'a
| If of 'a * 'a * 'a
| Not of 'a
type t = term view
module type ARG = sig
type t
val hash : t -> int
val equal : t -> t -> bool
val pp : t Fmt.printer
end
module Make_eq(A : ARG) = struct
let sub_hash = A.hash
let sub_eq = A.equal
let hash (t:A.t view) : int = match t with
| Bool b -> Hash.bool b
| App_cst (f,l) ->
Hash.combine3 4 (Cst.hash f) (Hash.iarray sub_hash l)
| Eq (a,b) -> Hash.combine3 12 (sub_hash a) (sub_hash b)
| If (a,b,c) -> Hash.combine4 7 (sub_hash a) (sub_hash b) (sub_hash c)
| Not u -> Hash.combine2 70 (sub_hash u)
(* equality that relies on physical equality of subterms *)
let equal (a:A.t view) b : bool = match a, b with
| Bool b1, Bool b2 -> CCBool.equal b1 b2
| App_cst (f1, a1), App_cst (f2, a2) ->
Cst.equal f1 f2 && IArray.equal sub_eq a1 a2
| Eq(a1,b1), Eq(a2,b2) -> sub_eq a1 a2 && sub_eq b1 b2
| If (a1,b1,c1), If (a2,b2,c2) ->
sub_eq a1 a2 && sub_eq b1 b2 && sub_eq c1 c2
| Not a, Not b -> sub_eq a b
| Bool _, _ | App_cst _, _ | If _, _ | Eq _, _ | Not _, _
-> false
let pp = Solver_types.pp_term_view_gen ~pp_id:ID.pp_name ~pp_t:A.pp
end[@@inline]
include Make_eq(struct
type t = term
let equal (t1:t) t2 = t1==t2
let hash (t:term): int = CCHash.int t.term_id
let pp = pp_term
end)
let true_ = Bool true
let false_ = Bool false
let app_cst f a = App_cst (f, a)
let const c = App_cst (c, IArray.empty)
let eq a b =
if term_equal_ a b then (
Bool true
) else (
(* canonize *)
let a,b = if a.term_id > b.term_id then b, a else a, b in
Eq (a,b)
)
let not_ t =
match t.term_view with
| Bool b -> Bool (not b)
| Not u -> u.term_view
| _ -> Not t
let if_ a b c =
assert (Ty.equal b.term_ty c.term_ty);
If (a,b,c)
let ty (t:t): Ty.t = match t with
| Bool _ | Eq _ | Not _ -> Ty.prop
| App_cst (f, args) ->
begin match Cst.view f with
| Cst_undef fty ->
let ty_args, ty_ret = Ty.Fun.unfold fty in
(* check arity *)
if List.length ty_args <> IArray.length args then (
Error.errorf "Term_cell.apply: expected %d args, got %d@ in %a"
(List.length ty_args) (IArray.length args) pp t
);
(* check types *)
List.iteri
(fun i ty_a ->
let a = IArray.get args i in
if not @@ Ty.equal a.term_ty ty_a then (
Error.errorf "Term_cell.apply: %d-th argument mismatch:@ \
%a does not have type %a@ in %a"
i pp_term a Ty.pp ty_a pp t
))
ty_args;
ty_ret
| Cst_def def -> def.ty f.cst_id args
end
| If (_,b,_) -> b.term_ty
let iter f view =
match view with
| Bool _ -> ()
| App_cst (_,a) -> IArray.iter f a
| Not u -> f u
| Eq (a,b) -> f a; f b
| If (a,b,c) -> f a; f b; f c
module Tbl = CCHashtbl.Make(struct
type t = term view
let equal = equal
let hash = hash
end)

View file

@ -1,42 +0,0 @@
open Solver_types
type 'a view = 'a Solver_types.term_view =
| Bool of bool
| App_cst of cst * 'a IArray.t
| Eq of 'a * 'a
| If of 'a * 'a * 'a
| Not of 'a
type t = term view
val equal : t -> t -> bool
val hash : t -> int
val true_ : t
val false_ : t
val const : cst -> t
val app_cst : cst -> term IArray.t -> t
val eq : term -> term -> t
val if_ : term -> term -> term -> t
val not_ : term -> t
val ty : t -> Ty.t
(** Compute the type of this term cell. Not totally free *)
val pp : t Fmt.printer
val iter : ('a -> unit) -> 'a view -> unit
module type ARG = sig
type t
val hash : t -> int
val equal : t -> t -> bool
val pp : t Fmt.printer
end
module Make_eq(X : ARG) : sig
val equal : X.t view -> X.t view -> bool
val hash : X.t view -> int
val pp : X.t view Fmt.printer
end

View file

@ -1,122 +0,0 @@
module Th_clause : sig
type t = Lit.t IArray.t
val pp : t CCFormat.printer
end = struct
type t = Lit.t IArray.t
let pp out c =
if IArray.length c = 0 then CCFormat.string out "false"
else if IArray.length c = 1 then Lit.pp out (IArray.get c 0)
else (
Format.fprintf out "[@[<hv>%a@]]"
(Util.pp_iarray ~sep:" " Lit.pp) c
)
end
(** Unsatisfiable conjunction.
Its negation will become a conflict clause *)
type conflict = Lit.t list
module CC_eq_class = CC.N
module CC_expl = CC.Expl
(** Actions available to a theory during its lifetime *)
module type ACTIONS = sig
val cc : CC.t
val raise_conflict: conflict -> 'a
(** Give a conflict clause to the solver *)
val propagate: Lit.t -> (unit -> Lit.t list) -> unit
(** Propagate a boolean using a unit clause.
[expl => lit] must be a theory lemma, that is, a T-tautology *)
val propagate_l: Lit.t -> Lit.t list -> unit
(** Propagate a boolean using a unit clause.
[expl => lit] must be a theory lemma, that is, a T-tautology *)
val add_lit : Lit.t -> unit
(** Add the given literal to the SAT solver, so it gets assigned
a boolean value *)
val add_local_axiom: Lit.t list -> unit
(** Add local clause to the SAT solver. This clause will be
removed when the solver backtracks. *)
val add_persistent_axiom: Lit.t list -> unit
(** Add toplevel clause to the SAT solver. This clause will
not be backtracked. *)
end
type actions = (module ACTIONS)
module type S = sig
type t
val name : string
(** Name of the theory *)
val create : Term.state -> t
(** Instantiate the theory's state *)
val on_new_term : t -> actions -> Term.t -> unit
(** Called when a new term is added *)
val on_merge: t -> actions -> CC_eq_class.t -> CC_eq_class.t -> CC_expl.t -> unit
(** Called when two classes are merged *)
val partial_check : t -> actions -> Lit.t Iter.t -> unit
(** Called when a literal becomes true *)
val final_check: t -> actions -> Lit.t Iter.t -> unit
(** Final check, must be complete (i.e. must raise a conflict
if the set of literals is not satisfiable) *)
val mk_model : t -> Lit.t Iter.t -> Model.t -> Model.t
(** Make a model for this theory's terms *)
val push_level : t -> unit
val pop_levels : t -> int -> unit
val cc_th : t -> CC.Theory.t list
(**/**)
val check_invariants : t -> unit
(**/**)
end
type t = (module S)
type 'a t1 = (module S with type t = 'a)
let make
(type st)
?(check_invariants=fun _ -> ())
?(on_new_term=fun _ _ _ -> ())
?(on_merge=fun _ _ _ _ _ -> ())
?(partial_check=fun _ _ _ -> ())
?(mk_model=fun _ _ m -> m)
?(push_level=fun _ -> ())
?(pop_levels=fun _ _ -> ())
?(cc_th=fun _->[])
~name
~final_check
~create
() : t =
let module A = struct
type nonrec t = st
let name = name
let create = create
let on_new_term = on_new_term
let on_merge = on_merge
let partial_check = partial_check
let final_check = final_check
let mk_model = mk_model
let check_invariants = check_invariants
let push_level = push_level
let pop_levels = pop_levels
let cc_th = cc_th
end in
(module A : S)

View file

@ -1,162 +0,0 @@
(** {1 Main theory} *)
(** Combine the congruence closure with a number of plugins *)
open Solver_types
module Proof = struct
type t = Solver_types.proof
let default = Proof_default
end
module Formula = Lit
module Eq_class = CC.N
module Expl = CC.Expl
type formula = Lit.t
type proof = Proof.t
type conflict = Theory.conflict
type theory_state =
| Th_state : ('a Theory.t1 * 'a) -> theory_state
(* TODO: first-class module instead *)
type t = {
tst: Term.state; (** state for managing terms *)
cc: CC.t lazy_t; (** congruence closure *)
stat: Stat.t;
count_axiom: int Stat.counter;
count_conflict: int Stat.counter;
count_propagate: int Stat.counter;
mutable theories : theory_state list; (** Set of theories *)
}
let[@inline] cc (t:t) = Lazy.force t.cc
let[@inline] tst t = t.tst
let[@inline] theories (self:t) : theory_state Iter.t =
fun k -> List.iter k self.theories
(** {2 Interface with the SAT solver} *)
(* handle a literal assumed by the SAT solver *)
let assert_lits_ ~final (self:t) acts (lits:Lit.t Iter.t) : unit =
Msat.Log.debugf 2
(fun k->k "(@[<hv1>@{<green>th_combine.assume_lits@}%s@ %a@])"
(if final then "[final]" else "") (Util.pp_seq ~sep:"; " Lit.pp) lits);
(* transmit to CC *)
let cc = cc self in
if not final then (
CC.assert_lits cc lits;
);
(* transmit to theories. *)
CC.check cc acts;
let module A = struct
let cc = cc
let[@inline] raise_conflict c : 'a =
Stat.incr self.count_conflict;
acts.Msat.acts_raise_conflict c Proof_default
let[@inline] propagate p cs : unit =
Stat.incr self.count_propagate;
acts.Msat.acts_propagate p (Msat.Consequence (fun () -> cs(), Proof_default))
let[@inline] propagate_l p cs : unit = propagate p (fun()->cs)
let[@inline] add_local_axiom lits : unit =
Stat.incr self.count_axiom;
acts.Msat.acts_add_clause ~keep:false lits Proof_default
let[@inline] add_persistent_axiom lits : unit =
Stat.incr self.count_axiom;
acts.Msat.acts_add_clause ~keep:true lits Proof_default
let[@inline] add_lit lit : unit = acts.Msat.acts_mk_lit lit
end in
let acts = (module A : Theory.ACTIONS) in
theories self
(fun (Th_state ((module Th),st)) ->
(* give new merges, then call {final,partial}-check *)
if final then Th.final_check st acts lits else Th.partial_check st acts lits);
()
let[@inline] iter_atoms_ acts : _ Iter.t =
fun f ->
acts.Msat.acts_iter_assumptions
(function
| Msat.Lit a -> f a
| Msat.Assign _ -> assert false)
(* propagation from the bool solver *)
let check_ ~final (self:t) (acts:_ Msat.acts) =
let iter = iter_atoms_ acts in
(* TODO if Config.progress then print_progress(); *)
Msat.Log.debugf 5 (fun k->k "(th_combine.assume :len %d)" (Iter.length iter));
assert_lits_ ~final self acts iter
let add_formula (self:t) (lit:Lit.t) =
let t = Lit.term lit in
let lazy cc = self.cc in
let n = CC.add_term cc t in
CC.set_as_lit cc n (Lit.abs lit);
()
(* propagation from the bool solver *)
let[@inline] partial_check (self:t) (acts:_ Msat.acts) : unit =
check_ ~final:false self acts
(* perform final check of the model *)
let[@inline] final_check (self:t) (acts:_ Msat.acts) : unit =
check_ ~final:true self acts
let push_level (self:t) : unit =
CC.push_level (cc self);
theories self (fun (Th_state ((module Th), st)) -> Th.push_level st)
let pop_levels (self:t) n : unit =
CC.pop_levels (cc self) n;
theories self (fun (Th_state ((module Th), st)) -> Th.pop_levels st n)
let mk_model (self:t) lits : Model.t =
let m =
Iter.fold
(fun m (Th_state ((module Th),st)) -> Th.mk_model st lits m)
Model.empty (theories self)
in
(* now complete model using CC *)
CC.mk_model (cc self) m
(** {2 Interface to Congruence Closure} *)
(** {2 Main} *)
(* create a new theory combination *)
let create ?(stat=Stat.global) () : t =
Log.debug 5 "th_combine.create";
let rec self = {
tst=Term.create ~size:1024 ();
cc = lazy (
(* lazily tie the knot *)
(* TODO: pass theories *)
CC.create ~size:`Big self.tst;
);
theories = [];
stat;
count_axiom = Stat.mk_int stat "th-axioms";
count_propagate = Stat.mk_int stat "th-propagations";
count_conflict = Stat.mk_int stat "th-conflicts";
} in
ignore (Lazy.force @@ self.cc : CC.t);
self
let check_invariants (self:t) =
if Util._CHECK_INVARIANTS then (
CC.check_invariants (cc self);
)
let add_theory (self:t) (th:Theory.t) : unit =
let (module Th) = th in
Log.debugf 2
(fun k-> k "(@[th_combine.add_th@ :name %S@])" Th.name);
let st = Th.create self.tst in
(* add micro theories *)
List.iter (CC.add_th (cc self)) (Th.cc_th st);
(* re-pack as a [Theory.t1] *)
self.theories <- (Th_state ((module Th),st)) :: self.theories
let add_theory_l self = List.iter (add_theory self)

View file

@ -1,29 +0,0 @@
(** {1 Main theory} *)
(** Combine the congruence closure with a number of plugins *)
module Proof : sig
type t = Solver_types.proof (* dummy proofs, for now *)
end
include Msat.Solver_intf.PLUGIN_CDCL_T
with module Formula = Lit
and type proof = Proof.t
val create : ?stat:Stat.t -> unit -> t
val cc : t -> CC.t
val tst : t -> Term.state
type theory_state =
| Th_state : ('a Theory.t1 * 'a) -> theory_state
val theories : t -> theory_state Iter.t
val mk_model : t -> Lit.t Iter.t -> Model.t
val add_theory : t -> Theory.t -> unit
(** How to add new theories *)
val add_theory_l : t -> Theory.t list -> unit

View file

@ -1,94 +0,0 @@
open Solver_types
type t = ty
type view = Solver_types.ty_view
type def = Solver_types.ty_def
let[@inline] id t = t.ty_id
let[@inline] view t = t.ty_view
let equal = eq_ty
let[@inline] compare a b = CCInt.compare a.ty_id b.ty_id
let[@inline] hash a = a.ty_id
let equal_def d1 d2 = match d1, d2 with
| Ty_uninterpreted id1, Ty_uninterpreted id2 -> ID.equal id1 id2
| Ty_def d1, Ty_def d2 -> ID.equal d1.id d2.id
| Ty_uninterpreted _, _ | Ty_def _, _
-> false
module H = Hashcons.Make(struct
type t = ty
let equal a b = match a.ty_view, b.ty_view with
| Ty_prop, Ty_prop -> true
| Ty_atomic a1, Ty_atomic a2 ->
equal_def a1.def a2.def && CCList.equal equal a1.args a2.args
| Ty_prop, _ | Ty_atomic _, _
-> false
let hash t = match t.ty_view with
| Ty_prop -> 1
| Ty_atomic {def=Ty_uninterpreted id; args; _} ->
Hash.combine3 10 (ID.hash id) (Hash.list hash args)
| Ty_atomic {def=Ty_def d; args; _} ->
Hash.combine3 20 (ID.hash d.id) (Hash.list hash args)
let set_id ty id =
assert (ty.ty_id < 0);
ty.ty_id <- id
end)
(* build a type *)
let make_ : ty_view -> t =
let tbl : H.t = H.create ~size:128 () in
fun[@inline] c ->
let ty = {ty_id= -1; ty_view=c; } in
H.hashcons tbl ty
let card t = match view t with
| Ty_prop -> Finite
| Ty_atomic {card=lazy c; _} -> c
let prop = make_ Ty_prop
let atomic def args : t =
let card = lazy (
match def with
| Ty_uninterpreted _ ->
if List.for_all (fun sub -> card sub = Finite) args then Finite else Infinite
| Ty_def d -> d.card args
) in
make_ (Ty_atomic {def; args; card})
let atomic_uninterpreted id = atomic (Ty_uninterpreted id) []
let is_prop t =
match t.ty_view with | Ty_prop -> true | _ -> false
let is_uninterpreted t =
match t.ty_view with | Ty_atomic {def=Ty_uninterpreted _; _} -> true | _ -> false
let pp = pp_ty
module Tbl = CCHashtbl.Make(struct
type t = ty
let equal = equal
let hash = hash
end)
module Fun = struct
type t = fun_ty
let[@inline] args f = f.fun_ty_args
let[@inline] ret f = f.fun_ty_ret
let[@inline] arity f = List.length @@ args f
let[@inline] mk args ret : t = {fun_ty_args=args; fun_ty_ret=ret}
let[@inline] unfold t = args t, ret t
let pp out f : unit =
match args f with
| [] -> pp out (ret f)
| args ->
Format.fprintf out "(@[(@[%a@])@ %a@])" (Util.pp_list pp) args pp (ret f)
end

View file

@ -1,41 +0,0 @@
(** {1 Hashconsed Types} *)
open Solver_types
type t = Solver_types.ty
type view = Solver_types.ty_view
type def = Solver_types.ty_def
val id : t -> int
val view : t -> view
val prop : t
val atomic : def -> t list -> t
val atomic_uninterpreted : ID.t -> t
val card : t -> ty_card
val is_prop : t -> bool
val is_uninterpreted : t -> bool
include Intf.EQ with type t := t
include Intf.ORD with type t := t
include Intf.HASH with type t := t
include Intf.PRINT with type t := t
module Tbl : CCHashtbl.S with type key = t
module Fun : sig
type t = fun_ty
val args : t -> ty list
val ret : t -> ty
val arity : t -> int
val unfold : t -> ty list * ty
val mk : ty list -> ty -> t
include Intf.PRINT with type t := t
end

View file

@ -1,19 +0,0 @@
open Solver_types
type t = ty_card
let (+) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite
let ( * ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite
let ( ^ ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite
let finite = Finite
let infinite = Infinite
let sum = List.fold_left (+) Finite
let product = List.fold_left ( * ) Finite
let equal = (=)
let compare = Pervasives.compare
let pp out = function
| Finite -> Fmt.string out "finite"
| Infinite -> Fmt.string out "infinite"

View file

@ -1,17 +0,0 @@
(** {1 Type Cardinality} *)
type t = Solver_types.ty_card
val (+) : t -> t -> t
val ( * ) : t -> t -> t
val ( ^ ) : t -> t -> t
val finite : t
val infinite : t
val sum : t list -> t
val product : t list -> t
val equal : t -> t -> bool
val compare : t -> t -> int
val pp : t Intf.printer

View file

@ -1,23 +0,0 @@
(** {1 Value} *)
open Solver_types
type t = value
let true_ = V_bool true
let false_ = V_bool false
let bool v = V_bool v
let mk_elt id ty : t = V_element {id; ty}
let is_bool = function V_bool _ -> true | _ -> false
let is_true = function V_bool true -> true | _ -> false
let is_false = function V_bool false -> true | _ -> false
let equal = eq_value
let hash = hash_value
let pp = pp_value
let fresh (t:term) : t =
mk_elt (ID.makef "v_%d" t.term_id) t.term_ty

View file

@ -1,24 +0,0 @@
(** {1 Value}
Semantic value *)
type t = Solver_types.value
val true_ : t
val false_ : t
val bool : bool -> t
val mk_elt : ID.t -> Ty.t -> t
val is_bool : t -> bool
val is_true : t -> bool
val is_false : t -> bool
val fresh : Term.t -> t
include Intf.EQ with type t := t
include Intf.HASH with type t := t
include Intf.PRINT with type t := t

View file

@ -1,10 +0,0 @@
(library
(name Sidekick_smt)
(public_name sidekick.smt)
(libraries containers containers.data iter
sidekick.util sidekick.cc msat zarith)
(flags :standard -warn-error -a+8
-color always -safe-string -short-paths -open Sidekick_util)
(ocamlopt_flags :standard -O3 -color always
-unbox-closures -unbox-closures-factor 20))

View file

@ -1,9 +1,8 @@
(* This file is free software. See file "license" for more details. *)
(** {1 Preprocessing AST} *)
module Fmt = CCFormat
open Sidekick_base_term
type 'a or_error = ('a, string) CCResult.t
@ -161,7 +160,6 @@ type statement =
| Decl of ID.t * Ty.t
| Define of definition list
| Assert of term
| Assert_bool of int list
| Goal of var list * term
| CheckSat
| Exit
@ -438,7 +436,6 @@ let pp_statement out = function
Fmt.fprintf out "(@[<1>declare-fun@ %a (@[%a@])@ %a@])"
ID.pp id (Util.pp_list Ty.pp) args Ty.pp ret
| Assert t -> Fmt.fprintf out "(@[assert@ %a@])" pp_term t
| Assert_bool l -> Fmt.fprintf out "(@[assert-bool@ %a@])" (Util.pp_list Fmt.int) l
| Goal (vars,g) ->
Fmt.fprintf out "(@[assert-not@ %a@])" pp_term (forall_l vars (not_ g))
| Exit -> Fmt.string out "(exit)"
@ -482,7 +479,7 @@ let env_add_statement env st =
List.fold_left
(fun map (id,ty,def) -> add_def id (E_defined (ty,def)) map)
env l
| Goal _ | Assert _ | Assert_bool _ | CheckSat | Exit
| Goal _ | Assert _ | CheckSat | Exit
| SetLogic _ | SetOption _ | SetInfo _
-> env

View file

@ -1,8 +1,9 @@
(* This file is free software. See file "license" for more details. *)
(** {1 Preprocessing AST} *)
open Sidekick_base_term
type 'a or_error = ('a, string) CCResult.t
(** {2 Types} *)
@ -129,7 +130,6 @@ type statement =
| Decl of ID.t * Ty.t
| Define of definition list
| Assert of term
| Assert_bool of int list
| Goal of var list * term
| CheckSat
| Exit

View file

@ -1,4 +1,3 @@
(* This file is free software, copyright Simon Cruanes. See file "LICENSE" for more details. *)
(** {1 Locations} *)

View file

@ -1,16 +1,190 @@
(** {2 Conversion into {!Term.t}} *)
open Sidekick_smt
open Sidekick_base_term
[@@@ocaml.warning "-32"]
type 'a or_error = ('a, string) CCResult.t
module E = CCResult
module A = Ast
module Form = Sidekick_th_bool.Bool_term
module Th_distinct = Sidekick_th_distinct
module Fmt = CCFormat
module Dot = Msat_backend.Dot.Make(Solver.Sat_solver)(Msat_backend.Dot.Default(Solver.Sat_solver))
module Form = struct
module T = Term
open Sidekick_th_bool_static
exception Not_a_th_term
let id_and = ID.make "and"
let id_or = ID.make "or"
let id_imply = ID.make "=>"
let id_ite = ID.make "ite"
let view_id fid args =
if ID.equal fid id_and then (
B_and args
) else if ID.equal fid id_or then (
B_or args
) else if ID.equal fid 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 fid id_ite && IArray.length args = 3 then (
B_ite (IArray.get args 0, IArray.get args 1, IArray.get args 2)
) else (
raise_notrace Not_a_th_term
)
let view_as_bool (t:T.t) : T.t bool_view =
match T.view t with
| Bool b -> B_bool b
| Not u -> B_not u
| Eq (a, b) when Ty.is_bool (T.ty a) -> B_equiv (a,b)
| App_fun ({fun_id; _}, args) ->
(try view_id fun_id args with Not_a_th_term -> B_atom t)
| _ -> B_atom t
module Funs = struct
let get_ty id args =
if ID.equal id id_ite then T.ty (IArray.get args 1)
else Ty.bool
let abs ~self _a =
match T.view self with
| Not u -> u, false
| _ -> self, true
(* no congruence closure for boolean terms *)
let relevant _id _ _ = false
let eval id args =
let open Value in
match view_id id args with
| B_bool b -> Value.bool b
| 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_ite(a,b,c) ->
if Value.is_true a then b
else if Value.is_false a then c
else Error.errorf "non boolean value %a in ite" Value.pp a
| B_equiv (a,b) | B_eq(a,b) -> Value.bool (Value.equal a b)
| B_atom v -> v
| B_not _ | B_and _ | B_or _ | B_imply _
-> Error.errorf "non boolean value in boolean connective"
let mk_fun ?(do_cc=false) id : Fun.t =
{fun_id=id;
fun_view=Fun_def {
pp=None; abs; ty=get_ty; relevant; do_cc; eval=eval id; }; }
let and_ = mk_fun id_and
let or_ = mk_fun id_or
let imply = mk_fun id_imply
let ite = mk_fun id_ite
end
let as_id id (t:T.t) : T.t IArray.t option =
match T.view t with
| App_fun ({fun_id; _}, args) when ID.equal id fun_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_fun st Funs.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_fun st Funs.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 ite st a b c = match T.view a with
| T.Bool ba -> if ba then b else c
| _ -> T.app_fun st Funs.ite (IArray.of_array_unsafe [| a;b;c |])
let equiv st a b =
if T.equal a b then T.true_ st
else if T.is_true a then b
else if T.is_true b then a
else if T.is_false a then not_ st b
else if T.is_false b then not_ st a
else T.eq st a b
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_fun st Funs.imply (IArray.append (IArray.singleton y) xs)
let imply_l st xs y = match xs with
| [] -> y
| _ -> T.app_fun st Funs.imply (IArray.of_list @@ y :: xs)
let imply st a b = imply_a st (IArray.singleton a) b
let distinct_l tst l =
match l with
| [] | [_] -> T.true_ tst
| l ->
(* turn into [and_{i<j} t_i != t_j] *)
let cs =
CCList.diagonal l |> List.map (fun (a,b) -> neq tst a b)
in
and_l tst cs
let mk_bool st = function
| B_bool b -> T.bool st b
| 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_ite (a,b,c) -> ite st a b c
| B_equiv (a,b) -> equiv st a b
| B_eq (a,b) -> T.eq st a b
| B_not t -> not_ st t
module Gensym = struct
type t = {
tst: T.state;
mutable fresh: int;
}
let create tst : t = {tst; fresh=0}
let fresh_term (self:t) ~pre (ty:Ty.t) : T.t =
let name = Printf.sprintf "_tseitin_%s%d" pre self.fresh in
self.fresh <- 1 + self.fresh;
let id = ID.make name in
T.const self.tst @@ Fun.mk_undef_const id ty
end
end
module Subst = struct
type 'a t = 'a ID.Map.t
@ -31,7 +205,7 @@ module Conv = struct
let mk_ty id = Ty.atomic_uninterpreted id in
(* convert a type *)
let aux_ty (ty:A.Ty.t) : Ty.t = match ty with
| A.Ty.Prop -> Ty.prop
| A.Ty.Prop -> Ty.bool
(* | A.Ty.Rat -> Reg.find_exn reg Mc2_lra.k_rat *)
| A.Ty.App (id, []) -> mk_ty id
| A.Ty.App (_, _) ->
@ -52,8 +226,8 @@ module Conv = struct
let conv_term (tst:Term.state) (t:A.term): Term.t =
(* polymorphic equality *)
let mk_eq t u = Form.eq tst t u in (* TODO: use theory of booleans *)
let mk_app f l = Term.app_cst tst f (IArray.of_list l) in
let mk_eq t u = Term.eq tst t u in
let mk_app f l = Term.app_fun tst f (IArray.of_list l) in
let mk_const = Term.const tst in
(*
let mk_lra_pred = Reg.find_exn reg Mc2_lra.k_make_pred in
@ -98,20 +272,20 @@ module Conv = struct
end
| A.Const id ->
let ty = conv_fun_ty @@ A.ty t in
mk_const (Cst.mk_undef id ty)
mk_const (Fun.mk_undef id ty)
| A.App (f, l) ->
let l = List.map (aux subst) l in
begin match A.term_view f with
| A.Const id ->
(* TODO: lookup definition of [f] *)
mk_app (Cst.mk_undef id (conv_fun_ty @@ A.ty f)) l
mk_app (Fun.mk_undef id (conv_fun_ty @@ A.ty f)) l
| _ -> Error.errorf "cannot process HO application %a" A.pp_term t
end
| A.If (a,b,c) ->
let a = aux subst a in
let b = aux subst b in
let c = aux subst c in
Term.if_ tst a b c
Form.ite tst a b c
| A.Let (vbs,u) ->
let subst =
List.fold_left
@ -138,7 +312,7 @@ module Conv = struct
in
Form.and_l tst (curry_eq l)
| A.Op (A.Distinct, l) ->
Th_distinct.distinct_l 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
@ -218,10 +392,74 @@ end
let conv_ty = Conv.conv_ty
let conv_term = Conv.conv_term
(* instantiate solver here *)
module Solver_arg = struct
include Sidekick_base_term
let cc_view = Term.cc_view
module Proof = struct
type t = Default
let default=Default
let pp out _ = Fmt.string out "default"
end
end
module Solver = Sidekick_msat_solver.Make(Solver_arg)
module Check_cc = struct
module SI = Solver.Solver_internal
module CC = Solver.Solver_internal.CC
module MCC = Sidekick_mini_cc.Make(Solver_arg)
let pp_c out c = Fmt.fprintf out "(@[%a@])" (Util.pp_list ~sep:" " Lit.pp) c
let pp_and out c = Fmt.fprintf out "(@[%a@])" (Util.pp_list ~sep:"" Lit.pp) c
let add_cc_lit (cc:MCC.t) (lit:Lit.t) : unit =
let t = Lit.term lit in
MCC.add_lit cc t (Lit.sign lit)
(* check that this is a proper CC conflict *)
let check_conflict si _cc (confl:Lit.t list) : unit =
Log.debugf 15 (fun k->k "(@[check-cc-conflict@ %a@])" pp_c confl);
let tst = SI.tst si in
let cc = MCC.create tst in
(* add [¬confl] and check it's unsat *)
List.iter (fun lit -> add_cc_lit cc @@ Lit.neg lit) confl;
if MCC.check_sat cc then (
Error.errorf "@[<2>check-cc-conflict:@ @[clause %a@]@ \
is not a UF tautology (negation is sat)@]" pp_c confl
) else (
Log.debugf 15 (fun k->k "(@[check-cc-conflict.ok@ %a@])" pp_c confl);
)
let check_propagation si _cc p reason : unit =
let reason = reason() in
Log.debugf 15 (fun k->k "(@[check-cc-prop@ %a@ :reason %a@])" Lit.pp p pp_and reason);
let tst = SI.tst si in
let cc = MCC.create tst in
(* add [reason & ¬lit] and check it's unsat *)
List.iter (add_cc_lit cc) reason;
add_cc_lit cc (Lit.neg p);
if MCC.check_sat cc then (
Error.errorf "@[<2>check-cc-prop:@ @[%a => %a@]@ \
is not a UF tautology (negation is sat)@]" pp_and reason Lit.pp p
) else (
Log.debugf 15
(fun k->k "(@[check-cc-prop.ok@ @[%a => %a@]@])" pp_and reason Lit.pp p);
)
let theory =
Solver.mk_theory ~name:"cc-check"
~create_and_setup:(fun si ->
Solver.Solver_internal.on_cc_conflict si (check_conflict si))
()
end
(* TODO
(* check SMT model *)
let check_smt_model (solver:Solver.Sat_solver.t) (hyps:_ Vec.t) (m:Model.t) : unit =
Log.debug 1 "(smt.check-smt-model)";
let open Solver_types in
let module S = Solver.Sat_solver in
let check_atom (lit:Lit.t) : Msat.lbool =
Log.debugf 5 (fun k->k "(@[smt.check-smt-model.atom@ %a@])" Lit.pp lit);
@ -259,6 +497,7 @@ let check_smt_model (solver:Solver.Sat_solver.t) (hyps:_ Vec.t) (m:Model.t) : un
);
in
Vec.iter check_c hyps
*)
(* call the solver to check-sat *)
let solve
@ -268,7 +507,7 @@ let solve
?(pp_model=false)
?(check=false)
?time:_ ?memory:_ ?progress:_
?hyps
?hyps:_
~assumptions
s : unit =
let t1 = Sys.time() in
@ -280,17 +519,20 @@ let solve
begin match res with
| Solver.Sat m ->
if pp_model then (
Format.printf "(@[<hv1>model@ %a@])@." Model.pp m
(* TODO: use actual {!Model} in the solver? or build it afterwards *)
Format.printf "(@[<hv1>model@ %a@])@." Solver.Model.pp m
);
(* TODO
if check then (
Solver.check_model s;
CCOpt.iter (fun h -> check_smt_model (Solver.solver s) h m) hyps;
);
*)
let t3 = Sys.time () -. t2 in
Format.printf "Sat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
| Solver.Unsat None ->
| Solver.Unsat {proof=None;_} ->
Format.printf "Unsat (%.3f/%.3f/-)@." t1 (t2-.t1);
| Solver.Unsat (Some p) ->
| Solver.Unsat {proof=Some p;_} ->
if check then (
Solver.Proof.check p;
);
@ -301,28 +543,19 @@ let solve
(fun oc ->
Log.debugf 1 (fun k->k "write proof into `%s`" file);
let fmt = Format.formatter_of_out_channel oc in
Dot.pp fmt p;
Solver.Proof.pp_dot fmt p;
Format.pp_print_flush fmt (); flush oc)
end;
let t3 = Sys.time () -. t2 in
Format.printf "Unsat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
| Solver.Unknown reas ->
Format.printf "Unknown (:reason %a)" Solver.pp_unknown reas
Format.printf "Unknown (:reason %a)" Solver.Unknown.pp reas
end
(* NOTE: hack for testing with dimacs. Proper treatment should go into
scoping in Ast, or having theory-specific state in `Term.state` *)
let mk_iatom =
let tbl = Util.Int_tbl.create 6 in (* for atoms *)
fun tst i ->
let c = Util.Int_tbl.get_or_add tbl ~k:(abs i)
~f:(fun i -> Cst.mk_undef_const (ID.makef "a_%d" i) Ty.prop) in
Lit.atom tst ~sign:(i>0) @@ Term.const tst c
(* process a single statement *)
let process_stmt
?hyps
?gc ?restarts ?(pp_cnf=false) ?dot_proof ?pp_model ?check
?gc ?restarts ?(pp_cnf=false) ?dot_proof ?pp_model ?(check=false)
?time ?memory ?progress
(solver:Solver.t)
(stmt:Ast.statement) : unit or_error =
@ -353,7 +586,7 @@ let process_stmt
raise Exit
| A.CheckSat ->
solve
?gc ?restarts ?dot_proof ?check ?pp_model ?time ?memory ?progress
?gc ?restarts ?dot_proof ~check ?pp_model ?time ?memory ?progress
~assumptions:[] ?hyps
solver;
E.return()
@ -373,13 +606,8 @@ let process_stmt
);
let atom = Lit.atom tst t in
CCOpt.iter (fun h -> Vec.push h [atom]) hyps;
Solver.assume solver (IArray.singleton atom);
Solver.add_clause_lits solver (IArray.singleton atom);
E.return()
| A.Assert_bool l ->
let c = List.rev_map (mk_iatom tst) l in
CCOpt.iter (fun h -> Vec.push h c) hyps;
Solver.assume solver (IArray.of_list c);
E.return ()
| A.Goal (_, _) ->
Error.errorf "cannot deal with goals yet"
| A.Data _ ->
@ -388,381 +616,11 @@ let process_stmt
Error.errorf "cannot deal with definitions yet"
end
module Th_bool = Sidekick_th_bool_static.Make(struct
module S = Solver
type term = S.A.Term.t
include Form
end)
(* FIXME: merge this
module Conv : sig
val add_statement : Ast.statement -> unit
val add_statement_l : Ast.statement list -> unit
val ty_to_ast: Ty.t -> Ast.Ty.t
val term_to_ast: term -> Ast.term
end = struct
(* for converting Ast.Ty into Ty *)
let ty_tbl_ : Ty.t lazy_t ID.Tbl.t = ID.Tbl.create 16
(* for converting constants *)
let decl_ty_ : cst lazy_t ID.Tbl.t = ID.Tbl.create 16
(* environment for variables *)
type conv_env = {
let_bound: (term * int) ID.Map.t;
(* let-bound variables, to be replaced. int=depth at binding position *)
bound: (int * Ty.t) ID.Map.t;
(* set of bound variables. int=depth at binding position *)
depth: int;
}
let empty_env : conv_env =
{let_bound=ID.Map.empty; bound=ID.Map.empty; depth=0}
let rec conv_ty (ty:Ast.Ty.t): Ty.t = match ty with
| Ast.Ty.Prop -> Ty.prop
| Ast.Ty.Const id ->
begin try ID.Tbl.find ty_tbl_ id |> Lazy.force
with Not_found -> Error.errorf "type %a not in ty_tbl" ID.pp id
end
| Ast.Ty.Arrow (a,b) -> Ty.arrow (conv_ty a) (conv_ty b)
let add_bound env v =
let ty = Ast.Var.ty v |> conv_ty in
{ env with
depth=env.depth+1;
bound=ID.Map.add (Ast.Var.id v) (env.depth,ty) env.bound; }
(* add [v := t] to bindings. Depth is not incremented
(there will be no binders) *)
let add_let_bound env v t =
{ env with
let_bound=ID.Map.add (Ast.Var.id v) (t,env.depth) env.let_bound }
let find_env env v =
let id = Ast.Var.id v in
ID.Map.get id env.let_bound, ID.Map.get id env.bound
let rec conv_term_rec
(env: conv_env)
(t:Ast.term): term = match Ast.term_view t with
| Ast.Bool true -> Term.true_
| Ast.Bool false -> Term.false_
| Ast.Unknown _ -> assert false
| Ast.Const id ->
begin
try ID.Tbl.find decl_ty_ id |> Lazy.force |> Term.const
with Not_found ->
errorf "could not find constant `%a`" ID.pp id
end
| Ast.App (f, l) ->
begin match Ast.term_view f with
| Ast.Const id ->
let f =
try ID.Tbl.find decl_ty_ id |> Lazy.force
with Not_found ->
errorf "could not find constant `%a`" ID.pp id
in
let l = List.map (conv_term_rec env) l in
if List.length l = fst (Ty.unfold_n (Cst.ty f))
then Term.app_cst f (IArray.of_list l) (* fully applied *)
else Term.app (Term.const f) l
| _ ->
let f = conv_term_rec env f in
let l = List.map (conv_term_rec env) l in
Term.app f l
end
| Ast.Var v ->
(* look whether [v] must be replaced by some term *)
begin match AstVarMap.get v env.subst with
| Some t -> t
| None ->
(* lookup as bound variable *)
begin match CCList.find_idx (Ast.Var.equal v) env.bound with
| None -> errorf "could not find var `%a`" Ast.Var.pp v
| Some (i,_) ->
let ty = Ast.Var.ty v |> conv_ty in
Term.db (DB.make i ty)
end
end
| Ast.Bind (Ast.Fun,v,body) ->
let body = conv_term_rec {env with bound=v::env.bound} body in
let ty = Ast.Var.ty v |> conv_ty in
Term.fun_ ty body
| Ast.Bind ((Ast.Forall | Ast.Exists),_, _) ->
errorf "quantifiers not supported"
| Ast.Bind (Ast.Mu,v,body) ->
let env' = add_bound env v in
let body = conv_term_rec env' body in
Term.mu body
| Ast.Select _ -> assert false (* TODO *)
| Ast.Match (u,m) ->
let any_rhs_depends_vars = ref false in (* some RHS depends on matched arg? *)
let m =
ID.Map.map
(fun (vars,rhs) ->
let n_vars = List.length vars in
let env', tys =
CCList.fold_map
(fun env v -> add_bound env v, Ast.Var.ty v |> conv_ty)
env vars
in
let rhs = conv_term_rec env' rhs in
let depends_on_vars =
Term.to_seq_depth rhs
|> Iter.exists
(fun (t,k) -> match t.term_cell with
| DB db ->
DB.level db < n_vars + k (* [k]: number of intermediate binders *)
| _ -> false)
in
if depends_on_vars then any_rhs_depends_vars := true;
tys, rhs)
m
in
(* optim: check whether all branches return the same term, that
does not depend on matched variables *)
(* TODO: do the closedness check during conversion, above *)
let rhs_l =
ID.Map.values m
|> Iter.map snd
|> Iter.sort_uniq ~cmp:Term.compare
|> Iter.to_rev_list
in
begin match rhs_l with
| [x] when not (!any_rhs_depends_vars) ->
(* every branch yields the same [x], which does not depend
on the argument: remove the match and return [x] instead *)
x
| _ ->
let u = conv_term_rec env u in
Term.match_ u m
end
| Ast.Switch _ ->
errorf "cannot convert switch %a" Ast.pp_term t
| Ast.Let (v,t,u) ->
(* substitute on the fly *)
let t = conv_term_rec env t in
let env' = add_let_bound env v t in
conv_term_rec env' u
| Ast.If (a,b,c) ->
let b = conv_term_rec env b in
let c = conv_term_rec env c in
(* optim: [if _ b b --> b] *)
if Term.equal b c
then b
else Term.if_ (conv_term_rec env a) b c
| Ast.Not t -> Term.not_ (conv_term_rec env t)
| Ast.Binop (op,a,b) ->
let a = conv_term_rec env a in
let b = conv_term_rec env b in
begin match op with
| Ast.And -> Term.and_ a b
| Ast.Or -> Term.or_ a b
| Ast.Imply -> Term.imply a b
| Ast.Eq -> Term.eq a b
end
| Ast.Undefined_value ->
Term.undefined_value (conv_ty t.Ast.ty) Undef_absolute
| Ast.Asserting (t, g) ->
(* [t asserting g] becomes [if g t fail] *)
let t = conv_term_rec env t in
let g = conv_term_rec env g in
Term.if_ g t (Term.undefined_value t.term_ty Undef_absolute)
let add_statement st =
Log.debugf 2
(fun k->k "(@[add_statement@ @[%a@]@])" Ast.pp_statement st);
model_env_ := Ast.env_add_statement !model_env_ st;
begin match st with
| Ast.Assert t ->
let t = conv_term_rec empty_env t in
Top_goals.push t;
push_clause (Clause.make [Lit.atom t])
| Ast.Goal (vars, t) ->
(* skolemize *)
let env, consts =
CCList.fold_map
(fun env v ->
let ty = Ast.Var.ty v |> conv_ty in
let c = Cst.make_undef (Ast.Var.id v) ty in
{env with subst=AstVarMap.add v (Term.const c) env.subst}, c)
empty_env
vars
in
(* model should contain values of [consts] *)
List.iter add_cst_support_ consts;
let t = conv_term_rec env t in
Top_goals.push t;
push_clause (Clause.make [Lit.atom t])
| Ast.TyDecl id ->
let ty = Ty.atomic id Uninterpreted ~card:(Lazy.from_val Infinite) in
add_ty_support_ ty;
ID.Tbl.add ty_tbl_ id (Lazy.from_val ty)
| Ast.Decl (id, ty) ->
assert (not (ID.Tbl.mem decl_ty_ id));
let ty = conv_ty ty in
let cst = Cst.make_undef id ty in
add_cst_support_ cst; (* need it in model *)
ID.Tbl.add decl_ty_ id (Lazy.from_val cst)
| Ast.Data l ->
(* the datatypes in [l]. Used for computing cardinalities *)
let in_same_block : ID.Set.t =
List.map (fun {Ast.Ty.data_id; _} -> data_id) l |> ID.Set.of_list
in
(* declare the type, and all the constructors *)
List.iter
(fun {Ast.Ty.data_id; data_cstors} ->
let ty = lazy (
let card_ : ty_card ref = ref Finite in
let cstors = lazy (
data_cstors
|> ID.Map.map
(fun c ->
let c_id = c.Ast.Ty.cstor_id in
let ty_c = conv_ty c.Ast.Ty.cstor_ty in
let ty_args, ty_ret = Ty.unfold ty_c in
(* add cardinality of [c] to the cardinality of [data_id].
(product of cardinalities of args) *)
let cstor_card =
ty_args
|> List.map
(fun ty_arg -> match ty_arg.ty_cell with
| Atomic (id, _) when ID.Set.mem id in_same_block ->
Infinite
| _ -> Lazy.force ty_arg.ty_card)
|> Ty_card.product
in
card_ := Ty_card.( !card_ + cstor_card );
let rec cst = lazy (
Cst.make_cstor c_id ty_c cstor
) and cstor = lazy (
let cstor_proj = lazy (
let n = ref 0 in
List.map2
(fun id ty_arg ->
let ty_proj = Ty.arrow ty_ret ty_arg in
let i = !n in
incr n;
Cst.make_proj id ty_proj cstor i)
c.Ast.Ty.cstor_proj ty_args
|> IArray.of_list
) in
let cstor_test = lazy (
let ty_test = Ty.arrow ty_ret Ty.prop in
Cst.make_tester c.Ast.Ty.cstor_test ty_test cstor
) in
{ cstor_ty=ty_c; cstor_cst=Lazy.force cst;
cstor_args=IArray.of_list ty_args;
cstor_proj; cstor_test; cstor_card; }
) in
ID.Tbl.add decl_ty_ c_id cst; (* declare *)
Lazy.force cstor)
)
in
let data = { data_cstors=cstors; } in
let card = lazy (
ignore (Lazy.force cstors);
let r = !card_ in
Log.debugf 5
(fun k->k "(@[card_of@ %a@ %a@])" ID.pp data_id Ty_card.pp r);
r
) in
Ty.atomic data_id (Data data) ~card
) in
ID.Tbl.add ty_tbl_ data_id ty;
)
l;
(* force evaluation *)
List.iter
(fun {Ast.Ty.data_id; _} ->
let lazy ty = ID.Tbl.find ty_tbl_ data_id in
ignore (Lazy.force ty.ty_card);
begin match ty.ty_cell with
| Atomic (_, Data {data_cstors=lazy _; _}) -> ()
| _ -> assert false
end)
l
| Ast.Define (k,l) ->
(* declare the mutually recursive functions *)
List.iter
(fun (id,ty,rhs) ->
let ty = conv_ty ty in
let rhs = lazy (conv_term_rec empty_env rhs) in
let k = match k with
| Ast.Recursive -> Cst_recursive
| Ast.Non_recursive -> Cst_non_recursive
in
let cst = lazy (
Cst.make_defined id ty rhs k
) in
ID.Tbl.add decl_ty_ id cst)
l;
(* force thunks *)
List.iter
(fun (id,_,_) -> ignore (ID.Tbl.find decl_ty_ id |> Lazy.force))
l
end
let add_statement_l = List.iter add_statement
module A = Ast
let rec ty_to_ast (t:Ty.t): A.Ty.t = match t.ty_cell with
| Prop -> A.Ty.Prop
| Atomic (id,_) -> A.Ty.const id
| Arrow (a,b) -> A.Ty.arrow (ty_to_ast a) (ty_to_ast b)
let fresh_var =
let n = ref 0 in
fun ty ->
let id = ID.makef "x%d" !n in
incr n;
A.Var.make id (ty_to_ast ty)
let with_var ty env ~f =
let v = fresh_var ty in
let env = DB_env.push (A.var v) env in
f v env
let term_to_ast (t:term): Ast.term =
let rec aux env t = match t.term_cell with
| True -> A.true_
| False -> A.false_
| DB d ->
begin match DB_env.get d env with
| Some t' -> t'
| None -> errorf "cannot find DB %a in env" Term.pp t
end
| App_cst (f, args) when IArray.is_empty args ->
A.const f.cst_id (ty_to_ast t.term_ty)
| App_cst (f, args) ->
let f = A.const f.cst_id (ty_to_ast (Cst.ty f)) in
let args = IArray.map (aux env) args in
A.app f (IArray.to_list args)
| App_ho (f,l) -> A.app (aux env f) (List.map (aux env) l)
| Fun (ty,bod) ->
with_var ty env
~f:(fun v env -> A.fun_ v (aux env bod))
| Mu _ -> assert false
| If (a,b,c) -> A.if_ (aux env a)(aux env b) (aux env c)
| Case (u,m) ->
let u = aux env u in
let m =
ID.Map.mapi
(fun _c_id _rhs ->
assert false (* TODO: fetch cstor; bind variables; convert rhs *)
(*
with_vars tys env ~f:(fun vars env -> vars, aux env rhs)
*)
)
m
in
A.match_ u m
| Builtin b ->
begin match b with
| B_not t -> A.not_ (aux env t)
| B_and (a,b) -> A.and_ (aux env a) (aux env b)
| B_or (a,b) -> A.or_ (aux env a) (aux env b)
| B_eq (a,b) -> A.eq (aux env a) (aux env b)
| B_imply (a,b) -> A.imply (aux env a) (aux env b)
end
in aux DB_env.empty t
end
*)
let th_bool : Solver.theory =
Th_bool.theory

View file

@ -1,7 +1,14 @@
(** {1 Process Statements} *)
open Sidekick_smt
open Sidekick_base_term
module Solver
: Sidekick_msat_solver.S with type A.Term.t = Term.t
and type A.Term.state = Term.state
and type A.Lit.t = Lit.t
and type A.Ty.t = Ty.t
val th_bool : Solver.theory
type 'a or_error = ('a, string) CCResult.t
@ -11,6 +18,11 @@ val conv_ty : Ast.Ty.t -> Ty.t
val conv_term : Term.state -> Ast.term -> Term.t
module Check_cc : sig
(** theory that check validity of conflicts *)
val theory : Solver.theory
end
val process_stmt :
?hyps:Lit.t list Vec.t ->
?gc:bool ->

View file

@ -1,11 +1,17 @@
(** {1 Process Statements} *)
module ID = Sidekick_base_term.ID
module Fmt = CCFormat
module Ast = Sidekick_smt.Ast
module Ast = Ast
module E = CCResult
module Loc = Locations
module Process = Process
module Solver = Process.Solver
module Proof = struct
type t = Proof_default
let default = Proof_default
end
type 'a or_error = ('a, string) CCResult.t
@ -15,10 +21,6 @@ module Parse = struct
Loc.set_file lexbuf filename;
Parser.parse_list Lexer.token lexbuf
let parse_chan ?filename ic =
try Result.Ok (parse_chan_exn ?filename ic)
with e -> Result.Error (Printexc.to_string e)
let parse_file_exn file : Parse_ast.statement list =
CCIO.with_in file (parse_chan_exn ~filename:file)
@ -45,5 +47,183 @@ module Parse = struct
with e -> Result.Error (Printexc.to_string e)
end
(* TODO: remove
module Term_bool : sig
open Sidekick_th_bool_dyn
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
end = struct
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
end
*)
module Theories = struct
(* TODO
module Th_cstor = Sidekick_th_cstor.Make(struct
module Solver = Solver
module T = Solver.A.Term
let[@inline] view_as_cstor t = match view t with
| App_cst (c, args) when Fun.do_cc
| If (a,b,c) -> T_ite (a,b,c)
| Bool b -> T_bool b
| _ -> T_other t
end
end)
*)
end
let parse = Parse.parse
let parse_stdin = Parse.parse_stdin

View file

@ -1,4 +1,3 @@
(** {1 SMTLib-2 Interface} *)
(** This library provides a parser, a type-checker, and a solver interface
@ -7,10 +6,10 @@
type 'a or_error = ('a, string) CCResult.t
module Ast = Sidekick_smt.Ast
module Ast = Ast
module Process = Process
module Solver = Process.Solver
val parse : string -> Ast.statement list or_error
val parse_stdin : unit -> Ast.statement list or_error

View file

@ -1,14 +1,13 @@
(* This file is free software. See file "license" for more details. *)
(** {1 Preprocessing AST} *)
module ID = Sidekick_smt.ID
open Sidekick_base_term
module Loc = Locations
module Fmt = CCFormat
module Log = Msat.Log
module A = Sidekick_smt.Ast
module A = Ast
module PA = Parse_ast
type 'a or_error = ('a, string) CCResult.t
@ -17,11 +16,7 @@ let pp_loc_opt = Loc.pp_opt
(** {2 Parsing} *)
module StrTbl = CCHashtbl.Make(struct
type t = string
let equal = CCString.equal
let hash = CCString.hash
end)
module StrTbl = CCHashtbl.Make(CCString)
module Ctx = struct
type kind =
@ -325,13 +320,6 @@ let rec conv_term ctx (t:PA.term) : A.term = match t with
| _ ->
errorf_ctx ctx "unsupported term %a" PA.pp_term t
let find_file_ name ~dir : string option =
Log.debugf 2 (fun k->k "search %s in %s" name dir);
let abs_path = Filename.concat dir name in
if Sys.file_exists abs_path
then Some abs_path
else None
let conv_fun_decl ctx f : string * A.Ty.t =
if f.PA.fun_ty_vars <> [] then (
errorf_ctx ctx "cannot convert polymorphic function@ %a"

View file

@ -1,4 +1,3 @@
(* This file is free software. See file "license" for more details. *)
(** {1 Preprocessing AST} *)
@ -16,7 +15,7 @@ module Ctx : sig
end
module PA = Parse_ast
module A = Sidekick_smt.Ast
module A = Ast
val conv_term : Ctx.t -> PA.term -> A.term

View file

@ -1,11 +1,13 @@
(library
(name sidekick_smtlib)
(public_name sidekick.smtlib)
(libraries containers zarith msat sidekick.smt sidekick.util
sidekick.smt.th-bool sidekick.smt.th-distinct msat.backend)
(flags :standard -open Sidekick_util))
(name sidekick_smtlib)
(public_name sidekick.smtlib)
(libraries containers zarith msat sidekick.core sidekick.util
sidekick.msat-solver sidekick.base-term sidekick.th-bool-static
sidekick.mini-cc msat.backend)
(flags :standard -open Sidekick_util))
(menhir (modules Parser))
(menhir
(modules Parser))
(ocamllex (modules Lexer))
(ocamllex
(modules Lexer))

View file

@ -0,0 +1,128 @@
(** {1 Theory of Booleans} *)
(** {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 type ARG = sig
module S : Sidekick_core.SOLVER
type term = S.A.Term.t
val view_as_bool : term -> term View.t
val mk_bool : S.A.Term.state -> term View.t -> term
end
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 SI = A.S.Solver_internal
module T = SI.A.Term
module Lit = SI.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:SI.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 ();
SI.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 = SI.mk_lit solver sub in
SI.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 (SI.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 = SI.mk_lit solver ~sign:false sub in
SI.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 (SI.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 =
SI.mk_lit solver concl :: Lit.neg lit ::
List.map (SI.mk_lit solver ~sign:false) guard in
add_axiom c
) else if not @@ Lit.sign lit then (
(* propagate [¬lit => ¬concl] *)
SI.propagate_l solver (SI.mk_lit solver ~sign:false concl) [lit];
(* propagate [¬lit => ∧_i guard_i] *)
IArray.iter
(fun sub ->
let sublit = SI.mk_lit solver ~sign:true sub in
SI.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:SI.t) : t =
let self = {expanded=T_tbl.create 24} in
SI.on_final_check solver (final_check self);
SI.on_partial_check solver (partial_check self);
self
let theory =
A.S.mk_theory ~name:"boolean" ~create_and_setup ()
end

6
src/th-bool-dyn/dune.bak Normal file
View file

@ -0,0 +1,6 @@
(library
(name Sidekick_th_bool_dyn)
(public_name sidekick.th-bool-dyn)
(libraries containers sidekick.core sidekick.util)
(flags :standard -open Sidekick_util))

View file

@ -0,0 +1,189 @@
(** {2 Signatures for booleans} *)
type 'a bool_view =
| B_bool of bool
| B_not of 'a
| B_and of 'a IArray.t
| B_or of 'a IArray.t
| B_imply of 'a IArray.t * 'a
| B_equiv of 'a * 'a
| B_eq of 'a * 'a
| B_ite of 'a * 'a * 'a
| B_atom of 'a
module type ARG = sig
module S : Sidekick_core.SOLVER
type term = S.A.Term.t
val view_as_bool : term -> term bool_view
(** Project the term into the boolean view *)
val mk_bool : S.A.Term.state -> term bool_view -> term
(** Make a term from the given boolean view *)
module Gensym : sig
type t
val create : S.A.Term.state -> t
val fresh_term : t -> pre:string -> S.A.Ty.t -> term
(** Make a fresh term of the given type *)
end
end
module type S = sig
module A : ARG
module T = A.S.A.Term
module SI = A.S.Solver_internal
type state
val create : T.state -> state
val simplify : state -> SI.simplify_hook
(** Simplify given term *)
val cnf : state -> SI.preprocess_hook
(** add clauses for the booleans within the term. *)
val theory : A.S.theory
end
module Make(A : ARG) : S with module A = A = struct
module A = A
module Ty = A.S.A.Ty
module T = A.S.A.Term
module Lit = A.S.A.Lit
module SI = A.S.Solver_internal
type state = {
tst: T.state;
simps: T.t T.Tbl.t; (* cache *)
cnf: Lit.t T.Tbl.t; (* tseitin CNF *)
cnf_ite: T.t T.Tbl.t; (* proxies for "ite" *)
gensym: A.Gensym.t;
}
let create tst : state =
{ tst; simps=T.Tbl.create 128;
cnf=T.Tbl.create 128; cnf_ite=T.Tbl.create 32;
gensym=A.Gensym.create tst;
}
let[@inline] not_ tst t = A.mk_bool tst (B_not t)
let[@inline] and_a tst a = A.mk_bool tst (B_and a)
let[@inline] or_a tst a = A.mk_bool tst (B_or a)
let[@inline] ite tst a b c = A.mk_bool tst (B_ite (a,b,c))
let[@inline] equiv tst a b = A.mk_bool tst (B_equiv (a,b))
let[@inline] eq tst a b = A.mk_bool tst (B_eq (a,b))
let is_true t = match T.as_bool t with Some true -> true | _ -> false
let is_false t = match T.as_bool t with Some false -> true | _ -> false
let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : T.t option =
let tst = self.tst in
match A.view_as_bool t with
| B_bool _ -> None
| B_not u when is_true u -> Some (T.bool tst false)
| B_not u when is_false u -> Some (T.bool tst true)
| B_not _ -> None
| B_and a ->
if IArray.exists is_false a then Some (T.bool tst false)
else if IArray.for_all is_true a then Some (T.bool tst true)
else None
| B_or a ->
if IArray.exists is_true a then Some (T.bool tst true)
else if IArray.for_all is_false a then Some (T.bool tst false)
else None
| B_imply (args, u) ->
(* turn into a disjunction *)
let u =
or_a tst @@
IArray.append (IArray.map (not_ tst) args) (IArray.singleton u)
in
Some u
| B_ite (a,b,c) ->
(* directly simplify [a] so that maybe we never will simplify one
of the branches *)
let a = SI.Simplify.normalize simp a in
begin match A.view_as_bool a with
| B_bool true -> Some b
| B_bool false -> Some c
| _ -> None
end
| B_equiv (a,b) when is_true a -> Some b
| B_equiv (a,b) when is_false a -> Some (not_ tst b)
| B_equiv (a,b) when is_true b -> Some a
| B_equiv (a,b) when is_false b -> Some (not_ tst a)
| B_equiv _ -> None
| B_eq (a,b) when T.equal a b -> Some (T.bool tst true)
| B_eq _ -> None
| B_atom _ -> None
let fresh_term self ~pre ty = A.Gensym.fresh_term self.gensym ~pre ty
let fresh_lit (self:state) ~pre : Lit.t =
let t = fresh_term ~pre self Ty.bool in
Lit.atom self.tst t
(* TODO: polarity? *)
let cnf (self:state) (_solver:SI.t) ~add_clause (t:T.t) : T.t option =
let rec get_lit (t:T.t) : Lit.t =
match A.view_as_bool t with
| B_bool b -> Lit.atom self.tst ~sign:b (T.bool self.tst true)
| B_not u ->
let lit = get_lit u in
Lit.neg lit
| B_and l ->
let subs = IArray.to_list_map get_lit l in
let proxy = fresh_lit ~pre:"and_" self in
(* add clauses *)
List.iter (fun u -> add_clause [Lit.neg proxy; u]) subs;
add_clause (proxy :: List.map Lit.neg subs);
proxy
| B_or l ->
let subs = IArray.to_list_map get_lit l in
let proxy = fresh_lit ~pre:"or_" self in
(* add clauses *)
List.iter (fun u -> add_clause [Lit.neg u; proxy]) subs;
add_clause (Lit.neg proxy :: subs);
proxy
| B_imply (args, u) ->
let t' =
or_a self.tst @@
IArray.append (IArray.map (not_ self.tst) args) (IArray.singleton u) in
get_lit t'
| B_ite _ | B_eq _ ->
Lit.atom self.tst t
| B_equiv (a,b) ->
let a = get_lit a in
let b = get_lit b in
let proxy = fresh_lit ~pre:"equiv_" self in
(* proxy => a<=> b,
¬proxy => a xor b *)
add_clause [Lit.neg proxy; Lit.neg a; b];
add_clause [Lit.neg proxy; Lit.neg b; a];
add_clause [proxy; a; b];
add_clause [proxy; Lit.neg a; Lit.neg b];
proxy
| B_atom u -> Lit.atom self.tst u
in
let lit = get_lit t in
let u = Lit.term lit in
(* put sign back as a "not" *)
let u = if Lit.sign lit then u else A.mk_bool self.tst (B_not u) in
if T.equal u t then None else Some u
let create_and_setup si =
Log.debug 2 "(th-bool.setup)";
let st = create (SI.tst si) in
SI.add_simplifier si (simplify st);
SI.add_preprocess si (cnf st);
st
let theory =
A.S.mk_theory
~name:"th-bool"
~create_and_setup
()
end

5
src/th-bool-static/dune Normal file
View file

@ -0,0 +1,5 @@
(library
(name sidekick_th_bool_static)
(public_name sidekick.th-bool-static)
(flags :standard -open Sidekick_util)
(libraries sidekick.core sidekick.util))

View file

@ -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

View file

@ -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

View file

@ -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

View file

@ -1,22 +0,0 @@
(** {1 Theory of Booleans} *)
type term = Sidekick_smt.Term.t
module Intf = Bool_intf
module Bool_term = Bool_term
module Th_dyn_tseitin = Th_dyn_tseitin
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
module type BOOL_TERM = Intf.BOOL_TERM
(** Dynamic Tseitin transformation *)
let th_dynamic_tseitin =
let module Th = Th_dyn_tseitin.Make(Bool_term) in
Th.th

View file

@ -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

View file

@ -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

View file

@ -1,6 +0,0 @@
(library
(name Sidekick_th_bool)
(public_name sidekick.smt.th-bool)
(libraries containers sidekick.smt)
(flags :standard -open Sidekick_util))

View file

@ -1,95 +1,80 @@
(** {1 Theory for constructors} *)
type ('c,'t) cstor_view =
| T_cstor of 'c * 't list
| T_other of 't
module type S = sig
type lit
type term
(** Micro theory only *)
val cc_th : Sidekick_smt.CC.Theory.t
end
let name = "th-cstor"
module type ARG = sig
module Fun : sig
type t
val equal : t -> t -> bool
end
module T : sig
type t
val pp : t Fmt.printer
val equal : t -> t -> bool
val view_as_cstor : t -> (Fun.t,t) cstor_view
end
module S : Sidekick_core.SOLVER
val view_as_cstor : S.A.Term.t -> (S.A.Fun.t, S.A.Term.t) cstor_view
end
module Make(Arg : ARG with type T.t = Sidekick_smt.Term.t)
(* : S with type lit = Arg.Lit.t and type term = Arg.T.t *)
= struct
module N = Sidekick_smt.Theory.CC_eq_class
module Expl = Sidekick_smt.Theory.CC_expl
module CC = Sidekick_smt.CC
module type S = sig
module A : ARG
val theory : A.S.theory
end
open Arg
type term = T.t
module Make(A : ARG) : S with module A = A = struct
module A = A
module SI = A.S.Solver_internal
module T = A.S.A.Term
module N = SI.N
module Fun = A.S.A.Fun
module Expl = SI.Expl
type data = {
type cstor_repr = {
t: T.t;
n: N.t;
}
(* associate to each class a unique constructor term in the class (if any) *)
let pp_data out x = T.pp out x.t
(* TODO
module N_tbl = Backtrackable_tbl.Make(N)
*)
module N_tbl = CCHashtbl.Make(N)
let key : (_,_,data) Sidekick_cc.Key.t = Sidekick_cc.Key.create
~pp:pp_data ~name:"cstor"
~eq:(fun x y -> T.equal x.t y.t)
~merge:(fun x _ -> x) ()
type t = {
cstors: T.t N_tbl.t; (* repr -> cstor for the class *)
(* TODO: also allocate a bit in CC to filter out quickly classes without cstors *)
}
type t = unit
let on_merge (cc:CC.t) n1 tc1 n2 tc2 e_n1_n2 : unit =
let on_merge (solver:SI.t) n1 tc1 n2 tc2 e_n1_n2 : unit =
Log.debugf 5
(fun k->k "(@[th-cstor.on_merge@ @[:c1 %a@ (term %a)@]@ @[:c2 %a@ (term %a)@]@])"
N.pp n1 T.pp tc1.t N.pp n2 T.pp tc2.t);
let expl = Expl.mk_list [e_n1_n2; Expl.mk_merge n1 tc1.n; Expl.mk_merge n2 tc2.n] in
match T.view_as_cstor tc1.t, T.view_as_cstor tc2.t with
match A.view_as_cstor tc1.t, A.view_as_cstor tc2.t with
| T_cstor (f1, l1), T_cstor (f2, l2) ->
if Arg.Fun.equal f1 f2 then (
(* merging two constructor terms: injectivity + disjointness checks *)
if Fun.equal f1 f2 then (
(* same function: injectivity *)
assert (List.length l1 = List.length l2);
List.iter2
(fun u1 u2 -> CC.Theory.merge cc (CC.add_term cc u1) (CC.add_term cc u2) expl)
(fun u1 u2 -> SI.cc_merge_t solver u1 u2 expl)
l1 l2
) else (
(* different function: disjointness *)
CC.Theory.raise_conflict cc expl
SI.cc_raise_conflict solver expl
)
| _ -> assert false
(* attach data to constructor terms *)
let on_new_term _ n (t:T.t) =
match T.view_as_cstor t with
match A.view_as_cstor t with
| T_cstor _ -> Some {t;n}
| _ -> None
let cc_th = Sidekick_smt.CC.Theory.make ~key ~on_new_term ~on_merge ()
let create_and_setup (_solver:SI.t) : t =
let self = {
cstors=N_tbl.create 32;
} in
(* TODO
SI.on_cc_merge solver on_merge;
SI.on_cc_new_term solver on_new_term;
*)
self
let theory = A.S.mk_theory ~name ~create_and_setup ()
end
(* TODO: default building of constructor terms
include Make(struct
module Fun = Sidekick_smt.Cst
module T = struct
include Sidekick_smt.Term
let[@inline] view_as_cstor t = match view t with
| App_cst (c, args) when Fun.do_cc
| If (a,b,c) -> T_ite (a,b,c)
| Bool b -> T_bool b
| _ -> T_other t
end
end)
*)

View file

@ -2,6 +2,6 @@
(library
(name Sidekick_th_cstor)
(public_name sidekick.smt.th-cstor)
(libraries containers sidekick.smt)
(libraries containers sidekick.core sidekick.util)
(flags :standard -open Sidekick_util))

View file

@ -1,216 +0,0 @@
module Term = Sidekick_smt.Term
module Theory = Sidekick_smt.Theory
module type ARG = sig
module T : sig
type t
type state
val pp : t Fmt.printer
val equal : t -> t -> bool
val hash : t -> int
val as_distinct : t -> t Iter.t option
val mk_eq : state -> t -> t -> t
end
module Lit : sig
type t
val term : t -> T.t
val neg : t -> t
val sign : t -> bool
val compare : t -> t -> int
val atom : T.state -> ?sign:bool -> T.t -> t
val pp : t Fmt.printer
end
end
module type S = sig
type term
type term_state
type lit
type data
val key : (term, lit, data) Sidekick_cc.Key.t
val th : Sidekick_smt.Theory.t
end
module Make(A : ARG with type Lit.t = Sidekick_smt.Lit.t
and type T.t = Sidekick_smt.Term.t
and type T.state = Sidekick_smt.Term.state) = struct
module T = A.T
module Lit = A.Lit
module IM = CCMap.Make(Lit)
type term = T.t
type term_state = T.state
type lit = A.Lit.t
type data = term IM.t (* "distinct" lit -> term appearing under it*)
let pp_data out m =
Fmt.fprintf out
"{@[%a@]}" Fmt.(seq ~sep:(return ",@ ") @@ pair Lit.pp T.pp) (IM.to_seq m)
let key : (term,lit,data) Sidekick_cc.Key.t =
let merge m1 m2 =
IM.merge_safe m1 m2
~f:(fun _ pair -> match pair with
| `Left x | `Right x -> Some x
| `Both (x,_) -> Some x)
and eq = IM.equal T.equal in
Sidekick_cc.Key.create
~pp:pp_data
~name:"distinct"
~merge ~eq ()
(* micro theory *)
module Micro(CC : Sidekick_cc.Congruence_closure.S
with type term = T.t
and type lit = Lit.t
and module Key = Sidekick_cc.Key) = struct
exception E_exit
let on_merge cc n1 m1 n2 m2 expl12 =
Log.debugf 5
(fun k->k "(@[th_distinct.on_merge@ @[:n1 %a@ :map2 %a@]@ @[:n2 %a@ :map2 %a@]@])"
CC.N.pp n1 pp_data m1 CC.N.pp n2 pp_data m2);
try
let _i =
IM.merge
(fun lit o1 o2 ->
match o1, o2 with
| Some t1, Some t2 ->
(* conflict! two terms under the same "distinct" [lit]
are merged, where [lit = distinct(t1,t2,)].
The conflict is:
[lit, t1=n1, t2=n2, expl-merge(n1,n2) ==> false]
*)
assert (not @@ T.equal t1 t2);
let expl = CC.Expl.mk_list
[expl12;
CC.Expl.mk_lit lit;
CC.Expl.mk_merge n1 (CC.Theory.add_term cc t1);
CC.Expl.mk_merge n2 (CC.Theory.add_term cc t2);
] in
CC.Theory.raise_conflict cc expl;
raise_notrace E_exit
| _ -> None)
m1 m2
in
()
with E_exit -> ()
let on_new_term _ _ _ = None
let th =
CC.Theory.make ~key ~on_merge ~on_new_term ()
end
module T_tbl = CCHashtbl.Make(T)
type st = {
tst: T.state;
expanded: unit T_tbl.t; (* negative "distinct" that have been case-split on *)
}
let create tst : st = { expanded=T_tbl.create 12; tst; }
let pp_c out c = Fmt.fprintf out "(@[<hv>%a@])" (Util.pp_list Lit.pp) c
module CC = Sidekick_smt.CC
let process_lit (st:st) (acts:Theory.actions) (lit:Lit.t) (lit_t:term) (subs:term Iter.t) : unit =
let (module A) = acts in
Log.debugf 5 (fun k->k "(@[th_distinct.process@ %a@])" Lit.pp lit);
let add_axiom c = A.add_persistent_axiom c in
let cc = A.cc in
if Lit.sign lit then (
(* assert [distinct subs], so we update the node of each [t in subs]
with [lit] *)
(* FIXME: detect if some subs are already equal *)
subs
(fun sub ->
let n = CC.Theory.add_term cc sub in
CC.Theory.add_data cc n key (IM.singleton lit sub));
) else if not @@ T_tbl.mem st.expanded lit_t then (
(* add clause [distinct t1…tn _{i,j>i} t_i=j] *)
T_tbl.add st.expanded lit_t ();
let l = Iter.to_list subs in
let c =
Iter.diagonal_l l
|> Iter.map (fun (t,u) -> Lit.atom st.tst @@ T.mk_eq st.tst t u)
|> Iter.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
)
let partial_check st (acts:Theory.actions) lits : unit =
lits
(fun lit ->
let t = Lit.term lit in
match T.as_distinct t with
| None -> ()
| Some subs -> process_lit st acts lit t subs)
let cc_th = let module T = Micro(CC) in T.th
let th =
Sidekick_smt.Theory.make
~name:"distinct"
~partial_check
~final_check:(fun _ _ _ -> ())
~cc_th:(fun _ -> [cc_th])
~create ()
end
module Arg = struct
open Sidekick_smt
open Sidekick_smt.Solver_types
let id_distinct = ID.make "distinct"
let relevant _id _ _ = true
let get_ty _ _ = Ty.prop
let abs ~self _a = self, true
module T = struct
include Term
let mk_eq = eq
let as_distinct t : _ option =
match view t with
| App_cst ({cst_id;_}, args) when ID.equal cst_id id_distinct ->
Some (IArray.to_seq args)
| _ -> None
end
module Lit = Sidekick_smt.Lit
let eval args =
let module Value = Sidekick_smt.Value in
Log.debugf 5
(fun k->k "(@[distinct.eval@ %a@])" (Fmt.seq Value.pp) (IArray.to_seq args));
if
Iter.diagonal (IArray.to_seq args)
|> Iter.for_all (fun (x,y) -> not @@ Value.equal x y)
then Value.true_
else Value.false_
let c_distinct =
{cst_id=id_distinct;
cst_view=Cst_def {
pp=None; abs; ty=get_ty; relevant; do_cc=true; eval; }; }
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)
end
let distinct = Arg.distinct
let distinct_l = Arg.distinct_l
include Make(Arg)

View file

@ -1,53 +0,0 @@
(** {1 Theory of "distinct"}
This is an extension of the congruence closure that handles
"distinct" efficiently.
*)
module Term = Sidekick_smt.Term
module type ARG = sig
module T : sig
type t
type state
val pp : t Fmt.printer
val equal : t -> t -> bool
val hash : t -> int
val as_distinct : t -> t Iter.t option
val mk_eq : state -> t -> t -> t
end
module Lit : sig
type t
val term : t -> T.t
val neg : t -> t
val sign : t -> bool
val compare : t -> t -> int
val atom : T.state -> ?sign:bool -> T.t -> t
val pp : t Fmt.printer
end
end
module type S = sig
type term
type term_state
type lit
type data
val key : (term, lit, data) Sidekick_cc.Key.t
val th : Sidekick_smt.Theory.t
end
(* TODO: generalize theories *)
module Make(A : ARG with type T.t = Sidekick_smt.Term.t
and type T.state = Sidekick_smt.Term.state
and type Lit.t = Sidekick_smt.Lit.t) :
S with type term = A.T.t
and type lit = A.Lit.t
and type term_state = A.T.state
val distinct : Term.state -> Term.t IArray.t -> Term.t
val distinct_l : Term.state -> Term.t list -> Term.t
(** Default instance *)
include S with type term = Term.t and type lit = Sidekick_smt.Lit.t

View file

@ -1,7 +0,0 @@
(library
(name Sidekick_th_distinct)
(public_name sidekick.smt.th-distinct)
(libraries containers sidekick.smt)
(flags :standard -open Sidekick_util))

View file

@ -1,113 +0,0 @@
(** {1 Theory for if-then-else} *)
type 't ite_view =
| T_ite of 't * 't * 't
| T_bool of bool
| T_other of 't
module type S = sig
type lit
type term
val th : Sidekick_smt.Theory.t
end
module type ARG = sig
module T : sig
type t
type state
val pp : t Fmt.printer
val equal : t -> t -> bool
val view_as_ite : t -> t ite_view
module Set : CCSet.S with type elt = t
end
module Lit : sig
type t
val term : t -> T.t
val atom : T.state -> ?sign:bool -> T.t -> t
val pp : t Fmt.printer
end
end
module Make(Arg : ARG with type T.state = Sidekick_smt.Term.state and type T.t = Sidekick_smt.Term.t)
: S with type lit = Arg.Lit.t and type term = Arg.T.t
= struct
module Th = Sidekick_smt.Theory
module N = Th.CC_eq_class
module Expl = Th.CC_expl
module CC = Sidekick_smt.CC
open Arg
type lit = Lit.t
type term = T.t
type data = T.Set.t
(* associate to each class [t] the set of [ite a b c] where [a=t] *)
let pp_data = Fmt.(map T.Set.to_seq @@ seq ~sep:(return ",@ ") T.pp)
let key : (_,_,data) Sidekick_cc.Key.t = Sidekick_cc.Key.create
~pp:pp_data ~name:"ite" ~eq:T.Set.equal ~merge:T.Set.union ()
type t = T.state
let on_merge (_st:t) (acts:Sidekick_smt.Theory.actions) n1 n2 e_n1_n2 : unit =
let (module A) = acts in
Log.debugf 5
(fun k->k "(@[th-ite.on_merge@ :c1 %a@ :c2 %a@])" N.pp n1 N.pp n2);
(* check if [n1] has some [ite] parents, and if [n2] is true/false *)
let check_ n1 n2 =
match CC.Theory.get_data A.cc n1 key, T.view_as_ite (N.term n2) with
| Some set, T_bool n2_true ->
assert (not @@ T.Set.is_empty set);
T.Set.iter
(fun parent_1 -> match T.view_as_ite parent_1 with
| T_ite (a1,b1,c1) ->
let n_parent1 = CC.add_term A.cc parent_1 in
let expl = Expl.mk_list [e_n1_n2; Expl.mk_merge n1 (CC.add_term A.cc a1)] in
if n2_true then (
(* [a1 = n1 = n2 = true] so [if a1 b1 c1 = b1] *)
CC.Theory.merge A.cc n_parent1 (CC.add_term A.cc b1) expl
) else (
(* [a1 = n1 = n2 = false] so [if a1 b1 c1 = c1] *)
CC.Theory.merge A.cc n_parent1 (CC.add_term A.cc c1) expl
)
| _ -> assert false)
set
| _ -> ()
in
check_ n1 n2;
check_ n2 n1;
()
let on_new_term _ (acts:Sidekick_smt.Theory.actions) (t:T.t) =
let (module A) = acts in
match T.view_as_ite t with
| T_ite (a,_,_) ->
(* add [t] to parents of [a] *)
let n_a = CC.find A.cc @@ CC.add_term A.cc a in
CC.Theory.add_data A.cc n_a key (T.Set.singleton t)
| _ -> ()
let th =
Sidekick_smt.Theory.make ~name:"ite" ~create:(fun st->st)
~on_merge ~final_check:(fun _ _ _ -> ())
~on_new_term
()
end
include Make(struct
module T = struct
include Sidekick_smt.Term
let[@inline] view_as_ite t = match view t with
| If (a,b,c) -> T_ite (a,b,c)
| Bool b -> T_bool b
| _ -> T_other t
end
module Lit = Sidekick_smt.Lit
end)

View file

@ -1,8 +0,0 @@
(library
(name Sidekick_th_ite)
(public_name sidekick.smt.th-ite)
(libraries containers sidekick.smt)
(flags :standard -open Sidekick_util))

View file

@ -4,7 +4,7 @@ import sys, csv, argparse
def read_csv(f):
with open(f) as fd:
content = fd.readlines()[1:]
content = fd.readlines()
return list(csv.DictReader(content))
def analyze_file(f, potential_errors=False):

38
src/util/Event.ml Normal file
View file

@ -0,0 +1,38 @@
type 'a small_set =
| S0
| S1 of 'a
| S2 of 'a * 'a
| S3 of 'a * 'a * 'a * 'a small_set
type 'a t = {
mutable set: ('a -> unit) small_set;
}
let[@unroll 1] rec cons_ f set = match set with
| S0 -> S1 f
| S1 f2 -> S2(f,f2)
| S2(f2,f3) -> S3 (f,f2,f3, S0)
| S3(f1,f2,f3,tl) -> S3 (f,f1,f2,cons_ f3 tl)
let on (e:_ t) f : unit =
let set' = cons_ f e.set in
e.set <- set'
module Emitter = struct
type nonrec 'a t = 'a t
let rec fire_set_ set x =
match set with
| S0 -> ()
| S1 f -> f x
| S2 (f1,f2) -> f1 x; f2 x
| S3 (f1,f2,f3,tl) -> f1 x; f2 x; f3 x; fire_set_ tl x
let[@inline] fire e x = fire_set_ e.set x
end
let make () =
let e = {set=S0} in
e, e

15
src/util/Event.mli Normal file
View file

@ -0,0 +1,15 @@
(** {1 Observer pattern} *)
type 'a t
val on : 'a t -> ('a -> unit) -> unit
module Emitter : sig
type 'a t
val fire : 'a t -> 'a -> unit
end
val make : unit -> 'a t * 'a Emitter.t

View file

@ -1,8 +1,4 @@
(library
(name sidekick_util)
(public_name sidekick.util)
(libraries containers iter msat)
(flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)
(ocamlopt_flags :standard -O3 -bin-annot
-unbox-closures -unbox-closures-factor 20)
)
(libraries containers iter msat))

View file

@ -5,7 +5,7 @@ default_expect = "sat"
[sidekick]
binary = "./sidekick"
cmd = "./sidekick -no-check -time $timeout $file"
cmd = "./sidekick --no-check --time $timeout $file"
unsat = "Unsat"
sat = "Sat"
unknown = "Timeout|Unknown"
@ -20,7 +20,7 @@ sat = ":status sat"
[test]
timeout=10
problems = ".*\\.(smt2|cnf)"
problems = ".*\\.smt2"
provers = [ "sidekick", ]
dir = [ "." ]