Skip to content
This repository has been archived by the owner on Jan 27, 2021. It is now read-only.

relations of enumerated types (related to issue 45) #46

Open
asgeir386 opened this issue Oct 25, 2019 · 13 comments
Open

relations of enumerated types (related to issue 45) #46

asgeir386 opened this issue Oct 25, 2019 · 13 comments

Comments

@asgeir386
Copy link

Please refer to Issue #45

After the fix there is still a failure, i.e. when I change the following (that passes)

type packet
type node

to the following:

type packet
type node = {bridge,router}

With same command line as in #45 I now get

..
Initialization must establish the invariant
learning_switch.ivy: line 24: route(N:node) ... PASS
learning_switch.ivy: line 25: route(N:node) ... PASS
learning_switch.ivy: line 26: route(N:node) ... FAIL
searching for a small model... done
warning: model doesn't give a value for enumerated term @n. returning bridge.
warning: model doesn't give a value for enumerated term @n. returning bridge.

Trace follows...


pending(0,bridge,bridge) = false
pending(0,bridge,router) = false
pending(0,router,bridge) = false
pending(0,router,router) = false
@N = bridge
@Y = bridge
@X = router
route.tc(bridge,bridge,bridge) = true
route.tc(bridge,router,router) = true
route.tc(router,bridge,bridge) = true
route.tc(router,router,router) = true
route.tc(bridge,bridge,router) = false
route.tc(bridge,router,bridge) = false
route.tc(router,bridge,router) = false
route.tc(router,router,bridge) = false
link(bridge,bridge) = false
link(bridge,router) = false
link(router,bridge) = false
link(router,router) = false
route.dom(bridge,bridge) = false
route.dom(bridge,router) = false
route.dom(router,bridge) = false
route.dom(router,router) = false
kenmcmil pushed a commit that referenced this issue Oct 29, 2019
@kenmcmil
Copy link
Contributor

Fixed in commit ddb4f25.

This is a bit risky, since it changes the way enumerated types are encoded in Z3, which might impact performance. If you notice any significant performance regressions, please let me know.

@asgeir386
Copy link
Author

Please re-open this issue because I'm seeing a regression, e.g. in ivy-master/examples/ivy/flash3.ivy

Before Issue #46 release: ivy_check diagnose=true trace=true debug=true flash3.ivy
..
in action ni_NAK_Clear when called from the environment:
flash3.ivy: line 442: assumption

OK

After Issue #46 release: ivy_check diagnose=true trace=true debug=true flash3.ivy
..
Initialization must establish the invariant
flash3.ivy: line 477: coherent ... FAIL
searching for a small model... done

Trace follows...


home = 1
@X = 0

flash3.ivy: line 61: cache.state(X) := invalid
cache.state(0) = invalid
cache.state(1) = invalid

kenmcmil added a commit that referenced this issue Oct 29, 2019
@kenmcmil
Copy link
Contributor

Fixed in commit cb17739.

Thanks for catching that, Asgeir.

@asgeir386
Copy link
Author

Ran one of the larger test cases we have (4000 line model + 200 conjectures/invariants + 8 exports) and the test passes (this run didn't exercise any assert statements and I'll do that next)

The run-time went from 45min to 16 hours and that's why I wanted to give you an early heads-up before the regression testing is complete

@kenmcmil
Copy link
Contributor

Thanks, Asgeir. Is that compared to the version just before the fix for this issue (i.e., commit a7585aa)?

I was using a Boolean encoding for enumerated types, but it couldn't handle functions or quantifiers over enumerated types. The fix was to switch to native Z3 enumerated types (that is, using inductive datatypes) but perhaps that is not well optimized in Z3. I could try bit vectors, which probably have received more attention.

@asgeir386
Copy link
Author

asgeir386 commented Oct 30, 2019 via email

@asgeir386
Copy link
Author

It turns out I was running with z3 version 4.4.2

Once I fixed the PATH to pick up z3 version 4.7.1 the run time improved to 4 1/2 hours

@kenmcmil
Copy link
Contributor

I have pushed a new version on branch bv_enum. This version uses Z3 bit vectors to represent Ivy enumerated types. It passes the regression suite, but there are not many tests of enumerated types. Would you might running your tests on this version to look for both performance and functional regressions?

Thanks.

@kenmcmil kenmcmil reopened this Oct 31, 2019
@asgeir386
Copy link
Author

