Merge pull request #411 from pysmt/griggio_smtlib_tests

Extend parser to support declare-sort/define-sort

pysmt/environment.py

@@ -53,7 +53,7 @@ class Environment(object):
     FreeVarsOracleClass= pysmt.oracles.FreeVarsOracle
     SizeOracleClass = pysmt.oracles.SizeOracle
     AtomsOracleClass = pysmt.oracles.AtomsOracle
-
+    TypesOracleClass = pysmt.oracles.TypesOracle
 
     def __init__(self):
         self._stc = self.TypeCheckerClass(self)
@@ -68,6 +68,7 @@ def __init__(self):
         self._fvo = self.FreeVarsOracleClass(self)
         self._sizeo = self.SizeOracleClass(self)
         self._ao = self.AtomsOracleClass(self)
+        self._typeso = self.TypesOracleClass(self)
         self._type_manager = self.TypeManagerClass(self)
 
         self._factory = None
@@ -118,6 +119,11 @@ def theoryo(self):
         """ Get the Theory Oracle """
         return self._theoryo
 
+    @property
+    def typeso(self):
+        """ Get the Types Oracle """
+        return self._typeso
+
     @property
     def fvo(self):
         """ Get the FreeVars Oracle """

pysmt/logics.py

@@ -27,28 +27,29 @@
 class Theory(object):
     """Describes a theory similarly to the SMTLIB 2.0."""
     def __init__(self,
-                 arrays = False,
-                 arrays_const = False,
-                 bit_vectors = False,
-                 floating_point = False,
-                 integer_arithmetic = False,
-                 real_arithmetic = False,
-                 integer_difference = False,
-                 real_difference = False,
-                 linear = True,
-                 uninterpreted = False):
-        self.arrays = arrays
-        self.arrays_const = arrays_const
-        self.bit_vectors = bit_vectors
-        self.floating_point = floating_point
-        self.integer_arithmetic = integer_arithmetic
-        self.real_arithmetic = real_arithmetic
-        self.integer_difference = integer_difference
-        self.real_difference = real_difference
-        self.linear = linear
-        self.uninterpreted = uninterpreted
+                 arrays = None,
+                 arrays_const = None,
+                 bit_vectors = None,
+                 floating_point = None,
+                 integer_arithmetic = None,
+                 real_arithmetic = None,
+                 integer_difference = None,
+                 real_difference = None,
+                 linear = None,
+                 uninterpreted = None,
+                 custom_type = None):
+        self.arrays = arrays or False
+        self.arrays_const = arrays_const or False
+        self.bit_vectors = bit_vectors or False
+        self.floating_point = floating_point or False
+        self.integer_arithmetic = integer_arithmetic or False
+        self.real_arithmetic = real_arithmetic or False
+        self.integer_difference = integer_difference or False
+        self.real_difference = real_difference or False
+        self.linear = linear if linear is not None else True
+        self.uninterpreted = uninterpreted or False
+        self.custom_type = custom_type or False
         assert not arrays_const or arrays, "Cannot set arrays_const w/o arrays"
-
         return
 
     def set_lira(self, value=True):
@@ -93,7 +94,8 @@ def copy(self):
                             integer_difference = self.integer_difference,
                             real_difference = self.real_difference,
                             linear = self.linear,
-                            uninterpreted = self.uninterpreted)
+                            uninterpreted = self.uninterpreted,
+                            custom_type = self.custom_type)
         return new_theory
 
     def combine(self, other):
@@ -127,22 +129,24 @@ def combine(self, other):
             integer_difference=integer_difference,
             real_difference=real_difference,
             linear=self.linear and other.linear,
-            uninterpreted=self.uninterpreted or other.uninterpreted)
+            uninterpreted=self.uninterpreted or other.uninterpreted,
+            custom_type=self.custom_type or other.custom_type)
 
     def __eq__(self, other):
         if other is None or (not isinstance(other, Theory)):
             return False
 
