Commit 3fc515ae authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Add the exponent operator. 

Add parsing and generating support for the exponent operator.  It currently
doesn't support generation over fixed point values, since CVC3 doesn't include
an easy to use function.

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

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/BinaryOperation.java

+1 −0
Original line number Diff line number Diff line
@@ -17,6 +17,7 @@ public enum BinaryOperation { 
    Minus,

    Multiplication,

    Division,

    Exponentiation,



    GreaterThen,

    GreaterThenEqual,

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/CVC3Generator.java

+5 −0
Original line number Diff line number Diff line
@@ -71,6 +71,8 @@ final public class CVC3Generator implements CheckerGenerator{ 
                return "*";

            case Division:

                return "/";

            case Exponentiation:

                return "^";

            case GreaterThen:

                return ">";

            case GreaterThenEqual:
@@ -115,6 +117,9 @@ final public class CVC3Generator implements CheckerGenerator{ 


    private static OperationType OpTypeForVariableType(BinaryOperation op, VariableType type) {

        if (type instanceof FixedPointVariableType && op != BinaryOperation.Equals && op != BinaryOperation.NotEquals) {

            if (op == BinaryOperation.Exponentiation) {

                throw new IllegalArgumentException("Cannot generate exponential functions in fixed point!");

            }

            return OperationType.Function;

        } else {

            return OperationType.CenterOp;

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/SMTLIBGenerator.java

+2 −0
Original line number Diff line number Diff line
@@ -89,6 +89,8 @@ public class SMTLIBGenerator implements CheckerGenerator { 
                return "*";

            case Division:

                return "/";

            case Exponentiation:

                return "^";

            case GreaterThen:

                return ">";

            case GreaterThenEqual:

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/MatlabParser.java

+2 −0
Original line number Diff line number Diff line
@@ -144,6 +144,8 @@ final public class MatlabParser { 
                return BinaryOperation.Multiplication;

            } else if (text.equals("/")) {

                return BinaryOperation.Division;

            } else if (text.equals("^")) {

                return BinaryOperation.Exponentiation;

            } else if (text.equals(">")) {

                return BinaryOperation.GreaterThen;

            } else if (text.equals(">=")) {

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/PVSSimpleParser.java

+2 −0
Original line number Diff line number Diff line
@@ -146,6 +146,8 @@ final public class PVSSimpleParser { 
                return BinaryOperation.Multiplication;

            } else if (text.equals("/")) {

                return BinaryOperation.Division;

            } else if (text.equals("^")) {

                return BinaryOperation.Exponentiation;

            } else if (text.equals(">")) {

                return BinaryOperation.GreaterThen;

            } else if (text.equals(">=")) {