-
Notifications
You must be signed in to change notification settings - Fork 54
Add support for arrays in Yices2 #523
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
Show all changes
6 commits
Select commit
Hold shift + click to select a range
afdcd46
Yices: Add array theory
daniel-raffler fc68ec6
Yices: Fix Checkstyle issues
daniel-raffler 2d3ed63
Yices2: avoid repeated access to map.
kfriedberger 07c40f7
Yices2: rename constant for function-application or array-select.
kfriedberger 4dfcf13
SolverFormulaIOTest: check declared function symbols, also for arrays.
kfriedberger c410213
SolverFormulaIOTest: remove empty statement / unneeded semicolon.
kfriedberger File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
77 changes: 77 additions & 0 deletions
77
src/org/sosy_lab/java_smt/solvers/yices2/Yices2ArrayFormulaManager.java
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 |
|---|---|---|
| @@ -0,0 +1,77 @@ | ||
| /* | ||
| * This file is part of JavaSMT, | ||
| * an API wrapper for a collection of SMT solvers: | ||
| * https://github.com/sosy-lab/java-smt | ||
| * | ||
| * SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org> | ||
| * | ||
| * SPDX-License-Identifier: Apache-2.0 | ||
| */ | ||
|
|
||
| package org.sosy_lab.java_smt.solvers.yices2; | ||
|
|
||
| import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_application; | ||
| import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_eq; | ||
| import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_function_type; | ||
| import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_lambda; | ||
| import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_new_variable; | ||
| import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_update; | ||
|
|
||
| import com.google.common.collect.HashBasedTable; | ||
| import com.google.common.collect.Table; | ||
| import org.sosy_lab.java_smt.api.Formula; | ||
| import org.sosy_lab.java_smt.api.FormulaType; | ||
| import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager; | ||
|
|
||
| @SuppressWarnings({"ClassTypeParameterName", "MethodTypeParameterName"}) | ||
| public class Yices2ArrayFormulaManager | ||
| extends AbstractArrayFormulaManager<Integer, Integer, Long, Integer> { | ||
|
|
||
| /** | ||
| * Cache with constant array values. | ||
| * | ||
| * <p>Used in {@link #internalMakeArray(FormulaType, FormulaType, Integer)} to guarantee that | ||
| * existing constant array values are never re-created | ||
| */ | ||
| private final Table<Integer, Integer, Integer> constCache = HashBasedTable.create(); | ||
|
|
||
| public Yices2ArrayFormulaManager(Yices2FormulaCreator pCreator) { | ||
| super(pCreator); | ||
| } | ||
|
|
||
| @Override | ||
| protected Integer select(Integer pArray, Integer pIndex) { | ||
| return yices_application(pArray, 1, new int[] {pIndex}); | ||
| } | ||
|
|
||
| @Override | ||
| protected Integer store(Integer pArray, Integer pIndex, Integer pValue) { | ||
| return yices_update(pArray, 1, new int[] {pIndex}, pValue); | ||
| } | ||
|
|
||
| @Override | ||
| protected <TI extends Formula, TE extends Formula> Integer internalMakeArray( | ||
| String pName, FormulaType<TI> pIndexType, FormulaType<TE> pElementType) { | ||
| var yicesFuncType = | ||
| yices_function_type(1, new int[] {toSolverType(pIndexType)}, toSolverType(pElementType)); | ||
| return ((Yices2FormulaCreator) getFormulaCreator()).createNamedVariable(yicesFuncType, pName); | ||
| } | ||
|
|
||
| @Override | ||
| protected <TI extends Formula, TE extends Formula> Integer internalMakeArray( | ||
| FormulaType<TI> pIndexType, FormulaType<TE> pElementType, Integer defaultElement) { | ||
| var arraySort = toSolverType(FormulaType.getArrayType(pIndexType, pElementType)); | ||
| var constantArray = constCache.get(arraySort, defaultElement); | ||
| if (constantArray == null) { | ||
| constantArray = | ||
| yices_lambda(1, new int[] {yices_new_variable(toSolverType(pIndexType))}, defaultElement); | ||
| constCache.put(arraySort, defaultElement, constantArray); | ||
| } | ||
| return constantArray; | ||
| } | ||
|
|
||
| @Override | ||
| protected Integer equivalence(Integer pArray1, Integer pArray2) { | ||
| return yices_eq(pArray1, pArray2); | ||
| } | ||
| } |
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.
Uh oh!
There was an error while loading. Please reload this page.