fixing fragment checker to allow quantifiers over finite sorts

ivy/ivy_logic.py

@@ -70,6 +70,7 @@ from logic import And,Or,Not,Implies,Iff,Ite,ForAll,Exists,Lambda
 from type_inference import concretize_sorts, concretize_terms
 from collections import defaultdict
 from itertools import chain
+import ivy_smtlib
 
 allow_unsorted = False
 repr = str
@@ -1249,6 +1250,11 @@ def is_uninterpreted_sort(s):
     s = canonize_sort(s)
     return isinstance(s,UninterpretedSort) and s.name not in sig.interp
 
+# For now, int is the only infinite interpreted sort
+def has_infinite_interpretation(s):
+    s = canonize_sort(s)
+    return s.name in sig.interp and not ivy_smtlib.quantifiers_decidable(s.name)
+
 def is_interpreted_sort(s):
     s = canonize_sort(s)
     return (isinstance(s,UninterpretedSort) or isinstance(s,EnumeratedSort)) and s.name in sig.interp

ivy/ivy_smtlib.py

@@ -0,0 +1,30 @@
+#
+# Copyright (c) Microsoft Corporation. All Rights Reserved.
+#
+"""
+   This module defines the theories available in SMTLIB
+"""
+
+class Theory(object):
+    def __init__(self,ivy_name,sorts,ops,infinite):
+        self.ivy_name,self.sorts,self.ops,self.infinite = ivy_name,sorts,ops,infinite
+    pass
+
+class Sort(object):
+    def __init__(self,ivy_name):
+        self.ivy_name = ivy_name
+
+class Operator(object):
+    def __init__(self,ivy_name,dom,rng):
+        self.ivy_name,self.dom,self.rng = ivy_name,dom,rng
+
+
+intSort = Sort('int')
+intOps = [Operator(n,[intSort,intSort],intSort) for n in ['+','-','*','/']]
+liaTheory = Theory('int',[intSort],intOps,True)
+
+# Returns true if the theory with quantifiers is decidable
+def quantifiers_decidable(theory_name):
+    return theory_name != 'int'
+
+    

ivy/ivy_theory.py

@@ -221,7 +221,8 @@ def get_unstratified_funs(assumes,asserts,macros):
         y = find(y)
         if isinstance(x,tuple) and (il.is_interpreted_symbol(x[0]) or x[0].name == '='):
             if any(v in universally_quantified_variables and 
-                   v.sort == x[0].sort.dom[x[1]] for v in y.variables):
+                   v.sort == x[0].sort.dom[x[1]] and
+                   il.has_infinite_interpretation(v.sort) for v in y.variables):
                 bad_interpreted.add(x[0])
 
     return fun_sccs, bad_interpreted

ivy/ivy_utils.py

@@ -547,16 +547,18 @@ def get_default_ui_compile_kwargs():
     return mod.compile_kwargs
     
 
-
+enable_debug = BooleanParameter("debug",False)
 
 def dbg(*exprs):
     """Print expressions evaluated in the caller's frame."""
+    assert enable_debug,"must use debug=true to enable debug output"
     import inspect
     frame = inspect.currentframe()
     try:
         locs = frame.f_back.f_locals
+        globs = frame.f_back.f_globals
         for e in exprs:
-            print "{}:{}".format(e,eval(e,globals(),locs))
+            print "{}:{}".format(e,eval(e,globs,locs))
     finally:
         del frame