diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java index 3a6b37ab3a..834a3d74d9 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java @@ -22,7 +22,6 @@ final class BoolectorFormulaManager extends AbstractFormulaManager -// -// SPDX-License-Identifier: Apache-2.0 - -package org.sosy_lab.java_smt.solvers.boolector; - -import static com.google.common.base.Preconditions.checkArgument; - -import com.google.common.collect.ImmutableList; -import com.google.common.primitives.Longs; -import java.util.List; -import org.sosy_lab.java_smt.api.SolverException; -import org.sosy_lab.java_smt.basicimpl.AbstractQuantifiedFormulaManager; -import org.sosy_lab.java_smt.basicimpl.FormulaCreator; - -public class BoolectorQuantifiedFormulaManager - extends AbstractQuantifiedFormulaManager { - - private final long btor; - - BoolectorQuantifiedFormulaManager(FormulaCreator pCreator) { - super(pCreator); - btor = getFormulaCreator().getEnv(); - } - - @Override - protected Long eliminateQuantifiers(Long pExtractInfo) - throws SolverException, InterruptedException { - throw new UnsupportedOperationException("Boolector can not eliminate quantifier."); - } - - /** - * Note: Boolector only supports bitvector quantifier! The vars used MUST be boolector_param (not - * boolector_var)! Therefore, we have to change every var into param with the visitor! - * Additionally, no param may be used twice (Boolector will end if you do!). - */ - // TODO with the comment above, the user has no way to call boolector_param. - // This implementation seems to be broken and not usable. - @Override - public Long mkQuantifier(Quantifier pQ, List pVars, Long pBody) { - checkArgument(!pVars.isEmpty(), "List of quantified variables can not be empty"); - for (long param : pVars) { - checkArgument( - BtorJNI.boolector_is_param(btor, param), - "pVariables need to be parameter nodes in boolector."); - } - final long newQuantifier; - final long[] varsArray = Longs.toArray(pVars); - if (pQ == Quantifier.FORALL) { - newQuantifier = BtorJNI.boolector_forall(btor, varsArray, varsArray.length, pBody); - } else { - newQuantifier = BtorJNI.boolector_exists(btor, varsArray, varsArray.length, pBody); - } - return newQuantifier; - } - - static class QuantifiedFormula { - private final boolean isForall; // false for EXISTS, true for FORALL - private final long body; - private final ImmutableList boundVariables; - - QuantifiedFormula(boolean pIsForall, long pBody, List pVars) { - isForall = pIsForall; - body = pBody; - boundVariables = ImmutableList.copyOf(pVars); - } - - public boolean isForall() { - return isForall; - } - - public long getBody() { - return body; - } - - public ImmutableList getBoundVariables() { - return boundVariables; - } - } -} diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java index 057fbc3905..6d2bb3b9d9 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java @@ -94,12 +94,10 @@ public static BoolectorSolverContext create( BoolectorBooleanFormulaManager booleanTheory = new BoolectorBooleanFormulaManager(creator); BoolectorBitvectorFormulaManager bitvectorTheory = new BoolectorBitvectorFormulaManager(creator, booleanTheory); - BoolectorQuantifiedFormulaManager quantifierTheory = - new BoolectorQuantifiedFormulaManager(creator); BoolectorArrayFormulaManager arrayTheory = new BoolectorArrayFormulaManager(creator); BoolectorFormulaManager manager = new BoolectorFormulaManager( - creator, functionTheory, booleanTheory, bitvectorTheory, quantifierTheory, arrayTheory); + creator, functionTheory, booleanTheory, bitvectorTheory, arrayTheory); return new BoolectorSolverContext(manager, creator, pShutdownNotifier); } diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java index 3d336c0d80..d963c1c99b 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java @@ -35,6 +35,7 @@ import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_DIVIDES_ATOM; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_EQ_TERM; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_FLOOR; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_FORALL_TERM; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_IDIV; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_IMOD; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_IS_INT_ATOM; @@ -81,6 +82,7 @@ import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_eq; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_floor; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_function_type; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_get_term_by_name; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_get_term_name; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_idiv; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_imod; @@ -89,7 +91,8 @@ import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_is_int_atom; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_ite; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_mul; -import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_named_variable; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_new_uninterpreted_term; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_new_variable; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_not; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_or; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_parse_rational; @@ -100,6 +103,7 @@ import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_proj_index; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_rational_const_value; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_real_type; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_set_term_name; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_sum; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_sum_component; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_bitsize; @@ -120,9 +124,11 @@ import com.google.common.base.Joiner; import com.google.common.base.Preconditions; import com.google.common.collect.Collections2; +import com.google.common.collect.HashBasedTable; import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; import com.google.common.collect.Lists; +import com.google.common.collect.Table; import com.google.common.primitives.Ints; import java.math.BigInteger; import java.util.ArrayList; @@ -135,6 +141,7 @@ import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; import org.sosy_lab.java_smt.api.FunctionDeclarationKind; +import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier; import org.sosy_lab.java_smt.api.visitors.FormulaVisitor; import org.sosy_lab.java_smt.basicimpl.FormulaCreator; import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl; @@ -153,6 +160,12 @@ public class Yices2FormulaCreator extends FormulaCreator formulaCache = HashBasedTable.create(); + protected Yices2FormulaCreator() { super(null, yices_bool_type(), yices_int_type(), yices_real_type(), null, null); } @@ -174,7 +187,7 @@ public Integer getArrayType(Integer pIndexType, Integer pElementType) { @Override public Integer makeVariable(Integer pType, String pVarName) { - return yices_named_variable(pType, pVarName); + return createNamedVariable(pType, pVarName); } @Override @@ -246,6 +259,60 @@ public FormulaType getFormulaType(Integer pFormula) { yices_type_to_string(yices_type_of_term(pFormula)), yices_term_to_string(pFormula))); } + /** Creates a named, free variable. Might retrieve it from the cache if created prior. */ + protected int createNamedVariable(int type, String name) { + Integer maybeFormula = formulaCache.get(name, type); + if (maybeFormula != null) { + return maybeFormula; + } + if (formulaCache.containsRow(name)) { + throw new IllegalArgumentException( + "Symbol " + name + " already used for a variable of type " + formulaCache.row(name)); + } + int var = yices_new_uninterpreted_term(type); + // Names in Yices2 behave like a stack. The last variable named is retrieved when asking for + // a term with a specific name. Since we substitute free vars with bound for quantifiers, + // this sometimes mixes them up, hence we track them ourselves. + yices_set_term_name(var, name); + formulaCache.put(name, type, var); + return var; + } + + protected int createBoundVariableFromFreeVariable(int unboundVar) { + int type = yices_type_of_term(unboundVar); + String name = yices_get_term_name(unboundVar); + + int termFromName = yices_get_term_by_name(name); + if (termFromName != -1) { + int termFromNameType = yices_type_of_term(termFromName); + if (type == termFromNameType) { + int constructor = yices_term_constructor(termFromName); + if (constructor == YICES_VARIABLE) { + // Already a bound var + return termFromName; + } + } else { + throw new IllegalArgumentException( + String.format( + "Can't create variable with name '%s' and type '%s' " + + "as it would omit a variable with type '%s'", + name, yices_type_to_string(type), yices_type_to_string(termFromNameType))); + } + } + // reset term name binding + // TODO: add yices_remove_term_name(); + int bound = yices_new_variable(type); + // Names in Yices2 behave like a stack. The last variable named is retrieved when asking for + // a term with a specific name. Since we substitute free vars with bound for quantifiers, + // this sometimes mixes them up, hence we track them ourselves. + // This overrides the naming, but the old is cached. + // Meaning that if we remove the new name, the old term gets its name back. + // Since we just want to retrieve the same var for the quantifier we are currently building, + // this is fine. + yices_set_term_name(bound, name); + return bound; + } + @Override public R visit(FormulaVisitor pVisitor, Formula pFormula, Integer pF) { int constructor = yices_term_constructor(pF); @@ -258,6 +325,22 @@ public R visit(FormulaVisitor pVisitor, Formula pFormula, Integer pF) { return pVisitor.visitConstant(pFormula, convertValue(pF, pF)); case YICES_UNINTERPRETED_TERM: return pVisitor.visitFreeVariable(pFormula, yices_get_term_name(pF)); + case YICES_VARIABLE: + return pVisitor.visitBoundVariable(pFormula, 0); + case YICES_FORALL_TERM: + int children = yices_term_num_children(pF); + ImmutableList.Builder boundVars = ImmutableList.builder(); + for (int i = 0; i < children - 1; i++) { + int boundVar = yices_term_child(pF, i); + boundVars.add(encapsulateWithTypeOf(boundVar)); + } + BooleanFormula body = encapsulateBoolean(yices_term_child(pF, children - 1)); + Quantifier quant = Quantifier.EXISTS; + if (yices_term_to_string(pF).startsWith("(forall")) { + // TODO: this is stupid, but i could not find a way of discerning between the quantifiers + quant = Quantifier.FORALL; + } + return pVisitor.visitQuantifier((BooleanFormula) pFormula, quant, boundVars.build(), body); default: return visitFunctionApplication(pVisitor, pFormula, pF, constructor); } @@ -696,7 +779,7 @@ public Integer declareUFImpl(String pName, Integer pReturnType, List pA } else { yicesFuncType = yices_function_type(size, argTypeArray, pReturnType); } - int uf = yices_named_variable(yicesFuncType, pName); + int uf = createNamedVariable(yicesFuncType, pName); return uf; } diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java index 53aa7b20d4..e473f6591b 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java @@ -48,7 +48,8 @@ protected Yices2FormulaManager( Yices2BooleanFormulaManager pBooleanManager, Yices2IntegerFormulaManager pIntegerManager, Yices2RationalFormulaManager pRationalManager, - Yices2BitvectorFormulaManager pBitvectorManager) { + Yices2BitvectorFormulaManager pBitvectorManager, + Yices2QuantifiedFormulaManager pQuantifiedFormulaManager) { super( pFormulaCreator, pFunctionManager, @@ -57,7 +58,7 @@ protected Yices2FormulaManager( pRationalManager, pBitvectorManager, null, - null, + pQuantifiedFormulaManager, null, null, null, diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java index 2ea4894d0d..079170529a 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java @@ -783,25 +783,6 @@ public static String yices_model_to_string(long m) { public static native int yices_subst_term(int size, int[] from, int[] to, int t); - public static int yices_named_variable(int type, String name) { - int termFromName = yices_get_term_by_name(name); - if (termFromName != -1) { - int termFromNameType = yices_type_of_term(termFromName); - if (type == termFromNameType) { - return termFromName; - } else { - throw new IllegalArgumentException( - String.format( - "Can't create variable with name '%s' and type '%s' " - + "as it would omit a variable with type '%s'", - name, yices_type_to_string(type), yices_type_to_string(termFromNameType))); - } - } - int var = yices_new_uninterpreted_term(type); - yices_set_term_name(var, name); - return var; - } - /** * @return int 1 if the Yices2-lib is compiled thread-safe and 0 otherwise */ diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApiTest.java index 4cba71dd14..a14bde9908 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApiTest.java @@ -46,6 +46,7 @@ import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_free_config; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_free_context; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_function_type; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_get_term_by_name; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_get_term_name; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_idiv; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_iff; @@ -54,7 +55,6 @@ import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_int64; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_int_type; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_mul; -import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_named_variable; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_new_config; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_new_context; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_new_uninterpreted_term; @@ -81,6 +81,8 @@ import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_num_children; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_to_string; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_true; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_of_term; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_to_string; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_zero_extend; import com.google.common.base.Joiner; @@ -95,6 +97,7 @@ import org.junit.AssumptionViolatedException; import org.junit.Before; import org.junit.BeforeClass; +import org.junit.Ignore; import org.junit.Test; import org.sosy_lab.common.NativeLibraries; import org.sosy_lab.common.rationals.Rational; @@ -201,6 +204,8 @@ public void rationalError() { System.out.println(rat); // "use" variable } + // TODO: what is this test supposed to be doing? And remove print. + @Ignore @Test public void negativeRationalError() { // TODO negative unsigned integer causes no error. Need to ensure positive value before @@ -467,6 +472,8 @@ public void arithSimplification() { assertThat(yices_term_constructor(mul)).isEqualTo(YICES_ARITH_CONST); } + // TODO: what is this test supposed to be doing? And remove print. + @Ignore @Test public void sumComponents() { int three = yices_int32(3); @@ -499,6 +506,8 @@ public void sumComponents() { } } + // TODO: what is this test supposed to be doing? And remove print. + @Ignore @Test public void bvSumComponents() { int bv1 = yices_parse_bvbin("00101"); @@ -521,6 +530,8 @@ public void bvSumComponents() { } } + // TODO: what is this test supposed to be doing? And remove print. + @Ignore @Test public void bvExtensionStructureTest() { int extendBy = 5; @@ -569,6 +580,8 @@ public void bvSum() { assertThat(constructor).isEqualTo(YICES_BV_SUM); } + // TODO: what is this test supposed to be doing? And remove print. + @Ignore @Test public void bvMul() { int type = yices_bv_type(5); @@ -580,4 +593,27 @@ public void bvMul() { System.out.println(component[1]); System.out.println(yices_term_constructor(yices_bvpower(component[0], component[1]))); } + + /** + * Only to be used for tests in this class. Old implementation used for creating/retrieving named + * variables. Superseded by Yices2FormulaCreator.createNamedVariable() for reasons outlined there. + */ + private static int yices_named_variable(int type, String name) { + int termFromName = yices_get_term_by_name(name); + if (termFromName != -1) { + int termFromNameType = yices_type_of_term(termFromName); + if (type == termFromNameType) { + return termFromName; + } else { + throw new IllegalArgumentException( + String.format( + "Can't create variable with name '%s' and type '%s' " + + "as it would omit a variable with type '%s'", + name, yices_type_to_string(type), yices_type_to_string(termFromNameType))); + } + } + int var = yices_new_uninterpreted_term(type); + yices_set_term_name(var, name); + return var; + } } diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2QuantifiedFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2QuantifiedFormulaManager.java index 957d078f9b..76fa7022f2 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2QuantifiedFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2QuantifiedFormulaManager.java @@ -10,8 +10,10 @@ import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_exists; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_forall; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_subst_term; import com.google.common.primitives.Ints; +import java.util.ArrayList; import java.util.List; import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.basicimpl.AbstractQuantifiedFormulaManager; @@ -28,27 +30,31 @@ protected Yices2QuantifiedFormulaManager( @Override protected Integer eliminateQuantifiers(Integer pExtractInfo) throws SolverException, InterruptedException { - // TODO Auto-generated method stub - throw new UnsupportedOperationException("Yices does not support eliminating Quantifiers."); + throw new UnsupportedOperationException("Yices2 does not support quantifier elimination."); } @Override public Integer mkQuantifier(Quantifier pQ, List pVars, Integer pBody) { - /* - * TODO Yices needs variables constructed using yices_new_variable(), but variables passed in - * pVars are constructed with yices_new uninterpreted_term(). Need to construct the correct - * variable type from the variables in pVars and map between them. - */ + // Quantifier support is very limited in Yices2 if (pVars.isEmpty()) { throw new IllegalArgumentException("Empty variable list for Quantifier."); } else { - int[] terms = Ints.toArray(pVars); + List yicesVars = new ArrayList<>(); + for (int var : pVars) { + yicesVars.add( + ((Yices2FormulaCreator) formulaCreator).createBoundVariableFromFreeVariable(var)); + } + int substBody = pBody; + substBody = + yices_subst_term( + yicesVars.size(), Ints.toArray(pVars), Ints.toArray(yicesVars), substBody); + + int[] terms = Ints.toArray(yicesVars); if (pQ == Quantifier.FORALL) { - return yices_forall(terms.length, terms, pBody); - } else if (pQ == Quantifier.EXISTS) { - return yices_exists(terms.length, terms, pBody); + return yices_forall(terms.length, terms, substBody); + } else { + return yices_exists(terms.length, terms, substBody); } } - return null; } } diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java index c68e90aa3c..2b8a12c3f4 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java @@ -72,9 +72,16 @@ public static Yices2SolverContext create( new Yices2IntegerFormulaManager(creator, pNonLinearArithmetic); Yices2RationalFormulaManager rationalTheory = new Yices2RationalFormulaManager(creator, pNonLinearArithmetic); + Yices2QuantifiedFormulaManager quantTheory = new Yices2QuantifiedFormulaManager(creator); Yices2FormulaManager manager = new Yices2FormulaManager( - creator, functionTheory, booleanTheory, integerTheory, rationalTheory, bitvectorTheory); + creator, + functionTheory, + booleanTheory, + integerTheory, + rationalTheory, + bitvectorTheory, + quantTheory); return new Yices2SolverContext(manager, creator, booleanTheory, pShutdownManager); } diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index 3fa91e29bc..16c0379330 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -575,6 +575,10 @@ public void testGetMultipleUFsWithBvsWithMultipleArguments() throws Exception { public void testQuantifiedUF() throws SolverException, InterruptedException { requireQuantifiers(); requireIntegers(); + assume() + .withMessage("Yices2 quantifier support is very limited at the moment") + .that(solverToUse()) + .isNotEqualTo(Solvers.YICES2); // create query: "(var == 1) && exists bound : (bound == 0 && var == func(bound))" // then check that the model contains an evaluation "func(0) := 1" @@ -630,6 +634,10 @@ public void testQuantifiedUF() throws SolverException, InterruptedException { public void testQuantifiedUF2() throws SolverException, InterruptedException { requireQuantifiers(); requireIntegers(); + assume() + .withMessage("Yices2 quantifier support is very limited at the moment") + .that(solverToUse()) + .isNotEqualTo(Solvers.YICES2); IntegerFormula var = imgr.makeVariable("var"); BooleanFormula varIsOne = imgr.equal(var, imgr.makeNumber(1)); @@ -1854,6 +1862,10 @@ private BooleanFormula makeAssignment(Formula pFormula1, Formula pFormula2) { public void quantifierTestShort() throws SolverException, InterruptedException { requireQuantifiers(); requireIntegers(); + assume() + .withMessage("Yices2 quantifier support is very limited at the moment") + .that(solverToUse()) + .isNotEqualTo(Solvers.YICES2); IntegerFormula ctr = imgr.makeVariable("x"); BooleanFormula body = imgr.equal(ctr, imgr.makeNumber(0)); diff --git a/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java b/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java index cf712ef5d7..2adf6b9644 100644 --- a/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java @@ -65,10 +65,13 @@ public class QuantifierManagerTest extends SolverBasedTest0.ParameterizedSolverB private BooleanFormula bv_forall_x_a_at_x_eq_0; @Before + public void setUp() { + requireQuantifiers(); + } + public void setUpLIA() { requireIntegers(); requireArrays(); - requireQuantifiers(); x = imgr.makeVariable("x"); a = amgr.makeArray("a", FormulaType.IntegerType, FormulaType.IntegerType); @@ -79,15 +82,9 @@ public void setUpLIA() { forall_x_a_at_x_eq_0 = qmgr.forall(ImmutableList.of(x), a_at_x_eq_0); } - @Before public void setUpBV() { requireBitvectors(); requireArrays(); - requireQuantifiers(); - assume() - .withMessage("Solver %s does not support quantifiers via JavaSMT", solverToUse()) - .that(solverToUse()) - .isNotEqualTo(Solvers.BOOLECTOR); xbv = bvmgr.makeVariable(bvWidth, "xbv"); bvArray = @@ -122,7 +119,7 @@ public void testLIAForallArrayConjunctUnsat() throws SolverException, Interrupte .isNotEqualTo(Solvers.CVC5); // (forall x . b[x] = 0) AND (b[123] = 1) is UNSAT - requireIntegers(); + setUpLIA(); BooleanFormula f = bmgr.and( @@ -139,11 +136,9 @@ public void testBVForallArrayConjunctUnsat() throws SolverException, Interrupted .isNotEqualTo(Solvers.CVC5); // (forall x . b[x] = 0) AND (b[123] = 1) is UNSAT - requireBitvectors(); + setUpBV(); // Princess does not support bitvectors in arrays assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); - // Boolector quants need to be reworked - assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); BooleanFormula f = bmgr.and( @@ -162,7 +157,7 @@ public void testLIAForallArrayConjunctSat() throws SolverException, InterruptedE .isNotEqualTo(Solvers.CVC5); // (forall x . b[x] = 0) AND (b[123] = 0) is SAT - requireIntegers(); + setUpLIA(); BooleanFormula f = bmgr.and( @@ -184,11 +179,9 @@ public void testBVForallArrayConjunctSat() throws SolverException, InterruptedEx .isNotEqualTo(Solvers.CVC5); // (forall x . b[x] = 0) AND (b[123] = 0) is SAT - requireBitvectors(); + setUpBV(); // Princess does not support bitvectors in arrays assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); - // Boolector quants need to be reworked - assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); BooleanFormula f = bmgr.and( @@ -212,7 +205,7 @@ public void testLIAForallArrayDisjunct1() throws SolverException, InterruptedExc .isNotEqualTo(Solvers.CVC5); // (forall x . b[x] = 0) AND (b[123] = 1 OR b[123] = 0) is SAT - requireIntegers(); + setUpLIA(); BooleanFormula f = bmgr.and( qmgr.forall(ImmutableList.of(x), a_at_x_eq_0), @@ -234,7 +227,7 @@ public void testLIAForallArrayDisjunctSat2() throws SolverException, Interrupted .that(solverToUse()) .isNotEqualTo(Solvers.CVC5); // (forall x . b[x] = 0) OR (b[123] = 1) is SAT - requireIntegers(); + setUpLIA(); BooleanFormula f = bmgr.or( qmgr.forall(ImmutableList.of(x), a_at_x_eq_0), @@ -255,7 +248,7 @@ public void testLIANotExistsArrayConjunct1() throws SolverException, Interrupted .isNotEqualTo(Solvers.CVC5); // (not exists x . not b[x] = 0) AND (b[123] = 1) is UNSAT - requireIntegers(); + setUpLIA(); BooleanFormula f = bmgr.and( bmgr.not(qmgr.exists(ImmutableList.of(x), bmgr.not(a_at_x_eq_0))), @@ -275,7 +268,7 @@ public void testLIANotExistsArrayConjunct2() throws SolverException, Interrupted .isNotEqualTo(Solvers.CVC5); // (not exists x . not b[x] = 0) AND (b[123] = 0) is SAT - requireIntegers(); + setUpLIA(); BooleanFormula f = bmgr.and( bmgr.not(qmgr.exists(ImmutableList.of(x), bmgr.not(a_at_x_eq_0))), @@ -295,7 +288,7 @@ public void testLIANotExistsArrayConjunct3() throws SolverException, Interrupted .isNotEqualTo(Solvers.CVC5); // (not exists x . b[x] = 0) AND (b[123] = 0) is UNSAT - requireIntegers(); + setUpLIA(); BooleanFormula f = bmgr.and( bmgr.not(qmgr.exists(ImmutableList.of(x), a_at_x_eq_0)), @@ -311,7 +304,7 @@ public void testLIANotExistsArrayDisjunct1() throws SolverException, Interrupted .isNotEqualTo(Solvers.CVC5); // (not exists x . not b[x] = 0) AND (b[123] = 1 OR b[123] = 0) is SAT - requireIntegers(); + setUpLIA(); BooleanFormula f = bmgr.and( bmgr.not(qmgr.exists(ImmutableList.of(x), bmgr.not(a_at_x_eq_0))), @@ -333,7 +326,7 @@ public void testLIANotExistsArrayDisjunct2() throws SolverException, Interrupted .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse()) .that(solverToUse()) .isNotEqualTo(Solvers.CVC5); - requireIntegers(); + setUpLIA(); BooleanFormula f = bmgr.or( bmgr.not(qmgr.exists(ImmutableList.of(x), bmgr.not(a_at_x_eq_0))), @@ -349,7 +342,7 @@ public void testLIANotExistsArrayDisjunct2() throws SolverException, Interrupted @Test public void testLIAExistsArrayConjunct1() throws SolverException, InterruptedException { // (exists x . b[x] = 0) AND (b[123] = 1) is SAT - requireIntegers(); + setUpLIA(); BooleanFormula f = bmgr.and( qmgr.exists(ImmutableList.of(x), a_at_x_eq_0), @@ -360,15 +353,13 @@ public void testLIAExistsArrayConjunct1() throws SolverException, InterruptedExc @Test public void testBVExistsArrayConjunct1() throws SolverException, InterruptedException { // (exists x . b[x] = 0) AND (b[123] = 1) is SAT - requireBitvectors(); + setUpBV(); // Princess does not support bitvectors in arrays assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); - // Boolector quants need to be reworked - assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); BooleanFormula f = bmgr.and( - qmgr.exists(ImmutableList.of(x), a_at_x_eq_0), + qmgr.exists(ImmutableList.of(xbv), bvArray_at_x_eq_0), bvmgr.equal( amgr.select(bvArray, bvmgr.makeBitvector(bvWidth, 123)), bvmgr.makeBitvector(bvWidth, 1))); @@ -377,6 +368,7 @@ public void testBVExistsArrayConjunct1() throws SolverException, InterruptedExce @Test public void testLIAExistsArrayConjunct2() throws SolverException, InterruptedException { + setUpLIA(); assume() .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse()) .that(solverToUse()) @@ -384,7 +376,6 @@ public void testLIAExistsArrayConjunct2() throws SolverException, InterruptedExc // (exists x . b[x] = 1) AND (forall x . b[x] = 0) is UNSAT - requireIntegers(); BooleanFormula f = bmgr.and(qmgr.exists(ImmutableList.of(x), a_at_x_eq_1), forall_x_a_at_x_eq_0); assertThatFormula(f).isUnsatisfiable(); @@ -398,11 +389,9 @@ public void testBVExistsArrayConjunct2() throws SolverException, InterruptedExce .isNotEqualTo(Solvers.CVC5); // (exists x . b[x] = 1) AND (forall x . b[x] = 0) is UNSAT - requireBitvectors(); + setUpBV(); // Princess does not support bitvectors in arrays assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); - // Boolector quants need to be reworked - assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); BooleanFormula f = bmgr.and(qmgr.exists(ImmutableList.of(xbv), bvArray_at_x_eq_1), bv_forall_x_a_at_x_eq_0); @@ -417,7 +406,7 @@ public void testLIAExistsArrayConjunct3() throws SolverException, InterruptedExc .isNotEqualTo(Solvers.CVC5); // (exists x . b[x] = 0) AND (forall x . b[x] = 0) is SAT - requireIntegers(); + setUpLIA(); BooleanFormula f = bmgr.and(qmgr.exists(ImmutableList.of(x), a_at_x_eq_0), forall_x_a_at_x_eq_0); @@ -432,13 +421,12 @@ public void testLIAExistsArrayConjunct3() throws SolverException, InterruptedExc @Test public void testBVExistsArrayConjunct3() throws SolverException, InterruptedException { // (exists x . b[x] = 0) AND (forall x . b[x] = 0) is SAT - requireBitvectors(); + setUpBV(); // Princess does not support bitvectors in arrays - // Boolector quants need to be reworked assume() .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse()) .that(solverToUse()) - .isNoneOf(Solvers.CVC5, Solvers.CVC4, Solvers.BOOLECTOR); + .isNoneOf(Solvers.CVC5, Solvers.CVC4); BooleanFormula f = bmgr.and(qmgr.exists(ImmutableList.of(xbv), bvArray_at_x_eq_0), bv_forall_x_a_at_x_eq_0); @@ -454,7 +442,7 @@ public void testBVExistsArrayConjunct3() throws SolverException, InterruptedExce public void testLIAExistsArrayDisjunct1() throws SolverException, InterruptedException { // (exists x . b[x] = 0) OR (forall x . b[x] = 1) is SAT - requireIntegers(); + setUpLIA(); BooleanFormula f = bmgr.or( qmgr.exists(ImmutableList.of(x), a_at_x_eq_0), @@ -470,11 +458,9 @@ public void testLIAExistsArrayDisjunct1() throws SolverException, InterruptedExc @Test public void testBVExistsArrayDisjunct1() throws SolverException, InterruptedException { // (exists x . b[x] = 0) OR (forall x . b[x] = 1) is SAT - requireBitvectors(); + setUpBV(); // Princess does not support bitvectors in arrays assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); - // Boolector quants need to be reworked - assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); BooleanFormula f = bmgr.or( @@ -487,7 +473,7 @@ public void testBVExistsArrayDisjunct1() throws SolverException, InterruptedExce public void testLIAExistsArrayDisjunct2() throws SolverException, InterruptedException { // (exists x . b[x] = 1) OR (exists x . b[x] = 1) is SAT - requireIntegers(); + setUpLIA(); BooleanFormula f = bmgr.or( qmgr.exists(ImmutableList.of(x), a_at_x_eq_1), @@ -498,11 +484,9 @@ public void testLIAExistsArrayDisjunct2() throws SolverException, InterruptedExc @Test public void testBVExistsArrayDisjunct2() throws SolverException, InterruptedException { // (exists x . b[x] = 1) OR (exists x . b[x] = 1) is SAT - requireBitvectors(); + setUpBV(); // Princess does not support bitvectors in arrays assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); - // Boolector quants need to be reworked - assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); BooleanFormula f = bmgr.or( @@ -516,6 +500,7 @@ public void testLIAContradiction() throws SolverException, InterruptedException // forall x . x = x+1 is UNSAT requireIntegers(); + x = imgr.makeVariable("x"); BooleanFormula f = qmgr.forall(ImmutableList.of(x), imgr.equal(x, imgr.add(x, imgr.makeNumber(1)))); assertThatFormula(f).isUnsatisfiable(); @@ -525,8 +510,6 @@ public void testLIAContradiction() throws SolverException, InterruptedException public void testBVContradiction() throws SolverException, InterruptedException { // forall x . x = x+1 is UNSAT requireBitvectors(); - // Boolector quants need to be reworked - assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); int width = 16; BitvectorFormula z = bvmgr.makeVariable(width, "z"); @@ -540,7 +523,7 @@ public void testBVContradiction() throws SolverException, InterruptedException { public void testLIASimple() throws SolverException, InterruptedException { // forall x . x+2 = x+1+1 is SAT requireIntegers(); - + x = imgr.makeVariable("x"); BooleanFormula f = qmgr.forall( ImmutableList.of(x), @@ -554,8 +537,6 @@ public void testLIASimple() throws SolverException, InterruptedException { public void testBVSimple() throws SolverException, InterruptedException { // forall z . z+2 = z+1+1 is SAT requireBitvectors(); - // Boolector quants need to be reworked - assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); int width = 16; BitvectorFormula z = bvmgr.makeVariable(width, "z"); @@ -572,6 +553,10 @@ public void testBVSimple() throws SolverException, InterruptedException { @Test public void testLIAEquality() throws SolverException, InterruptedException { requireIntegers(); + assume() + .withMessage("Yices2 quantifier support is very limited at the moment") + .that(solverToUse()) + .isNotEqualTo(Solvers.YICES2); // Note that due to the variable cache we simply get the existing var x here! IntegerFormula z = imgr.makeVariable("x"); @@ -584,8 +569,10 @@ public void testLIAEquality() throws SolverException, InterruptedException { @Test public void testBVEquality() throws SolverException, InterruptedException { requireBitvectors(); - // Boolector quants need to be reworked - assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); + assume() + .withMessage("Yices2 quantifier support is very limited at the moment") + .that(solverToUse()) + .isNotEqualTo(Solvers.YICES2); BitvectorFormula z = bvmgr.makeVariable(bvWidth, "z"); BitvectorFormula y = bvmgr.makeVariable(bvWidth, "y"); @@ -597,8 +584,10 @@ public void testBVEquality() throws SolverException, InterruptedException { @Test public void testBVEquality2() throws SolverException, InterruptedException { requireBitvectors(); - // Boolector quants need to be reworked - assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); + assume() + .withMessage("Yices2 quantifier support is very limited at the moment") + .that(solverToUse()) + .isNotEqualTo(Solvers.YICES2); BitvectorFormula z = bvmgr.makeVariable(bvWidth, "z"); BitvectorFormula y = bvmgr.makeVariable(bvWidth, "y"); @@ -611,8 +600,10 @@ public void testBVEquality3() throws SolverException, InterruptedException { // exists z . (forall y . z = y && z + 2 > z) // UNSAT because of bv behaviour requireBitvectors(); - // Boolector quants need to be reworked - assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); + assume() + .withMessage("Yices2 quantifier support is very limited at the moment") + .that(solverToUse()) + .isNotEqualTo(Solvers.YICES2); BitvectorFormula z = bvmgr.makeVariable(bvWidth, "z"); BitvectorFormula zPlusTwo = @@ -631,6 +622,11 @@ public void testBVEquality3() throws SolverException, InterruptedException { public void testLIABoundVariables() throws SolverException, InterruptedException { // If the free and bound vars are equal, this will be UNSAT requireIntegers(); + assume() + .withMessage("Yices2 quantifier support is very limited at the moment") + .that(solverToUse()) + .isNotEqualTo(Solvers.YICES2); + IntegerFormula aa = imgr.makeVariable("aa"); IntegerFormula one = imgr.makeNumber(1); BooleanFormula restrict = bmgr.not(imgr.equal(aa, one)); @@ -643,8 +639,10 @@ public void testLIABoundVariables() throws SolverException, InterruptedException public void testBVBoundVariables() throws SolverException, InterruptedException { // If the free and bound vars are equal, this will be UNSAT requireBitvectors(); - // Boolector quants need to be reworked - assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); + assume() + .withMessage("Yices2 quantifier support is very limited at the moment") + .that(solverToUse()) + .isNotEqualTo(Solvers.YICES2); int width = 2; BitvectorFormula aa = bvmgr.makeVariable(width, "aa"); @@ -659,6 +657,7 @@ public void testBVBoundVariables() throws SolverException, InterruptedException public void testQELight() throws InterruptedException { requireIntegers(); assume().that(solverToUse()).isEqualTo(Solvers.Z3); + x = imgr.makeVariable("x"); // exists y : (y=4 && x=y+3) --> simplified: x=7 IntegerFormula y = imgr.makeVariable("y"); BooleanFormula f1 = @@ -672,7 +671,7 @@ public void testQELight() throws InterruptedException { @Test public void testIntrospectionForall() { - requireIntegers(); + setUpLIA(); BooleanFormula forall = qmgr.forall(ImmutableList.of(x), a_at_x_eq_0); final AtomicBoolean isQuantifier = new AtomicBoolean(false); @@ -704,7 +703,7 @@ public Void visitQuantifier( @Test public void testIntrospectionExists() { - requireIntegers(); + setUpLIA(); BooleanFormula exists = qmgr.exists(ImmutableList.of(x), a_at_x_eq_0); final AtomicBoolean isQuantifier = new AtomicBoolean(false); final AtomicBoolean isForall = new AtomicBoolean(false); @@ -760,6 +759,7 @@ public void checkLIAQuantifierElimination() throws InterruptedException, SolverE // build formula: (forall x . ((x < 5) | (7 < x + y))) // quantifier-free equivalent: (2 < y) requireIntegers(); + requireQuantifierElimination(); IntegerFormula xx = imgr.makeVariable("x"); IntegerFormula yy = imgr.makeVariable("y"); BooleanFormula f = @@ -781,7 +781,9 @@ public void checkLIAQuantifierEliminationFail() throws InterruptedException, Sol // build formula: (exists x : arr[x] = 3) && (forall y: arr[y] = 2) // as there is no quantifier free equivalent, it should return the input formula. - requireIntegers(); + setUpLIA(); + requireQuantifierElimination(); + IntegerFormula xx = imgr.makeVariable("x"); IntegerFormula yy = imgr.makeVariable("y"); ArrayFormula a1 = @@ -801,12 +803,12 @@ public void checkBVQuantifierEliminationFail() throws InterruptedException, Solv // build formula: (exists x : arr[x] = 3) && (forall y: arr[y] = 2) // as there is no quantifier free equivalent, it should return the input formula. requireBitvectors(); - // Boolector quants need to be reworked + requireQuantifierElimination(); // Princess does not support bitvectors in arrays assume() .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse()) .that(solverToUse()) - .isNoneOf(Solvers.CVC5, Solvers.BOOLECTOR, Solvers.PRINCESS); + .isNoneOf(Solvers.CVC5, Solvers.PRINCESS); int width = 2; BitvectorFormula xx = bvmgr.makeVariable(width, "x_bv"); @@ -829,13 +831,11 @@ public void checkBVQuantifierEliminationFail() throws InterruptedException, Solv @Test public void checkBVQuantifierElimination() throws InterruptedException, SolverException { requireBitvectors(); - + requireQuantifierElimination(); // build formula: exists y : bv[2]. x * y = 1 // quantifier-free equivalent: x = 1 | x = 3 // or extract_0_0 x = 1 - // Boolector quants need to be reworked - assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); int i = index.getFreshId(); int width = 2; @@ -853,6 +853,7 @@ public void checkBVQuantifierElimination() throws InterruptedException, SolverEx @Test public void checkBVQuantifierElimination2() throws InterruptedException, SolverException { requireBitvectors(); + requireQuantifierElimination(); // build formula: exists a2 : (and (= a2 #x00000006) // (= b2 #x00000006) @@ -860,8 +861,6 @@ public void checkBVQuantifierElimination2() throws InterruptedException, SolverE // quantifier-free equivalent: (and (= b2 #x00000006) // (= a3 #x00000000)) - // Boolector quants need to be reworked - assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); // Z3 fails this currently. Remove once thats not longer the case! assume().that(solverToUse()).isNotEqualTo(Solvers.Z3); int width = 32; @@ -888,7 +887,7 @@ public void checkBVQuantifierElimination2() throws InterruptedException, SolverE @Test public void testExistsRestrictedRange() throws SolverException, InterruptedException { - requireIntegers(); + setUpLIA(); assume() .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse()) .that(solverToUse()) @@ -922,7 +921,7 @@ public void testExistsRestrictedRange() throws SolverException, InterruptedExcep @Test public void testExistsRestrictedRangeWithoutInconclusiveSolvers() throws SolverException, InterruptedException { - requireIntegers(); + setUpLIA(); assume() .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse()) .that(solverToUse()) @@ -946,7 +945,7 @@ public void testExistsRestrictedRangeWithoutInconclusiveSolvers() @Test public void testForallRestrictedRange() throws SolverException, InterruptedException { - requireIntegers(); + setUpLIA(); assume() .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse()) .that(solverToUse()) @@ -981,7 +980,7 @@ public void testForallRestrictedRange() throws SolverException, InterruptedExcep @Test public void testForallRestrictedRangeWithoutConclusiveSolvers() throws SolverException, InterruptedException { - requireIntegers(); + setUpLIA(); assume() .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse()) .that(solverToUse()) diff --git a/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java index 1515133f88..87cd7d2879 100644 --- a/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java @@ -93,6 +93,11 @@ public void floorIsGreaterThanValueTest() throws SolverException, InterruptedExc public void forallFloorIsLessOrEqualsValueTest() throws SolverException, InterruptedException { requireRationals(); requireQuantifiers(); + assume() + .withMessage("Yices2 quantifier support is very limited at the moment") + .that(solverToUse()) + .isNotEqualTo(Solvers.YICES2); + RationalFormula v = rmgr.makeVariable("v"); assertThatFormula(qmgr.forall(v, rmgr.lessOrEquals(rmgr.floor(v), v))).isTautological(); } @@ -101,6 +106,11 @@ public void forallFloorIsLessOrEqualsValueTest() throws SolverException, Interru public void forallFloorIsLessThanValueTest() throws SolverException, InterruptedException { requireRationals(); requireQuantifiers(); + assume() + .withMessage("Yices2 quantifier support is very limited at the moment") + .that(solverToUse()) + .isNotEqualTo(Solvers.YICES2); + RationalFormula v = rmgr.makeVariable("v"); // counterexample: all integers assertThatFormula(qmgr.forall(v, rmgr.lessThan(rmgr.floor(v), v))).isUnsatisfiable(); diff --git a/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java b/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java index 0ef9a46b14..ab8ea826f8 100644 --- a/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java @@ -251,6 +251,11 @@ public void allSatTest_withQuantifier() throws SolverException, InterruptedExcep assertThat(env.isUnsat()).isFalse(); + assume() + .withMessage("Yices2 quantifier support is very limited at the moment") + .that(solverToUse()) + .isNotEqualTo(Solvers.YICES2); + TestAllSatCallback callback = new TestAllSatCallback(); assertThat(env.allSat(callback, ImmutableList.of(pred1, pred3))).isEqualTo(EXPECTED_RESULT); diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index f38248560d..e121a0b764 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -241,6 +241,15 @@ protected final void requireQuantifiers() { .isNotNull(); } + @SuppressWarnings("unused") + protected final void requireQuantifierElimination() { + requireQuantifiers(); + assume() + .withMessage("Solver %s does not support quantifier elimination", solverToUse()) + .that(solverToUse()) + .isNoneOf(Solvers.BOOLECTOR, Solvers.MATHSAT5, Solvers.YICES2, Solvers.BITWUZLA); + } + /** Skip test if the solver does not support arrays. */ protected /*final*/ void requireArrays() { assume() diff --git a/src/org/sosy_lab/java_smt/test/SolverTacticsTest.java b/src/org/sosy_lab/java_smt/test/SolverTacticsTest.java index db5b9841ae..827c2b939e 100644 --- a/src/org/sosy_lab/java_smt/test/SolverTacticsTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverTacticsTest.java @@ -202,6 +202,7 @@ public void ufEliminationNestedUfsTest() throws SolverException, InterruptedExce public void ufEliminationNesteQuantifierTest() throws InterruptedException { requireIntegers(); requireQuantifiers(); + // f := exists v1,v2v,v3,v4 : uf(v1, v3) == uf(v2, v4) IntegerFormula variable1 = imgr.makeVariable("variable1"); IntegerFormula variable2 = imgr.makeVariable("variable2"); diff --git a/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java b/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java index 5f406a50c0..76fbb84311 100644 --- a/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java @@ -635,6 +635,7 @@ public void testUfWithBoolArg() throws SolverException, InterruptedException { public void quantifierEliminationTest1() throws SolverException, InterruptedException { requireQuantifiers(); requireIntegers(); + requireQuantifierElimination(); IntegerFormula var_B = imgr.makeVariable("b"); IntegerFormula var_C = imgr.makeVariable("c"); @@ -659,6 +660,7 @@ public void quantifierEliminationTest1() throws SolverException, InterruptedExce public void quantifierEliminationTest2() throws SolverException, InterruptedException { requireQuantifiers(); requireIntegers(); + requireQuantifierElimination(); IntegerFormula i1 = imgr.makeVariable("i@1"); IntegerFormula j1 = imgr.makeVariable("j@1"); diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index 8a7eb0eb1d..5687a0591d 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -821,6 +821,10 @@ public void testBooleanFormulaQuantifierHandling() throws Exception { .withMessage("Princess does not support quantifier over boolean variables") .that(solverToUse()) .isNotEqualTo(Solvers.PRINCESS); + assume() + .withMessage("Yices2 quantifier support is very limited at the moment") + .that(solverToUse()) + .isNotEqualTo(Solvers.YICES2); BooleanFormula x = bmgr.makeVariable("x"); BooleanFormula constraint = qmgr.forall(ImmutableList.of(x), x); @@ -837,6 +841,10 @@ public void testBooleanFormulaQuantifierRecursiveHandling() throws Exception { .withMessage("Princess does not support quantifier over boolean variables") .that(solverToUse()) .isNotEqualTo(Solvers.PRINCESS); + assume() + .withMessage("Yices2 quantifier support is very limited at the moment") + .that(solverToUse()) + .isNotEqualTo(Solvers.YICES2); BooleanFormula x = bmgr.makeVariable("x"); BooleanFormula constraint = qmgr.forall(ImmutableList.of(x), x); @@ -851,6 +859,10 @@ public void testBooleanFormulaQuantifierRecursiveHandling() throws Exception { public void testIntegerFormulaQuantifierHandlingUNSAT() throws Exception { requireQuantifiers(); requireIntegers(); + assume() + .withMessage("Yices2 quantifier support is very limited at the moment") + .that(solverToUse()) + .isNotEqualTo(Solvers.YICES2); IntegerFormula x = imgr.makeVariable("x"); BooleanFormula xEq1 = bmgr.not(imgr.equal(imgr.makeNumber(1), x)); @@ -926,6 +938,10 @@ public void testNestedIntegerFormulaQuantifierHandling() throws Exception { requireIntegers(); // Z3 returns UNKNOWN as its quantifiers can not handle this. assume().that(solverToUse()).isNotEqualTo(Solvers.Z3); + assume() + .withMessage("Yices2 quantifier support is very limited at the moment") + .that(solverToUse()) + .isNotEqualTo(Solvers.YICES2); IntegerFormula x = imgr.makeVariable("x"); BooleanFormula xEq1 = imgr.equal(x, imgr.makeNumber(1)); @@ -944,6 +960,10 @@ public void testNestedIntegerFormulaQuantifierRecursiveHandling() throws Excepti requireIntegers(); // Z3 returns UNKNOWN as its quantifiers can not handle this. assume().that(solverToUse()).isNotEqualTo(Solvers.Z3); + assume() + .withMessage("Yices2 quantifier support is very limited at the moment") + .that(solverToUse()) + .isNotEqualTo(Solvers.YICES2); IntegerFormula x = imgr.makeVariable("x"); BooleanFormula xEq1 = imgr.equal(x, imgr.makeNumber(1)); @@ -1134,6 +1154,8 @@ public void testTransformationInsideQuantifiersWithTrue() throws SolverException, InterruptedException { requireQuantifiers(); requireIntegers(); + requireQuantifierElimination(); + List quantifiedVars = ImmutableList.of(imgr.makeVariable("x")); BooleanFormula body = bmgr.makeTrue(); BooleanFormula f = qmgr.exists(quantifiedVars, body); @@ -1147,6 +1169,8 @@ public void testTransformationInsideQuantifiersWithFalse() throws SolverException, InterruptedException { requireQuantifiers(); requireIntegers(); + requireQuantifierElimination(); + List quantifiedVars = ImmutableList.of(imgr.makeVariable("x")); BooleanFormula body = bmgr.makeFalse(); BooleanFormula f = qmgr.exists(quantifiedVars, body); @@ -1160,6 +1184,8 @@ public void testTransformationInsideQuantifiersWithVariable() throws SolverException, InterruptedException { requireQuantifiers(); requireIntegers(); + requireQuantifierElimination(); + List quantifiedVars = ImmutableList.of(imgr.makeVariable("x")); BooleanFormula body = bmgr.makeVariable("b"); BooleanFormula f = qmgr.exists(quantifiedVars, body);