Existential quantifiers as symbolic values #147
Conversation
pcarrott
force-pushed
the
svalue-exists
branch
from
5abc62c to
861bab9
Compare
|
C_values will go away, so no need :) |
N1ark
left a comment
N1ark
left a comment
There was a problem hiding this comment.
Nice addition thanks :)
Sorry ton of nitpicks just to keep the codebase clean
| | Var v -> | ||
| if List.exists (fun (v', _) -> Var.equal v v') vs then () | ||
| else f sv |
There was a problem hiding this comment.
| | Var v -> | |
| if List.exists (fun (v', _) -> Var.equal v v') vs then () | |
| else f sv | |
| | Var v when List.exists (fun (v', _) -> Var.equal v v') vs -> () |
| match List.find_opt (fun (v', _) -> Var.equal v v') vs with | ||
| | Some (v, _) -> v | ||
| | None -> subst_var v |
There was a problem hiding this comment.
| match List.find_opt (fun (v', _) -> Var.equal v v') vs with | |
| | Some (v, _) -> v | |
| | None -> subst_var v | |
| if List.exists (fun (v', _) -> Var.equal v v') vs then v | |
| else subst_var v |
| let exists vs body = Exists (vs, body) <| TBool | ||
|
|
There was a problem hiding this comment.
| let exists vs body = Exists (vs, body) <| TBool | |
| let exists vs body = | |
| match vs with [] -> body | _ :: _ -> Exists (vs, body) <| TBool |
| let eval_without_vars vs = | ||
| let eval_var v ty = | ||
| match List.find_opt (fun (v', _) -> Var.equal v v') vs with | ||
| | Some (v, ty) -> mk_var v ty | ||
| | None -> eval_var v ty | ||
| in | ||
| eval ~eval_var |
There was a problem hiding this comment.
could you move this into the Exists branch since it's only used there? this also avoids an intermediary function since the inputs are known
|
|
||
| let rec encode_value (v : Svalue.t) = | ||
| let var v = atom (Svalue.Var.to_string v) in |
There was a problem hiding this comment.
I'm being a bit nitpicky here I'll admit but it feels more cohesive to, instead of defining this inside encode_value, having
let encode_var v = atom (Svalue.Var.to_string v) | | Exists (vs, sv) -> | ||
| let exists l x = list [ atom "exists"; list l; x ] in | ||
| let encode_var_memo (v, ty) = list [ var v; sort_of_ty ty ] in | ||
| exists (List.map encode_var_memo vs) (encode_value_memo sv) |
There was a problem hiding this comment.
- I avoid direct uses of
atomin encodings, as it can be error prone and overall not super nice; could you move this tosolvers/smt_utils?
Also ideally use the appropriate Smtlib functions, so i think it should rather look likelet exists qs e = app_ "exists" [ list qs; e ]
encode_var_memoseems to imply there is some memoisation happening, which there isn't; can you rename it likeencode_bindingplease :)
| let test = | ||
| let v = Svalue.Var.of_int 42 in | ||
| let ty = Svalue.t_bool in | ||
| let sv = Svalue.mk_var v ty in | ||
| let exists = Svalue.Bool.exists [ (v, ty) ] sv in | ||
| if%sat Typed.type_ exists then return 42 else return (-1) |
There was a problem hiding this comment.
last thing ; add a definition for exists in Typed, so this test is well typed, rather than having to resort to Typed.type_ at the end
The signature should be something like
val exists : (Var.t * ty) list -> [< T.sbool ] t -> [> T.sbool ] t
|
when possible always use the most restrained form of a function -- e.g. if a |
N1ark
added
enhancement
Added a new symbolic value
Exists of (Var.t * ty) list * ttobv_values. This is needed for RUXt.Can do the same for
c_valuesfor consistency, though it is not something I need atm.