Skip to content

Commit

Permalink
Merge branch 'main' of https://github.com/ajreynol/AletheLF-tc
Browse files Browse the repository at this point in the history
  • Loading branch information
@ajreynol
ajreynol committed Nov 20, 2023
2 parents fa23955 + 9fd829d commit ca4c815
Show file tree
Hide file tree
Showing 11 changed files with 20 additions and 424 deletions.
3 changes: 3 additions & 0 deletions src/kind.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,7 @@ std::ostream& operator<<(std::ostream& o, Kind k)
case Kind::EVAL_NEG: o << "EVAL_NEG"; break;
case Kind::EVAL_MUL: o << "EVAL_MUL"; break;
case Kind::EVAL_INT_DIV: o << "EVAL_INT_DIV"; break;
case Kind::EVAL_INT_MOD: o << "EVAL_INT_MOD"; break;
case Kind::EVAL_RAT_DIV: o << "EVAL_RAT_DIV"; break;
case Kind::EVAL_IS_NEG: o << "EVAL_IS_NEG"; break;
// strings
Expand Down Expand Up @@ -113,6 +114,7 @@ std::string kindToTerm(Kind k)
case Kind::EVAL_NEG: ss << "neg";break;
case Kind::EVAL_MUL: ss << "mul";break;
case Kind::EVAL_INT_DIV: ss << "zdiv";break;
case Kind::EVAL_INT_MOD: ss << "zmod";break;
case Kind::EVAL_RAT_DIV: ss << "qdiv";break;
case Kind::EVAL_IS_NEG: ss << "is_neg";break;
// strings
Expand Down Expand Up @@ -188,6 +190,7 @@ bool isLiteralOp(Kind k)
case Kind::EVAL_NEG:
case Kind::EVAL_MUL:
case Kind::EVAL_INT_DIV:
case Kind::EVAL_INT_MOD:
case Kind::EVAL_RAT_DIV:
case Kind::EVAL_IS_NEG:
// strings
Expand Down
1 change: 1 addition & 0 deletions src/kind.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,7 @@ enum class Kind
EVAL_NEG,
EVAL_MUL,
EVAL_INT_DIV,
EVAL_INT_MOD,
EVAL_RAT_DIV,
EVAL_IS_NEG,
// strings
Expand Down
8 changes: 6 additions & 2 deletions src/literal.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -259,15 +259,18 @@ Literal Literal::evaluate(Kind k, const std::vector<const Literal*>& args)
}
break;
case Kind::EVAL_INT_DIV:
case Kind::EVAL_INT_MOD:
{
bool isDiv = (k==Kind::EVAL_INT_DIV);
switch (ka)
{
case Kind::NUMERAL:
{
const Integer& d = args[1]->d_int;
if (d.sgn()!=0)
{
return Literal(Integer(args[0]->d_int.euclidianDivideQuotient(d)));
return Literal(isDiv ? args[0]->d_int.euclidianDivideQuotient(d) :
args[0]->d_int.euclidianDivideRemainder(d));
}
}
break;
Expand All @@ -277,7 +280,8 @@ Literal Literal::evaluate(Kind k, const std::vector<const Literal*>& args)
{
return Literal();
}
return Literal(ka, BitVector(args[0]->d_bv.unsignedDivTotal(args[1]->d_bv)));
return Literal(ka, isDiv ? args[0]->d_bv.unsignedDivTotal(args[1]->d_bv) :
args[0]->d_bv.unsignedRemTotal(args[1]->d_bv));
break;
default: break;
}
Expand Down
1 change: 1 addition & 0 deletions src/state.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,7 @@ State::State(Options& opts, Stats& stats)
bindBuiltinEval("neg", Kind::EVAL_NEG);
bindBuiltinEval("mul", Kind::EVAL_MUL);
bindBuiltinEval("zdiv", Kind::EVAL_INT_DIV);
bindBuiltinEval("zmod", Kind::EVAL_INT_MOD);
bindBuiltinEval("qdiv", Kind::EVAL_RAT_DIV);
bindBuiltinEval("is_neg", Kind::EVAL_IS_NEG);
bindBuiltinEval("to_z", Kind::EVAL_TO_INT);
Expand Down
2 changes: 2 additions & 0 deletions src/type_checker.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -151,6 +151,7 @@ bool TypeChecker::checkArity(Kind k, size_t nargs, std::ostream* out)
break;
case Kind::EVAL_IS_EQ:
case Kind::EVAL_INT_DIV:
case Kind::EVAL_INT_MOD:
case Kind::EVAL_RAT_DIV:
case Kind::EVAL_TO_BV:
case Kind::EVAL_FIND:
Expand Down Expand Up @@ -1274,6 +1275,7 @@ ExprValue* TypeChecker::getLiteralOpType(Kind k,
return d_state.mkBoolType().getValue();
case Kind::EVAL_HASH:
case Kind::EVAL_INT_DIV:
case Kind::EVAL_INT_MOD:
case Kind::EVAL_TO_INT:
case Kind::EVAL_LENGTH:
case Kind::EVAL_FIND:
Expand Down
174 changes: 0 additions & 174 deletions src/util/bitvector.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,15 +25,6 @@ const Integer& BitVector::getValue() const { return d_value; }

Integer BitVector::toInteger() const { return d_value; }

Integer BitVector::toSignedInteger() const
{
unsigned size = d_size;
Integer sign_bit = d_value.extractBitRange(1, size - 1);
Integer val = d_value.extractBitRange(size - 1, 0);
Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
return res;
}

std::string BitVector::toString(unsigned int base) const
{
std::string str = d_value.toString(base);
Expand All @@ -57,24 +48,6 @@ size_t BitVector::hash() const
return std::hash<size_t>()(d_value.hash()) ^ std::hash<size_t>()(d_size);
}

BitVector& BitVector::setBit(uint32_t i, bool value)
{
Assert(i < d_size);
d_value.setBit(i, value);
return *this;
}

bool BitVector::isBitSet(uint32_t i) const
{
Assert(i < d_size);
return d_value.isBitSet(i);
}

unsigned BitVector::isPow2() const
{
return d_value.isPow2();
}

/* -----------------------------------------------------------------------
* Operators
* ----------------------------------------------------------------------- */
Expand Down Expand Up @@ -103,30 +76,6 @@ bool operator==(const BitVector& a, const BitVector& b)
return a.getValue() == b.getValue();
}

/* Signed Inequality ----------------------------------------------------- */

bool BitVector::signedLessThan(const BitVector& y) const
{
Assert(d_size == y.d_size);
Assert(d_value.sgn()>=0);
Assert(y.d_value.sgn() >= 0);
Integer a = (*this).toSignedInteger();
Integer b = y.toSignedInteger();

return b > a;
}

bool BitVector::signedLessThanEq(const BitVector& y) const
{
Assert(d_size == y.d_size);
Assert(d_value.sgn() >= 0);
Assert(y.d_value.sgn() >= 0);
Integer a = (*this).toSignedInteger();
Integer b = y.toSignedInteger();

return b >= a;
}

/* Bit-wise operations --------------------------------------------------- */

BitVector operator^(const BitVector& a, const BitVector& b)
Expand Down Expand Up @@ -199,127 +148,4 @@ BitVector BitVector::unsignedRemTotal(const BitVector& y) const
return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
}

