From ccc281acbe450bdfbf658ae85200b10af28a9b5d Mon Sep 17 00:00:00 2001 From: Alejandro Serrano Date: Mon, 6 Dec 2021 11:34:55 +0100 Subject: [PATCH 001/103] Start working on string theory for Princess --- .../basicimpl/AbstractBaseFormulaManager.java | 2 +- .../AbstractStringFormulaManager.java | 4 +- .../solvers/princess/PrincessEnvironment.java | 23 +- .../princess/PrincessFormulaCreator.java | 55 ++++- .../princess/PrincessFormulaManager.java | 5 +- .../princess/PrincessSolverContext.java | 5 +- .../PrincessStringFormulaManager.java | 216 ++++++++++++++++++ 7 files changed, 301 insertions(+), 9 deletions(-) create mode 100644 src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractBaseFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractBaseFormulaManager.java index ad8a650b5a..4890fb6a61 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractBaseFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractBaseFormulaManager.java @@ -30,7 +30,7 @@ protected final FormulaCreator getFormulaC return formulaCreator; } - final TFormulaInfo extractInfo(Formula pBits) { + protected final TFormulaInfo extractInfo(Formula pBits) { return getFormulaCreator().extractInfo(pBits); } diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java index 12efe42c95..fbf17b66b5 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java @@ -32,11 +32,11 @@ protected AbstractStringFormulaManager( super(pCreator); } - private StringFormula wrapString(TFormulaInfo formulaInfo) { + protected StringFormula wrapString(TFormulaInfo formulaInfo) { return getFormulaCreator().encapsulateString(formulaInfo); } - private RegexFormula wrapRegex(TFormulaInfo formulaInfo) { + protected RegexFormula wrapRegex(TFormulaInfo formulaInfo) { return getFormulaCreator().encapsulateRegex(formulaInfo); } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java index a53b362435..72af599a9d 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -31,6 +31,8 @@ import ap.terfor.preds.Predicate; import ap.theories.ExtArray; import ap.theories.bitvectors.ModuloArithmetic; +import ap.theories.strings.SeqStringTheory; +import ap.theories.strings.SeqStringTheoryBuilder; import ap.types.Sort; import ap.types.Sort$; import ap.types.Sort.MultipleValueBool$; @@ -100,6 +102,18 @@ 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 int STRING_ALPHABET_SIZE = 500; + static SeqStringTheory stringTheory; + static { + SeqStringTheoryBuilder builder = new SeqStringTheoryBuilder(); + builder.setAlphabetSize(STRING_ALPHABET_SIZE); + stringTheory = builder.theory(); + } + + public static final Sort STRING_SORT = stringTheory.StringSort(); + public static final Sort REGEX_SORT = stringTheory.RegexSort(); @Option(secure = true, description = "log all queries as Princess-specific Scala code") private boolean logAllQueriesAsScala = false; @@ -512,7 +526,8 @@ 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); } } @@ -524,8 +539,12 @@ static FormulaType getFormulaType(IExpression pFormula) { 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 == PrincessEnvironment.STRING_SORT) { + return FormulaType.StringType; + } else if (sort == PrincessEnvironment.REGEX_SORT) { + return FormulaType.RegexType; } else if (sort instanceof ExtArray.ArraySort) { Seq indexSorts = ((ExtArray.ArraySort) sort).theory().indexSorts(); Sort elementSort = ((ExtArray.ArraySort) sort).theory().objSort(); 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 d1aef66645..3fe1d5da3f 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -42,6 +42,8 @@ import ap.theories.ExtArray; import ap.theories.bitvectors.ModuloArithmetic; import ap.theories.nia.GroebnerMultiplication$; +import ap.theories.strings.SeqStringTheory; +import ap.theories.strings.SeqStringTheoryBuilder; import ap.types.Sort; import ap.types.Sort$; import com.google.common.collect.HashBasedTable; @@ -108,6 +110,54 @@ 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_char(), + 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_in_re(), + FunctionDeclarationKind.STR_IN_RE); } /** @@ -121,7 +171,9 @@ 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, + null, + PrincessEnvironment.STRING_SORT, PrincessEnvironment.REGEX_SORT); } @Override @@ -178,6 +230,7 @@ public Sort getArrayType(Sort pIndexType, Sort pElementType) { return result; } + @SuppressWarnings("unchecked") @Override public FormulaType getFormulaType(final T pFormula) { 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 fd599418d0..fa39ec7afd 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java @@ -32,7 +32,8 @@ final class PrincessFormulaManager PrincessIntegerFormulaManager pIntegerManager, PrincessBitvectorFormulaManager pBitpreciseManager, PrincessArrayFormulaManager pArrayManager, - PrincessQuantifiedFormulaManager pQuantifierManager) { + PrincessQuantifiedFormulaManager pQuantifierManager, + PrincessStringFormulaManager pStringManager) { super( pCreator, pFunctionManager, @@ -44,7 +45,7 @@ final class PrincessFormulaManager pQuantifierManager, pArrayManager, null, - null); + pStringManager); creator = pCreator; } 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 d2544a4c8e..996e639f6c 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java @@ -56,6 +56,8 @@ public static SolverContext create( PrincessArrayFormulaManager arrayTheory = new PrincessArrayFormulaManager(creator); PrincessQuantifiedFormulaManager quantifierTheory = new PrincessQuantifiedFormulaManager(creator); + PrincessStringFormulaManager stringTheory = + new PrincessStringFormulaManager(creator); PrincessFormulaManager manager = new PrincessFormulaManager( creator, @@ -64,7 +66,8 @@ public static SolverContext create( integerTheory, 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..dcec8e205f --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java @@ -0,0 +1,216 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2021 Alejandro SerranoMena +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.solvers.princess; + +import ap.parser.IAtom; +import ap.parser.IBinFormula; +import ap.parser.IBinJunctor; +import ap.parser.IExpression; +import ap.parser.IFormula; +import ap.parser.IFunApp; +import ap.parser.INot; +import ap.parser.ITerm; +import ap.types.Sort; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; +import org.sosy_lab.java_smt.api.RegexFormula; +import org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager; +import scala.collection.immutable.Seq; + +public class PrincessStringFormulaManager + extends AbstractStringFormulaManager< + IExpression, Sort, PrincessEnvironment, PrincessFunctionDeclaration> { + + PrincessStringFormulaManager(PrincessFormulaCreator pCreator) { + super(pCreator); + } + + static Seq toSeq(List exprs) { + ArrayList result = new ArrayList(); + for (IExpression expr : exprs) result.add((ITerm)expr); + return PrincessEnvironment.toSeq(result); + } + + static Seq toSeq(IExpression... exprs) { + return toSeq(Arrays.asList(exprs)); + } + + @Override + protected IExpression makeStringImpl(String value) { + return PrincessEnvironment.stringTheory.string2Term(value); + } + + @Override + protected IExpression makeVariableImpl(String pVar) { + Sort t = getFormulaCreator().getStringType(); + return getFormulaCreator().makeVariable(t, pVar); + } + + @Override + protected IFormula equal(IExpression pParam1, IExpression pParam2) { + return ((ITerm) pParam1).$eq$eq$eq((ITerm) pParam2); + } + + @Override + protected IFormula greaterThan(IExpression pParam1, IExpression pParam2) { + IFormula leq = greaterOrEquals(pParam1, pParam2); + IFormula eq = equal(pParam1, pParam2); + return new IBinFormula(IBinJunctor.And(), leq, new INot(eq)); + } + + @Override + protected IFormula lessOrEquals(IExpression pParam1, IExpression pParam2) { + return new IAtom(PrincessEnvironment.stringTheory.str_$less$eq(), toSeq(pParam1, pParam2)); + } + + @Override + protected IFormula greaterOrEquals(IExpression pParam1, IExpression pParam2) { + // just reverse the order + return lessOrEquals(pParam2, pParam1); + } + + @Override + protected IFormula lessThan(IExpression pParam1, IExpression pParam2) { + IFormula leq = lessOrEquals(pParam1, pParam2); + IFormula eq = equal(pParam1, pParam2); + return new IBinFormula(IBinJunctor.And(), leq, new INot(eq)); + } + + @Override + protected ITerm length(IExpression pParam) { + return new IFunApp(PrincessEnvironment.stringTheory.str_len(), toSeq(pParam)); + } + + @Override + protected ITerm concatImpl(List parts) { + return new IFunApp(PrincessEnvironment.stringTheory.str_$plus$plus(), toSeq(parts)); + } + + @Override + protected IFormula prefix(IExpression prefix, IExpression str) { + return new IAtom(PrincessEnvironment.stringTheory.str_prefixof(), toSeq(prefix, str)); + } + + @Override + protected IFormula suffix(IExpression suffix, IExpression str) { + return new IAtom(PrincessEnvironment.stringTheory.str_suffixof(), toSeq(suffix, str)); + } + + @Override + protected IFormula in(IExpression str, IExpression regex) { + return new IAtom(PrincessEnvironment.stringTheory.str_in_re(), toSeq(str, regex)); + } + + @Override + protected IFormula contains(IExpression str, IExpression part) { + return new IAtom(PrincessEnvironment.stringTheory.str_contains(), toSeq(str, part)); + } + + @Override + protected ITerm indexOf(IExpression str, IExpression part, IExpression startIndex) { + return new IFunApp(PrincessEnvironment.stringTheory.str_indexof(), toSeq(str, part, startIndex)); + } + + @Override + protected ITerm charAt(IExpression str, IExpression index) { + return new IFunApp(PrincessEnvironment.stringTheory.str_char(), toSeq(str, index)); + } + + @Override + protected ITerm substring(IExpression str, IExpression index, IExpression length) { + return new IFunApp(PrincessEnvironment.stringTheory.str_substr(), toSeq(str, index, length)); + } + + @Override + protected ITerm replace( + IExpression fullStr, IExpression target, IExpression replacement) { + return new IFunApp(PrincessEnvironment.stringTheory.str_replace(), toSeq(fullStr, target, replacement)); + } + + @Override + protected ITerm replaceAll( + IExpression fullStr, IExpression target, IExpression replacement) { + return new IFunApp(PrincessEnvironment.stringTheory.str_replaceall(), toSeq(fullStr, target, + replacement)); + } + + @Override + protected ITerm makeRegexImpl(String value) { + return new IFunApp(PrincessEnvironment.stringTheory.str_to_re(), toSeq(makeStringImpl(value))); + } + + @Override + protected ITerm noneImpl() { + return new IFunApp(PrincessEnvironment.stringTheory.re_none(), toSeq()); + } + + @Override + protected ITerm allImpl() { + return new IFunApp(PrincessEnvironment.stringTheory.re_all(), toSeq()); + } + + @Override + protected ITerm range(IExpression start, IExpression end) { + return new IFunApp(PrincessEnvironment.stringTheory.re_range(), toSeq()); + } + + @Override + public RegexFormula cross(RegexFormula regex) { + return wrapRegex(new IFunApp(PrincessEnvironment.stringTheory.re_$plus(), + toSeq(extractInfo(regex)))); + } + + @Override + public RegexFormula optional(RegexFormula regex) { + return wrapRegex(new IFunApp(PrincessEnvironment.stringTheory.re_opt(), + toSeq(extractInfo(regex)))); + } + + @Override + public RegexFormula difference(RegexFormula regex1, RegexFormula regex2) { + return wrapRegex(new IFunApp(PrincessEnvironment.stringTheory.re_diff(), + toSeq(extractInfo(regex1), extractInfo(regex2)))); + } + + @Override + protected ITerm concatRegexImpl(List parts) { + return new IFunApp(PrincessEnvironment.stringTheory.re_$plus$plus(), toSeq(parts)); + } + + @Override + protected ITerm union(IExpression pParam1, IExpression pParam2) { + return new IFunApp(PrincessEnvironment.stringTheory.re_union(), toSeq(pParam1, pParam2)); + } + + @Override + protected ITerm intersection(IExpression pParam1, IExpression pParam2) { + return new IFunApp(PrincessEnvironment.stringTheory.re_inter(), toSeq(pParam1, pParam2)); + } + + @Override + protected ITerm closure(IExpression pParam) { + return new IFunApp(PrincessEnvironment.stringTheory.re_$times(), toSeq(pParam)); + } + + @Override + protected ITerm complement(IExpression pParam) { + return new IFunApp(PrincessEnvironment.stringTheory.re_comp(), toSeq(pParam)); + } + + @Override + protected ITerm toIntegerFormula(IExpression pParam) { + return new IFunApp(PrincessEnvironment.stringTheory.str_to_int(), toSeq(pParam)); + } + + @Override + protected ITerm toStringFormula(IExpression pParam) { + return new IFunApp(PrincessEnvironment.stringTheory.int_to_str(), toSeq(pParam)); + } +} From 1f7be15890fe7e93c780844d5123a3b6982cc1f9 Mon Sep 17 00:00:00 2001 From: Alejandro Serrano Date: Mon, 6 Dec 2021 13:42:39 +0100 Subject: [PATCH 002/103] Rationals in Princess --- .../solvers/princess/PrincessEnvironment.java | 7 ++ .../princess/PrincessFormulaCreator.java | 27 +++++- .../princess/PrincessFormulaManager.java | 3 +- .../PrincessRationalFormulaManager.java | 88 +++++++++++++++++++ .../princess/PrincessSolverContext.java | 3 + 5 files changed, 124 insertions(+), 4 deletions(-) create mode 100644 src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java 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 72af599a9d..a0959ccc0e 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -31,6 +31,8 @@ import ap.terfor.preds.Predicate; import ap.theories.ExtArray; import ap.theories.bitvectors.ModuloArithmetic; +import ap.theories.rationals.Fractions; +import ap.theories.rationals.Rationals$; import ap.theories.strings.SeqStringTheory; import ap.theories.strings.SeqStringTheoryBuilder; import ap.types.Sort; @@ -112,6 +114,9 @@ class PrincessEnvironment { stringTheory = builder.theory(); } + static Fractions rationalTheory = Rationals$.MODULE$; + public static final Sort FRACTION_SORT = rationalTheory.dom(); + public static final Sort STRING_SORT = stringTheory.StringSort(); public static final Sort REGEX_SORT = stringTheory.RegexSort(); @@ -541,6 +546,8 @@ private static FormulaType getFormulaTypeFromSort(final Sort sort) { return FormulaType.BooleanType; } else if (sort == PrincessEnvironment.INTEGER_SORT || sort == PrincessEnvironment.NAT_SORT) { return FormulaType.IntegerType; + } else if (sort == PrincessEnvironment.FRACTION_SORT) { + return FormulaType.RationalType; } else if (sort == PrincessEnvironment.STRING_SORT) { return FormulaType.StringType; } else if (sort == PrincessEnvironment.REGEX_SORT) { 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 3fe1d5da3f..a0a57f6939 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -42,6 +42,9 @@ import ap.theories.ExtArray; import ap.theories.bitvectors.ModuloArithmetic; import ap.theories.nia.GroebnerMultiplication$; +import ap.theories.rationals.Fractions.Fraction$; +import ap.theories.rationals.Fractions.FractionSort$; +import ap.theories.rationals.Rationals$; import ap.theories.strings.SeqStringTheory; import ap.theories.strings.SeqStringTheoryBuilder; import ap.types.Sort; @@ -171,9 +174,12 @@ class PrincessFormulaCreator private final Table arraySortCache = HashBasedTable.create(); PrincessFormulaCreator(PrincessEnvironment pEnv) { - super(pEnv, PrincessEnvironment.BOOL_SORT, PrincessEnvironment.INTEGER_SORT, - null, - PrincessEnvironment.STRING_SORT, PrincessEnvironment.REGEX_SORT); + super(pEnv, + PrincessEnvironment.BOOL_SORT, + PrincessEnvironment.INTEGER_SORT, + PrincessEnvironment.FRACTION_SORT, + PrincessEnvironment.STRING_SORT, + PrincessEnvironment.REGEX_SORT); } @Override @@ -192,6 +198,21 @@ public Object convertValue(IExpression value) { 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": + assert fun.fun().arity() == 1; + ITerm term = fun.apply(0); + if (term instanceof IIntLit) + return ((IIntLit) term).value().doubleValue(); + else + break; + case "_frac": + assert fun.fun().arity() == 2; + ITerm term1 = fun.apply(0); + ITerm term2 = fun.apply(0); + if (term1 instanceof IIntLit && term2 instanceof IIntLit) + return ((IIntLit) term1).value().doubleValue() / ((IIntLit) term2).value().doubleValue(); + else + break; default: } } 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 fa39ec7afd..16553f671f 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java @@ -30,6 +30,7 @@ final class PrincessFormulaManager PrincessUFManager pFunctionManager, PrincessBooleanFormulaManager pBooleanManager, PrincessIntegerFormulaManager pIntegerManager, + PrincessRationalFormulaManager pRationalManager, PrincessBitvectorFormulaManager pBitpreciseManager, PrincessArrayFormulaManager pArrayManager, PrincessQuantifiedFormulaManager pQuantifierManager, @@ -39,7 +40,7 @@ final class PrincessFormulaManager pFunctionManager, pBooleanManager, pIntegerManager, - null, + pRationalManager, pBitpreciseManager, null, pQuantifierManager, 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..01a9651823 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java @@ -0,0 +1,88 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2021 Alejandro SerranoMena +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.solvers.princess; + +import ap.parser.IExpression; +import ap.parser.IFunApp; +import ap.parser.ITerm; +import ap.theories.rationals.Fractions.Fraction$; +import java.math.BigDecimal; +import java.math.BigInteger; +import java.util.ArrayList; +import org.sosy_lab.java_smt.api.NumeralFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; +import org.sosy_lab.java_smt.api.RationalFormulaManager; + +public class PrincessRationalFormulaManager + extends PrincessNumeralFormulaManager + implements RationalFormulaManager { + + private PrincessIntegerFormulaManager pInteger; + + PrincessRationalFormulaManager( + PrincessFormulaCreator pCreator, NonLinearArithmetic pNonLinearArithmetic, + PrincessIntegerFormulaManager pInteger) { + super(pCreator, pNonLinearArithmetic); + this.pInteger = pInteger; + } + + @Override + protected boolean isNumeral(IExpression value) { + if (value instanceof IFunApp) { + IFunApp fun = (IFunApp) value; + switch (fun.fun().name()) { + case "int": + assert fun.fun().arity() == 1; + return pInteger.isNumeral(fun.apply(0)); + case "frac": + assert fun.fun().arity() == 2; + return pInteger.isNumeral(fun.apply(0)) && pInteger.isNumeral(fun.apply(1)); + } + } + return false; + } + + protected IExpression fromInteger(ITerm i) { + return PrincessEnvironment.rationalTheory.int2ring(i); + } + + @Override + protected IExpression makeNumberImpl(long i) { + return fromInteger(pInteger.makeNumberImpl(i)); + } + + @Override + protected IExpression makeNumberImpl(BigInteger i) { + return fromInteger(pInteger.makeNumberImpl(i)); + } + + @Override + protected IExpression makeNumberImpl(String i) { + return makeNumberImpl(new BigDecimal(i)); + } + + @Override + protected IExpression makeNumberImpl(double pNumber) { + return makeNumberImpl(BigDecimal.valueOf(pNumber)); + } + + @Override + protected IExpression makeNumberImpl(BigDecimal pNumber) { + ArrayList args = new ArrayList<>(2); + args.add(pInteger.makeNumberImpl(pNumber.unscaledValue())); + args.add(pInteger.makeNumberImpl(BigInteger.valueOf(10).pow(pNumber.scale()))); + return new IFunApp(PrincessEnvironment.rationalTheory.frac(), + PrincessEnvironment.toSeq(args)); + } + + @Override + protected IExpression makeVariableImpl(String varName) { + return getFormulaCreator().makeVariable(PrincessEnvironment.FRACTION_SORT, varName); + } +} 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 996e639f6c..372d9cde90 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java @@ -51,6 +51,8 @@ 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); @@ -64,6 +66,7 @@ public static SolverContext create( functionTheory, booleanTheory, integerTheory, + rationalTheory, bitvectorTheory, arrayTheory, quantifierTheory, From 99337b7f11b1af4c72539c2ff23ee46bd21e46e2 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 15 Dec 2021 20:47:25 +0100 Subject: [PATCH 003/103] formatting code. Please apply 'ant format-diff' before commiting, or the extended version 'ant format-source'. --- .../solvers/princess/PrincessEnvironment.java | 1 + .../princess/PrincessFormulaCreator.java | 115 ++++++++---------- .../PrincessRationalFormulaManager.java | 7 +- .../princess/PrincessSolverContext.java | 3 +- .../PrincessStringFormulaManager.java | 32 ++--- 5 files changed, 76 insertions(+), 82 deletions(-) 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 a0959ccc0e..4f089606ca 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -108,6 +108,7 @@ class PrincessEnvironment { static int STRING_ALPHABET_SIZE = 500; static SeqStringTheory stringTheory; + static { SeqStringTheoryBuilder builder = new SeqStringTheoryBuilder(); builder.setAlphabetSize(STRING_ALPHABET_SIZE); 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 a0a57f6939..53b0b64744 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -42,11 +42,6 @@ import ap.theories.ExtArray; import ap.theories.bitvectors.ModuloArithmetic; import ap.theories.nia.GroebnerMultiplication$; -import ap.theories.rationals.Fractions.Fraction$; -import ap.theories.rationals.Fractions.FractionSort$; -import ap.theories.rationals.Rationals$; -import ap.theories.strings.SeqStringTheory; -import ap.theories.strings.SeqStringTheoryBuilder; import ap.types.Sort; import ap.types.Sort$; import com.google.common.collect.HashBasedTable; @@ -114,53 +109,53 @@ class PrincessFormulaCreator 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_char(), - 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_in_re(), - FunctionDeclarationKind.STR_IN_RE); + 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_char(), 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_in_re(), FunctionDeclarationKind.STR_IN_RE); } /** @@ -174,7 +169,8 @@ class PrincessFormulaCreator private final Table arraySortCache = HashBasedTable.create(); PrincessFormulaCreator(PrincessEnvironment pEnv) { - super(pEnv, + super( + pEnv, PrincessEnvironment.BOOL_SORT, PrincessEnvironment.INTEGER_SORT, PrincessEnvironment.FRACTION_SORT, @@ -201,18 +197,16 @@ public Object convertValue(IExpression value) { case "_int": assert fun.fun().arity() == 1; ITerm term = fun.apply(0); - if (term instanceof IIntLit) - return ((IIntLit) term).value().doubleValue(); - else - break; + if (term instanceof IIntLit) return ((IIntLit) term).value().doubleValue(); + else break; case "_frac": assert fun.fun().arity() == 2; ITerm term1 = fun.apply(0); ITerm term2 = fun.apply(0); if (term1 instanceof IIntLit && term2 instanceof IIntLit) - return ((IIntLit) term1).value().doubleValue() / ((IIntLit) term2).value().doubleValue(); - else - break; + return ((IIntLit) term1).value().doubleValue() + / ((IIntLit) term2).value().doubleValue(); + else break; default: } } @@ -251,7 +245,6 @@ public Sort getArrayType(Sort pIndexType, Sort pElementType) { return result; } - @SuppressWarnings("unchecked") @Override public FormulaType getFormulaType(final T pFormula) { 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 01a9651823..a69e47eb9e 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java @@ -11,7 +11,6 @@ import ap.parser.IExpression; import ap.parser.IFunApp; import ap.parser.ITerm; -import ap.theories.rationals.Fractions.Fraction$; import java.math.BigDecimal; import java.math.BigInteger; import java.util.ArrayList; @@ -26,7 +25,8 @@ public class PrincessRationalFormulaManager private PrincessIntegerFormulaManager pInteger; PrincessRationalFormulaManager( - PrincessFormulaCreator pCreator, NonLinearArithmetic pNonLinearArithmetic, + PrincessFormulaCreator pCreator, + NonLinearArithmetic pNonLinearArithmetic, PrincessIntegerFormulaManager pInteger) { super(pCreator, pNonLinearArithmetic); this.pInteger = pInteger; @@ -77,8 +77,7 @@ protected IExpression makeNumberImpl(BigDecimal pNumber) { ArrayList args = new ArrayList<>(2); args.add(pInteger.makeNumberImpl(pNumber.unscaledValue())); args.add(pInteger.makeNumberImpl(BigInteger.valueOf(10).pow(pNumber.scale()))); - return new IFunApp(PrincessEnvironment.rationalTheory.frac(), - PrincessEnvironment.toSeq(args)); + return new IFunApp(PrincessEnvironment.rationalTheory.frac(), PrincessEnvironment.toSeq(args)); } @Override 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 372d9cde90..4343c06523 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessSolverContext.java @@ -58,8 +58,7 @@ public static SolverContext create( PrincessArrayFormulaManager arrayTheory = new PrincessArrayFormulaManager(creator); PrincessQuantifiedFormulaManager quantifierTheory = new PrincessQuantifiedFormulaManager(creator); - PrincessStringFormulaManager stringTheory = - new PrincessStringFormulaManager(creator); + PrincessStringFormulaManager stringTheory = new PrincessStringFormulaManager(creator); PrincessFormulaManager manager = new PrincessFormulaManager( 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 index dcec8e205f..64247ce347 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java @@ -34,7 +34,7 @@ public class PrincessStringFormulaManager static Seq toSeq(List exprs) { ArrayList result = new ArrayList(); - for (IExpression expr : exprs) result.add((ITerm)expr); + for (IExpression expr : exprs) result.add((ITerm) expr); return PrincessEnvironment.toSeq(result); } @@ -115,7 +115,8 @@ protected IFormula contains(IExpression str, IExpression part) { @Override protected ITerm indexOf(IExpression str, IExpression part, IExpression startIndex) { - return new IFunApp(PrincessEnvironment.stringTheory.str_indexof(), toSeq(str, part, startIndex)); + return new IFunApp( + PrincessEnvironment.stringTheory.str_indexof(), toSeq(str, part, startIndex)); } @Override @@ -129,16 +130,15 @@ protected ITerm substring(IExpression str, IExpression index, IExpression length } @Override - protected ITerm replace( - IExpression fullStr, IExpression target, IExpression replacement) { - return new IFunApp(PrincessEnvironment.stringTheory.str_replace(), toSeq(fullStr, target, replacement)); + protected ITerm replace(IExpression fullStr, IExpression target, IExpression replacement) { + return new IFunApp( + PrincessEnvironment.stringTheory.str_replace(), toSeq(fullStr, target, replacement)); } @Override - protected ITerm replaceAll( - IExpression fullStr, IExpression target, IExpression replacement) { - return new IFunApp(PrincessEnvironment.stringTheory.str_replaceall(), toSeq(fullStr, target, - replacement)); + protected ITerm replaceAll(IExpression fullStr, IExpression target, IExpression replacement) { + return new IFunApp( + PrincessEnvironment.stringTheory.str_replaceall(), toSeq(fullStr, target, replacement)); } @Override @@ -163,20 +163,22 @@ protected ITerm range(IExpression start, IExpression end) { @Override public RegexFormula cross(RegexFormula regex) { - return wrapRegex(new IFunApp(PrincessEnvironment.stringTheory.re_$plus(), - toSeq(extractInfo(regex)))); + return wrapRegex( + new IFunApp(PrincessEnvironment.stringTheory.re_$plus(), toSeq(extractInfo(regex)))); } @Override public RegexFormula optional(RegexFormula regex) { - return wrapRegex(new IFunApp(PrincessEnvironment.stringTheory.re_opt(), - toSeq(extractInfo(regex)))); + return wrapRegex( + new IFunApp(PrincessEnvironment.stringTheory.re_opt(), toSeq(extractInfo(regex)))); } @Override public RegexFormula difference(RegexFormula regex1, RegexFormula regex2) { - return wrapRegex(new IFunApp(PrincessEnvironment.stringTheory.re_diff(), - toSeq(extractInfo(regex1), extractInfo(regex2)))); + return wrapRegex( + new IFunApp( + PrincessEnvironment.stringTheory.re_diff(), + toSeq(extractInfo(regex1), extractInfo(regex2)))); } @Override From b7bbc3c4665411154b12ece9c17c12edc8f96f88 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Thu, 16 Dec 2021 00:56:33 +0100 Subject: [PATCH 004/103] Princess: revert from Scala 2.13 to Scala 2.12. Scala is not upwards and not downwards compatible. The upcoming Ostrich library is only available for Scala 2.12, so we downgrade Scala for Princess. --- .classpath | 4 ++-- .idea/JavaSMT.iml | 8 ++++---- lib/ivy.xml | 4 ++-- .../princess/PrincessAbstractProver.java | 10 +++++----- .../solvers/princess/PrincessEnvironment.java | 19 +++++++++++-------- .../princess/PrincessFormulaCreator.java | 6 +++--- .../princess/PrincessFunctionDeclaration.java | 2 +- .../princess/PrincessInterpolatingProver.java | 14 ++++++++------ .../solvers/princess/PrincessModel.java | 11 ++++++----- .../PrincessNumeralFormulaManager.java | 4 ++-- .../PrincessQuantifiedFormulaManager.java | 5 +++-- .../PrincessStringFormulaManager.java | 2 +- 12 files changed, 48 insertions(+), 41 deletions(-) diff --git a/.classpath b/.classpath index 0cddccbfc8..054a67722c 100644 --- a/.classpath +++ b/.classpath @@ -24,9 +24,9 @@ SPDX-License-Identifier: Apache-2.0 - + - + diff --git a/.idea/JavaSMT.iml b/.idea/JavaSMT.iml index 7d5c10ba3b..656d8e751a 100644 --- a/.idea/JavaSMT.iml +++ b/.idea/JavaSMT.iml @@ -193,18 +193,18 @@ SPDX-License-Identifier: Apache-2.0 - + - + - + @@ -213,7 +213,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/lib/ivy.xml b/lib/ivy.xml index 349049b410..8138e3b32b 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -146,9 +146,9 @@ SPDX-License-Identifier: Apache-2.0 - + - + diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java index 817d36da80..3f071f6e57 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java @@ -9,8 +9,8 @@ package org.sosy_lab.java_smt.solvers.princess; import static com.google.common.base.Preconditions.checkNotNull; -import static scala.collection.JavaConverters.asJava; -import static scala.collection.JavaConverters.asScala; +import static scala.collection.JavaConverters.collectionAsScalaIterable; +import static scala.collection.JavaConverters.setAsJavaSet; import ap.SimpleAPI; import ap.SimpleAPI.PartialModel; @@ -116,8 +116,8 @@ public void pop() { // 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.addBooleanVariables(collectionAsScalaIterable(level.booleanSymbols)); + api.addConstants(collectionAsScalaIterable(level.intSymbols)); level.functionSymbols.forEach(api::addFunction); if (!trackingStack.isEmpty()) { trackingStack.peek().mergeWithHigher(level); @@ -163,7 +163,7 @@ public List getUnsatCore() { Preconditions.checkState(!closed); checkGenerateUnsatCores(); final List result = new ArrayList<>(); - final Set core = asJava(api.getUnsatCore()); + final Set core = setAsJavaSet(api.getUnsatCore()); int cnt = 0; for (IExpression formula : getAssertedFormulas()) { 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 4f089606ca..5e154e007b 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -8,8 +8,9 @@ package org.sosy_lab.java_smt.solvers.princess; -import static scala.collection.JavaConverters.asJava; import static scala.collection.JavaConverters.collectionAsScalaIterableConverter; +import static scala.collection.JavaConverters.mapAsJavaMap; +import static scala.collection.JavaConverters.seqAsJavaList; import ap.SimpleAPI; import ap.parser.BooleanCompactifier; @@ -30,6 +31,7 @@ import ap.terfor.ConstantTerm; import ap.terfor.preds.Predicate; import ap.theories.ExtArray; +import ap.theories.ExtArray.ArraySort; import ap.theories.bitvectors.ModuloArithmetic; import ap.theories.rationals.Fractions; import ap.theories.rationals.Rationals$; @@ -78,7 +80,7 @@ import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import scala.Tuple2; import scala.Tuple4; -import scala.collection.immutable.Seq; +import scala.collection.Seq; /** * This is a Wrapper around Princess. This Wrapper allows to set a logfile for all Smt-Queries @@ -270,7 +272,7 @@ void close() { public List parseStringToTerms(String s, PrincessFormulaCreator creator) { Tuple4< - Seq, + scala.collection.Seq, scala.collection.immutable.Map, scala.collection.immutable.Map, scala.collection.immutable.Map> @@ -282,7 +284,7 @@ public List parseStringToTerms(String s, PrincessFormulaC throw new IllegalArgumentException(nested); } - final List formulas = asJava(parserResult._1()); + final List formulas = seqAsJavaList(parserResult._1()); ImmutableSet.Builder declaredFunctions = ImmutableSet.builder(); for (IExpression f : formulas) { @@ -314,7 +316,7 @@ public List parseStringToTerms(String s, PrincessFormulaC /* EnvironmentException is not unused, but the Java compiler does not like Scala. */ @SuppressWarnings("unused") private Tuple4< - Seq, + scala.collection.Seq, scala.collection.immutable.Map, scala.collection.immutable.Map, scala.collection.immutable.Map> @@ -352,7 +354,7 @@ public Appender dumpFormula(IFormula formula, final PrincessFormulaCreator creat Tuple2> tuple = api.abbrevSharedExpressionsWithMap(formula, 1); final IExpression lettedFormula = tuple._1(); - final Map abbrevMap = asJava(tuple._2()); + final Map abbrevMap = mapAsJavaMap(tuple._2()); return new Appenders.AbstractAppender() { @@ -398,7 +400,8 @@ private void appendTo0(Appendable out) throws IOException { for (Entry function : ufs.entrySet()) { List argSorts = Lists.transform( - asJava(function.getValue().args()), a -> getFormulaType(a).toSMTLIBString()); + seqAsJavaList(function.getValue().args()), + a -> getFormulaType(a).toSMTLIBString()); out.append( String.format( "(declare-fun %s (%s) %s)%n", @@ -554,7 +557,7 @@ private static FormulaType getFormulaTypeFromSort(final Sort sort) { } else if (sort == PrincessEnvironment.REGEX_SORT) { return FormulaType.RegexType; } else if (sort instanceof ExtArray.ArraySort) { - Seq indexSorts = ((ExtArray.ArraySort) sort).theory().indexSorts(); + Seq indexSorts = ((ArraySort) sort).theory().indexSorts(); Sort elementSort = ((ExtArray.ArraySort) sort).theory().objSort(); assert indexSorts.iterator().size() == 1 : "unexpected index type in Array type:" + sort; // assert indexSorts.size() == 1; // TODO Eclipse does not like simpler code. 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 53b0b64744..c6c054d1f2 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -12,7 +12,7 @@ import static org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier.EXISTS; import static org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier.FORALL; import static org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.toSeq; -import static scala.collection.JavaConverters.asJava; +import static scala.collection.JavaConverters.asJavaCollection; import ap.basetypes.IdealInt; import ap.parser.IAtom; @@ -329,7 +329,7 @@ public R visit(FormulaVisitor visitor, final Formula f, final IExpression return visitor.visitBoundVariable(f, ((IVariable) input).index()); // nullary atoms and constant are variables - } else if (((input instanceof IAtom) && asJava(((IAtom) input).args()).isEmpty()) + } else if (((input instanceof IAtom) && asJavaCollection(((IAtom) input).args()).isEmpty()) || input instanceof IConstant) { return visitor.visitFreeVariable(f, input.toString()); @@ -473,7 +473,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/PrincessFunctionDeclaration.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java index d252ff4522..cf987145d9 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java @@ -28,7 +28,7 @@ import ap.types.SortedIFunction$; import java.util.ArrayList; import java.util.List; -import scala.collection.immutable.Seq; +import scala.collection.Seq; /** * Unlike other solvers, Princess does not have a class representing the built-in functions (OR, diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java index 99a447c659..5ae9bc49e5 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java @@ -8,8 +8,8 @@ package org.sosy_lab.java_smt.solvers.princess; -import static scala.collection.JavaConverters.asJava; -import static scala.collection.JavaConverters.asScala; +import static scala.collection.JavaConverters.asJavaIterable; +import static scala.collection.JavaConverters.collectionAsScalaIterable; import ap.SimpleAPI; import ap.basetypes.Tree; @@ -113,7 +113,7 @@ public List getSeqInterpolants( // convert to needed data-structure final ArrayBuffer> args = new ArrayBuffer<>(); for (Collection partition : partitions) { - args.$plus$eq(asScala(partition).toSet()); + args.$plus$eq(collectionAsScalaIterable(partition).toSet()); } // do the hard work @@ -134,7 +134,7 @@ public List getSeqInterpolants( // convert data-structure back // TODO check that interpolants do not contain abbreviations we did not introduce ourselves final List result = new ArrayList<>(); - for (final IFormula itp : asJava(itps)) { + for (final IFormula itp : asJavaIterable(itps)) { result.add(mgr.encapsulateBooleanFormula(itp)); } return result; @@ -163,7 +163,9 @@ public List getTreeInterpolants( children.$plus$eq$colon(stack.pop()); // prepend } subtreeStarts.push(start); - stack.push(new Tree<>(asScala(partitionedFormulas.get(i)).toSet(), children.toList())); + stack.push( + new Tree<>( + collectionAsScalaIterable(partitionedFormulas.get(i)).toSet(), children.toList())); } Preconditions.checkState(subtreeStarts.peek() == 0, "subtree of root should start at 0."); @@ -190,7 +192,7 @@ public List getTreeInterpolants( private List tree2List(Tree tree) { List lst = FluentIterable.from( - Traverser.>forTree(node -> asJava(node.children())) + Traverser.>forTree(node -> asJavaIterable(node.children())) .depthFirstPostOrder(tree)) .transform(node -> mgr.encapsulateBooleanFormula(node.d())) .toList(); 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 e19e434fa2..d6ba264670 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java @@ -8,7 +8,8 @@ package org.sosy_lab.java_smt.solvers.princess; -import static scala.collection.JavaConverters.asJava; +import static scala.collection.JavaConverters.asJavaIterable; +import static scala.collection.JavaConverters.mapAsJavaMap; import ap.SimpleAPI; import ap.SimpleAPI.PartialModel; @@ -55,7 +56,7 @@ protected ImmutableList toList() { // get abbreviations, we do not want to export them. Set abbrevs = new LinkedHashSet<>(); - for (var entry : asJava(api.ap$SimpleAPI$$abbrevPredicates()).entrySet()) { + for (var entry : mapAsJavaMap(api.ap$SimpleAPI$$abbrevPredicates()).entrySet()) { abbrevs.add(entry.getKey()); // collect the abbreviation. abbrevs.add(entry.getValue()._2()); // the definition is also handled as abbreviation here. } @@ -65,7 +66,7 @@ protected ImmutableList toList() { // then iterate over the model and generate the assignments ImmutableSet.Builder assignments = ImmutableSet.builder(); - for (Map.Entry entry : asJava(interpretation).entrySet()) { + for (Map.Entry entry : mapAsJavaMap(interpretation).entrySet()) { if (!isAbbrev(abbrevs, entry.getKey())) { assignments.addAll(getAssignments(entry.getKey(), entry.getValue(), arrays)); } @@ -103,7 +104,7 @@ private boolean isAbbrev(Set abbrevs, IExpression var) { private Multimap getArrays( scala.collection.Map interpretation) { Multimap arrays = ArrayListMultimap.create(); - for (Map.Entry entry : asJava(interpretation).entrySet()) { + for (Map.Entry entry : mapAsJavaMap(interpretation).entrySet()) { if (entry.getKey() instanceof IConstant) { ITerm maybeArray = (IConstant) entry.getKey(); IExpression value = entry.getValue(); @@ -155,7 +156,7 @@ private ImmutableList getAssignments( // normal variable or UF IFunApp cKey = (IFunApp) key; argumentInterpretations = new ArrayList<>(); - for (ITerm arg : asJava(cKey.args())) { + for (ITerm arg : asJavaIterable(cKey.args())) { argumentInterpretations.add(creator.convertValue(arg)); } name = cKey.fun().name(); diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java index 708024a9a1..d9defc6c7b 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessNumeralFormulaManager.java @@ -8,7 +8,7 @@ package org.sosy_lab.java_smt.solvers.princess; -import static scala.collection.JavaConverters.asScala; +import static scala.collection.JavaConverters.iterableAsScalaIterable; import ap.parser.IExpression; import ap.parser.IFormula; @@ -57,7 +57,7 @@ protected IFormula equal(IExpression pNumber1, IExpression pNumber2) { @Override protected IExpression distinctImpl(List pNumbers) { - return IExpression.distinct(asScala(Iterables.filter(pNumbers, ITerm.class))); + return IExpression.distinct(iterableAsScalaIterable(Iterables.filter(pNumbers, ITerm.class))); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessQuantifiedFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessQuantifiedFormulaManager.java index 813d30d273..d96c107434 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessQuantifiedFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessQuantifiedFormulaManager.java @@ -9,7 +9,7 @@ package org.sosy_lab.java_smt.solvers.princess; import static com.google.common.base.Preconditions.checkArgument; -import static scala.collection.JavaConverters.asScala; +import static scala.collection.JavaConverters.iterableAsScalaIterable; import ap.parser.IConstant; import ap.parser.IExpression; @@ -48,7 +48,8 @@ public IExpression mkQuantifier(Quantifier q, List vars, IExpressio return new ISortedQuantified(pq, PrincessEnvironment.INTEGER_SORT, (IFormula) body); } else { // TODO: add support for boolean quantification! - return IExpression.quanConsts(pq, asScala(toConstantTerm(vars)), (IFormula) body); + return IExpression.quanConsts( + pq, iterableAsScalaIterable(toConstantTerm(vars)), (IFormula) body); } } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java index 64247ce347..2bc0c98b41 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java @@ -22,7 +22,7 @@ import java.util.List; import org.sosy_lab.java_smt.api.RegexFormula; import org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager; -import scala.collection.immutable.Seq; +import scala.collection.Seq; public class PrincessStringFormulaManager extends AbstractStringFormulaManager< From 53a1885bce035f8d3d9c76249b20ba7713fcde98 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Thu, 16 Dec 2021 01:00:07 +0100 Subject: [PATCH 005/103] adding dependency for Ostrich into JavaSMT. This is an initial step and the usage is still unclear. This is not tested. --- .classpath | 4 ++++ lib/ivy.xml | 11 +++++++++-- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/.classpath b/.classpath index 054a67722c..4a106f825c 100644 --- a/.classpath +++ b/.classpath @@ -28,6 +28,10 @@ SPDX-License-Identifier: Apache-2.0 + + + + diff --git a/lib/ivy.xml b/lib/ivy.xml index 8138e3b32b..46596ae186 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -145,10 +145,17 @@ SPDX-License-Identifier: Apache-2.0 - + + + --> + + + + + From 6f62e0559be7fa8f63541e70fc4e03bb361a8435 Mon Sep 17 00:00:00 2001 From: Alejandro Serrano Date: Thu, 16 Dec 2021 12:26:44 +0100 Subject: [PATCH 006/103] Use Ostrich for strings --- .../solvers/princess/PrincessEnvironment.java | 24 +++++++++---------- 1 file changed, 12 insertions(+), 12 deletions(-) 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 5e154e007b..f913b87ad2 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -37,6 +37,7 @@ import ap.theories.rationals.Rationals$; import ap.theories.strings.SeqStringTheory; import ap.theories.strings.SeqStringTheoryBuilder; +import ap.theories.strings.StringTheory; import ap.types.Sort; import ap.types.Sort$; import ap.types.Sort.MultipleValueBool$; @@ -78,6 +79,11 @@ import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; +import ostrich.OFlags; +import ostrich.OFlags.LengthOptions$; +import ostrich.OstrichStringTheory; +import ostrich.OstrichStringTheoryBuilder; +import ostrich.automata.Transducer; import scala.Tuple2; import scala.Tuple4; import scala.collection.Seq; @@ -108,21 +114,15 @@ class PrincessEnvironment { public static final Sort INTEGER_SORT = Sort.Integer$.MODULE$; public static final Sort NAT_SORT = Sort.Nat$.MODULE$; - static int STRING_ALPHABET_SIZE = 500; - static SeqStringTheory stringTheory; - - static { - SeqStringTheoryBuilder builder = new SeqStringTheoryBuilder(); - builder.setAlphabetSize(STRING_ALPHABET_SIZE); - stringTheory = builder.theory(); - } - - static Fractions rationalTheory = Rationals$.MODULE$; - public static final Sort FRACTION_SORT = rationalTheory.dom(); - + static StringTheory stringTheory = + new OstrichStringTheory(toSeq(new ArrayList>()), + new OFlags(false, false, LengthOptions$.MODULE$.Auto(), false, false)); 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; From d59e56cdb070f466f176488b06710f0450e42cbc Mon Sep 17 00:00:00 2001 From: Alejandro Serrano Date: Thu, 16 Dec 2021 12:27:03 +0100 Subject: [PATCH 007/103] Do not use 'floor' for rationals in Princess --- .../solvers/princess/PrincessRationalFormulaManager.java | 5 +++++ .../sosy_lab/java_smt/test/RationalFormulaManagerTest.java | 7 +++++++ src/org/sosy_lab/java_smt/test/SolverBasedTest0.java | 7 +++++++ 3 files changed, 19 insertions(+) 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 a69e47eb9e..683c250f24 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java @@ -84,4 +84,9 @@ protected IExpression makeNumberImpl(BigDecimal pNumber) { protected IExpression makeVariableImpl(String varName) { return getFormulaCreator().makeVariable(PrincessEnvironment.FRACTION_SORT, varName); } + + @Override + protected IExpression floor(IExpression number) { + throw new AssertionError("floor is not supported in Princess"); + } } diff --git a/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java index 60f66c6ea6..cb0b544524 100644 --- a/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java @@ -54,6 +54,7 @@ protected Solvers solverToUse() { @Test public void rationalToIntTest() throws SolverException, InterruptedException { requireRationals(); + requireRationalFloor(); for (double v : SOME_DOUBLES) { IntegerFormula i = imgr.makeNumber((int) Math.floor(v)); RationalFormula r = rmgr.makeNumber(v); @@ -77,6 +78,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); @@ -89,6 +91,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(); } @@ -97,6 +100,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(); } @@ -105,6 +109,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(); } @@ -113,6 +118,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(); @@ -121,6 +127,7 @@ public void forallFloorIsLessThanValueTest() throws SolverException, Interrupted @Test public void visitFloorTest() { requireRationals(); + requireRationalFloor(); IntegerFormula f = rmgr.floor(rmgr.makeVariable("v")); assertThat(mgr.extractVariables(f)).hasSize(1); FunctionCollector collector = new FunctionCollector(); diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index 529421280b..0031fd3b6c 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -184,6 +184,13 @@ protected final void requireRationals() { .isNotNull(); } + protected final void requireRationalFloor() { + assume() + .withMessage("Princess does not support floor for rationals") + .that(solverToUse()) + .isNotEqualTo(Solvers.PRINCESS); + } + /** Skip test if the solver does not support bitvectors. */ protected final void requireBitvectors() { assume() From adaa89cda772a42db49bb86fd908cba44cc4ca3f Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Fri, 14 Jan 2022 19:29:12 +0100 Subject: [PATCH 008/103] add Ostrich library into IntelliJ config. --- .idea/JavaSMT.iml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/.idea/JavaSMT.iml b/.idea/JavaSMT.iml index 656d8e751a..8a335ee6e2 100644 --- a/.idea/JavaSMT.iml +++ b/.idea/JavaSMT.iml @@ -302,6 +302,15 @@ SPDX-License-Identifier: Apache-2.0 + + + + + + + + +