Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Added array literal creation to API and implementation #367

Closed
wants to merge 4 commits into from
Closed

Added array literal creation to API and implementation #367

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
a0e0e8f
Added array literal creation to API and implementation
leventeBajczi Mar 24, 2024
7a9ec22
Fix docstring
leventeBajczi Mar 24, 2024
4363b31
Added extra tests, removed default implementation for uninit array li…
leventeBajczi Mar 24, 2024
dc58237
Removed unused vars
leventeBajczi Mar 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 1 addition & 12 deletions .idea/ant.xml
View file
Open in desktop
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please do not change basic project files.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ah sorry, I didn't pay attention when adding files to the commit (and IntelliJ is adamant on changing these all the time..)

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

24 changes: 24 additions & 0 deletions src/org/sosy_lab/java_smt/api/ArrayFormulaManager.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,30 @@ <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> store(
<TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> makeArray(
String pName, ArrayFormulaType<TI, TE> type);

/** Create a new array constant with uninitialized values. */
<TI extends Formula, TE extends Formula, FTI extends FormulaType<TI>, FTE extends FormulaType<TE>>
leventeBajczi marked this conversation as resolved.
Show resolved Hide resolved
ArrayFormula<TI, TE> makeArray(FTI pIndexType, FTE pElementType);

/** Create a new array constant with uninitialized values. */
<TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> makeArray(
kfriedberger marked this conversation as resolved.
Show resolved Hide resolved
ArrayFormulaType<TI, TE> type);

/**
* Create a new array constant with values initialized to elseElem.
*
* @param elseElem: The default value of all entries in the array.
*/
<TI extends Formula, TE extends Formula, FTI extends FormulaType<TI>, FTE extends FormulaType<TE>>
ArrayFormula<TI, TE> makeArray(TE elseElem, FTI pIndexType, FTE pElementType);

/**
* Create a new array constant with values initialized to elseElem.
*
* @param elseElem: The default value of all entries in the array.
*/
<TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> makeArray(
TE elseElem, ArrayFormulaType<TI, TE> type);

/** Make a {@link BooleanFormula} that represents the equality of two {@link ArrayFormula}. */
<TI extends Formula, TE extends Formula> BooleanFormula equivalence(
ArrayFormula<TI, TE> pArray1, ArrayFormula<TI, TE> pArray2);
Expand Down
50 changes: 50 additions & 0 deletions src/org/sosy_lab/java_smt/basicimpl/AbstractArrayFormulaManager.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,6 +80,56 @@ ArrayFormula<TI, TE> makeArray(String pName, FTI pIndexType, FTE pElementType) {
protected abstract <TI extends Formula, TE extends Formula> TFormulaInfo internalMakeArray(
String pName, FormulaType<TI> pIndexType, FormulaType<TE> pElementType);

@Override
public <
TI extends Formula,
TE extends Formula,
FTI extends FormulaType<TI>,
FTE extends FormulaType<TE>>
ArrayFormula<TI, TE> makeArray(FTI pIndexType, FTE pElementType) {
final TFormulaInfo arrayConst = internalMakeArray(pIndexType, pElementType);
return getFormulaCreator().encapsulateArray(arrayConst, pIndexType, pElementType);
}

@Override
public <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> makeArray(
ArrayFormulaType<TI, TE> type) {
final TFormulaInfo arrayConst = internalMakeArray(type.getIndexType(), type.getElementType());
return getFormulaCreator()
.encapsulateArray(arrayConst, type.getIndexType(), type.getElementType());
}

@Override
public <
TI extends Formula,
TE extends Formula,
FTI extends FormulaType<TI>,
FTE extends FormulaType<TE>>
ArrayFormula<TI, TE> makeArray(TE elseElem, FTI pIndexType, FTE pElementType) {
final TFormulaInfo arrayConst =
internalMakeArray(extractInfo(elseElem), pIndexType, pElementType);
return getFormulaCreator().encapsulateArray(arrayConst, pIndexType, pElementType);
}

@Override
public <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> makeArray(
TE elseElem, ArrayFormulaType<TI, TE> type) {
final TFormulaInfo arrayConst =
internalMakeArray(extractInfo(elseElem), type.getIndexType(), type.getElementType());
return getFormulaCreator()
.encapsulateArray(arrayConst, type.getIndexType(), type.getElementType());
}

protected <TI extends Formula, TE extends Formula> TFormulaInfo internalMakeArray(
FormulaType<TI> pIndexType, FormulaType<TE> pElementType) {
throw new UnsupportedOperationException("Array literals are not supported.");
}

protected <TI extends Formula, TE extends Formula> TFormulaInfo internalMakeArray(
TFormulaInfo elseElem, FormulaType<TI> pIndexType, FormulaType<TE> pElementType) {
throw new UnsupportedOperationException("Initialized arrays are not supported.");
}

@Override
public <TI extends Formula> FormulaType<TI> getIndexType(ArrayFormula<TI, ?> pArray) {
return getFormulaCreator().getArrayFormulaIndexType(pArray);
Expand Down
36 changes: 36 additions & 0 deletions src/org/sosy_lab/java_smt/delegate/statistics/StatisticsArrayFormulaManager.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,42 @@ public <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> makeArray(
return delegate.makeArray(pName, pType);
}

@Override
public <
TI extends Formula,
TE extends Formula,
FTI extends FormulaType<TI>,
FTE extends FormulaType<TE>>
ArrayFormula<TI, TE> makeArray(FTI pIndexType, FTE pElementType) {
stats.arrayOperations.getAndIncrement();
return delegate.makeArray(pIndexType, pElementType);
}

@Override
public <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> makeArray(
ArrayFormulaType<TI, TE> type) {
stats.arrayOperations.getAndIncrement();
return delegate.makeArray(type);
}

@Override
public <
TI extends Formula,
TE extends Formula,
FTI extends FormulaType<TI>,
FTE extends FormulaType<TE>>
ArrayFormula<TI, TE> makeArray(TE elseElem, FTI pIndexType, FTE pElementType) {
stats.arrayOperations.getAndIncrement();
return delegate.makeArray(elseElem, pIndexType, pElementType);
}

@Override
public <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> makeArray(
TE elseElem, ArrayFormulaType<TI, TE> type) {
stats.arrayOperations.getAndIncrement();
return delegate.makeArray(elseElem, type);
}

@Override
public <TI extends Formula, TE extends Formula> BooleanFormula equivalence(
ArrayFormula<TI, TE> pArray1, ArrayFormula<TI, TE> pArray2) {
Expand Down
40 changes: 40 additions & 0 deletions src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedArrayFormulaManager.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,46 @@ public <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> makeArray(
}
}

@Override
public <
TI extends Formula,
TE extends Formula,
FTI extends FormulaType<TI>,
FTE extends FormulaType<TE>>
ArrayFormula<TI, TE> makeArray(FTI pIndexType, FTE pElementType) {
synchronized (sync) {
return delegate.makeArray(pIndexType, pElementType);
}
}

@Override
public <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> makeArray(
ArrayFormulaType<TI, TE> type) {
synchronized (sync) {
return delegate.makeArray(type);
}
}

@Override
public <
TI extends Formula,
TE extends Formula,
FTI extends FormulaType<TI>,
FTE extends FormulaType<TE>>
ArrayFormula<TI, TE> makeArray(TE elseElem, FTI pIndexType, FTE pElementType) {
synchronized (sync) {
return delegate.makeArray(elseElem, pIndexType, pElementType);
}
}

@Override
public <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> makeArray(
TE elseElem, ArrayFormulaType<TI, TE> type) {
synchronized (sync) {
return delegate.makeArray(elseElem, type);
}
}

@Override
public <TI extends Formula, TE extends Formula> BooleanFormula equivalence(
ArrayFormula<TI, TE> pArray1, ArrayFormula<TI, TE> pArray2) {
Expand Down
9 changes: 9 additions & 0 deletions src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ArrayFormulaManager.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,15 @@ protected <TI extends Formula, TE extends Formula> Term internalMakeArray(
return getFormulaCreator().makeVariable(cvc5ArrayType, pName);
}

@Override
protected <TI extends Formula, TE extends Formula> Term internalMakeArray(
Term elseElem, FormulaType<TI> pIndexType, FormulaType<TE> pElementType) {
final ArrayFormulaType<TI, TE> arrayFormulaType =
FormulaType.getArrayType(pIndexType, pElementType);
final Sort cvc5ArrayType = toSolverType(arrayFormulaType);
return solver.mkConstArray(cvc5ArrayType, elseElem);
}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I took this part of the code and merged it to master.


@Override
protected Term equivalence(Term pArray1, Term pArray2) {
return solver.mkTerm(Kind.EQUAL, pArray1, pArray2);
Expand Down
10 changes: 10 additions & 0 deletions src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5ArrayFormulaManager.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@

package org.sosy_lab.java_smt.solvers.mathsat5;

import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_array_const;
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_array_read;
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_array_write;
import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_equal;
Expand Down Expand Up @@ -48,6 +49,15 @@ protected <TI extends Formula, TE extends Formula> Long internalMakeArray(
return getFormulaCreator().makeVariable(mathsatArrayType, pName);
}

@Override
protected <TI extends Formula, TE extends Formula> Long internalMakeArray(
Long elseElem, FormulaType<TI> pIndexType, FormulaType<TE> pElementType) {
final ArrayFormulaType<TI, TE> arrayFormulaType =
FormulaType.getArrayType(pIndexType, pElementType);
final Long mathsatArrayType = toSolverType(arrayFormulaType);
return msat_make_array_const(mathsatEnv, mathsatArrayType, elseElem);
}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I took this part of the code and merged it to master.


@Override
protected Long equivalence(Long pArray1, Long pArray2) {
return msat_make_equal(mathsatEnv, pArray1, pArray2);
Expand Down
17 changes: 17 additions & 0 deletions src/org/sosy_lab/java_smt/solvers/z3/Z3ArrayFormulaManager.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
package org.sosy_lab.java_smt.solvers.z3;

import com.microsoft.z3.Native;
import java.util.List;
import org.sosy_lab.java_smt.api.Formula;
import org.sosy_lab.java_smt.api.FormulaType;
import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType;
Expand Down Expand Up @@ -45,6 +46,22 @@ protected <TI extends Formula, TE extends Formula> Long internalMakeArray(
return getFormulaCreator().makeVariable(z3ArrayType, pName);
}

@Override
protected <TI extends Formula, TE extends Formula> Long internalMakeArray(
FormulaType<TI> pIndexType, FormulaType<TE> pElementType) {
long func =
getFormulaCreator()
.declareUFImpl(
"__unnamed_arr", toSolverType(pElementType), List.of(toSolverType(pIndexType)));
Copy link
Member

@kfriedberger kfriedberger Mar 24, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

return Native.mkAsArray(z3context, func);
}

@Override
protected <TI extends Formula, TE extends Formula> Long internalMakeArray(
Long elseElem, FormulaType<TI> pIndexType, FormulaType<TE> pElementType) {
return Native.mkConstArray(z3context, toSolverType(pIndexType), elseElem);
}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I took this part of the code and merged it to master.


@Override
protected Long equivalence(Long pArray1, Long pArray2) {
return Native.mkEq(z3context, pArray1, pArray2);
Expand Down
Loading