Partial fix of bvsmod, bvsrem. Both operations still report spurious division by...

Also, updated BVTypeCheck to return a boolean (so it is easy to use in asserts()). A trivial recursive typecheck function.

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

diff --git a/AST/AST.cpp b/AST/AST.cpp
index a03283350150654ebc52940f6981c03126c87d1b..9c97d6dd2cbeabe4ce11fa7ac06325e09b28d455 100644 (file)
--- a/AST/AST.cpp
+++ b/AST/AST.cpp
@@ -59,7 +59,7 @@ bool smtlib_parser_enable = false;
 //print the input back
 bool print_STPinput_back = false;
 
-enum BEEV::inputStatus input_status = NOT_DECLARED;
+enum inputStatus input_status = NOT_DECLARED;
 
 // Used only in smtlib lexer/parser
 ASTNode SingleBitOne;
@@ -1247,15 +1247,36 @@ ASTNode::ASTNode(const ASTNode &n) :
 #endif
 }
 
+// If there is a lot of sharing in the graph, this will take a long time.
+// it doesn't mark subgraphs as already having been typechecked.
+bool BeevMgr::BVTypeCheckRecursive(const ASTNode& n)
+{
+       const ASTVec& c = n.GetChildren();
+
+       BVTypeCheck(n);
+
+       for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++)
+               BVTypeCheckRecursive(*it);
+
+       return true;
+}
+
+
+
 /* FUNCTION: Typechecker for terms and formulas
  *
  * TypeChecker: Assumes that the immediate Children of the input
  * ASTNode have been typechecked. This function is suitable in
  * scenarios like where you are building the ASTNode Tree, and you
  * typecheck as you go along. It is not suitable as a general
- * typechecker
+ * typechecker.
+ *
+ * This ALWAYS returns true. If there is an error it will call
+ * FatalError() and abort.
  */
-void BeevMgr::BVTypeCheck(const ASTNode& n)
+
+
+bool BeevMgr::BVTypeCheck(const ASTNode& n)
 {
        Kind k = n.GetKind();
        //The children of bitvector terms are in turn bitvectors.
@@ -1269,7 +1290,7 @@ void BeevMgr::BVTypeCheck(const ASTNode& n)
                                        FatalError("BVTypeCheck: The term t does not typecheck, where t = \n", n);
                                break;
                        case SYMBOL:
-                               return;
+                               return true;
                        case ITE:
                                if (BOOLEAN_TYPE != n[0].GetType() || (n[1].GetType() != n[2].GetType()))
                                        FatalError("BVTypeCheck: The term t does not typecheck, where t = \n", n);
@@ -1392,7 +1413,7 @@ void BeevMgr::BVTypeCheck(const ASTNode& n)
                        case TRUE:
                        case FALSE:
                        case SYMBOL:
-                               return;
+                               return true;
                        case EQ:
                        case NEQ:
                                if (!(n[0].GetValueWidth() == n[1].GetValueWidth() && n[0].GetIndexWidth() == n[1].GetIndexWidth()))
@@ -1445,6 +1466,7 @@ void BeevMgr::BVTypeCheck(const ASTNode& n)
                                break;
                }
        }
+       return true;
 } //End of TypeCheck function
 
 //add an assertion to the current logical context

diff --git a/AST/AST.h b/AST/AST.h
index 3c487b255fc47b93eea4dd71c0edb2d4aa73b189..627bd899ad461d201bfb646cf73d9d3fda7a2ee5 100644 (file)
--- a/AST/AST.h
+++ b/AST/AST.h
@@ -1724,7 +1724,8 @@ public:
        ASTNode TransformFormula(const ASTNode& query);
        ASTNode TransformTerm(const ASTNode& term);
        ASTNode TransformArray(const ASTNode& term);
-       ASTNode TranslateSignedDivMod(const ASTNode& term);
+       ASTNode TranslateSignedDivModRem(const ASTNode& term);
+       void    assertTransformPostConditions(const ASTNode & term);
 
        //LET Management
 private:
@@ -1843,7 +1844,14 @@ public:
        //in scenarios like where you are building the ASTNode Tree, and
        //you typecheck as you go along. It is not suitable as a general
        //typechecker
