misc fixes

ivy/ivy_compiler.py

@@ -969,7 +969,7 @@ def create_sort_order(mod):
     arcs = [(x,s) for s in mod.sort_order for x in sort_dependencies(mod,s)]
     # do nothing if sccs already sorted
     number = dict((x,i) for i,x in enumerate(mod.sort_order))
-    if all(number[x] < number[y] for x,y in arcs):
+    if all(x == 'bool' or number[x] < number[y] for x,y in arcs):
         return
     m = defaultdict(set)
     for x,y in arcs:

ivy/ivy_parser.py

@@ -393,10 +393,6 @@ def p_top_symdecl(p):
     p[0] = p[1]
     p[0].declare(p[2])
 
-def p_symdecl_relationdecl(p):
-    'symdecl : relationdecl'
-    p[0] = p[1]
-
 def p_symdecl_constantdecl(p):
     'symdecl : constantdecl'
     p[0] = p[1]
@@ -413,9 +409,29 @@ def p_constantdecl_var_tterms(p):
     'constantdecl : VAR tterms'
     p[0] = ConstantDecl(*p[2])
 
-def p_relationdecl_relation_tatoms(p):
-    'relationdecl : RELATION tatoms'
-    p[0] = RelationDecl(*apps_to_atoms(p[2]))
+def p_rel_defnlhs(p):
+    'rel : defnlhs'
+    p[1].sort = 'bool'
+    p[0] = ConstantDecl(p[1])
+
+def p_rel_defn(p):
+    'rel : defn'
+    p[0] = DerivedDecl(mk_lf(p[1]))
+
+def p_rels_rel(p):
+    'rels : rel'
+    p[0] = [p[1]]
+
+def p_rels_rels_comma_rel(p):
+    'rels : rels COMMA rel'
+    p[0] = p[1]
+    p[0].append(p[3])
+
+def p_top_relation_rels(p):
+    'top : top RELATION rels'
+    p[0] = p[1]
+    for d in p[3]:
+        p[0].declare(d)
 
 def p_tatoms_tatom(p):
     'tatoms : tatom'

test/run_expects.py

@@ -47,7 +47,7 @@ checks = [
       ['object_example','OK'],
       ['paraminit2','OK'],
       ['paraminit3','OK'],
-      ['paraminit','OK'],
+      ['paraminit','isolate=iso_foo','OK'],
       ['pingpongclock','OK'],
       ['pingpong','OK'],
       ['po_example','OK'],
@@ -104,7 +104,7 @@ to_cpps = [
          ['leader_election_ring_repl_err','target=repl','isolate=iso_impl','error: relevant axiom asgn.injectivity not enforced'],
          ['leader_election_ring_repl_err2','target=repl','isolate=iso_impl','error: No implementation for action node.get_next'],
          ['leader_election_ring_udp2_warn','target=repl','isolate=iso_impl','warning: action sec.timeout is implicitly exported'],
-         ['paraminit','target=repl','error: cannot compile "foo.bit" because type t is uninterpreted'],
+         ['paraminit','target=repl','error: cannot compile initial constraint on "foo.bit" because type t is large. suggest using "after init"'],
          ['paraminit2','target=repl','isolate=iso_foo','initial condition depends on stripped parameter'],
       ]
      ]

test/tilelink_unit_test.sh

@@ -2,5 +2,5 @@
 
 cd ../examples/tilelink/unit_test
 ivy_to_cpp isolate=iso_b tilelink_coherence_manager_tester.ivy
-g++ -c tilelink_coherence_manager_tester.cpp
+g++ -c -I$Z3DIR/include tilelink_coherence_manager_tester.cpp