2 files changed, 101 insertions, 20 deletions

diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
index 1b68fed2..9e11d2cf 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
@@ -1,6 +1,7 @@
 package hu.bme.mit.inf.dslreasoner.viatra2logic

 

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IfThenElse

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable

 import java.util.Map

@@ -8,9 +9,11 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
 import org.eclipse.xtext.xbase.XBinaryOperation

 import org.eclipse.xtext.xbase.XExpression

 import org.eclipse.xtext.xbase.XFeatureCall

+import org.eclipse.xtext.xbase.XIfExpression

 import org.eclipse.xtext.xbase.XMemberFeatureCall

 import org.eclipse.xtext.xbase.XNumberLiteral

 import org.eclipse.xtext.xbase.XUnaryOperation

+import org.eclipse.xtext.xbase.XBlockExpression

 

 class ExpressionEvaluation2Logic {

         val extension LogicProblemBuilder builder = new LogicProblemBuilder

@@ -139,6 +142,41 @@ class ExpressionEvaluation2Logic {
                 throw new UnsupportedOperationException('''Unsupported numeric type: "«s»"''')

         }

         

+        def protected dispatch Term transform(XIfExpression i, Map<PVariable, Variable> variable2Variable) {

+                

+                val cond_op = i.^if.transform(variable2Variable)

+                val then_op = i.then.transform(variable2Variable)

+                val else_op = i.^else.transform(variable2Variable)

+                

+                if (cond_op === null) {

+                        println("-> " + i.^if)

+                        println("-> " + i.then)

+                        println("-> " + i.^else)

+                        throw new UnsupportedOperationException('''Your ITE statement has a null condition.''')

+                }

+                if (then_op === null) {

+                        println("-> " + i.^if)

+                        println("-> " + i.then)

+                        println("-> " + i.^else)

+                        throw new UnsupportedOperationException('''Your ITE statement has a null "then" statement"".''')

+                }

+                return ITE(cond_op, then_op, else_op)

+        }

+        

+                def protected dispatch Term transform(XBlockExpression b, Map<PVariable, Variable> variable2Variable) {

+                val exprs = newArrayList

+                for(e:b.expressions){ exprs.add(transform(e, variable2Variable)) }

+                

+                if (exprs.size > 1)

+                        throw new UnsupportedOperationException('''blocks with more than 1 statement are not currently supportes: "«exprs»"''')

+                if (exprs.isEmpty)

+                        throw new UnsupportedOperationException('''blocks is empty: "«exprs»"''')

+

+                return exprs.get(0)

+        }

+        

+        

+        

         def protected dispatch Term transform(XExpression e, Map<PVariable, Variable> variable2Variable) {

                 throw new UnsupportedOperationException('''Unsupported expression: "«e.class.simpleName»" - «e»''')

         }

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 30e68260..575a9224 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
@@ -20,8 +20,10 @@ import java.util.regex.Pattern;
 

 import org.eclipse.xtext.common.types.JvmIdentifiableElement;

 import org.eclipse.xtext.xbase.XBinaryOperation;

+import org.eclipse.xtext.xbase.XBlockExpression;

 import org.eclipse.xtext.xbase.XExpression;

 import org.eclipse.xtext.xbase.XFeatureCall;

+import org.eclipse.xtext.xbase.XIfExpression;

 import org.eclipse.xtext.xbase.XNumberLiteral;

 import org.eclipse.xtext.xbase.XUnaryOperation;

 

@@ -72,7 +74,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
                 //TODO timeout if needed

                 if (!p.waitFor(timeout, TimeUnit.SECONDS)) {

                         p.destroy();

-                        System.err.println("TIMEOUT"); //DEBUG

+                        return null;

                 }

                 return p;

         }

