* The simplifying node factory now removes TRUEs when creating ANDS.

* The simplifying node factory never creates IFF, just XORS.

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

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index c3bf3bda4ba9f22ed1eb23a184c04a29b425754c..7c009c92e8ff99c8af64a8c287e95e38f80f3ff7 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -100,6 +100,17 @@ ASTNode SimplifyingNodeFactory::CreateNode(Kind kind, const ASTVec & children)
        case BEEV::EQ:
                result = CreateSimpleEQ(children);
                break;
+       case BEEV::IFF:
+       {
+               assert(children.size() ==2);
+               ASTVec newCh;
+               newCh.reserve(2);
+               newCh.push_back(CreateSimpleNot(children[0]));
+               newCh.push_back(children[1]);
+           result = CreateSimpleXor(newCh);
+           break;
+       }
+
        default:
                result = hashing.CreateNode(kind, children);
        }
@@ -171,17 +182,12 @@ ASTNode SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd,
 {
        const Kind k = IsAnd ? BEEV::AND : BEEV::OR;
 
-       if (debug_simplifyingNodeFactory)
-       {
-               cout << "========" << endl << "CreateSimpAndOr " << k << " ";
-               lpvec(children);
-               cout << endl;
-       }
-
        const ASTNode& annihilator = (IsAnd ? ASTFalse : ASTTrue);
        const ASTNode& identity = (IsAnd ? ASTTrue : ASTFalse);
 
        ASTNode retval;
+       ASTVec new_children;
+       new_children.reserve(children.size());
 
        const ASTVec::const_iterator it_end = children.end();
        for (ASTVec::const_iterator it = children.begin(); it != it_end; it++)
@@ -196,41 +202,32 @@ ASTNode SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd,
 
                if (*it == annihilator)
                {
-                       retval = annihilator;
-                       if (debug_simplifyingNodeFactory)
-                       {
-                               cout << "Annihilator" << endl;
-                       }
-                       return retval;
+                       return annihilator;
                }
                else if (*it == identity || (nextexists && (*next_it == *it)))
                {
                        // just drop it
-               }
+               }else
+                       new_children.push_back(*it);
        }
 
        // If we get here, we saw no annihilators, and children should
        // be only the non-True nodes.
-       if (children.size() < 2)
+
+
+       if (0 == new_children.size())
        {
-               if (0 == children.size())
-               {
-                       retval = identity;
-               }
-               else
-               {
-                       // there is just one child
-                       retval = children[0];
-               }
+               retval = identity;
        }
-       else
+       else if (1==new_children.size())
        {
-               // 2 or more children.  Create a new node.
-               retval = hashing.CreateNode(IsAnd ? BEEV::AND : BEEV::OR, children);
+               // there is just one child
+               retval = new_children[0];
        }
-       if (debug_simplifyingNodeFactory)
+       else
        {
-               cout << "returns " << retval << endl;
+               // 2 or more children.  Create a new node.
+               retval = hashing.CreateNode(IsAnd ? BEEV::AND : BEEV::OR, new_children);
        }
        return retval;
 }

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 3f0ecfdbfb4fe40715f4f6eb9f96f4dcba8c5178..7c4cf1ff32ac2271f1a94ff114e04911c8f11df4 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -173,6 +173,7 @@ namespace BEEV {
     BVSolver* bvSolver = new BVSolver(bm,simp);
 
     simplified_solved_InputToSAT = sizeReducing(inputToSAT,bvSolver);
+    //simplified_solved_InputToSAT = sizeReducing(simplified_solved_InputToSAT,bvSolver);
 
     initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT);
     if (bm->UserFlags.stats_flag)