Add Proper Yices2 Quantifier Support #447
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -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_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<Integer, Integer, Long, | |
| YICES_VARIABLE, | ||
| YICES_UNINTERPRETED_TERM); | ||
|
|
||
| /** | ||
| * Maps a name and a free variable or function type to a concrete formula node. We allow only 1 | ||
| * type per var name, meaning there is only 1 column per row! | ||
| */ | ||
| private final Table<String, Integer, Integer> 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 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> R visit(FormulaVisitor<R> pVisitor, Formula pFormula, Integer pF) { | ||
| int constructor = yices_term_constructor(pF); | ||
|
|
@@ -258,6 +325,22 @@ public <R> R visit(FormulaVisitor<R> 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<Formula> 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")) { | ||
|
There was a problem hiding this comment. Yices is open source. We could find out, how Yices computes the string and check for the flag that tells the difference from FORALL to EXISTS: There was a problem hiding this comment. Yices does not seem to have a separate term for To see if we have a I couldn't find any public API for this, but we could probably just keep track of the polarity in the visitor. There was a problem hiding this comment. No actually that is the solution! Thank you very much! This opens another questions however: do we traverse and/or rebuild terms correctly with this? There was a problem hiding this comment. (I fear that the visitor might rebuild a formula There was a problem hiding this comment. Exactly as i expected, this happens. I added a test that should work for all solvers that checks this for both types of quantifiers. There was a problem hiding this comment. OK so Yices2 does simply transform the formula on-the-fly while traversing it. Do we want to accept this behavior @kfriedberger ? |
||
| // 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<Integer> pA | |
| } else { | ||
| yicesFuncType = yices_function_type(size, argTypeArray, pReturnType); | ||
| } | ||
| int uf = createNamedVariable(yicesFuncType, pName); | ||
| return uf; | ||
| } | ||
|
|
||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
it looks like some ELSE-cases are missing. Is this intentional?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is intentional. I added documentation for it.
Essentially: Names work like a stack in Yices2. If we associate a term with a name, we get that term if we ask yices_get_term_by_name(). However, if we create bound variables, we associate them with the same name as the free variable (so that it has the same name). This pushes the name stack, and we get the bound var when asking yices_get_term_by_name(). That's why i added a cache for free vars. So this way we can re-use bound variables, and don't clash with free vars.