/* Extend operations ----------------------------------------------------- */

BitVector BitVector::zeroExtend(unsigned n) const
{
return BitVector(d_size + n, d_value);
}

BitVector BitVector::signExtend(unsigned n) const
{
Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
if (sign_bit == Integer("0"))
{
return BitVector(d_size + n, d_value);
}
Integer val = d_value.oneExtend(d_size, n);
return BitVector(d_size + n, val);
}

/* Shift operations ------------------------------------------------------ */

BitVector BitVector::leftShift(const BitVector& y) const
{
Integer zero("0");
if (y.d_value > Integer(d_size))
{
return BitVector(d_size, zero);
}
if (y.d_value == zero)
{
return *this;
}
// making sure we don't lose information casting
//Assert(y.d_value < Integer(1).multiplyByPow2(32));
uint32_t amount = y.d_value.toUnsignedInt();
Integer res = d_value.multiplyByPow2(amount);
return BitVector(d_size, res);
}

BitVector BitVector::logicalRightShift(const BitVector& y) const
{
Integer zero(0);
if (y.d_value > Integer(d_size))
{
return BitVector(d_size, zero);
}
// making sure we don't lose information casting
//Assert(y.d_value < Integer(1).multiplyByPow2(32));
uint32_t amount = y.d_value.toUnsignedInt();
Integer res = d_value.divByPow2(amount);
return BitVector(d_size, res);
}

BitVector BitVector::arithRightShift(const BitVector& y) const
{
Integer zero(0);
Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
if (y.d_value > Integer(d_size))
{
if (sign_bit == zero)
{
return BitVector(d_size, zero);
}
else
{
return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size)+(-Integer(1)));
}
}