-       void BVTypeCheck(const ASTNode& n);
+
+       // NB: The boolean value is always true!
+       bool BVTypeCheck(const ASTNode& n);
+
+       // Checks recursively all the way down.
+       bool BVTypeCheckRecursive(const ASTNode& n);
+
+
 
 private:
        //stack of Logical Context. each entry in the stack is a logical

diff --git a/AST/ToSAT.cpp b/AST/ToSAT.cpp
index f0505242c537759539e93d0029ad8abeb52c1e3b..e8cd1016f42bddc6718d7a2a050934ce24dee19a 100644 (file)
--- a/AST/ToSAT.cpp
+++ b/AST/ToSAT.cpp
@@ -1158,6 +1158,7 @@ int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts)
        Begin_RemoveWrites = false;
 
        newq = TransformFormula(newq);
+       assertTransformPostConditions(newq);
        ASTNodeStats("after transformation: ", newq);
        TermsAlreadySeenMap.clear();
 
@@ -1197,7 +1198,7 @@ int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts)
                return res;
        }
 
-       FatalError("TopLevelSAT: reached the end without proper conclusion:"
+       FatalError("TopLevelSATAux: reached the end without proper conclusion:"
                "either a divide by zero in the input or a bug in STP");
        //bogus return to make the compiler shut up
        return 2;

diff --git a/AST/Transform.cpp b/AST/Transform.cpp
index ecb522348f35e25d7b7afc0c78dcdadae09dfc1c..8dd760cac9419314943613290d573d7ceee22fdc 100644 (file)
--- a/AST/Transform.cpp
+++ b/AST/Transform.cpp
@@ -7,19 +7,20 @@
  ********************************************************************/
 // -*- c++ -*-
 
+// Transform: * Converts signed Div/ signed remainder/ signed modulus into unsigned.
+//            * Removes array selects / stores from formula.
+
+
 #include "AST.h"
 #include <stdlib.h>
 #include <stdio.h>
 namespace BEEV
 {
 
-//Translates signed BVDIV/BVMOD into unsigned variety
-ASTNode BeevMgr::TranslateSignedDivMod(const ASTNode& in)
+//Translates signed BVDIV,BVMOD and BVREM into unsigned variety
+ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in)
 {
-       if (!(SBVREM == in.GetKind() || SBVDIV == in.GetKind()))
-       {
-               FatalError("TranslateSignedDivMod: input must be signed DIV/MOD\n", in);
-       }
+       assert(in.GetChildren().size() ==2);
 
        ASTNode dividend = in[0];
        ASTNode divisor = in[1];
@@ -51,10 +52,13 @@ ASTNode BeevMgr::TranslateSignedDivMod(const ASTNode& in)
 
                //put everything together, simplify, and return
                ASTNode n = CreateTerm(ITE, len, cond_dividend, minus_modnode, modnode);
-               return SimplifyTerm_TopLevel(n);
+               return SimplifyTerm(n);
        }
 
-       if (SBVMOD == in.GetKind())
+       // This is the modulus of dividing rounding to -infinity.
+       // Except if the signs are different, and it perfectly divides
+       // the modulus is the divisor (not zero).
+       else if (SBVMOD == in.GetKind())
        {
                // (let (?msb_s (extract[|m-1|:|m-1|] s))
                // (let (?msb_t (extract[|m-1|:|m-1|] t))
@@ -67,16 +71,16 @@ ASTNode BeevMgr::TranslateSignedDivMod(const ASTNode& in)
                //      (bvneg (bvurem (bvneg s) (bvneg t)))))))
                ASTNode & s = dividend;
                ASTNode & t = divisor;
-               ASTNode & msb_s = cond_dividend;
-               ASTNode & msb_t = cond_divisor;
 
-               ASTNode isSPos = CreateNode(EQ, msb_s, zero); // (= ?msb_s bit0)
-               ASTNode isSNeg = CreateNode(EQ, msb_s, one); // (= ?msb_s bit1)
-               ASTNode isTPos = CreateNode(EQ, msb_t, zero); // (= ?msb_t bit0)
-               ASTNode isTNeg = CreateNode(EQ, msb_t, one); // (= ?msb_t bit1)
+               ASTNode isSNeg = cond_dividend; // (= ?msb_s bit1)
+               ASTNode isSPos = CreateNode(NOT, isSNeg); // (= ?msb_s bit0)
+
+               ASTNode isTNeg = cond_divisor; // (= ?msb_t bit1)
+               ASTNode isTPos = CreateNode(NOT, isTNeg); // (= ?msb_t bit0)
+
 
                ASTNode negS = CreateTerm(BVUMINUS, len, s); // (bvneg s)
-               ASTNode negT = CreateTerm(BVUMINUS, len, t); // (bvneg s)
+               ASTNode negT = CreateTerm(BVUMINUS, len, t); // (bvneg t)
 
                // (bvneg (bvurem (bvneg s) (bvneg t)))
                ASTNode branch4 = CreateTerm(BVUMINUS, len, CreateTerm(BVMOD, len, negS, negT));
@@ -91,133 +95,76 @@ ASTNode BeevMgr::TranslateSignedDivMod(const ASTNode& in)
                ASTNode ite2 = CreateTerm(ITE, len, CreateNode(AND, isSNeg, isTPos), branch2, ite3);
                ASTNode ite1 = CreateTerm(ITE, len, CreateNode(AND, isSPos, isTPos), branch1, ite2);
 
-               return SimplifyTerm_TopLevel(ite1);
+               return SimplifyTerm(ite1);
+       }
+       else if (SBVDIV == in.GetKind())
+       {
+               //now handle the BVDIV case
+               //if topBit(dividend) is 1 and topBit(divisor) is 0
+               //
+               //then output is -BVDIV(-dividend,divisor)
+               //
+               //elseif topBit(dividend) is 0 and topBit(divisor) is 1
+               //
+               //then output is -BVDIV(dividend,-divisor)
+               //
+               //elseif topBit(dividend) is 1 and topBit(divisor) is 1
+               //
+               // then output is BVDIV(-dividend,-divisor)
+               //
+               //else simply output BVDIV(dividend,divisor)
+
+               ASTNode divnode = CreateTerm(BVDIV, len, dividend, divisor);
+
+               ASTNode cond1 = CreateNode(AND, CreateNode(EQ, zero, CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1)), CreateNode(EQ, one, CreateTerm(BVEXTRACT,
+                               1, divisor, hi1, hi1)));
+               ASTNode minus_divnode1 = CreateTerm(BVDIV, len, dividend, CreateTerm(BVUMINUS, len, divisor));
+               minus_divnode1 = CreateTerm(BVUMINUS, len, minus_divnode1);
+
+               ASTNode cond2 = CreateNode(AND, CreateNode(EQ, one, CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1)), CreateNode(EQ, zero, CreateTerm(BVEXTRACT,
+                               1, divisor, hi1, hi1)));
+               ASTNode minus_divnode2 = CreateTerm(BVDIV, len, CreateTerm(BVUMINUS, len, dividend), divisor);
+               minus_divnode2 = CreateTerm(BVUMINUS, len, minus_divnode2);
+
+               ASTNode cond3 = CreateNode(AND, CreateNode(EQ, one, CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1)), CreateNode(EQ, one, CreateTerm(BVEXTRACT,
+                               1, divisor, hi1, hi1)));
+               ASTNode minus_divnode3 = CreateTerm(BVDIV, len, CreateTerm(BVUMINUS, len, dividend), CreateTerm(BVUMINUS, len, divisor));
+               ASTNode n = CreateTerm(ITE, len, cond1, minus_divnode1, CreateTerm(ITE, len, cond2, minus_divnode2, CreateTerm(ITE, len, cond3,
+                               minus_divnode3, divnode)));
+               return SimplifyTerm(n);
        }
 
