forked from hernanponcedeleon/Dat3M
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add support for encoding tuples (Tuple theory) (hernanponcedeleon#775)
* Add support for AggregateTypes in encoding. Also add new Aggregate operations EQ and NEQ * Remove RegisterDecomposition.java
- Loading branch information
1 parent
1b8251d
commit c5468bf
Showing
19 changed files
with
251 additions
and
99 deletions.
There are no files selected for viewing
This file contains 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 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
45 changes: 45 additions & 0 deletions
45
dartagnan/src/main/java/com/dat3m/dartagnan/encoding/formulas/TupleFormula.java
This file contains 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,45 @@ | ||
| package com.dat3m.dartagnan.encoding.formulas; | ||
|
|
||
| import org.sosy_lab.java_smt.api.Formula; | ||
|
|
||
| import java.util.List; | ||
| import java.util.stream.Collectors; | ||
|
|
||
| /* | ||
| Implementation Note: | ||
| We implement JavaSMT's Formula interface so this appears like a normal formula, | ||
| however, it won't support many of JavaSMT's features like formula traversal. | ||
| */ | ||
| public class TupleFormula implements Formula { | ||
|
|
||
| final List<Formula> elements; | ||
|
|
||
| TupleFormula(List<Formula> elements) { | ||
| this.elements = elements; | ||
| } | ||
|
|
||
| @Override | ||
| public String toString() { | ||
| return elements.stream() | ||
| .map(Object::toString) | ||
| .collect(Collectors.joining(",", "{ ", " }")); | ||
| } | ||
|
|
||
| @Override | ||
| public int hashCode() { | ||
| return elements.hashCode(); | ||
| } | ||
|
|
||
| @Override | ||
| public boolean equals(Object obj) { | ||
| if (obj == this) { | ||
| return true; | ||
| } else if (obj == null || obj.getClass() != this.getClass()) { | ||
| return false; | ||
| } else { | ||
| final TupleFormula other = (TupleFormula) obj; | ||
| return this.elements.equals(other.elements); | ||
| } | ||
| } | ||
|
|
||
| } |
45 changes: 45 additions & 0 deletions
45
dartagnan/src/main/java/com/dat3m/dartagnan/encoding/formulas/TupleFormulaManager.java
This file contains 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,45 @@ | ||
| package com.dat3m.dartagnan.encoding.formulas; | ||
|
|
||
| import com.dat3m.dartagnan.encoding.EncodingContext; | ||
| import com.google.common.base.Preconditions; | ||
| import org.sosy_lab.java_smt.api.BooleanFormula; | ||
| import org.sosy_lab.java_smt.api.BooleanFormulaManager; | ||
| import org.sosy_lab.java_smt.api.Formula; | ||
|
|
||
| import java.util.ArrayList; | ||
| import java.util.List; | ||
|
|
||
|
|
||
| /* | ||
| Note: This class cannot actually create variables of tuple type and merely gives the illusion of | ||
| a proper tuple theory. | ||
| To simulate tuple variables, the user instead has to construct tuples of variables. | ||
| */ | ||
| public final class TupleFormulaManager { | ||
|
|
||
| private final EncodingContext context; | ||
|
|
||
| public TupleFormulaManager(EncodingContext context) { | ||
| this.context = context; | ||
|
|
||
| } | ||
|
|
||
| public BooleanFormula equal(TupleFormula x, TupleFormula y) { | ||
| Preconditions.checkArgument(x.elements.size() == y.elements.size()); | ||
| final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); | ||
| final List<BooleanFormula> enc = new ArrayList<>(); | ||
| for (int i = 0; i < x.elements.size(); i++) { | ||
| enc.add(context.equal(x.elements.get(i), y.elements.get(i)));; | ||
| } | ||
| return bmgr.and(enc); | ||
| } | ||
|
|
||
| public Formula extract(TupleFormula f, int index) { | ||
| Preconditions.checkArgument(0 <= index && index < f.elements.size()); | ||
| return f.elements.get(index); | ||
| } | ||
|
|
||
| public TupleFormula makeTuple(List<Formula> elements) { | ||
| return new TupleFormula(elements); | ||
| } | ||
| } |
This file contains 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 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 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
21 changes: 21 additions & 0 deletions
21
dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/AggregateCmpExpr.java
This file contains 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,21 @@ | ||
| package com.dat3m.dartagnan.expression.aggregates; | ||
|
|
||
| import com.dat3m.dartagnan.expression.Expression; | ||
| import com.dat3m.dartagnan.expression.ExpressionVisitor; | ||
| import com.dat3m.dartagnan.expression.base.BinaryExpressionBase; | ||
| import com.dat3m.dartagnan.expression.type.AggregateType; | ||
| import com.dat3m.dartagnan.expression.type.BooleanType; | ||
| import com.dat3m.dartagnan.expression.utils.ExpressionHelper; | ||
|
|
||
| public final class AggregateCmpExpr extends BinaryExpressionBase<BooleanType, AggregateCmpOp> { | ||
|
|
||
| public AggregateCmpExpr(BooleanType type, Expression left, AggregateCmpOp kind, Expression right) { | ||
| super(type, kind, left, right); | ||
| ExpressionHelper.checkSameExpectedType(left, right, AggregateType.class); | ||
| } | ||
|
|
||
| @Override | ||
| public <T> T accept(ExpressionVisitor<T> visitor) { | ||
| return visitor.visitAggregateCmpExpression(this); | ||
| } | ||
| } |
20 changes: 20 additions & 0 deletions
20
dartagnan/src/main/java/com/dat3m/dartagnan/expression/aggregates/AggregateCmpOp.java
This file contains 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,20 @@ | ||
| package com.dat3m.dartagnan.expression.aggregates; | ||
|
|
||
| import com.dat3m.dartagnan.expression.ExpressionKind; | ||
|
|
||
| public enum AggregateCmpOp implements ExpressionKind { | ||
| EQ, NEQ; | ||
|
|
||
| @Override | ||
| public String toString() { | ||
| return getSymbol(); | ||
| } | ||
|
|
||
| @Override | ||
| public String getSymbol() { | ||
| return switch (this) { | ||
| case EQ -> "=="; | ||
| case NEQ -> "!="; | ||
| }; | ||
| } | ||
| } |
2 changes: 1 addition & 1 deletion
2
...tagnan/expression/misc/ConstructExpr.java → .../expression/aggregates/ConstructExpr.java
This file contains 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
2 changes: 1 addition & 1 deletion
2
...artagnan/expression/misc/ExtractExpr.java → ...an/expression/aggregates/ExtractExpr.java
This file contains 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.