handling finite types in new fragment checker

ivy/ivy_fragment.py

@@ -332,7 +332,9 @@ def create_strat_map(assumes,asserts,macros):
     # Get the universally quantified variables. The free variables of
     # asserts and macros won't count as universal.
 
-    universally_quantified_variables = il.universal_variables(all_fmlas)
+    universally_quantified_variables = set(v for v in il.universal_variables(all_fmlas) if
+                                           il.is_uninterpreted_sort(v.sort) or
+                                           il.has_infinite_interpretation(v.sort))
 
 #    print 'universally_quantified_variables : {}'.format([str(v) for v in universally_quantified_variables])
 

ivy/ivy_smtlib.py

@@ -25,6 +25,6 @@ def __init__(self,ivy_name,dom,rng):
 
 # Returns true if the theory with quantifiers is decidable
 def quantifiers_decidable(theory_name):
-    return theory_name in ['int','nat']
+    return theory_name not in ['int','nat']
 
 

ivy/ivy_to_cpp.py

@@ -703,6 +703,7 @@ class init_gen : public gen {
     for ldf in im.relevant_definitions(ilu.symbols_asts(constraints)):
         constraints.append(fix_definition(ldf.formula).to_constraint())
     for c in constraints:
+        print slv.formula_to_z3(c).sexpr()
         fmla = slv.formula_to_z3(c).sexpr().replace('|!1','!1|').replace('\n',' "\n"')
         indent(impl)
         impl.append("  {}\\\n".format(fmla))