From cad49b374786750bc3f2ba3a8a153c8acf5acce8 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 6 Jun 2019 17:13:21 -0500 Subject: [PATCH] wip: preprocess/simplify as part of theories --- src/base-term/Base_types.ml | 9 + src/core/Sidekick_core.ml | 42 ++- src/msat-solver/Sidekick_msat_solver.ml | 80 +++++- src/smtlib/Process.ml | 18 +- src/smtlib/Typecheck.ml | 13 +- src/th-bool-static/Sidekick_th_bool_static.ml | 263 +++++++----------- 6 files changed, 226 insertions(+), 199 deletions(-) diff --git a/src/base-term/Base_types.ml b/src/base-term/Base_types.ml index fbe05dfe..ae67a54f 100644 --- a/src/base-term/Base_types.ml +++ b/src/base-term/Base_types.ml @@ -594,6 +594,8 @@ module Term : sig val iter_dag : t -> t Iter.t + val map_shallow : state -> (t -> t) -> t -> t + val pp : t Fmt.printer (** {6 Views} *) @@ -745,6 +747,13 @@ end = struct let iter_dag t yield = let st = Iter_dag.create() in Iter_dag.iter_dag st t yield + + let map_shallow (tst:state) f (t:t) : t = + match view t with + | Bool _ -> t + | App_fun (hd, a) -> app_fun tst hd (IArray.map f a) + | Not u -> not_ tst (f u) + | Eq (a,b) -> eq tst (f a) (f b) end module Lit : sig diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index c6704554..5e209f8e 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -78,6 +78,9 @@ module type TERM = sig val bool : state -> bool -> t (* build true/false *) val as_bool : t -> bool option + val map_shallow : state -> (t -> t) -> t -> t + (** Map function on immediate subterms *) + val iter_dag : t -> (t -> unit) -> unit module Tbl : Hashtbl.S with type key = t @@ -312,13 +315,37 @@ module type SOLVER_INTERNAL = sig Its negation will become a conflict clause *) type conflict = lit list - (** {3 Actions available to theories} *) - val tst : t -> term_state val cc : t -> CC.t (** Congruence closure for this solver *) + (** {3 Simplifiers} *) + + module Simplify : sig + type t + + val tst : t -> term_state + + val clear : t -> unit + (** Reset internal cache, etc. *) + + type hook = t -> term -> term option + (** Given a term, try to simplify it. Return [None] if it didn't change. + Can also add clauses to the simplifier. *) + + val normalize : t -> term -> term + (** Normalize a term using all the hooks. *) + end + + type simplify_hook = Simplify.hook + + val add_simplifier : t -> Simplify.hook -> unit + + val simplifier : t -> Simplify.t + + val simp_t : t -> term -> term + (** {3 hooks for the theory} *) type actions @@ -398,6 +425,17 @@ module type SOLVER_INTERNAL = sig Must be complete (i.e. must raise a conflict if the set of literals is not satisfiable) and can be expensive. The function is given the whole trail. *) + + (** {3 Preprocessors} + These preprocessors turn mixed, raw literals (possibly simplified) into + literals suitable for reasoning. + Typically some clauses are also added to the solver. *) + + type preprocess_hook = t -> actions -> term -> term option + (** Given a term, try to preprocess it. Return [None] if it didn't change. + Can also add clauses to define new terms. *) + + val add_preprocess : t -> preprocess_hook -> unit end (** Public view of the solver *) diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index ee7fd1d5..560e1483 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -67,6 +67,43 @@ module Make(A : ARG) type actions = msat_acts + module Simplify = struct + type t = { + tst: term_state; + mutable hooks: hook list; + cache: T.t T.Tbl.t; + } + and hook = t -> term -> term option + + let create tst : t = {tst; hooks=[]; cache=T.Tbl.create 32;} + let[@inline] tst self = self.tst + let add_hook self f = self.hooks <- f :: self.hooks + let clear self = T.Tbl.clear self.cache + + let normalize (self:t) (t:T.t) : T.t = + (* compute and cache normal form of [t] *) + let rec aux t = + match T.Tbl.find self.cache t with + | u -> u + | exception Not_found -> + let u = aux_rec t self.hooks in + T.Tbl.add self.cache t u; + u + (* try each function in [hooks] successively, and rewrite subterms *) + and aux_rec t hooks = match hooks with + | [] -> + let u = T.map_shallow self.tst aux t in + if T.equal t u then t else aux u + | h :: hooks_tl -> + match h self t with + | None -> aux_rec t hooks_tl + | Some u when T.equal t u -> aux_rec t hooks_tl + | Some u -> aux u + in + aux t + end + type simplify_hook = Simplify.hook + type t = { tst: T.state; (** state for managing terms *) cc: CC.t lazy_t; (** congruence closure *) @@ -74,10 +111,15 @@ module Make(A : ARG) count_axiom: int Stat.counter; count_conflict: int Stat.counter; count_propagate: int Stat.counter; + simp: Simplify.t; + mutable preprocess: preprocess_hook list; + preprocess_cache: T.t T.Tbl.t; mutable th_states : th_states; (** Set of theories *) mutable on_partial_check: (t -> actions -> lit Iter.t -> unit) list; mutable on_final_check: (t -> actions -> lit Iter.t -> unit) list; } + and preprocess_hook = t -> actions -> term -> term option + type solver = t module Formula = struct @@ -95,6 +137,12 @@ module Make(A : ARG) let[@inline] cc (t:t) = Lazy.force t.cc let[@inline] tst t = t.tst + let simplifier self = self.simp + let simp_t self (t:T.t) : T.t = Simplify.normalize self.simp t + let add_simplifier (self:t) f : unit = Simplify.add_hook self.simp f + + let add_preprocess self f = self.preprocess <- f :: self.preprocess + let[@inline] raise_conflict self acts c : 'a = Stat.incr self.count_conflict; acts.Msat.acts_raise_conflict c A.Proof.default @@ -110,7 +158,31 @@ module Make(A : ARG) Stat.incr self.count_axiom; acts.Msat.acts_add_clause ~keep lits A.Proof.default - let[@inline] mk_lit self _acts ?sign t = Lit.atom self.tst ?sign t + let preprocess_lit_ (self:t) (acts:actions) (lit:lit) : lit = + (* compute and cache normal form of [t] *) + let rec aux t = + match T.Tbl.find self.preprocess_cache t with + | u -> u + | exception Not_found -> + (* first, map subterms *) + let u = T.map_shallow self.tst aux t in + (* then rewrite *) + let u = aux_rec u self.preprocess in + T.Tbl.add self.preprocess_cache t u; + u + (* try each function in [hooks] successively *) + and aux_rec t hooks = match hooks with + | [] -> t + | h :: hooks_tl -> + match h self acts t with + | None -> aux_rec t hooks_tl + | Some u -> aux u + in + let t = aux (Lit.term lit) in + Lit.atom self.tst ~sign:(Lit.sign lit) t + + let[@inline] mk_lit self acts ?sign t = + preprocess_lit_ self acts @@ Lit.atom self.tst ?sign t let[@inline] add_clause_temp self acts lits : unit = add_sat_clause_ self acts ~keep:false lits @@ -118,8 +190,7 @@ module Make(A : ARG) let[@inline] add_clause_permanent self acts lits : unit = add_sat_clause_ self acts ~keep:true lits - let[@inline] add_lit _self acts lit : unit = - acts.Msat.acts_mk_lit lit + let add_lit _self acts lit : unit = acts.Msat.acts_mk_lit lit let add_lit_t self acts ?sign t = add_lit self acts (mk_lit self acts ?sign t) @@ -215,6 +286,9 @@ module Make(A : ARG) ); th_states=Ths_nil; stat; + simp=Simplify.create tst; + preprocess=[]; + preprocess_cache=T.Tbl.create 32; count_axiom = Stat.mk_int stat "th-axioms"; count_propagate = Stat.mk_int stat "th-propagations"; count_conflict = Stat.mk_int stat "th-conflicts"; diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 81034575..fa0c590b 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -35,6 +35,7 @@ module Form = struct let view_as_bool (t:T.t) : T.t bool_view = match T.view t with + | Bool b -> B_bool b | Not u -> B_not u | Eq (a, b) when Ty.is_bool (T.ty a) -> B_equiv (a,b) | App_fun ({fun_id; _}, args) -> @@ -57,6 +58,7 @@ module Form = struct let eval id args = let open Value in match view_id id args with + | B_bool b -> Value.bool b | B_not (V_bool b) -> Value.bool (not b) | B_and a when IArray.for_all Value.is_true a -> Value.true_ | B_and a when IArray.exists Value.is_false a -> Value.false_ @@ -156,6 +158,7 @@ module Form = struct and_l tst cs let mk_bool st = function + | B_bool b -> T.bool st b | B_atom t -> t | B_and l -> and_a st l | B_or l -> or_a st l @@ -165,19 +168,6 @@ module Form = struct | 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; @@ -508,8 +498,6 @@ let solve Format.printf "Unknown (:reason %a)" Solver.Unknown.pp reas end -(* NOTE: hack for testing with dimacs. Proper treatment should go into - scoping in Ast, or having theory-specific state in `Term.state` *) (* process a single statement *) let process_stmt ?hyps diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index 09e6193e..9a691b7d 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -16,11 +16,7 @@ let pp_loc_opt = Loc.pp_opt (** {2 Parsing} *) -module StrTbl = CCHashtbl.Make(struct - type t = string - let equal = CCString.equal - let hash = CCString.hash - end) +module StrTbl = CCHashtbl.Make(CCString) module Ctx = struct type kind = @@ -324,13 +320,6 @@ let rec conv_term ctx (t:PA.term) : A.term = match t with | _ -> errorf_ctx ctx "unsupported term %a" PA.pp_term t -let find_file_ name ~dir : string option = - Log.debugf 2 (fun k->k "search %s in %s" name dir); - let abs_path = Filename.concat dir name in - if Sys.file_exists abs_path - then Some abs_path - else None - let conv_fun_decl ctx f : string * A.Ty.t = if f.PA.fun_ty_vars <> [] then ( errorf_ctx ctx "cannot convert polymorphic function@ %a" diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 4f024226..0e5a782f 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -1,6 +1,7 @@ (** {2 Signatures for booleans} *) type 'a bool_view = + | B_bool of bool | B_not of 'a | B_and of 'a IArray.t | B_or of 'a IArray.t @@ -10,11 +11,6 @@ type 'a bool_view = | 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 @@ -23,14 +19,9 @@ module type ARG = sig 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 @@ -44,15 +35,16 @@ end module type S = sig module A : ARG module T = A.S.A.Term + module SI = A.S.Solver_internal type state val create : T.state -> state - val simplify : state -> T.t -> T.t + val simplify : state -> SI.simplify_hook (** Simplify given term *) - val cnf : state -> T.t -> A.S.A.Lit.t list Vec.t + val cnf : state -> SI.preprocess_hook (** add clauses for the booleans within the term. *) val theory : A.S.theory @@ -63,6 +55,7 @@ module Make(A : ARG) : S with module A = A = struct module Ty = A.S.A.Ty module T = A.S.A.Term module Lit = A.S.A.Lit + module SI = A.S.Solver_internal type state = { tst: T.state; @@ -88,169 +81,105 @@ module Make(A : ARG) : S with module A = A = struct 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 simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : T.t option = + let tst = self.tst in + match A.view_as_bool t with + | B_bool _ -> None + | B_not u when is_true u -> Some (T.bool tst false) + | B_not u when is_false u -> Some (T.bool tst true) + | B_not _ -> None + | B_and a -> + if IArray.exists is_false a then Some (T.bool tst false) + else if IArray.for_all is_true a then Some (T.bool tst true) + else None + | B_or a -> + if IArray.exists is_true a then Some (T.bool tst true) + else if IArray.for_all is_false a then Some (T.bool tst false) + else None + | B_imply (args, u) -> + (* turn into a disjunction *) + let u = + or_a tst @@ + IArray.append (IArray.map (not_ tst) args) (IArray.singleton u) + in + Some u + | B_ite (a,b,c) -> + (* directly simplify [a] so that maybe we never will simplify one + of the branches *) + let a = SI.Simplify.normalize simp a in + begin match A.view_as_bool a with + | B_bool true -> Some b + | B_bool false -> Some c + | _ -> None + end + | B_equiv (a,b) when is_true a -> Some b + | B_equiv (a,b) when is_false a -> Some (not_ tst b) + | B_equiv (a,b) when is_true b -> Some a + | B_equiv (a,b) when is_false b -> Some (not_ tst a) + | B_equiv _ -> None + | B_eq (a,b) when T.equal a b -> Some (T.bool tst true) + | B_eq _ -> None + | B_atom _ -> None let fresh_term self ~pre ty = A.Gensym.fresh_term self.gensym ~pre ty let fresh_lit (self:state) ~pre : Lit.t = let t = fresh_term ~pre self Ty.bool in Lit.atom self.tst t - (* TODO: polarity *) - let cnf (self:state) (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 + (* TODO: polarity? *) + let cnf (self:state) (solver:SI.t) (acts:SI.actions) (t:T.t) : T.t option = + let add_clause lits = SI.add_clause_permanent solver acts lits in + let rec get_lit (t:T.t) : Lit.t = + match A.view_as_bool t with + | B_bool b -> Lit.atom self.tst ~sign:b (T.bool self.tst true) + | B_not u -> + let lit = get_lit u in + Lit.neg lit + | B_and l -> + let subs = IArray.to_list_map get_lit l in + let proxy = fresh_lit ~pre:"and_" self in + (* add clauses *) + List.iter (fun u -> add_clause [Lit.neg proxy; u]) subs; + add_clause (proxy :: List.map Lit.neg subs); + proxy + | B_or l -> + let subs = IArray.to_list_map get_lit l in + let proxy = fresh_lit ~pre:"or_" self in + (* add clauses *) + List.iter (fun u -> add_clause [Lit.neg u; proxy]) subs; + add_clause (Lit.neg proxy :: subs); + proxy + | B_imply (args, u) -> + let t' = + or_a self.tst @@ + IArray.append (IArray.map (not_ self.tst) args) (IArray.singleton u) in + get_lit t' + | B_ite _ | B_eq _ -> + Lit.atom self.tst t + | B_equiv (a,b) -> + Format.printf "@[cnf: equiv@ %a@ and %a@]@." T.pp a T.pp b; + let a = get_lit a in + let b = get_lit b in + let proxy = fresh_lit ~pre:"equiv_" self in + (* proxy => a<=> b, + ¬proxy => a xor b *) + add_clause [Lit.neg proxy; Lit.neg a; b]; + add_clause [Lit.neg proxy; Lit.neg b; a]; + add_clause [proxy; a; b]; + add_clause [proxy; Lit.neg a; Lit.neg b]; + proxy + | B_atom u -> Lit.atom self.tst u in - (* 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 + let lit = get_lit t in + let u = Lit.term lit in + if T.equal u t then None else Some u - (* TODO: register [cnf] as a clausifier, register [simplify] as a - preprocessor *) - let create_and_setup _si = () + let create_and_setup si = + Log.debug 2 "(th-bool.setup)"; + let st = create (SI.tst si) in + SI.add_simplifier si (simplify st); + SI.add_preprocess si (cnf st); + st let theory = A.S.mk_theory