@@ -147,7 +149,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
         }       

         

         private String formNumericConstraint(XExpression e, Map<JvmIdentifiableElement, PrimitiveElement> aMatch) throws Exception {

-                //The check equation MUST be a binary operation

+                //The check equation MUST be a binary operation of the listed types (comparisons)

                 if (!(e instanceof XBinaryOperation)) {

                         throw new Exception ("error in check expression!!!");

                 }

@@ -159,19 +161,20 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
                 String left_operand = formNumericConstraintHelper(((XBinaryOperation) e).getLeftOperand(), aMatch);

                 String right_operand = formNumericConstraintHelper(((XBinaryOperation) e).getRightOperand(), aMatch);

 

+                //NOTE that everything  is inverted, due to how the MG handles vql constraints

                 if (nameEndsWith(name, N_LESSTHAN)) {

-                        operator = "<";

+                        operator = ">";

                 } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) {

-                        operator = "<=";

+                        operator = ">=";

                 } else if (nameEndsWith(name, N_GREATERTHAN)) {

-                        operator = ">";

+                        operator = "<";

                 } else if (nameEndsWith(name, N_GREATEREQUALTHAN)) {

-                        operator = ">=";

+                        operator = "<=";

                 } else if (nameEndsWith(name, N_EQUALS)) {

-                        operator = "<";

-                } else if (nameEndsWith(name, N_NOTEQUALS)) {

                         //Exceptional case

                         return "(not (="  + " " + left_operand + " " + right_operand + "))";

+                } else if (nameEndsWith(name, N_NOTEQUALS)) {

+                        operator = "=";

 //              } else if (nameEndsWith(name, N_EQUALS3)) {

 //                      operator = "<";

 //              } else if (nameEndsWith(name, N_NOTEQUALS3)) {

@@ -240,6 +243,19 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
                                 operator = "*";

                         } else if (nameEndsWith(name, N_DIVIDE)) {

                                 operator = "/";

+                        } else if (nameEndsWith(name, N_LESSTHAN)) {

+                                operator = "<";

+                        } else if (nameEndsWith(name, N_LESSEQUALSTHAN)) {

+                                operator = "<=";

+                        } else if (nameEndsWith(name, N_GREATERTHAN)) {

+                                operator = ">";

+                        } else if (nameEndsWith(name, N_GREATEREQUALTHAN)) {

+                                operator = ">=";

+                        } else if (nameEndsWith(name, N_EQUALS)) {

+                                operator = "<";

+                        } else if (nameEndsWith(name, N_NOTEQUALS)) {

+                                //Exceptional case

+                                return "(not (="  + " " + left_operand + " " + right_operand + "))";

 //                      } else if (nameEndsWith(name, N_MODULO)) {

 //                              expr = ctx.mkMod((IntExpr)left_operand, (IntExpr)right_operand);

                         } else {

@@ -249,12 +265,30 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
                         expr = "(" + operator + " " + left_operand + " " + right_operand + ")";                 

                 } 

                 else if (e instanceof XUnaryOperation){

-                        String name = ((XUnaryOperation) e).getFeature().getQualifiedName();

-                        System.out.println(name);

-                        String op = ((XUnaryOperation) e).getOperand().toString();                      

-                        System.out.println(op);

+                        //TODO

+                        //This is, for example, "-1000"

                         throw new Exception ("Unsupported expression " + e.getClass().getSimpleName());

-                } else {

+                }

+                else if (e instanceof XIfExpression) {

+                        

+                        String if_operand = formNumericConstraintHelper(((XIfExpression) e).getIf(), aMatch);

+                        String then_operand = formNumericConstraintHelper(((XIfExpression) e).getThen(), aMatch);

+                        String else_operand = formNumericConstraintHelper(((XIfExpression) e).getElse(), aMatch);

+                        

+                        expr = "(ite " + if_operand + " " + then_operand + " " + else_operand + ")";

+                }

+                else if (e instanceof XBlockExpression) {

+                        XBlockExpression ebl = (XBlockExpression) e;

+                        

+                        if (ebl.getExpressions().size() > 1)

+                                throw new Exception("Unsupported: blocks with more than 1 statement are not currently supportes: " + ebl);

+                        if (ebl.getExpressions().isEmpty())

+                                throw new Exception("Unsupported: blocks is empty:" + ebl);

+                        

+                        //TODO make this more general

+                        expr = formNumericConstraintHelper(ebl.getExpressions().get(0), aMatch);

+                }

+                else {

                         throw new Exception ("Unsupported expression " + e.getClass().getSimpleName());

                 }

                 return expr;

@@ -279,7 +313,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
                         Iterable<Map<JvmIdentifiableElement, PrimitiveElement>> matchSets = matches.get(e);

                         for (Map<JvmIdentifiableElement, PrimitiveElement> aMatch: matchSets) {

                                 String constraint = formNumericConstraint(e, aMatch);

-                                String negAssert = "(assert (not " + constraint +  "))";

+                                String negAssert = "(assert " + constraint +  ")";

                                 curConstraints.add(negAssert);

                         }

                 }

@@ -329,16 +363,24 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
                 Process outputProcess;

                 if (this.useDocker) outputProcess = callDrealDocker(numProbContent, false);

                 else outputProcess = callDrealLocal(numProbContent, false);

-                        

-                List<List<String>> outputs = getProcessOutput(outputProcess);

-                boolean result = getDrealResult(outputProcess.exitValue(), outputs);

+                

+                boolean result = false;

+                List<List<String>> outputs = null;

+                if (outputProcess != null) { 
+                        outputs = getProcessOutput(outputProcess);
+                        result = getDrealResult(outputProcess.exitValue(), outputs);

+                }

                 endSolvingProblem = System.nanoTime()-startSolvingProblem;

                 

                 //DEBUG - Print things

+                if (outputProcess == null) {

+                        System.err.println("TIMEOUT");

+//                      printOutput(numProbContent);

+                }

 //              printOutput(numProbContent);

-//              printOutput(outputs.get(0));

-                System.out.println(result);

-                //END DEBUG

+//              if (outputs != null) printOutput(outputs.get(0));

+//              System.out.println(result);

+//              END DEBUG

                 

                 return result;

         }

@@ -391,6 +433,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
                 endSolvingProblem = System.nanoTime()-startSolvingProblem;

                 

                 //DEBUG - Print things

+                System.out.println("Getting Solution!");

 //              printOutput(numProbContent);

 //              printOutput(outputs.get(0));

 //              System.out.println(result);