-       //now handle the BVDIV case
-       //if topBit(dividend) is 1 and topBit(divisor) is 0
-       //
-       //then output is -BVDIV(-dividend,divisor)
-       //
-       //elseif topBit(dividend) is 0 and topBit(divisor) is 1
-       //
-       //then output is -BVDIV(dividend,-divisor)
-       //
-       //elseif topBit(dividend) is 1 and topBit(divisor) is 1
-       //
-       // then output is BVDIV(-dividend,-divisor)
-       //
-       //else simply output BVDIV(dividend,divisor)
-       ASTNode divnode = CreateTerm(BVDIV, len, dividend, divisor);
-
-       ASTNode cond1 = CreateNode(AND, CreateNode(EQ, zero, CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1)), CreateNode(EQ, one, CreateTerm(BVEXTRACT, 1,
-                       divisor, hi1, hi1)));
-       ASTNode minus_divnode1 = CreateTerm(BVDIV, len, dividend, CreateTerm(BVUMINUS, len, divisor));
-       minus_divnode1 = CreateTerm(BVUMINUS, len, minus_divnode1);
-
-       ASTNode cond2 = CreateNode(AND, CreateNode(EQ, one, CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1)), CreateNode(EQ, zero, CreateTerm(BVEXTRACT, 1,
-                       divisor, hi1, hi1)));
-       ASTNode minus_divnode2 = CreateTerm(BVDIV, len, CreateTerm(BVUMINUS, len, dividend), divisor);
-       minus_divnode2 = CreateTerm(BVUMINUS, len, minus_divnode2);
-
-       ASTNode cond3 = CreateNode(AND, CreateNode(EQ, one, CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1)), CreateNode(EQ, one, CreateTerm(BVEXTRACT, 1,
-                       divisor, hi1, hi1)));
-       ASTNode minus_divnode3 = CreateTerm(BVDIV, len, CreateTerm(BVUMINUS, len, dividend), CreateTerm(BVUMINUS, len, divisor));
-       ASTNode n = CreateTerm(ITE, len, cond1, minus_divnode1, CreateTerm(ITE, len, cond2, minus_divnode2, CreateTerm(ITE, len, cond3, minus_divnode3,
-                       divnode)));
-       return SimplifyTerm_TopLevel(n);
-}//end of TranslateSignedDivMod()
-
-/*
- //Translates signed BVDIV/BVMOD into unsigned variety
- ASTNode BeevMgr::TranslateSignedDivMod(const ASTNode& in) {
- if(!(SBVREM == in.GetKind() || SBVDIV == in.GetKind())) {
- FatalError("TranslateSignedDivMod: input must be signed DIV/MOD\n",in);
- }
-
- ASTNode dividend = in[0];
- ASTNode divisor  = in[1];
- unsigned len = in.GetValueWidth();
- if(SBVMOD == in.GetKind()) {
- //if(TopBit(dividend)==1)
- //
- //then -BVMOD(-dividend,abs(divisor))
- //
- //else BVMOD(dividend,abs(divisor))
-
- //create the condition for the dividend
- ASTNode hi1  = CreateBVConst(32,len-1);
- ASTNode one  = CreateOneConst(1);
- ASTNode cond = CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,dividend,hi1,hi1));
-
- //create the condition and conditional for the divisor
- ASTNode cond_divisor = CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,divisor,hi1,hi1));
- ASTNode pos_divisor  = CreateTerm(ITE,len,cond_divisor,CreateTerm(BVUMINUS,len,divisor),divisor);
-
- //create the modulus term for each case
- ASTNode modnode = CreateTerm(BVMOD,len,dividend,pos_divisor);
- ASTNode minus_modnode = CreateTerm(BVMOD,len,CreateTerm(BVUMINUS,len,dividend),pos_divisor);
- minus_modnode = CreateTerm(BVUMINUS,len,minus_modnode);
-
- //put everything together, simplify, and return
- ASTNode n = CreateTerm(ITE,len,cond,minus_modnode,modnode);
- return SimplifyTerm_TopLevel(n);
- }
-
- //now handle the BVDIV case
- //if topBit(dividend) is 1 and topBit(divisor) is 0
- //
- //then output is -BVDIV(-dividend,divisor)
- //
- //elseif topBit(dividend) is 0 and topBit(divisor) is 1
- //
- //then output is -BVDIV(dividend,-divisor)
- //
- //elseif topBit(dividend) is 1 and topBit(divisor) is 1
- //
- // then output is BVDIV(-dividend,-divisor)
- //
- //else simply output BVDIV(dividend,divisor)
- ASTNode hi1 = CreateBVConst(32,len-1);
- ASTNode zero = CreateZeroConst(1);
- ASTNode one = CreateOneConst(1);
- ASTNode divnode = CreateTerm(BVDIV, len, dividend, divisor);
-
- ASTNode cond1 = CreateNode(AND,
- CreateNode(EQ,zero,CreateTerm(BVEXTRACT,1,dividend,hi1,hi1)),
- CreateNode(EQ,one, CreateTerm(BVEXTRACT,1,divisor,hi1,hi1)));
- ASTNode minus_divnode1 = CreateTerm(BVDIV,len,
- dividend,
- CreateTerm(BVUMINUS,len,divisor));
- minus_divnode1 = CreateTerm(BVUMINUS,len,minus_divnode1);
-
- ASTNode cond2 = CreateNode(AND,
- CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,dividend,hi1,hi1)),
- CreateNode(EQ,zero,CreateTerm(BVEXTRACT,1,divisor,hi1,hi1)));
- ASTNode minus_divnode2 = CreateTerm(BVDIV,len,
- CreateTerm(BVUMINUS,len,dividend),
- divisor);
- minus_divnode2 = CreateTerm(BVUMINUS,len,minus_divnode2);
-
- ASTNode cond3 = CreateNode(AND,
- CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,dividend,hi1,hi1)),
- CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,divisor,hi1,hi1)));
- ASTNode minus_divnode3 = CreateTerm(BVDIV,len,
- CreateTerm(BVUMINUS,len,dividend),
- CreateTerm(BVUMINUS,len,divisor));
- ASTNode n = CreateTerm(ITE,len,
- cond1,
- minus_divnode1,
- CreateTerm(ITE,len,
- cond2,
- minus_divnode2,
- CreateTerm(ITE,len,
- cond3,
- minus_divnode3,
- divnode)));
- return SimplifyTerm_TopLevel(n);
- }//end of TranslateSignedDivMod()
- */
+       FatalError("TranslateSignedDivModRem: input must be signed DIV/MOD/REM", in);
+       return ASTUndefined;
+
+}//end of TranslateSignedDivModRem()
+
+// Check that the transformations have occurred.
+void BeevMgr::assertTransformPostConditions(const ASTNode & term)
+{
+       const Kind k = term.GetKind();
+
+       // Check the signed operations have been removed.
+       assert(  SBVDIV != k);
+       assert(  SBVMOD != k);
+       assert(  SBVREM !=k);
+
+       // Check the array reads / writes have been removed
+       assert(  READ !=k );
+       assert(  WRITE !=k);
+
+       // There should be no nodes left of type array.
+       assert(0 == term.GetIndexWidth());
+
+       ASTVec c = term.GetChildren();
+       ASTVec::iterator it = c.begin();
+       ASTVec::iterator itend = c.end();
+       ASTVec o;
+       for (; it != itend; it++)
+       {
+               assertTransformPostConditions(*it);
+       }
+}
 
 ASTNode BeevMgr::TransformFormula(const ASTNode& form)
 {
@@ -304,7 +251,7 @@ ASTNode BeevMgr::TransformFormula(const ASTNode& form)
                        }
                        break;
        }