-        return self.arrays == other.arrays and \
-            self.arrays_const == other.arrays_const and \
-            self.bit_vectors == other.bit_vectors and \
-            self.floating_point == other.floating_point and \
-            self.integer_arithmetic == other.integer_arithmetic and \
-            self.real_arithmetic == other.real_arithmetic and \
-            self.integer_difference == other.integer_difference and \
-            self.real_difference == other.real_difference and \
-            self.linear == other.linear and \
-            self.uninterpreted == other.uninterpreted
+        return (self.arrays == other.arrays and
+                self.arrays_const == other.arrays_const and
+                self.bit_vectors == other.bit_vectors and
+                self.floating_point == other.floating_point and
+                self.integer_arithmetic == other.integer_arithmetic and
+                self.real_arithmetic == other.real_arithmetic and
+                self.integer_difference == other.integer_difference and
+                self.real_difference == other.real_difference and
+                self.linear == other.linear and
+                self.uninterpreted == other.uninterpreted and
+                self.custom_type == other.custom_type)
 
     def __ne__(self, other):
         return not (self == other)
@@ -178,23 +182,25 @@ def __le__(self, other):
                 self.bit_vectors <= other.bit_vectors and
                 self.floating_point <= other.floating_point and
                 self.uninterpreted <= other.uninterpreted and
+                self.custom_type <= other.custom_type and
                 le_integer_difference and
                 self.integer_arithmetic <= other.integer_arithmetic and
                 le_real_difference and
                 self.real_arithmetic <= other.real_arithmetic and
                 le_linear)
 
     def __str__(self):
-        return "Arrays: %s, " % self.arrays +\
-            "ArraysConst: %s, " % self.arrays_const +\
-            "BV: %s, " % self.bit_vectors +\
-            "FP: %s, " % self.floating_point +\
-            "IA: %s, " % self.integer_arithmetic +\
-            "RA: %s, " % self.real_arithmetic +\
-            "ID: %s, " % self.integer_difference +\
-            "RD: %s, " % self.real_difference +\
-            "Linear: %s, " % self.linear +\
-            "EUF: %s" % self.uninterpreted
+        return ("Arrays: %s, " % self.arrays +
+                "ArraysConst: %s, " % self.arrays_const +
+                "BV: %s, " % self.bit_vectors +
+                "FP: %s, " % self.floating_point +
+                "IA: %s, " % self.integer_arithmetic +
+                "RA: %s, " % self.real_arithmetic +
+                "ID: %s, " % self.integer_difference +
+                "RD: %s, " % self.real_difference +
+                "Linear: %s, " % self.linear +
+                "EUF: %s, " % self.uninterpreted +
+                "Type: %s" % self.custom_type)
 
     __repr__ = __str__
 
@@ -210,34 +216,14 @@ class Logic(object):
     def __init__(self, name, description,
                  quantifier_free = False,
                  theory=None,
-                 arrays=False,
-                 arrays_const=False,
-                 bit_vectors=False,
-                 floating_point=False,
-                 integer_arithmetic=False,
-                 real_arithmetic=False,
-                 integer_difference=False,
-                 real_difference=False,
-                 linear=True,
-                 uninterpreted=False):
-
+                 **theory_kwargs):
         self.name = name
         self.description = description
         self.quantifier_free = quantifier_free
         if theory is None:
-            self.theory = Theory(arrays=arrays,
-                                 arrays_const=arrays_const,
-                                 bit_vectors=bit_vectors,
-                                 floating_point=floating_point,
-                                 integer_arithmetic=integer_arithmetic,
-                                 real_arithmetic=real_arithmetic,
-                                 integer_difference=integer_difference,
-                                 real_difference=real_difference,
-                                 linear=linear,
-                                 uninterpreted=uninterpreted)
+            self.theory = Theory(**theory_kwargs)
         else:
             self.theory = theory
-
         return
 
     def get_quantified_version(self):
@@ -263,10 +249,9 @@ def __eq__(self, other):
         if other is None or (not isinstance(other, Logic)):
             return False
 
-        return self.name == other.name and \
-            self.description == other.description and \
-            self.quantifier_free == other.quantifier_free and \
-            self.theory == other.theory
+        return (self.name == other.name and
+                self.quantifier_free == other.quantifier_free and
+                self.theory == other.theory)
 
     def __ne__(self, other):
         return not (self == other)
@@ -294,13 +279,19 @@ def __hash__(self):
                 """The simplest logic: quantifier-free boolean logic.""",
                 quantifier_free=True)
 
-
 BOOL = Logic(name="BOOL",
              description=\
              """Quantified boolean logic.""")
 QBF=BOOL # Provide additional name for consistency with literature
 
 
