Implement Real operators for CVC3 generation.

Real operators are now added for CVC3 generation.  Fixed point is still left
out.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10707 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

Matlab2SMT/src/main/java/ca/mcmaster/cas/matlab2smt/CVC3Generator.java

@@ -46,14 +46,26 @@ final public class CVC3Generator implements CheckerGenerator{
         switch (op) {
             case Addition:
                 return "+";
+            case Minus:
+                return "-";
             case Multiplication:
                 return "*";
+            case Division:
+                return "/";
             case GreaterThen:
                 return ">";
+            case GreaterThenEqual:
+                return ">=";
+            case LessThen:
+                return "<";
+            case LessThenEqual:
+                return "<=";
             case Equals:
                 return "=";
             case BooleanAnd:
                 return "AND";
+            case BooleanOr:
+                return "OR";
         }
         throw new RuntimeException("Should never happen!");
     }
@@ -98,12 +110,19 @@ final public class CVC3Generator implements CheckerGenerator{
         }
     }
 
+    private static String GetUnaryOperationSymbolFor(MatlabUnaryOperation op) {
+        switch (op) {
+            case Negation:
+                return "NOT";
+            case Minus:
+                return "-";
+        }
+        throw new RuntimeException("Should never happen!  Asked for unhandled op: " + op + "!");
+    }
+
     @Override
     public String GenerateUnaryOperation(MatlabUnaryOperation op, String expression, VariableType usedType) {
-        if (op != MatlabUnaryOperation.Negation) {
-            throw new RuntimeException("Stubbed function just became inadequate!");
-        }
-        return "(NOT " + expression + ")";
+        return "(" + GetUnaryOperationSymbolFor(op) + " " + expression + ")";
     }
 
     public String GenerateVariableType(VariableType type) {

Matlab2SMT/src/test/java/ca/mcmaster/cas/matlab2smt/GenericGeneratorTest.java

@@ -35,7 +35,8 @@ public class GenericGeneratorTest {
     @Parameters
     public static Collection<Object[]> data() {
         return Arrays.asList(new Object[][]{
-                {new SMTLIBGenerator(), "(or (or (or (= (* x 5.0) (/ 1.0 (- 4.0))) (and (> 4.0 (+ 8.0 3.0)) (< 9.0 (- 1.0 2.0)))) (>= 11.0 12.0)) (not (<= 34.0 (- 54.0))))"}
+                {new SMTLIBGenerator(), "(or (or (or (= (* x 5.0) (/ 1.0 (- 4.0))) (and (> 4.0 (+ 8.0 3.0)) (< 9.0 (- 1.0 2.0)))) (>= 11.0 12.0)) (not (<= 34.0 (- 54.0))))"},
+                {new CVC3Generator(), "(((((x * 5) = (1 / (- 4))) OR ((4 > (8 + 3)) AND (9 < (1 - 2)))) OR (11 >= 12)) OR (NOT (34 <= (- 54))))"}
         });
     }
 
@@ -52,7 +53,6 @@ public class GenericGeneratorTest {
     public void doTest() {
         VariableParser vars = new VariableParser("x");
         MatlabParser parser = new MatlabParser(vars, query);
-System.out.println(parser.getRootExpression().toString());
         assertEquals(RealExpectedOutput, parser.getRootExpression().getCheckerOutput(generator, outputType));
     }
 }