mirror of
https://github.com/c-cube/sidekick.git
synced 2026-01-21 16:56:41 -05:00
wip: implement model construction and evaluation
This commit is contained in:
Simon Cruanes
parent
20ecdd6c1f
commit
f3c02ebd58
13 changed files with 217 additions and 599 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
(**/**)
|
||||
|
|
|
|||
392
src/smt/Model.ml
392
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@ (@[<hv>%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 "(@[<v>%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
|
||||
"@[<hv2>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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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 *)
|
||||
|
|
|
|||
|
|
@ -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 *)
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue