<commit_before>// -*- c++ -*-
/********************************************************************
 * AUTHORS: <NAME>, <NAME>
 *
 * BEGIN DATE: November, 2005
 *
 * LICENSE: Please view LICENSE file in the home dir of this Program
 ********************************************************************/

#include <cassert>
#include "simplifier.h"

namespace BEEV
{

  //error printing
  static void BVConstEvaluatorError(CONSTANTBV::ErrCode e, const ASTNode& t)
  {
    std::string ss("BVConstEvaluator:");
    ss += (const char*) BitVector_Error(e);
    FatalError(ss.c_str(), t);
  }

// Const evaluator logical and arithmetic operations.
  ASTNode NonMemberBVConstEvaluator(const ASTNode& t)
  {
    if (t.isConstant())
	 	return t;

	ASTNode OutputNode;
    Kind k = t.GetKind();

    STPMgr* _bm = t.GetSTPMgr();
    ASTNode& ASTTrue = _bm->ASTTrue;
    ASTNode& ASTFalse = _bm->ASTFalse;

    OutputNode = t;

    unsigned int inputwidth = t.GetValueWidth();
    unsigned int outputwidth = inputwidth;
    CBV output = NULL;

    CBV tmp0 = NULL;
    CBV tmp1 = NULL;

    ASTVec children;
    children.reserve(t.Degree());
    for (int i =0; i < t.Degree(); i++)
    {
    	if (t[i].isConstant())
    		children.push_back(t[i]);
    	else
    		children.push_back(NonMemberBVConstEvaluator(t[i]));
    }

    if ((t.Degree() ==2 || t.Degree() == 1) && t[0].GetType() == BITVECTOR_TYPE)
    {
    //saving some typing. BVPLUS does not use these variables. if the
    //input BVPLUS has two nodes, then we want to avoid setting these
    //variables.
    if (1 == t.Degree())
      {
        tmp0 = children[0].GetBVConst();
      }
    else if (2 == t.Degree() && k != BVPLUS)
      {
        tmp0 = children[0].GetBVConst();
        tmp1 = children[1].GetBVConst();
      }
	}

    switch (k)
      {
      case UNDEFINED:
      case READ:
      case WRITE:
      case SYMBOL:
    	    FatalError("BVConstEvaluator: term is not a constant-term", t);
        break;
      case BVCONST:
        OutputNode = t;
        break;
      case BVNEG:
        {
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          CONSTANTBV::Set_Complement(output, tmp0);
          OutputNode = _bm->CreateBVConst(output, outputwidth);
          break;
        }
      case BVSX:
      case BVZX:
        {
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          unsigned t0_width = t[0].GetValueWidth();
          if (inputwidth == t0_width)
            {
              CONSTANTBV::BitVector_Copy(output, tmp0);
              OutputNode = _bm->CreateBVConst(output, outputwidth);
            }
          else
            {
              bool topbit_sign = (k == BVSX)?(CONSTANTBV::BitVector_Sign(tmp0) < 0): false;

              if (topbit_sign)
                {
                  CONSTANTBV::BitVector_Fill(output);
                }
              CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, t0_width);
              OutputNode = _bm->CreateBVConst(output, outputwidth);
            }
          break;
        }

      case BVLEFTSHIFT:
      case BVRIGHTSHIFT:
      case BVSRSHIFT:
        {
          // load in the bitWidth.
          CBV width = CONSTANTBV::BitVector_Create(inputwidth, true);
          for (unsigned i = 0; i < sizeof(inputwidth) * 8; i++)
            if ((inputwidth & (0x1 << i)) != 0)
              CONSTANTBV::BitVector_Bit_On(width, i);

          output = CONSTANTBV::BitVector_Create(inputwidth, true);

          // Number of bits to shift it.
          ASTNode shiftNode = children[1];

          bool msb = CONSTANTBV::BitVector_msb_(tmp0);

          // If this shift is greater than the bitWidth, make it zero.
          if (CONSTANTBV::BitVector_Lexicompare(width, shiftNode.GetBVConst()) < 0)
            {
              if (k == BVSRSHIFT && msb)
                CONSTANTBV::Set_Complement(output, output);
            }
          else
            {
              // the shift is destructive, get a copy.
              CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, inputwidth);

              unsigned int shift = shiftNode.GetUnsignedConst();

              if (k == BVLEFTSHIFT)
                CONSTANTBV::BitVector_Move_Left(output, shift);
              else
                CONSTANTBV::BitVector_Move_Right(output, shift);

              if (k == BVSRSHIFT && msb)
                {
                  // signed shift, and the number was originally negative.
                  // Shift may be larger than the inputwidth.
                  for (unsigned 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 = _bm->CreateBVConst(output, outputwidth);

          CONSTANTBV::BitVector_Destroy(width);
          break;
        }


      case BVAND:
        {
          assert(2==t.Degree());
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          CONSTANTBV::Set_Intersection(output, tmp0, tmp1);
          OutputNode = _bm->CreateBVConst(output, outputwidth);
          break;
        }
      case BVOR:
        {
          assert(2==t.Degree());
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          CONSTANTBV::Set_Union(output, tmp0, tmp1);
          OutputNode = _bm->CreateBVConst(output, outputwidth);
          break;
        }
      case BVXOR:
        {
          assert(2==t.Degree());
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          CONSTANTBV::Set_ExclusiveOr(output, tmp0, tmp1);
          OutputNode = _bm->CreateBVConst(output, outputwidth);
          break;
        }
      case BVSUB:
        {
          assert(2==t.Degree());
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          bool carry = false;
          CONSTANTBV::BitVector_sub(output, tmp0, tmp1, &carry);
          OutputNode = _bm->CreateBVConst(output, outputwidth);
          break;
        }
      case BVUMINUS:
        {
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          CONSTANTBV::BitVector_Negate(output, tmp0);
          OutputNode = _bm->CreateBVConst(output, outputwidth);
          break;
        }
      case BVEXTRACT:
        {
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          tmp0 = children[0].GetBVConst();
          unsigned int hi = children[1].GetUnsignedConst();
          unsigned int low = children[2].GetUnsignedConst();
          unsigned int len = hi - low + 1;

          CONSTANTBV::BitVector_Destroy(output);
          output = CONSTANTBV::BitVector_Create(len, false);
          CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, low, len);
          outputwidth = len;
          OutputNode = _bm->CreateBVConst(output, outputwidth);
          break;
        }

      case BVCONCAT:
        {
          assert(2==t.Degree());
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          unsigned t0_width = children[0].GetValueWidth();
          unsigned t1_width = children[1].GetValueWidth();
          CONSTANTBV::BitVector_Destroy(output);

          output = CONSTANTBV::BitVector_Concat(tmp0, tmp1);
          outputwidth = t0_width + t1_width;
          OutputNode = _bm->CreateBVConst(output, outputwidth);

          break;
        }
      case BVMULT:
        {
        output = CONSTANTBV::BitVector_Create(inputwidth, true);
        CONSTANTBV::BitVector_increment(output);

        CBV tmp = CONSTANTBV::BitVector_Create(2 * inputwidth, true);

        for (ASTVec::iterator it = children.begin(), itend = children.end(); it != itend; it++)
          {
            CBV kk = (*it).GetBVConst();
            CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Multiply(tmp, output, kk);

            if (0 != e)
              {
                BVConstEvaluatorError(e, t);
              }
            CONSTANTBV::BitVector_Interval_Copy(output, tmp, 0, 0, inputwidth);

          }

        OutputNode = _bm->CreateBVConst(output, outputwidth);
        CONSTANTBV::BitVector_Destroy(tmp);
        break;
      }
      case BVPLUS:
        {
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          bool carry = false;
          for (ASTVec::iterator it = children.begin(), itend = children.end(); it != itend; it++)
            {
              CBV kk = (*it).GetBVConst();
              CONSTANTBV::BitVector_add(output, output, kk, &carry);
              carry = false;
            }
          OutputNode = _bm->CreateBVConst(output, outputwidth);
          break;
        }

        // 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:
        {
          assert(2==t.Degree());
          CBV quotient = CONSTANTBV::BitVector_Create(inputwidth, true);
          CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true);

          if (_bm->UserFlags.division_by_zero_returns_one_flag 
              && CONSTANTBV::BitVector_is_empty(tmp1))
            {
              // Expecting a division by zero. Just return one.
              OutputNode = _bm->CreateOneConst(outputwidth);
              CONSTANTBV::BitVector_Destroy(remainder);
              CONSTANTBV::BitVector_Destroy(quotient);
            }
          else
            {
              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 = _bm->CreateBVConst(quotient, outputwidth);
                  CONSTANTBV::BitVector_Destroy(remainder);
                }
              else
                {
                  OutputNode = _bm->CreateBVConst(remainder, outputwidth);
                  CONSTANTBV::BitVector_Destroy(quotient);

                }
            }
          break;
        }

