Skip to content

Commit

Permalink
Use solverfactory instead of supplier and change output path
Browse files Browse the repository at this point in the history
  • Loading branch information
@mondokm
mondokm committed Feb 15, 2024
1 parent 6fccd26 commit e70661a
Showing 1 changed file with 22 additions and 13 deletions.
35 changes: 22 additions & 13 deletions ...mon/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddExpressionTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
import hu.bme.mit.delta.java.mdd.*;
import hu.bme.mit.delta.mdd.MddVariableDescriptor;
import hu.bme.mit.theta.analysis.algorithm.symbolic.symbolicnode.MddValuationCollector;
import hu.bme.mit.theta.analysis.algorithm.symbolic.symbolicnode.SolverPool;
import hu.bme.mit.theta.analysis.algorithm.symbolic.symbolicnode.expression.ExprLatticeDefinition;
import hu.bme.mit.theta.analysis.algorithm.symbolic.symbolicnode.expression.MddExpressionTemplate;
import hu.bme.mit.theta.analysis.utils.MddNodeVisualizer;
Expand Down Expand Up @@ -47,7 +48,8 @@ public void exprNodeTest1(){
// x >= 2 && y = x + 1 && x <= 6
Expr<BoolType> expr = And(Geq(declX.getRef(),Int(2)), Eq(declY.getRef(),Add(declX.getRef(),Int(1))),Leq(declX.getRef(), Int(6)));

MddNode rootNode = x.checkInNode(MddExpressionTemplate.of(expr, o -> (Decl) o, Z3SolverFactory.getInstance()::createSolver));
SolverPool solverPool = new SolverPool(Z3SolverFactory.getInstance());
MddNode rootNode = x.checkInNode(MddExpressionTemplate.of(expr, o -> (Decl) o, solverPool));

var interpreter = x.getNodeInterpreter(rootNode);

Expand Down Expand Up @@ -77,7 +79,7 @@ public void exprNodeTest1(){

final Graph graph = new MddNodeVisualizer(MddExpressionTest::nodeToString).visualize(rootNode);
try {
GraphvizWriter.getInstance().writeFile(graph, "/home/milan/programming/mdd.dot");
GraphvizWriter.getInstance().writeFile(graph, "build\\mdd.dot");
} catch (FileNotFoundException e) {
e.printStackTrace();
}
Expand All @@ -99,7 +101,8 @@ public void exprNodeTest2(){

Expr<BoolType> expr = And(Or(declA.getRef(), Not(declB.getRef())), Eq(declX.getRef(), Int(2)));

MddNode rootNode = a.checkInNode(MddExpressionTemplate.of(expr, o -> (Decl) o, Z3SolverFactory.getInstance()::createSolver));
SolverPool solverPool = new SolverPool(Z3SolverFactory.getInstance());
MddNode rootNode = a.checkInNode(MddExpressionTemplate.of(expr, o -> (Decl) o, solverPool));

for (var c = rootNode.cursor(); c.moveNext(); ){}

Expand All @@ -121,7 +124,7 @@ public void exprNodeTest2(){

final Graph graph = new MddNodeVisualizer(MddExpressionTest::nodeToString).visualize(rootNode);
try {
GraphvizWriter.getInstance().writeFile(graph, "/home/milan/programming/mdd.dot");
GraphvizWriter.getInstance().writeFile(graph, "build\\mdd.dot");
} catch (FileNotFoundException e) {
e.printStackTrace();
}
Expand All @@ -131,6 +134,8 @@ public void exprNodeTest2(){
@Test
public void exprNodeTest3(){

// TODO need to fix nodeinterpreters and cursors

MddGraph<Expr> mddGraph = JavaMddFactory.getDefault().createMddGraph(ExprLatticeDefinition.forExpr());
MddVariableOrder varOrder = JavaMddFactory.getDefault().createMddVariableOrder(mddGraph);

Expand All @@ -145,7 +150,8 @@ public void exprNodeTest3(){
// y >= 2 && z = y + 1 && y <= 6
Expr<BoolType> expr = And(Geq(declY.getRef(),Int(2)), Eq(declZ.getRef(),Add(declY.getRef(),Int(1))),Leq(declY.getRef(), Int(6)));

MddNode rootNode = x.checkInNode(MddExpressionTemplate.of(expr, o -> (Decl) o, Z3SolverFactory.getInstance()::createSolver));
SolverPool solverPool = new SolverPool(Z3SolverFactory.getInstance());
MddNode rootNode = x.checkInNode(MddExpressionTemplate.of(expr, o -> (Decl) o, solverPool));

var interpreter = x.getNodeInterpreter(rootNode);

Expand All @@ -165,7 +171,7 @@ public void exprNodeTest3(){

final Graph graph = new MddNodeVisualizer(MddExpressionTest::nodeToString).visualize(rootNode);
try {
GraphvizWriter.getInstance().writeFile(graph, "/home/milan/programming/mdd.dot");
GraphvizWriter.getInstance().writeFile(graph, "build\\mdd.dot");
} catch (FileNotFoundException e) {
e.printStackTrace();
}
Expand All @@ -188,7 +194,8 @@ public void exprNodeTest4(){
// x >= 2 && y = x + 1 && x <= 6 && z = y + 2
Expr<BoolType> expr = And(Geq(declX.getRef(),Int(2)), Eq(declY.getRef(),Add(declX.getRef(),Int(1))),Leq(declX.getRef(), Int(6)), Eq(declZ.getRef(), Add(declY.getRef(), Int(2))));

MddNode rootNode = x.checkInNode(MddExpressionTemplate.of(expr, o -> (Decl) o, Z3SolverFactory.getInstance()::createSolver));
SolverPool solverPool = new SolverPool(Z3SolverFactory.getInstance());
MddNode rootNode = x.checkInNode(MddExpressionTemplate.of(expr, o -> (Decl) o, solverPool));

var interpreter = x.getNodeInterpreter(rootNode);

Expand Down Expand Up @@ -218,7 +225,7 @@ public void exprNodeTest4(){

final Graph graph = new MddNodeVisualizer(MddExpressionTest::nodeToString).visualize(rootNode);
try {
GraphvizWriter.getInstance().writeFile(graph, "/home/milan/programming/mdd.dot");
GraphvizWriter.getInstance().writeFile(graph, "build\\mdd.dot");
} catch (FileNotFoundException e) {
e.printStackTrace();
}
Expand All @@ -242,7 +249,8 @@ public void exprNodeTest5(){
// x = y && y = z && z = 2
Expr<BoolType> expr = And(Eq(declX.getRef(), declY.getRef()), And(Eq(declY.getRef(),declZ.getRef()), Eq(declZ.getRef(), Int(2))));

MddNode rootNode = x.checkInNode(MddExpressionTemplate.of(expr, o -> (Decl) o, Z3SolverFactory.getInstance()::createSolver));
SolverPool solverPool = new SolverPool(Z3SolverFactory.getInstance());
MddNode rootNode = x.checkInNode(MddExpressionTemplate.of(expr, o -> (Decl) o, solverPool));

var interpreter = x.getNodeInterpreter(rootNode);

Expand All @@ -257,7 +265,7 @@ public void exprNodeTest5(){

final Graph graph = new MddNodeVisualizer(MddExpressionTest::nodeToString).visualize(rootNode);
try {
GraphvizWriter.getInstance().writeFile(graph, "/home/milan/programming/mdd.dot");
GraphvizWriter.getInstance().writeFile(graph, "build\\mdd.dot");
} catch (FileNotFoundException e) {
e.printStackTrace();
}
Expand All @@ -281,7 +289,8 @@ public void exprNodeTest6(){
// x >= 0 && x <= 2 && y >= x && y <= x + 2 && z >= y && z <= y + 2
Expr<BoolType> expr = And(And(Geq(declX.getRef(),Int(0)), Leq(declX.getRef(),Int(2))), And(Geq(declY.getRef(), declX.getRef()), Leq(declY.getRef(), Add(declX.getRef(), Int(2)))), And(Geq(declZ.getRef(), declY.getRef()), Leq(declZ.getRef(), Add(declY.getRef(), Int(2)))));

MddNode rootNode = x.checkInNode(MddExpressionTemplate.of(expr, o -> (Decl) o, Z3SolverFactory.getInstance()::createSolver));
SolverPool solverPool = new SolverPool(Z3SolverFactory.getInstance());
MddNode rootNode = x.checkInNode(MddExpressionTemplate.of(expr, o -> (Decl) o, solverPool));

var interpreter = x.getNodeInterpreter(rootNode);

Expand All @@ -305,11 +314,11 @@ public void exprNodeTest6(){

final Set<Valuation> valuations = MddValuationCollector.collect(rootNode);

assertEquals(valuations.size(), 5);
assertEquals(27, valuations.size());

final Graph graph = new MddNodeVisualizer(MddExpressionTest::nodeToString).visualize(rootNode);
try {
GraphvizWriter.getInstance().writeFile(graph, "/home/milan/programming/mdd.dot");
GraphvizWriter.getInstance().writeFile(graph, "build\\mddasd.dot");
} catch (FileNotFoundException e) {
e.printStackTrace();
}
Expand Down

0 comments on commit e70661a

Please sign in to comment.