Code to apply the alwaysTrueSet. Not currently enabled.

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

diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp
index 74bda591f613086a92b4335fe9cf2fa5dc7a2ae7..a7adb9c901c655daf3f8d1ee39a61a5a91a1c77f 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","Variable Elimination", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation","Array Read Refinement", "Applying Substitutions", "Removing Unconstrained", "Pure Literals" , "ITE Contexts", "AIG core simplification", "Interval Propagation"};
+std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Variable Elimination", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation","Array Read Refinement", "Applying Substitutions", "Removing Unconstrained", "Pure Literals" , "ITE Contexts", "AIG core simplification", "Interval Propagation", "Always True"};
 
 namespace BEEV
 {

diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h
index 4a558e67c53ede5d64c2555dc48b5e36841c90ef..f19839765ae0b5aef0bd829ca9b57f8c93c97ea7 100644 (file)
--- a/src/AST/RunTimes.h
+++ b/src/AST/RunTimes.h
@@ -37,7 +37,8 @@ public:
       PureLiterals,
       UseITEContext,
       AIGSimplifyCore,
-      IntervalPropagation
+      IntervalPropagation,
+      AlwaysTrue
     };
 
   static std::string CategoryNames[];

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index e87ea4c6543fd0eefdb6b7fa85238440a6bbc1be..1c5478fce37bde1b28117df7f64a791a615d4c70 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -19,6 +19,7 @@
 #include "../simplifier/FindPureLiterals.h"
 #include "../simplifier/EstablishIntervals.h"
 #include "../simplifier/UseITEContext.h"
+#include "../simplifier/AlwaysTrue.h"
 #include "../simplifier/AIGSimplifyPropositionalCore.h"
 #include <memory>
 
@@ -146,6 +147,15 @@ namespace BEEV {
             bm->ASTNodeStats("After Pure Literals: ", simplified_solved_InputToSAT);
           }
       }
+
+    if (bm->UserFlags.isSet("always-true", "0"))
+      {
+        SimplifyingNodeFactory nf(*(bm->hashingNodeFactory), *bm);
+        AlwaysTrue always (simp,bm,&nf);
+        simplified_solved_InputToSAT = always.topLevel(simplified_solved_InputToSAT);
+        bm->ASTNodeStats("After removing always true: ", simplified_solved_InputToSAT);
+      }
+
     if (bm->UserFlags.wordlevel_solve_flag && bm->UserFlags.optimize_flag)
       {
         simplified_solved_InputToSAT = bvSolver->TopLevelBVSolve(simplified_solved_InputToSAT, false);
@@ -341,6 +351,15 @@ namespace BEEV {
 
             simplified_solved_InputToSAT = simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
             bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
+
+
+            if (bm->UserFlags.isSet("always-true", "0"))
+              {
+                SimplifyingNodeFactory nf(*(bm->hashingNodeFactory), *bm);
+                AlwaysTrue always (simp,bm,&nf);
+                simplified_solved_InputToSAT = always.topLevel(simplified_solved_InputToSAT);
+                bm->ASTNodeStats("After removing always true: ", simplified_solved_InputToSAT);
+              }
           }
 
         // The word level solver uses the simplifier to apply the rewrites it makes,

diff --git a/src/simplifier/AlwaysTrue.h b/src/simplifier/AlwaysTrue.h
new file mode 100644 (file)
index 0000000..878e01f
--- /dev/null
+++ b/src/simplifier/AlwaysTrue.h
@@ -0,0 +1,113 @@
+#ifndef ALWAYSTRUE_H_
+#define ALWAYSTRUE_H_
+
+//Applies the AlwaysTrueSet to the input node.
+
+#include <map>
+#include "../AST/AST.h"
+#include "../STPManager/STPManager.h"
+#include "../simplifier/simplifier.h"
+
+namespace BEEV
+{
+
+class AlwaysTrue
+{
+  Simplifier *simplifier;
+  STPMgr* stp;
+  NodeFactory *nf;
+
+  enum State {AND_STATE, NOT_STATE, BOTTOM_STATE};
+
+public:
+  AlwaysTrue(Simplifier *simplifier_, STPMgr* stp_, NodeFactory *nf_)
+  {
+    simplifier = simplifier_;
+    stp = stp_;
+    nf = nf_;
+  }
+
+  virtual
+  ~AlwaysTrue()
+  {}
+
+  ASTNode topLevel(ASTNode& n)
+  {
+    stp->GetRunTimes()->start(RunTimes::AlwaysTrue);
+    ASTNodeMap fromTo;
+    ASTNode result = visit(n,AND_STATE,fromTo);
+    stp->GetRunTimes()->stop(RunTimes::AlwaysTrue);
+    return result;
+  }
+
+  // Replace nodes that aren't conjoined to the top with TRUE/FALSE,
+  // if that node is conjoined..
+  // The "state" tracks whether we are still at nodes that are conjoined to the top,
+  // only after we get out of the top part can we replace nodes that we know to be
+  // true or false.
+  ASTNode visit(const ASTNode&n, State state, ASTNodeMap& fromTo)
+  {
+    if (n.isConstant())
+      return n;
+
+    if (fromTo.find(n) != fromTo.end())
+    {
+        // It has been visited as BOTTOM_STATE once before.
+        return fromTo.find(n)->second;
+    }
+
+    ASTVec newChildren;
+    newChildren.reserve(n.Degree());
+    State new_state;
+
+    if (state == BOTTOM_STATE)
+    {
+        bool result;
+        if (simplifier->CheckAlwaysTrueFormSet(n,result))
+          {
+            cerr << "+";
+            if (result)
+              return stp->ASTTrue;
+            else
+              return stp->ASTFalse;
+          }
+    }
+
+    if (n.GetKind() == SYMBOL)
+      return n;
+
+    if (n.GetKind() != AND && state == AND_STATE )
+      {
+        if (n.GetKind() == NOT)
+          new_state = NOT_STATE;
+        else
+          new_state = BOTTOM_STATE;
+      }
+    else if (state == NOT_STATE)
+      new_state = BOTTOM_STATE;
+    else
+      new_state = state;
+
+    for (int i=0; i < n.Degree(); i++)
+      {
+        newChildren.push_back(visit(n[i],new_state,fromTo));
+      }
+
+    ASTNode result = n;
+    if (newChildren != n.GetChildren())
+      {
+        if (n.GetType() == BOOLEAN_TYPE)
+          result =  nf->CreateNode(n.GetKind(), newChildren);
+        else
+          result = nf->CreateArrayTerm(n.GetKind(), n.GetIndexWidth(), n.GetValueWidth(), newChildren);
+      }
+
+    if (state == BOTTOM_STATE)
+      {
+          fromTo.insert(make_pair(n,result));
+      }
+    return result;
+  }
+};
+};
+#endif