+QF_BOOLt = Logic(name="QF_BOOLt",
+                description=\
+                """Quantifier-free boolean logic with custom sorts.""",
+                 quantifier_free=True,
+                 custom_type=True)
+
+
 AUFLIA = Logic(name="AUFLIA",
                description=\
 """Closed formulas over the theory of linear integer arithmetic and
@@ -655,11 +646,22 @@ def __hash__(self):
                           QF_NRA, QF_NIA, UFBV, BV,
                       ])
 
-# PySMT Supports constant arrays: We auto-generate these logics
-#     QF_AUFBV  becomes QF_AUFBV*
+# PySMT Logics includes additional features:
+#  - constant arrays: QF_AUFBV  becomes QF_AUFBV*
+#  - theories without custom types (no-name) QF_AUFBV QF_AUFBVt
 #
+
 ext_logics = set()
 for l in PYSMT_LOGICS:
+    if not l.theory.custom_type:
+        new_theory = l.theory.copy()
+        new_theory.custom_type = True
+        nl = Logic(name=l.name+"t",
+                   description=l.description+" (with Custom Types)",
+                   quantifier_free=l.quantifier_free,
+                   theory=new_theory)
+        ext_logics.add(nl)
+
     if l.theory.arrays:
         new_theory = l.theory.copy()
         new_theory.arrays_const = True
@@ -669,6 +671,8 @@ def __hash__(self):
                    theory=new_theory)
         ext_logics.add(nl)
 
+
+
 LOGICS = LOGICS | frozenset(ext_logics)
 PYSMT_LOGICS = PYSMT_LOGICS | frozenset(ext_logics)
 
@@ -696,30 +700,14 @@ def convert_logic_from_string(name):
         name = get_logic_by_name(name)
     return name
 
-def get_logic_name(quantifier_free=False,
-                   arrays=False,
-                   arrays_const=False,
-                   bit_vectors=False,
-                   floating_point=False,
-                   integer_arithmetic=False,
-                   real_arithmetic=False,
-                   integer_difference=False,
-                   real_difference=False,
-                   linear=True,
-                   uninterpreted=False):
-    """Returns the name of the Logic that matches the given properties."""
-
-    return get_logic(quantifier_free,
-                     arrays,
-                     arrays_const,
-                     bit_vectors,
-                     floating_point,
-                     integer_arithmetic,
-                     real_arithmetic,
-                     integer_difference,
-                     real_difference,
-                     linear,
-                     uninterpreted).name
+
+def get_logic_name(**logic_kwargs):
+    """Returns the name of the Logic that matches the given properties.
+
+    See get_logic for the list of parameters.
+    """
+    return get_logic(**logic_kwargs).name
+
 
 def get_logic(quantifier_free=False,
               arrays=False,
@@ -731,24 +719,26 @@ def get_logic(quantifier_free=False,
               integer_difference=False,
               real_difference=False,
               linear=True,
-              uninterpreted=False):
+              uninterpreted=False,
+              custom_type=False):
     """Returns the Logic that matches the given properties.
 
     Equivalent (but better) to executing get_logic_by_name(get_logic_name(...))
     """
 
     for logic in LOGICS:
-        if (  logic.quantifier_free == quantifier_free and
-              logic.theory.arrays == arrays and \
-              logic.theory.arrays_const == arrays_const and \
-              logic.theory.bit_vectors == bit_vectors and \
-              logic.theory.floating_point == floating_point and \
-              logic.theory.integer_arithmetic == integer_arithmetic and \
-              logic.theory.real_arithmetic == real_arithmetic and \
-              logic.theory.integer_difference == integer_difference and \
-              logic.theory.real_difference == real_difference and \
-              logic.theory.linear == linear and \
-              logic.theory.uninterpreted == uninterpreted):
+        if (logic.quantifier_free == quantifier_free and
+            logic.theory.arrays == arrays and
+            logic.theory.arrays_const == arrays_const and
+            logic.theory.bit_vectors == bit_vectors and
+            logic.theory.floating_point == floating_point and
+            logic.theory.integer_arithmetic == integer_arithmetic and
+            logic.theory.real_arithmetic == real_arithmetic and
+            logic.theory.integer_difference == integer_difference and
+            logic.theory.real_difference == real_difference and
+            logic.theory.linear == linear and
+            logic.theory.uninterpreted == uninterpreted and
+            logic.theory.custom_type == custom_type):
             return logic
     raise UndefinedLogicError