diff --git a/src/main/java/ca/mcscert/jtet/cvc3generator/CVC3VariablesDeclarationGenerator.java b/src/main/java/ca/mcscert/jtet/cvc3generator/CVC3VariablesDeclarationGenerator.java index e499574c28dabd392df49620c8f8c1746cce1b83..26d0d4b8c4cb86f4fbdda7171eb9385191b0e24e 100644 --- a/src/main/java/ca/mcscert/jtet/cvc3generator/CVC3VariablesDeclarationGenerator.java +++ b/src/main/java/ca/mcscert/jtet/cvc3generator/CVC3VariablesDeclarationGenerator.java @@ -55,9 +55,9 @@ final public class CVC3VariablesDeclarationGenerator implements VariablesDeclara // Then generate the variable predicates. This ensures any dependent variables are declared. for(Variable var : variables) { - if (var.type().subtypePredicate() != null) { + if (var.subtypePredicate() != null) { ret.append("ASSERT ") - .append(var.type().subtypePredicate().getCheckerOutput(CVC3ExpressionGenerator.Generator, BooleanType.Type)) + .append(var.subtypePredicate().getCheckerOutput(CVC3ExpressionGenerator.Generator, BooleanType.Type)) .append(";\n"); } } diff --git a/src/main/java/ca/mcscert/jtet/expression/Type.java b/src/main/java/ca/mcscert/jtet/expression/Type.java index 86f19063da2368d31b43907d79882eb166bdfcd1..8377ea97de0e7fc2e2034a07672afa8dd7910b28 100644 --- a/src/main/java/ca/mcscert/jtet/expression/Type.java +++ b/src/main/java/ca/mcscert/jtet/expression/Type.java @@ -25,14 +25,4 @@ public abstract class Type implements TypeMarker { public boolean isMarkerFor(Type m_type) { return this.equals(m_type); } - - public Expression subtypePredicate() { - return m_subtypePredicate; - } - - public void setSubtypePredicate(Expression subtypePredicate) { - m_subtypePredicate = subtypePredicate; - } - - private Expression m_subtypePredicate; } diff --git a/src/main/java/ca/mcscert/jtet/expression/Variable.java b/src/main/java/ca/mcscert/jtet/expression/Variable.java index 722ec45e821d004d42745b8fb38e78835b1379b2..5ae93542e22db8dc910a586f52640f6f846b7ab3 100644 --- a/src/main/java/ca/mcscert/jtet/expression/Variable.java +++ b/src/main/java/ca/mcscert/jtet/expression/Variable.java @@ -80,8 +80,25 @@ public class Variable implements Expression, ExpressionValue { return null; } + /** + * Returns the expression representing the subtype predicate for this variable. + * @return Expression representing the predicate. + */ + public Expression subtypePredicate() { + return m_subtypePredicate; + } + + /** + * Sets the expression to represent the subtype predicate for this variable. + * @param subtypePredicate The expression to use as the subtype predicate. + */ + public void setSubtypePredicate(Expression subtypePredicate) { + m_subtypePredicate = subtypePredicate; + } + final private String m_name; private String m_outputName; + private Expression m_subtypePredicate; final private Type m_type; /** diff --git a/src/main/java/ca/mcscert/jtet/parsers/VariableParser.java b/src/main/java/ca/mcscert/jtet/parsers/VariableParser.java index 869292d9112cf9291dde1dd407e26597406bc519..ea0c63ebfd0109704638101993418efbb59e4d8c 100644 --- a/src/main/java/ca/mcscert/jtet/parsers/VariableParser.java +++ b/src/main/java/ca/mcscert/jtet/parsers/VariableParser.java @@ -172,7 +172,7 @@ final public class VariableParser { m_variables.put(subtypeVar, m_variables.get(limitingExpression.getKey())); VariableCollection variableCollection = new VariableCollection(new PartialVariableCollection(m_variables, m_usedEnumerationTypes)); - m_variables.get(limitingExpression.getKey()).type().setSubtypePredicate(PVSSimpleParser.parsePVSCode(variableCollection, subtypeExpression)); + m_variables.get(limitingExpression.getKey()).setSubtypePredicate(PVSSimpleParser.parsePVSCode(variableCollection, subtypeExpression)); // Undo the variables hack, to avoid having unused variables bleed into the verification scripts! m_variables.remove(subtypeVar); diff --git a/src/main/java/ca/mcscert/jtet/salgenerator/SALVariablesDeclarationGenerator.java b/src/main/java/ca/mcscert/jtet/salgenerator/SALVariablesDeclarationGenerator.java index 9676a0a544e554a5351e3f656df4d2a88f1f5b5c..103408e0471abee518f1e06d56d9071c8af7bd01 100644 --- a/src/main/java/ca/mcscert/jtet/salgenerator/SALVariablesDeclarationGenerator.java +++ b/src/main/java/ca/mcscert/jtet/salgenerator/SALVariablesDeclarationGenerator.java @@ -45,16 +45,15 @@ public class SALVariablesDeclarationGenerator implements VariablesDeclarationGen // Generate all the variables. for(Variable var : variables) { ret.append(var.outputName()).append(":"); - Type type = var.type(); - if (type.subtypePredicate() == null) { - ret.append(GenerateType(type)); + if (var.subtypePredicate() == null) { + ret.append(GenerateType(var.type())); } else { ret.append("{") .append(var.outputName()) .append(":") - .append(GenerateType(type)) + .append(GenerateType(var.type())) .append("|") - .append(type.subtypePredicate().getCheckerOutput(SALExpressionGenerator.Generator, BooleanType.Type)) + .append(var.subtypePredicate().getCheckerOutput(SALExpressionGenerator.Generator, BooleanType.Type)) .append("}"); } ret.append("\n"); diff --git a/src/main/java/ca/mcscert/jtet/smtlibchecker/SMTLIBVariablesDeclarationGenerator.java b/src/main/java/ca/mcscert/jtet/smtlibchecker/SMTLIBVariablesDeclarationGenerator.java index 70e586ed70631a4e0ec99e5aeebee056100599eb..72f00ba1e7bfe922d65a6216534c911c0111aab4 100644 --- a/src/main/java/ca/mcscert/jtet/smtlibchecker/SMTLIBVariablesDeclarationGenerator.java +++ b/src/main/java/ca/mcscert/jtet/smtlibchecker/SMTLIBVariablesDeclarationGenerator.java @@ -63,9 +63,9 @@ public class SMTLIBVariablesDeclarationGenerator implements VariablesDeclaration // Then generate the variable predicates. This ensures any dependent variables are declared. for(Variable var : variables) { - if (var.type().subtypePredicate() != null) { + if (var.subtypePredicate() != null) { ret.append("(assert ") - .append(var.type().subtypePredicate().getCheckerOutput(SMTLIBExpressionGenerator.Generator, BooleanType.Type)) + .append(var.subtypePredicate().getCheckerOutput(SMTLIBExpressionGenerator.Generator, BooleanType.Type)) .append(")\n"); } } diff --git a/src/test/java/ca/mcscert/jtet/expression/VariableTest.java b/src/test/java/ca/mcscert/jtet/expression/VariableTest.java index 0d324d0b5dff95680b5f4610abd6e94447d65771..86b02b880debbf19ca20e02144a86e0fd3398299 100644 --- a/src/test/java/ca/mcscert/jtet/expression/VariableTest.java +++ b/src/test/java/ca/mcscert/jtet/expression/VariableTest.java @@ -41,10 +41,10 @@ public class VariableTest { // Next create a subtype predicate. For now, make it work over positive reals (excluding 0) Expression predicate = new ExpressionBinaryOperation(var, BinaryOperation.GreaterThen, new Literal("0")); - var.type().setSubtypePredicate(predicate); + var.setSubtypePredicate(predicate); // Verify the predicate took. - assertThat(var.type().subtypePredicate(), is(predicate)); + assertThat(var.subtypePredicate(), is(predicate)); } @Test diff --git a/src/test/java/ca/mcscert/jtet/parsers/test/VariableParserTest.java b/src/test/java/ca/mcscert/jtet/parsers/test/VariableParserTest.java index d5650ab6c34285634a96f432eeeed94d51a3069e..fb6f4a87ba993139848c538d8deb05e0feb06e6b 100644 --- a/src/test/java/ca/mcscert/jtet/parsers/test/VariableParserTest.java +++ b/src/test/java/ca/mcscert/jtet/parsers/test/VariableParserTest.java @@ -125,23 +125,23 @@ public class VariableParserTest { assertThat(vars.get("d").name(), is("d")); assertThat(vars.get("d").type(), is((Type) RealType.Type)); - assertThat(vars.get("d").type().subtypePredicate().toString(), is("(c BooleanOr (d GreaterThen 5))")); + assertThat(vars.get("d").subtypePredicate().toString(), is("(c BooleanOr (d GreaterThen 5))")); assertThat(vars.get("a").name(), is("a")); assertThat(vars.get("a").type(), is((Type) RealType.Type)); - assertThat(vars.get("a").type().subtypePredicate(), is((Object)null)); + assertThat(vars.get("a").subtypePredicate(), is((Object)null)); assertThat(vars.get("b").name(), is("b")); assertThat(vars.get("b").type(), is((Type) RealType.Type)); - assertThat(vars.get("b").type().subtypePredicate().toString(), is("(b GreaterThen 5)")); + assertThat(vars.get("b").subtypePredicate().toString(), is("(b GreaterThen 5)")); assertThat(vars.get("c").name(), is("c")); assertThat(vars.get("c").type(), is((Type) BooleanType.Type)); - assertThat(vars.get("c").type().subtypePredicate(), is((Object)null)); + assertThat(vars.get("c").subtypePredicate(), is((Object)null)); assertThat(vars.get("z").name(), is("z")); assertThat(vars.get("z").type(), is((Type) BooleanType.Type)); - assertThat(vars.get("z").type().subtypePredicate().toString(), is("(z NotEquals c)")); + assertThat(vars.get("z").subtypePredicate().toString(), is("(z NotEquals c)")); } @Test @@ -149,7 +149,6 @@ public class VariableParserTest { VariableParser variableParser = new VariableParser(); variableParser.addCustomType("myreal", new RealType()); BooleanType customBool = new BooleanType(); - customBool.setSubtypePredicate(new Variable("c", new BooleanType())); variableParser.addCustomType("mybool", customBool); Map vars = variableParser.parseVariables("a:myreal,b:mybool").m_variables; @@ -160,7 +159,7 @@ public class VariableParserTest { assertThat(vars.get("b").name(), is("b")); assertThat(vars.get("b").type(), is((Type) BooleanType.Type)); - assertThat(vars.get("b").type().subtypePredicate().toString(), is("c")); + assertThat(vars.get("b").type(), sameInstance((Type) customBool)); } @Test