From 2e7ab9ba9b76004a8e1d9a2a777e905af839fe2c Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 5 Jun 2019 16:53:13 -0500 Subject: [PATCH] wip: simplify a lot and only keep th-bool-static in the functor --- Makefile | 19 +- src/base-term/Base_types.ml | 740 +++++++++++++++++- src/base-term/Cst.ml | 41 - src/base-term/Cst.mli | 22 - src/base-term/Lit.ml | 34 - src/base-term/Lit.mli | 25 - src/base-term/Model.ml | 37 +- src/base-term/Model.mli | 5 +- src/base-term/Sidekick_base_term.ml | 23 +- src/base-term/Term.ml | 147 ---- src/base-term/Term.mli | 67 -- src/base-term/Term_cell.ml | 120 --- src/base-term/Term_cell.mli | 42 - src/base-term/Ty.ml | 94 --- src/base-term/Ty.mli | 41 - src/base-term/Ty_card.ml | 19 - src/base-term/Ty_card.mli | 17 - src/base-term/Value.ml | 23 - src/base-term/Value.mli | 24 - src/cc/Sidekick_cc.ml | 127 ++- src/cc/Sidekick_cc.mli | 2 +- src/core/Sidekick_core.ml | 246 +++--- src/main/main.ml | 18 +- src/msat-solver/Sidekick_msat_solver.ml | 384 ++++----- src/msat-solver/dune | 11 +- src/{base-term => smtlib}/Ast.ml | 3 +- src/{base-term => smtlib}/Ast.mli | 3 +- src/smtlib/Locations.ml | 1 - src/smtlib/Process.ml | 626 ++++++--------- src/smtlib/Process.mli | 11 +- src/smtlib/Sidekick_smtlib.ml | 73 +- src/smtlib/Sidekick_smtlib.mli | 5 +- src/smtlib/Typecheck.ml | 5 +- src/smtlib/Typecheck.mli | 3 +- src/smtlib/dune | 19 +- .../Sidekick_th_bool_dyn.ml} | 1 - src/{th-bool/dune => th-bool-dyn/dune.bak} | 4 +- src/th-bool-static/Sidekick_th_bool_static.ml | 260 ++++++ src/th-bool-static/dune | 5 + src/th-cstor/Sidekick_th_cstor.ml | 32 +- src/th-cstor/{dune => dune.bak} | 0 src/th-ite/Sidekick_th_ite.ml | 98 --- src/th-ite/dune | 8 - 43 files changed, 1604 insertions(+), 1881 deletions(-) delete mode 100644 src/base-term/Cst.ml delete mode 100644 src/base-term/Cst.mli delete mode 100644 src/base-term/Lit.ml delete mode 100644 src/base-term/Lit.mli delete mode 100644 src/base-term/Term.ml delete mode 100644 src/base-term/Term.mli delete mode 100644 src/base-term/Term_cell.ml delete mode 100644 src/base-term/Term_cell.mli delete mode 100644 src/base-term/Ty.ml delete mode 100644 src/base-term/Ty.mli delete mode 100644 src/base-term/Ty_card.ml delete mode 100644 src/base-term/Ty_card.mli delete mode 100644 src/base-term/Value.ml delete mode 100644 src/base-term/Value.mli rename src/{base-term => smtlib}/Ast.ml (99%) rename src/{base-term => smtlib}/Ast.mli (99%) rename src/{th-bool/Sidekick_th_bool.ml => th-bool-dyn/Sidekick_th_bool_dyn.ml} (99%) rename src/{th-bool/dune => th-bool-dyn/dune.bak} (60%) create mode 100644 src/th-bool-static/Sidekick_th_bool_static.ml create mode 100644 src/th-bool-static/dune rename src/th-cstor/{dune => dune.bak} (100%) delete mode 100644 src/th-ite/Sidekick_th_ite.ml delete mode 100644 src/th-ite/dune diff --git a/Makefile b/Makefile index 497d277d..e647329a 100644 --- a/Makefile +++ b/Makefile @@ -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 diff --git a/src/base-term/Base_types.ml b/src/base-term/Base_types.ml index 4b8a306b..fbe05dfe 100644 --- a/src/base-term/Base_types.ml +++ b/src/base-term/Base_types.ml @@ -1,8 +1,9 @@ - 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 *) @@ -13,9 +14,8 @@ type term = { (* term shallow structure *) and 'a term_view = | Bool of bool - | App_cst of cst * 'a IArray.t (* full, first-order application *) + | App_fun of fun_ * 'a IArray.t (* full, first-order application *) | Eq of 'a * 'a - | If of 'a * 'a * 'a | Not of 'a (* boolean literal *) @@ -24,14 +24,14 @@ and lit = { lit_sign: bool; } -and cst = { - cst_id: ID.t; - cst_view: cst_view; +and fun_ = { + fun_id: ID.t; + fun_view: fun_view; } -and cst_view = - | Cst_undef of fun_ty (* simple undefined constant *) - | Cst_def of { +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? *) @@ -61,7 +61,7 @@ and ty = { } and ty_view = - | Ty_prop + | Ty_bool | Ty_atomic of { def: ty_def; args: ty list; @@ -106,14 +106,14 @@ let cmp_lit a b = 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 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_cst out a = ID.pp out a.cst_id -let id_of_cst a = a.cst_id +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 @@ -139,7 +139,7 @@ let pp_value out = function 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_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 @@ -148,14 +148,12 @@ let rec pp_ty out t = match t.ty_view with 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 + | 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 "(@[=@ %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 = @@ -172,3 +170,703 @@ 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 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 +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) diff --git a/src/base-term/Cst.ml b/src/base-term/Cst.ml deleted file mode 100644 index 105b704e..00000000 --- a/src/base-term/Cst.ml +++ /dev/null @@ -1,41 +0,0 @@ - -open Base_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) diff --git a/src/base-term/Cst.mli b/src/base-term/Cst.mli deleted file mode 100644 index bbf2322a..00000000 --- a/src/base-term/Cst.mli +++ /dev/null @@ -1,22 +0,0 @@ - -open Base_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 diff --git a/src/base-term/Lit.ml b/src/base-term/Lit.ml deleted file mode 100644 index f14fe935..00000000 --- a/src/base-term/Lit.ml +++ /dev/null @@ -1,34 +0,0 @@ - -open Base_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 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 - -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) diff --git a/src/base-term/Lit.mli b/src/base-term/Lit.mli deleted file mode 100644 index af82e940..00000000 --- a/src/base-term/Lit.mli +++ /dev/null @@ -1,25 +0,0 @@ -(** {2 Literals} *) - -open Base_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 apply_sign : t -> bool -> t -val norm_sign : t -> t * bool -module Set : CCSet.S with type elt = t -module Tbl : CCHashtbl.S with type key = t - diff --git a/src/base-term/Model.ml b/src/base-term/Model.ml index 5e822c5a..039540ea 100644 --- a/src/base-term/Model.ml +++ b/src/base-term/Model.ml @@ -1,4 +1,3 @@ - (* This file is free software. See file "license" for more details. *) (** {1 Model} *) @@ -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 "(@[%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 (@[%a@])@]@ @[:funs (@[%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 diff --git a/src/base-term/Model.mli b/src/base-term/Model.mli index 8dfe6da2..1d80a308 100644 --- a/src/base-term/Model.mli +++ b/src/base-term/Model.mli @@ -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 diff --git a/src/base-term/Sidekick_base_term.ml b/src/base-term/Sidekick_base_term.ml index ea9150d5..3bd3882f 100644 --- a/src/base-term/Sidekick_base_term.ml +++ b/src/base-term/Sidekick_base_term.ml @@ -1,27 +1,24 @@ - +module Base_types = Base_types module ID = ID -module Ty_card = Ty_card -module Cst = Cst +module Ty_card = Base_types.Ty_card +module Fun = Base_types.Fun 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 Value = Value - +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 = Cst.t + and type Fun.t = Fun.t and type Ty.t = Ty.t = struct module Term = Term module Lit = Lit - module Fun = Cst + module Fun = Fun module Ty = Ty end diff --git a/src/base-term/Term.ml b/src/base-term/Term.ml deleted file mode 100644 index a3c9ca63..00000000 --- a/src/base-term/Term.ml +++ /dev/null @@ -1,147 +0,0 @@ - -open Base_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_core.CC_view 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 = Base_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) - *) diff --git a/src/base-term/Term.mli b/src/base-term/Term.mli deleted file mode 100644 index 4c39eabc..00000000 --- a/src/base-term/Term.mli +++ /dev/null @@ -1,67 +0,0 @@ - -open Base_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_core.CC_view.t - -(* 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 diff --git a/src/base-term/Term_cell.ml b/src/base-term/Term_cell.ml deleted file mode 100644 index 02903cbf..00000000 --- a/src/base-term/Term_cell.ml +++ /dev/null @@ -1,120 +0,0 @@ - -open Base_types - -(* TODO: normalization of {!term_cell} for use in signatures? *) - -type 'a view = 'a Base_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 = Base_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) - diff --git a/src/base-term/Term_cell.mli b/src/base-term/Term_cell.mli deleted file mode 100644 index 73bd5101..00000000 --- a/src/base-term/Term_cell.mli +++ /dev/null @@ -1,42 +0,0 @@ - -open Base_types - -type 'a view = 'a Base_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 diff --git a/src/base-term/Ty.ml b/src/base-term/Ty.ml deleted file mode 100644 index d6e7fd40..00000000 --- a/src/base-term/Ty.ml +++ /dev/null @@ -1,94 +0,0 @@ - -open Base_types - -type t = ty -type view = Base_types.ty_view -type def = Base_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 diff --git a/src/base-term/Ty.mli b/src/base-term/Ty.mli deleted file mode 100644 index bdebcfd7..00000000 --- a/src/base-term/Ty.mli +++ /dev/null @@ -1,41 +0,0 @@ - -(** {1 Hashconsed Types} *) - -open Base_types - -type t = Base_types.ty -type view = Base_types.ty_view -type def = Base_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 diff --git a/src/base-term/Ty_card.ml b/src/base-term/Ty_card.ml deleted file mode 100644 index 75004d42..00000000 --- a/src/base-term/Ty_card.ml +++ /dev/null @@ -1,19 +0,0 @@ - -open Base_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" diff --git a/src/base-term/Ty_card.mli b/src/base-term/Ty_card.mli deleted file mode 100644 index 4a23e646..00000000 --- a/src/base-term/Ty_card.mli +++ /dev/null @@ -1,17 +0,0 @@ - -(** {1 Type Cardinality} *) - -type t = Base_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 diff --git a/src/base-term/Value.ml b/src/base-term/Value.ml deleted file mode 100644 index 740e7794..00000000 --- a/src/base-term/Value.ml +++ /dev/null @@ -1,23 +0,0 @@ - -(** {1 Value} *) - -open Base_types - -type t = value - -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 diff --git a/src/base-term/Value.mli b/src/base-term/Value.mli deleted file mode 100644 index 4cc1574a..00000000 --- a/src/base-term/Value.mli +++ /dev/null @@ -1,24 +0,0 @@ - -(** {1 Value} - - Semantic value *) - -type t = Base_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 - - diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 8451dd23..339523b1 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -1,4 +1,3 @@ - module View = Sidekick_core.CC_view type ('f, 't, 'ts) view = ('f, 't, 'ts) View.t = @@ -13,31 +12,25 @@ type ('f, 't, 'ts) view = ('f, 't, 'ts) View.t = module type ARG = Sidekick_core.CC_ARG module type S = Sidekick_core.CC_S -module Bits = CCBitField.Make() - -let field_is_pending = Bits.mk_field() -(** true iff the node is in the [cc.pending] queue *) - -let field_usr1 = Bits.mk_field() -(** General purpose *) - -let field_usr2 = Bits.mk_field() -(** General purpose *) - -let () = Bits.freeze() - -module Make(A: ARG) = struct - module A = A +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 th_data = A.Data.t - type actions = A.Actions.t + type actions = CC_A.Actions.t module T = A.Term module Fun = A.Fun + module Lit = A.Lit + + 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 *) (** A node of the congruence closure. An equivalence class is represented by its "root" element, @@ -52,7 +45,6 @@ module Make(A: ARG) = struct 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 *) - mutable n_th_data: th_data; (* theory data *) } and signature = (fun_, node, node list) view @@ -84,7 +76,6 @@ module Make(A: ARG) = struct 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[@inline] th_data n = n.n_th_data let make (t:term) : t = let rec n = { @@ -97,7 +88,6 @@ module Make(A: ARG) = struct n_expl=FL_none; n_next=n; n_size=1; - n_th_data=A.Data.empty; } in n @@ -122,11 +112,6 @@ module Make(A: ARG) = struct 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 - - let[@inline] get_field_usr1 t = get_field field_usr1 t - let[@inline] set_field_usr1 t b = set_field field_usr1 b t - let[@inline] get_field_usr2 t = get_field field_usr2 t - let[@inline] set_field_usr2 t b = set_field field_usr2 b t end module N_tbl = CCHashtbl.Make(N) @@ -136,7 +121,7 @@ module Make(A: ARG) = struct let rec pp out (e:explanation) = match e with | E_reduction -> Fmt.string out "reduction" - | E_lit lit -> A.Lit.pp out lit + | 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 @@ -244,8 +229,8 @@ module Make(A: ARG) = struct several times. See "fast congruence closure and extensions", Nieuwenhis&al, page 14 *) - and ev_on_merge = t -> N.t -> th_data -> N.t -> th_data -> Expl.t -> unit - and ev_on_new_term = t -> N.t -> term -> th_data option + and ev_on_merge = t -> actions -> N.t -> N.t -> Expl.t -> unit + and ev_on_new_term = t -> N.t -> term -> unit let[@inline] size_ (r:repr) = r.n_size let[@inline] true_ cc = Lazy.force cc.true_ @@ -357,7 +342,7 @@ module Make(A: ARG) = struct Vec.clear cc.pending; Vec.clear cc.combine; Stat.incr cc.count_conflict; - A.Actions.raise_conflict acts e A.Proof.default + CC_A.Actions.raise_conflict acts e A.Proof.default let[@inline] all_classes cc : repr Iter.t = T_tbl.values cc.tbl @@ -501,16 +486,7 @@ module Make(A: ARG) = struct (* [n] might be merged with other equiv classes *) push_pending cc n; ); - (* initial theory data *) - let th_data = - List.fold_left - (fun data f -> - match f cc n t with - | None -> data - | Some d -> A.Data.merge data d) - A.Data.empty cc.on_new_term - in - n.n_th_data <- th_data; + List.iter (fun f -> f cc n t) cc.on_new_term; n (* compute the initial signature of the given node *) @@ -527,7 +503,7 @@ module Make(A: ARG) = struct sub in let[@inline] return x = Some x in - match A.cc_view n.n_term with + match CC_A.cc_view n.n_term with | Bool _ | Opaque _ -> None | Eq (a,b) -> let a = deref_sub a in @@ -551,7 +527,7 @@ module Make(A: ARG) = struct match n.n_as_lit with | Some _ -> () | None -> - Log.debugf 15 (fun k->k "(@[cc.set-as-lit@ %a@ %a@])" N.pp n A.Lit.pp lit); + 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 @@ -653,17 +629,9 @@ module Make(A: ARG) = struct 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 - let th_into = r_into.n_th_data in - let th_from = r_from.n_th_data in - let new_data = A.Data.merge th_into th_from in - (* restore old data, if it changed *) - if new_data != th_into then ( - on_backtrack cc (fun () -> r_into.n_th_data <- th_into); - ); - r_into.n_th_data <- new_data; (* 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 r_into th_into r_from th_from expl) cc.on_merge; + 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 *) @@ -732,33 +700,16 @@ module Make(A: ARG) = struct *) match N.as_lit u1 with | Some lit when not (N.equal r2 t2) -> - let lit = if sign then lit else A.Lit.neg lit in (* apply sign *) - Log.debugf 5 (fun k->k "(@[cc.bool_propagate@ %a@])" A.Lit.pp lit); + 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 yield = - let e = explain_eq_n ~init:(Lazy.force half_expl) cc u1 t1 in - List.iter yield e + let reason = + let e = lazy (explain_eq_n ~init:(Lazy.force half_expl) cc u1 t1) in + fun () -> Lazy.force e in - A.Actions.propagate acts lit ~reason A.Proof.default + CC_A.Actions.propagate acts lit ~reason CC_A.A.Proof.default | _ -> ()) - module Theory = struct - type cc = t - - (* raise a conflict *) - let raise_conflict cc expl = - Log.debugf 5 - (fun k->k "(@[cc.theory.raise-conflict@ :expl %a@])" Expl.pp expl); - merge_classes cc (true_ cc) (false_ cc) expl - - 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 add_term = add_term - end - let check_invariants_ (cc:t) = Log.debug 5 "(cc.check-invariants)"; Log.debugf 15 (fun k-> k "%a" pp_full cc); @@ -813,14 +764,18 @@ module Make(A: ARG) = struct 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 = A.Lit.term lit in - Log.debugf 5 (fun k->k "(@[cc.assert_lit@ %a@])" A.Lit.pp lit); - let sign = A.Lit.sign lit in - begin match A.cc_view t with + 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 @@ -840,10 +795,18 @@ module Make(A: ARG) = struct let[@inline] assert_lits cc lits : unit = Iter.iter (assert_lit cc) lits - let assert_eq cc t1 t2 (e:lit list) : unit = - let expl = Expl.mk_list @@ List.rev_map Expl.mk_lit e in - let n1 = add_term cc t1 in - let n2 = add_term cc t2 in + (* 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); + ps_clear cc; + decompose_explain cc expl; + let lits = cc.ps_lits in + CC_A.Actions.raise_conflict acts lits A.Proof.default + + 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 diff --git a/src/cc/Sidekick_cc.mli b/src/cc/Sidekick_cc.mli index 07259b23..298146aa 100644 --- a/src/cc/Sidekick_cc.mli +++ b/src/cc/Sidekick_cc.mli @@ -3,4 +3,4 @@ module type ARG = Sidekick_core.CC_ARG module type S = Sidekick_core.CC_S -module Make(A: ARG) : S with module A = A +module Make(CC_A: ARG) : S with module CC_A = CC_A diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index e72d6f29..c6704554 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -1,4 +1,3 @@ - (** {1 Main Environment} Theories and concrete solvers rely on an environment that defines @@ -56,6 +55,17 @@ module type TERM = sig 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 @@ -64,15 +74,13 @@ module type TERM = sig type state - val bool : state -> bool -> t - end + val ty : t -> Ty.t + val bool : state -> bool -> t (* build true/false *) + val as_bool : t -> bool option - module Ty : sig - type t + val iter_dag : t -> (t -> unit) -> unit - val equal : t -> t -> bool - val hash : t -> int - val pp : t Fmt.printer + module Tbl : Hashtbl.S with type key = t end end @@ -115,37 +123,29 @@ module type TERM_LIT_PROOF = sig end module type CC_ARG = sig - include TERM_LIT_PROOF + module A : TERM_LIT_PROOF - val cc_view : Term.t -> (Fun.t, Term.t, Term.t Iter.t) CC_view.t + 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 *) - (** Monoid embedded in every node *) - module Data : sig - type t - val merge : t -> t -> t - val pp : t Fmt.printer - val empty : t - end - module Actions : sig type t - val raise_conflict : t -> Lit.t list -> Proof.t -> 'a + val raise_conflict : t -> A.Lit.t list -> A.Proof.t -> 'a - val propagate : t -> Lit.t -> reason:Lit.t Iter.t -> Proof.t -> unit + val propagate : t -> A.Lit.t -> reason:(unit -> A.Lit.t list) -> A.Proof.t -> unit end end module type CC_S = sig - module A : CC_ARG + 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 th_data = A.Data.t - type actions = A.Actions.t + type actions = CC_A.Actions.t type t (** Global state of the congruence closure *) @@ -184,15 +184,6 @@ module type CC_S = sig val iter_parents : t -> t Iter.t (** Traverse the parents of the class. Precondition: [is_root n] (see {!find} below) *) - - val th_data : t -> th_data - (** Access theory data for this node *) - - val get_field_usr1 : t -> bool - val set_field_usr1 : t -> bool -> unit - - val get_field_usr2 : t -> bool - val set_field_usr2 : t -> bool -> unit end module Expl : sig @@ -226,26 +217,8 @@ module type CC_S = sig (** Add the term to the congruence closure, if not present already. Will be backtracked. *) - module Theory : sig - type cc = 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 *) - end - - type ev_on_merge = t -> N.t -> th_data -> N.t -> th_data -> Expl.t -> unit - type ev_on_new_term = t -> N.t -> term -> th_data option + type ev_on_merge = t -> actions -> N.t -> N.t -> Expl.t -> unit + type ev_on_new_term = t -> N.t -> term -> unit val create : ?stat:Stat.t -> @@ -285,15 +258,15 @@ module type CC_S = sig 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 *) + 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. *) - (* 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 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. @@ -316,18 +289,11 @@ module type CC_S = sig (**/**) end -type ('model, 'proof, 'ucore, 'unknown) solver_res = - | Sat of 'model - | Unsat of { - proof: 'proof option; - unsat_core: 'ucore; - } - | Unknown of 'unknown - (** A view of the solver from a theory's point of view *) module type SOLVER_INTERNAL = sig - module A : CC_ARG - module CC : CC_S with module A = A + 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 @@ -339,13 +305,6 @@ module type SOLVER_INTERNAL = sig type t type solver = t - (**/**) - module Debug_ : sig - val on_check_invariants : t -> (unit -> unit) -> unit - val check_model : t -> unit - end - (**/**) - module Expl = CC.Expl module N = CC.N @@ -353,25 +312,6 @@ module type SOLVER_INTERNAL = sig Its negation will become a conflict clause *) type conflict = lit list - (** {3 Storage of theory-specific data in the CC} - - Theories can create keys to store data in each representative of the - congruence closure. The data will be automatically merged - when classes are merged. - - A callback must be provided, called before merging two classes - containing this data, to check consistency of the theory. - *) - module Key : sig - type 'a t - - type 'a data = (module MERGE_PP with type t = 'a) - - val create : solver -> 'a data -> 'a t - (** Create a key for storing and accessing data of type ['a]. - Values have to be mergeable. *) - end - (** {3 Actions available to theories} *) val tst : t -> term_state @@ -379,83 +319,72 @@ module type SOLVER_INTERNAL = sig val cc : t -> CC.t (** Congruence closure for this solver *) - val raise_conflict: t -> conflict -> 'a + (** {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 -> lit -> (unit -> lit list) -> unit + 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 -> lit -> lit list -> unit + 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 mk_lit : t -> ?sign:bool -> term -> lit - (** Create a literal *) - val add_lit : t -> lit -> unit - (** Add the given literal to the SAT solver, so it gets assigned - a boolean value *) - - val add_lit_t : t -> ?sign:bool -> term -> unit - (** Add the given (signed) bool term to the SAT solver, so it gets assigned - a boolean value *) - - val add_local_axiom: t -> lit list -> unit + 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_persistent_axiom: t -> lit list -> unit + val add_clause_permanent : t -> actions -> lit list -> unit (** Add toplevel clause to the SAT solver. This clause will not be backtracked. *) - val raise_conflict : t -> Expl.t -> 'a - (** Raise a conflict with the given explanation + 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 -> N.t -> N.t -> Expl.t -> unit + 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 cc_data : t -> k:'a Key.t -> N.t -> 'a option - (** Theory specific data for the given node *) - - val cc_add_data : t -> k:'a Key.t -> N.t -> 'a -> unit - (** Add data for this node. This might trigger a conflict if the class - already contains data that is not compatible. *) - - val cc_merge_t : t -> term -> term -> Expl.t -> unit - (** Merge these two terms in the congruence closure, given this explanation. - See {!cc_merge} *) - - val on_cc_merge : - t -> - k:'a Key.t -> - (t -> N.t -> 'a -> N.t -> 'a -> Expl.t -> unit) -> - unit + 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_merge_all : t -> (t -> N.t -> N.t -> Expl.t -> unit) -> unit - (** Callback for when any two classes are merged *) - - val on_cc_new_term : - t -> - k:'a Key.t -> - (t -> N.t -> term -> 'a option) -> - unit + 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_partial_check : t -> (t -> lit Iter.t -> unit) -> unit + 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. @@ -463,7 +392,7 @@ module type SOLVER_INTERNAL = sig to be complete, only correct. It's given only the slice of the trail consisting in new literals. *) - val on_final_check: t -> (t -> lit Iter.t -> unit) -> unit + 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 @@ -473,16 +402,17 @@ end (** Public view of the solver *) module type SOLVER = sig - module Solver_internal : SOLVER_INTERNAL + 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. *) - module A = Solver_internal.A type t type solver = t type term = A.Term.t type ty = A.Ty.t type lit = A.Lit.t - type proof = A.Proof.t + type lemma = A.Proof.t (** {3 A theory} @@ -520,12 +450,6 @@ module type SOLVER = sig type theory = (module THEORY) (** A theory that can be used for this particular solver. *) - type theory_with_st = Tst : { - m: (module THEORY with type t = 'th); - st: 'th; - } -> theory_with_st - (** An instantiated theory *) - val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> @@ -579,9 +503,17 @@ module type SOLVER = sig *) 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 -> @@ -612,8 +544,14 @@ module type SOLVER = sig val add_clause_l : t -> Atom.t list -> unit - type res = (Model.t, proof, lit IArray.t, Unknown.t) solver_res - (** Result of solving for the current set of clauses *) + 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 -> @@ -629,4 +567,10 @@ module type SOLVER = sig val pp_term_graph: t CCFormat.printer val pp_stats : t CCFormat.printer + + (**/**) + module Debug_ : sig + val check_invariants : t -> unit + end + (**/**) end diff --git a/src/main/main.ml b/src/main/main.ml index 7dda80f6..59c33d5f 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -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 @@ -79,7 +79,7 @@ let argspec = Arg.align [ "-no-p", Arg.Clear p_progress, " no progress bar"; "-size", Arg.String (int_arg size_limit), " [kMGT] sets the size limit for the sat solver"; "-time", Arg.String (int_arg time_limit), " [smhd] sets the time limit for the sat solver"; - "-v", Arg.Int Sidekick_smt.Log.set_debug, " sets the debug verbose level"; + "-v", Arg.Int Msat.Log.set_debug, " sets the debug verbose level"; ] type syntax = @@ -111,18 +111,16 @@ let main () = 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] + [Process.th_bool ] | Smtlib -> - [ Sidekick_th_bool.th_dynamic_tseitin; - Sidekick_th_distinct.th; - Sidekick_th_ite.th; + [Process.th_bool ; ] (* TODO: more theories *) in - Sidekick_smt.Solver.create ~store_proof:!check ~theories () + Process.Solver.create ~store_proof:!check ~theories tst () in let dot_proof = if !p_dot_proof = "" then None else Some !p_dot_proof in begin match syn with diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index 59f26dee..ee7fd1d5 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -1,5 +1,3 @@ - - (** {1 Implementation of a Solver using Msat} *) module Vec = Msat.Vec @@ -14,130 +12,49 @@ end module type S = Sidekick_core.SOLVER module Make(A : ARG) -(* : S with type A.Term.t = A.Term.t *) + : 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 - (** 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 CC_key = struct - type 'a data = (module Sidekick_core.MERGE_PP with type t = 'a) - module type KEY_IMPL = sig - include Sidekick_core.MERGE_PP - val id : int - exception Store of t - end - - type 'a t = (module KEY_IMPL with type t = 'a) - - let n_ = ref 0 - - let create (type d) (x:d data) : d t = - let (module D) = x in - let module K = struct - include D - let id = !n_ - exception Store of t - end in - incr n_; - (module K) - - let[@inline] id : type a. a t -> int = fun (module K) -> K.id - - let[@inline] equal - : type a b. a t -> b t -> bool - = fun (module K1) (module K2) -> K1.id = K2.id - - let pp - : type a. a t -> a Fmt.printer - = fun (module K) out x -> K.pp out x - end - - (** Map for theory data associated with representatives, given - to the congruence closure. *) - module Key_set = struct - type 'a key = 'a CC_key.t - type k1 = - | K1 : { - k: 'a key; - e: exn; - } -> k1 - - type t = k1 IM.t - - let empty = IM.empty - - let[@inline] mem k t = IM.mem (CC_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 - | K1 {e=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 (K1 {k; e=K.Store v}) self - - let remove (type a) (k: a key) self : t = - let (module K) = k in - IM.remove K.id self - - let merge (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 (K1 {k=(module K1) as key1; e=pair1; }), Some (K1{e=pair2;_}) -> - match pair1, pair2 with - | K1.Store v1, K1.Store v2 -> - let v12 = K1.merge v1 v2 in (* merge content *) - Some (K1 {k=key1; e=K1.Store v12; }) - | _ -> assert false) - m1 m2 - - let pp_pair out (K1 {k=(module K);e=x; _}) = - match x with - | K.Store x -> K.pp out x - | _ -> assert false - - let pp out (self:t) = - if IM.is_empty self then Fmt.string out "{}" - else Fmt.fprintf out "{@[%a@]}" (Util.pp_seq pp_pair) (IM.values self) - end + (* 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 A = struct - include A + module CC_A = struct + module A = A + let cc_view = A.cc_view - module Data = Key_set module Actions = struct - type t = { - raise_conflict : 'a. Lit.t list -> Proof.t -> 'a; - propagate : Lit.t -> reason:Lit.t Iter.t -> Proof.t -> unit; - } - let[@inline] raise_conflict a lits p = a.raise_conflict lits p - let[@inline] propagate a lit ~reason p = a.propagate lit ~reason p + 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(A) + 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 @@ -148,8 +65,7 @@ module Make(A : ARG) next: th_states; } -> th_states - (* actions from msat *) - type msat_acts = (Msat.void, Lit.t, Msat.void, A.Proof.t) Msat.acts + type actions = msat_acts type t = { tst: T.state; (** state for managing terms *) @@ -158,24 +74,11 @@ module Make(A : ARG) count_axiom: int Stat.counter; count_conflict: int Stat.counter; count_propagate: int Stat.counter; - cc_acts: CC.actions lazy_t; mutable th_states : th_states; (** Set of theories *) - mutable msat_acts: msat_acts option; - mutable on_partial_check: (t -> lit Iter.t -> unit) list; - mutable on_final_check: (t -> lit Iter.t -> unit) list; - mutable on_cc_merge: on_cc_merge list IM.t; - mutable on_cc_new_term : on_cc_new_term IM.t; + mutable on_partial_check: (t -> actions -> lit Iter.t -> unit) list; + mutable on_final_check: (t -> actions -> lit Iter.t -> unit) list; } - - and on_cc_merge = On_cc_merge : { - k: 'a CC_key.t; - f: t -> CC.N.t -> 'a -> CC.N.t -> 'a -> CC.Expl.t -> unit; - } -> on_cc_merge - - and on_cc_new_term = On_cc_new_term : { - k: 'a CC_key.t; - f: t -> N.t -> T.t -> 'a option; - } -> on_cc_new_term + type solver = t module Formula = struct include Lit @@ -186,50 +89,52 @@ module Make(A : ARG) module Eq_class = CC.N module Expl = CC.Expl - type formula = Lit.t type proof = A.Proof.t type conflict = lit list let[@inline] cc (t:t) = Lazy.force t.cc let[@inline] tst t = t.tst - let[@inline] raise_conflict self c : 'a = + let[@inline] raise_conflict self acts c : 'a = Stat.incr self.count_conflict; - match self.msat_acts with - | None -> assert false - | Some acts -> - acts.Msat.acts_raise_conflict c A.Proof.default + acts.Msat.acts_raise_conflict c A.Proof.default - let[@inline] propagate self p cs : unit = + let[@inline] propagate self acts p cs : unit = Stat.incr self.count_propagate; - match self.msat_acts with - | None -> assert false - | Some acts -> - acts.Msat.acts_propagate p (Msat.Consequence (fun () -> cs(), A.Proof.default)) + acts.Msat.acts_propagate p (Msat.Consequence (fun () -> cs(), A.Proof.default)) - let[@inline] propagate_l self p cs : unit = propagate self p (fun()->cs) + let[@inline] propagate_l self acts p cs : unit = + propagate self acts p (fun()->cs) - let add_axiom_ self ~keep lits : unit = + let add_sat_clause_ self acts ~keep lits : unit = Stat.incr self.count_axiom; - match self.msat_acts with - | None -> assert false - | Some acts -> - acts.Msat.acts_add_clause ~keep lits A.Proof.default + acts.Msat.acts_add_clause ~keep lits A.Proof.default - let[@inline] mk_lit self ?sign t = Lit.atom self.tst ?sign t + let[@inline] mk_lit self _acts ?sign t = Lit.atom self.tst ?sign t - let[@inline] add_local_axiom self lits : unit = - add_axiom_ self ~keep:false lits + let[@inline] add_clause_temp self acts lits : unit = + add_sat_clause_ self acts ~keep:false lits - let[@inline] add_persistent_axiom self lits : unit = - add_axiom_ self ~keep:true lits + let[@inline] add_clause_permanent self acts lits : unit = + add_sat_clause_ self acts ~keep:true lits - let[@inline] add_lit self lit : unit = - match self.msat_acts with - | None -> assert false - | Some acts -> acts.Msat.acts_mk_lit lit + let[@inline] add_lit _self acts lit : unit = + acts.Msat.acts_mk_lit lit - let add_lit_t self ?sign t = add_lit self (mk_lit self ?sign t) + 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 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} *) @@ -250,7 +155,7 @@ module Make(A : ARG) pop_lvls_ n self.th_states (* handle a literal assumed by the SAT solver *) - let assert_lits_ ~final (self:t) (lits:Lit.t Iter.t) : unit = + let assert_lits_ ~final (self:t) (acts:actions) (lits:Lit.t Iter.t) : unit = Msat.Log.debugf 2 (fun k->k "(@[@{th_combine.assume_lits@}%s@ %a@])" (if final then "[final]" else "") (Util.pp_seq ~sep:"; " Lit.pp) lits); @@ -260,11 +165,11 @@ module Make(A : ARG) CC.assert_lits cc lits; ); (* transmit to theories. *) - CC.check cc (Lazy.force self.cc_acts); + CC.check cc acts; if final then ( - List.iter (fun f -> f self lits) self.on_final_check; + List.iter (fun f -> f self acts lits) self.on_final_check; ) else ( - List.iter (fun f -> f self lits) self.on_partial_check; + List.iter (fun f -> f self acts lits) self.on_partial_check; ); () @@ -277,25 +182,10 @@ module Make(A : ARG) (* propagation from the bool solver *) let check_ ~final (self:t) (acts: msat_acts) = - let old_acts = self.msat_acts in - self.msat_acts <- Some acts; - try - 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 iter; - self.msat_acts <- old_acts; - () - with e -> - self.msat_acts <- old_acts; - raise e - - 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); - () + 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 (* propagation from the bool solver *) let[@inline] partial_check (self:t) (acts:_ Msat.acts) : unit = @@ -316,13 +206,6 @@ module Make(A : ARG) CC.mk_model (cc self) m *) - let cc_raise_conflict self lits _p = - raise_conflict self lits - - let cc_propagate self p ~reason _p = - let reason() = Iter.to_list reason in - propagate self p reason - let create ~stat (tst:A.Term.state) () : t = let rec self = { tst; @@ -330,42 +213,40 @@ module Make(A : ARG) (* lazily tie the knot *) CC.create ~size:`Big self.tst; ); - cc_acts=lazy { - raise_conflict=cc_raise_conflict self; - propagate=cc_propagate self; - }; th_states=Ths_nil; 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"; - msat_acts=None; on_partial_check=[]; on_final_check=[]; - on_cc_merge=IM.empty; - on_cc_new_term=IM.empty; } in ignore (Lazy.force @@ self.cc : CC.t); self - end - type conflict = lit list - - (** the Main Solver *) + (** 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 = Sat_solver.Proof + 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 @@ -409,6 +290,8 @@ module Make(A : ARG) 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] *) @@ -420,17 +303,41 @@ module Make(A : ARG) end; self - let check_invariants (self:t) = - if Util._CHECK_INVARIANTS then ( - CC.Debug_.check_invariants (Solver_internal.cc self.si); - ) + 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[@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-to-lit@ :subterm %a@])" T.pp sub); + ignore (mk_atom_t_ self sub : Sat_solver.atom)) + + let mk_atom_lit self lit : Atom.t = + 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 @@ -447,6 +354,15 @@ module Make(A : ARG) | 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 "" end (* TODO *) @@ -464,15 +380,17 @@ module Make(A : ARG) let pp_model = Model.pp *) - type res = (Model.t, Proof.t, lit IArray.t, Unknown.t) Sidekick_core.solver_res + 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} *) - (* 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) = () @@ -480,25 +398,18 @@ module Make(A : ARG) let pp_stats out (self:t) : unit = Stat.pp_all out (Stat.all @@ stats self) - (* map boolean subterms to literals *) - let add_bool_subterms_ (self:t) (t:T.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 + let add_clause (self:t) (c:Atom.t IArray.t) : unit = Stat.incr self.count_clause; - Sat_solver.add_clause_a sat c Proof_default + 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 = @@ -512,8 +423,6 @@ module Make(A : ARG) *) () - (* 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 do_on_exit () = List.iter (fun f->f()) on_exit; @@ -523,8 +432,10 @@ module Make(A : ARG) 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 + 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 (* @@ -534,14 +445,27 @@ module Make(A : ARG) Unknown U_incomplete (* TODO *) *) | Sat_solver.Unsat us -> - let pr = + 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 pr + 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 diff --git a/src/msat-solver/dune b/src/msat-solver/dune index d774e2eb..e4be5812 100644 --- a/src/msat-solver/dune +++ b/src/msat-solver/dune @@ -1,7 +1,6 @@ - (library - (name Sidekick_msat_solver) - (public_name sidekick.msat-solver) - (libraries containers containers.data iter - sidekick.core sidekick.util sidekick.cc msat zarith) - (flags :standard -open Sidekick_util)) + (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)) diff --git a/src/base-term/Ast.ml b/src/smtlib/Ast.ml similarity index 99% rename from src/base-term/Ast.ml rename to src/smtlib/Ast.ml index db9f3470..8a1bfe39 100644 --- a/src/base-term/Ast.ml +++ b/src/smtlib/Ast.ml @@ -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 diff --git a/src/base-term/Ast.mli b/src/smtlib/Ast.mli similarity index 99% rename from src/base-term/Ast.mli rename to src/smtlib/Ast.mli index 4d61162d..5e71174d 100644 --- a/src/base-term/Ast.mli +++ b/src/smtlib/Ast.mli @@ -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} *) diff --git a/src/smtlib/Locations.ml b/src/smtlib/Locations.ml index 34f7efb5..bf5368e7 100644 --- a/src/smtlib/Locations.ml +++ b/src/smtlib/Locations.ml @@ -1,4 +1,3 @@ - (* This file is free software, copyright Simon Cruanes. See file "LICENSE" for more details. *) (** {1 Locations} *) diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 66ff2d12..f3118500 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -1,16 +1,198 @@ - (** {2 Conversion into {!Term.t}} *) -open Sidekick_smt +open Sidekick_base_term 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 + | 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_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 List.map (fun (a,b) -> neq tst a b) + in + and_l tst cs + + let mk_bool 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_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 + + let view_as_non_bool t = + match T.view t with + | T.App_fun (f, args) -> + begin match view_id (Fun.id f) args with + | exception Not_a_th_term -> + NB_functor(args, fun tst args -> T.app_fun tst f args) + | B_ite (a,b,c) -> NB_ite(a,b,c) + | _ -> NB_bool t + end + | T.Bool _ | T.Eq _ | T.Not _ -> NB_bool t + + let mk_ite = ite + + 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 +213,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 +234,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 +280,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 +320,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 +400,22 @@ end let conv_ty = Conv.conv_ty let conv_term = Conv.conv_term +(* instantiate solver here *) +module Solver = Sidekick_msat_solver.Make(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) + +(* 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 +453,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 +463,7 @@ let solve ?(pp_model=false) ?(check=false) ?time:_ ?memory:_ ?progress:_ - ?hyps + ?hyps:_ ~assumptions s : unit = let t1 = Sys.time() in @@ -280,17 +475,20 @@ let solve begin match res with | Solver.Sat m -> if pp_model then ( - Format.printf "(@[model@ %a@])@." Model.pp m + (* TODO: use actual {!Model} in the solver? or build it afterwards *) + Format.printf "(@[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,13 +499,13 @@ 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 @@ -316,7 +514,7 @@ 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 + ~f:(fun i -> Fun.mk_undef_const (ID.makef "a_%d" i) Ty.bool) in Lit.atom tst ~sign:(i>0) @@ Term.const tst c (* process a single statement *) @@ -373,12 +571,12 @@ 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); + Solver.add_clause_lits_l solver c; E.return () | A.Goal (_, _) -> Error.errorf "cannot deal with goals yet" @@ -388,381 +586,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 diff --git a/src/smtlib/Process.mli b/src/smtlib/Process.mli index 46c20333..d4c58f5d 100644 --- a/src/smtlib/Process.mli +++ b/src/smtlib/Process.mli @@ -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 diff --git a/src/smtlib/Sidekick_smtlib.ml b/src/smtlib/Sidekick_smtlib.ml index 4baacebf..474a64e4 100644 --- a/src/smtlib/Sidekick_smtlib.ml +++ b/src/smtlib/Sidekick_smtlib.ml @@ -1,11 +1,12 @@ - (** {1 Process Statements} *) +module ID = Sidekick_base_term.ID module Fmt = CCFormat -module Ast = Sidekick_base_term.Ast +module Ast = Ast module E = CCResult module Loc = Locations module Process = Process +module Solver = Process.Solver module Proof = struct type t = Proof_default @@ -20,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) @@ -50,8 +47,9 @@ module Parse = struct with e -> Result.Error (Printexc.to_string e) end +(* TODO: remove module Term_bool : sig - open Sidekick_th_bool + open Sidekick_th_bool_dyn type 'a view = 'a Bool_intf.view type term = Sidekick_smt.Term.t @@ -208,66 +206,10 @@ end = struct | B_imply (a,b) -> imply_a st a b | B_not t -> not_ st t end - -module Term_distinct = struct - open Sidekick_base_term - - 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 - -module Term_ite = struct - open Sidekick_base_term - - let[@inline] view_as_ite t = match Term.view t with - | If (a,b,c) -> T_ite (a,b,c) - | Bool b -> T_bool b - | _ -> T_other t -end - -module Solver = Sidekick_msat_solver.Solver + *) module Theories = struct + (* TODO module Th_cstor = Sidekick_th_cstor.Make(struct module Solver = Solver module T = Solver.A.Term @@ -280,6 +222,7 @@ module Theories = struct end end) + *) end let parse = Parse.parse diff --git a/src/smtlib/Sidekick_smtlib.mli b/src/smtlib/Sidekick_smtlib.mli index aea16d17..eddef0a6 100644 --- a/src/smtlib/Sidekick_smtlib.mli +++ b/src/smtlib/Sidekick_smtlib.mli @@ -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 - diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index c96bc106..09e6193e 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -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 diff --git a/src/smtlib/Typecheck.mli b/src/smtlib/Typecheck.mli index 9c295dfa..9bd19de8 100644 --- a/src/smtlib/Typecheck.mli +++ b/src/smtlib/Typecheck.mli @@ -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 diff --git a/src/smtlib/dune b/src/smtlib/dune index edcab872..c9337849 100644 --- a/src/smtlib/dune +++ b/src/smtlib/dune @@ -1,12 +1,13 @@ - (library - (name sidekick_smtlib) - (public_name sidekick.smtlib) - (libraries containers zarith msat sidekick.core sidekick.util - sidekick.msat-solver sidekick.base-term - sidekick.th-bool sidekick.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 + msat.backend) + (flags :standard -open Sidekick_util)) -(menhir (modules Parser)) +(menhir + (modules Parser)) -(ocamllex (modules Lexer)) +(ocamllex + (modules Lexer)) diff --git a/src/th-bool/Sidekick_th_bool.ml b/src/th-bool-dyn/Sidekick_th_bool_dyn.ml similarity index 99% rename from src/th-bool/Sidekick_th_bool.ml rename to src/th-bool-dyn/Sidekick_th_bool_dyn.ml index 0cf324d4..90432015 100644 --- a/src/th-bool/Sidekick_th_bool.ml +++ b/src/th-bool-dyn/Sidekick_th_bool_dyn.ml @@ -1,4 +1,3 @@ - (** {1 Theory of Booleans} *) (** {2 Signatures for booleans} *) diff --git a/src/th-bool/dune b/src/th-bool-dyn/dune.bak similarity index 60% rename from src/th-bool/dune rename to src/th-bool-dyn/dune.bak index 8ac7acad..b0fc4dd6 100644 --- a/src/th-bool/dune +++ b/src/th-bool-dyn/dune.bak @@ -1,6 +1,6 @@ (library - (name Sidekick_th_bool) - (public_name sidekick.th-bool) + (name Sidekick_th_bool_dyn) + (public_name sidekick.th-bool-dyn) (libraries containers sidekick.core sidekick.util) (flags :standard -open Sidekick_util)) diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml new file mode 100644 index 00000000..4f024226 --- /dev/null +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -0,0 +1,260 @@ +(** {2 Signatures for booleans} *) + +type 'a bool_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_equiv of 'a * 'a + | B_eq of 'a * 'a + | B_ite of 'a * 'a * 'a + | B_atom of 'a + +type ('tst,'a) non_bool_view = + | NB_ite of 'a * 'a * 'a + | NB_functor of 'a IArray.t * ('tst -> 'a IArray.t -> 'a) + | NB_bool of 'a (* boolean subterm *) + +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 view_as_non_bool : term -> (S.A.Term.state,term) non_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 *) + + val mk_ite : S.A.Term.state -> term -> term -> term -> term + + 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 + + type state + + val create : T.state -> state + + val simplify : state -> T.t -> T.t + (** Simplify given term *) + + val cnf : state -> T.t -> A.S.A.Lit.t list Vec.t + (** 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 + + 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) (t:T.t) : T.t = + let rec aux t = + let tst = self.tst in + match T.Tbl.find self.simps t with + | u -> u + | exception Not_found -> + let u, cache = + match A.view_as_bool t with + | B_not u -> not_ tst (aux u), false + | B_and a -> + let a = IArray.map aux a in + let u = + if IArray.exists is_false a then T.bool tst false + else if IArray.for_all is_true a then T.bool tst true + else and_a tst a + in + u, true + | B_or a -> + let a = IArray.map aux a in + let u = + if IArray.exists is_true a then T.bool tst true + else if IArray.for_all is_false a then T.bool tst false + else or_a tst a + in + u, true + | B_imply (args, u) -> + (* turn into a disjunction *) + let u = + aux @@ or_a tst @@ + IArray.append (IArray.map (not_ tst) args) (IArray.singleton u) + in + u, true + | B_ite (a,b,c) -> + let a = aux a in + begin match T.as_bool a with + | Some true -> aux b + | Some false -> aux c + | _ -> ite tst a (aux b) (aux c) + end, true + | B_equiv (a,b) -> + let u = equiv tst (aux a) (aux b) in + u, true + | B_eq (a,b) -> + let u = eq tst (aux a) (aux b) in + u, true + | B_atom a -> + begin match A.view_as_non_bool a with + | NB_bool _ -> assert false + | NB_ite (a,b,c) -> + A.mk_ite tst (aux a) (aux b) (aux c), true + | NB_functor (args, mk) -> + mk tst (IArray.map aux args), true + end + in + if cache then ( + T.Tbl.add self.simps t u; (* cache rewriting step *) + ); + u + in + let u = aux t in + if not (T.equal t u) then ( + Log.debugf 5 + (fun k->k "(@[th-bool.simplified@ :from %a@ :to %a@])" T.pp t T.pp u); + ); + u + + 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) (t:T.t) : Lit.t list Vec.t = + let cs: Lit.t list Vec.t = Vec.create() in + let add_clause lits = Vec.push cs lits in + let rec aux_bool (t:T.t) : Lit.t = + let tst = self.tst in + match T.Tbl.find self.cnf t with + | u -> u + | exception Not_found -> + let lit, cache = + match A.view_as_bool t with + | B_not u -> + let lit = aux_bool u in + Lit.neg lit, false + | B_and l -> + let subs = IArray.to_list_map aux_bool 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, true + | B_or l -> + let subs = IArray.to_list_map aux_bool 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, true + | B_imply (args, u) -> + let t' = + or_a tst @@ + IArray.append (IArray.map (not_ tst) args) (IArray.singleton u) in + aux_bool t', true + | B_ite _ -> + Lit.atom tst (aux_t t), true + | B_eq _ -> + Lit.atom tst (aux_t t), true + | B_equiv (a,b) -> + Format.printf "@[cnf: equiv@ %a@ and %a@]@." T.pp a T.pp b; + let a = aux_bool a in + let b = aux_bool 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, true + | B_atom u -> + Lit.atom tst (aux_t u), false + in + if cache then ( + T.Tbl.add self.cnf t lit; (* cache rewriting step *) + ); + lit + + and aux_t (t:T.t) : T.t = + let tst = self.tst in + match A.view_as_non_bool t with + | NB_ite (a,b,c) -> + begin match T.Tbl.find self.cnf_ite t with + | u -> u + | exception Not_found -> + let a = aux_bool a in + let b = aux_t b in + let c = aux_t c in + let proxy = fresh_term ~pre:"ite_" self (T.ty b) in + T.Tbl.add self.cnf_ite t proxy; + (* add clauses: [a => proxy=b], [¬a => proxy=c] *) + add_clause [Lit.neg a; Lit.atom tst (eq tst proxy b)]; + add_clause [a; Lit.atom tst (eq tst proxy c)]; + proxy + end + | NB_bool _ -> Lit.term (aux_bool t) + | NB_functor (args, mk) -> + (* pass through *) + let args = IArray.map aux_t args in + mk tst args + in + (* traverse [t] to produce clauses *) + if Ty.is_bool (T.ty t) then ( + let top = aux_bool t in + add_clause [top]; (* also add a clause standing for [t = true] *) + ) else ( + ignore (aux_t t: T.t); + ); + cs + + (* TODO: register [cnf] as a clausifier, register [simplify] as a + preprocessor *) + let create_and_setup _si = () + + let theory = + A.S.mk_theory + ~name:"th-bool" + ~create_and_setup + () +end diff --git a/src/th-bool-static/dune b/src/th-bool-static/dune new file mode 100644 index 00000000..ae7257a1 --- /dev/null +++ b/src/th-bool-static/dune @@ -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)) diff --git a/src/th-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml index 549a720e..11c11754 100644 --- a/src/th-cstor/Sidekick_th_cstor.ml +++ b/src/th-cstor/Sidekick_th_cstor.ml @@ -1,4 +1,3 @@ - (** {1 Theory for constructors} *) type ('c,'t) cstor_view = @@ -25,21 +24,20 @@ module Make(A : ARG) : S with module A = A = struct 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) *) - module Data = struct - type t = data - let pp out x = T.pp out x.t - (* let equal x y = T.equal x.t y.t *) - let merge x _ = x - end + (* TODO + module N_tbl = Backtrackable_tbl.Make(N) + *) + module N_tbl = CCHashtbl.Make(N) type t = { - k: data SI.Key.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 *) } let on_merge (solver:SI.t) n1 tc1 n2 tc2 e_n1_n2 : unit = @@ -58,7 +56,7 @@ module Make(A : ARG) : S with module A = A = struct l1 l2 ) else ( (* different function: disjointness *) - SI.raise_conflict solver expl + SI.cc_raise_conflict solver expl ) | _ -> assert false @@ -68,11 +66,15 @@ module Make(A : ARG) : S with module A = A = struct | T_cstor _ -> Some {t;n} | _ -> None - let create_and_setup (solver:SI.t) : t = - let k = SI.Key.create solver (module Data) in - SI.on_cc_merge solver ~k on_merge; - SI.on_cc_new_term solver ~k on_new_term; - {k} + 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 diff --git a/src/th-cstor/dune b/src/th-cstor/dune.bak similarity index 100% rename from src/th-cstor/dune rename to src/th-cstor/dune.bak diff --git a/src/th-ite/Sidekick_th_ite.ml b/src/th-ite/Sidekick_th_ite.ml deleted file mode 100644 index a35931fc..00000000 --- a/src/th-ite/Sidekick_th_ite.ml +++ /dev/null @@ -1,98 +0,0 @@ - -(** {1 Theory for if-then-else} *) - -module Ite_view = struct - type 't t = - | T_ite of 't * 't * 't - | T_bool of bool - | T_other of 't -end - -module type ARG = sig - module S : Sidekick_core.SOLVER - type term = S.A.Term.t - - val view_as_ite : term -> term Ite_view.t - - module T_set : CCSet.S with type elt = term -end - -module type S = sig - module A : ARG - val theory : A.S.theory -end - -module Make(A : ARG) -(* : S with module A = A *) -= struct - module A = A - module Solver = A.S.Solver_internal - module N = Solver.N - module Expl = Solver.Expl - module T = A.S.A.Term - - type lit = A.S.A.Lit.t - type term = T.t - - module Data = struct - type t = A.T_set.t - (* associate to each class [t] the set of [ite a b c] where [a=t] *) - - let pp = Fmt.(map A.T_set.to_seq @@ seq ~sep:(return ",@ ") T.pp) - let merge = A.T_set.union - end - - type t = { - k: Data.t Solver.Key.t; - } - - let on_merge (self:t) (solver:Solver.t) n1 n2 e_n1_n2 : unit = - 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 Solver.cc_data solver ~k:self.k n1, A.view_as_ite (N.term n2) with - | Some set, T_bool n2_true -> - assert (not @@ A.T_set.is_empty set); - A.T_set.iter - (fun parent_1 -> match A.view_as_ite parent_1 with - | T_ite (a1,b1,c1) -> - let n_parent1 = Solver.cc_add_term solver parent_1 in - let expl = - Expl.mk_list [ - e_n1_n2; - Expl.mk_merge n1 (Solver.cc_add_term solver a1)] in - if n2_true then ( - (* [a1 = n1 = n2 = true] so [if a1 b1 c1 = b1] *) - Solver.cc_merge solver n_parent1 (Solver.cc_add_term solver b1) expl - ) else ( - (* [a1 = n1 = n2 = false] so [if a1 b1 c1 = c1] *) - Solver.cc_merge solver n_parent1 (Solver.cc_add_term solver c1) expl - ) - | _ -> assert false) - set - | _ -> () - in - check_ n1 n2; - check_ n2 n1; - () - - let on_new_term (self:t) (solver:Solver.t) _n (t:T.t) = - match A.view_as_ite t with - | T_ite (a,_,_) -> - (* add [t] to parents of [a] *) - let n_a = Solver.cc_find solver @@ Solver.cc_add_term solver a in - Solver.cc_add_data solver n_a ~k:self.k (A.T_set.singleton t); - None - | _ -> None - - let create_and_setup (solver:Solver.t) : t = - let k = Solver.Key.create solver (module Data) in - let self = {k} in - Solver.on_cc_merge_all solver (on_merge self); - Solver.on_cc_new_term solver ~k (on_new_term self); - self - - let theory = A.S.mk_theory ~name:"ite" ~create_and_setup () -end - diff --git a/src/th-ite/dune b/src/th-ite/dune deleted file mode 100644 index a521adf2..00000000 --- a/src/th-ite/dune +++ /dev/null @@ -1,8 +0,0 @@ - - -(library - (name Sidekick_th_ite) - (public_name sidekick.th-ite) - (libraries containers sidekick.core) - (flags :standard -open Sidekick_util)) -