diff --git a/README.md b/README.md index 7c6b285bc2..a9c8e16e4a 100644 --- a/README.md +++ b/README.md @@ -43,9 +43,13 @@ JavaSMT can express formulas in the following theories: - Integer - Rational - Bitvector - - Floating point + - Floating Point - Array - Uninterpreted Function + - String and RegEx + +The concrete support for a certain theory depends on the underlying SMT solver. +Only a few SMT solvers provide support for theories like Arrays, Floating Point, String or RegEx. Currently JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started.md) for installation): diff --git a/src/org/sosy_lab/java_smt/api/FormulaManager.java b/src/org/sosy_lab/java_smt/api/FormulaManager.java index cee7686f0f..2259a03f73 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/FormulaManager.java @@ -78,6 +78,13 @@ public interface FormulaManager { */ QuantifiedFormulaManager getQuantifiedFormulaManager(); + /** + * Returns the String Theory. + * + * @throws UnsupportedOperationException If the theory is not supported by the solver. + */ + StringFormulaManager getStringFormulaManager(); + /** * Create variable of the type equal to {@code formulaType}. * diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index ede56e95b7..4f32783d61 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -62,6 +62,14 @@ public boolean isSLType() { return false; } + public boolean isStringType() { + return false; + } + + public boolean isRegexType() { + return false; + } + @Override public abstract String toString(); @@ -344,6 +352,44 @@ public String toSMTLIBString() { } } + public static final FormulaType StringType = + new FormulaType<>() { + + @Override + public boolean isStringType() { + return true; + } + + @Override + public String toString() { + return "String"; + } + + @Override + public String toSMTLIBString() { + return "String"; + } + }; + + public static final FormulaType RegexType = + new FormulaType<>() { + + @Override + public boolean isRegexType() { + return true; + } + + @Override + public String toString() { + return "RegLan"; + } + + @Override + public String toSMTLIBString() { + return "RegLan"; + } + }; + /** * Parse a string and return the corresponding type. This method is the counterpart of {@link * #toString()}. @@ -355,6 +401,10 @@ public static FormulaType fromString(String t) { return IntegerType; } else if (RationalType.toString().equals(t)) { return RationalType; + } else if (StringType.toString().equals(t)) { + return StringType; + } else if (RegexType.toString().equals(t)) { + return RegexType; } else if (FloatingPointRoundingModeType.toString().equals(t)) { return FloatingPointRoundingModeType; } else if (t.startsWith("FloatingPoint<")) { diff --git a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java index dcd0524d74..ed05d08d95 100644 --- a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java +++ b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java @@ -256,6 +256,34 @@ public enum FunctionDeclarationKind { FP_AS_IEEEBV, FP_FROM_IEEEBV, + // String and Regex theory + + STR_CONCAT, + STR_PREFIX, + STR_SUFFIX, + STR_CONTAINS, + STR_SUBSTRING, + STR_REPLACE, + STR_REPLACE_ALL, + STR_CHAR_AT, + STR_LENGTH, + STR_INDEX_OF, + STR_TO_RE, + STR_IN_RE, + STR_TO_INT, + INT_TO_STR, + STR_LT, + STR_LE, + RE_PLUS, + RE_STAR, + RE_OPTIONAL, + RE_CONCAT, + RE_UNION, + RE_RANGE, + RE_INTERSECT, + RE_COMPLEMENT, + RE_DIFFERENCE, + // default case /** diff --git a/src/org/sosy_lab/java_smt/api/Model.java b/src/org/sosy_lab/java_smt/api/Model.java index 6e786a837b..d7c13caae5 100644 --- a/src/org/sosy_lab/java_smt/api/Model.java +++ b/src/org/sosy_lab/java_smt/api/Model.java @@ -90,6 +90,14 @@ public interface Model extends Iterable, AutoCloseable { @Nullable BigInteger evaluate(BitvectorFormula f); + /** + * Type-safe evaluation for string formulas. + * + *

The formula does not need to be a variable, we also allow complex expression. + */ + @Nullable + String evaluate(StringFormula f); + /** * Iterate over all values present in the model. Note that iterating multiple times may be * inefficient for some solvers, it is recommended to use {@link diff --git a/src/org/sosy_lab/java_smt/api/RegexFormula.java b/src/org/sosy_lab/java_smt/api/RegexFormula.java new file mode 100644 index 0000000000..af7849bd32 --- /dev/null +++ b/src/org/sosy_lab/java_smt/api/RegexFormula.java @@ -0,0 +1,15 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2021 Alejandro Serrano Mena +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.api; + +import com.google.errorprone.annotations.Immutable; + +/** A formula of the string sort. */ +@Immutable +public interface RegexFormula extends Formula {} diff --git a/src/org/sosy_lab/java_smt/api/StringFormula.java b/src/org/sosy_lab/java_smt/api/StringFormula.java new file mode 100644 index 0000000000..17054a822c --- /dev/null +++ b/src/org/sosy_lab/java_smt/api/StringFormula.java @@ -0,0 +1,15 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2021 Alejandro Serrano Mena +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.api; + +import com.google.errorprone.annotations.Immutable; + +/** A formula of the string sort. */ +@Immutable +public interface StringFormula extends Formula {} diff --git a/src/org/sosy_lab/java_smt/api/StringFormulaManager.java b/src/org/sosy_lab/java_smt/api/StringFormulaManager.java new file mode 100644 index 0000000000..174562ce7d --- /dev/null +++ b/src/org/sosy_lab/java_smt/api/StringFormulaManager.java @@ -0,0 +1,190 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2021 Alejandro Serrano Mena +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.api; + +import java.util.Arrays; +import java.util.List; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; + +/** + * Manager for dealing with string formulas. Functions come from + * http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml. + */ +public interface StringFormulaManager { + + /** + * Returns a {@link StringFormula} representing the given constant. + * + * @param value the string value the returned Formula should represent + * @return a Formula representing the given value + */ + StringFormula makeString(String value); + + /** + * Creates a variable of type String with exactly the given name. + * + *

This variable (symbol) represents a "String" for which the SMT solver needs to find a model. + * + *

Please make sure that the given name is valid in SMT-LIB2. Take a look at {@link + * FormulaManager#isValidName} for further information. + * + *

This method does not quote or unquote the given name, but uses the plain name "AS IS". + * {@link Formula#toString} can return a different String than the given one. + */ + StringFormula makeVariable(String pVar); + + // TODO: There is currently no way to use variables of type "Regex", i.e., that represent full + // regular expression for which the SMT solver need to find a model. + // The reason for this is that the current SMT solvers do not support this feature. + // However, we can build a RegexFormula from basic parts like Strings (including + // variables of type String) and operations like range, union, or complement. + + BooleanFormula equal(StringFormula str1, StringFormula str2); + + BooleanFormula greaterThan(StringFormula str1, StringFormula str2); + + BooleanFormula greaterOrEquals(StringFormula str1, StringFormula str2); + + BooleanFormula lessThan(StringFormula str1, StringFormula str2); + + BooleanFormula lessOrEquals(StringFormula str1, StringFormula str2); + + /** Check whether the given prefix is a real prefix of str. */ + BooleanFormula prefix(StringFormula prefix, StringFormula str); + + /** Check whether the given suffix is a real suffix of str. */ + BooleanFormula suffix(StringFormula suffix, StringFormula str); + + BooleanFormula contains(StringFormula str, StringFormula part); + + /** + * Get the first index for a substring in a String, or -1 if the substring is not found. + * startIndex (inlcuded) denotes the start of the search for the index. + */ + IntegerFormula indexOf(StringFormula str, StringFormula part, IntegerFormula startIndex); + + /** + * Get a substring of length 1 from the given String. + * + *

The result is underspecified, if the index is out of bounds for the given String. + */ + StringFormula charAt(StringFormula str, IntegerFormula index); + + /** + * Get a substring from the given String. + * + *

The result is underspecified, if the start index is out of bounds for the given String or if + * the requested length is negative. The length of the result is the minimum of the requested + * length and the remaining length of the given String. + */ + StringFormula substring(StringFormula str, IntegerFormula index, IntegerFormula length); + + /** Replace the first appearances of target in fullStr with the replacement. */ + StringFormula replace(StringFormula fullStr, StringFormula target, StringFormula replacement); + + /** Replace all appearances of target in fullStr with the replacement. */ + StringFormula replaceAll(StringFormula fullStr, StringFormula target, StringFormula replacement); + + IntegerFormula length(StringFormula str); + + default StringFormula concat(StringFormula... parts) { + return concat(Arrays.asList(parts)); + } + + StringFormula concat(List parts); + + /** + * @param str formula representing the string to match + * @param regex formula representing the regular expression + * @return a formula representing the acceptance of the string by the regular expression + */ + BooleanFormula in(StringFormula str, RegexFormula regex); + + /** + * Returns a {@link RegexFormula} representing the given constant. + * + *

This method does not parse an existing regex from String, but uses the String directly as a + * constant. + * + * @param value the regular expression the returned Formula should represent + */ + RegexFormula makeRegex(String value); + + // basic regex operations + + /** @return formula denoting the empty set of strings */ + RegexFormula none(); + + /** @return formula denoting the set of all strings, also known as Regex ".*". */ + RegexFormula all(); + + /** @return formula denoting the range regular expression over two sequences of length 1. */ + RegexFormula range(StringFormula start, StringFormula end); + + /** + * @return formula denoting the range regular expression over two chars. + * @see #range(StringFormula, StringFormula) + */ + default RegexFormula range(char start, char end) { + return range(makeString(String.valueOf(start)), makeString(String.valueOf(end))); + } + + /** @return formula denoting the concatenation */ + default RegexFormula concat(RegexFormula... parts) { + return concatRegex(Arrays.asList(parts)); + } + + /** @return formula denoting the concatenation */ + // TODO the naming of this function collides with #concat(List). + // Maybe we should split String and Regex manager. + RegexFormula concatRegex(List parts); + + /** @return formula denoting the union */ + RegexFormula union(RegexFormula regex1, RegexFormula regex2); + + /** @return formula denoting the intersection */ + RegexFormula intersection(RegexFormula regex1, RegexFormula regex2); + + /** @return formula denoting the Kleene closure */ + RegexFormula complement(RegexFormula regex); + + /** @return formula denoting the Kleene closure (0 or more), also known as STAR operand. */ + RegexFormula closure(RegexFormula regex); + + // derived regex operations + + /** @return formula denoting the difference */ + RegexFormula difference(RegexFormula regex1, RegexFormula regex2); + + /** @return formula denoting the Kleene cross (1 or more), also known as PLUS operand. */ + RegexFormula cross(RegexFormula regex); + + /** @return formula denoting the optionality, also known as QUESTIONMARK operand. */ + RegexFormula optional(RegexFormula regex); + + /** @return formula denoting the concatenation n times */ + RegexFormula times(RegexFormula regex, int repetitions); + + /** + * Interpret a String formula as an Integer formula. + * + *

The number is interpreted in base 10 and has no leading zeros. The method works as expected + * for positive numbers, including zero. It returns the constant value of -1 for + * negative numbers or invalid number representations, for example if any char is no digit. + */ + IntegerFormula toIntegerFormula(StringFormula str); + + /** + * Interpret an Integer formula as a String formula. + * + *

The number is in base 10. The method works as expected for positive numbers, including zero. + * It returns the empty string "" for negative numbers. + */ + StringFormula toStringFormula(IntegerFormula number); +} diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractBaseFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractBaseFormulaManager.java index 044253e028..ad8a650b5a 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractBaseFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractBaseFormulaManager.java @@ -46,6 +46,8 @@ protected final TType toSolverType(FormulaType formulaType) { t = getFormulaCreator().getIntegerType(); } else if (formulaType.isRationalType()) { t = getFormulaCreator().getRationalType(); + } else if (formulaType.isStringType()) { + t = getFormulaCreator().getStringType(); } else if (formulaType.isBitvectorType()) { FormulaType.BitvectorType bitPreciseType = (FormulaType.BitvectorType) formulaType; t = getFormulaCreator().getBitvectorType(bitPreciseType.getSize()); diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormula.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormula.java index 8f70b30f34..95b992c6d9 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormula.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormula.java @@ -21,6 +21,8 @@ import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; +import org.sosy_lab.java_smt.api.RegexFormula; +import org.sosy_lab.java_smt.api.StringFormula; /** * A Formula represented as a TFormulaInfo object. @@ -132,4 +134,20 @@ static final class RationalFormulaImpl extends AbstractFormula extends AbstractFormula + implements StringFormula { + StringFormulaImpl(TFormulaInfo pT) { + super(pT); + } + } + + /** Simple RegexFormula implementation. */ + static final class RegexFormulaImpl extends AbstractFormula + implements RegexFormula { + RegexFormulaImpl(TFormulaInfo pT) { + super(pT); + } + } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java index a7b984b74f..0e0c03fb9e 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java @@ -36,6 +36,7 @@ import org.sosy_lab.java_smt.api.IntegerFormulaManager; import org.sosy_lab.java_smt.api.RationalFormulaManager; import org.sosy_lab.java_smt.api.SLFormulaManager; +import org.sosy_lab.java_smt.api.StringFormulaManager; import org.sosy_lab.java_smt.api.Tactic; import org.sosy_lab.java_smt.api.visitors.FormulaTransformationVisitor; import org.sosy_lab.java_smt.api.visitors.FormulaVisitor; @@ -117,6 +118,9 @@ public abstract class AbstractFormulaManager slManager; + private final @Nullable AbstractStringFormulaManager + strManager; + private final FormulaCreator formulaCreator; /** Builds a solver from the given theory implementations. */ @@ -135,7 +139,8 @@ protected AbstractFormulaManager( @Nullable AbstractQuantifiedFormulaManager quantifiedManager, @Nullable AbstractArrayFormulaManager arrayManager, - @Nullable AbstractSLFormulaManager slManager) { + @Nullable AbstractSLFormulaManager slManager, + @Nullable AbstractStringFormulaManager strManager) { this.arrayManager = arrayManager; this.quantifiedManager = quantifiedManager; @@ -146,6 +151,7 @@ protected AbstractFormulaManager( this.bitvectorManager = bitvectorManager; this.floatingPointManager = floatingPointManager; this.slManager = slManager; + this.strManager = strManager; this.formulaCreator = pFormulaCreator; checkArgument( @@ -230,6 +236,14 @@ public ArrayFormulaManager getArrayFormulaManager() { return arrayManager; } + @Override + public StringFormulaManager getStringFormulaManager() { + if (strManager == null) { + throw new UnsupportedOperationException("Solver does not support string theory"); + } + return strManager; + } + public abstract Appender dumpFormula(TFormulaInfo t); @Override @@ -391,6 +405,9 @@ public T makeVariable(FormulaType formulaType, String nam } else if (formulaType.isRationalType()) { assert rationalManager != null; t = rationalManager.makeVariable(name); + } else if (formulaType.isStringType()) { + assert strManager != null; + t = strManager.makeVariable(name); } else if (formulaType.isBitvectorType()) { assert bitvectorManager != null; t = bitvectorManager.makeVariable((BitvectorType) formulaType, name); diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractModel.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractModel.java index 9cf0ee8e9f..1f9525c819 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractModel.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractModel.java @@ -21,6 +21,7 @@ import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; +import org.sosy_lab.java_smt.api.StringFormula; @SuppressWarnings("ClassTypeParameterName") public abstract class AbstractModel implements Model { @@ -56,6 +57,12 @@ public Boolean evaluate(BooleanFormula f) { return (Boolean) evaluateImpl(creator.extractInfo(f)); } + @Nullable + @Override + public String evaluate(StringFormula f) { + return (String) evaluateImpl(creator.extractInfo(f)); + } + @Nullable @Override public BigInteger evaluate(BitvectorFormula f) { diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java new file mode 100644 index 0000000000..12efe42c95 --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java @@ -0,0 +1,295 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2021 Alejandro SerranoMena +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.basicimpl; + +import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName; + +import com.google.common.collect.Iterables; +import com.google.common.collect.Lists; +import java.util.Collections; +import java.util.List; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.NumeralFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.RegexFormula; +import org.sosy_lab.java_smt.api.StringFormula; +import org.sosy_lab.java_smt.api.StringFormulaManager; + +@SuppressWarnings("ClassTypeParameterName") +public abstract class AbstractStringFormulaManager + extends AbstractBaseFormulaManager + implements StringFormulaManager { + + protected AbstractStringFormulaManager( + FormulaCreator pCreator) { + super(pCreator); + } + + private StringFormula wrapString(TFormulaInfo formulaInfo) { + return getFormulaCreator().encapsulateString(formulaInfo); + } + + private RegexFormula wrapRegex(TFormulaInfo formulaInfo) { + return getFormulaCreator().encapsulateRegex(formulaInfo); + } + + @Override + public StringFormula makeString(String value) { + return wrapString(makeStringImpl(value)); + } + + protected abstract TFormulaInfo makeStringImpl(String value); + + @Override + public StringFormula makeVariable(String pVar) { + checkVariableName(pVar); + return wrapString(makeVariableImpl(pVar)); + } + + protected abstract TFormulaInfo makeVariableImpl(String pVar); + + @Override + public BooleanFormula equal(StringFormula str1, StringFormula str2) { + return wrapBool(equal(extractInfo(str1), extractInfo(str2))); + } + + protected abstract TFormulaInfo equal(TFormulaInfo pParam1, TFormulaInfo pParam2); + + @Override + public BooleanFormula greaterThan(StringFormula str1, StringFormula str2) { + return wrapBool(greaterThan(extractInfo(str1), extractInfo(str2))); + } + + protected abstract TFormulaInfo greaterThan(TFormulaInfo pParam1, TFormulaInfo pParam2); + + @Override + public BooleanFormula greaterOrEquals(StringFormula str1, StringFormula str2) { + return wrapBool(greaterOrEquals(extractInfo(str1), extractInfo(str2))); + } + + protected abstract TFormulaInfo greaterOrEquals(TFormulaInfo pParam1, TFormulaInfo pParam2); + + @Override + public BooleanFormula lessThan(StringFormula str1, StringFormula str2) { + return wrapBool(lessThan(extractInfo(str1), extractInfo(str2))); + } + + protected abstract TFormulaInfo lessThan(TFormulaInfo pParam1, TFormulaInfo pParam2); + + @Override + public BooleanFormula lessOrEquals(StringFormula str1, StringFormula str2) { + return wrapBool(lessOrEquals(extractInfo(str1), extractInfo(str2))); + } + + protected abstract TFormulaInfo lessOrEquals(TFormulaInfo pParam1, TFormulaInfo pParam2); + + @Override + public NumeralFormula.IntegerFormula length(StringFormula str) { + return getFormulaCreator().encapsulate(FormulaType.IntegerType, length(extractInfo(str))); + } + + protected abstract TFormulaInfo length(TFormulaInfo pParam); + + @Override + public StringFormula concat(List parts) { + switch (parts.size()) { + case 0: + return makeString(""); // empty sequence + case 1: + return Iterables.getOnlyElement(parts); + default: + return wrapString(concatImpl(Lists.transform(parts, this::extractInfo))); + } + } + + protected abstract TFormulaInfo concatImpl(List parts); + + @Override + public BooleanFormula prefix(StringFormula prefix, StringFormula str) { + return wrapBool(prefix(extractInfo(prefix), extractInfo(str))); + } + + protected abstract TFormulaInfo prefix(TFormulaInfo prefix, TFormulaInfo str); + + @Override + public BooleanFormula suffix(StringFormula suffix, StringFormula str) { + return wrapBool(suffix(extractInfo(suffix), extractInfo(str))); + } + + protected abstract TFormulaInfo suffix(TFormulaInfo suffix, TFormulaInfo str); + + @Override + public BooleanFormula in(StringFormula str, RegexFormula regex) { + return wrapBool(in(extractInfo(str), extractInfo(regex))); + } + + protected abstract TFormulaInfo in(TFormulaInfo str, TFormulaInfo regex); + + @Override + public BooleanFormula contains(StringFormula str, StringFormula part) { + return wrapBool(contains(extractInfo(str), extractInfo(part))); + } + + protected abstract TFormulaInfo contains(TFormulaInfo str, TFormulaInfo part); + + @Override + public IntegerFormula indexOf(StringFormula str, StringFormula part, IntegerFormula startIndex) { + return getFormulaCreator() + .encapsulate( + FormulaType.IntegerType, + indexOf(extractInfo(str), extractInfo(part), extractInfo(startIndex))); + } + + protected abstract TFormulaInfo indexOf( + TFormulaInfo str, TFormulaInfo part, TFormulaInfo startIndex); + + @Override + public StringFormula charAt(StringFormula str, IntegerFormula index) { + return wrapString(charAt(extractInfo(str), extractInfo(index))); + } + + protected abstract TFormulaInfo charAt(TFormulaInfo str, TFormulaInfo index); + + @Override + public StringFormula substring(StringFormula str, IntegerFormula index, IntegerFormula length) { + return wrapString(substring(extractInfo(str), extractInfo(index), extractInfo(length))); + } + + protected abstract TFormulaInfo substring( + TFormulaInfo str, TFormulaInfo index, TFormulaInfo length); + + @Override + public StringFormula replace( + StringFormula fullStr, StringFormula target, StringFormula replacement) { + return wrapString(replace(extractInfo(fullStr), extractInfo(target), extractInfo(replacement))); + } + + protected abstract TFormulaInfo replace( + TFormulaInfo fullStr, TFormulaInfo target, TFormulaInfo replacement); + + @Override + public StringFormula replaceAll( + StringFormula fullStr, StringFormula target, StringFormula replacement) { + return wrapString( + replaceAll(extractInfo(fullStr), extractInfo(target), extractInfo(replacement))); + } + + protected abstract TFormulaInfo replaceAll( + TFormulaInfo fullStr, TFormulaInfo target, TFormulaInfo replacement); + + @Override + public RegexFormula makeRegex(String value) { + return wrapRegex(makeRegexImpl(value)); + } + + protected abstract TFormulaInfo makeRegexImpl(String value); + + @Override + public RegexFormula none() { + return wrapRegex(noneImpl()); + } + + protected abstract TFormulaInfo noneImpl(); + + @Override + public RegexFormula all() { + return wrapRegex(allImpl()); + } + + protected abstract TFormulaInfo allImpl(); + + @Override + public RegexFormula range(StringFormula start, StringFormula end) { + return wrapRegex(range(extractInfo(start), extractInfo(end))); + } + + protected abstract TFormulaInfo range(TFormulaInfo start, TFormulaInfo end); + + @Override + public RegexFormula concatRegex(List parts) { + switch (parts.size()) { + case 0: + return none(); // empty sequence + case 1: + return Iterables.getOnlyElement(parts); + default: + return wrapRegex(concatRegexImpl(Lists.transform(parts, this::extractInfo))); + } + } + + protected abstract TFormulaInfo concatRegexImpl(List parts); + + @Override + public RegexFormula union(RegexFormula regex1, RegexFormula regex2) { + return wrapRegex(union(extractInfo(regex1), extractInfo(regex2))); + } + + protected abstract TFormulaInfo union(TFormulaInfo pParam1, TFormulaInfo pParam2); + + @Override + public RegexFormula intersection(RegexFormula regex1, RegexFormula regex2) { + return wrapRegex(union(extractInfo(regex1), extractInfo(regex2))); + } + + protected abstract TFormulaInfo intersection(TFormulaInfo pParam1, TFormulaInfo pParam2); + + @Override + public RegexFormula closure(RegexFormula regex) { + return wrapRegex(closure(extractInfo(regex))); + } + + protected abstract TFormulaInfo closure(TFormulaInfo pParam); + + @Override + public RegexFormula complement(RegexFormula regex) { + return wrapRegex(complement(extractInfo(regex))); + } + + protected abstract TFormulaInfo complement(TFormulaInfo pParam); + + @Override + public RegexFormula difference(RegexFormula regex1, RegexFormula regex2) { + return wrapRegex(difference(extractInfo(regex1), extractInfo(regex2))); + } + + protected TFormulaInfo difference(TFormulaInfo pParam1, TFormulaInfo pParam2) { + return union(pParam1, complement(pParam2)); + } + + @Override + public RegexFormula cross(RegexFormula regex) { + return concat(regex, closure(regex)); + } + + @Override + public RegexFormula optional(RegexFormula regex) { + return union(regex, makeRegex("")); + } + + @Override + public RegexFormula times(RegexFormula regex, int repetitions) { + return concatRegex(Collections.nCopies(repetitions, regex)); + } + + @Override + public IntegerFormula toIntegerFormula(StringFormula str) { + return getFormulaCreator() + .encapsulate(FormulaType.IntegerType, toIntegerFormula(extractInfo(str))); + } + + protected abstract TFormulaInfo toIntegerFormula(TFormulaInfo pParam); + + @Override + public StringFormula toStringFormula(IntegerFormula number) { + return wrapString(toStringFormula(extractInfo(number))); + } + + protected abstract TFormulaInfo toStringFormula(TFormulaInfo pParam); +} diff --git a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java index b9bdfc121b..4f40706866 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java @@ -40,6 +40,8 @@ import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier; +import org.sosy_lab.java_smt.api.RegexFormula; +import org.sosy_lab.java_smt.api.StringFormula; import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor; import org.sosy_lab.java_smt.api.visitors.FormulaVisitor; import org.sosy_lab.java_smt.api.visitors.TraversalProcess; @@ -50,6 +52,8 @@ import org.sosy_lab.java_smt.basicimpl.AbstractFormula.FloatingPointRoundingModeFormulaImpl; import org.sosy_lab.java_smt.basicimpl.AbstractFormula.IntegerFormulaImpl; import org.sosy_lab.java_smt.basicimpl.AbstractFormula.RationalFormulaImpl; +import org.sosy_lab.java_smt.basicimpl.AbstractFormula.RegexFormulaImpl; +import org.sosy_lab.java_smt.basicimpl.AbstractFormula.StringFormulaImpl; /** * This is a helper class with several methods that are commonly used throughout the basicimpl @@ -67,14 +71,23 @@ public abstract class FormulaCreator { private final TType boolType; private final @Nullable TType integerType; private final @Nullable TType rationalType; + private final @Nullable TType stringType; + private final @Nullable TType regexType; protected final TEnv environment; protected FormulaCreator( - TEnv env, TType boolType, @Nullable TType pIntegerType, @Nullable TType pRationalType) { + TEnv env, + TType boolType, + @Nullable TType pIntegerType, + @Nullable TType pRationalType, + @Nullable TType stringType, + @Nullable TType regexType) { this.environment = env; this.boolType = boolType; this.integerType = pIntegerType; this.rationalType = pRationalType; + this.stringType = stringType; + this.regexType = regexType; } public final TEnv getEnv() { @@ -105,6 +118,20 @@ public final TType getRationalType() { public abstract TType getArrayType(TType indexType, TType elementType); + public final TType getStringType() { + if (stringType == null) { + throw new UnsupportedOperationException("String theory is not supported by this solver."); + } + return stringType; + } + + public final TType getRegexType() { + if (regexType == null) { + throw new UnsupportedOperationException("String theory is not supported by this solver."); + } + return regexType; + } + public abstract TFormulaInfo makeVariable(TType type, String varName); public BooleanFormula encapsulateBoolean(TFormulaInfo pTerm) { @@ -133,6 +160,16 @@ assert getFormulaType(pTerm).equals(FormulaType.getArrayType(pIndexType, pElemen return new ArrayFormulaImpl<>(pTerm, pIndexType, pElementType); } + protected StringFormula encapsulateString(TFormulaInfo pTerm) { + assert getFormulaType(pTerm).isStringType(); + return new StringFormulaImpl<>(pTerm); + } + + protected RegexFormula encapsulateRegex(TFormulaInfo pTerm) { + assert getFormulaType(pTerm).isRegexType(); + return new RegexFormulaImpl<>(pTerm); + } + public Formula encapsulateWithTypeOf(TFormulaInfo pTerm) { return encapsulate(getFormulaType(pTerm), pTerm); } @@ -149,6 +186,10 @@ public T encapsulate(FormulaType pType, TFormulaInfo pTer return (T) new IntegerFormulaImpl<>(pTerm); } else if (pType.isRationalType()) { return (T) new RationalFormulaImpl<>(pTerm); + } else if (pType.isStringType()) { + return (T) new StringFormulaImpl<>(pTerm); + } else if (pType.isRegexType()) { + return (T) new RegexFormulaImpl<>(pTerm); } else if (pType.isBitvectorType()) { return (T) new BitvectorFormulaImpl<>(pTerm); } else if (pType.isFloatingPointType()) { @@ -195,6 +236,10 @@ protected FormulaType getFormulaType(T formula) { t = FormulaType.IntegerType; } else if (formula instanceof RationalFormula) { t = FormulaType.RationalType; + } else if (formula instanceof StringFormula) { + t = FormulaType.StringType; + } else if (formula instanceof RegexFormula) { + t = FormulaType.RegexType; } else if (formula instanceof FloatingPointRoundingModeFormula) { t = FormulaType.FloatingPointRoundingModeType; } else if (formula instanceof ArrayFormula) { diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/SolverStatistics.java b/src/org/sosy_lab/java_smt/delegate/statistics/SolverStatistics.java index 2fd8a84707..c774334f58 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/SolverStatistics.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/SolverStatistics.java @@ -36,6 +36,7 @@ public class SolverStatistics { final AtomicInteger bvOperations = new AtomicInteger(); final AtomicInteger fpOperations = new AtomicInteger(); final AtomicInteger typeOperations = new AtomicInteger(); + final AtomicInteger stringOperations = new AtomicInteger(); // model operations final AtomicInteger modelEvaluations = new AtomicInteger(); @@ -140,6 +141,10 @@ public int getNumberOfFPOperations() { return fpOperations.get(); } + public int getNumberOfStringOperations() { + return stringOperations.get(); + } + public int getNumberOfModelEvaluationQueries() { return modelEvaluations.get(); } diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFormulaManager.java index 238f99ded3..0d3f9a634e 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFormulaManager.java @@ -28,6 +28,7 @@ import org.sosy_lab.java_smt.api.QuantifiedFormulaManager; import org.sosy_lab.java_smt.api.RationalFormulaManager; import org.sosy_lab.java_smt.api.SLFormulaManager; +import org.sosy_lab.java_smt.api.StringFormulaManager; import org.sosy_lab.java_smt.api.Tactic; import org.sosy_lab.java_smt.api.UFManager; import org.sosy_lab.java_smt.api.visitors.FormulaTransformationVisitor; @@ -90,6 +91,11 @@ public QuantifiedFormulaManager getQuantifiedFormulaManager() { return new StatisticsQuantifiedFormulaManager(delegate.getQuantifiedFormulaManager(), stats); } + @Override + public StringFormulaManager getStringFormulaManager() { + return new StatisticsStringFormulaManager(delegate.getStringFormulaManager(), stats); + } + @Override public T makeVariable(FormulaType pFormulaType, String pName) { return delegate.makeVariable(pFormulaType, pName); diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsModel.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsModel.java index 376179b958..4eaeb0342c 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsModel.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsModel.java @@ -20,6 +20,7 @@ import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; +import org.sosy_lab.java_smt.api.StringFormula; class StatisticsModel implements Model { @@ -67,6 +68,12 @@ class StatisticsModel implements Model { return delegate.evaluate(pF); } + @Override + public @Nullable String evaluate(StringFormula pF) { + stats.modelEvaluations.getAndIncrement(); + return delegate.evaluate(pF); + } + @Override public ImmutableList asList() { stats.modelListings.getAndIncrement(); diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsStringFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsStringFormulaManager.java new file mode 100644 index 0000000000..b47a38a72d --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsStringFormulaManager.java @@ -0,0 +1,230 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2021 Alejandro Serrano Mena +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.delegate.statistics; + +import static com.google.common.base.Preconditions.checkNotNull; + +import java.util.List; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.NumeralFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.RegexFormula; +import org.sosy_lab.java_smt.api.StringFormula; +import org.sosy_lab.java_smt.api.StringFormulaManager; + +class StatisticsStringFormulaManager implements StringFormulaManager { + + private final StringFormulaManager delegate; + private final SolverStatistics stats; + + StatisticsStringFormulaManager(StringFormulaManager pDelegate, SolverStatistics pStats) { + delegate = checkNotNull(pDelegate); + stats = checkNotNull(pStats); + } + + @Override + public StringFormula makeString(String value) { + stats.stringOperations.getAndIncrement(); + return delegate.makeString(value); + } + + @Override + public StringFormula makeVariable(String pVar) { + stats.stringOperations.getAndIncrement(); + return delegate.makeVariable(pVar); + } + + @Override + public BooleanFormula equal(StringFormula str1, StringFormula str2) { + stats.stringOperations.getAndIncrement(); + return delegate.equal(str1, str2); + } + + @Override + public BooleanFormula greaterThan(StringFormula str1, StringFormula str2) { + stats.stringOperations.getAndIncrement(); + return delegate.greaterThan(str1, str2); + } + + @Override + public BooleanFormula greaterOrEquals(StringFormula str1, StringFormula str2) { + stats.stringOperations.getAndIncrement(); + return delegate.greaterOrEquals(str1, str2); + } + + @Override + public BooleanFormula lessThan(StringFormula str1, StringFormula str2) { + stats.stringOperations.getAndIncrement(); + return delegate.lessThan(str1, str2); + } + + @Override + public BooleanFormula lessOrEquals(StringFormula str1, StringFormula str2) { + stats.stringOperations.getAndIncrement(); + return delegate.lessOrEquals(str1, str2); + } + + @Override + public NumeralFormula.IntegerFormula length(StringFormula str) { + stats.stringOperations.getAndIncrement(); + return delegate.length(str); + } + + @Override + public StringFormula concat(List parts) { + stats.stringOperations.getAndIncrement(); + return delegate.concat(parts); + } + + @Override + public BooleanFormula prefix(StringFormula str1, StringFormula str2) { + stats.stringOperations.getAndIncrement(); + return delegate.prefix(str1, str2); + } + + @Override + public BooleanFormula suffix(StringFormula str1, StringFormula str2) { + stats.stringOperations.getAndIncrement(); + return delegate.suffix(str1, str2); + } + + @Override + public BooleanFormula contains(StringFormula str, StringFormula part) { + stats.stringOperations.getAndIncrement(); + return delegate.contains(str, part); + } + + @Override + public IntegerFormula indexOf(StringFormula str, StringFormula part, IntegerFormula startIndex) { + stats.stringOperations.getAndIncrement(); + return delegate.indexOf(str, part, startIndex); + } + + @Override + public StringFormula charAt(StringFormula str, IntegerFormula index) { + stats.stringOperations.getAndIncrement(); + return delegate.charAt(str, index); + } + + @Override + public StringFormula substring(StringFormula str, IntegerFormula index, IntegerFormula length) { + stats.stringOperations.getAndIncrement(); + return delegate.substring(str, index, length); + } + + @Override + public StringFormula replace( + StringFormula fullStr, StringFormula target, StringFormula replacement) { + stats.stringOperations.getAndIncrement(); + return delegate.replace(fullStr, target, replacement); + } + + @Override + public StringFormula replaceAll( + StringFormula fullStr, StringFormula target, StringFormula replacement) { + stats.stringOperations.getAndIncrement(); + return delegate.replaceAll(fullStr, target, replacement); + } + + @Override + public BooleanFormula in(StringFormula str, RegexFormula regex) { + stats.stringOperations.getAndIncrement(); + return delegate.in(str, regex); + } + + @Override + public RegexFormula makeRegex(String value) { + stats.stringOperations.getAndIncrement(); + return delegate.makeRegex(value); + } + + @Override + public RegexFormula none() { + stats.stringOperations.getAndIncrement(); + return delegate.none(); + } + + @Override + public RegexFormula all() { + stats.stringOperations.getAndIncrement(); + return delegate.all(); + } + + @Override + public RegexFormula range(StringFormula start, StringFormula end) { + stats.stringOperations.getAndIncrement(); + return delegate.range(start, end); + } + + @Override + public RegexFormula concatRegex(List parts) { + stats.stringOperations.getAndIncrement(); + return delegate.concatRegex(parts); + } + + @Override + public RegexFormula union(RegexFormula regex1, RegexFormula regex2) { + stats.stringOperations.getAndIncrement(); + return delegate.union(regex1, regex2); + } + + @Override + public RegexFormula intersection(RegexFormula regex1, RegexFormula regex2) { + stats.stringOperations.getAndIncrement(); + return delegate.intersection(regex1, regex2); + } + + @Override + public RegexFormula closure(RegexFormula regex) { + stats.stringOperations.getAndIncrement(); + return delegate.closure(regex); + } + + @Override + public RegexFormula complement(RegexFormula regex) { + stats.stringOperations.getAndIncrement(); + return delegate.complement(regex); + } + + @Override + public RegexFormula difference(RegexFormula regex1, RegexFormula regex2) { + stats.stringOperations.getAndIncrement(); + return delegate.difference(regex1, regex2); + } + + @Override + public RegexFormula cross(RegexFormula regex) { + stats.stringOperations.getAndIncrement(); + return delegate.cross(regex); + } + + @Override + public RegexFormula optional(RegexFormula regex) { + stats.stringOperations.getAndIncrement(); + return delegate.optional(regex); + } + + @Override + public RegexFormula times(RegexFormula regex, int repetitions) { + stats.stringOperations.getAndIncrement(); + return delegate.times(regex, repetitions); + } + + @Override + public IntegerFormula toIntegerFormula(StringFormula str) { + stats.stringOperations.getAndIncrement(); + return delegate.toIntegerFormula(str); + } + + @Override + public StringFormula toStringFormula(IntegerFormula number) { + stats.stringOperations.getAndIncrement(); + return delegate.toStringFormula(number); + } +} diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFormulaManager.java index b5f68aeb3e..2aa83f35fe 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFormulaManager.java @@ -29,6 +29,7 @@ import org.sosy_lab.java_smt.api.RationalFormulaManager; import org.sosy_lab.java_smt.api.SLFormulaManager; import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.StringFormulaManager; import org.sosy_lab.java_smt.api.Tactic; import org.sosy_lab.java_smt.api.UFManager; import org.sosy_lab.java_smt.api.visitors.FormulaTransformationVisitor; @@ -109,6 +110,13 @@ public QuantifiedFormulaManager getQuantifiedFormulaManager() { } } + @Override + public StringFormulaManager getStringFormulaManager() { + synchronized (sync) { + return new SynchronizedStringFormulaManager(delegate.getStringFormulaManager(), sync); + } + } + @Override public T makeVariable(FormulaType pFormulaType, String pName) { synchronized (sync) { diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModel.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModel.java index fe29633b2f..b353ba7a45 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModel.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModel.java @@ -21,6 +21,7 @@ import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.StringFormula; class SynchronizedModel implements Model { @@ -74,6 +75,13 @@ class SynchronizedModel implements Model { } } + @Override + public @Nullable String evaluate(StringFormula pF) { + synchronized (sync) { + return delegate.evaluate(pF); + } + } + @Override public ImmutableList asList() { synchronized (sync) { diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModelWithContext.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModelWithContext.java index 3fd941a005..546450b94b 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModelWithContext.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModelWithContext.java @@ -22,6 +22,7 @@ import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.StringFormula; class SynchronizedModelWithContext implements Model { @@ -75,6 +76,11 @@ class SynchronizedModelWithContext implements Model { throw new UnsupportedOperationException(UNSUPPORTED_OPERATION); } + @Override + public @Nullable String evaluate(StringFormula pF) { + throw new UnsupportedOperationException(UNSUPPORTED_OPERATION); + } + @Override public ImmutableList asList() { throw new UnsupportedOperationException(UNSUPPORTED_OPERATION); diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedStringFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedStringFormulaManager.java new file mode 100644 index 0000000000..5c3a0b807a --- /dev/null +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedStringFormulaManager.java @@ -0,0 +1,264 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2021 Alejandro Serrano Mena +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.delegate.synchronize; + +import static com.google.common.base.Preconditions.checkNotNull; + +import java.util.List; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.NumeralFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.RegexFormula; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.StringFormula; +import org.sosy_lab.java_smt.api.StringFormulaManager; + +class SynchronizedStringFormulaManager implements StringFormulaManager { + + private final StringFormulaManager delegate; + private final SolverContext sync; + + SynchronizedStringFormulaManager(StringFormulaManager pDelegate, SolverContext pSync) { + delegate = checkNotNull(pDelegate); + sync = checkNotNull(pSync); + } + + @Override + public StringFormula makeString(String value) { + synchronized (sync) { + return delegate.makeString(value); + } + } + + @Override + public StringFormula makeVariable(String pVar) { + synchronized (sync) { + return delegate.makeVariable(pVar); + } + } + + @Override + public BooleanFormula equal(StringFormula str1, StringFormula str2) { + synchronized (sync) { + return delegate.equal(str1, str2); + } + } + + @Override + public BooleanFormula greaterThan(StringFormula str1, StringFormula str2) { + synchronized (sync) { + return delegate.greaterThan(str1, str2); + } + } + + @Override + public BooleanFormula greaterOrEquals(StringFormula str1, StringFormula str2) { + synchronized (sync) { + return delegate.greaterOrEquals(str1, str2); + } + } + + @Override + public BooleanFormula lessThan(StringFormula str1, StringFormula str2) { + synchronized (sync) { + return delegate.lessThan(str1, str2); + } + } + + @Override + public BooleanFormula lessOrEquals(StringFormula str1, StringFormula str2) { + synchronized (sync) { + return delegate.lessOrEquals(str1, str2); + } + } + + @Override + public NumeralFormula.IntegerFormula length(StringFormula str) { + synchronized (sync) { + return delegate.length(str); + } + } + + @Override + public StringFormula concat(List parts) { + synchronized (sync) { + return delegate.concat(parts); + } + } + + @Override + public BooleanFormula prefix(StringFormula str1, StringFormula str2) { + synchronized (sync) { + return delegate.prefix(str1, str2); + } + } + + @Override + public BooleanFormula suffix(StringFormula str1, StringFormula str2) { + synchronized (sync) { + return delegate.suffix(str1, str2); + } + } + + @Override + public BooleanFormula contains(StringFormula str, StringFormula part) { + synchronized (sync) { + return delegate.contains(str, part); + } + } + + @Override + public IntegerFormula indexOf(StringFormula str, StringFormula part, IntegerFormula startIndex) { + synchronized (sync) { + return delegate.indexOf(str, part, startIndex); + } + } + + @Override + public StringFormula charAt(StringFormula str, IntegerFormula index) { + synchronized (sync) { + return delegate.charAt(str, index); + } + } + + @Override + public StringFormula substring(StringFormula str, IntegerFormula index, IntegerFormula length) { + synchronized (sync) { + return delegate.substring(str, index, length); + } + } + + @Override + public StringFormula replace( + StringFormula fullStr, StringFormula target, StringFormula replacement) { + synchronized (sync) { + return delegate.replace(fullStr, target, replacement); + } + } + + @Override + public StringFormula replaceAll( + StringFormula fullStr, StringFormula target, StringFormula replacement) { + synchronized (sync) { + return delegate.replaceAll(fullStr, target, replacement); + } + } + + @Override + public BooleanFormula in(StringFormula str, RegexFormula regex) { + synchronized (sync) { + return delegate.in(str, regex); + } + } + + @Override + public RegexFormula makeRegex(String value) { + synchronized (sync) { + return delegate.makeRegex(value); + } + } + + @Override + public RegexFormula none() { + synchronized (sync) { + return delegate.none(); + } + } + + @Override + public RegexFormula all() { + synchronized (sync) { + return delegate.all(); + } + } + + @Override + public RegexFormula range(StringFormula start, StringFormula end) { + synchronized (sync) { + return delegate.range(start, end); + } + } + + @Override + public RegexFormula concatRegex(List parts) { + synchronized (sync) { + return delegate.concatRegex(parts); + } + } + + @Override + public RegexFormula union(RegexFormula regex1, RegexFormula regex2) { + synchronized (sync) { + return delegate.union(regex1, regex2); + } + } + + @Override + public RegexFormula intersection(RegexFormula regex1, RegexFormula regex2) { + synchronized (sync) { + return delegate.intersection(regex1, regex2); + } + } + + @Override + public RegexFormula closure(RegexFormula regex) { + synchronized (sync) { + return delegate.closure(regex); + } + } + + @Override + public RegexFormula complement(RegexFormula regex) { + synchronized (sync) { + return delegate.complement(regex); + } + } + + @Override + public RegexFormula difference(RegexFormula regex1, RegexFormula regex2) { + synchronized (sync) { + return delegate.difference(regex1, regex2); + } + } + + @Override + public RegexFormula cross(RegexFormula regex) { + synchronized (sync) { + return delegate.cross(regex); + } + } + + @Override + public RegexFormula optional(RegexFormula regex) { + synchronized (sync) { + return delegate.optional(regex); + } + } + + @Override + public RegexFormula times(RegexFormula regex, int repetitions) { + synchronized (sync) { + return delegate.times(regex, repetitions); + } + } + + @Override + public IntegerFormula toIntegerFormula(StringFormula str) { + synchronized (sync) { + return delegate.toIntegerFormula(str); + } + } + + @Override + public StringFormula toStringFormula(IntegerFormula number) { + synchronized (sync) { + return delegate.toStringFormula(number); + } + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaCreator.java index b8fc47f558..96eb7d3732 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaCreator.java @@ -41,7 +41,7 @@ public class BoolectorFormulaCreator extends FormulaCreator nameFormulaCache = HashBasedTable.create(); BoolectorFormulaCreator(Long btor) { - super(btor, BtorJNI.boolector_bool_sort(btor), null, null); + super(btor, BtorJNI.boolector_bool_sort(btor), null, null, null, null); } @SuppressWarnings("unchecked") diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java index 9716563d9f..cad33eb7c0 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java @@ -34,6 +34,7 @@ final class BoolectorFormulaManager extends AbstractFormulaManager { @@ -71,7 +75,9 @@ protected CVC4FormulaCreator(ExprManager pExprManager) { pExprManager, pExprManager.booleanType(), pExprManager.integerType(), - pExprManager.realType()); + pExprManager.realType(), + pExprManager.stringType(), + pExprManager.regExpType()); exprManager = pExprManager; } @@ -189,8 +195,13 @@ private FormulaType getFormulaTypeFromTermType(Type t) { FormulaType indexType = getFormulaTypeFromTermType(arrayType.getIndexType()); FormulaType elementType = getFormulaTypeFromTermType(arrayType.getConstituentType()); return FormulaType.getArrayType(indexType, elementType); + } else if (t.isString()) { + return FormulaType.StringType; + } else if (t.isRegExp()) { + return FormulaType.RegexType; } else { - throw new AssertionError("Unhandled type " + t.getBaseType()); + throw new AssertionError( + String.format("Unhandled type '%s' with base type '%s'.", t, t.getBaseType())); } } @@ -218,6 +229,10 @@ && getFormulaType(pTerm).equals(FormulaType.IntegerType)) return (T) new CVC4FloatingPointFormula(pTerm); } else if (pType.isFloatingPointRoundingModeType()) { return (T) new CVC4FloatingPointRoundingModeFormula(pTerm); + } else if (pType.isStringType()) { + return (T) new CVC4StringFormula(pTerm); + } else if (pType.isRegexType()) { + return (T) new CVC4RegexFormula(pTerm); } throw new IllegalArgumentException("Cannot create formulas of type " + pType + " in CVC4"); } @@ -258,6 +273,20 @@ assert getFormulaType(pTerm).equals(FormulaType.getArrayType(pIndexType, pElemen return new CVC4ArrayFormula<>(pTerm, pIndexType, pElementType); } + @Override + protected StringFormula encapsulateString(Expr pTerm) { + assert getFormulaType(pTerm).isStringType() + : String.format( + "%s is no String, but %s (%s)", pTerm, pTerm.getType(), getFormulaType(pTerm)); + return new CVC4StringFormula(pTerm); + } + + @Override + protected RegexFormula encapsulateRegex(Expr pTerm) { + assert getFormulaType(pTerm).isRegexType(); + return new CVC4RegexFormula(pTerm); + } + private static String getName(Expr e) { Preconditions.checkState(!e.isNull()); if (!e.isConst() && !e.isVariable()) { @@ -294,6 +323,8 @@ public R visit(FormulaVisitor visitor, Formula formula, final Expr f) { } else if (type.isRoundingMode()) { // TODO is this correct? return visitor.visitConstant(formula, f.getConstRoundingMode()); + } else if (type.isString()) { + return visitor.visitConstant(formula, f.getConstString()); } else { throw new UnsupportedOperationException("Unhandled constant " + f + " with type " + type); } @@ -375,6 +406,7 @@ public R visit(FormulaVisitor visitor, Formula formula, final Expr f) { .put(Kind.LEQ, FunctionDeclarationKind.LTE) .put(Kind.GT, FunctionDeclarationKind.GT) .put(Kind.GEQ, FunctionDeclarationKind.GTE) + // Bitvector theory .put(Kind.BITVECTOR_PLUS, FunctionDeclarationKind.BV_ADD) .put(Kind.BITVECTOR_SUB, FunctionDeclarationKind.BV_SUB) .put(Kind.BITVECTOR_MULT, FunctionDeclarationKind.BV_MUL) @@ -400,6 +432,7 @@ public R visit(FormulaVisitor visitor, Formula formula, final Expr f) { .put(Kind.BITVECTOR_CONCAT, FunctionDeclarationKind.BV_CONCAT) .put(Kind.BITVECTOR_SIGN_EXTEND, FunctionDeclarationKind.BV_SIGN_EXTENSION) .put(Kind.BITVECTOR_ZERO_EXTEND, FunctionDeclarationKind.BV_ZERO_EXTENSION) + // Floating-point theory .put(Kind.TO_INTEGER, FunctionDeclarationKind.FLOOR) .put(Kind.FLOATINGPOINT_TO_SBV, FunctionDeclarationKind.FP_CASTTO_SBV) .put(Kind.FLOATINGPOINT_TO_UBV, FunctionDeclarationKind.FP_CASTTO_UBV) @@ -427,6 +460,32 @@ public R visit(FormulaVisitor visitor, Formula formula, final Expr f) { .put(Kind.FLOATINGPOINT_GEQ, FunctionDeclarationKind.FP_GE) .put(Kind.FLOATINGPOINT_RTI, FunctionDeclarationKind.FP_ROUND_TO_INTEGRAL) .put(Kind.FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, FunctionDeclarationKind.FP_AS_IEEEBV) + // String and Regex theory + .put(Kind.STRING_CONCAT, FunctionDeclarationKind.STR_CONCAT) + .put(Kind.STRING_PREFIX, FunctionDeclarationKind.STR_PREFIX) + .put(Kind.STRING_SUFFIX, FunctionDeclarationKind.STR_SUFFIX) + .put(Kind.STRING_STRCTN, FunctionDeclarationKind.STR_CONTAINS) + .put(Kind.STRING_SUBSTR, FunctionDeclarationKind.STR_SUBSTRING) + .put(Kind.STRING_STRREPL, FunctionDeclarationKind.STR_REPLACE) + .put(Kind.STRING_STRREPLALL, FunctionDeclarationKind.STR_REPLACE_ALL) + .put(Kind.STRING_CHARAT, FunctionDeclarationKind.STR_CHAR_AT) + .put(Kind.STRING_LENGTH, FunctionDeclarationKind.STR_LENGTH) + .put(Kind.STRING_STRIDOF, FunctionDeclarationKind.STR_INDEX_OF) + .put(Kind.STRING_TO_REGEXP, FunctionDeclarationKind.STR_TO_RE) + .put(Kind.STRING_IN_REGEXP, FunctionDeclarationKind.STR_IN_RE) + .put(Kind.STRING_STOI, FunctionDeclarationKind.STR_TO_INT) + .put(Kind.STRING_ITOS, FunctionDeclarationKind.INT_TO_STR) + .put(Kind.STRING_LT, FunctionDeclarationKind.STR_LT) + .put(Kind.STRING_LEQ, FunctionDeclarationKind.STR_LE) + .put(Kind.REGEXP_PLUS, FunctionDeclarationKind.RE_PLUS) + .put(Kind.REGEXP_STAR, FunctionDeclarationKind.RE_STAR) + .put(Kind.REGEXP_OPT, FunctionDeclarationKind.RE_OPTIONAL) + .put(Kind.REGEXP_CONCAT, FunctionDeclarationKind.RE_CONCAT) + .put(Kind.REGEXP_UNION, FunctionDeclarationKind.RE_UNION) + .put(Kind.REGEXP_RANGE, FunctionDeclarationKind.RE_RANGE) + .put(Kind.REGEXP_INTER, FunctionDeclarationKind.RE_INTERSECT) + .put(Kind.REGEXP_COMPLEMENT, FunctionDeclarationKind.RE_COMPLEMENT) + .put(Kind.REGEXP_DIFF, FunctionDeclarationKind.RE_DIFFERENCE) .build(); private FunctionDeclarationKind getDeclarationKind(Expr f) { @@ -487,22 +546,23 @@ public Object convertValue(Expr pF) { @Override public Object convertValue(Expr expForType, Expr value) { final Type type = expForType.getType(); + final Type valueType = value.getType(); if (value.getKind() == Kind.BOUND_VARIABLE) { // CVC4 does not allow model values for bound vars return value.toString(); - } else if (value.getType().isBoolean()) { + } else if (valueType.isBoolean()) { return value.getConstBoolean(); - } else if (value.getType().isInteger() && type.isInteger()) { + } else if (valueType.isInteger() && type.isInteger()) { return new BigInteger(value.getConstRational().toString()); - } else if (value.getType().isReal() && type.isReal()) { + } else if (valueType.isReal() && type.isReal()) { Rational rat = value.getConstRational(); return org.sosy_lab.common.rationals.Rational.of( new BigInteger(rat.getNumerator().toString()), new BigInteger(rat.getDenominator().toString())); - } else if (value.getType().isBitVector()) { + } else if (valueType.isBitVector()) { Integer bv = value.getConstBitVector().getValue(); if (bv.fitsSignedLong()) { return BigInteger.valueOf(bv.getUnsignedLong()); @@ -510,9 +570,12 @@ public Object convertValue(Expr expForType, Expr value) { return value.toString(); // default } - } else if (value.getType().isFloatingPoint()) { + } else if (valueType.isFloatingPoint()) { return parseFloatingPoint(value); + } else if (valueType.isString()) { + return value.getConstString().toString(); + } else { // String serialization for unknown terms. return value.toString(); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java index e5729141ae..619c4c2d49 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java @@ -40,9 +40,20 @@ class CVC4FormulaManager extends AbstractFormulaManager { + + private final ExprManager exprManager; + + CVC4StringFormulaManager(CVC4FormulaCreator pCreator) { + super(pCreator); + exprManager = pCreator.getEnv(); + } + + @Override + protected Expr makeStringImpl(String pValue) { + // The boolean enables escape characters! + return exprManager.mkConst(new CVC4String(pValue, true)); + } + + @Override + protected Expr makeVariableImpl(String varName) { + Type type = getFormulaCreator().getStringType(); + return getFormulaCreator().makeVariable(type, varName); + } + + @Override + protected Expr equal(Expr pParam1, Expr pParam2) { + return exprManager.mkExpr(Kind.EQUAL, pParam1, pParam2); + } + + @Override + protected Expr greaterThan(Expr pParam1, Expr pParam2) { + return exprManager.mkExpr(Kind.STRING_LT, pParam2, pParam1); + } + + @Override + protected Expr greaterOrEquals(Expr pParam1, Expr pParam2) { + return exprManager.mkExpr(Kind.STRING_LEQ, pParam2, pParam1); + } + + @Override + protected Expr lessThan(Expr pParam1, Expr pParam2) { + return exprManager.mkExpr(Kind.STRING_LT, pParam1, pParam2); + } + + @Override + protected Expr lessOrEquals(Expr pParam1, Expr pParam2) { + return exprManager.mkExpr(Kind.STRING_LEQ, pParam1, pParam2); + } + + @Override + protected Expr length(Expr pParam) { + return exprManager.mkExpr(Kind.STRING_LENGTH, pParam); + } + + @Override + protected Expr concatImpl(List parts) { + Preconditions.checkArgument(parts.size() > 1); + vectorExpr vector = new vectorExpr(); + parts.forEach(vector::add); + return exprManager.mkExpr(Kind.STRING_CONCAT, vector); + } + + @Override + protected Expr prefix(Expr prefix, Expr str) { + return exprManager.mkExpr(Kind.STRING_PREFIX, prefix, str); + } + + @Override + protected Expr suffix(Expr suffix, Expr str) { + return exprManager.mkExpr(Kind.STRING_SUFFIX, suffix, str); + } + + @Override + protected Expr in(Expr str, Expr regex) { + return exprManager.mkExpr(Kind.STRING_IN_REGEXP, str, regex); + } + + @Override + protected Expr contains(Expr str, Expr part) { + return exprManager.mkExpr(Kind.STRING_STRCTN, str, part); + } + + @Override + protected Expr indexOf(Expr str, Expr part, Expr startIndex) { + return exprManager.mkExpr(Kind.STRING_STRIDOF, str, part, startIndex); + } + + @Override + protected Expr charAt(Expr str, Expr index) { + return exprManager.mkExpr(Kind.STRING_CHARAT, str, index); + } + + @Override + protected Expr substring(Expr str, Expr index, Expr length) { + return exprManager.mkExpr(Kind.STRING_SUBSTR, str, index, length); + } + + @Override + protected Expr replace(Expr fullStr, Expr target, Expr replacement) { + return exprManager.mkExpr(Kind.STRING_STRREPL, fullStr, target, replacement); + } + + @Override + protected Expr replaceAll(Expr fullStr, Expr target, Expr replacement) { + return exprManager.mkExpr(Kind.STRING_STRREPLALL, fullStr, target, replacement); + } + + @Override + protected Expr makeRegexImpl(String value) { + Expr str = makeStringImpl(value); + return exprManager.mkExpr(Kind.STRING_TO_REGEXP, str); + } + + @Override + protected Expr noneImpl() { + return exprManager.mkExpr(Kind.REGEXP_EMPTY, new vectorExpr()); + } + + @Override + protected Expr allImpl() { + return exprManager.mkExpr(Kind.REGEXP_COMPLEMENT, noneImpl()); + } + + @Override + protected Expr range(Expr start, Expr end) { + return exprManager.mkExpr(Kind.REGEXP_RANGE, start, end); + } + + @Override + protected Expr concatRegexImpl(List parts) { + Preconditions.checkArgument(parts.size() > 1); + vectorExpr vector = new vectorExpr(); + parts.forEach(vector::add); + return exprManager.mkExpr(Kind.REGEXP_CONCAT, vector); + } + + @Override + protected Expr union(Expr pParam1, Expr pParam2) { + return exprManager.mkExpr(Kind.REGEXP_UNION, pParam1, pParam2); + } + + @Override + protected Expr intersection(Expr pParam1, Expr pParam2) { + return exprManager.mkExpr(Kind.REGEXP_INTER, pParam1, pParam2); + } + + @Override + protected Expr closure(Expr pParam) { + return exprManager.mkExpr(Kind.REGEXP_STAR, pParam); + } + + @Override + protected Expr complement(Expr pParam) { + return exprManager.mkExpr(Kind.REGEXP_COMPLEMENT, pParam); + } + + @Override + protected Expr difference(Expr pParam1, Expr pParam2) { + return exprManager.mkExpr(Kind.REGEXP_DIFF, pParam1, pParam2); + } + + @Override + protected Expr toIntegerFormula(Expr pParam) { + return exprManager.mkExpr(Kind.STRING_STOI, pParam); + } + + @Override + protected Expr toStringFormula(Expr pParam) { + return exprManager.mkExpr(Kind.STRING_ITOS, pParam); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java index 51c25ab6d2..9a131d38dc 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java @@ -96,6 +96,8 @@ private void setOptions(int randomSeed, Set pOptions) { // smtEngine.setOption("produce-unsat-cores", new SExpr(true)); smtEngine.setOption("output-language", new SExpr("smt2")); smtEngine.setOption("random-seed", new SExpr(randomSeed)); + // Set Strings option to enable all String features (such as lessOrEquals) + smtEngine.setOption("strings-exp", new SExpr(true)); } protected void setOptionForIncremental() { diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java index f45ab58f76..792da76881 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java @@ -144,7 +144,9 @@ class Mathsat5FormulaCreator extends FormulaCreator { msatEnv, msat_get_bool_type(msatEnv), msat_get_integer_type(msatEnv), - msat_get_rational_type(msatEnv)); + msat_get_rational_type(msatEnv), + null, + null); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaManager.java index ade4bd5c49..9511e50ea0 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaManager.java @@ -50,6 +50,7 @@ final class Mathsat5FormulaManager extends AbstractFormulaManager arraySortCache = HashBasedTable.create(); PrincessFormulaCreator(PrincessEnvironment pEnv) { - super(pEnv, PrincessEnvironment.BOOL_SORT, PrincessEnvironment.INTEGER_SORT, null); + super(pEnv, PrincessEnvironment.BOOL_SORT, PrincessEnvironment.INTEGER_SORT, null, null, null); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java index 8cae27356c..fd599418d0 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java @@ -43,6 +43,7 @@ final class PrincessFormulaManager null, pQuantifierManager, pArrayManager, + null, null); creator = pCreator; } diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java index 362e3478c4..1084ab9f66 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java @@ -44,7 +44,9 @@ class SmtInterpolFormulaCreator extends FormulaCreator { @@ -119,15 +123,18 @@ class Z3FormulaCreator extends FormulaCreator { private final Timer cleanupTimer = new Timer(); protected final ShutdownNotifier shutdownNotifier; + @SuppressWarnings("ParameterNumber") Z3FormulaCreator( long pEnv, long pBoolType, long pIntegerType, long pRealType, + long pStringType, + long pRegexType, Configuration config, ShutdownNotifier pShutdownNotifier) throws InvalidConfigurationException { - super(pEnv, pBoolType, pIntegerType, pRealType); + super(pEnv, pBoolType, pIntegerType, pRealType, pStringType, pRegexType); shutdownNotifier = pShutdownNotifier; config.inject(this); } @@ -186,19 +193,24 @@ public FormulaType getFormulaTypeFromSort(Long pSort) { Native.fpaGetEbits(z3context, pSort), Native.fpaGetSbits(z3context, pSort) - 1); case Z3_ROUNDING_MODE_SORT: return FormulaType.FloatingPointRoundingModeType; + case Z3_RE_SORT: + return FormulaType.RegexType; case Z3_DATATYPE_SORT: case Z3_RELATION_SORT: case Z3_FINITE_DOMAIN_SORT: case Z3_SEQ_SORT: - case Z3_RE_SORT: case Z3_UNKNOWN_SORT: case Z3_UNINTERPRETED_SORT: - // TODO: support for remaining sorts. - throw new IllegalArgumentException( - "Unknown formula type " - + Native.sortToString(z3context, pSort) - + " with sort " - + sortKind); + if (Native.isStringSort(z3context, pSort)) { + return FormulaType.StringType; + } else { + // TODO: support for remaining sorts. + throw new IllegalArgumentException( + "Unknown formula type " + + Native.sortToString(z3context, pSort) + + " with sort " + + sortKind); + } default: throw new UnsupportedOperationException("Unexpected state."); } @@ -257,6 +269,10 @@ && getFormulaType(pTerm).equals(FormulaType.IntegerType)) return (T) storePhantomReference(new Z3IntegerFormula(getEnv(), pTerm), pTerm); } else if (pType.isRationalType()) { return (T) storePhantomReference(new Z3RationalFormula(getEnv(), pTerm), pTerm); + } else if (pType.isStringType()) { + return (T) storePhantomReference(new Z3StringFormula(getEnv(), pTerm), pTerm); + } else if (pType.isRegexType()) { + return (T) storePhantomReference(new Z3RegexFormula(getEnv(), pTerm), pTerm); } else if (pType.isBitvectorType()) { return (T) storePhantomReference(new Z3BitvectorFormula(getEnv(), pTerm), pTerm); } else if (pType.isFloatingPointType()) { @@ -296,6 +312,28 @@ protected FloatingPointFormula encapsulateFloatingPoint(Long pTerm) { return storePhantomReference(new Z3FloatingPointFormula(getEnv(), pTerm), pTerm); } + @Override + protected StringFormula encapsulateString(Long pTerm) { + assert getFormulaType(pTerm).isStringType() + : String.format( + "Term %s has unexpected type %s.", + Native.astToString(getEnv(), pTerm), + Native.sortToString(getEnv(), Native.getSort(getEnv(), pTerm))); + cleanupReferences(); + return storePhantomReference(new Z3StringFormula(getEnv(), pTerm), pTerm); + } + + @Override + protected RegexFormula encapsulateRegex(Long pTerm) { + assert getFormulaType(pTerm).isRegexType() + : String.format( + "Term %s has unexpected type %s.", + Native.astToString(getEnv(), pTerm), + Native.sortToString(getEnv(), Native.getSort(getEnv(), pTerm))); + cleanupReferences(); + return storePhantomReference(new Z3RegexFormula(getEnv(), pTerm), pTerm); + } + @Override public Long getArrayType(Long pIndexType, Long pElementType) { Long allocatedArraySort = allocatedArraySorts.get(pIndexType, pElementType); @@ -351,11 +389,10 @@ public R visit(FormulaVisitor visitor, final Formula formula, final Long return visitor.visitConstant(formula, convertValue(f)); case Z3_APP_AST: int arity = Native.getAppNumArgs(environment, f); + int declKind = Native.getDeclKind(environment, Native.getAppDecl(environment, f)); if (arity == 0) { - // constants - int declKind = Native.getDeclKind(environment, Native.getAppDecl(environment, f)); Object value = Z3_CONSTANTS.get(declKind); if (value != null) { return visitor.visitConstant(formula, value); @@ -630,6 +667,54 @@ private FunctionDeclarationKind getDeclarationKind(long f) { return FunctionDeclarationKind.FP_IS_SUBNORMAL; case Z3_OP_FPA_IS_NORMAL: return FunctionDeclarationKind.FP_IS_NORMAL; + + case Z3_OP_SEQ_CONCAT: + return FunctionDeclarationKind.STR_CONCAT; + case Z3_OP_SEQ_PREFIX: + return FunctionDeclarationKind.STR_PREFIX; + case Z3_OP_SEQ_SUFFIX: + return FunctionDeclarationKind.STR_SUFFIX; + case Z3_OP_SEQ_CONTAINS: + return FunctionDeclarationKind.STR_CONTAINS; + case Z3_OP_SEQ_EXTRACT: + return FunctionDeclarationKind.STR_SUBSTRING; + case Z3_OP_SEQ_REPLACE: + return FunctionDeclarationKind.STR_REPLACE; + case Z3_OP_SEQ_AT: + return FunctionDeclarationKind.STR_CHAR_AT; + case Z3_OP_SEQ_LENGTH: + return FunctionDeclarationKind.STR_LENGTH; + case Z3_OP_SEQ_INDEX: + return FunctionDeclarationKind.STR_INDEX_OF; + case Z3_OP_SEQ_TO_RE: + return FunctionDeclarationKind.STR_TO_RE; + case Z3_OP_SEQ_IN_RE: + return FunctionDeclarationKind.STR_IN_RE; + case Z3_OP_STR_TO_INT: + return FunctionDeclarationKind.STR_TO_INT; + case Z3_OP_INT_TO_STR: + return FunctionDeclarationKind.INT_TO_STR; + case Z3_OP_STRING_LT: + return FunctionDeclarationKind.STR_LT; + case Z3_OP_STRING_LE: + return FunctionDeclarationKind.STR_LE; + case Z3_OP_RE_PLUS: + return FunctionDeclarationKind.RE_PLUS; + case Z3_OP_RE_STAR: + return FunctionDeclarationKind.RE_STAR; + case Z3_OP_RE_OPTION: + return FunctionDeclarationKind.RE_OPTIONAL; + case Z3_OP_RE_CONCAT: + return FunctionDeclarationKind.RE_CONCAT; + case Z3_OP_RE_UNION: + return FunctionDeclarationKind.RE_UNION; + case Z3_OP_RE_RANGE: + return FunctionDeclarationKind.RE_RANGE; + case Z3_OP_RE_INTERSECT: + return FunctionDeclarationKind.RE_INTERSECT; + case Z3_OP_RE_COMPLEMENT: + return FunctionDeclarationKind.RE_COMPLEMENT; + default: return FunctionDeclarationKind.OTHER; } @@ -642,6 +727,7 @@ private FunctionDeclarationKind getDeclarationKind(long f) { public boolean isConstant(long value) { return Native.isNumeralAst(environment, value) || Native.isAlgebraicNumber(environment, value) + || Native.isString(environment, value) || isOP(environment, value, Z3_decl_kind.Z3_OP_TRUE.toInt()) || isOP(environment, value, Z3_decl_kind.Z3_OP_FALSE.toInt()); } @@ -673,6 +759,8 @@ public Object convertValue(Long value) { return new BigInteger(Native.getNumeralString(environment, value)); } else if (type.isRationalType()) { return Rational.ofString(Native.getNumeralString(environment, value)); + } else if (type.isStringType()) { + return Native.getString(environment, value); } else if (type.isBitvectorType()) { return new BigInteger(Native.getNumeralString(environment, value)); } else if (type.isFloatingPointType()) { diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaManager.java index bdc16a64aa..68dab1ea26 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaManager.java @@ -40,7 +40,8 @@ final class Z3FormulaManager extends AbstractFormulaManager { + + private final long z3context; + + Z3StringFormulaManager(Z3FormulaCreator creator) { + super(creator); + z3context = creator.getEnv(); + } + + @Override + protected Long makeStringImpl(String pValue) { + return Native.mkString(z3context, pValue); + } + + @Override + protected Long makeVariableImpl(String varName) { + long type = getFormulaCreator().getStringType(); + return getFormulaCreator().makeVariable(type, varName); + } + + @Override + protected Long equal(Long pParam1, Long pParam2) { + return Native.mkEq(z3context, pParam1, pParam2); + } + + @Override + protected Long greaterThan(Long pParam1, Long pParam2) { + return lessThan(pParam2, pParam1); + } + + @Override + protected Long greaterOrEquals(Long pParam1, Long pParam2) { + return lessOrEquals(pParam2, pParam1); + } + + @Override + protected Long lessThan(Long pParam1, Long pParam2) { + return Native.mkStrLt(z3context, pParam1, pParam2); + } + + @Override + protected Long lessOrEquals(Long pParam1, Long pParam2) { + return Native.mkStrLe(z3context, pParam1, pParam2); + } + + @Override + protected Long length(Long pParam) { + return Native.mkSeqLength(z3context, pParam); + } + + @Override + protected Long concatImpl(List parts) { + Preconditions.checkArgument(!parts.isEmpty()); + return Native.mkSeqConcat(z3context, parts.size(), Longs.toArray(parts)); + } + + @Override + protected Long prefix(Long prefix, Long str) { + return Native.mkSeqPrefix(z3context, prefix, str); + } + + @Override + protected Long suffix(Long suffix, Long str) { + return Native.mkSeqSuffix(z3context, suffix, str); + } + + @Override + protected Long in(Long str, Long regex) { + return Native.mkSeqInRe(z3context, str, regex); + } + + @Override + protected Long contains(Long str, Long part) { + return Native.mkSeqContains(z3context, str, part); + } + + @Override + protected Long indexOf(Long str, Long part, Long startIndex) { + return Native.mkSeqIndex(z3context, str, part, startIndex); + } + + @Override + protected Long charAt(Long str, Long index) { + return Native.mkSeqAt(z3context, str, index); + } + + @Override + protected Long substring(Long str, Long index, Long length) { + return Native.mkSeqExtract(z3context, str, index, length); + } + + @Override + protected Long replace(Long fullStr, Long target, Long replacement) { + return Native.mkSeqReplace(z3context, fullStr, target, replacement); + } + + @Override + protected Long replaceAll(Long fullStr, Long target, Long replacement) { + throw new UnsupportedOperationException(); + } + + @Override + protected Long makeRegexImpl(String value) { + Long str = makeStringImpl(value); + return Native.mkSeqToRe(z3context, str); + } + + @Override + protected Long noneImpl() { + return Native.mkReEmpty(z3context, formulaCreator.getRegexType()); + } + + @Override + protected Long allImpl() { + return Native.mkReFull(z3context, formulaCreator.getRegexType()); + } + + @Override + protected Long range(Long start, Long end) { + return Native.mkReRange(z3context, start, end); + } + + @Override + protected Long concatRegexImpl(List parts) { + if (parts.isEmpty()) { + return noneImpl(); + } + return Native.mkReConcat(z3context, parts.size(), Longs.toArray(parts)); + } + + @Override + protected Long union(Long pParam1, Long pParam2) { + return Native.mkReUnion(z3context, 2, new long[] {pParam1, pParam2}); + } + + @Override + protected Long intersection(Long pParam1, Long pParam2) { + return Native.mkReIntersect(z3context, 2, new long[] {pParam1, pParam2}); + } + + @Override + protected Long closure(Long pParam) { + return Native.mkReStar(z3context, pParam); + } + + @Override + protected Long complement(Long pParam) { + return Native.mkReComplement(z3context, pParam); + } + + @Override + protected Long toIntegerFormula(Long pParam) { + return Native.mkStrToInt(z3context, pParam); + } + + @Override + protected Long toStringFormula(Long pParam) { + return Native.mkIntToStr(z3context, pParam); + } +} diff --git a/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java index 34fcdc80a0..b9ce021fb7 100644 --- a/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java @@ -8,6 +8,12 @@ package org.sosy_lab.java_smt.test; +import static org.sosy_lab.java_smt.api.FormulaType.IntegerType; +import static org.sosy_lab.java_smt.api.FormulaType.RationalType; +import static org.sosy_lab.java_smt.api.FormulaType.StringType; +import static org.sosy_lab.java_smt.api.FormulaType.getBitvectorTypeWithSize; +import static org.sosy_lab.java_smt.api.FormulaType.getSinglePrecisionFloatingPointType; + import org.junit.Before; import org.junit.Test; import org.junit.runner.RunWith; @@ -16,11 +22,15 @@ import org.junit.runners.Parameterized.Parameters; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.ArrayFormula; +import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.FloatingPointFormula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.StringFormula; /** Tests Arrays for all solvers that support it. */ @RunWith(Parameterized.class) @@ -45,12 +55,12 @@ public void init() { } @Test - public void uniqueType() throws SolverException, InterruptedException { + public void testIntIndexIntValue() throws SolverException, InterruptedException { requireIntegers(); // (arr2 = store(arr1, 4, 2)) & !(select(arr2, 4) = 2) ArrayFormulaType type = - FormulaType.getArrayType(FormulaType.IntegerType, FormulaType.IntegerType); + FormulaType.getArrayType(IntegerType, IntegerType); IntegerFormula num2 = imgr.makeNumber(2); IntegerFormula num4 = imgr.makeNumber(4); ArrayFormula arr1 = amgr.makeArray("arr1", type); @@ -61,4 +71,132 @@ public void uniqueType() throws SolverException, InterruptedException { bmgr.not(imgr.equal(num2, amgr.select(arr2, num4)))); assertThatFormula(query).isUnsatisfiable(); } + + /* + * Test whether or not String Arrays are possible with String indexes + */ + @Test + public void testStringIndexStringValue() throws SolverException, InterruptedException { + requireStrings(); + + // (arr2 = store(arr1, "four", "two")) & !(select(arr2, "four") = "two") + StringFormula num2 = smgr.makeString("two"); + StringFormula num4 = smgr.makeString("four"); + ArrayFormula arr1 = + amgr.makeArray("arr1", StringType, StringType); + ArrayFormula arr2 = + amgr.makeArray("arr2", StringType, StringType); + BooleanFormula query = + bmgr.and( + amgr.equivalence(arr2, amgr.store(arr1, num4, num2)), + bmgr.not(smgr.equal(num2, amgr.select(arr2, num4)))); + assertThatFormula(query).isUnsatisfiable(); + } + + /* + * Test whether or not String Arrays with Int indexes are possible + */ + @Test + public void testIntIndexStringValue() throws SolverException, InterruptedException { + requireStrings(); + + // (arr2 = store(arr1, 4, "two")) & !(select(arr2, 4) = "two") + StringFormula stringTwo = smgr.makeString("two"); + IntegerFormula intFour = imgr.makeNumber(4); + ArrayFormula arr1 = + amgr.makeArray("arr1", FormulaType.IntegerType, StringType); + ArrayFormula arr2 = + amgr.makeArray("arr2", FormulaType.IntegerType, StringType); + BooleanFormula query = + bmgr.and( + amgr.equivalence(arr2, amgr.store(arr1, intFour, stringTwo)), + bmgr.not(smgr.equal(stringTwo, amgr.select(arr2, intFour)))); + assertThatFormula(query).isUnsatisfiable(); + } + + /* + * Test whether or not String Arrays with bitvector indexes are possible + */ + @Test + public void testBvIndexStringValue() throws SolverException, InterruptedException { + requireStrings(); + + // (arr2 = store(arr1, 0100, "two")) & !(select(arr2, 0100) = "two") + StringFormula stringTwo = smgr.makeString("two"); + BitvectorFormula bv4 = bvmgr.makeBitvector(4, 4); + ArrayFormula arr1 = + amgr.makeArray("arr1", getBitvectorTypeWithSize(4), StringType); + ArrayFormula arr2 = + amgr.makeArray("arr2", getBitvectorTypeWithSize(4), StringType); + BooleanFormula query = + bmgr.and( + amgr.equivalence(arr2, amgr.store(arr1, bv4, stringTwo)), + bmgr.not(smgr.equal(stringTwo, amgr.select(arr2, bv4)))); + assertThatFormula(query).isUnsatisfiable(); + } + + /* + * Test whether or not Bitvector Arrays are possible with bv index + */ + @Test + public void testBvIndexBvValue() throws SolverException, InterruptedException { + requireBitvectors(); + + // (arr2 = store(arr1, 0100, 0010)) & !(select(arr2, 0100) = 0010) + BitvectorFormula num2 = bvmgr.makeBitvector(4, 2); + BitvectorFormula num4 = bvmgr.makeBitvector(4, 4); + ArrayFormula arr1 = + amgr.makeArray("arr1", getBitvectorTypeWithSize(4), getBitvectorTypeWithSize(4)); + ArrayFormula arr2 = + amgr.makeArray("arr2", getBitvectorTypeWithSize(4), getBitvectorTypeWithSize(4)); + BooleanFormula query = + bmgr.and( + amgr.equivalence(arr2, amgr.store(arr1, num4, num2)), + bmgr.not(bvmgr.equal(num2, amgr.select(arr2, num4)))); + assertThatFormula(query).isUnsatisfiable(); + } + + /* + * Test whether or not Rational Arrays are possible with Rational index + */ + @Test + public void testRationalIndexRationalValue() throws SolverException, InterruptedException { + requireRationals(); + + // (arr2 = store(arr1, 4, 2)) & !(select(arr2, 4) = 2) + RationalFormula num2 = rmgr.makeNumber(2); + RationalFormula num4 = rmgr.makeNumber(4); + ArrayFormula arr1 = + amgr.makeArray("arr1", RationalType, RationalType); + ArrayFormula arr2 = + amgr.makeArray("arr2", RationalType, RationalType); + BooleanFormula query = + bmgr.and( + amgr.equivalence(arr2, amgr.store(arr1, num4, num2)), + bmgr.not(rmgr.equal(num2, amgr.select(arr2, num4)))); + assertThatFormula(query).isUnsatisfiable(); + } + + /* + * Test whether or not Float Arrays are possible with Float index + */ + @Test + public void testFloatIndexFloatValue() throws SolverException, InterruptedException { + requireFloats(); + + // (arr2 = store(arr1, 4.0, 2.0)) & !(select(arr2, 4.0) = 2.0) + FloatingPointFormula num2 = fpmgr.makeNumber(2, getSinglePrecisionFloatingPointType()); + FloatingPointFormula num4 = fpmgr.makeNumber(4, getSinglePrecisionFloatingPointType()); + ArrayFormula arr1 = + amgr.makeArray( + "arr1", getSinglePrecisionFloatingPointType(), getSinglePrecisionFloatingPointType()); + ArrayFormula arr2 = + amgr.makeArray( + "arr2", getSinglePrecisionFloatingPointType(), getSinglePrecisionFloatingPointType()); + BooleanFormula query = + bmgr.and( + amgr.equivalence(arr2, amgr.store(arr1, num4, num2)), + bmgr.not(fpmgr.equalWithFPSemantics(num2, amgr.select(arr2, num4)))); + assertThatFormula(query).isUnsatisfiable(); + } } diff --git a/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java b/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java index 656667c1df..893e6e00d0 100644 --- a/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java @@ -33,6 +33,24 @@ @RunWith(Parameterized.class) public class ModelEvaluationTest extends SolverBasedTest0 { + /** + * This is the default boolean value for unknown model evaluations. For unknown model evaluation + * for variables or formulas, the solver can return NULL or a default value. + */ + private static final boolean DEFAULT_MODEL_BOOLEAN = false; + + /** + * This is the default integer value for unknown model evaluations. For unknown model evaluation + * for variables or formulas, the solver can return NULL or a default value. + */ + private static final int DEFAULT_MODEL_INT = 0; + + /** + * This is the default String value for unknown model evaluations. For unknown model evaluation + * for variables or formulas, the solver can return NULL or a default value. + */ + private static final String DEFAULT_MODEL_STRING = ""; + @Parameters(name = "{0}") public static Object[] getAllSolvers() { return Solvers.values(); @@ -80,8 +98,8 @@ public void testGetSmallIntegersEvaluation1() throws SolverException, Interrupte evaluateInModel( imgr.equal(imgr.makeVariable("x"), imgr.makeNumber(10)), imgr.add(imgr.makeVariable("y"), imgr.makeVariable("z")), - Lists.newArrayList(null, BigInteger.ZERO), - Lists.newArrayList(null, imgr.makeNumber(0))); + Lists.newArrayList(null, BigInteger.valueOf(DEFAULT_MODEL_INT)), + Lists.newArrayList(null, imgr.makeNumber(DEFAULT_MODEL_INT))); } @Test @@ -111,8 +129,8 @@ public void testGetSmallIntegralRationalsEvaluation1() evaluateInModel( rmgr.equal(rmgr.makeVariable("x"), rmgr.makeNumber(1)), rmgr.add(rmgr.makeVariable("y"), rmgr.makeVariable("y")), - Lists.newArrayList(null, Rational.ZERO), - Lists.newArrayList(null, rmgr.makeNumber(0))); + Lists.newArrayList(null, Rational.of(DEFAULT_MODEL_INT)), + Lists.newArrayList(null, rmgr.makeNumber(DEFAULT_MODEL_INT))); } @Test @@ -122,8 +140,8 @@ public void testGetSmallIntegralRationalsEvaluation2() evaluateInModel( rmgr.equal(rmgr.makeVariable("x"), rmgr.makeNumber(1)), rmgr.makeVariable("y"), - Lists.newArrayList(null, Rational.ZERO), - Lists.newArrayList(null, rmgr.makeNumber(0))); + Lists.newArrayList(null, Rational.of(DEFAULT_MODEL_INT)), + Lists.newArrayList(null, rmgr.makeNumber(DEFAULT_MODEL_INT))); } @Test @@ -132,8 +150,8 @@ public void testGetRationalsEvaluation() throws SolverException, InterruptedExce evaluateInModel( rmgr.equal(rmgr.makeVariable("x"), rmgr.makeNumber(Rational.ofString("1/3"))), rmgr.divide(rmgr.makeVariable("y"), rmgr.makeNumber(2)), - Lists.newArrayList(null, Rational.ZERO), - Lists.newArrayList(null, rmgr.makeNumber(0))); + Lists.newArrayList(null, Rational.of(DEFAULT_MODEL_INT)), + Lists.newArrayList(null, rmgr.makeNumber(DEFAULT_MODEL_INT))); } @Test @@ -141,7 +159,17 @@ public void testGetBooleansEvaluation() throws SolverException, InterruptedExcep evaluateInModel( bmgr.makeVariable("x"), bmgr.makeVariable("y"), - Lists.newArrayList(null, false), - Lists.newArrayList(null, bmgr.makeBoolean(false))); + Lists.newArrayList(null, DEFAULT_MODEL_BOOLEAN), + Lists.newArrayList(null, bmgr.makeBoolean(DEFAULT_MODEL_BOOLEAN))); + } + + @Test + public void testGetStringsEvaluation() throws SolverException, InterruptedException { + requireStrings(); + evaluateInModel( + smgr.equal(smgr.makeVariable("x"), smgr.makeString("hello")), + smgr.makeVariable("y"), + Lists.newArrayList(null, DEFAULT_MODEL_STRING), + Lists.newArrayList(null, smgr.makeString(DEFAULT_MODEL_STRING))); } } diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index 9bd06ab1fa..398d5596b6 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -462,6 +462,18 @@ public void testGetBitvectors() throws SolverException, InterruptedException { "x"); } + @Test + public void testGetString() throws SolverException, InterruptedException { + requireStrings(); + for (String word : new String[] {"", "a", "abc", "1", "123", "-abc", "\"test\"", "\""}) { + testModelGetters( + smgr.equal(smgr.makeVariable("x"), smgr.makeString(word)), + smgr.makeVariable("x"), + word, + "x"); + } + } + @Test public void testGetModelAssignments() throws SolverException, InterruptedException { if (imgr != null) { diff --git a/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java b/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java index 54fb45286a..de4c74a091 100644 --- a/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java @@ -10,6 +10,7 @@ import static com.google.common.truth.Truth.assertThat; import static com.google.common.truth.TruthJUnit.assume; +import static org.sosy_lab.java_smt.api.FormulaType.StringType; import com.google.common.collect.ImmutableList; import edu.umd.cs.findbugs.annotations.SuppressFBWarnings; @@ -33,6 +34,7 @@ import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.StringFormula; import org.sosy_lab.java_smt.api.Tactic; import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor; @@ -132,6 +134,8 @@ private SolverException handleSolverException(SolverException e) throws SolverEx @Test public void testLIAForallArrayConjunctUnsat() throws SolverException, InterruptedException { + assume().that(solverUnderTest).isNotEqualTo(Solvers.CVC4); + // (forall x . b[x] = 0) AND (b[123] = 1) is UNSAT requireIntegers(); @@ -150,6 +154,8 @@ public void testBVForallArrayConjunctUnsat() throws SolverException, Interrupted assume().that(solverUnderTest).isNotEqualTo(Solvers.PRINCESS); // Boolector quants need to be reworked assume().that(solverUnderTest).isNotEqualTo(Solvers.BOOLECTOR); + // CVC4 can solve less quants with String support enabled, TODO bug? + assume().that(solverUnderTest).isNotEqualTo(Solvers.CVC4); BooleanFormula f = bmgr.and( @@ -340,6 +346,8 @@ public void testBVExistsArrayConjunct1() throws SolverException, InterruptedExce @Test public void testLIAExistsArrayConjunct2() throws SolverException, InterruptedException { + assume().that(solverUnderTest).isNotEqualTo(Solvers.CVC4); + // (exists x . b[x] = 1) AND (forall x . b[x] = 0) is UNSAT requireIntegers(); @@ -350,6 +358,8 @@ public void testLIAExistsArrayConjunct2() throws SolverException, InterruptedExc @Test public void testBVExistsArrayConjunct2() throws SolverException, InterruptedException { + assume().that(solverUnderTest).isNotEqualTo(Solvers.CVC4); + // (exists x . b[x] = 1) AND (forall x . b[x] = 0) is UNSAT requireBitvectors(); // Princess does not support bitvectors in arrays @@ -785,6 +795,8 @@ public void checkBVQuantifierElimination() throws InterruptedException, SolverEx @Test public void testExistsRestrictedRange() throws SolverException, InterruptedException { + assume().that(solverUnderTest).isNotEqualTo(Solvers.CVC4); + ArrayFormula b = amgr.makeArray("b", FormulaType.IntegerType, FormulaType.IntegerType); BooleanFormula bAtXEq1 = imgr.equal(amgr.select(b, x), imgr.makeNumber(1)); @@ -905,6 +917,85 @@ public void testForallRestrictedRangeWithoutConclusiveSolvers() .isSatisfiable(); } + @Test + public void testExistsBasicStringTheorie() throws SolverException, InterruptedException { + requireStrings(); + requireIntegers(); + + // exists var ("a" < var < "c") & length var == 1 -> var == "b" + StringFormula stringA = smgr.makeString("a"); + StringFormula stringC = smgr.makeString("c"); + StringFormula var = smgr.makeVariable("var"); + + BooleanFormula query = + qmgr.exists( + var, + bmgr.and( + imgr.equal(smgr.length(var), imgr.makeNumber(1)), + smgr.lessThan(stringA, var), + smgr.lessThan(var, stringC))); + assertThatFormula(query).isSatisfiable(); + } + + @Test + public void testForallBasicStringTheorie() throws SolverException, InterruptedException { + requireStrings(); + requireIntegers(); + + // forall var ("a" < var < "c") & length var == 1 + StringFormula stringA = smgr.makeString("a"); + StringFormula stringC = smgr.makeString("c"); + StringFormula var = smgr.makeVariable("var"); + + BooleanFormula query = + qmgr.forall( + var, + bmgr.and( + imgr.equal(smgr.length(var), imgr.makeNumber(1)), + smgr.lessThan(stringA, var), + smgr.lessThan(var, stringC))); + assertThatFormula(query).isUnsatisfiable(); + } + + @Test + public void testExistsBasicStringArray() throws SolverException, InterruptedException { + requireStrings(); + requireIntegers(); + + // exists var (var = select(store(arr, 2, "bla"), 2) + IntegerFormula two = imgr.makeNumber(2); + StringFormula string = smgr.makeString("bla"); + StringFormula var = smgr.makeVariable("var"); + ArrayFormula arr = + amgr.makeArray("arr", FormulaType.IntegerType, StringType); + BooleanFormula query = + qmgr.exists(var, smgr.equal(var, amgr.select(amgr.store(arr, two, string), two))); + assertThatFormula(query).isSatisfiable(); + } + + @Test + public void testForallBasicStringArray() throws SolverException, InterruptedException { + requireStrings(); + requireIntegers(); + + // CVC4 returns null or UNKNOWN, however it does not seem to have a problem with + // declaring/starting the solving process! + assume() + .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.CVC4); + + // forall var (var = select(store(arr, 2, "bla"), 2) + IntegerFormula two = imgr.makeNumber(2); + StringFormula string = smgr.makeString("bla"); + StringFormula var = smgr.makeVariable("var"); + ArrayFormula arr = + amgr.makeArray("arr", FormulaType.IntegerType, StringType); + BooleanFormula query = + qmgr.forall(var, smgr.equal(var, amgr.select(amgr.store(arr, two, string), two))); + assertThatFormula(query).isUnsatisfiable(); + } + private BooleanFormula forall( final IntegerFormula pVariable, final IntegerFormula pLowerBound, diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index bef2838819..5cfb739aa6 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -35,6 +35,7 @@ import org.sosy_lab.java_smt.api.QuantifiedFormulaManager; import org.sosy_lab.java_smt.api.RationalFormulaManager; import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.StringFormulaManager; import org.sosy_lab.java_smt.api.UFManager; /** @@ -84,6 +85,7 @@ public abstract class SolverBasedTest0 { protected @Nullable QuantifiedFormulaManager qmgr; protected @Nullable ArrayFormulaManager amgr; protected @Nullable FloatingPointFormulaManager fpmgr; + protected @Nullable StringFormulaManager smgr; protected ShutdownManager shutdownManager = ShutdownManager.create(); protected ShutdownNotifier shutdownNotifierToUse() { @@ -152,6 +154,11 @@ public final void initSolver() throws InvalidConfigurationException { } catch (UnsupportedOperationException e) { fpmgr = null; } + try { + smgr = mgr.getStringFormulaManager(); + } catch (UnsupportedOperationException e) { + smgr = null; + } } @After @@ -217,6 +224,14 @@ protected final void requireFloats() { .isNotNull(); } + /** Skip test if the solver does not support strings. */ + protected final void requireStrings() { + assume() + .withMessage("Solver %s does not support the theory of strings", solverToUse()) + .that(smgr) + .isNotNull(); + } + /** Skip test if the solver does not support optimization. */ protected final void requireOptimization() { try { diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index 15185e5d42..ce368dfeb5 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -40,7 +40,9 @@ import org.sosy_lab.java_smt.api.FunctionDeclaration; import org.sosy_lab.java_smt.api.FunctionDeclarationKind; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.RegexFormula; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.StringFormula; import org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor; import org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor; import org.sosy_lab.java_smt.api.visitors.DefaultBooleanFormulaVisitor; @@ -380,6 +382,101 @@ public TraversalProcess visitFunction( } } + @Test + public void stringInBooleanFormulaIdVisit() throws SolverException, InterruptedException { + requireStrings(); + StringFormula x = smgr.makeVariable("xVariable"); + StringFormula y = smgr.makeVariable("yVariable"); + RegexFormula r = smgr.makeRegex("regex1"); + + for (BooleanFormula f : + ImmutableList.of( + smgr.equal(x, y), + smgr.contains(x, y), + smgr.lessThan(x, y), + smgr.lessOrEquals(x, y), + smgr.greaterOrEquals(x, y), + smgr.greaterThan(x, y), + smgr.prefix(x, y), + smgr.suffix(x, y), + smgr.in(x, r))) { + mgr.visit(f, new FunctionDeclarationVisitorNoUF()); + mgr.visit(f, new FunctionDeclarationVisitorNoOther()); + BooleanFormula f2 = mgr.transformRecursively(f, new FormulaTransformationVisitor(mgr) {}); + assertThat(f2).isEqualTo(f); + assertThatFormula(f).isEquivalentTo(f2); + } + } + + @Test + public void stringInStringFormulaVisit() throws SolverException, InterruptedException { + requireStrings(); + StringFormula x = smgr.makeVariable("xVariable"); + StringFormula y = smgr.makeVariable("yVariable"); + StringFormula z = smgr.makeString("zAsString"); + IntegerFormula offset = imgr.makeVariable("offset"); + IntegerFormula len = imgr.makeVariable("len"); + + ImmutableList.Builder formulas = + ImmutableList.builder() + .add(smgr.substring(x, offset, len)) + .add(smgr.replace(x, y, z)) + .add(smgr.charAt(x, offset)) + .add(smgr.toStringFormula(offset)) + .add(smgr.concat(x, y, z)); + if (solverToUse() != Solvers.Z3) { + formulas.add(smgr.replaceAll(x, y, z)); // unsupported in Z3 + } + for (StringFormula f : formulas.build()) { + mgr.visit(f, new FunctionDeclarationVisitorNoUF()); + mgr.visit(f, new FunctionDeclarationVisitorNoOther()); + StringFormula f2 = mgr.transformRecursively(f, new FormulaTransformationVisitor(mgr) {}); + assertThat(f2).isEqualTo(f); + assertThatFormula(bmgr.not(smgr.equal(f, f2))).isUnsatisfiable(); + } + } + + @Test + public void stringInRegexFormulaVisit() { + requireStrings(); + RegexFormula r = smgr.makeRegex("regex1"); + RegexFormula s = smgr.makeRegex("regex2"); + + ImmutableList.Builder formulas = + ImmutableList.builder() + .add(smgr.union(r, s)) + .add(smgr.closure(r)) + .add(smgr.concat(r, r, r, s, s, s)) + .add(smgr.cross(r)); + if (solverToUse() != Solvers.Z3) { + formulas.add(smgr.difference(r, s)).add(smgr.complement(r)); + // invalid function OTHER/INTERNAL in visitor, bug in Z3? + } + for (RegexFormula f : formulas.build()) { + mgr.visit(f, new FunctionDeclarationVisitorNoUF()); + mgr.visit(f, new FunctionDeclarationVisitorNoOther()); + RegexFormula f2 = mgr.transformRecursively(f, new FormulaTransformationVisitor(mgr) {}); + assertThat(f2).isEqualTo(f); + } + } + + @Test + public void stringInIntegerFormulaVisit() throws SolverException, InterruptedException { + requireStrings(); + StringFormula x = smgr.makeVariable("xVariable"); + StringFormula y = smgr.makeVariable("yVariable"); + IntegerFormula offset = imgr.makeVariable("offset"); + + for (IntegerFormula f : + ImmutableList.of(smgr.indexOf(x, y, offset), smgr.length(x), smgr.toIntegerFormula(x))) { + mgr.visit(f, new FunctionDeclarationVisitorNoUF()); + mgr.visit(f, new FunctionDeclarationVisitorNoOther()); + IntegerFormula f2 = mgr.transformRecursively(f, new FormulaTransformationVisitor(mgr) {}); + assertThat(f2).isEqualTo(f); + assertThatFormula(bmgr.not(imgr.equal(f, f2))).isUnsatisfiable(); + } + } + private void checkKind(Formula f, FunctionDeclarationKind expected) { FunctionDeclarationVisitorNoOther visitor = new FunctionDeclarationVisitorNoOther(); mgr.visit(f, visitor); diff --git a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java new file mode 100644 index 0000000000..403a7a6d13 --- /dev/null +++ b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java @@ -0,0 +1,1541 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2021 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.test; + +import static com.google.common.truth.TruthJUnit.assume; + +import com.google.common.collect.ImmutableList; +import edu.umd.cs.findbugs.annotations.SuppressFBWarnings; +import java.util.List; +import org.junit.Before; +import org.junit.Ignore; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.junit.runners.Parameterized.Parameter; +import org.junit.runners.Parameterized.Parameters; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.RegexFormula; +import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.StringFormula; + +@SuppressWarnings("ConstantConditions") +@SuppressFBWarnings(value = "DLS_DEAD_LOCAL_STORE", justification = "test code") +@RunWith(Parameterized.class) +public class StringFormulaManagerTest extends SolverBasedTest0 { + + private static final ImmutableList WORDS = + ImmutableList.of( + "", + "0", + "1", + "10", + "a", + "b", + "A", + "B", + "aa", + "Aa", + "aA", + "AA", + "ab", + "aB", + "Ab", + "AB", + "ac", + "bb", + "aaa", + "Aaa", + "aAa", + "aAA", + "aab", + "aaabbb", + "bbbccc", + "abcde", + "abdde", + "abcdf", + "abchurrdurr", + "abcdefaaaaa"); + + private StringFormula hello; + private RegexFormula a2z; + + @Parameters(name = "{0}") + public static Object[] getAllSolvers() { + return Solvers.values(); + } + + @Parameter public Solvers solverUnderTest; + + @Override + protected Solvers solverToUse() { + return solverUnderTest; + } + + @Before + public void setup() { + requireStrings(); + hello = smgr.makeString("hello"); + a2z = smgr.range('a', 'z'); + } + + // Utility methods + + private void assertEqual(IntegerFormula num1, IntegerFormula num2) + throws SolverException, InterruptedException { + assertThatFormula(imgr.equal(num1, num2)).isTautological(); + } + + private void assertDistinct(IntegerFormula num1, IntegerFormula num2) + throws SolverException, InterruptedException { + assertThatFormula(imgr.distinct(List.of(num1, num2))).isTautological(); + } + + private void assertEqual(StringFormula str1, StringFormula str2) + throws SolverException, InterruptedException { + assertThatFormula(smgr.equal(str1, str2)).isTautological(); + } + + private void assertDistinct(StringFormula str1, StringFormula str2) + throws SolverException, InterruptedException { + assertThatFormula(smgr.equal(str1, str2)).isUnsatisfiable(); + } + + // Tests + + @Test + public void testRegexAll() throws SolverException, InterruptedException { + RegexFormula regex = smgr.all(); + assertThatFormula(smgr.in(hello, regex)).isSatisfiable(); + } + + @Test + public void testRegexAll3() throws SolverException, InterruptedException { + // This is not ALL_CHAR! This matches ".*" literally! + RegexFormula regex = smgr.makeRegex(".*"); + assertThatFormula(smgr.in(hello, regex)).isUnsatisfiable(); + assertThatFormula(smgr.in(smgr.makeString(".*"), regex)).isSatisfiable(); + } + + @Test + public void testStringRegex2() throws SolverException, InterruptedException { + RegexFormula regex = smgr.concat(smgr.closure(a2z), smgr.makeRegex("ll"), smgr.closure(a2z)); + assertThatFormula(smgr.in(hello, regex)).isSatisfiable(); + } + + @Test + public void testStringRegex3() throws SolverException, InterruptedException { + RegexFormula regex = smgr.makeRegex(".*ll.*"); + assertThatFormula(smgr.in(hello, regex)).isUnsatisfiable(); + } + + @Test + public void testEmptyRegex() throws SolverException, InterruptedException { + RegexFormula regex = smgr.none(); + assertThatFormula(smgr.in(hello, regex)).isUnsatisfiable(); + } + + @Test + public void testStringConcat() throws SolverException, InterruptedException { + StringFormula str1 = smgr.makeString("hello"); + StringFormula str2 = smgr.makeString("world"); + StringFormula concat = smgr.concat(str1, str2); + StringFormula complete = smgr.makeString("helloworld"); + + assertEqual(concat, complete); + } + + @Test + public void testStringConcatEmpty() throws SolverException, InterruptedException { + StringFormula empty = smgr.makeString(""); + + assertEqual(empty, smgr.concat(ImmutableList.of())); + assertEqual(empty, smgr.concat(empty)); + assertEqual(empty, smgr.concat(empty, empty)); + assertEqual(empty, smgr.concat(ImmutableList.of(empty, empty, empty, empty))); + } + + @Test + public void testStringPrefixSuffixConcat() throws SolverException, InterruptedException { + // check whether "prefix + suffix == concat" + StringFormula prefix = smgr.makeVariable("prefix"); + StringFormula suffix = smgr.makeVariable("suffix"); + StringFormula concat = smgr.makeVariable("concat"); + + assertThatFormula( + bmgr.and( + smgr.prefix(prefix, concat), + smgr.suffix(suffix, concat), + imgr.equal( + smgr.length(concat), imgr.add(smgr.length(prefix), smgr.length(suffix))))) + .implies(smgr.equal(concat, smgr.concat(prefix, suffix))); + } + + @Test + public void testStringPrefixSuffix() throws SolverException, InterruptedException { + // check whether "prefix == suffix iff equal length" + StringFormula prefix = smgr.makeVariable("prefix"); + StringFormula suffix = smgr.makeVariable("suffix"); + + assertThatFormula(bmgr.and(smgr.prefix(prefix, suffix), smgr.suffix(suffix, prefix))) + .implies(smgr.equal(prefix, suffix)); + assertThatFormula( + bmgr.and( + smgr.prefix(prefix, suffix), imgr.equal(smgr.length(prefix), smgr.length(suffix)))) + .implies(smgr.equal(prefix, suffix)); + assertThatFormula( + bmgr.and( + smgr.suffix(suffix, prefix), imgr.equal(smgr.length(prefix), smgr.length(suffix)))) + .implies(smgr.equal(prefix, suffix)); + } + + @Test + public void testStringToIntConversion() throws SolverException, InterruptedException { + IntegerFormula ten = imgr.makeNumber(10); + StringFormula zeroStr = smgr.makeString("0"); + + for (int i = 0; i < 100; i += 7) { + StringFormula str = smgr.makeString(Integer.toString(i)); + IntegerFormula num = imgr.makeNumber(i); + IntegerFormula numInc = imgr.makeNumber(i + 1); + + assertEqual(str, smgr.toStringFormula(num)); + assertDistinct(str, smgr.toStringFormula(numInc)); + assertDistinct(str, smgr.toStringFormula(imgr.add(num, numInc))); + + assertEqual(num, smgr.toIntegerFormula(str)); + assertDistinct(numInc, smgr.toIntegerFormula(str)); + assertEqual(imgr.multiply(num, ten), smgr.toIntegerFormula(smgr.concat(str, zeroStr))); + assertDistinct(imgr.multiply(numInc, ten), smgr.toIntegerFormula(smgr.concat(str, zeroStr))); + + assertEqual(num, smgr.toIntegerFormula(smgr.toStringFormula(num))); + assertEqual(numInc, smgr.toIntegerFormula(smgr.toStringFormula(numInc))); + } + } + + @Test + public void testStringToIntConversionCornerCases() throws SolverException, InterruptedException { + assertEqual(imgr.makeNumber(-1), smgr.toIntegerFormula(smgr.makeString("-1"))); + assertEqual(imgr.makeNumber(-1), smgr.toIntegerFormula(smgr.makeString("-12"))); + assertEqual(imgr.makeNumber(-1), smgr.toIntegerFormula(smgr.makeString("-123"))); + assertEqual(imgr.makeNumber(-1), smgr.toIntegerFormula(smgr.makeString("-1234"))); + + assertDistinct(imgr.makeNumber(-12), smgr.toIntegerFormula(smgr.makeString("-1"))); + assertDistinct(imgr.makeNumber(-12), smgr.toIntegerFormula(smgr.makeString("-12"))); + assertDistinct(imgr.makeNumber(-12), smgr.toIntegerFormula(smgr.makeString("-123"))); + assertDistinct(imgr.makeNumber(-12), smgr.toIntegerFormula(smgr.makeString("-1234"))); + + assertEqual(imgr.makeNumber(-1), smgr.toIntegerFormula(smgr.makeString(""))); + assertEqual(imgr.makeNumber(-1), smgr.toIntegerFormula(smgr.makeString("a"))); + assertEqual(imgr.makeNumber(-1), smgr.toIntegerFormula(smgr.makeString("1a"))); + assertEqual(imgr.makeNumber(-1), smgr.toIntegerFormula(smgr.makeString("a1"))); + + assertDistinct(imgr.makeNumber(-12), smgr.toIntegerFormula(smgr.makeString(""))); + assertDistinct(imgr.makeNumber(-12), smgr.toIntegerFormula(smgr.makeString("a"))); + assertDistinct(imgr.makeNumber(-12), smgr.toIntegerFormula(smgr.makeString("1a"))); + assertDistinct(imgr.makeNumber(-12), smgr.toIntegerFormula(smgr.makeString("a1"))); + } + + @Test + public void testIntToStringConversionCornerCases() throws SolverException, InterruptedException { + assertEqual(smgr.makeString("123"), smgr.toStringFormula(imgr.makeNumber(123))); + assertEqual(smgr.makeString("1"), smgr.toStringFormula(imgr.makeNumber(1))); + assertEqual(smgr.makeString("0"), smgr.toStringFormula(imgr.makeNumber(0))); + assertEqual(smgr.makeString(""), smgr.toStringFormula(imgr.makeNumber(-1))); + assertEqual(smgr.makeString(""), smgr.toStringFormula(imgr.makeNumber(-123))); + + assertDistinct(smgr.makeString("1"), smgr.toStringFormula(imgr.makeNumber(-1))); + } + + @Test + public void testStringLength() throws SolverException, InterruptedException { + assertEqual(imgr.makeNumber(0), smgr.length(smgr.makeString(""))); + assertEqual(imgr.makeNumber(1), smgr.length(smgr.makeString("a"))); + assertEqual(imgr.makeNumber(2), smgr.length(smgr.makeString("aa"))); + assertEqual(imgr.makeNumber(9), smgr.length(smgr.makeString("aaabbbccc"))); + + assertDistinct(imgr.makeNumber(5), smgr.length(smgr.makeString(""))); + assertDistinct(imgr.makeNumber(5), smgr.length(smgr.makeString("a"))); + assertDistinct(imgr.makeNumber(5), smgr.length(smgr.makeString("aa"))); + assertDistinct(imgr.makeNumber(5), smgr.length(smgr.makeString("aaabbbcc"))); + } + + @Test + public void testStringLengthWithVariable() throws SolverException, InterruptedException { + StringFormula var = smgr.makeVariable("var"); + + assertThatFormula(imgr.equal(imgr.makeNumber(0), smgr.length(var))) + .implies(smgr.equal(var, smgr.makeString(""))); + + assertThatFormula( + bmgr.and( + imgr.equal(imgr.makeNumber(5), smgr.length(var)), + smgr.prefix(smgr.makeString("aba"), var), + smgr.suffix(smgr.makeString("aba"), var))) + .implies(smgr.equal(smgr.makeVariable("var"), smgr.makeString("ababa"))); + + assertThatFormula( + bmgr.and( + imgr.equal(imgr.makeNumber(4), smgr.length(var)), + smgr.prefix(smgr.makeString("aba"), var), + smgr.suffix(smgr.makeString("aba"), var))) + .isUnsatisfiable(); + + assertThatFormula( + bmgr.and( + imgr.equal(imgr.makeNumber(4), smgr.length(var)), + smgr.prefix(smgr.makeString("ab"), var), + smgr.suffix(smgr.makeString("ba"), var), + smgr.equal(smgr.makeString("c"), smgr.charAt(var, imgr.makeNumber(3))))) + .isUnsatisfiable(); + + assertThatFormula( + bmgr.and( + imgr.equal(imgr.makeNumber(5), smgr.length(var)), + smgr.prefix(smgr.makeString("ab"), var), + smgr.suffix(smgr.makeString("ba"), var), + smgr.equal(smgr.makeString("c"), smgr.charAt(var, imgr.makeNumber(3))))) + .implies(smgr.equal(smgr.makeVariable("var"), smgr.makeString("abcba"))); + } + + @Test + public void testStringLengthPositiv() throws SolverException, InterruptedException { + assertThatFormula(imgr.lessOrEquals(imgr.makeNumber(0), smgr.length(smgr.makeVariable("x")))) + .isTautological(); + assertThatFormula(imgr.greaterThan(imgr.makeNumber(0), smgr.length(smgr.makeVariable("x")))) + .isUnsatisfiable(); + } + + @Test + public void testStringCompare() throws SolverException, InterruptedException { + StringFormula var1 = smgr.makeVariable("0"); + StringFormula var2 = smgr.makeVariable("1"); + assertThatFormula(bmgr.and(smgr.lessOrEquals(var1, var2), smgr.greaterOrEquals(var1, var2))) + .implies(smgr.equal(var1, var2)); + assertThatFormula(smgr.equal(var1, var2)) + .implies(bmgr.and(smgr.lessOrEquals(var1, var2), smgr.greaterOrEquals(var1, var2))); + } + + /** Test const Strings = String variables + prefix and suffix constraints. */ + @Test + public void testConstStringEqStringVar() throws SolverException, InterruptedException { + String string1 = ""; + String string2 = "a"; + String string3 = "ab"; + String string4 = "abcdefghijklmnopqrstuvwxyz"; + StringFormula string1c = smgr.makeString(string1); + StringFormula string2c = smgr.makeString(string2); + StringFormula string3c = smgr.makeString(string3); + StringFormula string4c = smgr.makeString(string4); + StringFormula string1v = smgr.makeVariable("string1v"); + StringFormula string2v = smgr.makeVariable("string1v"); + StringFormula string3v = smgr.makeVariable("string1v"); + StringFormula string4v = smgr.makeVariable("string1v"); + + BooleanFormula formula = + bmgr.and( + smgr.equal(string1c, string1v), + smgr.equal(string2c, string2v), + smgr.equal(string3c, string3v), + smgr.equal(string4c, string4v)); + + BooleanFormula string1PrefixFormula = + bmgr.and( + smgr.prefix(string1c, string1v), + bmgr.not(smgr.prefix(string2c, string1v)), + bmgr.not(smgr.prefix(string3c, string1v)), + bmgr.not(smgr.prefix(string4c, string1v))); + + BooleanFormula string2PrefixFormula = + bmgr.and( + smgr.prefix(string1c, string2v), + smgr.prefix(string2c, string2v), + bmgr.not(smgr.prefix(string3c, string2v)), + bmgr.not(smgr.prefix(string4c, string2v))); + + BooleanFormula string3PrefixFormula = + bmgr.and( + smgr.prefix(string1c, string3v), + smgr.prefix(string2c, string3v), + smgr.prefix(string3c, string3v), + bmgr.not(smgr.prefix(string4c, string3v))); + + BooleanFormula string4PrefixFormula = + bmgr.and( + smgr.prefix(string1c, string4v), + smgr.prefix(string2c, string4v), + smgr.prefix(string3c, string4v), + smgr.prefix(string4c, string4v)); + + BooleanFormula string1SuffixFormula = + bmgr.and( + smgr.suffix(string1c, string1v), + bmgr.not(smgr.suffix(string2c, string1v)), + bmgr.not(smgr.suffix(string3c, string1v)), + bmgr.not(smgr.suffix(string4c, string1v))); + + BooleanFormula string2SuffixFormula = + bmgr.and( + smgr.suffix(string1c, string2v), + bmgr.not(smgr.suffix(string3c, string2v)), + bmgr.not(smgr.suffix(string4c, string2v))); + + BooleanFormula string3SuffixFormula = + bmgr.and( + smgr.suffix(string1c, string3v), + smgr.suffix(string3c, string3v), + bmgr.not(smgr.suffix(string4c, string3v))); + + BooleanFormula string4SuffixFormula = + bmgr.and(smgr.suffix(string1c, string4v), smgr.suffix(string4c, string4v)); + + assertThatFormula(bmgr.and(formula)) + .implies( + bmgr.and( + string1PrefixFormula, + string2PrefixFormula, + string3PrefixFormula, + string4PrefixFormula, + string1SuffixFormula, + string2SuffixFormula, + string3SuffixFormula, + string4SuffixFormula)); + } + + /** Test String variables with negative length (UNSAT). */ + @Test + public void testStringVariableLengthNegative() throws SolverException, InterruptedException { + StringFormula stringVariable1 = smgr.makeVariable("zeroLength"); + StringFormula stringVariable2 = smgr.makeVariable("negLength"); + + // SAT + UNSAT Formula -> UNSAT + assertThatFormula( + bmgr.and( + imgr.equal(smgr.length(stringVariable1), imgr.makeNumber(0)), + imgr.equal(smgr.length(stringVariable2), imgr.makeNumber(-100)))) + .isUnsatisfiable(); + // UNSAT below + assertThatFormula(imgr.equal(smgr.length(stringVariable2), imgr.makeNumber(-1))) + .isUnsatisfiable(); + assertThatFormula(imgr.equal(smgr.length(stringVariable2), imgr.makeNumber(-100))) + .isUnsatisfiable(); + } + + /** + * Test String formulas with inequalities in the negative range. + * + *

-10000 < stringVariable length < 0 -> UNSAT + * + *

-10000 < stringVariable length < -1 -> UNSAT + * + *

-10000 <= stringVariable length <= -1 -> UNSAT + * + *

-10000 <= stringVariable length <= 0 AND stringVariable != "" -> UNSAT + * + *

-10000 <= stringVariable length <= 0 -> SAT implies stringVariable = "" + */ + @Test + public void testStringLengthInequalityNegativeRange() + throws SolverException, InterruptedException { + StringFormula stringVariable = smgr.makeVariable("stringVariable"); + IntegerFormula stringVariableLength = smgr.length(stringVariable); + IntegerFormula minusTenThousand = imgr.makeNumber(-10000); + IntegerFormula minusOne = imgr.makeNumber(-1); + IntegerFormula zero = imgr.makeNumber(0); + + // -10000 < stringVariable length < 0 -> UNSAT + assertThatFormula( + bmgr.and( + imgr.lessThan(minusTenThousand, stringVariableLength), + imgr.lessThan(stringVariableLength, zero))) + .isUnsatisfiable(); + // -10000 < stringVariable length < -1 -> UNSAT + assertThatFormula( + bmgr.and( + imgr.lessThan(minusTenThousand, stringVariableLength), + imgr.lessThan(stringVariableLength, minusOne))) + .isUnsatisfiable(); + // -10000 <= stringVariable length <= -1 -> UNSAT + assertThatFormula( + bmgr.and( + imgr.lessOrEquals(minusTenThousand, stringVariableLength), + imgr.lessOrEquals(stringVariableLength, minusOne))) + .isUnsatisfiable(); + // -10000 <= stringVariable length <= 0 AND stringVariable != "" -> UNSAT + assertThatFormula( + bmgr.and( + imgr.lessOrEquals(minusTenThousand, stringVariableLength), + imgr.lessOrEquals(stringVariableLength, zero), + bmgr.not(smgr.equal(stringVariable, smgr.makeString(""))))) + .isUnsatisfiable(); + // -10000 <= stringVariable length <= 0 -> SAT implies stringVariable = "" + assertThatFormula( + bmgr.and( + imgr.lessOrEquals(minusTenThousand, stringVariableLength), + imgr.lessOrEquals(stringVariableLength, zero))) + .implies(smgr.equal(stringVariable, smgr.makeString(""))); + } + + /** + * Test String formulas with inequalities in the negative range. + * + *

0 < stringVariable length < 1 -> UNSAT + * + *

0 < stringVariable length < 2 -> SAT + * + *

0 <= stringVariable length < 1 -> SAT implies stringVariable = "" + * + *

1 < stringVariable length < 3 -> SAT implies stringVariable length = 2 + */ + @Test + public void testStringLengthInequalityPositiveRange() + throws SolverException, InterruptedException { + StringFormula stringVariable = smgr.makeVariable("stringVariable"); + IntegerFormula stringVariableLength = smgr.length(stringVariable); + IntegerFormula three = imgr.makeNumber(3); + IntegerFormula two = imgr.makeNumber(2); + IntegerFormula one = imgr.makeNumber(1); + IntegerFormula zero = imgr.makeNumber(0); + + // 0 < stringVariable length < 1 -> UNSAT + assertThatFormula( + bmgr.and( + imgr.lessThan(zero, stringVariableLength), + imgr.lessThan(stringVariableLength, one))) + .isUnsatisfiable(); + // 0 < stringVariable length < 2 -> SAT + assertThatFormula( + bmgr.and( + imgr.lessThan(zero, stringVariableLength), + imgr.lessThan(stringVariableLength, two))) + .isSatisfiable(); + // 0 <= stringVariable length < 1 -> SAT implies stringVariable = "" + assertThatFormula( + bmgr.and( + imgr.lessOrEquals(zero, stringVariableLength), + imgr.lessThan(stringVariableLength, one))) + .implies(smgr.equal(stringVariable, smgr.makeString(""))); + // 1 < stringVariable length < 3 -> SAT implies stringVariable length = 2 + assertThatFormula( + bmgr.and( + imgr.lessThan(one, stringVariableLength), + imgr.lessThan(stringVariableLength, three))) + .implies(imgr.equal(smgr.length(stringVariable), two)); + } + + /** Test simple String lexicographic ordering (< <= > >=) for constant Strings. */ + @Test + public void testSimpleConstStringLexicographicOrdering() + throws SolverException, InterruptedException { + List words = ImmutableList.sortedCopyOf(WORDS); + + for (int i = 1; i < words.size(); i++) { + StringFormula word1 = smgr.makeString(words.get(i - 1)); + StringFormula word2 = smgr.makeString(words.get(i)); + + assertThatFormula(smgr.lessThan(word1, word1)).isUnsatisfiable(); + assertThatFormula(smgr.lessOrEquals(word1, word1)).isSatisfiable(); + assertThatFormula(smgr.greaterOrEquals(word1, word1)).isSatisfiable(); + + assertThatFormula(smgr.lessThan(word1, word2)).isSatisfiable(); + assertThatFormula(smgr.lessOrEquals(word1, word2)).isSatisfiable(); + assertThatFormula(smgr.greaterThan(word1, word2)).isUnsatisfiable(); + assertThatFormula(smgr.greaterOrEquals(word1, word2)).isUnsatisfiable(); + } + } + + /** Test simple String lexicographic ordering (< <= > >=) for String variables. */ + @Test + public void testSimpleStringVariableLexicographicOrdering() + throws SolverException, InterruptedException { + StringFormula a = smgr.makeString("a"); + StringFormula b = smgr.makeString("b"); + StringFormula ab = smgr.makeString("ab"); + StringFormula abc = smgr.makeString("abc"); + StringFormula abd = smgr.makeString("abd"); + StringFormula abe = smgr.makeString("abe"); + StringFormula abaab = smgr.makeString("abaab"); + StringFormula abbab = smgr.makeString("abbab"); + StringFormula abcab = smgr.makeString("abcab"); + StringFormula stringVariable = smgr.makeVariable("stringVariable"); + + assertThatFormula( + bmgr.and( + smgr.lessThan(a, stringVariable), + smgr.lessThan(stringVariable, b), + imgr.equal(imgr.makeNumber(0), smgr.length(stringVariable)))) + .implies(smgr.equal(stringVariable, smgr.makeString(""))); + + assertThatFormula( + bmgr.and( + smgr.lessOrEquals(a, stringVariable), + smgr.lessThan(stringVariable, b), + imgr.equal(imgr.makeNumber(1), smgr.length(stringVariable)))) + .implies(smgr.equal(stringVariable, smgr.makeString("a"))); + + assertThatFormula( + bmgr.and( + smgr.lessThan(a, stringVariable), + smgr.lessOrEquals(stringVariable, b), + imgr.equal(imgr.makeNumber(1), smgr.length(stringVariable)))) + .implies(smgr.equal(stringVariable, b)); + + assertThatFormula( + bmgr.and( + smgr.lessOrEquals(abc, stringVariable), + smgr.lessThan(stringVariable, abd), + imgr.equal(imgr.makeNumber(3), smgr.length(stringVariable)))) + .implies(smgr.equal(stringVariable, abc)); + + assertThatFormula( + bmgr.and( + smgr.lessThan(abc, stringVariable), + smgr.lessThan(stringVariable, abe), + imgr.equal(imgr.makeNumber(3), smgr.length(stringVariable)))) + .implies(smgr.equal(stringVariable, abd)); + + assertThatFormula( + bmgr.and( + smgr.lessThan(abc, stringVariable), + smgr.lessOrEquals(stringVariable, abd), + imgr.equal(imgr.makeNumber(3), smgr.length(stringVariable)))) + .implies(smgr.equal(stringVariable, abd)); + + assertThatFormula( + bmgr.and( + smgr.lessThan(abaab, stringVariable), + smgr.lessThan(stringVariable, abcab), + smgr.prefix(ab, stringVariable), + smgr.suffix(ab, stringVariable), + imgr.equal(imgr.makeNumber(5), smgr.length(stringVariable)))) + .implies(smgr.equal(stringVariable, abbab)); + } + + /** Takeaway: invalid positions always refer to the empty string! */ + @Test + public void testCharAtWithConstString() throws SolverException, InterruptedException { + StringFormula empty = smgr.makeString(""); + StringFormula a = smgr.makeString("a"); + StringFormula b = smgr.makeString("b"); + StringFormula ab = smgr.makeString("ab"); + + assertEqual(smgr.charAt(empty, imgr.makeNumber(1)), empty); + assertEqual(smgr.charAt(empty, imgr.makeNumber(0)), empty); + assertEqual(smgr.charAt(empty, imgr.makeNumber(-1)), empty); + + assertDistinct(smgr.charAt(a, imgr.makeNumber(-1)), a); + assertEqual(smgr.charAt(a, imgr.makeNumber(-1)), empty); + assertEqual(smgr.charAt(a, imgr.makeNumber(0)), a); + assertDistinct(smgr.charAt(a, imgr.makeNumber(1)), a); + assertEqual(smgr.charAt(a, imgr.makeNumber(1)), empty); + assertDistinct(smgr.charAt(a, imgr.makeNumber(2)), a); + assertEqual(smgr.charAt(a, imgr.makeNumber(2)), empty); + + assertEqual(smgr.charAt(ab, imgr.makeNumber(0)), a); + assertEqual(smgr.charAt(ab, imgr.makeNumber(1)), b); + assertDistinct(smgr.charAt(ab, imgr.makeNumber(0)), b); + assertDistinct(smgr.charAt(ab, imgr.makeNumber(1)), a); + } + + /** + * Test escapecharacter treatment. Escape characters are treated as a single char! Example: + * "a\u1234T" has "a" at position 0, "\u1234" at position 1 and "T" at position 2 + * + *

SMTLIB2 uses an escape sequence for the numerals of the sort: {1234}. + */ + @Test + public void testCharAtWithSpecialCharacters() throws SolverException, InterruptedException { + assume() + .withMessage("Solver %s does only support 2 byte unicode", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.Z3); + + StringFormula num1 = smgr.makeString("1"); + StringFormula u = smgr.makeString("u"); + StringFormula curlyOpen = smgr.makeString("\u007B"); + StringFormula curlyClose = smgr.makeString("\u007D"); + StringFormula u1234WOEscape = smgr.makeString("u1234"); + StringFormula au1234WOEscape = smgr.makeString("au1234"); + // Java needs a double {{ as the first one is needed as an escape char for the second, this is a + // workaround + String workaround = "au\u007B1234\u007D"; + StringFormula au1234WOEscapeCurly = smgr.makeString(workaround); + StringFormula backSlash = smgr.makeString("\\"); + StringFormula a = smgr.makeString("a"); + StringFormula b = smgr.makeString("b"); + StringFormula u1234 = smgr.makeString("\\u{1234}"); + StringFormula au1234b = smgr.makeString("a\\u{1234}b"); + StringFormula stringVariable = smgr.makeVariable("stringVariable"); + + // Javas backslash (double written) is just 1 char + assertThatFormula(imgr.equal(smgr.length(backSlash), imgr.makeNumber(1))).isSatisfiable(); + + assertThatFormula(smgr.equal(smgr.charAt(au1234b, imgr.makeNumber(0)), stringVariable)) + .implies(smgr.equal(stringVariable, a)); + + // It seems like CVC4 sees the backslash as its own char! + assertThatFormula(smgr.equal(smgr.charAt(au1234b, imgr.makeNumber(1)), stringVariable)) + .implies(smgr.equal(stringVariable, u1234)); + + assertThatFormula(smgr.equal(smgr.charAt(au1234b, imgr.makeNumber(2)), stringVariable)) + .implies(smgr.equal(stringVariable, b)); + + assertThatFormula( + bmgr.and( + smgr.equal(smgr.charAt(u1234WOEscape, imgr.makeNumber(0)), u), + smgr.equal(smgr.charAt(u1234WOEscape, imgr.makeNumber(1)), num1))) + .isSatisfiable(); + + assertThatFormula( + bmgr.and( + smgr.equal(smgr.charAt(au1234WOEscape, imgr.makeNumber(0)), a), + smgr.equal(smgr.charAt(au1234WOEscape, imgr.makeNumber(1)), u), + smgr.equal(smgr.charAt(au1234WOEscape, imgr.makeNumber(2)), num1))) + .isSatisfiable(); + + assertThatFormula( + bmgr.and( + smgr.equal(smgr.charAt(au1234WOEscapeCurly, imgr.makeNumber(0)), a), + smgr.equal(smgr.charAt(au1234WOEscapeCurly, imgr.makeNumber(1)), u), + smgr.equal(smgr.charAt(au1234WOEscapeCurly, imgr.makeNumber(2)), curlyOpen), + smgr.equal(smgr.charAt(au1234WOEscapeCurly, imgr.makeNumber(7)), curlyClose))) + .isSatisfiable(); + + // Check that the unicode is not treated as seperate chars + assertThatFormula( + bmgr.and( + smgr.equal(smgr.charAt(u1234, imgr.makeNumber(0)), smgr.makeString("\\")), + smgr.equal(smgr.charAt(u1234, imgr.makeNumber(1)), u), + smgr.equal(smgr.charAt(u1234, imgr.makeNumber(2)), num1))) + .isUnsatisfiable(); + } + + /** + * Same as {@link #testCharAtWithSpecialCharacters} but only with 2 Byte special chars as Z3 only + * supports those. + */ + @Test + public void testCharAtWithSpecialCharacters2Byte() throws SolverException, InterruptedException { + StringFormula num7 = smgr.makeString("7"); + StringFormula u = smgr.makeString("u"); + StringFormula curlyOpen2BUnicode = smgr.makeString("\\u{7B}"); + StringFormula curlyClose2BUnicode = smgr.makeString("\\u{7D}"); + StringFormula acurlyClose2BUnicodeb = smgr.makeString("a\\u{7D}b"); + // Java needs a double {{ as the first one is needed as a escape char for the second, this is a + // workaround + String workaround = "au\u007B7B\u007D"; + StringFormula acurlyOpen2BUnicodeWOEscapeCurly = smgr.makeString(workaround); + // StringFormula backSlash = smgr.makeString("\\"); + StringFormula a = smgr.makeString("a"); + StringFormula b = smgr.makeString("b"); + StringFormula stringVariable = smgr.makeVariable("stringVariable"); + + // Curly braces unicode is treated as 1 char + assertThatFormula(imgr.equal(smgr.length(curlyOpen2BUnicode), imgr.makeNumber(1))) + .isSatisfiable(); + assertThatFormula(imgr.equal(smgr.length(curlyClose2BUnicode), imgr.makeNumber(1))) + .isSatisfiable(); + + // check a}b + assertThatFormula( + smgr.equal(smgr.charAt(acurlyClose2BUnicodeb, imgr.makeNumber(0)), stringVariable)) + .implies(smgr.equal(stringVariable, a)); + + assertThatFormula( + smgr.equal(smgr.charAt(acurlyClose2BUnicodeb, imgr.makeNumber(1)), stringVariable)) + .implies(smgr.equal(stringVariable, curlyClose2BUnicode)); + + assertThatFormula( + smgr.equal(smgr.charAt(acurlyClose2BUnicodeb, imgr.makeNumber(2)), stringVariable)) + .implies(smgr.equal(stringVariable, b)); + + // Check the unescaped version (missing backslash) + assertThatFormula( + bmgr.and( + smgr.equal(smgr.charAt(acurlyOpen2BUnicodeWOEscapeCurly, imgr.makeNumber(0)), a), + smgr.equal(smgr.charAt(acurlyOpen2BUnicodeWOEscapeCurly, imgr.makeNumber(1)), u), + smgr.equal( + smgr.charAt(acurlyOpen2BUnicodeWOEscapeCurly, imgr.makeNumber(2)), + curlyOpen2BUnicode), + smgr.equal(smgr.charAt(acurlyOpen2BUnicodeWOEscapeCurly, imgr.makeNumber(3)), num7), + smgr.equal( + smgr.charAt(acurlyOpen2BUnicodeWOEscapeCurly, imgr.makeNumber(4)), + smgr.makeString("B")), + smgr.equal( + smgr.charAt(acurlyOpen2BUnicodeWOEscapeCurly, imgr.makeNumber(5)), + curlyClose2BUnicode))) + .isSatisfiable(); + } + + @Test + public void testCharAtWithStringVariable() throws SolverException, InterruptedException { + StringFormula a = smgr.makeString("a"); + StringFormula b = smgr.makeString("b"); + StringFormula ab = smgr.makeString("ab"); + StringFormula aa = smgr.makeString("aa"); + StringFormula abc = smgr.makeString("abc"); + StringFormula aabc = smgr.makeString("aabc"); + StringFormula abcb = smgr.makeString("abcb"); + StringFormula stringVariable = smgr.makeVariable("stringVariable"); + + assertThatFormula(smgr.equal(smgr.charAt(ab, imgr.makeNumber(0)), stringVariable)) + .implies(smgr.equal(stringVariable, a)); + + assertThatFormula(smgr.equal(smgr.charAt(ab, imgr.makeNumber(1)), stringVariable)) + .implies(smgr.equal(stringVariable, b)); + + assertThatFormula( + bmgr.and( + smgr.equal(smgr.charAt(ab, imgr.makeNumber(0)), stringVariable), + smgr.equal(smgr.charAt(ab, imgr.makeNumber(1)), stringVariable))) + .isUnsatisfiable(); + + assertThatFormula( + bmgr.and( + smgr.equal(smgr.charAt(aa, imgr.makeNumber(0)), stringVariable), + smgr.equal(smgr.charAt(aa, imgr.makeNumber(1)), stringVariable))) + .implies(smgr.equal(stringVariable, a)); + + assertThatFormula( + bmgr.and( + smgr.equal(smgr.charAt(stringVariable, imgr.makeNumber(0)), a), + smgr.equal(smgr.charAt(stringVariable, imgr.makeNumber(1)), b), + imgr.equal(imgr.makeNumber(2), smgr.length(stringVariable)))) + .implies(smgr.equal(stringVariable, ab)); + + assertThatFormula( + bmgr.and( + smgr.equal(smgr.charAt(stringVariable, imgr.makeNumber(0)), a), + smgr.equal(smgr.charAt(stringVariable, imgr.makeNumber(2)), b), + imgr.equal(imgr.makeNumber(4), smgr.length(stringVariable)), + smgr.suffix(abc, stringVariable))) + .implies(smgr.equal(stringVariable, aabc)); + + assertThatFormula( + bmgr.and( + smgr.equal(smgr.charAt(stringVariable, imgr.makeNumber(0)), a), + smgr.equal(smgr.charAt(stringVariable, imgr.makeNumber(3)), b), + imgr.equal(imgr.makeNumber(4), smgr.length(stringVariable)), + smgr.suffix(abc, stringVariable))) + .implies(smgr.equal(stringVariable, abcb)); + + assertThatFormula( + bmgr.and( + smgr.equal(smgr.charAt(stringVariable, imgr.makeNumber(0)), a), + smgr.equal(smgr.charAt(stringVariable, imgr.makeNumber(3)), b), + imgr.equal(imgr.makeNumber(4), smgr.length(stringVariable)), + smgr.prefix(abc, stringVariable))) + .implies(smgr.equal(stringVariable, abcb)); + } + + @Test + public void testConstStringContains() throws SolverException, InterruptedException { + StringFormula empty = smgr.makeString(""); + StringFormula a = smgr.makeString("a"); + StringFormula aUppercase = smgr.makeString("A"); + StringFormula bUppercase = smgr.makeString("B"); + StringFormula b = smgr.makeString("b"); + StringFormula bbbbbb = smgr.makeString("bbbbbb"); + StringFormula bbbbbbb = smgr.makeString("bbbbbbb"); + StringFormula abbbbbb = smgr.makeString("abbbbbb"); + StringFormula aaaaaaaB = smgr.makeString("aaaaaaaB"); + StringFormula abcAndSoOn = smgr.makeString("abcdefghijklmnopqrstuVwxyz"); + StringFormula curlyOpen2BUnicode = smgr.makeString("\\u{7B}"); + StringFormula curlyClose2BUnicode = smgr.makeString("\\u{7D}"); + StringFormula multipleCurlys2BUnicode = smgr.makeString("\\u{7B}\\u{7D}\\u{7B}\\u{7B}"); + StringFormula curlyClose2BUnicodeEncased = smgr.makeString("blabla\\u{7D}bla"); + + assertThatFormula(smgr.contains(empty, empty)).isSatisfiable(); + assertThatFormula(smgr.contains(empty, a)).isUnsatisfiable(); + assertThatFormula(smgr.contains(a, empty)).isSatisfiable(); + assertThatFormula(smgr.contains(a, a)).isSatisfiable(); + assertThatFormula(smgr.contains(a, aUppercase)).isUnsatisfiable(); + assertThatFormula(smgr.contains(aUppercase, a)).isUnsatisfiable(); + assertThatFormula(smgr.contains(a, b)).isUnsatisfiable(); + assertThatFormula(smgr.contains(b, b)).isSatisfiable(); + assertThatFormula(smgr.contains(abbbbbb, a)).isSatisfiable(); + assertThatFormula(smgr.contains(abbbbbb, b)).isSatisfiable(); + assertThatFormula(smgr.contains(abbbbbb, bbbbbb)).isSatisfiable(); + assertThatFormula(smgr.contains(abbbbbb, bbbbbbb)).isUnsatisfiable(); + assertThatFormula(smgr.contains(abbbbbb, aUppercase)).isUnsatisfiable(); + assertThatFormula(smgr.contains(abbbbbb, aUppercase)).isUnsatisfiable(); + assertThatFormula(smgr.contains(aaaaaaaB, a)).isSatisfiable(); + assertThatFormula(smgr.contains(aaaaaaaB, b)).isUnsatisfiable(); + assertThatFormula(smgr.contains(aaaaaaaB, bUppercase)).isSatisfiable(); + assertThatFormula(smgr.contains(aaaaaaaB, curlyOpen2BUnicode)).isUnsatisfiable(); + assertThatFormula(smgr.contains(abcAndSoOn, smgr.makeString("xyz"))).isSatisfiable(); + assertThatFormula(smgr.contains(abcAndSoOn, smgr.makeString("Vwxyz"))).isSatisfiable(); + assertThatFormula(smgr.contains(abcAndSoOn, smgr.makeString("Vwxyza"))).isUnsatisfiable(); + assertThatFormula(smgr.contains(abcAndSoOn, smgr.makeString("t Vwxyz"))).isUnsatisfiable(); + assertThatFormula(smgr.contains(multipleCurlys2BUnicode, curlyOpen2BUnicode)).isSatisfiable(); + assertThatFormula(smgr.contains(multipleCurlys2BUnicode, curlyClose2BUnicode)).isSatisfiable(); + assertThatFormula(smgr.contains(curlyClose2BUnicodeEncased, curlyClose2BUnicode)) + .isSatisfiable(); + } + + @Test + public void testStringVariableContains() throws SolverException, InterruptedException { + StringFormula var1 = smgr.makeVariable("var1"); + StringFormula var2 = smgr.makeVariable("var2"); + + StringFormula empty = smgr.makeString(""); + StringFormula bUppercase = smgr.makeString("B"); + StringFormula ab = smgr.makeString("ab"); + StringFormula bbbbbb = smgr.makeString("bbbbbb"); + StringFormula abbbbbb = smgr.makeString("abbbbbb"); + StringFormula curlyOpen2BUnicode = smgr.makeString("\\u{7B}"); + StringFormula curlyClose2BUnicode = smgr.makeString("\\u{7D}"); + + assertThatFormula( + bmgr.and(smgr.contains(var1, empty), imgr.equal(imgr.makeNumber(0), smgr.length(var1)))) + .implies(smgr.equal(var1, empty)); + + assertThatFormula(bmgr.and(smgr.contains(var1, var2), smgr.contains(var2, var1))) + .implies(smgr.equal(var1, var2)); + + // Unicode is treated as 1 char. So \\u{7B} is treated as { and the B inside is not contained! + assertThatFormula( + bmgr.and( + smgr.contains(var1, curlyOpen2BUnicode), + smgr.contains(var1, bUppercase), + imgr.equal(imgr.makeNumber(1), smgr.length(var1)))) + .isUnsatisfiable(); + // Same goes for the curly brackets used as escape sequence + assertThatFormula( + bmgr.and( + smgr.contains(var1, curlyOpen2BUnicode), + smgr.contains(var1, curlyClose2BUnicode), + imgr.equal(imgr.makeNumber(1), smgr.length(var1)))) + .isUnsatisfiable(); + + assertThatFormula( + bmgr.and( + smgr.contains(var1, bbbbbb), + smgr.contains(var1, ab), + imgr.equal(imgr.makeNumber(7), smgr.length(var1)))) + .implies(smgr.equal(var1, abbbbbb)); + } + + @Test + public void testStringContainsOtherVariable() throws SolverException, InterruptedException { + assume() + .withMessage("Solver %s runs endlessly on this task", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.Z3); + + StringFormula var1 = smgr.makeVariable("var1"); + StringFormula var2 = smgr.makeVariable("var2"); + + StringFormula abUppercase = smgr.makeString("AB"); + StringFormula ab = smgr.makeString("ab"); + + assertThatFormula( + bmgr.and( + smgr.contains(var1, ab), + smgr.contains(var2, abUppercase), + smgr.contains(var1, var2))) + .implies(smgr.contains(var1, abUppercase)); + } + + @Test + public void testConstStringIndexOf() throws SolverException, InterruptedException { + StringFormula empty = smgr.makeString(""); + StringFormula a = smgr.makeString("a"); + StringFormula aUppercase = smgr.makeString("A"); + StringFormula b = smgr.makeString("b"); + StringFormula ab = smgr.makeString("ab"); + StringFormula bbbbbb = smgr.makeString("bbbbbb"); + StringFormula bbbbbbb = smgr.makeString("bbbbbbb"); + StringFormula abbbbbb = smgr.makeString("abbbbbb"); + StringFormula abcAndSoOn = smgr.makeString("abcdefghijklmnopqrstuVwxyz"); + StringFormula curlyOpen2BUnicode = smgr.makeString("\\u{7B}"); + StringFormula curlyClose2BUnicode = smgr.makeString("\\u{7D}"); + StringFormula multipleCurlys2BUnicode = smgr.makeString("\\u{7B}\\u{7D}\\u{7B}\\u{7B}"); + // Z3 transforms this into {}, but CVC4 does not! CVC4 is on the side of the SMTLIB2 standard as + // far as i can see. + StringFormula curlys2BUnicodeWOEscape = smgr.makeString("\\u7B\\u7D"); + + IntegerFormula zero = imgr.makeNumber(0); + + assertEqual(smgr.indexOf(empty, empty, zero), zero); + assertEqual(smgr.indexOf(a, empty, zero), zero); + assertEqual(smgr.indexOf(a, a, zero), zero); + assertEqual(smgr.indexOf(a, aUppercase, zero), imgr.makeNumber(-1)); + assertEqual(smgr.indexOf(abbbbbb, a, zero), zero); + assertEqual(smgr.indexOf(abbbbbb, b, zero), imgr.makeNumber(1)); + assertEqual(smgr.indexOf(abbbbbb, ab, zero), zero); + assertEqual(smgr.indexOf(abbbbbb, bbbbbb, zero), imgr.makeNumber(1)); + assertEqual(smgr.indexOf(abbbbbb, bbbbbbb, zero), imgr.makeNumber(-1)); + assertEqual(smgr.indexOf(abbbbbb, smgr.makeString("c"), zero), imgr.makeNumber(-1)); + assertEqual(smgr.indexOf(abcAndSoOn, smgr.makeString("z"), zero), imgr.makeNumber(25)); + assertEqual(smgr.indexOf(abcAndSoOn, smgr.makeString("V"), zero), imgr.makeNumber(21)); + assertEqual(smgr.indexOf(abcAndSoOn, smgr.makeString("v"), zero), imgr.makeNumber(-1)); + assertEqual(smgr.indexOf(multipleCurlys2BUnicode, curlyOpen2BUnicode, zero), zero); + assertEqual( + smgr.indexOf(multipleCurlys2BUnicode, curlyClose2BUnicode, zero), imgr.makeNumber(1)); + + // TODO: Z3 and CVC4 handle this differently! + // assertEqual(smgr.indexOf(multipleCurlys2BUnicode, curlys2BUnicodeWOEscape, zero), zero); + + assertEqual( + smgr.indexOf(multipleCurlys2BUnicode, curlys2BUnicodeWOEscape, imgr.makeNumber(1)), + imgr.makeNumber(-1)); + assertEqual( + smgr.indexOf(multipleCurlys2BUnicode, smgr.makeString("B"), zero), imgr.makeNumber(-1)); + } + + @Test + public void testStringVariableIndexOf() throws SolverException, InterruptedException { + StringFormula var1 = smgr.makeVariable("var1"); + StringFormula var2 = smgr.makeVariable("var2"); + IntegerFormula intVar = imgr.makeVariable("intVar"); + + StringFormula empty = smgr.makeString(""); + StringFormula curlyOpen2BUnicode = smgr.makeString("\\u{7B}"); + + IntegerFormula zero = imgr.makeNumber(0); + + // If the index of var2 is not -1, it is contained in var1. + assertThatFormula( + bmgr.and( + bmgr.not(imgr.equal(intVar, imgr.makeNumber(-1))), + imgr.equal(intVar, smgr.indexOf(var1, var2, zero)))) + .implies(smgr.contains(var1, var2)); + + // If the index is less than 0 (only -1 possible) it is not contained. + assertThatFormula( + bmgr.and( + imgr.equal(intVar, smgr.indexOf(var1, var2, zero)), imgr.lessThan(intVar, zero))) + .implies(bmgr.not(smgr.contains(var1, var2))); + + // If the index of var2 in var is >= 0 and vice versa, both contain each other. + assertThatFormula( + bmgr.and( + imgr.greaterOrEquals(smgr.indexOf(var1, var2, zero), zero), + imgr.greaterOrEquals(smgr.indexOf(var2, var1, zero), zero))) + .implies(bmgr.and(smgr.contains(var1, var2), smgr.contains(var2, var1))); + + // If the are indices equal and one is >= 0 and the strings are not "", both are contained in + // each other and the chars at the position must be the same. + assertThatFormula( + bmgr.and( + imgr.equal(smgr.indexOf(var1, var2, zero), smgr.indexOf(var2, var1, zero)), + imgr.greaterOrEquals(smgr.indexOf(var1, var2, zero), zero), + bmgr.not(smgr.equal(empty, smgr.charAt(var1, smgr.indexOf(var1, var2, zero)))))) + .implies( + bmgr.and( + smgr.contains(var1, var2), + smgr.contains(var2, var1), + smgr.equal( + smgr.charAt(var1, smgr.indexOf(var2, var1, zero)), + smgr.charAt(var1, smgr.indexOf(var1, var2, zero))))); + + // If a String contains {, but not B, the index of B must be -1. (unicode of { contains B) + assertThatFormula( + bmgr.and( + smgr.contains(var1, curlyOpen2BUnicode), + bmgr.not(smgr.contains(var1, smgr.makeString("B"))))) + .implies( + bmgr.and( + imgr.greaterOrEquals(smgr.indexOf(var1, curlyOpen2BUnicode, zero), zero), + imgr.equal(imgr.makeNumber(-1), smgr.indexOf(var1, smgr.makeString("B"), zero)))); + } + + @Test + public void testStringIndexOfWithSubStrings() throws SolverException, InterruptedException { + assume() + .withMessage("Solver %s runs endlessly on this task", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.Z3); + + StringFormula var1 = smgr.makeVariable("var1"); + + IntegerFormula zero = imgr.makeNumber(0); + + // If the index of the string abba is 0, the index of the string bba is 1, and b is 1, and ba is + // 2 + assertThatFormula(imgr.equal(zero, smgr.indexOf(var1, smgr.makeString("abba"), zero))) + .implies( + bmgr.and( + smgr.contains(var1, smgr.makeString("abba")), + imgr.equal(imgr.makeNumber(1), smgr.indexOf(var1, smgr.makeString("bba"), zero)), + imgr.equal(imgr.makeNumber(1), smgr.indexOf(var1, smgr.makeString("b"), zero)), + imgr.equal(imgr.makeNumber(2), smgr.indexOf(var1, smgr.makeString("ba"), zero)))); + } + + @Test + public void testStringPrefixImpliesPrefixIndexOf() throws SolverException, InterruptedException { + assume() + .withMessage("Solver %s runs endlessly on this task", solverToUse()) + .that(solverToUse()) + .isNoneOf(Solvers.Z3, Solvers.CVC4); + + StringFormula var1 = smgr.makeVariable("var1"); + StringFormula var2 = smgr.makeVariable("var2"); + + IntegerFormula zero = imgr.makeNumber(0); + + // If a prefix (var2) is non empty, the length of the string (var1) has to be larger or equal to + // the prefix + // and the chars have to be the same for the lenth of the prefix, meaning the indexOf the prefix + // must be 0 in the string. + assertThatFormula(bmgr.and(imgr.greaterThan(smgr.length(var2), zero), smgr.prefix(var2, var1))) + .implies( + bmgr.and( + smgr.contains(var1, var2), + imgr.greaterOrEquals(smgr.length(var1), smgr.length(var2)), + imgr.equal(zero, smgr.indexOf(var1, var2, zero)))); + } + + @Test + public void testConstStringSubStrings() throws SolverException, InterruptedException { + StringFormula empty = smgr.makeString(""); + StringFormula a = smgr.makeString("a"); + StringFormula aUppercase = smgr.makeString("A"); + StringFormula bUppercase = smgr.makeString("B"); + StringFormula bbbbbb = smgr.makeString("bbbbbb"); + StringFormula curlyOpen2BUnicode = smgr.makeString("\\u{7B}"); + StringFormula curlyClose2BUnicode = smgr.makeString("\\u{7D}"); + StringFormula multipleCurlys2BUnicode = smgr.makeString("\\u{7B}\\u{7D}\\u{7B}\\u{7B}"); + + IntegerFormula zero = imgr.makeNumber(0); + IntegerFormula one = imgr.makeNumber(1); + + // Check empty string + assertEqual(smgr.substring(empty, zero, zero), empty); + // Check length 0 = empty string + assertEqual(smgr.substring(a, one, zero), empty); + // Check that it correctly recognized uppercase + assertDistinct(smgr.substring(a, zero, one), aUppercase); + assertDistinct(smgr.substring(aUppercase, zero, one), a); + assertDistinct(smgr.substring(bbbbbb, zero, one), bUppercase); + // Check smgr length interaction + assertEqual(smgr.substring(bbbbbb, zero, smgr.length(bbbbbb)), bbbbbb); + // Check unicode substrings + assertEqual(smgr.substring(multipleCurlys2BUnicode, zero, one), curlyOpen2BUnicode); + assertEqual(smgr.substring(multipleCurlys2BUnicode, one, one), curlyClose2BUnicode); + } + + @Test + public void testConstStringAllPossibleSubStrings() throws SolverException, InterruptedException { + for (String wordString : WORDS) { + StringFormula word = smgr.makeString(wordString); + + for (int j = 0; j < wordString.length(); j++) { + for (int k = j; k < wordString.length(); k++) { + // Loop through all combinations of substrings + // Note: String.substring uses begin index and end index (non-including) while SMT based + // substring uses length! + // Length = endIndex - beginIndex + String wordSubString = wordString.substring(j, k); + assertEqual( + smgr.substring(word, imgr.makeNumber(j), imgr.makeNumber(k - j)), + smgr.makeString(wordSubString)); + } + } + } + } + + @Test + public void testStringSubstringOutOfBounds() throws SolverException, InterruptedException { + StringFormula bbbbbb = smgr.makeString("bbbbbb"); + StringFormula b = smgr.makeString("b"); + StringFormula abbbbbb = smgr.makeString("abbbbbb"); + + StringFormula multipleCurlys2BUnicode = smgr.makeString("\\u{7B}\\u{7D}\\u{7B}\\u{7B}"); + StringFormula multipleCurlys2BUnicodeFromIndex1 = smgr.makeString("\\u{7D}\\u{7B}\\u{7B}"); + + assertEqual(smgr.substring(abbbbbb, imgr.makeNumber(0), imgr.makeNumber(10000)), abbbbbb); + assertEqual(smgr.substring(abbbbbb, imgr.makeNumber(6), imgr.makeNumber(10000)), b); + assertEqual(smgr.substring(abbbbbb, imgr.makeNumber(1), imgr.makeNumber(10000)), bbbbbb); + assertEqual( + smgr.substring(multipleCurlys2BUnicode, imgr.makeNumber(1), imgr.makeNumber(10000)), + multipleCurlys2BUnicodeFromIndex1); + } + + @Test + public void testStringVariablesSubstring() throws SolverException, InterruptedException { + StringFormula var1 = smgr.makeVariable("var1"); + StringFormula var2 = smgr.makeVariable("var2"); + IntegerFormula intVar1 = imgr.makeVariable("intVar1"); + IntegerFormula intVar2 = imgr.makeVariable("intVar2"); + + // If a Prefix of a certain length exists, the substring over that equals the prefix + assertThatFormula(smgr.prefix(var2, var1)) + .implies(smgr.equal(var2, smgr.substring(var1, imgr.makeNumber(0), smgr.length(var2)))); + + // Same with suffix + assertThatFormula(smgr.suffix(var2, var1)) + .implies( + smgr.equal( + var2, + smgr.substring( + var1, imgr.subtract(smgr.length(var1), smgr.length(var2)), smgr.length(var2)))); + + // If a string has a char at a specified position, a substring beginning with the same index + // must have the same char, independent of the length of the substring. + // But its not really relevant to check out of bounds cases, hence the exclusion. + // So we test substring length 1 (== charAt) and larger + assertThatFormula( + bmgr.and( + imgr.greaterThan(intVar2, imgr.makeNumber(1)), + smgr.equal(var2, smgr.charAt(var1, intVar1)), + imgr.greaterThan(smgr.length(var1), intVar1))) + .implies( + smgr.equal( + var2, smgr.charAt(smgr.substring(var1, intVar1, intVar2), imgr.makeNumber(0)))); + + assertThatFormula(smgr.equal(var2, smgr.charAt(var1, intVar1))) + .implies(smgr.equal(var2, smgr.substring(var1, intVar1, imgr.makeNumber(1)))); + } + + @Test + public void testConstStringReplace() throws SolverException, InterruptedException { + for (int i = 0; i < WORDS.size(); i++) { + for (int j = 2; j < WORDS.size(); j++) { + String word1 = WORDS.get(j - 1); + String word2 = WORDS.get(j); + String word3 = WORDS.get(i); + StringFormula word1F = smgr.makeString(word1); + StringFormula word2F = smgr.makeString(word2); + StringFormula word3F = smgr.makeString(word3); + + StringFormula result = smgr.makeString(word3.replaceFirst(word2, word1)); + assertEqual(smgr.replace(word3F, word2F, word1F), result); + } + } + } + + // Neither CVC4 nor Z3 can solve this! + @Ignore + @Test + public void testStringVariableReplacePrefix() throws SolverException, InterruptedException { + StringFormula var1 = smgr.makeVariable("var1"); + StringFormula var2 = smgr.makeVariable("var2"); + StringFormula var3 = smgr.makeVariable("var3"); + StringFormula prefix = smgr.makeVariable("prefix"); + + // If var1 has a prefix, and you replace said prefix with var3 (saved in var2), the prefix of + // var2 is var3 + assertThatFormula( + bmgr.and( + smgr.equal(var2, smgr.replace(var1, prefix, var3)), + smgr.prefix(prefix, var1), + bmgr.not(smgr.equal(prefix, var3)), + imgr.greaterThan(smgr.length(prefix), imgr.makeNumber(0)), + imgr.greaterThan(smgr.length(var3), imgr.makeNumber(0)))) + .implies(bmgr.and(bmgr.not(smgr.equal(var1, var2)), smgr.prefix(var3, var2))); + assertThatFormula( + bmgr.and( + smgr.equal(var2, smgr.replace(var1, prefix, var3)), + smgr.prefix(prefix, var1), + bmgr.not(smgr.equal(prefix, var3)))) + .implies(bmgr.and(smgr.prefix(var3, var2), bmgr.not(smgr.equal(var1, var2)))); + } + + @Test + public void testStringVariableReplaceSubstring() throws SolverException, InterruptedException { + // I couldn't find stronger constraints in the implication that don't run endlessly..... + StringFormula original = smgr.makeVariable("original"); + StringFormula prefix = smgr.makeVariable("prefix"); + StringFormula replacement = smgr.makeVariable("replacement"); + StringFormula replaced = smgr.makeVariable("replaced"); + + // Set a prefix that does not contain the suffix substring, make sure that the substring that + // comes after the prefix is replaced + assertThatFormula( + bmgr.and( + smgr.prefix(prefix, original), + imgr.equal( + smgr.length(prefix), + smgr.indexOf( + original, + smgr.substring(original, smgr.length(prefix), smgr.length(original)), + imgr.makeNumber(0))), + imgr.greaterThan(smgr.length(original), smgr.length(prefix)), + imgr.greaterThan(smgr.length(prefix), imgr.makeNumber(0)), + imgr.greaterThan( + smgr.length( + smgr.substring(original, smgr.length(prefix), smgr.length(original))), + imgr.makeNumber(0)), + smgr.equal( + replaced, + smgr.replace( + original, + smgr.substring(original, smgr.length(prefix), smgr.length(original)), + replacement)))) + .implies( + smgr.equal( + replacement, smgr.substring(replaced, smgr.length(prefix), smgr.length(replaced)))); + + // In this version it is still possible that parts of the prefix and suffix together build the + // suffix, replacing parts of the prefix additionally to the implication above (or the + // replacement is empty) + assertThatFormula( + bmgr.and( + smgr.prefix(prefix, original), + bmgr.not(smgr.contains(original, replacement)), + bmgr.not( + smgr.contains( + smgr.substring(original, smgr.length(prefix), smgr.length(original)), + prefix)), + bmgr.not( + smgr.contains( + prefix, + smgr.substring(original, smgr.length(prefix), smgr.length(original)))), + imgr.greaterThan(smgr.length(original), smgr.length(prefix)), + imgr.greaterThan(smgr.length(prefix), imgr.makeNumber(0)), + smgr.equal( + replaced, + smgr.replace( + original, + smgr.substring(original, smgr.length(prefix), smgr.length(original)), + replacement)))) + .implies(smgr.contains(replacement, replacement)); + + // This version may have the original as a larger version of the prefix; prefix: a, original: + // aaa + assertThatFormula( + bmgr.and( + smgr.prefix(prefix, original), + bmgr.not(smgr.contains(original, replacement)), + bmgr.not( + smgr.contains( + prefix, + smgr.substring(original, smgr.length(prefix), smgr.length(original)))), + imgr.greaterThan(smgr.length(original), smgr.length(prefix)), + imgr.greaterThan(smgr.length(prefix), imgr.makeNumber(0)), + smgr.equal( + replaced, + smgr.replace( + original, + smgr.substring(original, smgr.length(prefix), smgr.length(original)), + replacement)))) + .implies(smgr.contains(replacement, replacement)); + + // This version can contain the substring in the prefix! + assertThatFormula( + bmgr.and( + smgr.prefix(prefix, original), + bmgr.not(smgr.contains(original, replacement)), + imgr.greaterThan(smgr.length(original), smgr.length(prefix)), + imgr.greaterThan(smgr.length(prefix), imgr.makeNumber(0)), + smgr.equal( + replaced, + smgr.replace( + original, + smgr.substring(original, smgr.length(prefix), smgr.length(original)), + replacement)))) + .implies(smgr.contains(replacement, replacement)); + } + + @Test + public void testStringVariableReplaceMiddle() throws SolverException, InterruptedException { + // TODO: either rework that this terminates, or remove + assume() + .withMessage("Solver %s runs endlessly on this task.", solverToUse()) + .that(solverToUse()) + .isNoneOf(Solvers.CVC4, Solvers.Z3); + + StringFormula original = smgr.makeVariable("original"); + StringFormula replacement = smgr.makeVariable("replacement"); + StringFormula replaced = smgr.makeVariable("replaced"); + StringFormula beginning = smgr.makeVariable("beginning"); + StringFormula middle = smgr.makeVariable("middle"); + StringFormula end = smgr.makeVariable("end"); + + // If beginning + middle + end (length of each > 0) get concated (in original), replacing + // beginning/middle/end + // with replacement (result = replaces; replacement > 0 and != the replaced) results in a + // string that is equal to the concat of the 2 remaining start strings and the replaced one + // replaced + // This is tested with 2 different implications, 1 that only checks wheter or not the + // replacement is contained in the string and not in the original and vice verse for the + // replaced String + BooleanFormula formula = + bmgr.and( + smgr.equal(original, smgr.concat(beginning, middle, end)), + smgr.equal(replaced, smgr.replace(original, middle, replacement)), + bmgr.not(smgr.equal(middle, replacement)), + bmgr.not(smgr.equal(beginning, replacement)), + bmgr.not(smgr.equal(end, replacement)), + bmgr.not(smgr.equal(beginning, middle)), + imgr.greaterThan(smgr.length(middle), imgr.makeNumber(0)), + imgr.greaterThan(smgr.length(replacement), imgr.makeNumber(0)), + imgr.greaterThan(smgr.length(beginning), imgr.makeNumber(0))); + assertThatFormula(formula) + .implies( + bmgr.and( + bmgr.not(smgr.equal(original, replaced)), smgr.contains(replaced, replacement))); + + // Same as above, but with concat instead of contains + assertThatFormula(formula) + .implies( + bmgr.and( + bmgr.not(smgr.equal(original, replaced)), + smgr.equal(replaced, smgr.concat(beginning, replacement, end)))); + } + + @Test + public void testStringVariableReplaceFront() throws SolverException, InterruptedException { + assume() + .withMessage("Solver %s runs endlessly on this task.", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.Z3); + + StringFormula var1 = smgr.makeVariable("var1"); + StringFormula var2 = smgr.makeVariable("var2"); + StringFormula var3 = smgr.makeVariable("var3"); + StringFormula var4 = smgr.makeVariable("var4"); + StringFormula var5 = smgr.makeVariable("var5"); + + // If var1 and 2 get concated (in var4) such that var1 is in front, replacing var1 with var3 + // (var5) results in a + // string that is equal to var3 + var2 + // First with length constraints, second without + assertThatFormula( + bmgr.and( + smgr.equal(var4, smgr.concat(var1, var2)), + smgr.equal(var5, smgr.replace(var4, var1, var3)), + bmgr.not(smgr.equal(var1, var3)), + imgr.greaterThan(smgr.length(var1), imgr.makeNumber(0)), + imgr.greaterThan(smgr.length(var3), imgr.makeNumber(0)))) + .implies(bmgr.and(bmgr.not(smgr.equal(var4, var5)), smgr.prefix(var3, var5))); + + assertThatFormula( + bmgr.and( + smgr.equal(var4, smgr.concat(var1, var2)), + smgr.equal(var5, smgr.replace(var4, var1, var3)), + bmgr.not(smgr.equal(var1, var3)))) + .implies(bmgr.and(bmgr.not(smgr.equal(var4, var5)), smgr.prefix(var3, var5))); + } + + @Test + public void testConstStringReplaceAll() throws SolverException, InterruptedException { + assume() + .withMessage("Solver %s does not support replaceAll()", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.Z3); + + for (int i = 0; i < WORDS.size(); i++) { + for (int j = 1; j < WORDS.size(); j++) { + String word1 = WORDS.get(i); + String word2 = WORDS.get(j); + String word3 = "replacement"; + StringFormula word1F = smgr.makeString(word1); + StringFormula word2F = smgr.makeString(word2); + StringFormula word3F = smgr.makeString(word3); + + StringFormula result = smgr.makeString(word3.replaceAll(word2, word1)); + assertEqual(smgr.replaceAll(word3F, word2F, word1F), result); + } + } + } + + /** + * Concat a String that consists of a String that is later replaces with replaceAll. The resulting + * String should consist of only concatinated versions of itself. + */ + @Test + public void testStringVariableReplaceAllConcatedString() + throws SolverException, InterruptedException { + assume() + .withMessage("Solver %s does not support replaceAll()", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.Z3); + + // 2 concats is the max number CVC4 supports without running endlessly + for (int numOfConcats = 0; numOfConcats < 3; numOfConcats++) { + + StringFormula original = smgr.makeVariable("original"); + StringFormula replacement = smgr.makeVariable("replacement"); + StringFormula replaced = smgr.makeVariable("replaced"); + StringFormula segment = smgr.makeVariable("segment"); + + StringFormula[] concatSegments = new StringFormula[numOfConcats]; + StringFormula[] concatReplacements = new StringFormula[numOfConcats]; + + for (int i = 0; i < numOfConcats; i++) { + concatSegments[i] = segment; + concatReplacements[i] = replacement; + } + + BooleanFormula formula = + bmgr.and( + smgr.equal(original, smgr.concat(concatSegments)), + smgr.equal(replaced, smgr.replaceAll(original, segment, replacement)), + bmgr.not(smgr.equal(segment, replacement)), + imgr.greaterThan(smgr.length(segment), imgr.makeNumber(0)), + imgr.greaterThan(smgr.length(replacement), imgr.makeNumber(0))); + assertThatFormula(formula).implies(smgr.equal(replaced, smgr.concat(concatReplacements))); + } + } + + @Test + public void testStringVariableReplaceAllSubstring() throws SolverException, InterruptedException { + assume() + .withMessage("Solver %s does not support replaceAll()", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.Z3); + + // I couldn't find stronger constraints in the implication that don't run endlessly..... + StringFormula original = smgr.makeVariable("original"); + StringFormula prefix = smgr.makeVariable("prefix"); + StringFormula replacement = smgr.makeVariable("replacement"); + StringFormula replaced = smgr.makeVariable("replaced"); + + // Set a prefix that does not contain the suffix substring, make sure that the substring that + // comes after the prefix is replaced + assertThatFormula( + bmgr.and( + smgr.prefix(prefix, original), + imgr.equal( + smgr.length(prefix), + smgr.indexOf( + original, + smgr.substring(original, smgr.length(prefix), smgr.length(original)), + imgr.makeNumber(0))), + imgr.greaterThan(smgr.length(original), smgr.length(prefix)), + imgr.greaterThan(smgr.length(prefix), imgr.makeNumber(0)), + imgr.greaterThan( + smgr.length( + smgr.substring(original, smgr.length(prefix), smgr.length(original))), + imgr.makeNumber(0)), + smgr.equal( + replaced, + smgr.replaceAll( + original, + smgr.substring(original, smgr.length(prefix), smgr.length(original)), + replacement)))) + .implies( + smgr.equal( + replacement, smgr.substring(replaced, smgr.length(prefix), smgr.length(replaced)))); + } + + @Test + public void testStringConcatWUnicode() throws SolverException, InterruptedException { + StringFormula backslash = smgr.makeString("\\"); + StringFormula u = smgr.makeString("u"); + StringFormula curlyOpen = smgr.makeString("\\u{7B}"); + StringFormula sevenB = smgr.makeString("7B"); + StringFormula curlyClose = smgr.makeString("\\u{7D}"); + StringFormula concat = smgr.concat(backslash, u, curlyOpen, sevenB, curlyClose); + StringFormula complete = smgr.makeString("\\u{7B}"); + + // Concatting parts of unicode does not result in the unicode char! + assertDistinct(concat, complete); + } + + @Test + public void testStringSimpleRegex() { + // TODO + } +} diff --git a/src/org/sosy_lab/java_smt/utils/UfElimination.java b/src/org/sosy_lab/java_smt/utils/UfElimination.java index 10ffd4a475..d417ff4c31 100644 --- a/src/org/sosy_lab/java_smt/utils/UfElimination.java +++ b/src/org/sosy_lab/java_smt/utils/UfElimination.java @@ -42,6 +42,7 @@ import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.QuantifiedFormulaManager; import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier; +import org.sosy_lab.java_smt.api.StringFormula; import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor; import org.sosy_lab.java_smt.api.visitors.TraversalProcess; @@ -210,6 +211,8 @@ private BooleanFormula makeEqual(Formula pLhs, Formula pRhs) { t = bfmgr.equivalence((BooleanFormula) pLhs, (BooleanFormula) pRhs); } else if (pLhs instanceof IntegerFormula && pRhs instanceof IntegerFormula) { t = fmgr.getIntegerFormulaManager().equal((IntegerFormula) pLhs, (IntegerFormula) pRhs); + } else if (pLhs instanceof StringFormula && pRhs instanceof StringFormula) { + t = fmgr.getStringFormulaManager().equal((StringFormula) pLhs, (StringFormula) pRhs); } else if (pLhs instanceof NumeralFormula && pRhs instanceof NumeralFormula) { t = fmgr.getRationalFormulaManager().equal((NumeralFormula) pLhs, (NumeralFormula) pRhs); } else if (pLhs instanceof BitvectorFormula) {