+
+ Expr ruleexpr=rule.getGuardExpr();
+ HashSet invariantvars=new HashSet();
+ Set invariants=ruleexpr.findInvariants(invariantvars);
+
+ if ((ruleexpr instanceof BooleanLiteralExpr)&&
+ ((BooleanLiteralExpr)ruleexpr).getValue()) {
+ if (rule.getInclusion() instanceof SetInclusion) {
+ invariants.addAll(((SetInclusion)rule.getInclusion()).getExpr().findInvariants(invariantvars));
+ } else if (rule.getInclusion() instanceof RelationInclusion) {
+ invariants.addAll(((RelationInclusion)rule.getInclusion()).getLeftExpr().findInvariants(invariantvars));
+ invariants.addAll(((RelationInclusion)rule.getInclusion()).getRightExpr().findInvariants(invariantvars));
+ }
+ }
+ ListIterator quantifiers = rule.quantifiers();
+ while (quantifiers.hasNext()) {
+ Quantifier quantifier = (Quantifier) quantifiers.next();
+ if (quantifier instanceof ForQuantifier) {
+ ForQuantifier fq=(ForQuantifier)quantifier;
+ invariants.addAll(fq.lower.findInvariants(invariantvars));
+ invariants.addAll(fq.upper.findInvariants(invariantvars));
+ }
+ }
+
+ for(Iterator invit=invariants.iterator();invit.hasNext();) {
+ Expr invexpr=(Expr)invit.next();
+ VarDescriptor tmpvd=VarDescriptor.makeNew("tmpvar");
+ VarDescriptor maybevd=VarDescriptor.makeNew("maybevar");
+ invexpr.generate(cr,tmpvd);
+ cr.outputline("int "+maybevd.getSafeSymbol()+"=maybe;");
+ cr.outputline("maybe=0;");
+ ivalue.assignPair(invexpr,tmpvd,maybevd);
+ }
+
+ quantifiers = rule.quantifiers();