      case SBVMOD:
        {
          assert(2==t.Degree());
          /* 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 (_bm->UserFlags.division_by_zero_returns_one_flag
              && CONSTANTBV::BitVector_is_empty(tmp1))
            {
              // Expecting a division by zero. Just return one.
              OutputNode = _bm->CreateOneConst(outputwidth);
              CONSTANTBV::BitVector_Destroy(remainder);
            }
          else
            {
              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 = _bm->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 = _bm->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 = _bm->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 = _bm->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:
        {
          assert(2==t.Degree());
          CBV quotient = CONSTANTBV::BitVector_Create(inputwidth, true);
          CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true);

          if (_bm->UserFlags.division_by_zero_returns_one_flag 
              && CONSTANTBV::BitVector_is_empty(tmp1))
            {
              // Expecting a division by zero. Just return one.
              OutputNode = _bm->CreateOneConst(outputwidth);
            }
          else
            {

              // tmp0 is dividend, tmp1 is the divisor All parameters
              //to BitVector_Div_Pos must be distinct unlike
              //BitVector_Divide FIXME the contents of the second
              //parameter to Div_Pos is destroyed As tmp0 is currently
              //the same as the copy belonging to an ASTNode t[0] this
              //must be copied.
              tmp0 = CONSTANTBV::BitVector_Clone(tmp0);
              CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1, remainder);
              CONSTANTBV::BitVector_Destroy(tmp0);

              if (0 != e)
                {
                  //error printing
                  if (_bm->counterexample_checking_during_refinement)
                    {
                      output = CONSTANTBV::BitVector_Create(inputwidth, true);
                      OutputNode = _bm->CreateBVConst(output, outputwidth);
                      _bm->bvdiv_exception_occured = true;

                      //  CONSTANTBV::BitVector_Destroy(output);
                      break;
                    }<commit_msg>Bugfix. Unsigned modulus of zero returned 1, it should return 0. <commit_after>// -*- c++ -*-
/********************************************************************
 * AUTHORS: <NAME>, <NAME>
 *
 * BEGIN DATE: November, 2005
 *
 * LICENSE: Please view LICENSE file in the home dir of this Program
 ********************************************************************/

#include <cassert>
#include "simplifier.h"

namespace BEEV
{

  //error printing
  static void BVConstEvaluatorError(CONSTANTBV::ErrCode e, const ASTNode& t)
  {
    std::string ss("BVConstEvaluator:");
    ss += (const char*) BitVector_Error(e);
    FatalError(ss.c_str(), t);
  }

// Const evaluator logical and arithmetic operations.
  ASTNode NonMemberBVConstEvaluator(const ASTNode& t)
  {
    if (t.isConstant())
	 	return t;

	ASTNode OutputNode;
    Kind k = t.GetKind();

    STPMgr* _bm = t.GetSTPMgr();
    ASTNode& ASTTrue = _bm->ASTTrue;
    ASTNode& ASTFalse = _bm->ASTFalse;

    OutputNode = t;

    unsigned int inputwidth = t.GetValueWidth();
    unsigned int outputwidth = inputwidth;
    CBV output = NULL;

    CBV tmp0 = NULL;
    CBV tmp1 = NULL;

    ASTVec children;
    children.reserve(t.Degree());
    for (int i =0; i < t.Degree(); i++)
    {
    	if (t[i].isConstant())
    		children.push_back(t[i]);
    	else
    		children.push_back(NonMemberBVConstEvaluator(t[i]));
    }

    if ((t.Degree() ==2 || t.Degree() == 1) && t[0].GetType() == BITVECTOR_TYPE)
    {
    //saving some typing. BVPLUS does not use these variables. if the
    //input BVPLUS has two nodes, then we want to avoid setting these
    //variables.
    if (1 == t.Degree())
      {
        tmp0 = children[0].GetBVConst();
      }
    else if (2 == t.Degree() && k != BVPLUS)
      {
        tmp0 = children[0].GetBVConst();
        tmp1 = children[1].GetBVConst();
      }
	}

    switch (k)
      {
      case UNDEFINED:
      case READ:
      case WRITE:
      case SYMBOL:
    	    FatalError("BVConstEvaluator: term is not a constant-term", t);
        break;
      case BVCONST:
        OutputNode = t;
        break;
      case BVNEG:
        {
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          CONSTANTBV::Set_Complement(output, tmp0);
          OutputNode = _bm->CreateBVConst(output, outputwidth);
          break;
        }
      case BVSX:
      case BVZX:
        {
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          unsigned t0_width = t[0].GetValueWidth();
          if (inputwidth == t0_width)
            {
              CONSTANTBV::BitVector_Copy(output, tmp0);
              OutputNode = _bm->CreateBVConst(output, outputwidth);
            }
          else
            {
              bool topbit_sign = (k == BVSX)?(CONSTANTBV::BitVector_Sign(tmp0) < 0): false;

              if (topbit_sign)
                {
                  CONSTANTBV::BitVector_Fill(output);
                }
              CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, t0_width);
              OutputNode = _bm->CreateBVConst(output, outputwidth);
            }
          break;
        }

      case BVLEFTSHIFT:
      case BVRIGHTSHIFT:
      case BVSRSHIFT:
        {
          // load in the bitWidth.
          CBV width = CONSTANTBV::BitVector_Create(inputwidth, true);
          for (unsigned i = 0; i < sizeof(inputwidth) * 8; i++)
            if ((inputwidth & (0x1 << i)) != 0)
              CONSTANTBV::BitVector_Bit_On(width, i);

          output = CONSTANTBV::BitVector_Create(inputwidth, true);

          // Number of bits to shift it.
          ASTNode shiftNode = children[1];

          bool msb = CONSTANTBV::BitVector_msb_(tmp0);

          // If this shift is greater than the bitWidth, make it zero.
          if (CONSTANTBV::BitVector_Lexicompare(width, shiftNode.GetBVConst()) < 0)
            {
              if (k == BVSRSHIFT && msb)
                CONSTANTBV::Set_Complement(output, output);
            }
          else
            {
              // the shift is destructive, get a copy.
              CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, inputwidth);

              unsigned int shift = shiftNode.GetUnsignedConst();

              if (k == BVLEFTSHIFT)
                CONSTANTBV::BitVector_Move_Left(output, shift);
              else
                CONSTANTBV::BitVector_Move_Right(output, shift);

              if (k == BVSRSHIFT && msb)
                {
                  // signed shift, and the number was originally negative.
                  // Shift may be larger than the inputwidth.
                  for (unsigned 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 = _bm->CreateBVConst(output, outputwidth);

          CONSTANTBV::BitVector_Destroy(width);
          break;
        }


      case BVAND:
        {
          assert(2==t.Degree());
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          CONSTANTBV::Set_Intersection(output, tmp0, tmp1);
          OutputNode = _bm->CreateBVConst(output, outputwidth);
          break;
        }
      case BVOR:
        {
          assert(2==t.Degree());
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          CONSTANTBV::Set_Union(output, tmp0, tmp1);
          OutputNode = _bm->CreateBVConst(output, outputwidth);
          break;
        }
      case BVXOR:
        {
          assert(2==t.Degree());
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          CONSTANTBV::Set_ExclusiveOr(output, tmp0, tmp1);
          OutputNode = _bm->CreateBVConst(output, outputwidth);
          break;
        }
      case BVSUB:
        {
          assert(2==t.Degree());
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          bool carry = false;
          CONSTANTBV::BitVector_sub(output, tmp0, tmp1, &carry);
          OutputNode = _bm->CreateBVConst(output, outputwidth);
          break;
        }
      case BVUMINUS:
        {
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          CONSTANTBV::BitVector_Negate(output, tmp0);
          OutputNode = _bm->CreateBVConst(output, outputwidth);
          break;
        }
      case BVEXTRACT:
        {
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          tmp0 = children[0].GetBVConst();
          unsigned int hi = children[1].GetUnsignedConst();
          unsigned int low = children[2].GetUnsignedConst();
          unsigned int len = hi - low + 1;

          CONSTANTBV::BitVector_Destroy(output);
          output = CONSTANTBV::BitVector_Create(len, false);
          CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, low, len);
          outputwidth = len;
          OutputNode = _bm->CreateBVConst(output, outputwidth);
          break;
        }

      case BVCONCAT:
        {
          assert(2==t.Degree());
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          unsigned t0_width = children[0].GetValueWidth();
          unsigned t1_width = children[1].GetValueWidth();
          CONSTANTBV::BitVector_Destroy(output);

          output = CONSTANTBV::BitVector_Concat(tmp0, tmp1);
          outputwidth = t0_width + t1_width;
          OutputNode = _bm->CreateBVConst(output, outputwidth);

          break;
        }
      case BVMULT:
        {
        output = CONSTANTBV::BitVector_Create(inputwidth, true);
        CONSTANTBV::BitVector_increment(output);

        CBV tmp = CONSTANTBV::BitVector_Create(2 * inputwidth, true);

        for (ASTVec::iterator it = children.begin(), itend = children.end(); it != itend; it++)
          {
            CBV kk = (*it).GetBVConst();
            CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Multiply(tmp, output, kk);

            if (0 != e)
              {
                BVConstEvaluatorError(e, t);
              }
            CONSTANTBV::BitVector_Interval_Copy(output, tmp, 0, 0, inputwidth);

          }

        OutputNode = _bm->CreateBVConst(output, outputwidth);
        CONSTANTBV::BitVector_Destroy(tmp);
        break;
      }
      case BVPLUS:
        {
          output = CONSTANTBV::BitVector_Create(inputwidth, true);
          bool carry = false;
          for (ASTVec::iterator it = children.begin(), itend = children.end(); it != itend; it++)
            {
              CBV kk = (*it).GetBVConst();
              CONSTANTBV::BitVector_add(output, output, kk, &carry);
              carry = false;
            }
          OutputNode = _bm->CreateBVConst(output, outputwidth);
          break;
        }

        // 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:
        {
          assert(2==t.Degree());
          CBV quotient = CONSTANTBV::BitVector_Create(inputwidth, true);
          CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true);

          if (_bm->UserFlags.division_by_zero_returns_one_flag 
              && CONSTANTBV::BitVector_is_empty(tmp1))
            {
              // Expecting a division by zero. Just return one.
              OutputNode = _bm->CreateOneConst(outputwidth);
              CONSTANTBV::BitVector_Destroy(remainder);
              CONSTANTBV::BitVector_Destroy(quotient);
            }
          else
            {
              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 = _bm->CreateBVConst(quotient, outputwidth);
                  CONSTANTBV::BitVector_Destroy(remainder);
                }
              else
                {
                  OutputNode = _bm->CreateBVConst(remainder, outputwidth);
                  CONSTANTBV::BitVector_Destroy(quotient);

                }
            }
          break;
        }

      case SBVMOD:
        {
          assert(2==t.Degree());
          /* 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 (_bm->UserFlags.division_by_zero_returns_one_flag
              && CONSTANTBV::BitVector_is_empty(tmp1))
            {
              // Expecting a division by zero. Just return one.
              OutputNode = _bm->CreateOneConst(outputwidth);
              CONSTANTBV::BitVector_Destroy(remainder);
            }
          else
            {
              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 = _bm->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 = _bm->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 = _bm->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 = _bm->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:
        {
          assert(2==t.Degree());
          CBV quotient = CONSTANTBV::BitVector_Create(inputwidth, true);
          CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true);

          if (_bm->UserFlags.division_by_zero_returns_one_flag 
              && CONSTANTBV::BitVector_is_empty(tmp1))
            {
              // a = bq + r, where b!=0 implies r < b. q is quotient, r remainder. i.e. a/b = q.
              // It doesn't matter what q is when b=0, but r needs to be 0.
              if (k == BVMOD)
                OutputNode = _bm->CreateZeroConst(outputwidth);
              else
                OutputNode = _bm->CreateOneConst(outputwidth);
                // Expecting a division by zero. Just return one.

            }
          else
            {

              // tmp0 is dividend, tmp1 is the divisor All parameters
              //to BitVector_Div_Pos must be distinct unlike
              //BitVector_Divide FIXME the contents of the second
              //parameter to Div_Pos is destroyed As tmp0 is currently
              //the same as the copy belonging to an ASTNode t[0] this
              //must be copied.
              tmp0 = CONSTANTBV::BitVector_Clone(tmp0);
              CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1, remainder);
              CONSTANTBV::BitVector_Destroy(tmp0);

              if (0 != e)
                {
                  //error printing
                  if (_bm->counterexample_checking_during_refinement)
                    {
                      output = CONSTANTBV::BitVector_Create(inputwidth, true);
                      OutputNode = _bm->CreateBVConst(output, outputwidth);
                      _bm->bvdiv_exception_occured = true;

                      //  CONSTANTBV::BitVector_Destroy(output);
                      break;
                    }
{'fraction_non_alphanumeric': 0.11350819861765811, 'fraction_numerical': 0.008762543740420486, 'mean_word_length': 1.7644096250699497, 'pattern_counts': {'":': 0, '<': 44, '<?xml version=': 0, '>': 70, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3839761', 'n_tokens_mistral': 10829, 'n_tokens_neox': 9806, 'n_words': 2075}