trackingStack = new ArrayDeque<>(); // symbols on all levels
+ /**
+ * Values returned by {@link Model#evaluate(Formula)}.
+ *
+ * We need to record these to make sure that the values returned by the evaluator are
+ * consistant. Calling {@link #isUnsat()} will reset this list as the underlying model has been
+ * updated.
+ */
+ protected final List evaluatedTerms = new ArrayList<>();
+
// assign a unique partition number for eah added constraint, for unsat-core and interpolation.
protected final UniqueIdGenerator idGenerator = new UniqueIdGenerator();
protected final Deque> partitions = new ArrayDeque<>();
@@ -76,9 +86,11 @@ protected PrincessAbstractProver(
public boolean isUnsat() throws SolverException {
Preconditions.checkState(!closed);
wasLastSatCheckSat = false;
+ evaluatedTerms.clear();
final Value result = api.checkSat(true);
if (result.equals(SimpleAPI.ProverStatus$.MODULE$.Sat())) {
wasLastSatCheckSat = true;
+ evaluatedTerms.add(api.partialModelAsFormula());
return false;
} else if (result.equals(SimpleAPI.ProverStatus$.MODULE$.Unsat())) {
return true;
@@ -121,7 +133,7 @@ protected void popImpl() {
// we have to recreate symbols on lower levels, because JavaSMT assumes "global" symbols.
Level level = trackingStack.pop();
api.addBooleanVariables(asScala(level.booleanSymbols));
- api.addConstants(asScala(level.intSymbols));
+ api.addConstants(asScala(level.theorySymbols));
level.functionSymbols.forEach(api::addFunction);
if (!trackingStack.isEmpty()) {
trackingStack.peek().mergeWithHigher(level);
@@ -129,6 +141,20 @@ protected void popImpl() {
partitions.pop();
}
+ /**
+ * Get a list of all terms that have been evaluated in the current model.
+ *
+ * The formulas in this list are assignments that extend the original model.
+ */
+ List getEvaluatedTerms() {
+ return evaluatedTerms;
+ }
+
+ /** Add a new term to the list of evaluated terms. */
+ void addEvaluatedTerm(IFormula pFormula) {
+ evaluatedTerms.add(pFormula);
+ }
+
@SuppressWarnings("resource")
@Override
public Model getModel() throws SolverException {
@@ -146,7 +172,7 @@ protected PrincessModel getEvaluatorWithoutChecks() throws SolverException {
} catch (SimpleAPIException ex) {
throw new SolverException(ex.getMessage(), ex);
}
- return new PrincessModel(this, partialModel, creator, api);
+ return registerEvaluator(new PrincessModel(this, partialModel, creator, api));
}
/**
@@ -213,12 +239,12 @@ void addSymbol(IFormula f) {
}
}
- /** add external definition: integer variable. */
+ /** add external definition: theory variable (integer, rational, string, etc). */
void addSymbol(ITerm f) {
Preconditions.checkState(!closed);
api.addConstant(f);
if (!trackingStack.isEmpty()) {
- trackingStack.peek().intSymbols.add(f);
+ trackingStack.peek().theorySymbols.add(f);
}
}
@@ -233,7 +259,7 @@ void addSymbol(IFunction f) {
static class Level {
final List booleanSymbols = new ArrayList<>();
- final List intSymbols = new ArrayList<>();
+ final List theorySymbols = new ArrayList<>();
final List functionSymbols = new ArrayList<>();
Level() {}
@@ -241,13 +267,13 @@ static class Level {
/** add higher level to current level, we keep the order of creating symbols. */
void mergeWithHigher(Level other) {
this.booleanSymbols.addAll(other.booleanSymbols);
- this.intSymbols.addAll(other.intSymbols);
+ this.theorySymbols.addAll(other.theorySymbols);
this.functionSymbols.addAll(other.functionSymbols);
}
@Override
public String toString() {
- return String.format("{%s, %s, %s}", booleanSymbols, intSymbols, functionSymbols);
+ return String.format("{%s, %s, %s}", booleanSymbols, theorySymbols, functionSymbols);
}
}
}
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 ede3155b8f..407ed2cb8b 100644
--- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java
+++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java
@@ -22,7 +22,10 @@
import ap.parser.IFunApp;
import ap.parser.IFunction;
import ap.parser.IIntFormula;
+import ap.parser.IPlus;
import ap.parser.ITerm;
+import ap.parser.ITermITE;
+import ap.parser.ITimes;
import ap.parser.Parser2InputAbsy.TranslationException;
import ap.parser.PartialEvaluator;
import ap.parser.SMTLineariser;
@@ -33,7 +36,8 @@
import ap.theories.arrays.ExtArray;
import ap.theories.arrays.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$;
@@ -54,6 +58,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;
@@ -64,6 +69,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;
@@ -76,6 +82,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;
@@ -104,6 +112,52 @@ 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(
+ /* OFlag default values:
+ * -- Pre-image specific options
+ * eagerAutomataOperations : false,
+ * measureTimes : false,
+ * useLength : OFlags.LengthOptions.Auto,
+ * useParikhConstraints : true,
+ * minimizeAutomata : false,
+ * forwardPropagation : false,
+ * backwardPropagation : true,
+ * nielsenSplitter : true,
+ * regexTranslator : OFlags.RegexTranslator.Hybrid,
+ */
+ 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(),
+ /* -- Options for the cost-enriched-automata solver
+ * ceaBackend : OFlags.CEABackend.Unary,
+ * useCostEnriched : false,
+ * debug : false,
+ * underApprox : true,
+ * underApproxBound : 15,
+ * simplifyAut : true
+ */
+ OFlags.$lessinit$greater$default$10(),
+ OFlags.$lessinit$greater$default$11(),
+ OFlags.$lessinit$greater$default$12(),
+ OFlags.$lessinit$greater$default$13(),
+ OFlags.$lessinit$greater$default$14(),
+ OFlags.$lessinit$greater$default$15()));
+ 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;
@@ -508,9 +562,25 @@ private static String getName(IExpression var) {
}
static FormulaType getFormulaType(IExpression pFormula) {
+ // TODO: We could use Sort.sortof() here, but it sometimes returns `integer` even though the
+ // term is rational. We should figure out why and then open a new issue for this.
if (pFormula instanceof IFormula) {
return FormulaType.BooleanType;
- } else if (pFormula instanceof ITerm) {
+ } else if (pFormula instanceof ITimes) {
+ // coeff is always INT, lets check the subterm.
+ ITimes times = (ITimes) pFormula;
+ return getFormulaType(times.subterm());
+ } else if (pFormula instanceof IPlus) {
+ IPlus plus = (IPlus) pFormula;
+ FormulaType t1 = getFormulaType(plus.t1());
+ FormulaType t2 = getFormulaType(plus.t2());
+ return mergeFormulaTypes(t1, t2);
+ } else if (pFormula instanceof ITermITE) {
+ ITermITE plus = (ITermITE) pFormula;
+ FormulaType t1 = getFormulaType(plus.left());
+ FormulaType t2 = getFormulaType(plus.right());
+ return mergeFormulaTypes(t1, t2);
+ } else {
final Sort sort = Sort$.MODULE$.sortOf((ITerm) pFormula);
try {
return getFormulaTypeFromSort(sort);
@@ -518,22 +588,43 @@ static FormulaType getFormulaType(IExpression pFormula) {
// 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);
}
}
+ }
+
+ /**
+ * 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(
- "Unknown formula type '%s' for formula '%s'.", pFormula.getClass(), pFormula));
+ 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 ArraySort) {
Seq indexSorts = ((ArraySort) sort).theory().indexSorts();
Sort elementSort = ((ArraySort) sort).theory().objSort();
@@ -661,6 +752,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 d8846fbb2b..ffc08c3ec5 100644
--- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java
+++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java
@@ -13,6 +13,7 @@
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;
@@ -42,15 +43,22 @@
import ap.theories.arrays.ExtArray;
import ap.theories.bitvectors.ModuloArithmetic;
import ap.theories.nia.GroebnerMultiplication$;
+import ap.theories.rationals.Fractions;
+import ap.theories.rationals.Rationals$;
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.lang.reflect.InvocationTargetException;
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 +84,7 @@ 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");
static {
theoryFunctionKind.put(ModuloArithmetic.bv_concat(), FunctionDeclarationKind.BV_CONCAT);
@@ -107,6 +116,58 @@ 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_$less(), FunctionDeclarationKind.STR_LT);
+ theoryPredKind.put(
+ PrincessEnvironment.stringTheory.str_in_re(), FunctionDeclarationKind.STR_IN_RE);
}
/**
@@ -120,7 +181,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
@@ -133,12 +200,39 @@ public Object convertValue(IExpression value) {
if (value instanceof IFunApp) {
IFunApp fun = (IFunApp) value;
switch (fun.fun().name()) {
+ case "true":
+ Preconditions.checkArgument(fun.fun().arity() == 0);
+ return true;
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 +241,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);
@@ -231,6 +351,33 @@ private String getName(IExpression input) {
}
}
+ /** Returns true if the expression is a constant number. */
+ private static boolean isConstant(IFunApp pExpr) {
+ for (IExpression sub : asJava(pExpr.args())) {
+ if (!(sub instanceof IIntLit)) {
+ return false;
+ }
+ }
+ return true;
+ }
+
+ /** Returns true if the expression is an integer literal. */
+ private static boolean isRatInt(IFunApp pExpr) {
+ // We need to use reflection to get Rationals.int() as `int` can't be a method name in Java
+ final IFunction ratInt;
+ try {
+ ratInt = (IFunction) Fractions.class.getMethod("int").invoke(Rationals$.MODULE$);
+ } catch (IllegalAccessException | NoSuchMethodException | InvocationTargetException pE) {
+ throw new RuntimeException(pE);
+ }
+ return isConstant(pExpr) && pExpr.fun().equals(ratInt);
+ }
+
+ /** Returns true if the expression is a faction literal. */
+ private static boolean isRatFrac(IFunApp pExpr) {
+ return isConstant(pExpr) && pExpr.fun().equals(Rationals$.MODULE$.frac());
+ }
+
@Override
public R visit(FormulaVisitor visitor, final Formula f, final IExpression input) {
if (input instanceof IIntLit) {
@@ -241,8 +388,12 @@ public R visit(FormulaVisitor visitor, final Formula f, final IExpression
IBoolLit literal = (IBoolLit) input;
return visitor.visitConstant(f, literal.value());
- // this is a quantifier
+ } else if (input instanceof IFunApp
+ && (isRatInt((IFunApp) input) || isRatFrac((IFunApp) input))) {
+ return visitor.visitConstant(f, convertValue(input));
+
} else if (input instanceof IQuantified) {
+ // this is a quantifier
BooleanFormula body = encapsulateBoolean(((IQuantified) input).subformula());
return visitor.visitQuantifier(
@@ -256,17 +407,17 @@ public R visit(FormulaVisitor visitor, final Formula f, final IExpression
new ArrayList<>(),
body);
- // variable bound by a quantifier
} else if (input instanceof IVariable) {
+ // variable bound by a quantifier
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) {
+ // nullary atoms and constant are variables
return visitor.visitFreeVariable(f, input.toString());
- // Princess encodes multiplication as "linear coefficient and factor" with arity 1.
} else if (input instanceof ITimes) {
+ // Princess encodes multiplication as "linear coefficient and factor" with arity 1.
assert input.length() == 1;
ITimes multiplication = (ITimes) input;
@@ -284,101 +435,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) {
@@ -412,7 +565,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..d7b470236d 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 (!exprIsRational(arg) && functionTakesRational(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,36 @@ public IExpression makeApp(PrincessEnvironment env, List args) {
return returnFormula;
}
}
+
+ /** Check if the expression returns a Rational. */
+ private boolean exprIsRational(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);
+ }
+ }
+ // TODO: What about other terms?
+ return false;
+ }
+
+ /** Checks if the k-th argument of the function is a Rational. */
+ private boolean functionTakesRational(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 3f47cc959b..d57d5e8c6e 100644
--- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java
+++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java
@@ -12,17 +12,23 @@
import ap.api.PartialModel;
import ap.api.SimpleAPI;
+import ap.basetypes.IdealInt;
import ap.parser.IAtom;
import ap.parser.IBinFormula;
import ap.parser.IBinJunctor;
+import ap.parser.IBoolLit$;
import ap.parser.IConstant;
import ap.parser.IExpression;
import ap.parser.IFormula;
import ap.parser.IFunApp;
+import ap.parser.IIntLit;
+import ap.parser.IPlus;
import ap.parser.ITerm;
+import ap.parser.ITimes;
import ap.terfor.preds.Predicate;
import ap.theories.arrays.ExtArray;
import ap.theories.arrays.ExtArray.ArraySort;
+import ap.theories.rationals.Rationals;
import ap.types.Sort;
import ap.types.Sort$;
import com.google.common.collect.ArrayListMultimap;
@@ -37,20 +43,21 @@
import java.util.Set;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.sosy_lab.java_smt.basicimpl.AbstractModel;
-import org.sosy_lab.java_smt.basicimpl.AbstractProver;
import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
-import scala.Option;
class PrincessModel extends AbstractModel {
+ private final PrincessAbstractProver prover;
+
private final PartialModel model;
private final SimpleAPI api;
PrincessModel(
- AbstractProver pProver,
+ PrincessAbstractProver pProver,
PartialModel partialModel,
FormulaCreator creator,
SimpleAPI pApi) {
super(pProver, creator);
+ this.prover = pProver;
this.model = partialModel;
this.api = pApi;
}
@@ -72,7 +79,7 @@ public ImmutableList asList() {
// then iterate over the model and generate the assignments
ImmutableSet.Builder assignments = ImmutableSet.builder();
for (Map.Entry entry : asJava(interpretation).entrySet()) {
- if (!isAbbrev(abbrevs, entry.getKey())) {
+ if (!entry.getKey().toString().equals("Rat_denom") && !isAbbrev(abbrevs, entry.getKey())) {
assignments.addAll(getAssignments(entry.getKey(), entry.getValue(), arrays));
}
}
@@ -237,29 +244,72 @@ public String toString() {
return model.toString();
}
- @Override
- public void close() {}
+ /** Tries to determine the Sort of a Term. */
+ private Sort getSort(IExpression pTerm) {
+ // Just using sortof() won't work as Princess may have simplified the original term
+ // FIXME: This may also affect other parts of the code that use sortof()
+ if (pTerm instanceof ITimes) {
+ ITimes times = (ITimes) pTerm;
+ return getSort(times.subterm());
+ } else if (pTerm instanceof IPlus) {
+ IPlus plus = (IPlus) pTerm;
+ return getSort(plus.apply(0));
+ } else if (pTerm instanceof IFormula) {
+ return creator.getBoolType();
+ } else {
+ // TODO: Do we need more cases?
+ return Sort$.MODULE$.sortOf((ITerm) pTerm);
+ }
+ }
- @Override
- protected IExpression evalImpl(IExpression formula) {
- IExpression evaluation = evaluate(formula);
- if (evaluation == null) {
- // fallback: try to simplify the query and evaluate again.
- evaluation = evaluate(creator.getEnv().simplify(formula));
+ /**
+ * Simplify rational values.
+ *
+ * Rewrite a/1 as a, otherwise return the term unchanged
+ */
+ private ITerm simplifyRational(ITerm pTerm) {
+ // TODO: Reduce the term further?
+ // TODO: Also do this for the values in the model?
+ if (Sort$.MODULE$.sortOf(pTerm).equals(creator.getRationalType())
+ && pTerm instanceof IFunApp
+ && ((IFunApp) pTerm).fun().name().equals("Rat_frac")
+ && pTerm.apply(1).equals(new IIntLit(IdealInt.ONE()))) {
+ return Rationals.int2ring((ITerm) pTerm.apply(0));
}
- return evaluation;
+ return pTerm;
}
- @Nullable
- private IExpression evaluate(IExpression formula) {
- if (formula instanceof ITerm) {
- Option out = model.evalToTerm((ITerm) formula);
- return out.isEmpty() ? null : out.get();
- } else if (formula instanceof IFormula) {
- Option out = model.evalExpression(formula);
- return out.isEmpty() ? null : out.get();
+ @Override
+ protected @Nullable IExpression evalImpl(IExpression expr) {
+ // Extending the partial model does not seem to work in Princess if the formula uses rational
+ // variables. To work around this issue we (temporarily) add the formula to the assertion
+ // stack and then repeat the sat-check to get the value.
+ if (expr instanceof ITerm) {
+ ITerm term = (ITerm) expr;
+ api.push();
+ for (IFormula fixed : prover.getEvaluatedTerms()) {
+ api.addAssertion(fixed);
+ }
+ ITerm var = api.createConstant("__tmp_", getSort(term));
+ api.addAssertion(var.$eq$eq$eq(term));
+ api.checkSat(true);
+ ITerm value = simplifyRational(api.evalToTerm(var));
+ api.pop();
+ prover.addEvaluatedTerm(value.$eq$eq$eq(term));
+ return value;
} else {
- throw new AssertionError("unexpected formula: " + formula);
+ IFormula formula = (IFormula) expr;
+ api.push();
+ for (IFormula fixed : prover.getEvaluatedTerms()) {
+ api.addAssertion(fixed);
+ }
+ IFormula var = api.createBooleanVariable("__tmp_");
+ api.addAssertion(var.$less$eq$greater(formula));
+ api.checkSat(true);
+ IFormula value = IBoolLit$.MODULE$.apply(api.eval(var));
+ api.pop();
+ prover.addEvaluatedTerm(value.$less$eq$greater(formula));
+ return value;
}
}
}
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..16a9aa2fd3
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java
@@ -0,0 +1,136 @@
+// 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.basetypes.IdealInt;
+import ap.parser.IExpression;
+import ap.parser.IFunApp;
+import ap.parser.IIntLit;
+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.FormulaType;
+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 ifmgr;
+
+ PrincessRationalFormulaManager(
+ PrincessFormulaCreator pCreator,
+ NonLinearArithmetic pNonLinearArithmetic,
+ PrincessIntegerFormulaManager pIntegerFormulaManager) {
+ super(pCreator, pNonLinearArithmetic);
+ this.ifmgr = pIntegerFormulaManager;
+ }
+
+ @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 ifmgr.isNumeral(fun.apply(0));
+ case "frac":
+ assert fun.fun().arity() == 2;
+ return ifmgr.isNumeral(fun.apply(0)) && ifmgr.isNumeral(fun.apply(1));
+ }
+ }
+ return false;
+ }
+
+ protected IExpression fromInteger(ITerm i) {
+ return PrincessEnvironment.rationalTheory.int2ring(i);
+ }
+
+ @Override
+ protected IExpression makeNumberImpl(long i) {
+ return fromInteger(ifmgr.makeNumberImpl(i));
+ }
+
+ @Override
+ protected IExpression makeNumberImpl(BigInteger i) {
+ return fromInteger(ifmgr.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) {
+ if (pNumber.stripTrailingZeros().scale() <= 0) {
+ // We have an integer number
+ // Return the term for a/1
+ return PrincessEnvironment.rationalTheory.int2ring(
+ ifmgr.makeNumberImpl(pNumber.toBigInteger()));
+ } else {
+ // We have a fraction a/b
+ // Convert the numerator and the divisor and then return the fraction
+ List args =
+ ImmutableList.of(
+ ifmgr.makeNumberImpl(pNumber.unscaledValue()),
+ ifmgr.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 UnsupportedOperationException("floor is not supported in Princess");
+ }
+
+ @Override
+ protected IExpression multiply(IExpression number1, IExpression number2) {
+ FormulaType sort1 = getFormulaCreator().getFormulaType(number1);
+ FormulaType sort2 = getFormulaCreator().getFormulaType(number1);
+
+ IExpression result = PrincessEnvironment.rationalTheory.mul((ITerm) number1, (ITerm) number2);
+
+ if (result instanceof IIntLit && ((IIntLit) result).value().equals(IdealInt.apply(0))) {
+ // If the result is (integer) zero we may have lost our type
+ // Check the type of both arguments and convert the result back to rational if needed
+ if (sort1.isRationalType() || sort2.isRationalType()) {
+ result = PrincessEnvironment.rationalTheory.int2ring((IIntLit) result);
+ }
+ }
+ return result;
+ }
+
+ @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..5f1bf1c717
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java
@@ -0,0 +1,312 @@
+// 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.IExpression;
+import ap.parser.IFormula;
+import ap.parser.IFunApp;
+import ap.parser.ITerm;
+import ap.types.Sort;
+import com.google.common.collect.ImmutableList;
+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);
+ }
+
+ /**
+ * Tries to parse an escaped Unicode character
+ *
+ * Returns the original String if parsing is not possible.
+ */
+ private static String literalOrSkip(String pToken) {
+ String literal;
+ if (pToken.startsWith("\\u{")) {
+ if (pToken.length() > 9 || !pToken.endsWith("}")) {
+ // Abort if there is no closing bracket, or if there are too many digits for the literal
+ // The longest allowed literal is \\u{d5 d4 d3 d2 d1}
+ return pToken;
+ }
+ literal = pToken.substring(3, pToken.length() - 1);
+ } else {
+ if (pToken.length() != 6) {
+ // Abort if there are not exactly 4 digits
+ // The literal must have this form: \\u d3 d2 d1 d0
+ return pToken;
+ }
+ literal = pToken.substring(2);
+ }
+
+ // Try to parse the digits as a (hexadecimal) integer
+ // Abort if there is an error
+ int value;
+ try {
+ value = Integer.parseInt(literal, 16);
+ } catch (NumberFormatException e) {
+ return pToken;
+ }
+
+ // Return the Unicode letter if it fits into a single 16bit character
+ // Otherwise throw an exception as we don't support Unicode characters with more than 4 digits
+ char[] chars = Character.toChars(value);
+ if (chars.length != 1) {
+ throw new IllegalArgumentException();
+ } else {
+ return String.valueOf(chars[0]);
+ }
+ }
+
+ /** Replace escape sequences for Unicode letters with their UTF16 representation. */
+ static String unescapeString(String pInput) {
+ StringBuilder builder = new StringBuilder();
+ while (!pInput.isEmpty()) {
+ // Search for the next escape sequence
+ int start = pInput.indexOf("\\u");
+ if (start == -1) {
+ // Append the rest of the String to the output if there are no more escaped Unicode
+ // characters
+ builder.append(pInput);
+ pInput = "";
+ } else {
+ // Store the prefix up to the escape sequence
+ String prefix = pInput.substring(0, start);
+
+ // Skip ahead and get the escape sequence
+ pInput = pInput.substring(start);
+ String value;
+ if (pInput.charAt(2) == '{') {
+ // Sequence has the form \\u{d5 d4 d3 d2 d1 d0}
+ // Find the closing bracket for the literal:
+ int stop = pInput.indexOf('}');
+ if (stop == -1) {
+ // Use the index right after "\\u{" if there is no closing bracket
+ stop = 2;
+ }
+ value = pInput.substring(0, stop + 1);
+ pInput = pInput.substring(stop + 1);
+ } else {
+ // Sequence has the form \\u d3 d2 d1 d0
+ int stop = 2;
+ while (stop < pInput.length()) {
+ char c = pInput.charAt(stop);
+ if (Character.digit(c, 16) == -1) {
+ break;
+ }
+ stop++;
+ }
+ value = pInput.substring(0, stop);
+ pInput = pInput.substring(stop);
+ }
+
+ // Try to parse the escape sequence to replace it with its 16bit Unicode character
+ // If parsing fails just keep it in the String
+ String nextToken = literalOrSkip(value);
+
+ // Collect the prefix and the (possibly) translated escape sequence
+ builder.append(prefix).append(nextToken);
+ }
+ }
+ return builder.toString();
+ }
+
+ @Override
+ protected IExpression makeStringImpl(String value) {
+ return PrincessEnvironment.stringTheory.string2Term(unescapeString(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) {
+ // just reverse the order
+ return lessThan(pParam2, pParam1);
+ }
+
+ @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) {
+ return new IAtom(PrincessEnvironment.stringTheory.str_$less(), toITermSeq(pParam1, pParam2));
+ }
+
+ @Override
+ protected ITerm length(IExpression pParam) {
+ return new IFunApp(PrincessEnvironment.stringTheory.str_len(), toITermSeq(pParam));
+ }
+
+ @Override
+ protected ITerm concatImpl(List parts) {
+ ITerm result = (ITerm) makeStringImpl("");
+ for (IExpression expr : parts) {
+ result =
+ new IFunApp(
+ PrincessEnvironment.stringTheory.str_$plus$plus(),
+ PrincessEnvironment.toSeq(ImmutableList.of(result, (ITerm) expr)));
+ }
+ return result;
+ }
+
+ @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/solvers/princess/UnicodeEscapeTest.java b/src/org/sosy_lab/java_smt/solvers/princess/UnicodeEscapeTest.java
new file mode 100644
index 0000000000..279902819b
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/princess/UnicodeEscapeTest.java
@@ -0,0 +1,60 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2024 Dirk Beyer
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.solvers.princess;
+
+import static com.google.common.truth.Truth.assertThat;
+import static org.junit.Assert.assertThrows;
+
+import com.google.common.collect.ImmutableList;
+import com.google.common.collect.ImmutableMap;
+import java.util.List;
+import java.util.Map;
+import org.junit.Test;
+
+public class UnicodeEscapeTest {
+ /** Some valid encodings for Unicode characters in SMTLIB2. */
+ Map validCodes =
+ ImmutableMap.of(
+ "\\uabcd", "ꯍ", "\\u{a}", "\n", "\\u{ab}", "«", "\\u{abc}", "઼", "\\u{abcd}", "ꯍ");
+
+ /** Examples of invalid encodings for Unicode characters. */
+ List invalidCodes =
+ ImmutableList.of(
+ "\\uabc", "\\uabcde", "\\u000g", "\\u{}", "\\u{abcdef}", "\\u{g}", "\\u{abcd");
+
+ @Test
+ public void validCodesTest() {
+ for (Map.Entry code : validCodes.entrySet()) {
+ assertThat(PrincessStringFormulaManager.unescapeString(code.getKey()))
+ .isEqualTo(code.getValue());
+ }
+ }
+
+ @Test
+ public void invalidCodesTest() {
+ for (String code : invalidCodes) {
+ // Invalid codes need to be preserved. It is important that we don't match, and simply copy
+ // them over.
+ assertThat(PrincessStringFormulaManager.unescapeString(code)).isEqualTo(code);
+ }
+ }
+
+ @Test
+ public void unsupportedCodesTest() {
+ // We don't support \\u{...} with 5 digits, even though it is legal in SMTLIB, as the code
+ // can't be represented as a single UTF16 character. If such a code is found we expect an
+ // exception to be thrown.
+ assertThrows(
+ IllegalArgumentException.class,
+ () -> PrincessStringFormulaManager.unescapeString("\\u{abcde}"));
+ assertThat(PrincessStringFormulaManager.unescapeString("\\u{abcdg}")).isEqualTo("\\u{abcdg}");
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/test/FormulaClassifierTest.java b/src/org/sosy_lab/java_smt/test/FormulaClassifierTest.java
index 68e0198be0..b256584f56 100644
--- a/src/org/sosy_lab/java_smt/test/FormulaClassifierTest.java
+++ b/src/org/sosy_lab/java_smt/test/FormulaClassifierTest.java
@@ -81,6 +81,11 @@ public void test_QF_AUFLIRA() {
.withMessage("Solver %s does not support mixed integer-real arithmetic", solverToUse())
.that(solverToUse())
.isNotEqualTo(Solvers.OPENSMT);
+ // FIXME: Princess uses quantified variables for the rationals and returns AUFNIRA
+ assume()
+ .withMessage("Solver %s does not support mixed real-array arithmetic", solverToUse())
+ .that(solverToUse())
+ .isNotEqualTo(Solvers.PRINCESS);
requireParser();
requireArrays();
@@ -93,6 +98,13 @@ public void test_QF_AUFLIRA() {
@Test
public void test_QF_AUFNIRA() {
+ // FIXME: Princess uses quantified variables for the rationals and returns AUFNIRA (without the
+ // "QF_" part)
+ assume()
+ .withMessage("Solver %s does not support mixed real-array arithmetic", solverToUse())
+ .that(solverToUse())
+ .isNotEqualTo(Solvers.PRINCESS);
+
requireParser();
requireArrays();
requireIntegers();
diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java
index 3fa91e29bc..beeef9c36b 100644
--- a/src/org/sosy_lab/java_smt/test/ModelTest.java
+++ b/src/org/sosy_lab/java_smt/test/ModelTest.java
@@ -80,7 +80,7 @@ public class ModelTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
FormulaType.getArrayType(IntegerType, IntegerType);
private static final ImmutableList SOLVERS_WITH_PARTIAL_MODEL =
- ImmutableList.of(Solvers.Z3, Solvers.PRINCESS);
+ ImmutableList.of(Solvers.Z3);
@Before
public void setup() {
@@ -2218,6 +2218,12 @@ public void arrayTest4() throws SolverException, InterruptedException {
requireArrays();
requireIntegers();
requireBitvectors();
+
+ assume()
+ .withMessage("Solver runs out memory while generating the model")
+ .that(solverToUse())
+ .isNotEqualTo(Solvers.PRINCESS);
+
BooleanFormula formula = context.getFormulaManager().parse(ARRAY_QUERY_BV);
checkModelIteration(formula, false);
}
@@ -2364,9 +2370,16 @@ public void testGetSmallIntegralRationals1() throws SolverException, Interrupted
@Test
public void testGetRationals1() throws SolverException, InterruptedException {
requireRationals();
+ RationalFormula x = rmgr.makeVariable("x");
+ evaluateInModel(
+ 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(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"))),
+ 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..d51e684806 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,12 +201,20 @@ 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.
assume()
.withMessage("Solver %s does not support division by zero", solverToUse())
.that(solverToUse())
.isNoneOf(Solvers.YICES2, Solvers.OPENSMT);
+ if (formulaType.isRationalType()) {
+ // Division by zero does not work for rationals with Princess.
+ assume()
+ .withMessage("Solver %s does not support division by zero", solverToUse())
+ .that(solverToUse())
+ .isNotEqualTo(Solvers.PRINCESS);
+ }
+
T a = nmgr.makeVariable("a");
T b = nmgr.makeVariable("b");
T zero = nmgr.makeNumber(0);
diff --git a/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java
index 1515133f88..266552557d 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,10 +35,7 @@ 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();
for (double v : SOME_DOUBLES) {
IntegerFormula i = imgr.makeNumber((int) Math.floor(v));
@@ -65,6 +60,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 +73,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 +82,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 +91,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 +100,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 +109,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/SolverAllSatTest.java b/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java
index 0ef9a46b14..49179e5d8f 100644
--- a/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java
+++ b/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java
@@ -221,6 +221,13 @@ public void allSatTest_withQuantifier() throws SolverException, InterruptedExcep
.isNotEqualTo(Solvers.PRINCESS);
}
+ if ("normal".equals(proverEnv)) {
+ assume()
+ .withMessage("solver reports a partial model when using quantifiers")
+ .that(solverToUse())
+ .isNotEqualTo(Solvers.PRINCESS);
+ }
+
// (y = 1)
// & (PRED1 <-> (y = 1))
// & (PRED3 <-> ALL x_0. (3 * x_0 != y))
diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java
index f38248560d..8d126c4dd4 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 5f406a50c0..f59f13330b 100644
--- a/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java
+++ b/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java
@@ -767,6 +767,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();
@@ -787,6 +814,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)");
}
diff --git a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java
index 98bd7e8d4b..49ff66db62 100644
--- a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java
+++ b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java
@@ -96,6 +96,17 @@ private void assertDistinct(StringFormula str1, StringFormula str2)
assertThatFormula(smgr.equal(str1, str2)).isUnsatisfiable();
}
+ private void requireVariableStringLiterals() {
+ // FIXME: Remove once support for operations on non-singleton Strings has been added
+ // See https://github.com/uuverifiers/ostrich/issues/88
+ assume()
+ .withMessage(
+ "Princess currently requires at least one of the arguments to be a "
+ + "singleton string")
+ .that(solverToUse())
+ .isNotEqualTo(Solvers.PRINCESS);
+ }
+
// Tests
@Test
@@ -114,6 +125,8 @@ public void testRegexAll3() throws SolverException, InterruptedException {
@Test
public void testRegexAllChar() throws SolverException, InterruptedException {
+ requireVariableStringLiterals();
+
RegexFormula regexAllChar = smgr.allChar();
assertThatFormula(smgr.in(smgr.makeString("a"), regexAllChar)).isSatisfiable();
@@ -130,11 +143,18 @@ public void testRegexAllChar() throws SolverException, InterruptedException {
@Test
public void testRegexAllCharUnicode() throws SolverException, InterruptedException {
+ requireVariableStringLiterals();
+
RegexFormula regexAllChar = smgr.allChar();
// Single characters.
assertThatFormula(smgr.in(smgr.makeString("\\u0394"), regexAllChar)).isSatisfiable();
- assertThatFormula(smgr.in(smgr.makeString("\\u{1fa6a}"), regexAllChar)).isSatisfiable();
+ if (solverToUse().equals(Solvers.PRINCESS)) {
+ // Princess/Ostrich does not support supplementary unicode character
+ assertThatFormula(smgr.in(smgr.makeString("\\u{fa6a}"), regexAllChar)).isSatisfiable();
+ } else {
+ assertThatFormula(smgr.in(smgr.makeString("\\u{1fa6a}"), regexAllChar)).isSatisfiable();
+ }
// Combining characters are not matched as one character.
assertThatFormula(smgr.in(smgr.makeString("a\\u0336"), regexAllChar)).isUnsatisfiable();
@@ -156,6 +176,8 @@ public void testRegexAllCharUnicode() throws SolverException, InterruptedExcepti
@Test
public void testStringRegex2() throws SolverException, InterruptedException {
+ requireVariableStringLiterals();
+
RegexFormula regex = smgr.concat(smgr.closure(a2z), smgr.makeRegex("ll"), smgr.closure(a2z));
assertThatFormula(smgr.in(hello, regex)).isSatisfiable();
}
@@ -224,6 +246,9 @@ public void testStringConcatEmpty() throws SolverException, InterruptedException
@Test
public void testStringPrefixSuffixConcat() throws SolverException, InterruptedException {
+ // FIXME: Princess will timeout on this test
+ assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS);
+
// check whether "prefix + suffix == concat"
StringFormula prefix = smgr.makeVariable("prefix");
StringFormula suffix = smgr.makeVariable("suffix");
@@ -382,6 +407,8 @@ public void testStringCompare() throws SolverException, InterruptedException {
// TODO regression:
// - CVC5 was able to solve this in v1.0.2, but no longer in v1.0.5
+ requireVariableStringLiterals();
+
StringFormula var1 = smgr.makeVariable("0");
StringFormula var2 = smgr.makeVariable("1");
assertThatFormula(bmgr.and(smgr.lessOrEquals(var1, var2), smgr.greaterOrEquals(var1, var2)))
@@ -790,7 +817,6 @@ public void testCharAtWithSpecialCharacters() throws SolverException, Interrupte
*/
@Test
public void testCharAtWithSpecialCharacters2Byte() throws SolverException, InterruptedException {
-
StringFormula num7 = smgr.makeString("7");
StringFormula u = smgr.makeString("u");
StringFormula curlyOpen2BUnicode = smgr.makeString("\\u{7B}");
@@ -950,6 +976,8 @@ public void testConstStringContains() throws SolverException, InterruptedExcepti
@Test
public void testStringVariableContains() throws SolverException, InterruptedException {
+ requireVariableStringLiterals();
+
StringFormula var1 = smgr.makeVariable("var1");
StringFormula var2 = smgr.makeVariable("var2");
@@ -998,6 +1026,8 @@ public void testStringContainsOtherVariable() throws SolverException, Interrupte
.that(solverToUse())
.isNotEqualTo(Solvers.Z3);
+ requireVariableStringLiterals();
+
StringFormula var1 = smgr.makeVariable("var1");
StringFormula var2 = smgr.makeVariable("var2");
@@ -1061,6 +1091,8 @@ public void testConstStringIndexOf() throws SolverException, InterruptedExceptio
@Test
public void testStringVariableIndexOf() throws SolverException, InterruptedException {
+ requireVariableStringLiterals();
+
StringFormula var1 = smgr.makeVariable("var1");
StringFormula var2 = smgr.makeVariable("var2");
IntegerFormula intVar = imgr.makeVariable("intVar");
@@ -1145,6 +1177,8 @@ public void testStringPrefixImpliesPrefixIndexOf() throws SolverException, Inter
.that(solverToUse())
.isNoneOf(Solvers.Z3, Solvers.CVC4);
+ requireVariableStringLiterals();
+
StringFormula var1 = smgr.makeVariable("var1");
StringFormula var2 = smgr.makeVariable("var2");
@@ -1230,6 +1264,9 @@ public void testStringSubstringOutOfBounds() throws SolverException, Interrupted
@Test
public void testStringVariablesSubstring() throws SolverException, InterruptedException {
+ // FIXME: Princess will timeout on this test
+ assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS);
+
StringFormula var1 = smgr.makeVariable("var1");
StringFormula var2 = smgr.makeVariable("var2");
IntegerFormula intVar1 = imgr.makeVariable("intVar1");
@@ -1310,6 +1347,8 @@ public void testStringVariableReplacePrefix() throws SolverException, Interrupte
@Test
public void testStringVariableReplaceSubstring() throws SolverException, InterruptedException {
+ requireVariableStringLiterals();
+
// I couldn't find stronger constraints in the implication that don't run endlessly.....
StringFormula original = smgr.makeVariable("original");
StringFormula prefix = smgr.makeVariable("prefix");
@@ -1412,6 +1451,8 @@ public void testStringVariableReplaceMiddle() throws SolverException, Interrupte
.that(solverToUse())
.isNoneOf(Solvers.CVC4, Solvers.Z3);
+ requireVariableStringLiterals();
+
StringFormula original = smgr.makeVariable("original");
StringFormula replacement = smgr.makeVariable("replacement");
StringFormula replaced = smgr.makeVariable("replaced");
@@ -1463,6 +1504,8 @@ public void testStringVariableReplaceFront() throws SolverException, Interrupted
.that(solverToUse())
.isNoneOf(Solvers.Z3, Solvers.CVC5);
+ requireVariableStringLiterals();
+
StringFormula var1 = smgr.makeVariable("var1");
StringFormula var2 = smgr.makeVariable("var2");
StringFormula var3 = smgr.makeVariable("var3");
@@ -1524,6 +1567,8 @@ public void testStringVariableReplaceAllConcatedString()
.that(solverToUse())
.isNotEqualTo(Solvers.Z3);
+ requireVariableStringLiterals();
+
// 2 concats is the max number CVC4 supports without running endlessly
for (int numOfConcats = 0; numOfConcats < 3; numOfConcats++) {
@@ -1558,6 +1603,8 @@ public void testStringVariableReplaceAllSubstring() throws SolverException, Inte
.that(solverToUse())
.isNotEqualTo(Solvers.Z3);
+ requireVariableStringLiterals();
+
// I couldn't find stronger constraints in the implication that don't run endlessly.....
StringFormula original = smgr.makeVariable("original");
StringFormula prefix = smgr.makeVariable("prefix");