-       //BVTypeCheck(result);
+       assert(BVTypeCheckRecursive(result));
        TransformMap[simpleForm] = result;
        return result;
 } //End of TransformFormula
@@ -371,7 +318,7 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm)
 
                        if (SBVDIV == result.GetKind() || SBVREM == result.GetKind() || SBVMOD == result.GetKind())
                        {
-                               result = TranslateSignedDivMod(result);
+                               result = TranslateSignedDivModRem(result);
                        }
                        break;
                }

diff --git a/AST/genkinds.pl b/AST/genkinds.pl
index 7944832b1ba9afbd6e00e1a06445f24e0993a8bc..1eaa4071807855b9682a51a8da9ecfc90247e687 100755 (executable)
--- a/AST/genkinds.pl
+++ b/AST/genkinds.pl
@@ -81,7 +81,7 @@ sub gen_h_file {
     print HFILE
        "extern const char *_kind_names[];\n\n",
        "/** Prints symbolic name of kind */\n",
-       "inline ostream& operator<<(ostream &os, const Kind &kind) { os << _kind_names[kind]; return os; }\n",
+       "inline std::ostream& operator<<(std::ostream &os, const Kind &kind) { os << _kind_names[kind]; return os; }\n",
        "\n\n",
        "};  // end namespace\n",
        "\n\n#endif\n";

diff --git a/bitvec/consteval.cpp b/bitvec/consteval.cpp
index e6ca42aac706264783937721ed85000ccdcda2ad..6ccb97d011971d3c9cbea735593472378271a3c4 100644 (file)
--- a/bitvec/consteval.cpp
+++ b/bitvec/consteval.cpp
@@ -236,13 +236,153 @@ ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t)
                        OutputNode = CreateBVConst(output, outputwidth);
                        break;
                }
