From 8eccaf54eb6f30bea1ad9b25b2ace0cabbb3fabb Mon Sep 17 00:00:00 2001
From: Daniel Plagge <plagge@cs.uni-duesseldorf.de>
Date: Fri, 8 Mar 2013 11:38:40 +0100
Subject: [PATCH] Added a flag that shows if a theory was used
---
.../translator/internal/TranslationVisitor.java | 14 ++++++++++++--
1 file changed, 12 insertions(+), 2 deletions(-)
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/TranslationVisitor.java b/de.prob.core/src/de/prob/eventb/translator/internal/TranslationVisitor.java
index 29021e9d..6c87173e 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/TranslationVisitor.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/TranslationVisitor.java
@@ -49,6 +49,8 @@ public class TranslationVisitor implements ISimpleVisitor {
private LookupStack<PSubstitution> substitutions = new LookupStack<PSubstitution>();
private LookupStack<String> boundVariables = new LookupStack<String>();
+ private boolean usesTheories = false;
+
public void visitAssociativeExpression(
final AssociativeExpression expression) {
// BUNION, BINTER, BCOMP, FCOMP, OVR, PLUS, MUL
@@ -602,6 +604,7 @@ public class TranslationVisitor implements ISimpleVisitor {
.getChildPredicates());
expressions.push(new AExtendedExprExpression(new TIdentifierLiteral(
symbol), childExprs, childPreds));
+ usesTheories = true;
}
@Override
@@ -613,6 +616,7 @@ public class TranslationVisitor implements ISimpleVisitor {
.getChildPredicates());
predicates.push(new AExtendedPredPredicate(new TIdentifierLiteral(
symbol), childExprs, childPreds));
+ usesTheories = true;
}
private List<PExpression> getSubExpressions(final Formula<?>[] children) {
@@ -701,14 +705,20 @@ public class TranslationVisitor implements ISimpleVisitor {
}
}
- public static void checkNewImplementation(Predicate p, PPredicate predicate) {
+ public static boolean checkNewImplementation(Formula<?> p,
+ Node oldImplementation) {
TranslationVisitor visitor = new TranslationVisitor();
p.accept(visitor);
- final String expected = predicate.toString();
+ final String expected = oldImplementation.toString();
final String actual = visitor.getPredicate().toString();
if (!expected.equals(actual)) {
throw new AssertionError("Expected:\n" + expected + "\n but was:\n"
+ actual);
}
+ return visitor.usesTheories;
+ }
+
+ public boolean usesTheories() {
+ return usesTheories;
}
}
--
GitLab