From aaa67b0ef8840d97b062a4f1383bf93410984af3 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Fri, 30 Jul 2021 10:04:27 +0200 Subject: Numeric solver dreal hardcoding -> config --- .../viatra2logic/FakeIntegerElement.java | 169 --------------------- .../viatra2logic/NumericDrealProblemSolver.java | 28 +++- .../viatra2logic/NumericDynamicProblemSolver.java | 43 ------ .../NumericDynamicProblemSolverXXX.java | 63 ++++++++ .../viatra2logic/NumericProblemSolver.java | 22 ++- .../viatra2logic/NumericTranslator.xtend | 21 +-- .../viatra2logic/NumericZ3ProblemSolver.java | 60 ++++++-- 7 files changed, 157 insertions(+), 249 deletions(-) delete mode 100644 Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/FakeIntegerElement.java delete mode 100644 Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java create mode 100644 Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolverXXX.java (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic') diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/FakeIntegerElement.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/FakeIntegerElement.java deleted file mode 100644 index 7b8634c4..00000000 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/FakeIntegerElement.java +++ /dev/null @@ -1,169 +0,0 @@ -package hu.bme.mit.inf.dslreasoner.viatra2logic; - -import java.lang.reflect.InvocationTargetException; - -import org.eclipse.emf.common.notify.Adapter; -import org.eclipse.emf.common.notify.Notification; -import org.eclipse.emf.common.util.EList; -import org.eclipse.emf.common.util.TreeIterator; -import org.eclipse.emf.ecore.EClass; -import org.eclipse.emf.ecore.EObject; -import org.eclipse.emf.ecore.EOperation; -import org.eclipse.emf.ecore.EReference; -import org.eclipse.emf.ecore.EStructuralFeature; -import org.eclipse.emf.ecore.resource.Resource; - -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; - -public class FakeIntegerElement implements PrimitiveElement{ - - public FakeIntegerElement() { - - } - - @Override - public EList getDefinedInType() { - // TODO Auto-generated method stub - return null; - } - - @Override - public String getName() { - // TODO Auto-generated method stub - return null; - } - - @Override - public void setName(String value) { - // TODO Auto-generated method stub - - } - - @Override - public EClass eClass() { - // TODO Auto-generated method stub - return null; - } - - @Override - public Resource eResource() { - // TODO Auto-generated method stub - return null; - } - - @Override - public EObject eContainer() { - // TODO Auto-generated method stub - return null; - } - - @Override - public EStructuralFeature eContainingFeature() { - // TODO Auto-generated method stub - return null; - } - - @Override - public EReference eContainmentFeature() { - // TODO Auto-generated method stub - return null; - } - - @Override - public EList eContents() { - // TODO Auto-generated method stub - return null; - } - - @Override - public TreeIterator eAllContents() { - // TODO Auto-generated method stub - return null; - } - - @Override - public boolean eIsProxy() { - // TODO Auto-generated method stub - return false; - } - - @Override - public EList eCrossReferences() { - // TODO Auto-generated method stub - return null; - } - - @Override - public Object eGet(EStructuralFeature feature) { - // TODO Auto-generated method stub - return null; - } - - @Override - public Object eGet(EStructuralFeature feature, boolean resolve) { - // TODO Auto-generated method stub - return null; - } - - @Override - public void eSet(EStructuralFeature feature, Object newValue) { - // TODO Auto-generated method stub - - } - - @Override - public boolean eIsSet(EStructuralFeature feature) { - // TODO Auto-generated method stub - return false; - } - - @Override - public void eUnset(EStructuralFeature feature) { - // TODO Auto-generated method stub - - } - - @Override - public Object eInvoke(EOperation operation, EList arguments) throws InvocationTargetException { - // TODO Auto-generated method stub - return null; - } - - @Override - public EList eAdapters() { - // TODO Auto-generated method stub - return null; - } - - @Override - public boolean eDeliver() { - // TODO Auto-generated method stub - return false; - } - - @Override - public void eSetDeliver(boolean deliver) { - // TODO Auto-generated method stub - - } - - @Override - public void eNotify(Notification notification) { - // TODO Auto-generated method stub - - } - - @Override - public boolean isValueSet() { - // TODO Auto-generated method stub - return false; - } - - @Override - public void setValueSet(boolean value) { - // TODO Auto-generated method stub - - } - -} diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java index cecd3623..f30e390b 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java @@ -365,8 +365,8 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ Iterable> matchSets = matches.get(e); for (Map aMatch: matchSets) { String constraint = formNumericConstraint(e, aMatch); - if (constraint != null) { - String negAssert = "(assert " + constraint + ")"; + if (constraint != null) { + String negAssert = "(assert " + constraint + ")"; curConstraints.add(negAssert); } } @@ -426,8 +426,8 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ boolean result = false; List> outputs = null; - if (outputProcess != null) { - outputs = getProcessOutput(outputProcess); + if (outputProcess != null) { + outputs = getProcessOutput(outputProcess); result = getDrealResult(outputProcess.exitValue(), outputs); // } else { // System.err.print("Timeout, RETRYING..."); @@ -575,4 +575,24 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ //TODO Check if above went well? } + @Override + protected void initialize() { + // TODO Auto-generated method stub + + } + + @Override + protected boolean internalIsSatisfiable( + Map>> matches) throws Exception { + // TODO Auto-generated method stub + return false; + } + + @Override + protected Map internalGetOneSolution(List objs, + Map>> matches) throws Exception { + // TODO Auto-generated method stub + return null; + } + } diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java deleted file mode 100644 index e8c20138..00000000 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java +++ /dev/null @@ -1,43 +0,0 @@ -package hu.bme.mit.inf.dslreasoner.viatra2logic; - -import java.io.IOException; -import java.util.List; -import java.util.Map; - -import org.eclipse.xtext.common.types.JvmIdentifiableElement; -import org.eclipse.xtext.xbase.XExpression; - -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; - -public class NumericDynamicProblemSolver extends NumericProblemSolver{ - -// private NumericZ3ProblemSolver z3Solver; - private NumericDrealProblemSolver drealSolver; - private int timeout; - - public NumericDynamicProblemSolver(String drealLocalPath, int drealTimeout) throws IOException, InterruptedException { -// this.z3Solver = new NumericZ3ProblemSolver(); - this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath, drealTimeout); - this.timeout = drealTimeout; - } - - public NumericProblemSolver selectSolver(String selection) { - switch (selection) { - case "z3": - return new NumericZ3ProblemSolver(timeout); - case "dreal": - return this.drealSolver; - default: - throw new IllegalArgumentException("Unknown numeric solver selection: " + selection); - } - } - - public boolean isSatisfiable(Map>> matches) - throws Exception { - throw new Exception("Should not reach here - isSatisfiable"); - } - - public Map getOneSolution(List objs, - Map>> matches) throws Exception { - throw new Exception("Should not reach here - getOneSolution"); - }} diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolverXXX.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolverXXX.java new file mode 100644 index 00000000..199c089b --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolverXXX.java @@ -0,0 +1,63 @@ +package hu.bme.mit.inf.dslreasoner.viatra2logic; + +import java.io.IOException; +import java.util.List; +import java.util.Map; + +import org.eclipse.xtext.common.types.JvmIdentifiableElement; +import org.eclipse.xtext.xbase.XExpression; + +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; + +public class NumericDynamicProblemSolverXXX extends NumericProblemSolver{ + +// private NumericZ3ProblemSolver z3Solver; + private NumericDrealProblemSolver drealSolver; + private int timeout; + + public NumericDynamicProblemSolverXXX(String drealLocalPath, int drealTimeout) throws IOException, InterruptedException { +// this.z3Solver = new NumericZ3ProblemSolver(); + this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath, drealTimeout); + this.timeout = drealTimeout; + } + + public NumericProblemSolver selectSolver(String selection) { + switch (selection) { + case "z3": + return new NumericZ3ProblemSolver(timeout); + case "dreal": + return this.drealSolver; + default: + throw new IllegalArgumentException("Unknown numeric solver selection: " + selection); + } + } + + public boolean isSatisfiable(Map>> matches) + throws Exception { + throw new Exception("Should not reach here - isSatisfiable"); + } + + public Map getOneSolution(List objs, + Map>> matches) throws Exception { + throw new Exception("Should not reach here - getOneSolution"); + } + + @Override + protected void initialize() { + // TODO Auto-generated method stub + + } + + @Override + protected boolean internalIsSatisfiable( + Map>> matches) throws Exception { + // TODO Auto-generated method stub + return false; + } + + @Override + protected Map internalGetOneSolution(List objs, + Map>> matches) throws Exception { + // TODO Auto-generated method stub + return null; + }} diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java index 5e823d9d..8f57e40c 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java @@ -35,6 +35,24 @@ public abstract class NumericProblemSolver { public long getEndSolvingProblem() {return endSolvingProblem;} public long getEndFormingSolution() {return endFormingSolution;} - public abstract boolean isSatisfiable(Map>> matches) throws Exception; - public abstract Map getOneSolution(List objs, Map>> matches) throws Exception; + public boolean isSatisfiable(Map>> matches) throws Exception { + if(!initialized) { + this.initialize(); + this.initialized=true; + } + return this.internalIsSatisfiable(matches); + } + public Map getOneSolution(List objs, Map>> matches) throws Exception{ + if(!initialized) { + this.initialize(); + this.initialized=true; + } + return this.internalGetOneSolution(objs, matches); + } + + boolean initialized = false; + protected abstract void initialize(); + + protected abstract boolean internalIsSatisfiable(Map>> matches) throws Exception; + protected abstract Map internalGetOneSolution(List objs, Map>> matches) throws Exception; } diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend index a11ae8a8..9ae36a6d 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend @@ -58,31 +58,18 @@ class NumericTranslator { return res } - def NumericProblemSolver selectProblemSolver(String selection) { -// return new NumericProblemSolver -// add numeric solver decision procedure here - if (numericSolver instanceof NumericDynamicProblemSolver) { - val NumericDynamicProblemSolver dynamicSolver = numericSolver as NumericDynamicProblemSolver - return dynamicSolver.selectSolver(selection); - } else{ - if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver(this.timeout) - return numericSolver; - } - } def delegateIsSatisfiable(Map> matches, String select) { val input = formNumericProblemInstance(matches) - val solver = selectProblemSolver(select) - val satisfiability = solver.isSatisfiable(input) - solver.updateTimes + val satisfiability = numericSolver.isSatisfiable(input) + numericSolver.updateTimes return satisfiability } def delegateGetSolution(List primitiveElements, Map> matches, String select) { val input = formNumericProblemInstance(matches) - val solver = selectProblemSolver(select) - val solution = solver.getOneSolution(primitiveElements,input) - solver.updateTimes + val solution = numericSolver.getOneSolution(primitiveElements,input) + numericSolver.updateTimes return solution } diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java index 0799953f..5b4f6de1 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java @@ -35,24 +35,18 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ private Context ctx; private Solver s; private Map varMap; + private int timeout; public NumericZ3ProblemSolver(int timeout) { - //FOR LINUX VM - //Not Elegant, but this is working for now -// String root = "/home/models/VIATRA-Generator"; -// String root = (new File(System.getProperty("user.dir"))).getParentFile().getParent(); -// System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.so"); -// System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); - //End non-elegance - + this.timeout=timeout; HashMap cfg = new HashMap(); cfg.put("model", "true"); ctx = new Context(cfg); ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL); s = ctx.mkSolver(); if (timeout != -1) { - Params p = ctx.mkParams(); - p.add("timeout", timeout); + Params p = ctx.mkParams(); + p.add("timeout", timeout); s.setParameters(p); } varMap = new HashMap(); @@ -62,7 +56,7 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ return ctx; } - private ArrayList getJvmIdentifiableElements(XExpression expression) { + private ArrayList getJvmIdentifiableElements(final XExpression expression) { ArrayList allElem = new ArrayList(); XExpression left = ((XBinaryOperation) expression).getLeftOperand(); XExpression right = ((XBinaryOperation) expression).getRightOperand(); @@ -80,8 +74,36 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ getJvmIdentifiableElementsHelper(((XBinaryOperation) e).getRightOperand(), allElem); } } - - public boolean isSatisfiable(Map>> matches) throws Exception { + + @Override + protected void initialize() { + // TODO Auto-generated method stub + + } + + private void start() { + HashMap cfg = new HashMap(); + cfg.put("model", "true"); + ctx = new Context(cfg); + ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL); + s = ctx.mkSolver(); + if (timeout != -1) { + Params p = ctx.mkParams(); + p.add("timeout", timeout); + s.setParameters(p); + } + varMap = new HashMap(); + } + private void stop() { + ctx=null; + s=null; + varMap=null; + } + + @Override + protected boolean internalIsSatisfiable(Map>> matches) throws Exception { + start(); + long startformingProblem = System.nanoTime(); BoolExpr problemInstance = formNumericProblemInstance(matches); s.add(problemInstance); @@ -94,10 +116,15 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ // System.out.println("end"); endSolvingProblem = System.nanoTime()-startSolvingProblem; this.ctx.close(); + + stop(); return result; } - public Map getOneSolution(List objs, Map>> matches) throws Exception { + @Override + protected Map internalGetOneSolution(List objs, Map>> matches) throws Exception { + start(); + Map sol = new HashMap(); long startformingProblem = System.nanoTime(); BoolExpr problemInstance = formNumericProblemInstance(matches); @@ -147,6 +174,9 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ System.out.println("Unsatisfiable numerical problem"); } this.ctx.close(); + + stop(); + return sol; } @@ -271,6 +301,8 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ } + + /* public void testIsSat(XExpression expression, Term t) throws Exception { int count = 10000; -- cgit v1.2.3-54-g00ecf