Improvement. An analysis that simplifies ITES by determining what must be true/false...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1175 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp
index e411c7b138c06fee7269880720de2a8f9e893e91..5d7abc4327176b14e5a96309df0cde648a4a48f1 100644 (file)
--- a/src/AST/RunTimes.cpp
+++ b/src/AST/RunTimes.cpp
@@ -16,7 +16,7 @@
 #include "../sat/utils/System.h"
 
 // BE VERY CAREFUL> Update the Category Names to match.
-std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation","Array Read Refinement", "Applying Substitutions", "Remove Unconstrained", "Pure Literals" };
+std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation","Array Read Refinement", "Applying Substitutions", "Remove Unconstrained", "Pure Literals" , "ITE Contexts"};
 
 namespace BEEV
 {

diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h
index 0c9bbd7ae55d9e5c668e416199d5c614b95a11b7..cde22699ed9ed532fc8b8cb161bd8bc14d8feedf 100644 (file)
--- a/src/AST/RunTimes.h
+++ b/src/AST/RunTimes.h
@@ -34,7 +34,8 @@ public:
       ArrayReadRefinement,
       ApplyingSubstitutions,
       RemoveUnconstrained,
-      PureLiterals
+      PureLiterals,
+      UseITEContext
     };
 
   static std::string CategoryNames[];

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 5c32d9be71e7a70bf31e43f41559cee79269ff65..af29b221c9899f5271033a954d3ab7c829b9b673 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -18,6 +18,7 @@
 #include "../simplifier/RemoveUnconstrained.h"
 #include "../simplifier/FindPureLiterals.h"
 #include "../simplifier/EstablishIntervals.h"
+#include "../simplifier/UseITEContext.h"
 #include <memory>
 
 namespace BEEV {
@@ -192,6 +193,12 @@ namespace BEEV {
             }
         }
 
+        // Simplify using Ite context
+        {
+          UseITEContext iteC(bm);
+          simplified_solved_InputToSAT  = iteC.topLevel(simplified_solved_InputToSAT);
+        }
+
     bm->ASTNodeStats("Before SimplifyWrites_Inplace begins: ", 
                      simplified_solved_InputToSAT);
 

diff --git a/src/simplifier/UseITEContext.h b/src/simplifier/UseITEContext.h
new file mode 100644 (file)
index 0000000..ba32f9d
--- /dev/null
+++ b/src/simplifier/UseITEContext.h
@@ -0,0 +1,129 @@
+/*
+  *    Descend through ITEs keeping a stack of what must be true/false.
+  *    For instance. In the following:
+  *        (ite (or a b) (not (or a b)) c )
+  *
+  *       In the lhs of the ITE, we know that a or b are true, so, we can rewrite it to:
+  *       (ite (or a b) false c)
+  *
+ */
+
+#ifndef UseITEContext_H_
+#define UseITEContext_H_
+
+#include "../AST/AST.h"
+#include "../STPManager/STPManager.h"
+
+namespace BEEV
+{
+  class UseITEContext
+  {
+    NodeFactory *nf;
+    RunTimes *runtimes;
+    ASTNode ASTTrue, ASTFalse;
+
+    void addToContext(const ASTNode&n , ASTNodeSet& context)
+    {
+      if (n.GetKind() == NOT && n[0].GetKind() == OR)
+        {
+          ASTVec flat = FlattenKind(OR, n[0].GetChildren());
+          for (int i = 0; i < flat.size(); i++)
+            context.insert(nf->CreateNode(NOT, flat[i]));
+        }
+      else if (n.GetKind() == AND)
+        {
+          ASTVec flat = FlattenKind(AND, n.GetChildren());
+          context.insert(flat.begin(), flat.end());
+        }
+      else
+        context.insert(n);
+
+        //ASTNodeSet::iterator it = context.begin();
+        //cout << "NEW CONTEXT";
+        //while(it!=context.end())
+        //  {
+         //   cout << *it;
+         //   it++;
+         // }
+    }
+
+    ASTNode
+    visit(const ASTNode &n, ASTNodeMap& visited, ASTNodeSet& context)
+    {
+      if (n.isConstant())
+        return n;
+
+      ASTNodeMap::iterator it;
+      if ((it = visited.find(n)) != visited.end())
+        return it->second;
+
+      if (context.find(n) != context.end())
+        return ASTTrue;
+
+      if (context.find(nf->CreateNode(NOT,n)) != context.end())
+        return ASTFalse;
+
+      if (n.isAtom())
+        return n;
+
+      ASTVec new_children;
+
+      if (n.GetKind() == ITE)
+        {
+            ASTNodeSet lhsContext(context), rhsContext(context);
+            addToContext(n[0],lhsContext);
+            addToContext(nf->CreateNode(NOT,n[0]),rhsContext);
+            new_children.push_back(visit(n[0], visited,context));
+            new_children.push_back(visit(n[1], visited,lhsContext));
+            new_children.push_back(visit(n[2], visited,rhsContext));
+        }
+      else
+        {
+          for (int i = 0; i < n.GetChildren().size(); i++)
+            new_children.push_back(visit(n[i], visited, context));
+        }
+
+      ASTNode result;
+      if (new_children != n.GetChildren())
+          if (n.GetType() == BOOLEAN_TYPE)
+              result =  nf->CreateNode(n.GetKind(), new_children);
+            else
+               result =  nf->CreateArrayTerm(n.GetKind(), n.GetIndexWidth(), n.GetValueWidth(), new_children);
+      else
+        result = n;
+
+      visited.insert(make_pair(n,result));
+      return result;
+
+    }
+
+  public:
+
+    ASTNode
+    topLevel(const ASTNode& n)
+    {
+      runtimes->start(RunTimes::UseITEContext);
+      ASTNodeMap visited;
+      ASTNodeSet context;
+      ASTNode result= visit(n,visited,context);
+      runtimes->stop(RunTimes::UseITEContext);
+      return result;
+    }
+
+    UseITEContext(STPMgr *bm)
+    {
+      runtimes = bm->GetRunTimes();
+      nf = new SimplifyingNodeFactory(*(bm->hashingNodeFactory) ,*bm);
+      ASTTrue = bm->ASTTrue;
+      ASTFalse = bm->ASTFalse;
+    }
+
+    ~UseITEContext()
+    {
+      delete nf;
+    }
+  };
+}
+;
+
+#endif

diff --git a/unit_test/ite.smt2 b/unit_test/ite.smt2
new file mode 100644 (file)
index 0000000..ae7f809
--- /dev/null
+++ b/unit_test/ite.smt2
@@ -0,0 +1,42 @@
+
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+
+; These can be simplified by considering the context
+; of the ITES they contain. 
+
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(assert (ite (or a b) (not (or a b)) c ) )
+
+(declare-fun d () Bool)
+(declare-fun e () Bool)
+(assert (ite (and e d) e (and e d)  ) )
+
+(declare-fun f () Bool)
+(declare-fun g () Bool)
+(declare-fun h () Bool)
+(assert (ite (or f g) (and g f)  g   ) )
+
+(declare-fun i () Bool)
+(declare-fun j () Bool)
+(declare-fun k () Bool)
+(assert (ite i (ite j i (not i)) i ))
+
+; This doesn't simplify nicely down yet::
+;  108:(OR 
+;  50:m
+;   52:(AND 
+;     48:l
+;     50:m))
+(declare-fun l () Bool)
+(declare-fun m () Bool)
+(assert (ite (not (and l m)) m l  ) )
+
+
+(check-sat)
+(exit)
+