Permalink
Browse files

Merge pull request #458 from pysmt/strings_theory

Strings Theory
  • Loading branch information...
mikand committed Nov 27, 2017
2 parents ce526e4 + ffafbdf commit fad65c38405d9bfbb2e2845b7fc2760ebd5f18c3
View
@@ -94,6 +94,7 @@ def check_validity_and_test(args):
big_f = And(f.expr for f in get_example_formulae() \
if not f.logic.theory.bit_vectors and \
not f.logic.theory.arrays and \
not f.logic.theory.strings and \
f.logic.theory.linear)
# Create keyword arguments for the function call.
View
@@ -200,3 +200,9 @@ class Numeral(object):
def __init__(self, obj):
raise NotImplementedError("Z3 is not installed. "\
"We currently do not support stand-alone algebraic numbers.")
#
# Strings
#
def is_python_string(str1):
return type(str1) == str
View
@@ -37,12 +37,21 @@
BV_COMP,
BV_SDIV, BV_SREM,
BV_ASHR,
STR_CONSTANT,
STR_LENGTH, STR_CONCAT, STR_CONTAINS,
STR_INDEXOF, STR_REPLACE, STR_SUBSTR,
STR_PREFIXOF, STR_SUFFIXOF,
STR_TO_INT, INT_TO_STR,
STR_CHARAT,
ARRAY_SELECT, ARRAY_STORE, ARRAY_VALUE,
ALGEBRAIC_CONSTANT)
from pysmt.operators import (BOOL_OPERATORS, THEORY_OPERATORS,
BV_OPERATORS, IRA_OPERATORS, ARRAY_OPERATORS,
STR_OPERATORS,
RELATIONS, CONSTANTS)
from pysmt.typing import BOOL, REAL, INT, BVType
from pysmt.typing import BOOL, REAL, INT, BVType, STRING
from pysmt.decorators import deprecated, assert_infix_enabled
from pysmt.utils import twos_complement
from pysmt.constants import (Fraction, is_python_integer,
@@ -158,6 +167,8 @@ def is_constant(self, _type=None, value=None):
return False
if _type.is_bool_type() and self.node_type() != BOOL_CONSTANT:
return False
if _type.is_string_type() and self.node_type() != STR_CONSTANT:
return False
if _type.is_bv_type():
if self.node_type() != BV_CONSTANT:
return False
@@ -203,6 +214,13 @@ def is_bv_constant(self, value=None, width=None):
return self.is_constant(_type=BVType(width=width),
value=value)
def is_string_constant(self, value=None):
"""Test whether the formula is a String constant.
Optionally, check that the constant has the given value.
"""
return self.is_constant(STRING, value)
def is_algebraic_constant(self):
"""Test whether the formula is an Algebraic Constant"""
return self.node_type() == ALGEBRAIC_CONSTANT
@@ -532,6 +550,9 @@ def is_term(self):
"""
return not (self.is_symbol() and self.symbol_type().is_function_type())
def is_str_op(self):
return self.node_type() in STR_OPERATORS
def symbol_type(self):
"""Return the type of the Symbol."""
assert self.is_symbol()
@@ -557,6 +578,8 @@ def constant_type(self):
return REAL
elif self.node_type() == BOOL_CONSTANT:
return BOOL
elif self.node_type() == STR_CONSTANT:
return STRING
else:
assert self.node_type() == BV_CONSTANT,\
"Unsupported method constant_type '%s'" % self
View
@@ -34,14 +34,17 @@
import pysmt.typing as types
import pysmt.operators as op
from pysmt.fnode import FNode, FNodeContent
from pysmt.exceptions import UndefinedSymbolError, PysmtValueError,PysmtTypeError
from pysmt.walkers.identitydag import IdentityDagWalker
from pysmt.constants import Fraction
from pysmt.constants import (is_pysmt_fraction, is_python_rational,
pysmt_fraction_from_rational)
from pysmt.constants import (is_pysmt_integer,
from pysmt.constants import (is_pysmt_fraction,
is_pysmt_integer,
is_python_rational,
is_python_integer,
is_python_string,
pysmt_fraction_from_rational,
pysmt_integer_from_integer)
@@ -60,6 +63,8 @@ def __init__(self, env=None):
self.int_constants = {}
self.real_constants = {}
self.string_constants = {}
self.true_formula = self.create_node(node_type=op.BOOL_CONSTANT,
args=tuple(),
payload=True)
@@ -364,6 +369,21 @@ def Int(self, value):
self.int_constants[value] = n
return n
def String(self, value):
"""Return a constant of type STRING."""
if value in self.string_constants:
return self.string_constants[value]
if is_python_string(value):
n = self.create_node(node_type=op.STR_CONSTANT,
args=tuple(),
payload=value)
self.string_constants[value] = n
return n
else:
raise TypeError("Invalid type in constant. The type was:" + \
str(type(value)))
def TRUE(self):
"""Return the boolean constant True."""
return self.true_formula
@@ -897,6 +917,86 @@ def BVRepeat(self, formula, count=1):
res = self.BVConcat(res, formula)
return res
def StrLength(self, formula):
"""Returns the length of a formula resulting a String"""
return self.create_node(node_type=op.STR_LENGTH, args=(formula,))
def StrConcat(self, *args):
"""Returns the concatenation of n Strings.
s1, s2, ..., and sn are String terms.
String concatenation takes at least 2 arguments.
"""
tuple_args = self._polymorph_args_to_tuple(args)
if len(tuple_args) <= 1:
raise TypeError("Cannot create a Str_Concat without arguments.")
return self.create_node(node_type=op.STR_CONCAT, args=tuple_args)
def StrContains(self, s, t):
"""Returns wether the String s contains the String t.
s and t are String terms.
"""
return self.create_node(node_type=op.STR_CONTAINS, args=(s, t))
def StrIndexOf(self, s, t, i):
"""Returns the position of the first occurrence of t in s after the index i.
s and t being a non empty strings and i a non-negative integer.
It returns -1 if the value to search for never occurs.
"""
return self.create_node(node_type=op.STR_INDEXOF, args=(s, t, i))
def StrReplace(self, s, t1, t2):
"""Returns a new string where the first occurrence of t1 is replace by t2.
where s, t1 and t2 are string terms, t1 is non-empty.
"""
return self.create_node(node_type=op.STR_REPLACE, args=(s, t1, t2))
def StrSubstr(self, s, i, j):
"""Returns a substring of s starting at i and ending at j+i.
where s is a string term and i, j are integer terms.
"""
return self.create_node(node_type=op.STR_SUBSTR, args=(s, i, j))
def StrPrefixOf(self, s, t):
"""Returns whether the s is a prefix of the string t.
where s and t are string terms.
"""
return self.create_node(node_type=op.STR_PREFIXOF, args=(s, t))
def StrSuffixOf(self, s, t):
"""Returns whether the string s is a suffix of the string t.
where s and t are string terms.
"""
return self.create_node(node_type=op.STR_SUFFIXOF, args=(s, t))
def StrToInt(self, s):
"""Returns the corresponding natural number of s.
If s does not represent a natural number, it returns -1.
"""
return self.create_node(node_type=op.STR_TO_INT, args=(s,))
def IntToStr(self, x):
"""Returns the corresponding String representing the natural number x.
where x is an integer term. If x is not a natural number it
returns the empty String.
"""
return self.create_node(node_type=op.INT_TO_STR, args=(x, ))
def StrCharAt(self, s, i):
"""Returns a single character String at position i.
s is a string term and i is an integer term. i is the position.
"""
return self.create_node(node_type=op.STR_CHARAT, args=(s, i))
def BVToNatural(self, formula):
"""Returns the Natural number represented by the BitVector.
View
@@ -37,7 +37,8 @@ def __init__(self,
real_difference = None,
linear = None,
uninterpreted = None,
custom_type = 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
@@ -49,6 +50,7 @@ def __init__(self,
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
@@ -63,6 +65,11 @@ def set_linear(self, value=True):
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:
@@ -95,7 +102,8 @@ def copy(self):
real_difference = self.real_difference,
linear = self.linear,
uninterpreted = self.uninterpreted,
custom_type = self.custom_type)
custom_type = self.custom_type,
strings = self.strings)
return new_theory
def combine(self, other):
@@ -130,12 +138,12 @@ def combine(self, other):
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)
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
@@ -146,7 +154,8 @@ def __eq__(self, other):
self.real_difference == other.real_difference and
self.linear == other.linear and
self.uninterpreted == other.uninterpreted and
self.custom_type == other.custom_type)
self.custom_type == other.custom_type and
self.strings == other.strings)
def __ne__(self, other):
return not (self == other)
@@ -187,7 +196,8 @@ def __le__(self, other):
self.integer_arithmetic <= other.integer_arithmetic and
le_real_difference and
self.real_arithmetic <= other.real_arithmetic and
le_linear)
le_linear and
self.strings <= other.strings)
def __str__(self):
return ("Arrays: %s, " % self.arrays +
@@ -200,7 +210,8 @@ def __str__(self):
"RD: %s, " % self.real_difference +
"Linear: %s, " % self.linear +
"EUF: %s, " % self.uninterpreted +
"Type: %s" % self.custom_type)
"Type: %s, " % self.custom_type +
"String: %s"% self.strings)
__repr__ = __str__
@@ -583,6 +594,16 @@ def __hash__(self):
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""",
@@ -594,6 +615,7 @@ def __hash__(self):
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.")
@@ -627,7 +649,8 @@ def __hash__(self):
QF_UFLRA,
QF_UFNRA,
QF_UFNIA,
QF_UFLIRA
QF_UFLIRA,
QF_SLIA
])
LOGICS = SMTLIB2_LOGICS | frozenset([ QF_BOOL, BOOL, QF_AUFBVLIRA])
@@ -641,6 +664,8 @@ def __hash__(self):
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,
@@ -676,6 +701,7 @@ def __hash__(self):
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)
@@ -720,7 +746,8 @@ def get_logic(quantifier_free=False,
real_difference=False,
linear=True,
uninterpreted=False,
custom_type=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(...))
@@ -738,7 +765,8 @@ def get_logic(quantifier_free=False,
logic.theory.real_difference == real_difference and
logic.theory.linear == linear and
logic.theory.uninterpreted == uninterpreted and
logic.theory.custom_type == custom_type):
logic.theory.custom_type == custom_type and
logic.theory.strings == strings):
return logic
raise UndefinedLogicError
Oops, something went wrong.

0 comments on commit fad65c3

Please sign in to comment.