From f3c02ebd58793b1417ec05eb1a5b7e7e11b60d68 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 28 May 2018 02:43:31 -0500 Subject: [PATCH] wip: implement model construction and evaluation --- src/smt/Congruence_closure.ml | 26 ++ src/smt/Congruence_closure.mli | 4 + src/smt/Equiv_class.ml | 5 + src/smt/Equiv_class.mli | 2 + src/smt/Model.ml | 392 ++++------------------------ src/smt/Model.mli | 31 +-- src/smt/Solver.ml | 207 +-------------- src/smt/Solver_types.ml | 32 +++ src/smt/Theory.ml | 7 +- src/smt/Theory_combine.ml | 9 + src/smt/Theory_combine.mli | 2 + src/smt/Ty.ml | 6 +- src/smt/th_bool/Sidekick_th_bool.ml | 93 ++++--- 13 files changed, 217 insertions(+), 599 deletions(-) diff --git a/src/smt/Congruence_closure.ml b/src/smt/Congruence_closure.ml index 89251165..fdd8b6ea 100644 --- a/src/smt/Congruence_closure.ml +++ b/src/smt/Congruence_closure.ml @@ -584,3 +584,29 @@ let final_check cc : unit = Log.debug 5 "(CC.final_check)"; update_pending cc +(* model: map each uninterpreted equiv class to some ID *) +let mk_model (cc:t) (m:Model.t) : Model.t = + (* populate [repr -> value] table *) + let tbl = Equiv_class.Tbl.create 32 in + Term.Tbl.values cc.tbl + (fun r -> + if is_root_ r then ( + let v = match Model.eval m r.n_term with + | Some v -> v + | None -> + Value.mk_elt + (ID.makef "v_%d" @@ Term.id r.n_term) + (Term.ty r.n_term) + in + Equiv_class.Tbl.add tbl r v + )); + (* now map every uninterpreted term to its representative's value *) + Term.Tbl.to_seq cc.tbl + |> Sequence.fold + (fun m (t,r) -> + if Model.mem t m then m + else ( + let v = Equiv_class.Tbl.find tbl r in + Model.add t v m + )) + m diff --git a/src/smt/Congruence_closure.mli b/src/smt/Congruence_closure.mli index f8cb8ed3..59b4d011 100644 --- a/src/smt/Congruence_closure.mli +++ b/src/smt/Congruence_closure.mli @@ -86,3 +86,7 @@ val explain_unfold_bag : ?init:Lit.Set.t -> t -> explanation Bag.t -> Lit.Set.t val explain_unfold_seq : ?init:Lit.Set.t -> t -> explanation Sequence.t -> Lit.Set.t (** Unfold those explanations into a complete set of literals implying them *) + +(** Enrich a model by mapping terms to their representative's value, + if any. Otherwise map the representative to a fresh value *) +val mk_model : t -> Model.t -> Model.t diff --git a/src/smt/Equiv_class.ml b/src/smt/Equiv_class.ml index ca534589..1f8d3c4e 100644 --- a/src/smt/Equiv_class.ml +++ b/src/smt/Equiv_class.ml @@ -59,5 +59,10 @@ let payload_pred ~f:p n = | l -> List.exists p l end +module Tbl = CCHashtbl.Make(struct + type t = cc_node + let equal = equal + let hash = hash + end) let dummy = make Term.dummy diff --git a/src/smt/Equiv_class.mli b/src/smt/Equiv_class.mli index 22677578..3f46b88b 100644 --- a/src/smt/Equiv_class.mli +++ b/src/smt/Equiv_class.mli @@ -49,6 +49,8 @@ val set_payload : ?can_erase:(payload -> bool) -> t -> payload -> unit @param can_erase if provided, checks whether an existing value is to be replaced instead of adding a new entry *) +module Tbl : CCHashtbl.S with type key = t + (**/**) val dummy : t (**/**) diff --git a/src/smt/Model.ml b/src/smt/Model.ml index 2844623b..2407eaea 100644 --- a/src/smt/Model.ml +++ b/src/smt/Model.ml @@ -3,352 +3,70 @@ (** {1 Model} *) -module A = Ast - -type term = A.term -type ty = A.Ty.t -type domain = ID.t list +open Solver_types type t = { - env: A.env; - (* environment, defining symbols *) - domains: domain A.Ty.Map.t; - (* uninterpreted type -> its domain *) - consts: term ID.Map.t; - (* constant -> its value *) + values: Value.t Term.Map.t; } -let empty : t = { env=A.env_empty; domains=A.Ty.Map.empty; consts=ID.Map.empty} +let empty : t = {values=Term.Map.empty} -let make ~env ~consts ~domains = - (* also add domains to [env] *) - let env = - A.Ty.Map.to_seq domains - |> Sequence.flat_map_l (fun (ty,l) -> List.map (CCPair.make ty) l) - |> Sequence.fold - (fun env (_,cst) -> A.env_add_def env cst A.E_uninterpreted_cst) - env +let[@inline] mem t m = Term.Map.mem t m.values +let[@inline] find t m = Term.Map.get t m.values + +let add t v m : t = + match Term.Map.find t m.values with + | v' -> + if not @@ Value.equal v v' then ( + Error.errorf "@[Model: incompatible values for term %a@ :previous %a@ :new %a@]" + Term.pp t Value.pp v Value.pp v' + ); + m + | exception Not_found -> + {values=Term.Map.add t v m.values} + +(* merge two models *) +let merge m1 m2 : t = + let values = Term.Map.merge_safe m1.values m2.values + ~f:(fun t o -> match o with + | `Left v | `Right v -> Some v + | `Both (v1,v2) -> + if Value.equal v1 v2 then Some v1 + else ( + Error.errorf "@[Model: incompatible values for term %a@ :previous %a@ :new %a@]" + Term.pp t Value.pp v1 Value.pp v2 + )) in - {env; consts; domains} - -type entry = - | E_ty of ty * domain - | E_const of ID.t * term + {values} let pp out (m:t) = - let pp_cst_name out c = ID.pp_name out c in - let pp_ty = A.Ty.pp in - let pp_term = A.pp_term in - let pp_entry out = function - | E_ty (ty,l) -> - Format.fprintf out "(@[<1>type@ %a@ (@[%a@])@])" - pp_ty ty (Util.pp_list pp_cst_name) l - | E_const (c,t) -> - Format.fprintf out "(@[<1>val@ %a@ %a@])" - ID.pp_name c pp_term t - in - let es = - CCList.append - (A.Ty.Map.to_list m.domains |> List.map (fun (ty,dom) -> E_ty (ty,dom))) - (ID.Map.to_list m.consts |> List.map (fun (c,t) -> E_const (c,t))) - in - Format.fprintf out "(@[%a@])" (Util.pp_list pp_entry) es + let pp_tv out (t,v) = Fmt.fprintf out "(@[%a@ -> %a@])" Term.pp t Value.pp v in + Fmt.fprintf out "(@[model@ %a@])" + (Fmt.seq ~sep:Fmt.(return "@ ") pp_tv) (Term.Map.to_seq m.values) -exception Bad_model of t * term * term -exception Error of string +exception No_value -let () = Printexc.register_printer - (function - | Error msg -> Some ("internal error: " ^ msg) - | Bad_model (m,t,t') -> - let msg = CCFormat.sprintf - "@[Bad model:@ goal `@[%a@]`@ evaluates to `@[%a@]`,@ \ - not true,@ in model @[%a@]@." - A.pp_term t A.pp_term t' pp m - in - Some msg - | _ -> None) - -let errorf msg = CCFormat.ksprintf msg ~f:(fun s -> raise (Error s)) - -module VarMap = CCMap.Make(struct - type t = A.Ty.t A.Var.t - let compare = A.Var.compare - end) - -(* var -> term in normal form *) -type subst = A.term lazy_t VarMap.t - -let empty_subst : subst = VarMap.empty - -let rename_var subst v = - let v' = A.Var.copy v in - VarMap.add v (Lazy.from_val (A.var v')) subst, v' - -let rename_vars = CCList.fold_map rename_var - -let pp_subst out (s:subst) = - let pp_pair out (v,lazy t) = - Format.fprintf out "@[<2>%a@ @<1>→ %a@]" A.Var.pp v A.pp_term t - in - Format.fprintf out "[@[%a@]]" - CCFormat.(list ~sep:(return ",@ ") pp_pair) (VarMap.to_list s |> List.rev) - -let rec as_cstor_app env t = match A.term_view t with - | A.Const id -> - begin match A.env_find_def env id with - | Some (A.E_cstor ty) -> Some (id, ty, []) - | _ -> None - end - | A.App (f, l) -> - CCOpt.map (fun (id,ty,l') -> id,ty,l'@l) (as_cstor_app env f) - | _ -> None - -let pp_stack out (l:term list) : unit = - let ppt out t = Format.fprintf out "(@[%a@ :ty %a@])" A.pp_term t A.Ty.pp t.A.ty in - CCFormat.(within "[" "]" (hvbox (list ppt))) out l - -let apply_subst (subst:subst) t = - let rec aux subst t = match A.term_view t with - | A.Num_z _ | A.Num_q _ -> t - | A.Var v -> - begin match VarMap.get v subst with - | None -> t - | Some (lazy t') -> t' +let eval (m:t) (t:Term.t) : Value.t option = + 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 - | A.Undefined_value - | A.Bool _ | A.Const _ -> t - | A.Select (sel, t) -> A.select ~ty:t.A.ty sel (aux subst t) - | A.App (f,l) -> A.app (aux subst f) (List.map (aux subst) l) - | A.If (a,b,c) -> A.if_ (aux subst a) (aux subst b) (aux subst c) - | A.Match (u,m) -> - A.match_ (aux subst u) - (ID.Map.map - (fun (vars,rhs) -> - let subst, vars = rename_vars subst vars in - vars, aux subst rhs) m) - | A.Let (vbs,u) -> - let subst', vbs' = - CCList.fold_map - (fun subst' (x,t) -> - let t = aux subst t in - let subst', x' = rename_var subst' x in - subst', (x',t)) - subst vbs - in - A.let_l vbs' (aux subst' u) - | A.Bind (A.Mu, _,_) -> assert false - | A.Bind (b, x,body) -> - let subst', x' = rename_var subst x in - A.bind ~ty:(A.ty t) b x' (aux subst' body) - | A.Not f -> A.not_ (aux subst f) - | A.Op (op,l) -> A.op op (List.map (aux subst) l) - | A.Asserting {t;guard} -> - A.asserting (aux subst t) (aux subst guard) - | A.Arith (op,l) -> - let ty = A.ty t in - A.arith ty op (List.map (aux subst) l) - in - if VarMap.is_empty subst then t else aux subst t - -type partial_eq = - | Eq - | Neq - | Unknown - -let equal_as_values (_:A.term) (_:A.term) : partial_eq = - Unknown (* TODO *) - -(* Weak Head Normal Form. - @param m the model - @param st the "stack trace" (terms around currently being evaluated) - @param t the term to eval *) -let rec eval_whnf (m:t) (st:term list) (subst:subst) (t:term): term = - Sidekick_sat.Log.debugf 5 - (fun k->k "%s@[<2>eval_whnf `@[%a@]`@ in @[%a@]@]" - (String.make (List.length st) ' ') (* indent *) - A.pp_term t pp_subst subst); - let st = t :: st in - try - eval_whnf_rec m st subst t - with Error.Error msg -> - errorf "@[<2>Model:@ internal type error `%s`@ in %a@]" msg pp_stack st -and eval_whnf_rec m st subst t = match A.term_view t with - | A.Num_q _ - | A.Num_z _ -> t - | A.Undefined_value | A.Bool _ -> t - | A.Var v -> - begin match VarMap.get v subst with - | None -> t - | Some (lazy t') -> - eval_whnf m st empty_subst t' - end - | A.Const c -> - begin match A.env_find_def m.env c with - | Some (A.E_defined (_, t')) -> eval_whnf m st empty_subst t' - | _ -> - begin match ID.Map.get c m.consts with - | None -> t - | Some {A.term=A.Const c';_} when (ID.equal c c') -> t (* trivial cycle *) - | Some t' -> eval_whnf m st empty_subst t' - end - end - | A.App (f,l) -> eval_whnf_app m st subst subst f l - | A.If (a,b,c) -> - let a = eval_whnf m st subst a in - begin match A.term_view a with - | A.Bool true -> eval_whnf m st subst b - | A.Bool false -> eval_whnf m st subst c - | _ -> - let b = apply_subst subst b in - let c = apply_subst subst c in - A.if_ a b c - end - | A.Bind (A.Mu,v,body) -> - let subst' = VarMap.add v (lazy t) subst in - eval_whnf m st subst' body - | A.Let (vbs,u) -> - let subst = - List.fold_left - (fun subst (x,t) -> - let t = lazy (eval_whnf m st subst t) in - VarMap.add x t subst) - subst vbs - in - eval_whnf m st subst u - | A.Bind (A.Fun,_,_) -> apply_subst subst t - | A.Bind ((A.Forall | A.Exists) as b,v,body) -> - let ty = A.Var.ty v in - let dom = - try A.Ty.Map.find ty m.domains - with Not_found -> - errorf "@[<2>could not find type %a in model@ stack %a@]" - A.Ty.pp ty pp_stack st - in - (* expand into and/or over the domain *) - let t' = - let l = - List.map - (fun c_dom -> - let subst' = VarMap.add v (lazy (A.const c_dom ty)) subst in - eval_whnf m st subst' body) - dom - in - begin match b with - | A.Forall -> A.and_l l - | A.Exists -> A.or_l l - | _ -> assert false + | App_cst (c, args) -> + begin try Term.Map.find t m.values + with Not_found -> + match Cst.view c with + | Cst_def udef -> + (* use builtin interpretation function *) + let args = IArray.map aux args in + udef.eval args + | Cst_undef _ -> + Log.debugf 5 (fun k->k "(@[model.eval.undef@ %a@])" Term.pp t); + raise No_value (* no particular interpretation *) end - in - eval_whnf m st subst t' - | A.Select (sel, u) -> - let u = eval_whnf m st subst u in - let t' = A.select ~ty:t.A.ty sel u in - begin match as_cstor_app m.env u with - | None -> t' - | Some (cstor, _, args) -> - if ID.equal cstor sel.A.select_cstor then ( - (* cstors match, take the argument *) - assert (List.length args > sel.A.select_i); - let new_t = List.nth args sel.A.select_i in - eval_whnf m st subst new_t - ) else ( - A.undefined_value t.A.ty - ) - end - | A.Match (u, branches) -> - let u = eval_whnf m st subst u in - begin match as_cstor_app m.env u with - | None -> - let branches = - ID.Map.map - (fun (vars,rhs) -> - let subst, vars = rename_vars subst vars in - vars, apply_subst subst rhs) - branches - in - A.match_ u branches - | Some (c, _, cstor_args) -> - match ID.Map.get c branches with - | None -> assert false - | Some (vars, rhs) -> - assert (List.length vars = List.length cstor_args); - let subst' = - List.fold_left2 - (fun s v arg -> - let arg' = lazy (apply_subst subst arg) in - VarMap.add v arg' s) - subst vars cstor_args - in - eval_whnf m st subst' rhs - end - | A.Not f -> - let f = eval_whnf m st subst f in - begin match A.term_view f with - | A.Bool true -> A.false_ - | A.Bool false -> A.true_ - | _ -> A.not_ f - end - | A.Asserting {t=u; guard=g} -> - let g' = eval_whnf m st subst g in - begin match A.term_view g' with - | A.Bool true -> eval_whnf m st subst u - | A.Bool false -> - A.undefined_value u.A.ty (* assertion failed, uncharted territory! *) - | _ -> A.asserting u g' - end - | A.Op (op, l) -> - let l = List.map (eval_whnf m st subst) l in - begin match op with - | A.And -> - if List.exists A.is_false l then A.false_ - else if List.for_all A.is_true l then A.true_ - else A.and_l l - | A.Or -> - if List.exists A.is_true l then A.true_ - else if List.for_all A.is_false l then A.false_ - else A.or_l l - | A.Imply -> - assert false (* TODO *) - | A.Eq -> - begin match l with - | [] -> assert false - | x :: tail -> - if List.for_all (fun y -> equal_as_values x y = Eq) tail - then A.true_ - else if List.exists (fun y -> equal_as_values x y = Neq) tail - then A.false_ - else A.op A.Eq l - end - | A.Distinct -> - if - Sequence.diagonal_l l - |> Sequence.exists (fun (t,u) -> equal_as_values t u = Eq) - then A.false_ - else if - Sequence.diagonal_l l - |> Sequence.for_all (fun (t,u) -> equal_as_values t u = Neq) - then A.true_ - else A.op A.Distinct l - end - | A.Arith (_, _) -> assert false (* TODO *) -(* beta-reduce [f l] while [f] is a function,constant or variable *) -and eval_whnf_app m st subst_f subst_l f l = match A.term_view f, l with - | A.Bind (A.Fun,v, body), arg :: tail -> - let subst_f = VarMap.add v (lazy (apply_subst subst_l arg)) subst_f in - eval_whnf_app m st subst_f subst_l body tail - | _ -> eval_whnf_app' m st subst_f subst_l f l -(* evaluate [f] and try to beta-reduce if [eval_whnf m f] is a function *) -and eval_whnf_app' m st subst_f subst_l f l = - let f' = eval_whnf m st subst_f f in - begin match A.term_view f', l with - | A.Bind (A.Fun,_,_), _::_ -> - eval_whnf_app m st subst_l subst_l f' l (* beta-reduce again *) - | _ -> - (* blocked *) - let l = List.map (apply_subst subst_l) l in - A.app f' l - end - -(* eval term [t] under model [m] *) -let eval (m:t) (t:term) = eval_whnf m [] empty_subst t + in + try Some (aux t) + with No_value -> None diff --git a/src/smt/Model.mli b/src/smt/Model.mli index 02cae326..e0ac5ebc 100644 --- a/src/smt/Model.mli +++ b/src/smt/Model.mli @@ -3,31 +3,20 @@ (** {1 Model} *) -type term = Ast.term -type ty = Ast.Ty.t -type domain = ID.t list - -type t = private { - env: Ast.env; - (* environment, defining symbols *) - domains: domain Ast.Ty.Map.t; - (* uninterpreted type -> its domain *) - consts: term ID.Map.t; - (* constant -> its value *) +type t = { + values: Value.t Term.Map.t; } -(* TODO: remove *) -(** Trivial model *) val empty : t -val make : - env:Ast.env -> - consts:term ID.Map.t -> - domains:domain Ast.Ty.Map.t -> - t +val add : Term.t -> Value.t -> t -> t + +val mem : Term.t -> t -> bool + +val find : Term.t -> t -> Value.t option + +val merge : t -> t -> t val pp : t CCFormat.printer -val eval : t -> term -> term - -exception Bad_model of t * term * term +val eval : t -> Term.t -> Value.t option diff --git a/src/smt/Solver.ml b/src/smt/Solver.ml index 6b8ffb44..3a14b70f 100644 --- a/src/smt/Solver.ml +++ b/src/smt/Solver.ml @@ -159,204 +159,6 @@ type res = | Unsat of Proof.t | Unknown of unknown -(* FIXME: repair this and output a nice model. -module Model_build : sig - val make: unit -> model - - val check : model -> unit -end = struct - module ValueListMap = CCMap.Make(struct - type t = Term.t list (* normal forms *) - let compare = CCList.compare Term.compare - end) - - type doms = { - dom_of_ty: ID.t list Ty.Tbl.t; (* uninterpreted type -> domain elements *) - dom_of_class: term Term.Tbl.t; (* representative -> normal form *) - dom_of_cst: term Cst.Tbl.t; (* cst -> its normal form *) - dom_of_fun: term ValueListMap.t Cst.Tbl.t; (* function -> args -> normal form *) - dom_traversed: unit Term.Tbl.t; (* avoid cycles *) - } - - let create_doms() : doms = - { dom_of_ty=Ty.Tbl.create 32; - dom_of_class = Term.Tbl.create 32; - dom_of_cst=Cst.Tbl.create 32; - dom_of_fun=Cst.Tbl.create 32; - dom_traversed=Term.Tbl.create 128; - } - - (* pick a term belonging to this type. - we just generate a new constant, as picking true/a constructor might - refine the partial model into an unsatisfiable state. *) - let pick_default ~prefix (doms:doms)(ty:Ty.t) : term = - (* introduce a fresh constant for this equivalence class *) - let elts = Ty.Tbl.get_or ~default:[] doms.dom_of_ty ty in - let cst = ID.makef "%s%s_%d" prefix (Ty.mangle ty) (List.length elts) in - let nf = Term.const (Cst.make_undef cst ty) in - Ty.Tbl.replace doms.dom_of_ty ty (cst::elts); - nf - - (* follow "normal form" pointers deeply in the term *) - let deref_deep (doms:doms) (t:term) : term = - let rec aux t = - let repr = (CC.find t :> term) in - (* if not already done, traverse all parents to update the functions' - models *) - if not (Term.Tbl.mem doms.dom_traversed repr) then ( - Term.Tbl.add doms.dom_traversed repr (); - Bag.to_seq repr.term_parents |> Sequence.iter aux_ignore; - ); - (* find a normal form *) - let nf: term = - begin match CC.normal_form t with - | Some (NF_bool true) -> Term.true_ - | Some (NF_bool false) -> Term.false_ - | Some (NF_cstor (cstor, args)) -> - (* cstor applied to sub-normal forms *) - Term.app_cst cstor.cstor_cst (IArray.map aux args) - | None -> - let repr = (CC.find t :> term) in - begin match Term.Tbl.get doms.dom_of_class repr with - | Some u -> u - | None when Ty.is_uninterpreted t.term_ty -> - let nf = pick_default ~prefix:"$" doms t.term_ty in - Term.Tbl.add doms.dom_of_class repr nf; - nf - | None -> - let nf = pick_default ~prefix:"?" doms t.term_ty in - Term.Tbl.add doms.dom_of_class repr nf; - nf - end - end - in - (* update other tables *) - begin match t.term_cell with - | True | False -> assert false (* should have normal forms *) - | Fun _ | DB _ | Mu _ - -> () - | Builtin b -> ignore (Term.map_builtin aux b) - | If (a,b,c) -> aux_ignore a; aux_ignore b; aux_ignore c - | App_ho (f, l) -> aux_ignore f; List.iter aux_ignore l - | Case (t, m) -> aux_ignore t; ID.Map.iter (fun _ rhs -> aux_ignore rhs) m - | App_cst (f, a) when IArray.is_empty a -> - (* remember [f := c] *) - Cst.Tbl.replace doms.dom_of_cst f nf - | App_cst (f, a) -> - (* remember [f a := c] *) - let a_values = IArray.map aux a |> IArray.to_list in - let map = - Cst.Tbl.get_or ~or_:ValueListMap.empty doms.dom_of_fun f - in - Cst.Tbl.replace doms.dom_of_fun f (ValueListMap.add a_values nf map) - end; - nf - and aux_ignore t = - ignore (aux t) - in - aux t - - (* TODO: maybe we really need a notion of "Undefined" that is - also not a domain element (i.e. equality not defined on it) - + some syntax for it *) - - (* build the model of a function *) - let model_of_fun (doms:doms) (c:cst): Ast.term = - let ty_args, ty_ret = Ty.unfold (Cst.ty c) in - assert (ty_args <> []); - let vars = - List.mapi - (fun i ty -> Ast.Var.make (ID.makef "x_%d" i) (Conv.ty_to_ast ty)) - ty_args - in - let default = match ty_ret.ty_cell with - | Prop -> Ast.true_ (* should be safe: we would have split it otherwise *) - | _ -> - (* TODO: what about other finites types? *) - pick_default ~prefix:"?" doms ty_ret |> Conv.term_to_ast - in - let cases = - Cst.Tbl.get_or ~or_:ValueListMap.empty doms.dom_of_fun c - |> ValueListMap.to_list - |> List.map - (fun (args,rhs) -> - assert (List.length ty_args = List.length vars); - let tests = - List.map2 - (fun v arg -> Ast.eq (Ast.var v) (Conv.term_to_ast arg)) - vars args - in - Ast.and_l tests, Conv.term_to_ast rhs) - in - (* decision tree for the body *) - let body = - List.fold_left - (fun else_ (test, then_) -> Ast.if_ test then_ else_) - default cases - in - Ast.fun_l vars body - - let make () : model = - let env = !model_env_ in - let doms = create_doms () in - (* compute values of meta variables *) - let consts = - !model_support_ - |> Sequence.of_list - |> Sequence.filter_map - (fun c -> - if Ty.is_arrow (Cst.ty c) then None - else - (* find normal form of [c] *) - let t = Term.const c in - let t = deref_deep doms t |> Conv.term_to_ast in - Some (c.cst_id, t)) - |> ID.Map.of_seq - in - (* now compute functions (the previous "deref_deep" have updated their use cases) *) - let consts = - !model_support_ - |> Sequence.of_list - |> Sequence.filter_map - (fun c -> - if Ty.is_arrow (Cst.ty c) - then ( - let t = model_of_fun doms c in - Some (c.cst_id, t) - ) else None) - |> ID.Map.add_seq consts - in - (* now we can convert domains *) - let domains = - Ty.Tbl.to_seq doms.dom_of_ty - |> Sequence.filter_map - (fun (ty,dom) -> - if Ty.is_uninterpreted ty - then Some (Conv.ty_to_ast ty, List.rev dom) - else None) - |> Ast.Ty.Map.of_seq - (* and update env: add every domain element to it *) - and env = - Ty.Tbl.to_seq doms.dom_of_ty - |> Sequence.flat_map_l (fun (_,dom) -> dom) - |> Sequence.fold - (fun env id -> Ast.env_add_def env id Ast.E_uninterpreted_cst) - env - in - Model.make ~env ~consts ~domains - - let check m = - Log.debugf 1 (fun k->k "checking model…"); - Log.debugf 5 (fun k->k "(@[<1>candidate model: %a@])" Model.pp m); - let goals = - Top_goals.to_seq - |> Sequence.map Conv.term_to_ast - |> Sequence.to_list - in - Model.check m ~goals -end - *) - (** {2 Main} *) (* convert unsat-core *) @@ -402,18 +204,15 @@ let[@inline] assume_distinct self l ~neq lit : unit = let check_model (s:t) = Sat_solver.check_model s.solver -(* -type unsat_core = Sat.clause list - *) - (* TODO: main loop with iterative deepening of the unrolling limit (not the value depth limit) *) let solve ?on_exit:(_=[]) ?check:(_=true) ~assumptions (self:t) : res = let r = Sat_solver.solve ~assumptions (solver self) () in match r with - | Sat_solver.Sat (Sidekick_sat.Sat_state _st) -> + | Sat_solver.Sat (Sidekick_sat.Sat_state st) -> Log.debugf 0 (fun k->k "SAT"); - Sat Model.empty + let m = Theory_combine.mk_model (th_combine self) st.iter_trail in + Sat m (* let env = Ast.env_empty in let m = Model.make ~env in diff --git a/src/smt/Solver_types.ml b/src/smt/Solver_types.ml index c7fed204..b9f4d4ed 100644 --- a/src/smt/Solver_types.ml +++ b/src/smt/Solver_types.ml @@ -76,6 +76,7 @@ and cst_view = do_cc: bool; (* participate in congruence closure? *) relevant : 'a. ID.t -> 'a IArray.t -> int -> bool; (* relevant argument? *) ty : ID.t -> term IArray.t -> ty; (* compute type *) + eval: value IArray.t -> value; (* evaluate term *) } (** Methods on the custom term view whose arguments are ['a]. Terms must be printable, and provide some additional theory handles. @@ -118,6 +119,21 @@ and ty_card = | Finite | Infinite +(** Semantic values, used for models (and possibly model-constructing calculi) *) +and value = + | V_bool of bool + | V_element of { + id: ID.t; + ty: ty; + } (** a named constant, distinct from any other constant *) + | V_custom of { + view: value_custom_view; + pp: value_custom_view Fmt.printer; + eq: value_custom_view -> value_custom_view -> bool; + } (** Custom value *) + +and value_custom_view = .. + let[@inline] term_equal_ (a:term) b = a==b let[@inline] term_hash_ a = a.term_id let[@inline] term_cmp_ a b = CCInt.compare a.term_id b.term_id @@ -165,6 +181,22 @@ let rec cmp_exp a b = let pp_cst out a = ID.pp out a.cst_id let id_of_cst a = a.cst_id +let[@inline] eq_ty a b = a.ty_id = b.ty_id + +let eq_value a b = match a, b with + | V_bool a, V_bool b -> a=b + | V_element e1, V_element e2 -> + ID.equal e1.id e2.id && eq_ty e1.ty e2.ty + | V_custom x1, V_custom x2 -> + x1.eq x1.view x2.view + | V_bool _, _ | V_element _, _ | V_custom _, _ + -> false + +let pp_value out = function + | V_bool b -> Fmt.bool out b + | V_element e -> ID.pp out e.id + | V_custom c -> c.pp out c.view + let pp_db out (i,_) = Format.fprintf out "%%%d" i let rec pp_ty out t = match t.ty_view with diff --git a/src/smt/Theory.ml b/src/smt/Theory.ml index fd4bce05..bf057add 100644 --- a/src/smt/Theory.ml +++ b/src/smt/Theory.ml @@ -28,11 +28,14 @@ module type STATE = sig val final_check: t -> Lit.t Sequence.t -> unit (** Final check, must be complete (i.e. must raise a conflict if the set of literals is not satisfiable) *) + + val mk_model : t -> Lit.t Sequence.t -> Model.t + (** Make a model for this theory's terms *) end (** Runtime state of a theory, with all the operations it provides. *) -type state = (module STATE) +type state = (module STATE) (** Unsatisfiable conjunction. Its negation will become a conflict clause *) @@ -85,6 +88,7 @@ let make_st (type st) ?(on_merge=fun _ _ _ _ -> ()) ?(on_assert=fun _ _ -> ()) + ?(mk_model=fun _ _ -> Model.empty) ~final_check ~st () : state = @@ -94,5 +98,6 @@ let make_st let on_merge = on_merge let on_assert = on_assert let final_check = final_check + let mk_model = mk_model end in (module A : STATE) diff --git a/src/smt/Theory_combine.ml b/src/smt/Theory_combine.ml index b9e23d15..c08d7f56 100644 --- a/src/smt/Theory_combine.ml +++ b/src/smt/Theory_combine.ml @@ -120,6 +120,15 @@ let if_sat (self:t) (slice:Lit.t Sat_solver.slice_actions) : _ Sat_solver.res = theories self (fun (module Th) -> Th.final_check Th.state SA.slice_iter)) +let mk_model (self:t) lits : Model.t = + let m = + Sequence.fold + (fun m (module Th : Theory.STATE) -> Model.merge m (Th.mk_model Th.state lits)) + Model.empty (theories self) + in + (* now complete model using CC *) + Congruence_closure.mk_model (cc self) m + (** {2 Various helpers} *) (* forward propagations from CC or theories directly to the SMT core *) diff --git a/src/smt/Theory_combine.mli b/src/smt/Theory_combine.mli index 72d83002..e78c766f 100644 --- a/src/smt/Theory_combine.mli +++ b/src/smt/Theory_combine.mli @@ -15,6 +15,8 @@ val cc : t -> Congruence_closure.t val tst : t -> Term.state val theories : t -> Theory.state Sequence.t +val mk_model : t -> Lit.t Sequence.t -> Model.t + val add_theory : t -> Theory.t -> unit (** How to add new theories *) diff --git a/src/smt/Ty.ml b/src/smt/Ty.ml index ed991ed5..7b944667 100644 --- a/src/smt/Ty.ml +++ b/src/smt/Ty.ml @@ -7,9 +7,9 @@ type def = Solver_types.ty_def let view t = t.ty_view -let equal a b = a.ty_id = b.ty_id -let compare a b = CCInt.compare a.ty_id b.ty_id -let hash a = a.ty_id +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 diff --git a/src/smt/th_bool/Sidekick_th_bool.ml b/src/smt/th_bool/Sidekick_th_bool.ml index f12e27b9..00666c99 100644 --- a/src/smt/th_bool/Sidekick_th_bool.ml +++ b/src/smt/th_bool/Sidekick_th_bool.ml @@ -23,6 +23,43 @@ let id_imply = ID.make "=>" let id_eq = ID.make "=" let id_distinct = ID.make "distinct" +type 'a view = + | B_not of 'a + | B_eq of 'a * 'a + | B_and of 'a IArray.t + | B_or of 'a IArray.t + | B_imply of 'a IArray.t * 'a + | B_distinct of 'a IArray.t + | B_atom of 'a + +exception Not_a_th_term + +let view_id cst_id args = + if ID.equal cst_id id_not && IArray.length args=1 then ( + B_not (IArray.get args 0) + ) else if ID.equal cst_id id_eq && IArray.length args=2 then ( + B_eq (IArray.get args 0, IArray.get args 1) + ) else if ID.equal cst_id id_and then ( + B_and args + ) else if ID.equal cst_id id_or then ( + B_or args + ) else if ID.equal cst_id id_imply && IArray.length args >= 2 then ( + (* conclusion is stored first *) + let len = IArray.length args in + B_imply (IArray.sub args 1 (len-1), IArray.get args 0) + ) else if ID.equal cst_id id_distinct then ( + B_distinct args + ) else ( + raise Not_a_th_term + ) + +let view (t:Term.t) : term view = + match Term.view t with + | App_cst ({cst_id; _}, args) -> + (try view_id cst_id args with Not_a_th_term -> B_atom t) + | _ -> B_atom t + + module C = struct let get_ty _ _ = Ty.prop @@ -37,8 +74,29 @@ module C = struct IArray.get args 0, false | _ -> self, true + let eval id args = match view_id id args with + | B_not (V_bool b) -> Value.bool (not b) + | B_and a when IArray.for_all Value.is_true a -> Value.true_ + | B_and a when IArray.exists Value.is_false a -> Value.false_ + | B_or a when IArray.exists Value.is_true a -> Value.true_ + | B_or a when IArray.for_all Value.is_false a -> Value.false_ + | B_imply (_, V_bool true) -> Value.true_ + | B_imply (a,_) when IArray.exists Value.is_false a -> Value.true_ + | B_imply (a,b) when IArray.for_all Value.is_bool a && Value.is_bool b -> Value.false_ + | B_eq (a,b) -> Value.bool @@ Value.equal a b + | B_atom v -> v + | B_distinct a -> + if + Sequence.diagonal (IArray.to_seq a) + |> Sequence.for_all (fun (x,y) -> not @@ Value.equal x y) + then Value.true_ + else Value.false_ + | B_not _ | B_and _ | B_or _ | B_imply _ + -> Error.errorf "non boolean value in boolean connective" + let mk_cst ?(do_cc=false) id : Cst.t = - {cst_id=id; cst_view=Cst_def { pp=None; abs; ty=get_ty; relevant; do_cc; }; } + {cst_id=id; + cst_view=Cst_def { pp=None; abs; ty=get_ty; relevant; do_cc; eval=eval id; }; } let not = mk_cst id_not let and_ = mk_cst id_and @@ -110,38 +168,6 @@ module Lit = struct let neq tst a b = Lit.atom ~sign:false (neq tst a b) end -type 'a view = - | B_not of 'a - | B_eq of 'a * 'a - | B_and of 'a IArray.t - | B_or of 'a IArray.t - | B_imply of 'a IArray.t * 'a - | B_distinct of 'a IArray.t - | B_atom of 'a - -let view (t:Term.t) : term view = - match Term.view t with - | App_cst ({cst_id; _}, args) -> - if ID.equal cst_id id_not && IArray.length args=1 then ( - B_not t - ) else if ID.equal cst_id id_eq && IArray.length args=2 then ( - B_eq (IArray.get args 0, IArray.get args 1) - ) else if ID.equal cst_id id_and then ( - B_and args - ) else if ID.equal cst_id id_or then ( - B_or args - ) else if ID.equal cst_id id_imply && IArray.length args >= 2 then ( - (* conclusion is stored first *) - let len = IArray.length args in - B_imply (IArray.sub args 1 (len-1), IArray.get args 0) - ) else if ID.equal cst_id id_distinct then ( - B_distinct args - ) else ( - B_atom t - ) - | _ -> B_atom t - - type t = { tst: Term.state; acts: Theory.actions; @@ -229,6 +255,7 @@ let th = Theory.make_st ~on_assert ~final_check + ?mk_model:None (* entirely interpreted *) ~st () in