#
# 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.
"""
import six
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-dimentional 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_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_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_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_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,
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, 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, six.string_types):
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.
"""
res = [l for l in supported_logics if logic <= l]
if len(res) == 0:
raise NoLogicAvailableError("Logic %s is not supported" % logic)
return min(res)
[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)