asgeir386 commented Nov 1, 2019 via email

@asgeir386
Copy link
Author

When I modify ivy-bv_enum/examples/pldi16/learning_switch.ivy

Before:

type packet

After:

type packet = {arp,ipv4,ipv6,udp,icmp}

I get the following failure:
Initialization must establish the invariant
Traceback (most recent call last):
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/bin/ivy_check", line 11, in
load_entry_point('ms-ivy==0.3', 'console_scripts', 'ivy_check')()
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_check.py", line 715, in main
check_module()
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_check.py", line 694, in check_module
check_isolate()
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_check.py", line 563, in check_isolate
summarize_isolate(mod)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_check.py", line 452, in summarize_isolate
check_conjs_in_state(mod,ag,ag.states[0])
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_check.py", line 345, in check_conjs_in_state
return check_fcs_in_state(mod,ag,post,[ConjChecker(c,indent) for c in lcs])
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_check.py", line 310, in check_fcs_in_state
model = itr.small_model_clauses(clauses,ffcs,shrink=True)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_transrel.py", line 555, in small_model_clauses
return get_small_model(cls,ivy_logic.uninterpreted_sorts(),[],final_cond=final_cond,shrink=shrink)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_solver.py", line 1105, in get_small_model
the_fmla = clauses_to_z3(clauses)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_solver.py", line 501, in clauses_to_z3
z3_clauses = [conj_to_z3(cl) for cl in clauses.fmlas]
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_solver.py", line 483, in conj_to_z3
return formula_to_z3_closed(cl)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_solver.py", line 544, in formula_to_z3_closed
z3_formula = formula_to_z3_int(fmla)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_solver.py", line 513, in formula_to_z3_int
args = [formula_to_z3_int(arg) for arg in fmla.args]
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_solver.py", line 510, in formula_to_z3_int
return atom_to_z3(fmla)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_solver.py", line 438, in atom_to_z3
tup = [term_to_z3(t) for t in atom.args]
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.3-py2.7.egg/ivy/ivy_solver.py", line 404, in term_to_z3
res = z3.If(z3.UGE(res,max),max,res)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/z3/z3.py", line 3787, in UGE
return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/z3/z3core.py", line 1825, in Z3_mk_bvuge
elems.Check(a0)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/z3/z3core.py", line 1336, in Check
raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: Argument #x3 at position 1 does not match declaration (declare-fun bvuge ((
BitVec 3) (_ BitVec 3)) Bool)

@kenmcmil
Copy link
Contributor

kenmcmil commented Nov 1, 2019

Thanks, Asgeir. That is fixed on branch bv_enum.

Let me know if the bv_enum branch is coming out substantially slower than the baseline. There is another encoding option I can try.

@asgeir386
Copy link
Author

The performance is Ok i.e. when I run a benchmark test that has many enum but no relations of enum types the run-time is 35min for the baseline and 39min for the bv_enum branch

When run a model with a relation of enum types I get an "error: Solver produced inconclusive result" and I think I'm recreating this by modifying the learning_switch.ivy example

command line: ivy_check diagnose=true trace=true learning_switch.ivy

With the learning_switch.ivy example modified as below produces the same error, but runs without issue using the ivy version that uses the Z3 enum type facility

bash-3.2$ diff -w /Users/asgeir/Downloads/ivy-bv_enum-2/examples/pldi16/learning_switch.ivy /Users/asgeir/Downloads/ivy-master/examples/pldi16/learning_switch.ivy
48c48
< type node = {bridge,router0,router1,router2,router3,router4,router5,router6,router7,router8}

type node
122,134d121
<
< conjecture route.tc(N1,N1,N0)
< -> (
< N1=bridge & (N0=router0 | N0=router1 | N0=router2) |
< N1=router0 & (N0=bridge | N0=router1 | N0=router2) |
< N1=router1 & (N0=bridge | N0=router0 | N0=router2) |
< N1=router2 & (N0=bridge | N0=router1 | N0=router1) |
< N1=N0
< )
<
< #
<

@kenmcmil
Copy link
Contributor

kenmcmil commented Nov 4, 2019

Thanks. I can repro that but unfortunately not using smtlib2, so it's a bit hard to submit an issue to Z3. I'm checking whether Z3 actually intends to be a decision procedure for EPR with bit vectors. If not, I have to use a different encoding.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants