diff --git a/.classpath b/.classpath index 52a207f1a7..f3b9323db7 100644 --- a/.classpath +++ b/.classpath @@ -28,6 +28,10 @@ SPDX-License-Identifier: Apache-2.0 + + + + diff --git a/.idea/JavaSMT.iml b/.idea/JavaSMT.iml index c9ee959dbd..b34b14fbca 100644 --- a/.idea/JavaSMT.iml +++ b/.idea/JavaSMT.iml @@ -322,6 +322,24 @@ SPDX-License-Identifier: Apache-2.0 + + + + + + + + + + + + + + + + + + diff --git a/lib/ivy.xml b/lib/ivy.xml index 701c0cf037..91989dfdcc 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -96,7 +96,8 @@ SPDX-License-Identifier: Apache-2.0 + Library for auto-generating value types. --> + @@ -146,10 +147,17 @@ SPDX-License-Identifier: Apache-2.0 - - - - + + + + + + + diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractBaseFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractBaseFormulaManager.java index ad8a650b5a..4890fb6a61 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractBaseFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractBaseFormulaManager.java @@ -30,7 +30,7 @@ protected final FormulaCreator getFormulaC return formulaCreator; } - final TFormulaInfo extractInfo(Formula pBits) { + protected final TFormulaInfo extractInfo(Formula pBits) { return getFormulaCreator().extractInfo(pBits); } diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java index 713e3df143..67618e392a 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java @@ -32,11 +32,11 @@ protected AbstractStringFormulaManager( super(pCreator); } - private StringFormula wrapString(TFormulaInfo formulaInfo) { + protected StringFormula wrapString(TFormulaInfo formulaInfo) { return getFormulaCreator().encapsulateString(formulaInfo); } - private RegexFormula wrapRegex(TFormulaInfo formulaInfo) { + protected RegexFormula wrapRegex(TFormulaInfo formulaInfo) { return getFormulaCreator().encapsulateRegex(formulaInfo); } diff --git a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java index 6259f33b4a..e5dd09e4ad 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java @@ -137,43 +137,59 @@ public final TType getRegexType() { public abstract TFormulaInfo makeVariable(TType type, String varName); public BooleanFormula encapsulateBoolean(TFormulaInfo pTerm) { - assert getFormulaType(pTerm).isBooleanType(); + checkArgument( + getFormulaType(pTerm).isBooleanType(), + "Boolean formula has unexpected type: %s", + getFormulaType(pTerm)); return new BooleanFormulaImpl<>(pTerm); } protected BitvectorFormula encapsulateBitvector(TFormulaInfo pTerm) { - assert getFormulaType(pTerm).isBitvectorType(); + checkArgument( + getFormulaType(pTerm).isBitvectorType(), + "Bitvector formula has unexpected type: %s", + getFormulaType(pTerm)); return new BitvectorFormulaImpl<>(pTerm); } protected FloatingPointFormula encapsulateFloatingPoint(TFormulaInfo pTerm) { - assert getFormulaType(pTerm).isFloatingPointType(); + checkArgument( + getFormulaType(pTerm).isFloatingPointType(), + "Floatingpoint formula has unexpected type: %s", + getFormulaType(pTerm)); return new FloatingPointFormulaImpl<>(pTerm); } protected ArrayFormula encapsulateArray( TFormulaInfo pTerm, FormulaType pIndexType, FormulaType pElementType) { - assert getFormulaType(pTerm).equals(FormulaType.getArrayType(pIndexType, pElementType)) - : "Expected: " - + getFormulaType(pTerm) - + " but found: " - + FormulaType.getArrayType(pIndexType, pElementType); - + checkArgument( + getFormulaType(pTerm).equals(FormulaType.getArrayType(pIndexType, pElementType)), + "Array formula has unexpected type: %s", + getFormulaType(pTerm)); return new ArrayFormulaImpl<>(pTerm, pIndexType, pElementType); } protected StringFormula encapsulateString(TFormulaInfo pTerm) { - assert getFormulaType(pTerm).isStringType(); + checkArgument( + getFormulaType(pTerm).isStringType(), + "String formula has unexpected type: %s", + getFormulaType(pTerm)); return new StringFormulaImpl<>(pTerm); } protected RegexFormula encapsulateRegex(TFormulaInfo pTerm) { - assert getFormulaType(pTerm).isRegexType(); + checkArgument( + getFormulaType(pTerm).isRegexType(), + "Regex formula has unexpected type: %s", + getFormulaType(pTerm)); return new RegexFormulaImpl<>(pTerm); } protected EnumerationFormula encapsulateEnumeration(TFormulaInfo pTerm) { - assert getFormulaType(pTerm).isEnumerationType(); + checkArgument( + getFormulaType(pTerm).isEnumerationType(), + "Enumeration formula has unexpected type: %s", + getFormulaType(pTerm)); return new EnumerationFormulaImpl<>(pTerm); } @@ -183,10 +199,12 @@ public Formula encapsulateWithTypeOf(TFormulaInfo pTerm) { @SuppressWarnings("unchecked") public T encapsulate(FormulaType pType, TFormulaInfo pTerm) { - assert pType.equals(getFormulaType(pTerm)) - : String.format( - "Trying to encapsulate formula %s of type %s as %s", - pTerm, getFormulaType(pTerm), pType); + checkArgument( + pType.equals(getFormulaType(pTerm)), + "Trying to encapsulate formula %s of type %s as %s", + pTerm, + getFormulaType(pTerm), + pType); if (pType.isBooleanType()) { return (T) new BooleanFormulaImpl<>(pTerm); } else if (pType.isIntegerType()) { diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java index 27304bfd40..445012d20d 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -21,7 +21,9 @@ import ap.parser.IFunApp; import ap.parser.IFunction; import ap.parser.IIntFormula; +import ap.parser.IPlus; import ap.parser.ITerm; +import ap.parser.ITimes; import ap.parser.Parser2InputAbsy.TranslationException; import ap.parser.PartialEvaluator; import ap.parser.SMTLineariser; @@ -30,8 +32,10 @@ import ap.terfor.ConstantTerm; import ap.terfor.preds.Predicate; import ap.theories.ExtArray; +import ap.theories.ExtArray.ArraySort; import ap.theories.bitvectors.ModuloArithmetic; -import ap.theories.rationals.Fractions.FractionSort$; +import ap.theories.rationals.Rationals$; +import ap.theories.strings.StringTheory; import ap.types.Sort; import ap.types.Sort$; import ap.types.Sort.MultipleValueBool$; @@ -50,6 +54,7 @@ import java.nio.file.Path; import java.util.ArrayDeque; import java.util.ArrayList; +import java.util.Arrays; import java.util.Deque; import java.util.HashMap; import java.util.HashSet; @@ -60,6 +65,7 @@ import java.util.Optional; import java.util.Set; import java.util.TreeMap; +import java.util.stream.Collectors; import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.Appender; import org.sosy_lab.common.Appenders; @@ -72,6 +78,8 @@ import org.sosy_lab.common.io.PathCounterTemplate; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; +import ostrich.OFlags; +import ostrich.OstrichStringTheory; import scala.Tuple2; import scala.Tuple4; import scala.collection.immutable.Seq; @@ -101,6 +109,29 @@ class PrincessEnvironment { public static final Sort BOOL_SORT = Sort$.MODULE$.Bool(); public static final Sort INTEGER_SORT = Sort.Integer$.MODULE$; + public static final Sort NAT_SORT = Sort.Nat$.MODULE$; + + static final StringTheory stringTheory = + new OstrichStringTheory( + toSeq(new ArrayList<>()), + new OFlags( + OFlags.$lessinit$greater$default$1(), + OFlags.$lessinit$greater$default$2(), + OFlags.$lessinit$greater$default$3(), + OFlags.$lessinit$greater$default$4(), + OFlags.$lessinit$greater$default$5(), + OFlags.$lessinit$greater$default$6(), + OFlags.$lessinit$greater$default$7(), + OFlags.$lessinit$greater$default$8(), + OFlags.$lessinit$greater$default$9(), + OFlags.$lessinit$greater$default$10(), + OFlags.$lessinit$greater$default$11(), + OFlags.$lessinit$greater$default$12())); + public static final Sort STRING_SORT = stringTheory.StringSort(); + public static final Sort REGEX_SORT = stringTheory.RegexSort(); + + static Rationals$ rationalTheory = Rationals$.MODULE$; + public static final Sort FRACTION_SORT = rationalTheory.dom(); @Option(secure = true, description = "log all queries as Princess-specific Scala code") private boolean logAllQueriesAsScala = false; @@ -509,14 +540,23 @@ static FormulaType getFormulaType(IExpression pFormula) { if (pFormula instanceof IFormula) { return FormulaType.BooleanType; } else if (pFormula instanceof ITerm) { - final Sort sort = Sort$.MODULE$.sortOf((ITerm) pFormula); + ITerm formula = (ITerm) pFormula; + if (pFormula instanceof ITimes) { + // coeff is always INT, lets check the subterm. + formula = ((ITimes) formula).subterm(); + } else if (pFormula instanceof IPlus) { + return mergeFormulaTypes( + getFormulaType(((IPlus) pFormula).t1()), getFormulaType(((IPlus) pFormula).t2())); + } + final Sort sort = Sort$.MODULE$.sortOf(formula); try { return getFormulaTypeFromSort(sort); } catch (IllegalArgumentException e) { // add more info about the formula, then rethrow throw new IllegalArgumentException( String.format( - "Unknown formula type '%s' for formula '%s'.", pFormula.getClass(), pFormula), + "Unknown formula type '%s' of sort '%s' for formula '%s'.", + pFormula.getClass(), sort.toString(), pFormula), e); } } @@ -525,15 +565,38 @@ static FormulaType getFormulaType(IExpression pFormula) { "Unknown formula type '%s' for formula '%s'.", pFormula.getClass(), pFormula)); } + /** + * Merge INTEGER and RATIONAL type or INTEGER and BITVECTOR and return the more general type. The + * ordering is: RATIONAL > INTEGER > BITVECTOR. + * + * @throws IllegalArgumentException for any other type. + */ + private static FormulaType mergeFormulaTypes(FormulaType type1, FormulaType type2) { + if ((type1.isIntegerType() || type1.isRationalType()) + && (type2.isIntegerType() || type2.isRationalType())) { + return type1.isRationalType() ? type1 : type2; + } + if ((type1.isIntegerType() || type1.isBitvectorType()) + && (type2.isIntegerType() || type2.isBitvectorType())) { + return type1.isIntegerType() ? type1 : type2; + } + throw new IllegalArgumentException( + String.format("Types %s and %s can not be merged.", type1, type2)); + } + private static FormulaType getFormulaTypeFromSort(final Sort sort) { if (sort == PrincessEnvironment.BOOL_SORT) { return FormulaType.BooleanType; - } else if (sort == PrincessEnvironment.INTEGER_SORT) { + } else if (sort == PrincessEnvironment.INTEGER_SORT || sort == PrincessEnvironment.NAT_SORT) { return FormulaType.IntegerType; - } else if (sort instanceof FractionSort$) { + } else if (sort == PrincessEnvironment.FRACTION_SORT) { return FormulaType.RationalType; + } else if (sort == PrincessEnvironment.STRING_SORT) { + return FormulaType.StringType; + } else if (sort == PrincessEnvironment.REGEX_SORT) { + return FormulaType.RegexType; } else if (sort instanceof ExtArray.ArraySort) { - Seq indexSorts = ((ExtArray.ArraySort) sort).theory().indexSorts(); + Seq indexSorts = ((ArraySort) sort).theory().indexSorts(); Sort elementSort = ((ExtArray.ArraySort) sort).theory().objSort(); assert indexSorts.iterator().size() == 1 : "unexpected index type in Array type:" + sort; // assert indexSorts.size() == 1; // TODO Eclipse does not like simpler code. @@ -643,6 +706,15 @@ static Seq toSeq(List list) { return collectionAsScalaIterableConverter(list).asScala().toSeq(); } + static Seq toITermSeq(List exprs) { + return PrincessEnvironment.toSeq( + exprs.stream().map(e -> (ITerm) e).collect(Collectors.toList())); + } + + static Seq toITermSeq(IExpression... exprs) { + return toITermSeq(Arrays.asList(exprs)); + } + IExpression simplify(IExpression f) { // TODO this method is not tested, check it! if (f instanceof IFormula) { diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java index 1c12854863..91e34a7340 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -12,7 +12,7 @@ import static org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier.EXISTS; import static org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier.FORALL; import static org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.toSeq; -import static scala.collection.JavaConverters.asJava; +import static scala.collection.JavaConverters.asJavaCollection; import ap.basetypes.IdealInt; import ap.parser.IAtom; @@ -44,13 +44,17 @@ import ap.theories.nia.GroebnerMultiplication$; import ap.types.Sort; import ap.types.Sort$; +import com.google.common.base.Preconditions; import com.google.common.collect.HashBasedTable; import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableSet; import com.google.common.collect.Table; import java.util.ArrayList; import java.util.HashMap; import java.util.List; import java.util.Map; +import java.util.Set; +import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.api.ArrayFormula; import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -76,6 +80,8 @@ class PrincessFormulaCreator // Java-SMT kind private static final Map theoryFunctionKind = new HashMap<>(); private static final Map theoryPredKind = new HashMap<>(); + private static final Set CONSTANT_UFS = + ImmutableSet.of("str_cons", "str_empty", "Rat_int", "Rat_frac"); static { theoryFunctionKind.put(ModuloArithmetic.bv_concat(), FunctionDeclarationKind.BV_CONCAT); @@ -107,6 +113,56 @@ class PrincessFormulaCreator theoryPredKind.put(ModuloArithmetic.bv_sle(), FunctionDeclarationKind.BV_SLE); theoryFunctionKind.put(GroebnerMultiplication$.MODULE$.mul(), FunctionDeclarationKind.MUL); + + theoryFunctionKind.put( + PrincessEnvironment.stringTheory.str_$plus$plus(), FunctionDeclarationKind.STR_CONCAT); + theoryFunctionKind.put( + PrincessEnvironment.stringTheory.str_len(), FunctionDeclarationKind.STR_LENGTH); + theoryFunctionKind.put( + PrincessEnvironment.stringTheory.str_indexof(), FunctionDeclarationKind.STR_INDEX_OF); + theoryFunctionKind.put( + PrincessEnvironment.stringTheory.str_at(), FunctionDeclarationKind.STR_CHAR_AT); + theoryFunctionKind.put( + PrincessEnvironment.stringTheory.str_substr(), FunctionDeclarationKind.STR_SUBSTRING); + theoryFunctionKind.put( + PrincessEnvironment.stringTheory.str_replace(), FunctionDeclarationKind.STR_REPLACE); + theoryFunctionKind.put( + PrincessEnvironment.stringTheory.str_replaceall(), FunctionDeclarationKind.STR_REPLACE_ALL); + theoryFunctionKind.put( + PrincessEnvironment.stringTheory.str_to_re(), FunctionDeclarationKind.STR_TO_RE); + theoryFunctionKind.put( + PrincessEnvironment.stringTheory.str_to_int(), FunctionDeclarationKind.STR_TO_INT); + theoryFunctionKind.put( + PrincessEnvironment.stringTheory.re_range(), FunctionDeclarationKind.RE_RANGE); + theoryFunctionKind.put( + PrincessEnvironment.stringTheory.re_$plus$plus(), FunctionDeclarationKind.RE_CONCAT); + theoryFunctionKind.put( + PrincessEnvironment.stringTheory.re_union(), FunctionDeclarationKind.RE_UNION); + theoryFunctionKind.put( + PrincessEnvironment.stringTheory.re_inter(), FunctionDeclarationKind.RE_INTERSECT); + theoryFunctionKind.put( + PrincessEnvironment.stringTheory.re_$times(), FunctionDeclarationKind.RE_STAR); + theoryFunctionKind.put( + PrincessEnvironment.stringTheory.re_$plus(), FunctionDeclarationKind.RE_PLUS); + theoryFunctionKind.put( + PrincessEnvironment.stringTheory.re_diff(), FunctionDeclarationKind.RE_DIFFERENCE); + theoryFunctionKind.put( + PrincessEnvironment.stringTheory.re_opt(), FunctionDeclarationKind.RE_OPTIONAL); + theoryFunctionKind.put( + PrincessEnvironment.stringTheory.re_comp(), FunctionDeclarationKind.RE_COMPLEMENT); + theoryFunctionKind.put( + PrincessEnvironment.stringTheory.int_to_str(), FunctionDeclarationKind.INT_TO_STR); + + theoryPredKind.put( + PrincessEnvironment.stringTheory.str_prefixof(), FunctionDeclarationKind.STR_PREFIX); + theoryPredKind.put( + PrincessEnvironment.stringTheory.str_suffixof(), FunctionDeclarationKind.STR_SUFFIX); + theoryPredKind.put( + PrincessEnvironment.stringTheory.str_contains(), FunctionDeclarationKind.STR_CONTAINS); + theoryPredKind.put( + PrincessEnvironment.stringTheory.str_$less$eq(), FunctionDeclarationKind.STR_LE); + theoryPredKind.put( + PrincessEnvironment.stringTheory.str_in_re(), FunctionDeclarationKind.STR_IN_RE); } /** @@ -120,7 +176,13 @@ class PrincessFormulaCreator private final Table arraySortCache = HashBasedTable.create(); PrincessFormulaCreator(PrincessEnvironment pEnv) { - super(pEnv, PrincessEnvironment.BOOL_SORT, PrincessEnvironment.INTEGER_SORT, null, null, null); + super( + pEnv, + PrincessEnvironment.BOOL_SORT, + PrincessEnvironment.INTEGER_SORT, + PrincessEnvironment.FRACTION_SORT, + PrincessEnvironment.STRING_SORT, + PrincessEnvironment.REGEX_SORT); } @Override @@ -134,11 +196,35 @@ public Object convertValue(IExpression value) { IFunApp fun = (IFunApp) value; switch (fun.fun().name()) { case "false": - assert fun.fun().arity() == 0; + Preconditions.checkArgument(fun.fun().arity() == 0); return false; case "mod_cast": // we found a bitvector BV(lower, upper, ctxt), lets extract the last parameter return ((IIntLit) fun.apply(2)).value().bigIntValue(); + case "_int": + case "Rat_int": + Preconditions.checkArgument(fun.fun().arity() == 1); + ITerm term = fun.apply(0); + if (term instanceof IIntLit) { + return ((IIntLit) term).value().bigIntValue(); + } + break; + case "_frac": + case "Rat_frac": + Preconditions.checkArgument(fun.fun().arity() == 2); + ITerm term1 = fun.apply(0); + ITerm term2 = fun.apply(1); + if (term1 instanceof IIntLit && term2 instanceof IIntLit) { + Rational ratValue = + Rational.of( + ((IIntLit) term1).value().bigIntValue(), + ((IIntLit) term2).value().bigIntValue()); + return ratValue.isIntegral() ? ratValue.getNum() : ratValue; + } + break; + case "str_empty": + case "str_cons": + return strToString(fun); default: } } @@ -147,6 +233,32 @@ public Object convertValue(IExpression value) { "unhandled model value " + value + " of type " + value.getClass()); } + /** + * convert a recursive string term like "str_cons(97, str_cons(98, str_cons(99, str_empty)))" to a + * real string "abc" for the user. + */ + private Object strToString(IFunApp fun) { + final StringBuilder str = new StringBuilder(); + while ("str_cons".equals(fun.fun().name())) { + checkArgument(fun.fun().arity() == 2); + ITerm arg = fun.apply(0); + IIntLit chr; + if (arg instanceof IIntLit) { + chr = ((IIntLit) arg); + } else if (arg instanceof IFunApp + && ModuloArithmetic.mod_cast().equals(((IFunApp) arg).fun())) { + chr = ((IIntLit) ((IFunApp) arg).apply(2)); + } else { + throw new AssertionError("unexpected string value: " + fun); + } + str.append(Character.toString(chr.value().bigIntValue().intValue())); + fun = (IFunApp) fun.apply(1); + } + checkArgument("str_empty".equals(fun.fun().name())); + checkArgument(fun.fun().arity() == 0); + return str.toString(); + } + @Override public FormulaType getFormulaType(IExpression pFormula) { return PrincessEnvironment.getFormulaType(pFormula); @@ -261,7 +373,7 @@ public R visit(FormulaVisitor visitor, final Formula f, final IExpression return visitor.visitBoundVariable(f, ((IVariable) input).index()); // nullary atoms and constant are variables - } else if (((input instanceof IAtom) && asJava(((IAtom) input).args()).isEmpty()) + } else if (((input instanceof IAtom) && asJavaCollection(((IAtom) input).args()).isEmpty()) || input instanceof IConstant) { return visitor.visitFreeVariable(f, input.toString()); @@ -284,101 +396,103 @@ public R visit(FormulaVisitor visitor, final Formula f, final IExpression ImmutableList.of(coeffType, factorType), getFormulaType(f), PrincessMultiplyDeclaration.INSTANCE)); + } - } else { - - // then we have to check the declaration kind - final FunctionDeclarationKind kind = getDeclarationKind(input); - - if (kind == FunctionDeclarationKind.EQ) { - scala.Option> maybeArgs = - IExpression.Eq$.MODULE$.unapply((IFormula) input); - - assert maybeArgs.isDefined(); + // then we have to check the declaration kind + final FunctionDeclarationKind kind = getDeclarationKind(input); - final ITerm left = maybeArgs.get()._1; - final ITerm right = maybeArgs.get()._2; + if (kind == FunctionDeclarationKind.EQ) { + scala.Option> maybeArgs = + IExpression.Eq$.MODULE$.unapply((IFormula) input); - ImmutableList.Builder args = ImmutableList.builder(); - ImmutableList.Builder> argTypes = ImmutableList.builder(); + assert maybeArgs.isDefined(); - FormulaType argumentTypeLeft = getFormulaType(left); - args.add(encapsulate(argumentTypeLeft, left)); - argTypes.add(argumentTypeLeft); - FormulaType argumentTypeRight = getFormulaType(right); - args.add(encapsulate(argumentTypeRight, right)); - argTypes.add(argumentTypeRight); + final ITerm left = maybeArgs.get()._1; + final ITerm right = maybeArgs.get()._2; - return visitor.visitFunction( - f, - args.build(), - FunctionDeclarationImpl.of( - getName(input), - FunctionDeclarationKind.EQ, - argTypes.build(), - getFormulaType(f), - PrincessEquationDeclaration.INSTANCE)); + ImmutableList.Builder args = ImmutableList.builder(); + ImmutableList.Builder> argTypes = ImmutableList.builder(); - } else if (kind == FunctionDeclarationKind.UF && input instanceof IIntFormula) { + FormulaType argumentTypeLeft = getFormulaType(left); + args.add(encapsulate(argumentTypeLeft, left)); + argTypes.add(argumentTypeLeft); + FormulaType argumentTypeRight = getFormulaType(right); + args.add(encapsulate(argumentTypeRight, right)); + argTypes.add(argumentTypeRight); - assert ((IIntFormula) input).rel().equals(IIntRelation.EqZero()); + return visitor.visitFunction( + f, + args.build(), + FunctionDeclarationImpl.of( + getName(input), + FunctionDeclarationKind.EQ, + argTypes.build(), + getFormulaType(f), + PrincessEquationDeclaration.INSTANCE)); + } - // this is really a Boolean formula, visit the lhs of the equation - return visit(visitor, f, ((IIntFormula) input).t()); + if (kind == FunctionDeclarationKind.UF && input instanceof IIntFormula) { + assert ((IIntFormula) input).rel().equals(IIntRelation.EqZero()); + // this is really a Boolean formula, visit the lhs of the equation + return visit(visitor, f, ((IIntFormula) input).t()); + } - } else if (kind == FunctionDeclarationKind.OTHER - && input instanceof IFunApp - && ((IFunApp) input).fun() == ModuloArithmetic.mod_cast() + if (kind == FunctionDeclarationKind.OTHER && input instanceof IFunApp) { + if (ModuloArithmetic.mod_cast().equals(((IFunApp) input).fun()) && ((IFunApp) input).apply(2) instanceof IIntLit) { + // mod_cast(0, 256, 7) -> BV=7 with bitsize=8 return visitor.visitConstant(f, convertValue(input)); + } + } - } else { - - ImmutableList.Builder args = ImmutableList.builder(); - ImmutableList.Builder> argTypes = ImmutableList.builder(); - int arity = input.length(); - int arityStart = 0; - - PrincessFunctionDeclaration solverDeclaration; - if (isBitvectorOperationWithAdditionalArgument(kind)) { - // the first argument is the bitsize, and it is not relevant for the user. - // we do not want type/sort information as arguments. - arityStart = 1; - if (input instanceof IAtom) { - solverDeclaration = new PrincessBitvectorToBooleanDeclaration(((IAtom) input).pred()); - } else if (input instanceof IFunApp) { - solverDeclaration = - new PrincessBitvectorToBitvectorDeclaration(((IFunApp) input).fun()); - } else { - throw new AssertionError( - String.format("unexpected bitvector operation '%s' for formula '%s'", kind, input)); - } - } else if (input instanceof IFunApp) { - if (kind == FunctionDeclarationKind.UF) { - solverDeclaration = new PrincessIFunctionDeclaration(((IFunApp) input).fun()); - } else if (kind == FunctionDeclarationKind.MUL) { - solverDeclaration = PrincessMultiplyDeclaration.INSTANCE; - } else { - solverDeclaration = new PrincessByExampleDeclaration(input); - } - } else { - solverDeclaration = new PrincessByExampleDeclaration(input); - } - - for (int i = arityStart; i < arity; i++) { - IExpression arg = input.apply(i); - FormulaType argumentType = getFormulaType(arg); - args.add(encapsulate(argumentType, arg)); - argTypes.add(argumentType); - } + if (kind == FunctionDeclarationKind.UF && input instanceof IFunApp) { + if (CONSTANT_UFS.contains(((IFunApp) input).fun().name())) { + return visitor.visitConstant(f, convertValue(input)); + } + } - return visitor.visitFunction( - f, - args.build(), - FunctionDeclarationImpl.of( - getName(input), kind, argTypes.build(), getFormulaType(f), solverDeclaration)); + ImmutableList.Builder args = ImmutableList.builder(); + ImmutableList.Builder> argTypes = ImmutableList.builder(); + int arity = input.length(); + int arityStart = 0; + + PrincessFunctionDeclaration solverDeclaration; + if (isBitvectorOperationWithAdditionalArgument(kind)) { + // the first argument is the bitsize, and it is not relevant for the user. + // we do not want type/sort information as arguments. + arityStart = 1; + if (input instanceof IAtom) { + solverDeclaration = new PrincessBitvectorToBooleanDeclaration(((IAtom) input).pred()); + } else if (input instanceof IFunApp) { + solverDeclaration = new PrincessBitvectorToBitvectorDeclaration(((IFunApp) input).fun()); + } else { + throw new AssertionError( + String.format("unexpected bitvector operation '%s' for formula '%s'", kind, input)); + } + } else if (input instanceof IFunApp) { + if (kind == FunctionDeclarationKind.UF) { + solverDeclaration = new PrincessIFunctionDeclaration(((IFunApp) input).fun()); + } else if (kind == FunctionDeclarationKind.MUL) { + solverDeclaration = PrincessMultiplyDeclaration.INSTANCE; + } else { + solverDeclaration = new PrincessByExampleDeclaration(input); } + } else { + solverDeclaration = new PrincessByExampleDeclaration(input); } + + for (int i = arityStart; i < arity; i++) { + IExpression arg = input.apply(i); + FormulaType argumentType = getFormulaType(arg); + args.add(encapsulate(argumentType, arg)); + argTypes.add(argumentType); + } + + return visitor.visitFunction( + f, + args.build(), + FunctionDeclarationImpl.of( + getName(input), kind, argTypes.build(), getFormulaType(f), solverDeclaration)); } private boolean isBitvectorOperationWithAdditionalArgument(FunctionDeclarationKind kind) { @@ -411,7 +525,7 @@ private boolean isBitvectorOperationWithAdditionalArgument(FunctionDeclarationKi } private FunctionDeclarationKind getDeclarationKind(IExpression input) { - assert !(((input instanceof IAtom) && asJava(((IAtom) input).args()).isEmpty()) + assert !(((input instanceof IAtom) && asJavaCollection(((IAtom) input).args()).isEmpty()) || input instanceof IConstant) : "Variables should be handled somewhere else"; 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 d7345b59a7..0e1055ea29 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java @@ -30,21 +30,23 @@ final class PrincessFormulaManager PrincessUFManager pFunctionManager, PrincessBooleanFormulaManager pBooleanManager, PrincessIntegerFormulaManager pIntegerManager, + PrincessRationalFormulaManager pRationalManager, PrincessBitvectorFormulaManager pBitpreciseManager, PrincessArrayFormulaManager pArrayManager, - PrincessQuantifiedFormulaManager pQuantifierManager) { + PrincessQuantifiedFormulaManager pQuantifierManager, + PrincessStringFormulaManager pStringManager) { super( pCreator, pFunctionManager, pBooleanManager, pIntegerManager, - null, + pRationalManager, pBitpreciseManager, null, pQuantifierManager, pArrayManager, null, - null, + pStringManager, null); creator = pCreator; } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java index ab36d9d8cf..078be24a32 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java @@ -13,6 +13,7 @@ import ap.basetypes.IdealInt; import ap.parser.IAtom; +import ap.parser.IConstant; import ap.parser.IExpression; import ap.parser.IExpression.BooleanFunApplier; import ap.parser.IFormula; @@ -21,10 +22,13 @@ import ap.parser.IIntLit; import ap.parser.ITerm; import ap.parser.ITermITE; +import ap.terfor.ConstantTerm; import ap.terfor.preds.Predicate; import ap.theories.nia.GroebnerMultiplication; +import ap.types.MonoSortedIFunction; import ap.types.Sort; import ap.types.Sort$; +import ap.types.SortedConstantTerm; import ap.types.SortedIFunction$; import java.util.ArrayList; import java.util.List; @@ -88,12 +92,16 @@ public IExpression makeApp(PrincessEnvironment env, List args) { args.size() == declarationItem.arity(), "functiontype has different number of args."); final List argsList = new ArrayList<>(); - for (IExpression arg : args) { - ITerm termArg; + for (int i = 0; i < args.size(); i++) { + final IExpression arg = args.get(i); + final ITerm termArg; if (arg instanceof IFormula) { // boolean term -> build ITE(t,0,1) termArg = new ITermITE( (IFormula) arg, new IIntLit(IdealInt.ZERO()), new IIntLit(IdealInt.ONE())); + } else if (!isRationalSortArg(arg) && isRationalSortArgument(i)) { + // sort does not match, so we need to cast the argument to rational theory. + termArg = PrincessEnvironment.rationalTheory.int2ring((ITerm) arg); } else { termArg = (ITerm) arg; } @@ -111,6 +119,33 @@ public IExpression makeApp(PrincessEnvironment env, List args) { return returnFormula; } } + + private boolean isRationalSortArg(IExpression arg) { + if (arg instanceof IFunApp) { + IFunction fun = ((IFunApp) arg).fun(); + if (fun instanceof MonoSortedIFunction) { + Sort sort = ((MonoSortedIFunction) fun).resSort(); + return PrincessEnvironment.FRACTION_SORT.equals(sort); + } + } + if (arg instanceof IConstant) { + ConstantTerm constant = ((IConstant) arg).c(); + if (constant instanceof SortedConstantTerm) { + Sort sort = ((SortedConstantTerm) constant).sort(); + return PrincessEnvironment.FRACTION_SORT.equals(sort); + } + } + return false; + } + + private boolean isRationalSortArgument(Integer index) { + // we switch from "int" to "Integer" in the signature to avoid ambiguous types with Scala API. + if (declarationItem instanceof MonoSortedIFunction) { + Sort sort = ((MonoSortedIFunction) declarationItem).argSorts().apply(index); + return PrincessEnvironment.rationalTheory.FractionSort().equals(sort); + } + return false; + } } static class PrincessByExampleDeclaration extends AbstractDeclaration { diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessIntegerFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessIntegerFormulaManager.java index 8896383855..971a5770fa 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessIntegerFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessIntegerFormulaManager.java @@ -100,4 +100,9 @@ public IExpression multiply(IExpression pNumber1, IExpression pNumber2) { protected boolean isNumeral(IExpression val) { return val instanceof IIntLit; } + + @Override + protected IExpression floor(IExpression pNumber) { + return pNumber; // identity for integers + } } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java index 5e65b30840..8c84ac8cbc 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java @@ -241,7 +241,7 @@ public String toString() { public void close() {} @Override - protected IExpression evalImpl(IExpression formula) { + protected @Nullable IExpression evalImpl(IExpression formula) { IExpression evaluation = evaluate(formula); if (evaluation == null) { // fallback: try to simplify the query and evaluate again. diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java new file mode 100644 index 0000000000..6a187b37d1 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java @@ -0,0 +1,111 @@ +// 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.solvers.princess; + +import ap.parser.IExpression; +import ap.parser.IFunApp; +import ap.parser.ITerm; +import com.google.common.collect.ImmutableList; +import java.math.BigDecimal; +import java.math.BigInteger; +import java.util.List; +import org.sosy_lab.common.rationals.Rational; +import org.sosy_lab.java_smt.api.NumeralFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; +import org.sosy_lab.java_smt.api.RationalFormulaManager; + +public class PrincessRationalFormulaManager + extends PrincessNumeralFormulaManager + implements RationalFormulaManager { + + private PrincessIntegerFormulaManager pInteger; + + PrincessRationalFormulaManager( + PrincessFormulaCreator pCreator, + NonLinearArithmetic pNonLinearArithmetic, + PrincessIntegerFormulaManager pInteger) { + super(pCreator, pNonLinearArithmetic); + this.pInteger = pInteger; + } + + @Override + protected boolean isNumeral(IExpression value) { + if (value instanceof IFunApp) { + IFunApp fun = (IFunApp) value; + switch (fun.fun().name()) { + case "int": + case "Rat_int": + assert fun.fun().arity() == 1; + return pInteger.isNumeral(fun.apply(0)); + case "frac": + assert fun.fun().arity() == 2; + return pInteger.isNumeral(fun.apply(0)) && pInteger.isNumeral(fun.apply(1)); + } + } + return false; + } + + protected IExpression fromInteger(ITerm i) { + return PrincessEnvironment.rationalTheory.int2ring(i); + } + + @Override + protected IExpression makeNumberImpl(long i) { + return fromInteger(pInteger.makeNumberImpl(i)); + } + + @Override + protected IExpression makeNumberImpl(BigInteger i) { + return fromInteger(pInteger.makeNumberImpl(i)); + } + + @Override + protected IExpression makeNumberImpl(Rational pI) { + return divide(makeNumberImpl(pI.getNum()), makeNumberImpl(pI.getDen())); + } + + @Override + protected IExpression makeNumberImpl(String i) { + return makeNumberImpl(new BigDecimal(i)); + } + + @Override + protected IExpression makeNumberImpl(double pNumber) { + return makeNumberImpl(BigDecimal.valueOf(pNumber)); + } + + @Override + protected IExpression makeNumberImpl(BigDecimal pNumber) { + List args = + ImmutableList.of( + pInteger.makeNumberImpl(pNumber.unscaledValue()), + pInteger.makeNumberImpl(BigInteger.valueOf(10).pow(pNumber.scale()))); + return new IFunApp(PrincessEnvironment.rationalTheory.frac(), PrincessEnvironment.toSeq(args)); + } + + @Override + protected IExpression makeVariableImpl(String varName) { + return getFormulaCreator().makeVariable(PrincessEnvironment.FRACTION_SORT, varName); + } + + @Override + protected IExpression floor(IExpression number) { + throw new AssertionError("floor is not supported in Princess"); + } + + @Override + protected IExpression multiply(IExpression number1, IExpression number2) { + return PrincessEnvironment.rationalTheory.mul((ITerm) number1, (ITerm) number2); + } + + @Override + protected IExpression divide(IExpression number1, IExpression number2) { + return PrincessEnvironment.rationalTheory.div((ITerm) number1, (ITerm) number2); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java index 36a7444539..bb7b14d6f8 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java @@ -50,20 +50,25 @@ public static SolverContext create( PrincessBooleanFormulaManager booleanTheory = new PrincessBooleanFormulaManager(creator); PrincessIntegerFormulaManager integerTheory = new PrincessIntegerFormulaManager(creator, pNonLinearArithmetic); + PrincessRationalFormulaManager rationalTheory = + new PrincessRationalFormulaManager(creator, pNonLinearArithmetic, integerTheory); PrincessBitvectorFormulaManager bitvectorTheory = new PrincessBitvectorFormulaManager(creator, booleanTheory); PrincessArrayFormulaManager arrayTheory = new PrincessArrayFormulaManager(creator); PrincessQuantifiedFormulaManager quantifierTheory = new PrincessQuantifiedFormulaManager(creator); + PrincessStringFormulaManager stringTheory = new PrincessStringFormulaManager(creator); PrincessFormulaManager manager = new PrincessFormulaManager( creator, functionTheory, booleanTheory, integerTheory, + rationalTheory, bitvectorTheory, arrayTheory, - quantifierTheory); + quantifierTheory, + stringTheory); return new PrincessSolverContext(manager, creator); } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java new file mode 100644 index 0000000000..c9721460d1 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java @@ -0,0 +1,215 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2023 Alejandro SerranoMena +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.solvers.princess; + +import static org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.toITermSeq; + +import ap.parser.IAtom; +import ap.parser.IBinFormula; +import ap.parser.IBinJunctor; +import ap.parser.IExpression; +import ap.parser.IFormula; +import ap.parser.IFunApp; +import ap.parser.INot; +import ap.parser.ITerm; +import ap.types.Sort; +import java.util.List; +import org.sosy_lab.java_smt.api.RegexFormula; +import org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager; + +public class PrincessStringFormulaManager + extends AbstractStringFormulaManager< + IExpression, Sort, PrincessEnvironment, PrincessFunctionDeclaration> { + + PrincessStringFormulaManager(PrincessFormulaCreator pCreator) { + super(pCreator); + } + + @Override + protected IExpression makeStringImpl(String value) { + return PrincessEnvironment.stringTheory.string2Term(value); + } + + @Override + protected IExpression makeVariableImpl(String pVar) { + Sort t = getFormulaCreator().getStringType(); + return getFormulaCreator().makeVariable(t, pVar); + } + + @Override + protected IFormula equal(IExpression pParam1, IExpression pParam2) { + return ((ITerm) pParam1).$eq$eq$eq((ITerm) pParam2); + } + + @Override + protected IFormula greaterThan(IExpression pParam1, IExpression pParam2) { + IFormula leq = greaterOrEquals(pParam1, pParam2); + IFormula eq = equal(pParam1, pParam2); + return new IBinFormula(IBinJunctor.And(), leq, new INot(eq)); + } + + @Override + protected IFormula lessOrEquals(IExpression pParam1, IExpression pParam2) { + return new IAtom(PrincessEnvironment.stringTheory.str_$less$eq(), toITermSeq(pParam1, pParam2)); + } + + @Override + protected IFormula greaterOrEquals(IExpression pParam1, IExpression pParam2) { + // just reverse the order + return lessOrEquals(pParam2, pParam1); + } + + @Override + protected IFormula lessThan(IExpression pParam1, IExpression pParam2) { + IFormula leq = lessOrEquals(pParam1, pParam2); + IFormula eq = equal(pParam1, pParam2); + return new IBinFormula(IBinJunctor.And(), leq, new INot(eq)); + } + + @Override + protected ITerm length(IExpression pParam) { + return new IFunApp(PrincessEnvironment.stringTheory.str_len(), toITermSeq(pParam)); + } + + @Override + protected ITerm concatImpl(List parts) { + return new IFunApp(PrincessEnvironment.stringTheory.str_$plus$plus(), toITermSeq(parts)); + } + + @Override + protected IFormula prefix(IExpression prefix, IExpression str) { + return new IAtom(PrincessEnvironment.stringTheory.str_prefixof(), toITermSeq(prefix, str)); + } + + @Override + protected IFormula suffix(IExpression suffix, IExpression str) { + return new IAtom(PrincessEnvironment.stringTheory.str_suffixof(), toITermSeq(suffix, str)); + } + + @Override + protected IFormula in(IExpression str, IExpression regex) { + return new IAtom(PrincessEnvironment.stringTheory.str_in_re(), toITermSeq(str, regex)); + } + + @Override + protected IFormula contains(IExpression str, IExpression part) { + return new IAtom(PrincessEnvironment.stringTheory.str_contains(), toITermSeq(str, part)); + } + + @Override + protected ITerm indexOf(IExpression str, IExpression part, IExpression startIndex) { + return new IFunApp( + PrincessEnvironment.stringTheory.str_indexof(), toITermSeq(str, part, startIndex)); + } + + @Override + protected ITerm charAt(IExpression str, IExpression index) { + return new IFunApp(PrincessEnvironment.stringTheory.str_at(), toITermSeq(str, index)); + } + + @Override + protected ITerm substring(IExpression str, IExpression index, IExpression length) { + return new IFunApp( + PrincessEnvironment.stringTheory.str_substr(), toITermSeq(str, index, length)); + } + + @Override + protected ITerm replace(IExpression fullStr, IExpression target, IExpression replacement) { + return new IFunApp( + PrincessEnvironment.stringTheory.str_replace(), toITermSeq(fullStr, target, replacement)); + } + + @Override + protected ITerm replaceAll(IExpression fullStr, IExpression target, IExpression replacement) { + return new IFunApp( + PrincessEnvironment.stringTheory.str_replaceall(), + toITermSeq(fullStr, target, replacement)); + } + + @Override + protected ITerm makeRegexImpl(String value) { + return new IFunApp( + PrincessEnvironment.stringTheory.str_to_re(), toITermSeq(makeStringImpl(value))); + } + + @Override + protected ITerm noneImpl() { + return new IFunApp(PrincessEnvironment.stringTheory.re_none(), toITermSeq()); + } + + @Override + protected ITerm allImpl() { + return new IFunApp(PrincessEnvironment.stringTheory.re_all(), toITermSeq()); + } + + @Override + protected IExpression allCharImpl() { + return new IFunApp(PrincessEnvironment.stringTheory.re_allchar(), toITermSeq()); + } + + @Override + protected ITerm range(IExpression start, IExpression end) { + return new IFunApp(PrincessEnvironment.stringTheory.re_range(), toITermSeq()); + } + + @Override + public RegexFormula cross(RegexFormula regex) { + return wrapRegex( + new IFunApp(PrincessEnvironment.stringTheory.re_$plus(), toITermSeq(extractInfo(regex)))); + } + + @Override + public RegexFormula optional(RegexFormula regex) { + return wrapRegex( + new IFunApp(PrincessEnvironment.stringTheory.re_opt(), toITermSeq(extractInfo(regex)))); + } + + @Override + public RegexFormula difference(RegexFormula regex1, RegexFormula regex2) { + return wrapRegex( + new IFunApp( + PrincessEnvironment.stringTheory.re_diff(), + toITermSeq(extractInfo(regex1), extractInfo(regex2)))); + } + + @Override + protected ITerm concatRegexImpl(List parts) { + return new IFunApp(PrincessEnvironment.stringTheory.re_$plus$plus(), toITermSeq(parts)); + } + + @Override + protected ITerm union(IExpression pParam1, IExpression pParam2) { + return new IFunApp(PrincessEnvironment.stringTheory.re_union(), toITermSeq(pParam1, pParam2)); + } + + @Override + protected ITerm intersection(IExpression pParam1, IExpression pParam2) { + return new IFunApp(PrincessEnvironment.stringTheory.re_inter(), toITermSeq(pParam1, pParam2)); + } + + @Override + protected ITerm closure(IExpression pParam) { + return new IFunApp(PrincessEnvironment.stringTheory.re_$times(), toITermSeq(pParam)); + } + + @Override + protected ITerm complement(IExpression pParam) { + return new IFunApp(PrincessEnvironment.stringTheory.re_comp(), toITermSeq(pParam)); + } + + @Override + protected ITerm toIntegerFormula(IExpression pParam) { + return new IFunApp(PrincessEnvironment.stringTheory.str_to_int(), toITermSeq(pParam)); + } + + @Override + protected ITerm toStringFormula(IExpression pParam) { + return new IFunApp(PrincessEnvironment.stringTheory.int_to_str(), toITermSeq(pParam)); + } +} diff --git a/src/org/sosy_lab/java_smt/test/FormulaClassifierTest.java b/src/org/sosy_lab/java_smt/test/FormulaClassifierTest.java index 7153a68204..ffc10d2699 100644 --- a/src/org/sosy_lab/java_smt/test/FormulaClassifierTest.java +++ b/src/org/sosy_lab/java_smt/test/FormulaClassifierTest.java @@ -70,6 +70,10 @@ public void test_QF_AUFLIRA() { .withMessage("Solver %s does not support mixed integer-real arithmetic", solverToUse()) .that(solverToUse()) .isNotEqualTo(Solvers.OPENSMT); + assume() + .withMessage("Solver %s does not support mixed real-array arithmetic", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.PRINCESS); requireParser(); requireRationals(); @@ -80,6 +84,11 @@ public void test_QF_AUFLIRA() { @Test public void test_QF_AUFNIRA() { + assume() + .withMessage("Solver %s does not support mixed real-array arithmetic", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.PRINCESS); + requireParser(); requireRationals(); requireNonlinear(); diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index ca880c17a3..ace0b1947c 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -2344,9 +2344,16 @@ public void testGetSmallIntegralRationals1() throws SolverException, Interrupted @Test public void testGetRationals1() throws SolverException, InterruptedException { requireRationals(); + RationalFormula x = rmgr.makeVariable("x"); evaluateInModel( - rmgr.equal(rmgr.makeVariable("x"), rmgr.makeNumber(Rational.ofString("1/3"))), - rmgr.divide(rmgr.makeVariable("x"), rmgr.makeNumber(2)), + rmgr.equal(x, rmgr.makeNumber(Rational.ofString("1/3"))), x, Rational.ofString("1/3")); + evaluateInModel( + rmgr.equal(x, rmgr.makeNumber(Rational.ofString("1/3"))), + rmgr.multiply(x, rmgr.makeNumber(2)), + Rational.ofString("2/3")); + evaluateInModel( + rmgr.equal(x, rmgr.makeNumber(Rational.ofString("1/3"))), + rmgr.divide(x, rmgr.makeNumber(2)), Rational.ofString("1/6")); } diff --git a/src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java b/src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java index 786ae61578..64a7f7f298 100644 --- a/src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java +++ b/src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java @@ -134,7 +134,8 @@ public void testLinearMultiplication() throws SolverException, InterruptedExcept } @Test - public void testLinearMultiplicationUnsatisfiable() throws SolverException, InterruptedException { + public void testLinearMultiplicationWithConstantUnsatisfiable() + throws SolverException, InterruptedException { T a = nmgr.makeVariable("a"); BooleanFormula f = @@ -200,11 +201,12 @@ public void testDivisionByConstant() throws SolverException, InterruptedExceptio @Test public void testDivisionByZero() throws SolverException, InterruptedException { - // INFO: OpenSmt does not allow division by zero + // OpenSmt and Yices do not allow division by zero and throw an exception. + // Princess does not allow division by zero and returns UNSAT. assume() .withMessage("Solver %s does not support division by zero", solverToUse()) .that(solverToUse()) - .isNoneOf(Solvers.YICES2, Solvers.OPENSMT); + .isNoneOf(Solvers.YICES2, Solvers.OPENSMT, Solvers.PRINCESS); T a = nmgr.makeVariable("a"); T b = nmgr.makeVariable("b"); diff --git a/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java index 1515133f88..dda96584b8 100644 --- a/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java @@ -10,14 +10,12 @@ import static com.google.common.truth.Truth.assertThat; import static com.google.common.truth.Truth.assert_; -import static com.google.common.truth.TruthJUnit.assume; import com.google.common.collect.Iterables; import java.util.HashSet; import java.util.List; import java.util.Set; import org.junit.Test; -import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FunctionDeclaration; @@ -37,11 +35,9 @@ public class RationalFormulaManagerTest extends SolverBasedTest0.ParameterizedSo @Test public void rationalToIntTest() throws SolverException, InterruptedException { requireRationals(); - assume() - .withMessage("Solver %s does not support floor operation", solverToUse()) - .that(solverToUse()) - .isNotEqualTo(Solvers.OPENSMT); + requireRationalFloor(); + requireRationalFloor(); for (double v : SOME_DOUBLES) { IntegerFormula i = imgr.makeNumber((int) Math.floor(v)); RationalFormula r = rmgr.makeNumber(v); @@ -65,6 +61,7 @@ public void intToIntTest() throws SolverException, InterruptedException { @Test public void intToIntWithRmgrTest() throws SolverException, InterruptedException { requireRationals(); + requireRationalFloor(); for (double v : SOME_DOUBLES) { IntegerFormula i = imgr.makeNumber((int) Math.floor(v)); assertThat(mgr.getFormulaType(i)).isEqualTo(FormulaType.IntegerType); @@ -77,6 +74,7 @@ public void intToIntWithRmgrTest() throws SolverException, InterruptedException public void floorIsLessOrEqualsValueTest() throws SolverException, InterruptedException { requireRationals(); requireQuantifiers(); + requireRationalFloor(); RationalFormula v = rmgr.makeVariable("v"); assertThatFormula(rmgr.lessOrEquals(rmgr.floor(v), v)).isTautological(); } @@ -85,6 +83,7 @@ public void floorIsLessOrEqualsValueTest() throws SolverException, InterruptedEx public void floorIsGreaterThanValueTest() throws SolverException, InterruptedException { requireRationals(); requireQuantifiers(); + requireRationalFloor(); RationalFormula v = rmgr.makeVariable("v"); assertThatFormula(rmgr.lessOrEquals(rmgr.floor(v), v)).isTautological(); } @@ -93,6 +92,7 @@ public void floorIsGreaterThanValueTest() throws SolverException, InterruptedExc public void forallFloorIsLessOrEqualsValueTest() throws SolverException, InterruptedException { requireRationals(); requireQuantifiers(); + requireRationalFloor(); RationalFormula v = rmgr.makeVariable("v"); assertThatFormula(qmgr.forall(v, rmgr.lessOrEquals(rmgr.floor(v), v))).isTautological(); } @@ -101,6 +101,7 @@ public void forallFloorIsLessOrEqualsValueTest() throws SolverException, Interru public void forallFloorIsLessThanValueTest() throws SolverException, InterruptedException { requireRationals(); requireQuantifiers(); + requireRationalFloor(); RationalFormula v = rmgr.makeVariable("v"); // counterexample: all integers assertThatFormula(qmgr.forall(v, rmgr.lessThan(rmgr.floor(v), v))).isUnsatisfiable(); @@ -109,10 +110,7 @@ public void forallFloorIsLessThanValueTest() throws SolverException, Interrupted @Test public void visitFloorTest() { requireRationals(); - assume() - .withMessage("Solver %s does not support floor operation", solverToUse()) - .that(solverToUse()) - .isNotEqualTo(Solvers.OPENSMT); + requireRationalFloor(); IntegerFormula f = rmgr.floor(rmgr.makeVariable("v")); assertThat(mgr.extractVariables(f)).hasSize(1); diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index 55db681570..f9ed066400 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -216,6 +216,13 @@ protected final void requireRationals() { .isNotNull(); } + protected final void requireRationalFloor() { + assume() + .withMessage("Solver %s does not support floor for rationals", solverToUse()) + .that(solverToUse()) + .isNoneOf(Solvers.PRINCESS, Solvers.OPENSMT); + } + /** Skip test if the solver does not support bitvectors. */ protected final void requireBitvectors() { assume() diff --git a/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java b/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java index 5b50bb5a62..025d9b6051 100644 --- a/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java @@ -799,6 +799,33 @@ public void testMakeBitVectorArray() { } } + @Test + public void testNestedIntegerArray() { + requireArrays(); + requireIntegers(); + + IntegerFormula _i = imgr.makeVariable("i"); + ArrayFormula> multi = + amgr.makeArray( + "multi", + FormulaType.IntegerType, + FormulaType.getArrayType(FormulaType.IntegerType, FormulaType.IntegerType)); + + IntegerFormula valueInMulti = amgr.select(amgr.select(multi, _i), _i); + + switch (solver) { + case MATHSAT5: + assertThat(valueInMulti.toString()) + .isEqualTo("(`read_int_int` (`read_int_T(17)` multi i) i)"); + break; + case PRINCESS: + assertThat(valueInMulti.toString()).isEqualTo("select(select(multi, i), i)"); + break; + default: + assertThat(valueInMulti.toString()).isEqualTo("(select (select multi i) i)"); + } + } + @Test public void testNestedRationalArray() { requireArrays(); @@ -819,6 +846,9 @@ public void testNestedRationalArray() { assertThat(valueInMulti.toString()) .isEqualTo("(`read_int_rat` (`read_int_T(17)` multi i) i)"); break; + case PRINCESS: + assertThat(valueInMulti.toString()).isEqualTo("select(select(multi, i), i)"); + break; default: assertThat(valueInMulti.toString()).isEqualTo("(select (select multi i) i)"); }