-                       //FIXME ANOTHER SPECIAL CASE
+
+                       // SBVREM : Result of rounding the quotient towards zero. i.e. (-10)/3, has a remainder of -1
+                       // SBVMOD : Result of rounding the quotient towards -infinity. i.e. (-10)/3, has a modulus of 2.
+                       //          EXCEPT THAT if it divides exactly and the signs are different, then it's equal to the dividend.
                case SBVDIV:
                case SBVREM:
                {
-                       OutputNode = BVConstEvaluator(TranslateSignedDivMod(t));
+                       CBV quotient = CONSTANTBV::BitVector_Create(inputwidth, true);
+                       CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true);
+
+                       CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Divide(quotient, tmp0, tmp1, remainder);
+
+                       if (e != 0)
+                       {
+                               cerr << "WARNING" << endl;
+                               FatalError((const char*) CONSTANTBV::BitVector_Error(e));
+                       }
+
+                       if (SBVDIV == k)
+                       {
+                               OutputNode = CreateBVConst(quotient, outputwidth);
+                               CONSTANTBV::BitVector_Destroy(remainder);
+                       }
+                       else
+                       {
+                               OutputNode = CreateBVConst(remainder, outputwidth);
+                               CONSTANTBV::BitVector_Destroy(quotient);
+
+                       }
+
                        break;
                }
