]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commitdiff
Search for a AND (NOT a), a OR (NOT a), when doing node creation. This is necessary...
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Thu, 2 Feb 2012 12:29:35 +0000 (12:29 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Thu, 2 Feb 2012 12:29:35 +0000 (12:29 +0000)
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1550 e59a4935-1847-0410-ae03-e826735625c1

src/AST/NodeFactory/SimplifyingNodeFactory.cpp

index 13021980109262f9afa99b2a9da43a5d4746b8f1..e52ce5a94e46ba22ac3e05174f0a47a4e81f62d7 100644 (file)
@@ -338,6 +338,10 @@ SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd, const ASTVec &children)
       else
         next_it = it_end;
 
+      if (nextexists)
+        if (next_it->GetKind() == BEEV::NOT && (*next_it)[0] == *it)
+          return annihilator;
+
       if (*it == annihilator)
         {
           return annihilator;