relations of enumerated types (related to issue 45)

[asgeir386]

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]

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]

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]

Fixed in commit cb17739.

Thanks for catching that, Asgeir.

[asgeir386]

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]

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]

Yes, that’s correct. I am comparing the performance with the version just before the fix

On Oct 30, 2019, at 11:10 AM, Ken McMillan notifications@github.com wrote:

Thanks, Asgeir. Is that compared to the version just before the fix for this issue (i.e., commit a7585aa https://github.com/microsoft/ivy/commit/a7585aa4d724f34408d1090fd281aaab9e922daf)?

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.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/microsoft/ivy/issues/46?email_source=notifications&email_token=ADB2EOTKVEQT33ZVL5ID2KLQRHEYHA5CNFSM4JFI66G2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOECVHU7I#issuecomment-548043389, or unsubscribe https://github.com/notifications/unsubscribe-auth/ADB2EOSPFIY6ZS2DVDJOOGLQRHEYHANCNFSM4JFI66GQ.

[asgeir386]

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]

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.

[asgeir386]

The run-time for the test case that took 4 1/2 hours with z3 enum is now down to about 112min

The cti also look Ok and I will test that part better tomorrow

I changed from MacOS 10.14 Mojave to 10.15 Catalina recently and tomorrow I’m going to try older ivy releases to verify I still see the 46min on Catalina 10.15 (aka that 10.15 is not causing some of the run-time increase)

On Oct 30, 2019, at 6:20 PM, Ken McMillan notifications@github.com wrote:

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.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/microsoft/ivy/issues/46?email_source=notifications&email_token=ADB2EOVEYUNYRGQJRVTC6HLQRIXFXA5CNFSM4JFI66G2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOECWIMIA#issuecomment-548177440, or unsubscribe https://github.com/notifications/unsubscribe-auth/ADB2EOSZJXRROG6Z5DED2K3QRIXFXANCNFSM4JFI66GQ.

[asgeir386]

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_errormessage(ctx, err)) z3.z3types.Z3Exception: Argument #x3 at position 1 does not match declaration (declare-fun bvuge (( BitVec 3) (_ BitVec 3)) Bool)

[kenmcmil]

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]

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]

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.