+
+               case SBVMOD:
+               {
+                       /* Definition taken from the SMTLIB website
+                        (bvsmod s t) abbreviates
+                        (let (?msb_s (extract[|m-1|:|m-1|] s))
+                        (let (?msb_t (extract[|m-1|:|m-1|] t))
+                        (ite (and (= ?msb_s bit0) (= ?msb_t bit0))
+                        (bvurem s t)
+                        (ite (and (= ?msb_s bit1) (= ?msb_t bit0))
+                        (bvadd (bvneg (bvurem (bvneg s) t)) t)
+                        (ite (and (= ?msb_s bit0) (= ?msb_t bit1))
+                        (bvadd (bvurem s (bvneg t)) t)
+                        (bvneg (bvurem (bvneg s) (bvneg t)))))))
+                        */
+
+                       assert(t[0].GetValueWidth() == t[1].GetValueWidth());
+
+                       bool isNegativeS = CONSTANTBV::BitVector_msb_(tmp0);
+                       bool isNegativeT = CONSTANTBV::BitVector_msb_(tmp1);
+
+                       CBV quotient = CONSTANTBV::BitVector_Create(inputwidth, true);
+                       CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true);
+                       tmp0 = CONSTANTBV::BitVector_Clone(tmp0);
+                       tmp1 = CONSTANTBV::BitVector_Clone(tmp1);
+
+                       if (CONSTANTBV::BitVector_is_empty(tmp1))
+                       {
+                               // If t is zero
+                               FatalError("Dividing by zero");
+                       }
+
+                       if (!isNegativeS && !isNegativeT)
+                       {
+                               // Signs are both positive
+                               CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1, remainder);
+                               if(e != CONSTANTBV::ErrCode_Ok)
+                               {
+                                       cerr << "Error code was:" << e << endl;
+                                       assert(e == CONSTANTBV::ErrCode_Ok);
+                               }
+                               OutputNode = CreateBVConst(remainder, outputwidth);
+                       }
+                       else if (isNegativeS && !isNegativeT)
+                       {
+                               // S negative, T positive.
+                               CBV tmp0b = CONSTANTBV::BitVector_Create(inputwidth, true);
+                               CONSTANTBV::BitVector_Negate(tmp0b, tmp0);
+
+                               CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0b, tmp1, remainder);
+
+                               assert(e == CONSTANTBV::ErrCode_Ok);
+
+                               CBV remb = CONSTANTBV::BitVector_Create(inputwidth, true);
+                               CONSTANTBV::BitVector_Negate(remb, remainder);
+
+                               bool carry = false;
+                               CBV res = CONSTANTBV::BitVector_Create(inputwidth, true);
+                               CONSTANTBV::BitVector_add(res, remb, tmp1, &carry);
+
+                               OutputNode = CreateBVConst(res, outputwidth);
+
+                               CONSTANTBV::BitVector_Destroy(tmp0b);
+                               CONSTANTBV::BitVector_Destroy(remb);
+                               CONSTANTBV::BitVector_Destroy(remainder);
+                       }
+                       else if (!isNegativeS && isNegativeT)
+                       {
+                               // If s is positive and t is negative
+                               CBV tmp1b = CONSTANTBV::BitVector_Create(inputwidth, true);
+                               CONSTANTBV::BitVector_Negate(tmp1b, tmp1);
+
+                               CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1b, remainder);
+
+                               assert(e == CONSTANTBV::ErrCode_Ok);
+
+                               bool carry = false;
+                               CBV res = CONSTANTBV::BitVector_Create(inputwidth, true);
+                               CONSTANTBV::BitVector_add(res, remainder, tmp1, &carry);
+
+                               OutputNode = CreateBVConst(res, outputwidth);
+
+                               CONSTANTBV::BitVector_Destroy(tmp1b);
+                               CONSTANTBV::BitVector_Destroy(remainder);
+                       }
+                       else if (isNegativeS && isNegativeT)
+                       {
+                               // Signs are both negative
+                               CBV tmp0b = CONSTANTBV::BitVector_Create(inputwidth, true);
+                               CBV tmp1b = CONSTANTBV::BitVector_Create(inputwidth, true);
+                               CONSTANTBV::BitVector_Negate(tmp0b, tmp0);
+                               CONSTANTBV::BitVector_Negate(tmp1b, tmp1);
+
+                               CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0b, tmp1b, remainder);
+                               assert(e == CONSTANTBV::ErrCode_Ok);
+
+                               CBV remb = CONSTANTBV::BitVector_Create(inputwidth, true);
+                               CONSTANTBV::BitVector_Negate(remb, remainder);
+
+                               OutputNode = CreateBVConst(remb, outputwidth);
+                               CONSTANTBV::BitVector_Destroy(tmp0b);
+                               CONSTANTBV::BitVector_Destroy(tmp1b);
+                               CONSTANTBV::BitVector_Destroy(remainder);
+                       }
+                       else
+                       {
+                               FatalError("never get called");
+                       }
+
+                       CONSTANTBV::BitVector_Destroy(tmp0);
+                       CONSTANTBV::BitVector_Destroy(tmp1);
+                       CONSTANTBV::BitVector_Destroy(quotient);
+               }
+                       break;
+
                case BVDIV:
                case BVMOD:
                {
@@ -291,12 +431,19 @@ ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t)
                        break;
                }
                case ITE:
