diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java index 4ea9cf3191..0477b3a32c 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java @@ -13,11 +13,10 @@ import ap.parser.ITerm; import ap.theories.bitvectors.ModuloArithmetic$; import ap.types.Sort; -import ap.types.Sort$; -import com.google.common.base.Preconditions; +import com.google.common.collect.ImmutableList; import java.math.BigInteger; import org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager; -import scala.Option; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessBitvectorToIntegerDeclaration; class PrincessBitvectorFormulaManager extends AbstractBitvectorFormulaManager< @@ -137,29 +136,11 @@ protected IExpression makeBitvectorImpl(int pLength, IExpression pIntegerFormula @Override protected IExpression toIntegerFormulaImpl(IExpression pBVFormula, boolean signed) { - final Sort sort = Sort$.MODULE$.sortOf((ITerm) pBVFormula); - final Option bitWidth = PrincessEnvironment.getBitWidth(sort); - Preconditions.checkArgument(bitWidth.isDefined()); - final int size = (Integer) bitWidth.get(); - - // compute range for integer value, - // example: bitWidth=4 => signed_range=[-8;7] and unsigned_range=[0;15] - final BigInteger min; - final BigInteger max; - if (signed) { - min = BigInteger.ONE.shiftLeft(size - 1).negate(); - max = BigInteger.ONE.shiftLeft(size - 1).subtract(BigInteger.ONE); - } else { - min = BigInteger.ZERO; - max = BigInteger.ONE.shiftLeft(size).subtract(BigInteger.ONE); - } - - ITerm bvInRange = - ModuloArithmetic$.MODULE$.cast2Interval( - IdealInt.apply(min), IdealInt.apply(max), (ITerm) pBVFormula); - - // Princess can not directly convert from BV to INT. However, adding zero helps. Ugly. - return IExpression.i(0).$plus(bvInRange); + var decl = + signed + ? PrincessBitvectorToIntegerDeclaration.SIGNED + : PrincessBitvectorToIntegerDeclaration.UNSIGNED; + return decl.makeApp(getFormulaCreator().getEnv(), ImmutableList.of(pBVFormula)); } @Override @@ -194,10 +175,8 @@ protected IExpression extract(IExpression pNumber, int pMsb, int pLsb) { @Override protected IExpression extend(IExpression pNumber, int pExtensionBits, boolean pSigned) { - if (pSigned) { - return ModuloArithmetic$.MODULE$.sign_extend(pExtensionBits, (ITerm) pNumber); - } else { - return ModuloArithmetic$.MODULE$.zero_extend(pExtensionBits, (ITerm) pNumber); - } + return new PrincessFunctionDeclaration.PrincessBitvectorExtendDeclaration( + pExtensionBits, pSigned) + .makeApp(getFormulaCreator().getEnv(), ImmutableList.of(pNumber)); } } 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 40aeaecb00..c0409b99ec 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -12,6 +12,7 @@ import static scala.collection.JavaConverters.collectionAsScalaIterableConverter; import ap.api.SimpleAPI; +import ap.basetypes.IdealInt; import ap.parameters.GlobalSettings; import ap.parser.BooleanCompactifier; import ap.parser.Environment.EnvironmentException; @@ -22,6 +23,8 @@ import ap.parser.IFunApp; import ap.parser.IFunction; import ap.parser.IIntFormula; +import ap.parser.IIntLit; +import ap.parser.IIntRelation; import ap.parser.IPlus; import ap.parser.ITerm; import ap.parser.ITermITE; @@ -33,7 +36,6 @@ import ap.parser.SMTTypes.SMTType; import ap.terfor.ConstantTerm; import ap.terfor.preds.Predicate; -import ap.theories.arrays.ExtArray; import ap.theories.arrays.ExtArray.ArraySort; import ap.theories.bitvectors.ModuloArithmetic; import ap.theories.rationals.Rationals$; @@ -53,8 +55,6 @@ import java.io.File; import java.io.IOException; import java.io.StringReader; -import java.lang.reflect.InvocationTargetException; -import java.lang.reflect.Method; import java.nio.file.Path; import java.util.ArrayDeque; import java.util.ArrayList; @@ -176,6 +176,8 @@ class PrincessEnvironment { private final Map functionsCache = new HashMap<>(); + private final Map, Map> constArrayCache = new HashMap<>(); + private final int randomSeed; private final @Nullable PathCounterTemplate basicLogfile; private final ShutdownNotifier shutdownNotifier; @@ -337,6 +339,15 @@ public List parseStringToTerms(String s, PrincessFormulaC IFunction fun = ((IFunApp) var).fun(); functionsCache.put(fun.name(), fun); addFunction(fun); + } else if (var instanceof IIntFormula + && ((IIntFormula) var).rel().equals(IIntRelation.EqZero()) + && ((IIntFormula) var).apply(0) instanceof IFunApp) { + // Functions with return type Bool are wrapped in a predicate as (=0 (uf ...)) + IFunction fun = ((IFunApp) var.apply(0)).fun(); + functionsCache.put(fun.name(), fun); + addFunction(fun); + } else { + throw new IllegalArgumentException(); } } return formulas; @@ -581,6 +592,18 @@ static FormulaType getFormulaType(IExpression pFormula) { FormulaType t1 = getFormulaType(plus.left()); FormulaType t2 = getFormulaType(plus.right()); return mergeFormulaTypes(t1, t2); + } else if (pFormula instanceof IFunApp + && ((IFunApp) pFormula).fun().equals(ModuloArithmetic.bv_extract())) { + IIntLit upper = (IIntLit) pFormula.apply(0); + IIntLit lower = (IIntLit) pFormula.apply(1); + IdealInt bwResult = upper.value().$minus(lower.value()); + return FormulaType.getBitvectorTypeWithSize(bwResult.intValue() + 1); + } else if (pFormula instanceof IFunApp + && ((IFunApp) pFormula).fun().equals(ModuloArithmetic.bv_concat())) { + IIntLit upper = (IIntLit) pFormula.apply(0); + IIntLit lower = (IIntLit) pFormula.apply(1); + IdealInt bwResult = upper.value().$plus(lower.value()); + return FormulaType.getBitvectorTypeWithSize(bwResult.intValue()); } else { final Sort sort = Sort$.MODULE$.sortOf((ITerm) pFormula); try { @@ -669,7 +692,14 @@ public IExpression makeVariable(Sort type, String varname) { } } else { if (sortedVariablesCache.containsKey(varname)) { - return sortedVariablesCache.get(varname); + ITerm found = sortedVariablesCache.get(varname); + Preconditions.checkArgument( + getFormulaType(found).equals(getFormulaTypeFromSort(type)), + "Can't declare variable \"%s\" with type %s. It has already been declared with type %s", + varname, + getFormulaTypeFromSort(type), + getFormulaType(found)); + return found; } else { ITerm var = api.createConstant(varname, type); addSymbol(var); @@ -682,6 +712,7 @@ public IExpression makeVariable(Sort type, String varname) { /** This function declares a new functionSymbol with the given argument types and result. */ public IFunction declareFun(String name, Sort returnType, List args) { if (functionsCache.containsKey(name)) { + // FIXME Check that the old declaration has the right type return functionsCache.get(name); } else { IFunction funcDecl = @@ -705,20 +736,32 @@ public ITerm makeStore(ITerm array, ITerm index, ITerm value) { return new IFunApp(arraySort.theory().store(), toSeq(args)); } - public ITerm makeConstArray(ArraySort arraySort, ITerm elseTerm) { - // return new IFunApp(arraySort.theory().const(), elseTerm); // I love Scala! So simple! ;-) - - // Scala uses keywords that are illegal in Java. Thus, we use reflection to access the method. - // TODO we should contact the developers of Princess and ask for a renaming. - final IFunction constArrayOp; - try { - Method constMethod = ExtArray.class.getMethod("const"); - constArrayOp = (IFunction) constMethod.invoke(arraySort.theory()); - } catch (IllegalAccessException | NoSuchMethodException | InvocationTargetException exception) { - throw new RuntimeException(exception); - } + void cacheConstArray(ArraySort arraySort, ITerm elseTerm, ITerm constArray) { + constArrayCache.compute( + getFormulaTypeFromSort(arraySort), + (sort, maps) -> { + if (maps == null) { + maps = new HashMap<>(); + } + maps.putIfAbsent(elseTerm, constArray); + return maps; + }); + } - return new IFunApp(constArrayOp, toSeq(ImmutableList.of(elseTerm))); + public ITerm makeConstArray(ArraySort arraySort, ITerm elseTerm) { + constArrayCache.compute( + getFormulaTypeFromSort(arraySort), + (sort, maps) -> { + if (maps == null) { + maps = new HashMap<>(); + } + maps.computeIfAbsent( + elseTerm, + term -> + new IFunApp(arraySort.theory().constArray(), toSeq(ImmutableList.of(elseTerm)))); + return maps; + }); + return constArrayCache.get(getFormulaTypeFromSort(arraySort)).get(elseTerm); } public boolean hasArrayType(IExpression exp) { 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 6f325cb173..02de968e1d 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -11,10 +11,15 @@ import static com.google.common.base.Preconditions.checkArgument; 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.BOOL_SORT; +import static org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.INTEGER_SORT; 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.ConstantSubstVisitor; +import ap.parser.ExpressionReplacingVisitor; import ap.parser.IAtom; import ap.parser.IBinFormula; import ap.parser.IBinJunctor; @@ -37,22 +42,29 @@ import ap.parser.ITermITE; import ap.parser.ITimes; import ap.parser.IVariable; +import ap.parser.Rewriter; +import ap.terfor.ConstantTerm; import ap.terfor.preds.Predicate; import ap.theories.arrays.ExtArray; import ap.theories.bitvectors.ModuloArithmetic; +import ap.theories.nia.GroebnerMultiplication; import ap.theories.nia.GroebnerMultiplication$; import ap.theories.rationals.Rationals; import ap.types.Sort; import ap.types.Sort$; +import ap.types.Sort.MultipleValueBool$; import com.google.common.base.Preconditions; import com.google.common.collect.HashBasedTable; import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableMap; import com.google.common.collect.ImmutableSet; +import com.google.common.collect.Sets; import com.google.common.collect.Table; import java.util.HashMap; import java.util.LinkedHashMap; import java.util.List; import java.util.Map; +import java.util.Optional; import java.util.Set; import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.api.ArrayFormula; @@ -69,10 +81,18 @@ import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessBitvectorToBitvectorDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessBitvectorToBooleanDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessByExampleDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessConstArrayDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessEquationDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessIFunctionDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessIntegerDivisionDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessIntegerModuloDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessModularCongruenceDeclaration; import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessMultiplyDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessRationalDivisionDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessRationalFloorDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessRationalMultiplyDeclaration; import scala.Enumeration; +import scala.collection.JavaConverters; class PrincessFormulaCreator extends FormulaCreator { @@ -81,8 +101,15 @@ 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"); + // Get the symbol for multiplication + private final IFunction symbolMul = GroebnerMultiplication.mul(); + + // We use a list of patterns to match complex operations like division in the visitor + private final List patterns = precompile(); + static { theoryFunctionKind.put(ModuloArithmetic.bv_concat(), FunctionDeclarationKind.BV_CONCAT); theoryFunctionKind.put(ModuloArithmetic.bv_extract(), FunctionDeclarationKind.BV_EXTRACT); @@ -118,6 +145,8 @@ class PrincessFormulaCreator theoryPredKind.put(ModuloArithmetic.bv_ule(), FunctionDeclarationKind.BV_ULE); theoryPredKind.put(ModuloArithmetic.bv_slt(), FunctionDeclarationKind.BV_SLT); theoryPredKind.put(ModuloArithmetic.bv_sle(), FunctionDeclarationKind.BV_SLE); + theoryPredKind.put(Rationals.lessThan(), FunctionDeclarationKind.LT); + theoryPredKind.put(Rationals.lessThanOrEqual(), FunctionDeclarationKind.LTE); theoryFunctionKind.put(GroebnerMultiplication$.MODULE$.mul(), FunctionDeclarationKind.MUL); @@ -391,18 +420,315 @@ private static boolean isValue(IExpression input) { return false; } + /** Cast integer terms to rational, if needed. */ + private ITerm toReal(ITerm number) { + return getFormulaType(number).isIntegerType() ? Rationals.int2ring(number) : number; + } + + private static class Pair { + private final A a; + private final B b; + + Pair(A pA, B pB) { + a = pA; + b = pB; + } + + A getA() { + return a; + } + + B getB() { + return b; + } + } + + /** Merge two substitutions, returns {@link Optional#empty()} when there is a conflict. */ + private Optional> merge( + Optional> maybeSubst1, Optional> maybeSubst2) { + if (maybeSubst1.isPresent() && maybeSubst2.isPresent()) { + var subst1 = maybeSubst1.orElseThrow(); + var subst2 = maybeSubst2.orElseThrow(); + + ImmutableMap.Builder builder = ImmutableMap.builder(); + for (var k : Sets.union(subst1.keySet(), subst2.keySet())) { + if (subst1.containsKey(k)) { + if (subst2.containsKey(k) && !subst1.get(k).equals(subst2.get(k))) { + return Optional.empty(); + } + builder.put(k, subst1.get(k)); + } else { + builder.put(k, subst2.get(k)); + } + } + return Optional.of(builder.buildOrThrow()); + } else { + return Optional.empty(); + } + } + + /** + * Simple term unification. + * + *

Assumes that the left term is more general. Will return {@link Optional#empty()} if the + * terms can't be unified. Otherwise, returns a substitution for the constant symbols in the left + * term. + */ + private Pair>, IExpression> unify( + IExpression t1, IExpression t2) { + if (t1.equals(t2)) { + return new Pair<>(Optional.of(ImmutableMap.of()), t1); + } else if (t1 instanceof IConstant) { + return new Pair<>(Optional.of(ImmutableMap.of(((IConstant) t1).c(), t2)), t2); + } else if (t1.getClass().equals(t2.getClass()) && t1.length() == t2.length()) { + // Recursively check the subterms + Optional> subst = Optional.of(ImmutableMap.of()); + ImmutableList.Builder terms = ImmutableList.builder(); + for (var i = 0; i < t1.length(); i++) { + Pair>, IExpression> r = + unify(t1.apply(i), t2.apply(i)); + subst = merge(subst, r.getA()); + + if (subst.isEmpty()) { + return new Pair<>(Optional.empty(), t1); + } + terms.add(r.getB()); + } + + // Check if the left term is equal to the right after the subtrees were unified + IExpression t = t1.update(toSeq(terms.build())); + if (t.equals(t2)) { + return new Pair<>(subst, t2); + } + } + return new Pair<>(Optional.empty(), t1); + } + + /** + * Rewrite terms of the form ((_ ITimes k) b) as (multiply (Expression.i k) b) + * . + * + *

This will later allow us to replace the first argument with a variable + */ + private IExpression rewriteMult(IExpression t) { + return Rewriter.rewrite( + t, + v -> { + if (v instanceof ITimes) { + var times = (ITimes) v; + return new IFunApp( + symbolMul, toSeq(ImmutableList.of(IExpression.i(times.coeff()), times.subterm()))); + } else { + return v; + } + }); + } + + /** + * Rewrite negative integer literals as -1 * a. + * + *

Will skip -1 terms while rewriting + */ + private IExpression rewriteNegated(IExpression t) { + return Rewriter.rewrite( + t, + v -> { + if (v instanceof IIntLit) { + var lit = ((IIntLit) v); + if (!lit.value().isUnit() && lit.value().signum() < 0) { + return new ITimes(IdealInt.apply(-1), IExpression.abs(lit)); + } + } + return v; + }); + } + + /** + * A pattern, consisting of an operation, it's arguments, and the resulting Princess term. + * + *

The princess term will be generalized, and by matching it to a given formula one can invert + * the operation and derive the original arguments. + */ + private static class Pattern { + private final PrincessFunctionDeclaration decl; + private final List args; + private final IExpression term; + + Pattern(PrincessFunctionDeclaration pDecl, List pArgs, IExpression pTerm) { + decl = pDecl; + args = pArgs; + term = pTerm; + } + } + + private Pattern buildPattern(PrincessFunctionDeclaration pDeclaration, List pArgs) { + return buildPattern(pDeclaration, pArgs, false); + } + + /** + * Helper function to build patterns. + * + *

If the last argument is set to true, we will generalize any constant terms in + * the arguments. + */ + private Pattern buildPattern( + PrincessFunctionDeclaration pDeclaration, List pArgs, boolean pFinal) { + var term = rewriteNegated(rewriteMult(pDeclaration.makeApp(environment, pArgs))); + if (pFinal) { + ImmutableList.Builder builder = ImmutableList.builder(); + for (var c : pArgs) { + if (c instanceof IConstant) { + // If the argument is already a variable, just keep it + builder.add(c); + } else if (c instanceof ITimes) { + // If it's a term (c * t), where c is an integer coefficient, and t is another integer + // literal, we replace t in (c * t) with a new variable + // Specifically, this can be used to generalize negative integer constants by first + // shifting the minus sign outside, and then replacing the nested integer term + var times = (ITimes) c; + if (times.apply(0) instanceof IIntLit) { + var newVar = + (ITerm) makeVariable(INTEGER_SORT, "@" + Integer.toUnsignedString(c.hashCode())); + term = ExpressionReplacingVisitor.apply(term, times.apply(0), newVar); + builder.add(new ITimes(times.coeff(), newVar)); + } else { + throw new IllegalArgumentException(); + } + } else { + // If we have an integer constant as argument, replace it with a new variable and + // update the term + var newVar = + (ITerm) makeVariable(INTEGER_SORT, "@" + Integer.toUnsignedString(c.hashCode())); + term = ExpressionReplacingVisitor.apply(term, c, newVar); + builder.add(newVar); + } + } + return new Pattern(pDeclaration, builder.build(), term); + } else { + return new Pattern(pDeclaration, pArgs, term); + } + } + + private List precompile() { + // Define two variable to match integer arguments + ITerm symbolInt1 = (ITerm) makeVariable(PrincessEnvironment.INTEGER_SORT, "@1integer"); + ITerm symbolInt2 = (ITerm) makeVariable(PrincessEnvironment.INTEGER_SORT, "@2integer"); + + // Define two variables for real arguments + ITerm symbolReal1 = (ITerm) makeVariable(PrincessEnvironment.FRACTION_SORT, "@1real"); + ITerm symbolReal2 = (ITerm) makeVariable(PrincessEnvironment.FRACTION_SORT, "@2real"); + + return ImmutableList.of( + // Rational.divide + buildPattern( + PrincessRationalDivisionDeclaration.INSTANCE, + ImmutableList.of(symbolReal1, toReal(symbolInt2)), + true), + buildPattern( + PrincessRationalDivisionDeclaration.INSTANCE, + ImmutableList.of(symbolReal1, symbolReal2)), + + // Rational.floor + buildPattern(PrincessRationalFloorDeclaration.INSTANCE, ImmutableList.of(symbolReal1)), + + // Integer.divide + buildPattern( + PrincessIntegerDivisionDeclaration.INSTANCE, + ImmutableList.of(IExpression.i(2), symbolInt2), + true), + buildPattern( + PrincessIntegerDivisionDeclaration.INSTANCE, + ImmutableList.of(symbolInt1, IExpression.i(2))), + buildPattern( + PrincessIntegerDivisionDeclaration.INSTANCE, + ImmutableList.of(symbolInt1, IExpression.i(2).unary_$minus())), + buildPattern( + PrincessIntegerDivisionDeclaration.INSTANCE, + ImmutableList.of(symbolInt1, IExpression.i(3)), + true), + buildPattern( + PrincessIntegerDivisionDeclaration.INSTANCE, + ImmutableList.of(symbolInt1, IExpression.i(3).unary_$minus()), + true), + + // Integer.modulo + buildPattern( + PrincessIntegerModuloDeclaration.INSTANCE, ImmutableList.of(symbolInt1, symbolInt2)), + buildPattern( + PrincessIntegerModuloDeclaration.INSTANCE, + ImmutableList.of(symbolInt1, IExpression.i(2))), + buildPattern( + PrincessIntegerModuloDeclaration.INSTANCE, + ImmutableList.of(symbolInt1, IExpression.i(2).unary_$minus()), + true), + buildPattern( + PrincessIntegerModuloDeclaration.INSTANCE, + ImmutableList.of(symbolInt1, IExpression.i(3)), + true), + buildPattern( + PrincessIntegerModuloDeclaration.INSTANCE, + ImmutableList.of(symbolInt1, IExpression.i(3).unary_$minus()), + true), + + // Integer.modularCongruence + buildPattern( + PrincessModularCongruenceDeclaration.INSTANCE, + ImmutableList.of(symbolInt1, symbolInt2, IExpression.i(3)), + true)); + } + @SuppressWarnings("deprecation") @Override public R visit(FormulaVisitor visitor, final Formula f, final IExpression input) { - if (isValue(input)) { - return visitor.visitConstant(f, convertValue(input)); + IExpression re = rewriteNegated(rewriteMult(input)); - } else if (input instanceof IQuantified) { - return visitQuantifier(visitor, (BooleanFormula) f, (IQuantified) input); + // Check if one of the patterns matches + for (Pattern p : patterns) { + Optional> subst = unify(p.term, re).getA(); - } else if (input instanceof IVariable) { - // variable bound by a quantifier - return visitor.visitBoundVariable(f, ((IVariable) input).index()); + if (subst.isPresent()) { + ImmutableList.Builder args = ImmutableList.builder(); + ImmutableList.Builder> sorts = ImmutableList.builder(); + + for (IExpression arg : p.args) { + ImmutableMap.Builder builder = ImmutableMap.builder(); + for (var entry : subst.orElseThrow().entrySet()) { + builder.put(entry.getKey(), (ITerm) entry.getValue()); + } + IExpression updated = + ConstantSubstVisitor.apply(arg, JavaConverters.asScala(builder.buildOrThrow())); + updated = + Rewriter.rewrite( + updated, + v -> { + if (v instanceof ITimes) { + var times = (ITimes) v; + if (times.apply(0) instanceof IIntLit) { + var lit = (IIntLit) times.apply(0); + return IExpression.i(times.coeff().$times(lit.value())); + } + } + return v; + }); + + args.add(encapsulateWithTypeOf(updated)); + sorts.add(getFormulaType(updated)); + } + + return visitor.visitFunction( + f, + args.build(), + FunctionDeclarationImpl.of( + p.decl.getName(), p.decl.getKind(), sorts.build(), getFormulaType(f), p.decl)); + } + } + + if (isValue(input)) { + return visitor.visitConstant(encapsulateWithTypeOf(input), convertValue(input)); + } + if (input instanceof IQuantified) { + // Is it a quantifier? + return visitQuantifier(visitor, (BooleanFormula) f, (IQuantified) input); } else if (((input instanceof IAtom) && asJavaCollection(((IAtom) input).args()).isEmpty()) || input instanceof IConstant) { @@ -410,7 +736,8 @@ public R visit(FormulaVisitor visitor, final Formula f, final IExpression return visitor.visitFreeVariable(f, input.toString()); } else if (input instanceof ITimes) { - // Princess encodes multiplication as "linear coefficient and factor" with arity 1. + // Princess encodes nonlinear multiplication as (coefficient* t), where "coefficient" is + // an integer constant and "t" is the only subterm assert input.length() == 1; ITimes multiplication = (ITimes) input; @@ -491,7 +818,15 @@ public R visit(FormulaVisitor visitor, final Formula f, final IExpression if (kind == FunctionDeclarationKind.UF) { solverDeclaration = new PrincessIFunctionDeclaration(((IFunApp) input).fun()); } else if (kind == FunctionDeclarationKind.MUL) { - solverDeclaration = PrincessMultiplyDeclaration.INSTANCE; + if (getFormulaType(input.apply(0)).isRationalType()) { + solverDeclaration = PrincessRationalMultiplyDeclaration.INSTANCE; + } else if (getFormulaType(input.apply(0)).isIntegerType()) { + solverDeclaration = PrincessMultiplyDeclaration.INSTANCE; + } else { + throw new IllegalArgumentException(); + } + } else if (kind == FunctionDeclarationKind.CONST) { + solverDeclaration = new PrincessConstArrayDeclaration(environment, (IFunApp) input); } else { solverDeclaration = new PrincessByExampleDeclaration(input); } @@ -600,19 +935,14 @@ private FunctionDeclarationKind getDeclarationKind(IExpression input) { return FunctionDeclarationKind.CONST; } else if (fun == ModuloArithmetic.mod_cast()) { return FunctionDeclarationKind.OTHER; - } else if (fun == ModuloArithmetic.int_cast()) { - return FunctionDeclarationKind.OTHER; + } else if (((IFunApp) input).fun().equals(Rationals.fromRing())) { + return FunctionDeclarationKind.TO_REAL; } else { return FunctionDeclarationKind.UF; } } else if (input instanceof IAtom) { final Predicate pred = ((IAtom) input).pred(); - final FunctionDeclarationKind theoryKind = theoryPredKind.get(pred); - if (theoryKind != null) { - return theoryKind; - } else { - return FunctionDeclarationKind.UF; - } + return theoryPredKind.getOrDefault(pred, FunctionDeclarationKind.UF); } else if (isBinaryFunction(input, IBinJunctor.And())) { return FunctionDeclarationKind.AND; } else if (isBinaryFunction(input, IBinJunctor.Or())) { @@ -632,8 +962,11 @@ private FunctionDeclarationKind getDeclarationKind(IExpression input) { IIntFormula f = (IIntFormula) input; if (f.rel().equals(IIntRelation.EqZero())) { final Sort sort = Sort$.MODULE$.sortOf(((IIntFormula) input).t()); - if (sort == PrincessEnvironment.BOOL_SORT) { - // this is really a Boolean formula, it has to be UF + if (sort == Sort.MultipleValueBool$.MODULE$) { + // Princess does not allow UFs to have return sort 'Bool' + // Instead, the function returns 'MultiplyValueBool' which is really an integer. The + // predicate (=0 (uf ...)) is then wrapped around the function application to get a + // (boolean) formula return FunctionDeclarationKind.UF; } else if (sort == PrincessEnvironment.INTEGER_SORT) { return FunctionDeclarationKind.EQ_ZERO; @@ -660,7 +993,9 @@ private static boolean isBinaryFunction(IExpression t, Enumeration.Value val) { @Override public PrincessFunctionDeclaration declareUFImpl( String pName, Sort pReturnType, List args) { - return new PrincessIFunctionDeclaration(environment.declareFun(pName, pReturnType, args)); + return new PrincessIFunctionDeclaration( + environment.declareFun( + pName, pReturnType.equals(BOOL_SORT) ? MultipleValueBool$.MODULE$ : pReturnType, args)); } @Override 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 670d2f1521..f1edd7cb49 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java @@ -24,14 +24,22 @@ import ap.parser.ITermITE; import ap.terfor.ConstantTerm; import ap.terfor.preds.Predicate; +import ap.theories.arrays.ExtArray.ArraySort; +import ap.theories.bitvectors.ModuloArithmetic$; import ap.theories.nia.GroebnerMultiplication; +import ap.theories.rationals.Rationals; import ap.types.MonoSortedIFunction; import ap.types.Sort; import ap.types.Sort$; +import ap.types.Sort.MultipleValueBool$; import ap.types.SortedConstantTerm; import ap.types.SortedIFunction$; +import com.google.common.base.Preconditions; +import java.math.BigInteger; import java.util.ArrayList; import java.util.List; +import org.sosy_lab.java_smt.api.FunctionDeclarationKind; +import scala.Option; import scala.collection.immutable.Seq; /** @@ -44,7 +52,11 @@ abstract class PrincessFunctionDeclaration { private PrincessFunctionDeclaration() {} - abstract IExpression makeApp(PrincessEnvironment environment, List args); + public abstract IExpression makeApp(PrincessEnvironment environment, List args); + + public abstract String getName(); + + public abstract FunctionDeclarationKind getKind(); private abstract static class AbstractDeclaration extends PrincessFunctionDeclaration { @@ -65,7 +77,7 @@ public boolean equals(Object o) { } @Override - abstract IExpression makeApp(PrincessEnvironment env, List args); + public abstract IExpression makeApp(PrincessEnvironment env, List args); @Override public int hashCode() { @@ -112,7 +124,7 @@ public IExpression makeApp(PrincessEnvironment env, List args) { Sort returnType = SortedIFunction$.MODULE$.iResultSort(declarationItem, returnFormula.args()); // boolean term, so we have to use the fun-applier instead of the function itself - if (returnType == PrincessEnvironment.BOOL_SORT) { + if (returnType == MultipleValueBool$.MODULE$) { BooleanFunApplier ap = new BooleanFunApplier(declarationItem); return ap.apply(argsBuf); } else { @@ -149,6 +161,16 @@ private boolean functionTakesRational(Integer index) { } return false; } + + @Override + public String getName() { + return declarationItem.name(); + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.UF; + } } static class PrincessByExampleDeclaration extends AbstractDeclaration { @@ -161,6 +183,40 @@ static class PrincessByExampleDeclaration extends AbstractDeclaration args) { return declarationItem.update(toSeq(args)); } + + @Override + public String getName() { + throw new UnsupportedOperationException(); + } + + @Override + public FunctionDeclarationKind getKind() { + throw new UnsupportedOperationException(); + } + } + + static class PrincessConstArrayDeclaration extends AbstractDeclaration { + + PrincessConstArrayDeclaration(PrincessEnvironment env, IFunApp pArray) { + super((ArraySort) Sort$.MODULE$.sortOf(pArray)); + env.cacheConstArray(declarationItem, pArray.apply(0), pArray); + } + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 1); + return env.makeConstArray(declarationItem, (ITerm) args.get(0)); + } + + @Override + public String getName() { + return "const"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.CONST; + } } static class PrincessBitvectorToBooleanDeclaration extends AbstractDeclaration { @@ -185,6 +241,16 @@ public IExpression makeApp(PrincessEnvironment env, List args) { return new IAtom(declarationItem, toSeq(newArgs)); } + + @Override + public String getName() { + throw new UnsupportedOperationException(); + } + + @Override + public FunctionDeclarationKind getKind() { + throw new UnsupportedOperationException(); + } } static class PrincessBitvectorToBitvectorDeclaration extends AbstractDeclaration { @@ -209,6 +275,16 @@ public IExpression makeApp(PrincessEnvironment env, List args) { return new IFunApp(declarationItem, toSeq(newArgs)); } + + @Override + public String getName() { + throw new UnsupportedOperationException(); + } + + @Override + public FunctionDeclarationKind getKind() { + throw new UnsupportedOperationException(); + } } static class PrincessEquationDeclaration extends PrincessFunctionDeclaration { @@ -222,6 +298,100 @@ public IExpression makeApp(PrincessEnvironment env, List args) { checkArgument(args.size() == 2); return ((ITerm) args.get(0)).$eq$eq$eq((ITerm) args.get(1)); } + + @Override + public String getName() { + return "="; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.EQ; + } + } + + static class PrincessBitvectorToIntegerDeclaration extends PrincessFunctionDeclaration { + static final PrincessBitvectorToIntegerDeclaration SIGNED = + new PrincessBitvectorToIntegerDeclaration(true) {}; + static final PrincessBitvectorToIntegerDeclaration UNSIGNED = + new PrincessBitvectorToIntegerDeclaration(false) {}; + + private final boolean signed; + + private PrincessBitvectorToIntegerDeclaration(boolean pSigned) { + signed = pSigned; + } + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 1); + ITerm bvFormula = (ITerm) args.get(0); + + final Sort sort = Sort$.MODULE$.sortOf(bvFormula); + final Option bitWidth = PrincessEnvironment.getBitWidth(sort); + Preconditions.checkArgument(bitWidth.isDefined()); + final int size = (Integer) bitWidth.get(); + + // compute range for integer value, + // example: bitWidth=4 => signed_range=[-8;7] and unsigned_range=[0;15] + final BigInteger min; + final BigInteger max; + if (signed) { + min = BigInteger.ONE.shiftLeft(size - 1).negate(); + max = BigInteger.ONE.shiftLeft(size - 1).subtract(BigInteger.ONE); + } else { + min = BigInteger.ZERO; + max = BigInteger.ONE.shiftLeft(size).subtract(BigInteger.ONE); + } + + ITerm bvInRange = + ModuloArithmetic$.MODULE$.cast2Interval( + IdealInt.apply(min), IdealInt.apply(max), bvFormula); + + return ModuloArithmetic$.MODULE$.cast2Int(bvInRange); + } + + @Override + public String getName() { + return signed ? "sbv_to_int" : "ubv_to_int"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.OTHER; + } + } + + static class PrincessBitvectorExtendDeclaration extends PrincessFunctionDeclaration { + private final int extensionBits; + private final boolean signed; + + PrincessBitvectorExtendDeclaration(int pExtensionBits, boolean pSigned) { + extensionBits = pExtensionBits; + signed = pSigned; + } + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 1); + if (signed) { + return ModuloArithmetic$.MODULE$.sign_extend(extensionBits, (ITerm) args.get(0)); + } else { + return ModuloArithmetic$.MODULE$.zero_extend(extensionBits, (ITerm) args.get(0)); + } + } + + @Override + public String getName() { + return signed ? "sign_extend" : "zero_extend"; + } + + @Override + public FunctionDeclarationKind getKind() { + return signed + ? FunctionDeclarationKind.BV_SIGN_EXTENSION + : FunctionDeclarationKind.BV_ZERO_EXTENSION; + } } static class PrincessMultiplyDeclaration extends PrincessFunctionDeclaration { @@ -235,5 +405,162 @@ public IExpression makeApp(PrincessEnvironment env, List args) { checkArgument(args.size() == 2); return GroebnerMultiplication.mult((ITerm) args.get(0), (ITerm) args.get(1)); } + + @Override + public String getName() { + return "mul"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.MUL; + } + } + + static class PrincessRationalMultiplyDeclaration extends PrincessFunctionDeclaration { + + static final PrincessRationalMultiplyDeclaration INSTANCE = + new PrincessRationalMultiplyDeclaration() {}; + + private PrincessRationalMultiplyDeclaration() {} + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 2); + return Rationals.mul((ITerm) args.get(0), (ITerm) args.get(1)); + } + + @Override + public String getName() { + return "mul"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.MUL; + } + } + + static class PrincessRationalDivisionDeclaration extends PrincessFunctionDeclaration { + static final PrincessRationalDivisionDeclaration INSTANCE = + new PrincessRationalDivisionDeclaration() {}; + + private PrincessRationalDivisionDeclaration() {} + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 2); + // SMT-LIB allows division by zero, so we use divWithSpecialZero here. + // If the divisor is zero, divWithSpecialZero will evaluate to a unary UF `ratDivZero`, + // otherwise it is the normal division + return Rationals.divWithSpecialZero((ITerm) args.get(0), (ITerm) args.get(1)); + } + + @Override + public String getName() { + return "div"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.DIV; + } + } + + static class PrincessRationalFloorDeclaration extends PrincessFunctionDeclaration { + static final PrincessRationalFloorDeclaration INSTANCE = + new PrincessRationalFloorDeclaration() {}; + + private PrincessRationalFloorDeclaration() {} + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 1); + return Rationals.ring2int((ITerm) args.get(0)); + } + + @Override + public String getName() { + return "floor"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.FLOOR; + } + } + + static class PrincessIntegerDivisionDeclaration extends PrincessFunctionDeclaration { + static final PrincessIntegerDivisionDeclaration INSTANCE = + new PrincessIntegerDivisionDeclaration() {}; + + private PrincessIntegerDivisionDeclaration() {} + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 2); + return GroebnerMultiplication.eDivWithSpecialZero((ITerm) args.get(0), (ITerm) args.get(1)); + } + + @Override + public String getName() { + return "div"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.DIV; + } + } + + static class PrincessIntegerModuloDeclaration extends PrincessFunctionDeclaration { + static final PrincessIntegerModuloDeclaration INSTANCE = + new PrincessIntegerModuloDeclaration() {}; + + private PrincessIntegerModuloDeclaration() {} + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 2); + return GroebnerMultiplication.eModWithSpecialZero((ITerm) args.get(0), (ITerm) args.get(1)); + } + + @Override + public String getName() { + return "mod"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.MODULO; + } + } + + static class PrincessModularCongruenceDeclaration extends PrincessFunctionDeclaration { + static final PrincessModularCongruenceDeclaration INSTANCE = + new PrincessModularCongruenceDeclaration() {}; + + private PrincessModularCongruenceDeclaration() {} + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 3); + var t1 = (ITerm) args.get(0); + var t2 = (ITerm) args.get(1); + var t3 = (ITerm) args.get(2); + return IExpression.ex( + IExpression.eqZero( + t1.$minus(t2).$plus(GroebnerMultiplication.mult(IExpression.v(0), t3)))); + } + + @Override + public String getName() { + return "div"; + } + + @Override + public FunctionDeclarationKind getKind() { + return FunctionDeclarationKind.OTHER; + } } } 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 a26011bdde..c1df5497aa 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java @@ -84,7 +84,12 @@ 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 (!entry.getKey().toString().equals("Rat_denom") && !isAbbrev(abbrevs, entry.getKey())) { + if (!entry.getKey().toString().equals("Rat_denom") + && !isAbbrev(abbrevs, entry.getKey()) + && !(entry.getKey() instanceof IAtom + && ((IAtom) entry.getKey()).pred().name().equals("arrayConstant")) + && !(entry.getKey() instanceof IFunApp + && ((IFunApp) entry.getKey()).fun().name().equals("valueAlmostEverywhere"))) { assignments.addAll(getAssignments(entry.getKey(), entry.getValue(), arrays)); } } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java index 85fbeb245e..33da542bce 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java @@ -22,6 +22,9 @@ 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; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessRationalDivisionDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessRationalFloorDeclaration; +import org.sosy_lab.java_smt.solvers.princess.PrincessFunctionDeclaration.PrincessRationalMultiplyDeclaration; public class PrincessRationalFormulaManager extends PrincessNumeralFormulaManager @@ -110,7 +113,8 @@ protected ITerm toType(IExpression param) { @Override protected IExpression floor(IExpression number) { - return Rationals.ring2int((ITerm) number); + return PrincessRationalFloorDeclaration.INSTANCE.makeApp( + getFormulaCreator().getEnv(), ImmutableList.of(number)); } @Override @@ -130,15 +134,14 @@ protected ITerm subtract(IExpression number1, IExpression number2) { @Override protected IExpression multiply(IExpression number1, IExpression number2) { - return Rationals.mul(toType(number1), toType(number2)); + return PrincessRationalMultiplyDeclaration.INSTANCE.makeApp( + getFormulaCreator().getEnv(), ImmutableList.of(toType(number1), toType(number2))); } @Override protected IExpression divide(IExpression number1, IExpression number2) { - // SMT-LIB allows division by zero, so we use divWithSpecialZero here. - // If the divisor is zero, divWithSpecialZero will evaluate to a unary UF `ratDivZero`, - // otherwise it is the normal division - return Rationals.divWithSpecialZero(toType(number1), toType(number2)); + return PrincessRationalDivisionDeclaration.INSTANCE.makeApp( + getFormulaCreator().getEnv(), ImmutableList.of(toType(number1), toType(number2))); } @Override