Method in Houdini to allow an expression to be turned into non-candidate form

1 files changed, 22 insertions, 0 deletions

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 4f1e2a8b..4dd985b4 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -548,6 +548,28 @@ namespace Microsoft.Boogie.Houdini {
       return false;

     }

 

+    public static bool GetCandidateWithoutConstant(Expr boogieExpr, IEnumerable<string> candidates, out string candidateConstant, out Expr exprWithoutConstant) {

+      candidateConstant = null;

+      exprWithoutConstant = null;

+      NAryExpr e = boogieExpr as NAryExpr;

+      if (e != null && e.Fun is BinaryOperator && ((BinaryOperator)e.Fun).Op == BinaryOperator.Opcode.Imp) {

+        Expr antecedent = e.Args[0];

+        Expr consequent = e.Args[1];

+

+        IdentifierExpr id = antecedent as IdentifierExpr;

+        if (id != null && id.Decl is Constant && candidates.Contains(id.Decl.Name)) {

+          candidateConstant = id.Decl.Name;

+          exprWithoutConstant = consequent;

+          return true;

+        }

+

+        if (GetCandidateWithoutConstant(consequent, candidates, out candidateConstant, out exprWithoutConstant))

+          exprWithoutConstant = Expr.Imp(antecedent, exprWithoutConstant);

+          return true;

+      }

+      return false;

+    }

+

     private static Expr AddConditionToCandidateRec(Expr boogieExpr, Expr condition, string candidateConstant, List<Expr> implicationStack)

     {

         NAryExpr e = boogieExpr as NAryExpr;