Source code for pysmt.logics

#
# This file is part of pySMT.
#
#   Copyright 2014 Andrea Micheli and Marco Gario
#
#   Licensed under the Apache License, Version 2.0 (the "License");
#   you may not use this file except in compliance with the License.
#   You may obtain a copy of the License at
#
#       http://www.apache.org/licenses/LICENSE-2.0
#
#   Unless required by applicable law or agreed to in writing, software
#   distributed under the License is distributed on an "AS IS" BASIS,
#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
#   See the License for the specific language governing permissions and
#   limitations under the License.
#
"""Describe all logics supported by pySMT and other logics defined in
the SMTLIB and provides methods to compare and search for particular
logics.
"""

from pysmt.exceptions import UndefinedLogicError, NoLogicAvailableError


[docs]class Theory(object): """Describes a theory similarly to the SMTLIB 2.0.""" def __init__(self, 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, strings = 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 self.strings = strings or False assert not arrays_const or arrays, "Cannot set arrays_const w/o arrays" return def set_lira(self, value=True): res = self.copy() res.integer_arithmetic = value res.real_arithmetic = value return res def set_linear(self, value=True): res = self.copy() res.linear = value return res def set_strings(self, value=True): res = self.copy() res.strings = value return res def set_difference_logic(self, value=True): res = self.copy() if res.integer_arithmetic: res.integer_difference = value if res.real_arithmetic: res.real_difference = value return res def set_arrays(self, value=True): res = self.copy() res.arrays = value return res def set_arrays_const(self, value=True): if not self.arrays and value: res = self.set_arrays() else: res = self.copy() res.arrays_const = value return res def copy(self): new_theory = Theory(arrays = self.arrays, arrays_const = self.arrays_const, bit_vectors = self.bit_vectors, floating_point = self.floating_point, integer_arithmetic = self.integer_arithmetic, real_arithmetic = self.real_arithmetic, integer_difference = self.integer_difference, real_difference = self.real_difference, linear = self.linear, uninterpreted = self.uninterpreted, custom_type = self.custom_type, strings = self.strings) return new_theory def combine(self, other): if self.integer_arithmetic and other.integer_arithmetic: integer_difference = self.integer_difference and other.integer_difference elif self.integer_arithmetic and not other.integer_arithmetic: integer_difference = self.integer_difference elif not self.integer_arithmetic and other.integer_arithmetic: integer_difference = other.integer_difference else: assert not self.integer_arithmetic and not other.integer_arithmetic integer_difference = False if self.real_arithmetic and other.real_arithmetic: real_difference = self.real_difference and other.real_difference elif self.real_arithmetic and not other.real_arithmetic: real_difference = self.real_difference elif not self.real_arithmetic and other.real_arithmetic: real_difference = other.real_difference else: assert not self.real_arithmetic and not other.real_arithmetic real_difference = False return Theory( arrays=self.arrays or other.arrays, arrays_const=self.arrays_const or other.arrays_const, bit_vectors=self.bit_vectors or other.bit_vectors, floating_point=self.floating_point or other.floating_point, integer_arithmetic=self.integer_arithmetic or other.integer_arithmetic, real_arithmetic=self.real_arithmetic or other.real_arithmetic, integer_difference=integer_difference, real_difference=real_difference, linear=self.linear and other.linear, uninterpreted=self.uninterpreted or other.uninterpreted, custom_type=self.custom_type or other.custom_type, strings=self.strings or other.strings) 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 and self.custom_type == other.custom_type and self.strings == other.strings) def __ne__(self, other): return not (self == other) def __le__(self, other): if self.integer_difference == other.integer_difference: le_integer_difference = True elif self.integer_difference and other.integer_arithmetic: le_integer_difference = True elif not self.integer_arithmetic and other.integer_arithmetic: le_integer_difference = True else: le_integer_difference = False if self.real_difference == other.real_difference: le_real_difference = True elif self.real_difference and other.real_arithmetic: le_real_difference = True elif not self.real_arithmetic and other.real_arithmetic: le_real_difference = True else: le_real_difference = False if self.linear == other.linear: le_linear = True elif self.linear and not other.linear: le_linear = True else: le_linear = 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.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 and self.strings <= other.strings) 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 + "Type: %s, " % self.custom_type + "String: %s"% self.strings) __repr__ = __str__
[docs]class Logic(object): """Describes a Logic similarly to the way they are defined in the SMTLIB 2.0 Note: We define more Logics than the ones defined in the SMTLib 2.0. See LOGICS for a list of all the logics and SMTLIB2_LOGICS for the restriction to the ones defined in SMTLIB2.0 """ def __init__(self, name, description, quantifier_free = False, theory=None, **theory_kwargs): self.name = name self.description = description self.quantifier_free = quantifier_free if theory is None: self.theory = Theory(**theory_kwargs) else: self.theory = theory return
[docs] def get_quantified_version(self): """Returns the quantified version of logic.""" if self.quantifier_free: return self target_logic = Logic(name="", description="", quantifier_free=False, theory=self.theory) return get_closer_pysmt_logic(target_logic)
[docs] def is_quantified(self): """Return whether the logic supports quantifiers.""" return not self.quantifier_free
def __str__(self): return self.name def __repr__(self): return str(self) def __eq__(self, other): if other is None or (not isinstance(other, Logic)): return False 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) def __lt__(self, other): return (self != other) and (self.__le__(other)) def __le__(self, other): return (self.theory <= other.theory and self.quantifier_free >= other.quantifier_free) def __ge__(self, other): return (other.__le__(self)) def __gt__(self, other): return (other.__lt__(self)) def __hash__(self): return hash(self.name)
# Logics QF_BOOL = Logic(name="QF_BOOL", description=\ """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 arrays extended with free sort and function symbols but restricted to arrays with integer indices and values.""", arrays=True, integer_arithmetic=True, uninterpreted=True) ALIA = Logic(name="ALIA", description=\ """Closed formulas over the theory of linear integer arithmetic and arrays.""", arrays=True, integer_arithmetic=True) AUFLIRA = Logic(name="AUFLIRA", description=\ """Closed linear formulas with free sort and function symbols over one- and two-dimensional arrays of integer index and real value.""", arrays=True, integer_arithmetic=True, real_arithmetic=True, uninterpreted=True) AUFNIRA = Logic(name="AUFNIRA", description=\ """Closed formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value.""", arrays=True, integer_arithmetic=True, real_arithmetic=True, linear=False, uninterpreted=True) LRA = Logic(name="LRA", description=\ """Closed linear formulas in linear real arithmetic.""", real_arithmetic=True) LIA = Logic(name="LIA", description=\ """Closed linear formulas in linear integer arithmetic.""", integer_arithmetic=True) UFLIRA = Logic(name="UFLIRA", description=\ """Closed linear formulas with free sort and function symbols in linear and real arithmetic.""", integer_arithmetic=True, real_arithmetic=True, linear=True, uninterpreted=True) QF_UFLIRA = Logic(name="QF_UFLIRA", description=\ """Quantifier-free, closed linear formulas with free sort and function symbols in linear and real arithmetic.""", integer_arithmetic=True, real_arithmetic=True, linear=True, quantifier_free=True, uninterpreted=True) NIA = Logic(name="NIA", description=\ """Closed formulas in non-linear integer arithmetic.""", integer_arithmetic=True, linear=False) NRA = Logic(name="NRA", description=\ """Closed formulas in non-linear real arithmetic.""", real_arithmetic=True, linear=False) QF_ABV = Logic(name="QF_ABV", description=\ """Closed quantifier-free formulas over the theory of bitvectors and bitvector arrays.""", quantifier_free=True, arrays=True, bit_vectors=True) QF_AUFBV = Logic(name="QF_AUFBV", description=\ """Closed quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols.""", quantifier_free=True, arrays=True, bit_vectors=True, uninterpreted=True) QF_AUFLIA = Logic(name="QF_AUFLIA", description=\ """Closed quantifier-free linear formulas over the theory of integer arrays extended with free sort and function symbols.""", quantifier_free=True, arrays=True, integer_arithmetic=True, uninterpreted=True) QF_ALIA = Logic(name="QF_ALIA", description=\ """Closed quantifier-free linear formulas over the theory of integer arrays.""", quantifier_free=True, arrays=True, integer_arithmetic=True) QF_AX = Logic(name="QF_AX", description=\ """Closed quantifier-free formulas over the theory of arrays with extensionality.""", quantifier_free=True, arrays=True) QF_BV = Logic(name="QF_BV", description=\ """Closed quantifier-free formulas over the theory of fixed-size bitvectors.""", quantifier_free=True, bit_vectors=True) BV = Logic(name="BV", description=\ """Closed formulas over the theory of fixed-size bitvectors.""", bit_vectors=True) UFBV = Logic(name="UFBV", description=\ """Closed formulas over the theory of fixed-size bitvectors and uninterpreted functions.""", bit_vectors=True, uninterpreted=True) QF_IDL = Logic(name="QF_IDL", description=\ """Difference Logic over the integers. In essence, Boolean combinations of inequations of the form x - y < b where x and y are integer variables and b is an integer constant.""", quantifier_free=True, integer_arithmetic=True, integer_difference=True) QF_LIA = Logic(name="QF_LIA", description=\ """Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables.""", quantifier_free=True, integer_arithmetic=True) QF_LRA = Logic(name="QF_LRA", description=\ """Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables.""", quantifier_free=True, real_arithmetic=True) QF_LIRA = Logic(name="QF_LIRA", description=\ """Unquantified linear integer and real arithmetic""", integer_arithmetic=True, real_arithmetic=True, linear=True, quantifier_free=True) QF_NIA = Logic(name="QF_NIA", description=\ """Quantifier-free integer arithmetic.""", quantifier_free=True, integer_arithmetic=True, linear=False) QF_NRA = Logic(name="QF_NRA", description=\ """Quantifier-free real arithmetic.""", quantifier_free=True, real_arithmetic=True, linear=False) QF_NIRA = Logic(name="QF_NIRA", description="""Quantifier-free integer and real arithmetic.""", quantifier_free=True, integer_arithmetic=True, real_arithmetic=True, linear=False) QF_RDL = Logic(name="QF_RDL", description=\ """Difference Logic over the reals. In essence, Boolean combinations of inequations of the form x - y < b where x and y are real variables and b is a rational constant.""", real_arithmetic=True, quantifier_free=True, real_difference=True) QF_UF = Logic(name="QF_UF", description=\ """Unquantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols.""", quantifier_free=True, uninterpreted=True) UF = Logic(name="UF", description=\ """Quantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols.""", uninterpreted=True) QF_UFBV = Logic(name="QF_UFBV", description=\ """Unquantified formulas over bitvectors with uninterpreted sort function and symbols.""", quantifier_free=True, bit_vectors=True, uninterpreted=True) QF_UFIDL = Logic(name="QF_UFIDL", description=\ """Difference Logic over the integers (in essence) but with uninterpreted sort and function symbols?""", quantifier_free=True, integer_arithmetic=True, integer_difference=True, uninterpreted=True) QF_UFLIA = Logic(name="QF_UFLIA", description=\ """Unquantified linear integer arithmetic with uninterpreted sort and function symbols.""", quantifier_free=True, integer_arithmetic=True, uninterpreted=True) QF_UFLRA = Logic(name="QF_UFLRA", description=\ """Unquantified linear real arithmetic with uninterpreted sort and function symbols.""", quantifier_free=True, real_arithmetic=True, uninterpreted=True) QF_UFNRA = Logic(name="QF_UFNRA", description=\ """Unquantified non-linear real arithmetic with uninterpreted sort and function symbols.""", quantifier_free=True, real_arithmetic=True, linear=False, uninterpreted=True) QF_UFNIA = Logic(name="QF_UFNIA", description=\ """Unquantified non-linear integer arithmetic with uninterpreted sort and function symbols.""", quantifier_free=True, integer_arithmetic=True, linear=False, uninterpreted=True) UFLRA = Logic(name="UFLRA", description=\ """Linear real arithmetic with uninterpreted sort and function symbols.""", real_arithmetic=True, uninterpreted=True) UFNIA = Logic(name="UFNIA", description=\ """Non-linear integer arithmetic with uninterpreted sort and function symbols.""", integer_arithmetic=True, integer_difference=True, linear=False, uninterpreted=True) QF_SLIA = Logic(name="QF_SLIA", description=\ """Extension of LIA including theory of Strings.""", integer_arithmetic=True, quantifier_free=True, uninterpreted=True, strings=True) QF_AUFBVLIRA = Logic(name="QF_AUFBVLIRA", description=\ """Quantifier free Arrays, Bitvectors and LIRA""", linear=True, uninterpreted=True, quantifier_free=True, arrays=True, bit_vectors=True, integer_arithmetic=True, real_arithmetic=True) AUTO = Logic(name="Auto", description="Special logic used to indicate that the logic to be used depends on the formula.") SMTLIB2_LOGICS = frozenset([AUFLIA, AUFLIRA, AUFNIRA, ALIA, LRA, LIA, NIA, NRA, UFLRA, UFNIA, UFLIRA, QF_ABV, QF_AUFBV, QF_AUFLIA, QF_ALIA, QF_AX, QF_BV, QF_IDL, QF_LIA, QF_LRA, QF_NIA, QF_NRA, QF_RDL, QF_UF, QF_UFBV, QF_UFIDL, QF_UFLIA, QF_UFLRA, QF_UFNRA, QF_UFNIA, QF_UFLIRA, QF_SLIA ]) LOGICS = SMTLIB2_LOGICS | frozenset([QF_BOOL, BOOL, QF_AUFBVLIRA, QF_NIRA]) QF_LOGICS = frozenset(_l for _l in LOGICS if _l.quantifier_free) # # This is the set of logics supported by the current version of pySMT # PYSMT_LOGICS = frozenset([QF_BOOL, QF_IDL, QF_LIA, QF_LRA, QF_RDL, QF_UF, QF_UFIDL, QF_UFLIA, QF_UFLRA, QF_UFLIRA, QF_LIRA, BOOL, LRA, LIA, UFLIRA, UFLRA, QF_BV, QF_UFBV, QF_SLIA, QF_BV, QF_UFBV, QF_ABV, QF_AUFBV, QF_AUFLIA, QF_ALIA, QF_AX, QF_AUFBVLIRA, QF_NRA, QF_NIA, QF_NIRA, UFBV, BV, ]) # 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 nl = Logic(name=l.name+"*", description=l.description+" (Extended with Const Arrays)", quantifier_free=l.quantifier_free, theory=new_theory) ext_logics.add(nl) LOGICS = LOGICS | frozenset(ext_logics) PYSMT_LOGICS = PYSMT_LOGICS | frozenset(ext_logics) PYSMT_QF_LOGICS = frozenset(_l for _l in PYSMT_LOGICS if _l.quantifier_free) BV_LOGICS = frozenset(_l for _l in PYSMT_LOGICS if _l.theory.bit_vectors) ARRAYS_LOGICS = frozenset(_l for _l in PYSMT_LOGICS if _l.theory.arrays) ARRAYS_CONST_LOGICS = frozenset(_l for _l in PYSMT_LOGICS \ if _l.theory.arrays_const)
[docs]def get_logic_by_name(name): """Returns the Logic that matches the provided name.""" for logic in LOGICS: if logic.name.lower() == name.lower(): return logic raise UndefinedLogicError(name)
[docs]def convert_logic_from_string(name): """Helper function to parse function arguments. This takes a logic or a string or None, and returns a logic or None. """ if name is not None and isinstance(name, str): name = get_logic_by_name(name) return name
[docs]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
[docs]def get_logic(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, custom_type=False, strings=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 and logic.theory.custom_type == custom_type and logic.theory.strings == strings): return logic raise UndefinedLogicError
[docs]def most_generic_logic(logics): """Given a set of logics, return the most generic one. If a unique most generic logic does not exists, throw an error. """ res = [ l for l in logics if all(l >= x for x in logics)] if len(res) != 1: raise NoLogicAvailableError("Could not find the most generic " "logic for %s." % str(logics)) return res[0]
[docs]def get_closer_logic(supported_logics, logic): """ Returns the smaller supported logic that is greater or equal to the given logic. Raises NoLogicAvailableError if the solver does not support the given logic. """ candidates = [l for l in supported_logics if logic <= l] if len(candidates) == 0: raise NoLogicAvailableError("Logic %s is not supported" % logic) # We remove from the candidates, the logics that subsume another candidate # (i.e. that are more general) because we are looking for the closer logic res = [l for l in candidates if not any(l != k and k <= l for k in candidates)] # There might be multiple incomparable logics that are closer, we # deterministically select the one having a lexicographically smaller name return sorted(res, key=lambda x:str(x))[0]
[docs]def get_closer_pysmt_logic(target_logic): """Returns the closer logic supported by PYSMT.""" return get_closer_logic(PYSMT_LOGICS, target_logic)
[docs]def get_closer_smtlib_logic(target_logic): """Returns the closer logic supported by SMT-LIB 2.0.""" if target_logic == QF_BOOL: return QF_UF if target_logic == BOOL: return LRA return get_closer_logic(SMTLIB2_LOGICS, target_logic)