From 698d3001da2f49c3ebeb3ba358c75e191e063a79 Mon Sep 17 00:00:00 2001 From: Matthew Dawson Date: Fri, 31 Oct 2014 00:12:13 -0400 Subject: [PATCH] Finally, move the subtype predicate storage to the Variable. Since the predicate subtype can be set per variable, move that logic to the Variable class, away from the Type class. Before, Type disagreed on whether two instances could be equal, and whether they could be easily duplicated. This makes the distinction unimportant. It does neuter the custom type functionality in VariableParser some, but that can be added back later. --- .../CVC3VariablesDeclarationGenerator.java | 4 ++-- .../java/ca/mcscert/jtet/expression/Type.java | 10 ---------- .../ca/mcscert/jtet/expression/Variable.java | 17 +++++++++++++++++ .../ca/mcscert/jtet/parsers/VariableParser.java | 2 +- .../SALVariablesDeclarationGenerator.java | 9 ++++----- .../SMTLIBVariablesDeclarationGenerator.java | 4 ++-- .../mcscert/jtet/expression/VariableTest.java | 4 ++-- .../jtet/parsers/test/VariableParserTest.java | 13 ++++++------- 8 files changed, 34 insertions(+), 29 deletions(-) diff --git a/src/main/java/ca/mcscert/jtet/cvc3generator/CVC3VariablesDeclarationGenerator.java b/src/main/java/ca/mcscert/jtet/cvc3generator/CVC3VariablesDeclarationGenerator.java index e499574..26d0d4b 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 86f1906..8377ea9 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 722ec45..5ae9354 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 869292d..ea0c63e 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 9676a0a..103408e 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 70e586e..72f00ba 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 0d324d0..86b02b8 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 d5650ab..fb6f4a8 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 -- GitLab