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

Implement the NotEquals operator. 

Somehow the NotEquals operator fell through the cracks when implementing
all the other operators.  Add it in, along with the necessary tests so it
will round trip the system properly.

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

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

+4 −1
Original line number Diff line number Diff line
@@ -23,6 +23,7 @@ public enum BinaryOperation { 
    LessThen,

    LessThenEqual,

    Equals,

    NotEquals,



    BooleanAnd,

    BooleanOr;
@@ -30,7 +31,7 @@ public enum BinaryOperation { 
    Collection<VariableTypeMarker> getInputTypeForOutput(VariableTypeMarker outputType) {

        // Boolean inputs only work with a boolean input!

        if (this == BooleanAnd || this == BooleanOr || this == GreaterThen || this == GreaterThenEqual ||

                this == LessThen || this == LessThenEqual || this == Equals) {

                this == LessThen || this == LessThenEqual || this == Equals || this == NotEquals) {

            if (!outputType.equals(new BooleanVariableType())) {

                throw new IllegalArgumentException("Boolean operators and comparisons require a boolean output type!");

            }
@@ -43,6 +44,7 @@ public enum BinaryOperation { 
            case LessThen:

            case LessThenEqual:

            case Equals:

            case NotEquals:

                return Arrays.asList(new VariableTypeMarker[]{new RealVariableType(), new FixedPointVariableType.Marker()});

        }

        return Arrays.asList(new VariableTypeMarker[]{outputType});
@@ -63,6 +65,7 @@ public enum BinaryOperation { 
            case LessThen:

            case LessThenEqual:

            case Equals:

            case NotEquals:

                return new BooleanVariableType();

        }

        return inputType;

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

+3 −1
Original line number Diff line number Diff line
@@ -81,6 +81,8 @@ final public class CVC3Generator implements CheckerGenerator{ 
                return "<=";

            case Equals:

                return "=";

            case NotEquals:

                return "/=";

            case BooleanAnd:

                return "AND";

            case BooleanOr:
@@ -110,7 +112,7 @@ final public class CVC3Generator implements CheckerGenerator{ 
    }



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

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

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

            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 Equals:

                return "=";

            case NotEquals:

                return "distinct";

            case BooleanAnd:

                return "and";

            case BooleanOr:

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

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

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

                return BinaryOperation.Equals;

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

                return BinaryOperation.NotEquals;

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

                return BinaryOperation.BooleanAnd;

            } 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
@@ -154,6 +154,8 @@ final public class PVSSimpleParser { 
                return BinaryOperation.LessThenEqual;

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

                return BinaryOperation.Equals;

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

                return BinaryOperation.NotEquals;

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

                return BinaryOperation.BooleanAnd;

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