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 627bd899ad461d201bfb646cf73d9d3fda7a2ee5..d8862c495438b6bbc3d0a3cd07077b310b11020c 100644 (file)
--- 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 8f50ccf41adf0413ed3146aea13ad4df1a60e8ea..4816064515a0dd8a90ff58de1777670a0ae6a973 100644 (file)
--- 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 e8cd1016f42bddc6718d7a2a050934ce24dee19a..bbee194d4824f8ec6b1127449ff24ec7a541a8d3 100644 (file)
--- 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 8dd760cac9419314943613290d573d7ceee22fdc..72f607a54a0ad949aecf658bc4a432e4e7233366 100644 (file)
--- 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 6ccb97d011971d3c9cbea735593472378271a3c4..8e96db69010938e12e35bafd70a744adc16fedbb 100644 (file)
--- 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 b1ed1510682333c989cc7f7f19906cd9ac57d740..b5be9d16028f58d4da68153d1803507f4d3a37ce 100644 (file)
--- 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 d94af9b8df81ccd1d0c0fa2f002b7c5c1a2184a9..0ba3d3a5eb9dec0cf6f9eb56e196b228c3938e59 100644 (file)
--- 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;
        }