From: trevor_hansen Date: Mon, 27 Jul 2009 15:35:56 +0000 (+0000) Subject: Signed right shift is implemented. Disable two very expensive assertion functions. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=cbc0cf6b4155a3598cbaaf48581256028a089ffc;p=francis%2Fstp.git Signed right shift is implemented. Disable two very expensive assertion functions. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@93 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/AST/AST.h b/AST/AST.h index 627bd89..d8862c4 100644 --- a/AST/AST.h +++ b/AST/AST.h @@ -1361,6 +1361,7 @@ private: void BBLShift(ASTVec& x); void BBRShift(ASTVec& x); + void BBRSignedShift(ASTVec& x, unsigned int shift); void BBLShift(ASTVec& x, unsigned int shift); void BBRShift(ASTVec& x, unsigned int shift); diff --git a/AST/BitBlast.cpp b/AST/BitBlast.cpp index 8f50ccf..4816064 100644 --- a/AST/BitBlast.cpp +++ b/AST/BitBlast.cpp @@ -122,6 +122,7 @@ const ASTNode BeevMgr::BBTerm(const ASTNode& term) } case BVRIGHTSHIFT: + case BVSRSHIFT: { if (BVCONST == term[1].GetKind()) { @@ -131,7 +132,11 @@ const ASTNode BeevMgr::BBTerm(const ASTNode& term) ASTNode term0 = BBTerm(term[0]); ASTVec children(term0.GetChildren()); // mutable copy of the children. - BBRShift(children, shift); + + if (BVRIGHTSHIFT == k) + BBRShift(children, shift); + else + BBRSignedShift(children, shift); result = CreateNode(BOOLVEC, children); } @@ -141,6 +146,14 @@ const ASTNode BeevMgr::BBTerm(const ASTNode& term) const ASTVec& bbarg1 = BBTerm(term[0]).GetChildren(); const ASTVec& bbarg2 = BBTerm(term[1]).GetChildren(); + + // Signed right shift, need to copy the sign bit. + ASTNode toFill; + if (BVRIGHTSHIFT == k) + toFill = ASTFalse; + else + toFill = bbarg1.back(); + ASTVec temp_result(bbarg1); for (unsigned int i = 0; i < bbarg2.size(); i++) @@ -155,7 +168,7 @@ const ASTNode BeevMgr::BBTerm(const ASTNode& term) for (unsigned int j = 0; j < temp_result.size(); j++) { if (j + shift_amount >= temp_result.size()) - temp_result[j] = CreateSimpForm(ITE, bbarg2[i], ASTFalse, temp_result[j]); + temp_result[j] = CreateSimpForm(ITE, bbarg2[i], toFill, temp_result[j]); else temp_result[j] = CreateSimpForm(ITE, bbarg2[i], temp_result[j + shift_amount], temp_result[j]); @@ -175,8 +188,6 @@ const ASTNode BeevMgr::BBTerm(const ASTNode& term) } } break; - - case BVSRSHIFT: case BVVARSHIFT: FatalError("BBTerm: These kinds have not been implemented in the BitBlaster: ", term); break; @@ -1038,6 +1049,23 @@ void BeevMgr::BBRShift(ASTVec& x, unsigned int shift) } } +// Right shift within fixed field copying the MSB. +// Writes result into first argument. +void BeevMgr::BBRSignedShift(ASTVec& x, unsigned int shift) +{ + // right shift x (destructively) within width. + ASTNode & MSB = x.back(); + ASTVec::iterator xend = x.end(); + ASTVec::iterator xit = x.begin(); + for (; xit < xend; xit++) + { + if (xit + shift < xend) + *xit = *(xit + shift); + else + *xit = MSB; // new MSB is zero. + } +} + // Right shift by 1 within fixed field, inserting new zeros at MSB. // Writes result into first argument. // Fixme: generalize to n bits. diff --git a/AST/ToSAT.cpp b/AST/ToSAT.cpp index e8cd101..bbee194 100644 --- a/AST/ToSAT.cpp +++ b/AST/ToSAT.cpp @@ -1158,7 +1158,8 @@ int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts) Begin_RemoveWrites = false; newq = TransformFormula(newq); - assertTransformPostConditions(newq); + if (false) + assertTransformPostConditions(newq); ASTNodeStats("after transformation: ", newq); TermsAlreadySeenMap.clear(); diff --git a/AST/Transform.cpp b/AST/Transform.cpp index 8dd760c..72f607a 100644 --- a/AST/Transform.cpp +++ b/AST/Transform.cpp @@ -251,7 +251,7 @@ ASTNode BeevMgr::TransformFormula(const ASTNode& form) } break; } - assert(BVTypeCheckRecursive(result)); + //assert(BVTypeCheckRecursive(result)); TransformMap[simpleForm] = result; return result; } //End of TransformFormula diff --git a/bitvec/consteval.cpp b/bitvec/consteval.cpp index 6ccb97d..8e96db6 100644 --- a/bitvec/consteval.cpp +++ b/bitvec/consteval.cpp @@ -125,7 +125,10 @@ ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t) break; } case BVRIGHTSHIFT: + case BVSRSHIFT: { + bool msb = CONSTANTBV::BitVector_msb_(tmp0); + output = CONSTANTBV::BitVector_Create(inputwidth, true); // the shift is destructive, get a copy. @@ -135,6 +138,18 @@ ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t) unsigned int shift = GetUnsignedConst(BVConstEvaluator(t[1])); CONSTANTBV::BitVector_Move_Right(output, shift); + + if (BVSRSHIFT == k && msb) + { + // signed shift, and the number was originally negative. + // Shift may be larger than the inputwidth. + for (int i =0; i < min(shift,inputwidth);i++) + { + CONSTANTBV::BitVector_Bit_On(output,(inputwidth-1 -i)); + } + assert(CONSTANTBV::BitVector_Sign(output) == -1); //must be negative. + } + OutputNode = CreateBVConst(output, outputwidth); break; } @@ -304,7 +319,7 @@ ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t) { // Signs are both positive CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1, remainder); - if(e != CONSTANTBV::ErrCode_Ok) + if (e != CONSTANTBV::ErrCode_Ok) { cerr << "Error code was:" << e << endl; assert(e == CONSTANTBV::ErrCode_Ok); diff --git a/parser/smtlib.y b/parser/smtlib.y index b1ed151..b5be9d1 100644 --- a/parser/smtlib.y +++ b/parser/smtlib.y @@ -1056,20 +1056,12 @@ an_nonbvconst_term: } | BVARITHRIGHTSHIFT_TOK an_term an_term { - unsigned int shift_amt = GetUnsignedConst(*$3); -// BEEV::ASTNode leading_zeros = BEEV::globalBeevMgr_for_parser->CreateBVConst(shift_amt, 0); + // shifting arithmetic right by who know how much? unsigned int w = $2->GetValueWidth(); - - BEEV::ASTNode width = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, shift_amt + w); - BEEV::ASTNode extended = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVSX, shift_amt+w, *$2, width); - - BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,w-1); - BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,shift_amt); - BEEV::ASTNode extract = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,w-shift_amt,*$2,hi,low); - - $$ = new BEEV::ASTNode(extract); + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVSRSHIFT,w,*$2,*$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; delete $2; - delete $3; } | BVROTATE_LEFT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term { diff --git a/simplifier/simplifier.cpp b/simplifier/simplifier.cpp index d94af9b..0ba3d3a 100644 --- a/simplifier/simplifier.cpp +++ b/simplifier/simplifier.cpp @@ -828,7 +828,7 @@ ASTNode BeevMgr::SimplifyXorFormula(const ASTNode& a, bool pushNeg) a1 = output[1]; if (a0 == a1) output = ASTFalse; - else if (a0 == ASTTrue && a1 == ASTFalse || a0 == ASTFalse && a1 == ASTTrue) + else if ((a0 == ASTTrue && a1 == ASTFalse) || (a0 == ASTFalse && a1 == ASTTrue)) output = ASTTrue; }