if (y.d_value == zero)
{
return *this;
}

// making sure we don't lose information casting
//Assert(y.d_value < Integer(1).multiplyByPow2(32));

uint32_t amount = y.d_value.toUnsignedInt();
Integer rest = d_value.divByPow2(amount);

if (sign_bit == Integer(0))
{
return BitVector(d_size, rest);
}
Integer res = rest.oneExtend(d_size - amount, amount);
return BitVector(d_size, res);
}

/* -----------------------------------------------------------------------
* Static helpers.
* ----------------------------------------------------------------------- */

BitVector BitVector::mkZero(unsigned size)
{
Assert(size > 0);
return BitVector(size);
}

BitVector BitVector::mkOne(unsigned size)
{
Assert(size > 0);
return BitVector(size, 1u);
}

BitVector BitVector::mkOnes(unsigned size)
{
Assert(size > 0);
return BitVector(1, Integer(1)).signExtend(size - 1);
}

BitVector BitVector::mkMinSigned(unsigned size)
{
Assert(size > 0);
BitVector res(size);
res.setBit(size - 1, true);
return res;
}

BitVector BitVector::mkMaxSigned(unsigned size)
{
Assert(size > 0);
return ~BitVector::mkMinSigned(size);
}

} // namespace cvc5::internal
65 changes: 0 additions & 65 deletions src/util/bitvector.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,27 +81,10 @@ class BitVector

/* Return value. */
Integer toInteger() const;
/* Return Integer corresponding to two's complement interpretation of this. */
Integer toSignedInteger() const;
/* Return (binary) string representation. */
std::string toString(unsigned int base = 2) const;
/* Return hash value. */
size_t hash() const;
/**
* Set bit at index 'i' to given value.
* Returns a reference to this bit-vector to allow for chaining.
*
* value: True to set bit to 1, and false to set it to 0.
*
* Note: Least significant bit is at index 0.
*/
BitVector& setBit(uint32_t i, bool value);

/** Return true if bit at index 'i' is 1, and false otherwise. */
bool isBitSet(uint32_t i) const;

/* Return k if the value of this is equal to 2^{k-1}, and zero otherwise. */
unsigned isPow2() const;

/* -----------------------------------------------------------------------
** Operators
Expand All @@ -115,14 +98,6 @@ class BitVector
/* Return the bit range from index 'high' to index 'low'. */
BitVector extract(unsigned high, unsigned low) const;

/* Signed Inequality ----------------------------------------------------- */

/* Return true if this is signed less than bit-vector 'y'. */
bool signedLessThan(const BitVector& y) const;

/* Return true if this is signed less than or equal to bit-vector 'y'. */
bool signedLessThanEq(const BitVector& y) const;

/* Arithmetic operations ------------------------------------------------- */

/* Total division function.
Expand All @@ -136,46 +111,6 @@ class BitVector
* (this % y), otherwise. */
BitVector unsignedRemTotal(const BitVector& y) const;

/* Extend operations ----------------------------------------------------- */

/* Return a bit-vector representing this extended by 'n' zero bits. */
BitVector zeroExtend(unsigned n) const;

/* Return a bit-vector representing this extended by 'n' bits of the value
* of the signed bit. */
BitVector signExtend(unsigned n) const;

/* Shift operations ------------------------------------------------------ */

/* Return a bit-vector representing a left shift of this by 'y'. */
BitVector leftShift(const BitVector& y) const;

/* Return a bit-vector representing a logical right shift of this by 'y'. */
BitVector logicalRightShift(const BitVector& y) const;

/* Return a bit-vector representing an arithmetic right shift of this
* by 'y'.*/
BitVector arithRightShift(const BitVector& y) const;

/* -----------------------------------------------------------------------
** Static helpers.
* ----------------------------------------------------------------------- */

/* Create zero bit-vector of given size. */
static BitVector mkZero(unsigned size);

/* Create bit-vector representing value 1 of given size. */
static BitVector mkOne(unsigned size);

/* Create bit-vector of ones of given size. */
static BitVector mkOnes(unsigned size);

/* Create bit-vector representing the minimum signed value of given size. */
static BitVector mkMinSigned(unsigned size);

/* Create bit-vector representing the maximum signed value of given size. */
static BitVector mkMaxSigned(unsigned size);

private:
/**
* Class invariants:
Expand Down
Loading

0 comments on commit ca4c815

Please sign in to comment.