simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-10 21:24:06 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix: model evaluation must prioritize defined constants' semantics

Browse source
This commit is contained in:
Simon Cruanes 2019-03-22 20:26:06 -05:00
parent 539186bfe6
commit 14992f07ec
2 changed files with 10 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/smt/Model.ml
View file

@ -155,14 +155,14 @@ let eval (m:t) (t:Term.t) : Value.t option =
let b = aux b in
if Value.equal a b then Value.true_ else Value.false_
| App_cst (c, args) ->
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 _ ->
match Cst.view c with
| Cst_def udef ->
(* use builtin interpretation function *)
let args = IArray.map aux args in
udef.eval args
| Cst_undef _ ->
try Term.Map.find t m.values
with Not_found ->
begin match Cst.Map.find c m.funs with
| fi ->
let args = IArray.map aux args |> IArray.to_list in

2
src/th-distinct/Sidekick_th_distinct.ml
View file

@ -181,6 +181,8 @@ module Arg = struct
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)