From 3c9b85d0ec6a06f14a299a0792b28742dbf85335 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 13 Apr 2011 14:21:58 +0000 Subject: [PATCH] Adds the reverse of rules to catch an obscure but important for some of our benchmarks rule. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1274 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/SubstitutionMap.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp index c4a4da7..ce0b742 100644 --- 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; } -- 2.47.3