Constraint { protected SMTLib smtlib() { return smtlib; } Constraint(String name, SMTLib smtlib); List<LocationVariable<?>> variablesForExpression(LocationVariableContainer container); List<LocationVariable<?>> variablesForSubexpression(LocationVariableContainer container); boolean isCompound(); ICommand definition(LocationVariableContainer container); List<IDeclaration> parameters(LocationVariableContainer container); IExpr invocation(LocationVariableContainer container); List<IExpr> invocationArguments(LocationVariableContainer container); IExpr invocationWithValues(LocationVariableContainer container, Map<String, Object> values);  }
@Test public void acyclicityConstraint() throws ParserException { Constraint acyclicity = new AcyclicityConstraint(smtlib()); LocationVariableContainer container = locationVariableContainerExample(); List<String> arguments = LocationVariable.expressionsOf(container.operatorsAndParameters()); checkArguments(acyclicity, container, arguments); checkInvocation(acyclicity, container, arguments); Map<String, String> types = typesFor(container); List<String> declarations = builtDeclarations(arguments, types); List<IDeclaration> smtDeclarations = checkParameters(acyclicity, container, declarations); List<String> definitions = Arrays.asList("(< L@op<0><0> L@op<0>)", "(< L@op<0><1> L@op<0>)", "(< L@op<1><0> L@op<1>)", "(< L@op<1><1> L@op<1>)", "(< L@op<2><0> L@op<2>)", "(< L@op<2><1> L@op<2>)", "(< L@op<2><2> L@op<2>)", "(< L@op<3><0> L@op<3>)"); Collection<IExpr> smtDefinitions = checkDefinitionExpressions(acyclicity, container, definitions); checkDefinition(acyclicity, container, declarations, smtDeclarations, definitions, smtDefinitions, "and"); }
@Test public void consistencyConstraint() throws ParserException { Constraint consistencty = new ConsistencyConstraint(smtlib()); LocationVariableContainer container = locationVariableContainerExample(); List<String> arguments = LocationVariable.expressionsOf((List) container.operators()); checkArguments(consistencty, container, arguments); checkInvocation(consistencty, container, arguments); Map<String, String> types = typesFor(container); List<String> declarations = builtDeclarations(arguments, types); List<IDeclaration> smtDeclarations = checkParameters(consistencty, container, declarations); List<String> definitions = Arrays.asList("(distinct L@op<0> L@op<1>)", "(distinct L@op<0> L@op<2>)", "(distinct L@op<0> L@op<3>)", "(distinct L@op<1> L@op<2>)", "(distinct L@op<1> L@op<3>)", "(distinct L@op<2> L@op<3>)"); Collection<IExpr> smtDefinitions = checkDefinitionExpressions(consistencty, container, definitions); checkDefinition(consistencty, container, declarations, smtDeclarations, definitions, smtDefinitions, "and"); }
@Test public void lineBoundConstraint() throws ParserException { Constraint lineBound = new LineBoundConstraint(smtlib()); LocationVariableContainer container = locationVariableContainerExample(); List<String> arguments = LocationVariable.expressionsOf(container.operatorsParametersAndOutput()); checkArguments(lineBound, container, arguments); checkInvocation(lineBound, container, arguments); Map<String, String> types = typesFor(container); List<String> declarations = builtDeclarations(arguments, types); List<IDeclaration> smtDeclarations = checkParameters(lineBound, container, declarations); List<String> definitions = Arrays.asList("(and (<= 3 L@op<0>) (<= L@op<0> 6))", "(and (<= 3 L@op<1>) (<= L@op<1> 6))", "(and (<= 3 L@op<2>) (<= L@op<2> 6))", "(and (<= 3 L@op<3>) (<= L@op<3> 6))", "(or (= 1 L@op<0><0>) (= 2 L@op<0><0>) (= L@op<2> L@op<0><0>))", "(or (= 1 L@op<0><1>) (= 2 L@op<0><1>) (= L@op<2> L@op<0><1>))", "(or (= 0 L@op<1><0>) (= L@op<3> L@op<1><0>))", "(or (= 0 L@op<1><1>) (= L@op<3> L@op<1><1>))", "(or (= 0 L@op<2><0>) (= L@op<1> L@op<2><0>) (= L@op<3> L@op<2><0>))", "(or (= 1 L@op<2><1>) (= 2 L@op<2><1>) (= L@op<0> L@op<2><1>))", "(or (= 1 L@op<2><2>) (= 2 L@op<2><2>) (= L@op<0> L@op<2><2>))", "(or (= 0 L@op<3><0>) (= L@op<1> L@op<3><0>))", "(or (= 0 L@out) (= L@op<1> L@out) (= L@op<3> L@out))"); Collection<IExpr> smtDefinitions = checkDefinitionExpressions(lineBound, container, definitions); checkDefinition(lineBound, container, declarations, smtDeclarations, definitions, smtDefinitions, "and"); }
@Test public void libraryConstraint() throws ParserException { Constraint library = new LibraryConstraint(smtlib()); LocationVariableContainer container = locationVariableContainerExample(); List<String> arguments = LocationVariable.subexpressionsOf(container.operatorsAndParameters()); checkArguments(library, container, arguments); checkInvocation(library, container, arguments); Map<String, String> types = typesFor(container); List<String> declarations = builtDeclarations(arguments, types); List<IDeclaration> smtDeclarations = checkParameters(library, container, declarations); List<String> definitions = Arrays.asList("(= op<0> (+ op<0><0> op<0><1>))", "(= op<1> (or op<1><0> op<1><1>))", "(= op<2> (ite op<2><0> op<2><1> op<2><2>))", "(= op<3> (not op<3><0>))"); Collection<IExpr> smtDefinitions = checkDefinitionExpressions(library, container, definitions); checkDefinition(library, container, declarations, smtDeclarations, definitions, smtDefinitions, "and"); }
@Test public void connectivityConstraint() throws ParserException { Constraint connectivity = new ConnectivityConstraint(smtlib()); LocationVariableContainer container = locationVariableContainerExample(); List<String> arguments = LocationVariable.expressionsOf(container.operatorsParametersAndOutput()); arguments.addAll(LocationVariable.subexpressionsOf((List) container.inputs())); arguments.addAll(LocationVariable.subexpressionsOf(container.operatorsParametersAndOutput())); checkArguments(connectivity, container, arguments); checkInvocation(connectivity, container, arguments); Map<String, String> types = typesFor(container); List<String> declarations = builtDeclarations(arguments, types); List<IDeclaration> smtDeclarations = checkParameters(connectivity, container, declarations); List<String> definitions = Arrays.asList("(=> (= L@out 0) (= out in<0>))", "(=> (= L@out L@op<1>) (= out op<1>))", "(=> (= L@out L@op<3>) (= out op<3>))", "(=> (= L@op<0><0> 1) (= op<0><0> in<1>))", "(=> (= L@op<0><0> 2) (= op<0><0> in<2>))", "(=> (= L@op<0><0> L@op<2>) (= op<0><0> op<2>))", "(=> (= L@op<0><1> 1) (= op<0><1> in<1>))", "(=> (= L@op<0><1> 2) (= op<0><1> in<2>))", "(=> (= L@op<0><1> L@op<2>) (= op<0><1> op<2>))", "(=> (= L@op<1><0> 0) (= op<1><0> in<0>))", "(=> (= L@op<1><0> L@op<3>) (= op<1><0> op<3>))", "(=> (= L@op<1><1> 0) (= op<1><1> in<0>))", "(=> (= L@op<1><1> L@op<3>) (= op<1><1> op<3>))", "(=> (= L@op<2><0> 0) (= op<2><0> in<0>))", "(=> (= L@op<2><0> L@op<1>) (= op<2><0> op<1>))", "(=> (= L@op<2><0> L@op<3>) (= op<2><0> op<3>))", "(=> (= L@op<2><1> 1) (= op<2><1> in<1>))", "(=> (= L@op<2><1> 2) (= op<2><1> in<2>))", "(=> (= L@op<2><1> L@op<0>) (= op<2><1> op<0>))", "(=> (= L@op<2><2> 1) (= op<2><2> in<1>))", "(=> (= L@op<2><2> 2) (= op<2><2> in<2>))", "(=> (= L@op<2><2> L@op<0>) (= op<2><2> op<0>))", "(=> (= L@op<3><0> 0) (= op<3><0> in<0>))", "(=> (= L@op<3><0> L@op<1>) (= op<3><0> op<1>))"); Collection<IExpr> smtDefinitions = checkDefinitionExpressions(connectivity, container, definitions); checkDefinition(connectivity, container, declarations, smtDeclarations, definitions, smtDefinitions, "and"); }
@Test public void verificationConstraint() throws ParserException { Constraint verification = new VerificationConstraint(smtlib()); LocationVariableContainer container = locationVariableContainerExample(); List<String> arguments = LocationVariable.expressionsOf(container.operatorsParametersAndOutput()); arguments.addAll(LocationVariable.subexpressionsOf(container.inputsAndOutput())); checkArguments(verification, container, arguments); checkInvocation(verification, container, arguments); Map<String, String> types = typesFor(container); List<String> declarations = builtDeclarations(arguments, types); List<IDeclaration> smtDeclarations = checkParameters(verification, container, declarations); List<String> existsDeclarations = builtDeclarations(LocationVariable.subexpressionsOf(container.operatorsAndParameters()), types); String connectivityInvocation = "(Connectivity L@op<0> L@op<1> L@op<2> L@op<3> L@op<0><0> L@op<0><1> L@op<1><0> " + "L@op<1><1> L@op<2><0> L@op<2><1> L@op<2><2> L@op<3><0> L@out in<0> in<1> in<2> op<0> op<1> op<2> op<3> op<0><0> " + "op<0><1> op<1><0> op<1><1> op<2><0> op<2><1> op<2><2> op<3><0> out)"; String libraryInvocation = "(Library op<0> op<1> op<2> op<3> op<0><0> op<0><1> op<1><0> op<1><1> op<2><0> op<2><1> op<2><2> op<3><0>)"; List<String> definitions = Arrays.asList(String.format("(exists (%s) (and %s %s))", StringLibrary.join(existsDeclarations, ' '), connectivityInvocation, libraryInvocation)); Collection<IExpr> smtDefinitions = checkDefinitionExpressions(verification, container, definitions); checkDefinition(verification, container, declarations, smtDeclarations, definitions, smtDefinitions, ""); arguments.removeAll(asList("in<0>", "in<1>", "in<2>", "out")); arguments.addAll(asList("true", "1", "3", "false")); Map<String, Object> values = MetaMap.newHashMap(asList("i != null", "i.size()", "i.get(\"n\")", "returnValue"), (List) asList(true, 1, 3, false)); checkInvocationWithValues(verification, container, values, arguments); }
@Test public void wellFormedProgramConstraint() throws ParserException { Constraint wellFormedProgram = new WellFormedProgramConstraint(smtlib()); LocationVariableContainer container = locationVariableContainerExample(); List<String> arguments = LocationVariable.expressionsOf(container.operatorsParametersAndOutput()); checkArguments(wellFormedProgram, container, arguments); checkInvocation(wellFormedProgram, container, arguments); Map<String, String> types = typesFor(container); List<String> declarations = builtDeclarations(arguments, types); List<IDeclaration> smtDeclarations = checkParameters(wellFormedProgram, container, declarations); String acyclicityInvocation = "(Acyclicity L@op<0> L@op<1> L@op<2> L@op<3> L@op<0><0> L@op<0><1> L@op<1><0> L@op<1><1> L@op<2><0> L@op<2><1> L@op<2><2> L@op<3><0>)"; String consistencyInvocation = "(Consistency L@op<0> L@op<1> L@op<2> L@op<3>)"; String lineBoundInovcation = "(LineBound L@op<0> L@op<1> L@op<2> L@op<3> L@op<0><0> L@op<0><1> L@op<1><0> L@op<1><1> L@op<2><0> L@op<2><1> L@op<2><2> L@op<3><0> L@out)"; List<String> definitions = Arrays.asList(acyclicityInvocation, consistencyInvocation, lineBoundInovcation); Collection<IExpr> smtDefinitions = checkDefinitionExpressions(wellFormedProgram, container, definitions); checkDefinition(wellFormedProgram, container, declarations, smtDeclarations, definitions, smtDefinitions, "and"); }