From 27d9d97208e172bd6ab6f89d141d92b331ee11ef Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 21 Feb 2011 04:06:29 +0000 Subject: [PATCH] Improvement. Simplifying EQ a little better. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1152 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/simplifier.cpp | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 87b6b45..7cb493e 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -956,6 +956,17 @@ namespace BEEV return ASTFalse; } + // The above loop has determined that the leading bits are the same. + if (constStart > 0) + { + int newWidth = in1.GetValueWidth() - constStart; + ASTNode zero = _bm->CreateZeroConst(32); + + ASTNode lhs = nf->CreateTerm(BVEXTRACT,newWidth, in1,_bm->CreateBVConst(32,newWidth-1) ,zero); + ASTNode rhs = nf->CreateTerm(BVEXTRACT,newWidth, in2,_bm->CreateBVConst(32,newWidth-1) ,zero); + return nf->CreateNode(EQ, lhs,rhs); + } + // If both the children are concats split them apart. // nb. This doesn't cover the case when the children are organised differently: // (concat (concat A B) C) == (concat A (concat B C)) @@ -964,6 +975,20 @@ namespace BEEV return nf->CreateNode(AND, nf->CreateNode(EQ, in1[0], in2[0]), nf->CreateNode(EQ, in1[1], in2[1])); } + // If the rhs is a concat, and the lhs is a constant. Split. + if (k1== BVCONST && k2 == BVCONCAT) + { + int width = in1.GetValueWidth(); + int bottomW = in2[1].GetValueWidth(); + ASTNode zero = _bm->CreateZeroConst(32); + + // split the constant. + ASTNode top = nf->CreateTerm(BVEXTRACT,bottomW, in1,_bm->CreateBVConst(32,width-1) ,_bm->CreateBVConst(32,bottomW)); + ASTNode bottom = nf->CreateTerm(BVEXTRACT,width-bottomW, in1,_bm->CreateBVConst(32,bottomW-1) ,zero); + + return nf->CreateNode(AND, nf->CreateNode(EQ, top, in2[0]), nf->CreateNode(EQ, bottom, in2[1])); + } + //last resort is to CreateNode return nf->CreateNode(EQ, in1, in2); -- 2.47.3