-                       if (ASTTrue == t[0])
+               {
+                       ASTNode tmp0 = t[0]; // Should this run BVConstEvaluator??
+
+                       if (ASTTrue == tmp0)
                                OutputNode = BVConstEvaluator(t[1]);
-                       else if (ASTFalse == t[0])
+                       else if (ASTFalse == tmp0)
                                OutputNode = BVConstEvaluator(t[2]);
                        else
+                       {
+                               cerr << tmp0;
                                FatalError("BVConstEvaluator: ITE condiional must be either TRUE or FALSE:", t);
+                       }
+               }
                        break;
                case EQ:
                        if (CONSTANTBV::BitVector_equal(tmp0, tmp1))

diff --git a/simplifier/simplifier.cpp b/simplifier/simplifier.cpp
index 77c374fd6af7176c35b0b30800ab2557e4830f78..d94af9b8df81ccd1d0c0fa2f002b7c5c1a2184a9 100644 (file)
--- a/simplifier/simplifier.cpp
+++ b/simplifier/simplifier.cpp
@@ -1896,6 +1896,7 @@ ASTNode BeevMgr::SimplifyTerm(const ASTNode& inputterm)
                }
                case SBVREM:
                case SBVDIV:
+               case SBVMOD:
                {
                        ASTVec c = inputterm.GetChildren();
                        ASTVec o;