Added array literal creation to API and implementation #367
Conversation
| long func = | ||
| getFormulaCreator() | ||
| .declareUFImpl( | ||
| "__unnamed_arr", toSolverType(pElementType), List.of(toSolverType(pIndexType))); |
There was a problem hiding this comment.
Is this extra UF really necessary?
How can we create two arrays with default values, when they have distinct types? (test missing)
Is this name forbidden as normal variable name and excluded in model generation? (test missing)
There was a problem hiding this comment.
I don't see another way of creating a non-initialized array literal. I added some extra tests to verify that these do not create problems with e.g. vars with the same name. It turns out that only Z3 works well with such literals (without a default value), and only Z3, MathSAT and CVC5 work with initialized literals.
|
I can see that the |
|
|
There was a problem hiding this comment.
Please do not change basic project files.
There was a problem hiding this comment.
ah sorry, I didn't pay attention when adding files to the commit (and IntelliJ is adamant on changing these all the time..)
| FormulaType.getArrayType(pIndexType, pElementType); | ||
| final Sort cvc5ArrayType = toSolverType(arrayFormulaType); | ||
| return solver.mkConstArray(cvc5ArrayType, elseElem); | ||
| } |
There was a problem hiding this comment.
I took this part of the code and merged it to master.
| FormulaType.getArrayType(pIndexType, pElementType); | ||
| final Long mathsatArrayType = toSolverType(arrayFormulaType); | ||
| return msat_make_array_const(mathsatEnv, mathsatArrayType, elseElem); | ||
| } |
There was a problem hiding this comment.
I took this part of the code and merged it to master.
| protected <TI extends Formula, TE extends Formula> Long internalMakeArray( | ||
| Long elseElem, FormulaType<TI> pIndexType, FormulaType<TE> pElementType) { | ||
| return Native.mkConstArray(z3context, toSolverType(pIndexType), elseElem); | ||
| } |
There was a problem hiding this comment.
I took this part of the code and merged it to master.
| // init array cannot read any value besides default | ||
| assertThatFormula(bvmgr.equal(numM1, amgr.select(arr, num2))).isUnsatisfiable(); | ||
| assertThatFormula(bvmgr.equal(num0, amgr.select(arr, num2))).isTautological(); | ||
| } |
There was a problem hiding this comment.
I took this part of these tests as basis for further tests that are merged to master.
|
I believe you're right that uninitialized arrays do not make a lot of sense. I also see that for the initialized arrays you merged the modifications to master manually - I'm closing this PR. Thanks for the help! |
As mentioned in #360, currently, array literals are not supported by the API. This PR adds two new methods to this end, one without a default value, and one with a default (else) value. I also added some tests to verify that these work normally.