Adds the reverse of rules to catch an obscure but important for some of our benchmark...

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

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index c4a4da73fe9aaa56e4f0d9fdde91526a0183cd27..ce0b742ed6a78b192cba1430044e5a364f10b527 100644 (file)
--- a/src/simplifier/SubstitutionMap.cpp
+++ b/src/simplifier/SubstitutionMap.cpp
@@ -141,6 +141,14 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
                   if (UpdateSolverMap(symbol, newN))
                       output =  ASTTrue;
                }
+             else if (a[1].GetKind() == NOT && a[1][0].GetKind() == EQ && a[1][0][0].GetValueWidth() ==1 && a[1][0][1].GetKind() == SYMBOL)
+                {
+                  const ASTNode& symbol = a[1][0][1];
+                  const ASTNode newN = nf->CreateTerm(ITE, 1, a[0], a[1][0][0], nf->CreateTerm(BVNEG, 1,a[1][0][0]));
+
+                  if (UpdateSolverMap(symbol, newN))
+                      output =  ASTTrue;
+                }
              else if (a[0].GetKind() == EQ && a[0][0].GetValueWidth() ==1 && a[0][1].GetKind() == SYMBOL)
                {
                   // XOR ((= 1 v) ... )
@@ -151,6 +159,14 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
                   if (UpdateSolverMap(symbol, newN))
                       output =  ASTTrue;
                }
+             else if (a[1].GetKind() == EQ && a[1][0].GetValueWidth() ==1 && a[1][1].GetKind() == SYMBOL)
+                {
+                  const ASTNode& symbol = a[1][1];
+                  const ASTNode newN = nf->CreateTerm(ITE, 1, a[0], nf->CreateTerm(BVNEG, 1,a[1][0]), a[1][0]);
+
+                  if (UpdateSolverMap(symbol, newN))
+                      output =  ASTTrue;
+                }
              else
              return output;
            }