This PR adds more getter functions for api::Term to retrieve values from constant terms (and terms that the average API use might consider constant).
It also introduces std::wstring as regular representation for string constants instead of std::vector<uint32> for the SMT-LIB parser and the String class.
CVC5_API_TRY_CATCH_END;
}
-Term Term::getConstArrayBase() const
-{
- NodeManagerScope scope(d_solver->getNodeManager());
- CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK_NOT_NULL;
- // CONST_ARRAY kind maps to STORE_ALL internal kind
- CVC5_API_CHECK(d_node->getKind() == cvc5::Kind::STORE_ALL)
- << "Expecting a CONST_ARRAY Term when calling getConstArrayBase()";
- //////// all checks before this line
- return Term(d_solver, d_node->getConst<ArrayStoreAll>().getValue());
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
std::vector<Term> Term::getConstSequenceElements() const
{
CVC5_API_TRY_CATCH_BEGIN;
namespace detail {
const Rational& getRational(const cvc5::Node& node)
{
- return node.getConst<Rational>();
+ switch (node.getKind())
+ {
+ case cvc5::Kind::CAST_TO_REAL: return node[0].getConst<Rational>();
+ case cvc5::Kind::CONST_RATIONAL: return node.getConst<Rational>();
+ default:
+ CVC5_API_CHECK(false) << "Node is not a rational.";
+ return node.getConst<Rational>();
+ }
}
Integer getInteger(const cvc5::Node& node)
{
&& checkIntegerBounds<std::uint64_t>(r.getDenominator());
}
+bool isReal(const Node& node)
+{
+ return node.getKind() == cvc5::Kind::CONST_RATIONAL
+ || node.getKind() == cvc5::Kind::CAST_TO_REAL;
+}
+bool isReal32(const Node& node)
+{
+ return isReal(node) && checkReal32Bounds(getRational(node));
+}
+bool isReal64(const Node& node)
+{
+ return isReal(node) && checkReal64Bounds(getRational(node));
+}
+
bool isInteger(const Node& node)
{
return node.getKind() == cvc5::Kind::CONST_RATIONAL
}
} // namespace detail
-bool Term::isInt32() const
+bool Term::isInt32Value() const
{
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_CHECK_NOT_NULL;
CVC5_API_TRY_CATCH_END;
}
-std::int32_t Term::getInt32() const
+std::int32_t Term::getInt32Value() const
{
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_CHECK_NOT_NULL;
- CVC5_API_CHECK(detail::isInt32(*d_node))
- << "Term should be a Int32 when calling getInt32()";
+ CVC5_API_ARG_CHECK_EXPECTED(detail::isInt32(*d_node), *d_node)
+ << "Term to be a 32-bit integer value when calling getInt32Value()";
//////// all checks before this line
return detail::getInteger(*d_node).getSignedInt();
////////
CVC5_API_TRY_CATCH_END;
}
-bool Term::isUInt32() const { return detail::isUInt32(*d_node); }
-std::uint32_t Term::getUInt32() const
+bool Term::isUInt32Value() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ return detail::isUInt32(*d_node);
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+std::uint32_t Term::getUInt32Value() const
{
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_CHECK_NOT_NULL;
- CVC5_API_CHECK(detail::isUInt32(*d_node))
- << "Term should be a UInt32 when calling getUInt32()";
+ CVC5_API_ARG_CHECK_EXPECTED(detail::isUInt32(*d_node), *d_node)
+ << "Term to be a unsigned 32-bit integer value when calling "
+ "getUInt32Value()";
//////// all checks before this line
return detail::getInteger(*d_node).getUnsignedInt();
////////
CVC5_API_TRY_CATCH_END;
}
-bool Term::isInt64() const { return detail::isInt64(*d_node); }
-std::int64_t Term::getInt64() const
+bool Term::isInt64Value() const
{
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_CHECK_NOT_NULL;
- CVC5_API_CHECK(detail::isInt64(*d_node))
- << "Term should be a Int64 when calling getInt64()";
+ //////// all checks before this line
+ return detail::isInt64(*d_node);
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+std::int64_t Term::getInt64Value() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ CVC5_API_ARG_CHECK_EXPECTED(detail::isInt64(*d_node), *d_node)
+ << "Term to be a 64-bit integer value when calling getInt64Value()";
//////// all checks before this line
return detail::getInteger(*d_node).getLong();
////////
CVC5_API_TRY_CATCH_END;
}
-bool Term::isUInt64() const
+bool Term::isUInt64Value() const
{
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_CHECK_NOT_NULL;
CVC5_API_TRY_CATCH_END;
}
-std::uint64_t Term::getUInt64() const
+std::uint64_t Term::getUInt64Value() const
{
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_CHECK_NOT_NULL;
- CVC5_API_CHECK(detail::isUInt64(*d_node))
- << "Term should be a UInt64 when calling getUInt64()";
+ CVC5_API_ARG_CHECK_EXPECTED(detail::isUInt64(*d_node), *d_node)
+ << "Term to be a unsigned 64-bit integer value when calling "
+ "getUInt64Value()";
//////// all checks before this line
return detail::getInteger(*d_node).getUnsignedLong();
////////
CVC5_API_TRY_CATCH_END;
}
-bool Term::isInteger() const { return detail::isInteger(*d_node); }
-std::string Term::getInteger() const
+bool Term::isIntegerValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ return detail::isInteger(*d_node);
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+std::string Term::getIntegerValue() const
{
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_CHECK_NOT_NULL;
- CVC5_API_CHECK(detail::isInteger(*d_node))
- << "Term should be an Int when calling getIntString()";
+ CVC5_API_ARG_CHECK_EXPECTED(detail::isInteger(*d_node), *d_node)
+ << "Term to be an integer value when calling getIntegerValue()";
//////// all checks before this line
return detail::getInteger(*d_node).toString();
////////
CVC5_API_TRY_CATCH_END;
}
-bool Term::isString() const
+bool Term::isStringValue() const
{
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_CHECK_NOT_NULL;
CVC5_API_TRY_CATCH_END;
}
-std::wstring Term::getString() const
+std::wstring Term::getStringValue() const
{
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_CHECK_NOT_NULL;
- CVC5_API_CHECK(d_node->getKind() == cvc5::Kind::CONST_STRING)
- << "Term should be a String when calling getString()";
+ CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::CONST_STRING,
+ *d_node)
+ << "Term to be a string value when calling getStringValue()";
//////// all checks before this line
return d_node->getConst<cvc5::String>().toWString();
////////
return res;
}
+bool Term::isReal32Value() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ return detail::isReal32(*d_node);
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+std::pair<std::int32_t, std::uint32_t> Term::getReal32Value() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ CVC5_API_ARG_CHECK_EXPECTED(detail::isReal32(*d_node), *d_node)
+ << "Term to be a 32-bit rational value when calling getReal32Value()";
+ //////// all checks before this line
+ const Rational& r = detail::getRational(*d_node);
+ return std::make_pair(r.getNumerator().getSignedInt(),
+ r.getDenominator().getUnsignedInt());
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+bool Term::isReal64Value() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ return detail::isReal64(*d_node);
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+std::pair<std::int64_t, std::uint64_t> Term::getReal64Value() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ CVC5_API_ARG_CHECK_EXPECTED(detail::isReal64(*d_node), *d_node)
+ << "Term to be a 64-bit rational value when calling getReal64Value()";
+ //////// all checks before this line
+ const Rational& r = detail::getRational(*d_node);
+ return std::make_pair(r.getNumerator().getLong(),
+ r.getDenominator().getUnsignedLong());
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+bool Term::isRealValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ return detail::isReal(*d_node);
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+std::string Term::getRealValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ CVC5_API_ARG_CHECK_EXPECTED(detail::isReal(*d_node), *d_node)
+ << "Term to be a rational value when calling getRealValue()";
+ //////// all checks before this line
+ return detail::getRational(*d_node).toString();
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
+bool Term::isConstArray() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ return d_node->getKind() == cvc5::Kind::STORE_ALL;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+Term Term::getConstArrayBase() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::STORE_ALL,
+ *d_node)
+ << "Term to be a constant array when calling getConstArrayBase()";
+ //////// all checks before this line
+ const auto& ar = d_node->getConst<ArrayStoreAll>();
+ return Term(d_solver, ar.getValue());
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
+bool Term::isBooleanValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ return d_node->getKind() == cvc5::Kind::CONST_BOOLEAN;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+bool Term::getBooleanValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::CONST_BOOLEAN,
+ *d_node)
+ << "Term to be a Boolean value when calling getBooleanValue()";
+ //////// all checks before this line
+ return d_node->getConst<bool>();
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
+bool Term::isBitVectorValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ return d_node->getKind() == cvc5::Kind::CONST_BITVECTOR;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+std::string Term::getBitVectorValue(std::uint32_t base) const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::CONST_BITVECTOR,
+ *d_node)
+ << "Term to be a bit-vector value when calling getBitVectorValue()";
+ //////// all checks before this line
+ return d_node->getConst<BitVector>().toString(base);
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
+bool Term::isAbstractValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ return d_node->getKind() == cvc5::Kind::ABSTRACT_VALUE;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+std::string Term::getAbstractValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::ABSTRACT_VALUE,
+ *d_node)
+ << "Term to be an abstract value when calling "
+ "getAbstractValue()";
+ //////// all checks before this line
+ return d_node->getConst<AbstractValue>().getIndex().toString();
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
+bool Term::isTupleValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ return d_node->getKind() == cvc5::Kind::APPLY_CONSTRUCTOR && d_node->isConst()
+ && d_node->getType().getDType().isTuple();
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+std::vector<Term> Term::getTupleValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::APPLY_CONSTRUCTOR
+ && d_node->isConst()
+ && d_node->getType().getDType().isTuple(),
+ *d_node)
+ << "Term to be a tuple value when calling getTupleValue()";
+ //////// all checks before this line
+ std::vector<Term> res;
+ for (size_t i = 0, n = d_node->getNumChildren(); i < n; ++i)
+ {
+ res.emplace_back(Term(d_solver, (*d_node)[i]));
+ }
+ return res;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
+bool Term::isFloatingPointPosZero() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ if (d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT)
+ {
+ const auto& fp = d_node->getConst<FloatingPoint>();
+ return fp.isZero() && fp.isPositive();
+ }
+ return false;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+bool Term::isFloatingPointNegZero() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ if (d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT)
+ {
+ const auto& fp = d_node->getConst<FloatingPoint>();
+ return fp.isZero() && fp.isNegative();
+ }
+ return false;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+bool Term::isFloatingPointPosInf() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ if (d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT)
+ {
+ const auto& fp = d_node->getConst<FloatingPoint>();
+ return fp.isInfinite() && fp.isPositive();
+ }
+ return false;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+bool Term::isFloatingPointNegInf() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ if (d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT)
+ {
+ const auto& fp = d_node->getConst<FloatingPoint>();
+ return fp.isInfinite() && fp.isNegative();
+ }
+ return false;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+bool Term::isFloatingPointNaN() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ return d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
+ && d_node->getConst<FloatingPoint>().isNaN();
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+bool Term::isFloatingPointValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ return d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+std::tuple<std::uint32_t, std::uint32_t, Term> Term::getFloatingPointValue()
+ const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ CVC5_API_ARG_CHECK_EXPECTED(
+ d_node->getKind() == cvc5::Kind::CONST_FLOATINGPOINT, *d_node)
+ << "Term to be a floating-point value when calling "
+ "getFloatingPointValue()";
+ //////// all checks before this line
+ const auto& fp = d_node->getConst<FloatingPoint>();
+ return std::make_tuple(fp.getSize().exponentWidth(),
+ fp.getSize().significandWidth(),
+ d_solver->mkValHelper<BitVector>(fp.pack()));
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
+bool Term::isSetValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ return d_node->getType().isSet() && d_node->isConst();
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
+void Term::collectSet(std::set<Term>& set,
+ const cvc5::Node& node,
+ const Solver* slv)
+{
+ // We asserted that node has a set type, and node.isConst()
+ // Thus, node only contains of EMPTYSET, UNION and SINGLETON.
+ switch (node.getKind())
+ {
+ case cvc5::Kind::EMPTYSET: break;
+ case cvc5::Kind::SINGLETON: set.emplace(Term(slv, node[0])); break;
+ case cvc5::Kind::UNION:
+ {
+ for (const auto& sub : node)
+ {
+ collectSet(set, sub, slv);
+ }
+ break;
+ }
+ default:
+ CVC5_API_ARG_CHECK_EXPECTED(false, node)
+ << "Term to be a set value when calling getSetValue()";
+ break;
+ }
+}
+
+std::set<Term> Term::getSetValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ CVC5_API_ARG_CHECK_EXPECTED(d_node->getType().isSet() && d_node->isConst(),
+ *d_node)
+ << "Term to be a set value when calling getSetValue()";
+ //////// all checks before this line
+ std::set<Term> res;
+ Term::collectSet(res, *d_node, d_solver);
+ return res;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
+bool Term::isSequenceValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ return d_node->getKind() == cvc5::Kind::CONST_SEQUENCE;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+std::vector<Term> Term::getSequenceValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::CONST_SEQUENCE,
+ *d_node)
+ << "Term to be a sequence value when calling getSequenceValue()";
+ //////// all checks before this line
+ std::vector<Term> res;
+ const Sequence& seq = d_node->getConst<Sequence>();
+ for (const auto& node: seq.getVec())
+ {
+ res.emplace_back(Term(d_solver, node));
+ }
+ return res;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
+bool Term::isUninterpretedValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ //////// all checks before this line
+ return d_node->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+std::pair<Sort, std::int32_t> Term::getUninterpretedValue() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK_NOT_NULL;
+ CVC5_API_ARG_CHECK_EXPECTED(
+ d_node->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT, *d_node)
+ << "Term to be an uninterpreted value when calling "
+ "getUninterpretedValue()";
+ //////// all checks before this line
+ const auto& uc = d_node->getConst<UninterpretedConstant>();
+ return std::make_pair(Sort(d_solver, uc.getType()),
+ uc.getIndex().toUnsignedInt());
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
std::ostream& operator<<(std::ostream& out, const Term& t)
{
out << t.toString();
return mkValHelper<cvc5::BitVector>(cvc5::BitVector(size, val));
}
-Term Solver::mkCharFromStrHelper(const std::string& s) const
-{
- CVC5_API_CHECK(s.find_first_not_of("0123456789abcdefABCDEF", 0)
- == std::string::npos
- && s.size() <= 5 && s.size() > 0)
- << "Unexpected string for hexadecimal character " << s;
- uint32_t val = static_cast<uint32_t>(std::stoul(s, 0, 16));
- CVC5_API_CHECK(val < String::num_codes())
- << "Not a valid code point for hexadecimal character " << s;
- //////// all checks before this line
- std::vector<unsigned> cpts;
- cpts.push_back(val);
- return mkValHelper<cvc5::String>(cvc5::String(cpts));
-}
-
Term Solver::getValueHelper(const Term& term) const
{
// Note: Term is checked in the caller to avoid double checks
CVC5_API_TRY_CATCH_END;
}
-Term Solver::mkString(const unsigned char c) const
-{
- NodeManagerScope scope(getNodeManager());
- CVC5_API_TRY_CATCH_BEGIN;
- //////// all checks before this line
- return mkValHelper<cvc5::String>(cvc5::String(std::string(1, c)));
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
-Term Solver::mkString(const std::vector<uint32_t>& s) const
+Term Solver::mkString(const std::wstring& s) const
{
NodeManagerScope scope(getNodeManager());
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_TRY_CATCH_END;
}
-Term Solver::mkChar(const std::string& s) const
-{
- NodeManagerScope scope(getNodeManager());
- CVC5_API_TRY_CATCH_BEGIN;
- //////// all checks before this line
- return mkCharFromStrHelper(s);
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
Term Solver::mkEmptySequence(const Sort& sort) const
{
NodeManagerScope scope(getNodeManager());
*/
bool isNull() const;
- /**
- * Return the base (element stored at all indices) of a constant array
- * throws an exception if the kind is not CONST_ARRAY
- * @return the base value
- */
- Term getConstArrayBase() const;
-
/**
* Return the elements of a constant sequence
* throws an exception if the kind is not CONST_SEQUENCE
const_iterator end() const;
/**
- * @return true if the term is an integer that fits within std::int32_t.
+ * @return true if the term is an integer value that fits within int32_t.
*/
- bool isInt32() const;
+ bool isInt32Value() const;
/**
- * @return the stored integer as a std::int32_t.
- * Note: Asserts isInt32().
+ * Asserts isInt32Value().
+ * @return the integer term as a int32_t.
*/
- std::int32_t getInt32() const;
+ int32_t getInt32Value() const;
/**
- * @return true if the term is an integer that fits within std::uint32_t.
+ * @return true if the term is an integer value that fits within uint32_t.
*/
- bool isUInt32() const;
+ bool isUInt32Value() const;
/**
- * @return the stored integer as a std::uint32_t.
- * Note: Asserts isUInt32().
+ * Asserts isUInt32Value().
+ * @return the integer term as a uint32_t.
*/
- std::uint32_t getUInt32() const;
+ uint32_t getUInt32Value() const;
/**
- * @return true if the term is an integer that fits within std::int64_t.
+ * @return true if the term is an integer value that fits within int64_t.
*/
- bool isInt64() const;
+ bool isInt64Value() const;
/**
- * @return the stored integer as a std::int64_t.
- * Note: Asserts isInt64().
+ * Asserts isInt64Value().
+ * @return the integer term as a int64_t.
*/
- std::int64_t getInt64() const;
+ int64_t getInt64Value() const;
/**
- * @return true if the term is an integer that fits within std::uint64_t.
+ * @return true if the term is an integer value that fits within uint64_t.
*/
- bool isUInt64() const;
+ bool isUInt64Value() const;
/**
- * @return the stored integer as a std::uint64_t.
- * Note: Asserts isUInt64().
+ * Asserts isUInt64Value().
+ * @return the integer term as a uint64_t.
*/
- std::uint64_t getUInt64() const;
+ uint64_t getUInt64Value() const;
/**
- * @return true if the term is an integer.
+ * @return true if the term is an integer value.
*/
- bool isInteger() const;
+ bool isIntegerValue() const;
/**
- * @return the stored integer in (decimal) string representation.
- * Note: Asserts isInteger().
+ * Asserts isIntegerValue().
+ * @return the integer term in (decimal) string representation.
*/
- std::string getInteger() const;
+ std::string getIntegerValue() const;
/**
- * @return true if the term is a string constant.
+ * @return true if the term is a string value.
*/
- bool isString() const;
+ bool isStringValue() const;
/**
- * @return the stored string constant.
- *
- * Note: This method is not to be confused with toString() which returns the
- * term in some string representation, whatever data it may hold.
- * Asserts isString().
+ * Note: This method is not to be confused with toString() which returns
+ * the term in some string representation, whatever data it may hold. Asserts
+ * isStringValue().
+ * @return the string term as a native string value.
+ */
+ std::wstring getStringValue() const;
+
+ /**
+ * @return true if the term is a rational value whose numerator and
+ * denominator fit within int32_t and uint32_t, respectively.
+ */
+ bool isReal32Value() const;
+ /**
+ * Asserts isReal32Value().
+ * @return the representation of a rational value as a pair of its numerator
+ * and denominator.
+ */
+ std::pair<int32_t, uint32_t> getReal32Value() const;
+ /**
+ * @return true if the term is a rational value whose numerator and
+ * denominator fit within int64_t and uint64_t, respectively.
*/
- std::wstring getString() const;
+ bool isReal64Value() const;
+ /**
+ * Asserts isReal64Value().
+ * @return the representation of a rational value as a pair of its numerator
+ * and denominator.
+ */
+ std::pair<int64_t, uint64_t> getReal64Value() const;
+ /**
+ * @return true if the term is a rational value.
+ */
+ bool isRealValue() const;
+ /**
+ * Asserts isRealValue().
+ * @return the representation of a rational value as a (decimal) string.
+ */
+ std::string getRealValue() const;
+
+ /**
+ * @return true if the term is a constant array.
+ */
+ bool isConstArray() const;
+ /**
+ * Asserts isConstArray().
+ * @return the base (element stored at all indices) of a constant array
+ */
+ Term getConstArrayBase() const;
+
+ /**
+ * @return true if the term is a Boolean value.
+ */
+ bool isBooleanValue() const;
+ /**
+ * Asserts isBooleanValue().
+ * @return the representation of a Boolean value as a native Boolean value.
+ */
+ bool getBooleanValue() const;
+
+ /**
+ * @return true if the term is a bit-vector value.
+ */
+ bool isBitVectorValue() const;
+ /**
+ * Asserts isBitVectorValue().
+ * @return the representation of a bit-vector value in string representation.
+ * Supported bases are 2 (bit string), 10 (decimal string) or 16 (hexadecimal
+ * string).
+ */
+ std::string getBitVectorValue(uint32_t base = 2) const;
+
+ /**
+ * @return true if the term is an abstract value.
+ */
+ bool isAbstractValue() const;
+ /**
+ * Asserts isAbstractValue().
+ * @return the representation of an abstract value as a string.
+ */
+ std::string getAbstractValue() const;
+
+ /**
+ * @return true if the term is a tuple value.
+ */
+ bool isTupleValue() const;
+ /**
+ * Asserts isTupleValue().
+ * @return the representation of a tuple value as a vector of terms.
+ */
+ std::vector<Term> getTupleValue() const;
+
+ /**
+ * @return true if the term is the floating-point value for positive zero.
+ */
+ bool isFloatingPointPosZero() const;
+ /**
+ * @return true if the term is the floating-point value for negative zero.
+ */
+ bool isFloatingPointNegZero() const;
+ /**
+ * @return true if the term is the floating-point value for positive
+ * infinity.
+ */
+ bool isFloatingPointPosInf() const;
+ /**
+ * @return true if the term is the floating-point value for negative
+ * infinity.
+ */
+ bool isFloatingPointNegInf() const;
+ /**
+ * @return true if the term is the floating-point value for not a number.
+ */
+ bool isFloatingPointNaN() const;
+ /**
+ * @return true if the term is a floating-point value.
+ */
+ bool isFloatingPointValue() const;
+ /**
+ * Asserts isFloatingPointValue().
+ * @return the representation of a floating-point value as a tuple of the
+ * exponent width, the significand width and a bit-vector value.
+ */
+ std::tuple<uint32_t, uint32_t, Term> getFloatingPointValue() const;
+
+ /**
+ * @return true if the term is a set value.
+ */
+ bool isSetValue() const;
+ /**
+ * Asserts isSetValue().
+ * @return the representation of a set value as a set of terms.
+ */
+ std::set<Term> getSetValue() const;
+
+ /**
+ * @return true if the term is a sequence value.
+ */
+ bool isSequenceValue() const;
+ /**
+ * Asserts isSequenceValue().
+ * Note that it is usually necessary for sequences to call
+ * `Solver::simplify()` to turn a sequence that is constructed by, e.g.,
+ * concatenation of unit sequences, into a sequence value.
+ * @return the representation of a sequence value as a vector of terms.
+ */
+ std::vector<Term> getSequenceValue() const;
+
+ /**
+ * @return true if the term is a value from an uninterpreted sort.
+ */
+ bool isUninterpretedValue() const;
+ /**
+ bool @return() const;
+ * Asserts isUninterpretedValue().
+ * @return the representation of an uninterpreted value as a pair of its
+ sort and its
+ * index.
+ */
+ std::pair<Sort, int32_t> getUninterpretedValue() const;
protected:
/**
/** Helper to convert a vector of Terms to internal Nodes. */
std::vector<Node> static termVectorToNodes(const std::vector<Term>& terms);
+ /** Helper method to collect all elements of a set. */
+ static void collectSet(std::set<Term>& set,
+ const cvc5::Node& node,
+ const Solver* slv);
+ /** Helper method to collect all elements of a sequence. */
+ static void collectSequence(std::vector<Term>& seq,
+ const cvc5::Node& node,
+ const Solver* slv);
+
/**
* Constructor.
* @param slv the associated solver object
Term mkSepNil(const Sort& sort) const;
/**
- * Create a String constant.
+ * Create a String constant from a `std::string` which may contain SMT-LIB
+ * compatible escape sequences like `\u1234` to encode unicode characters.
* @param s the string this constant represents
- * @param useEscSequences determines whether escape sequences in \p s should
- * be converted to the corresponding character
+ * @param useEscSequences determines whether escape sequences in `s` should
+ * be converted to the corresponding unicode character
* @return the String constant
*/
Term mkString(const std::string& s, bool useEscSequences = false) const;
/**
- * Create a String constant.
- * @param c the character this constant represents
- * @return the String constant
- */
- Term mkString(const unsigned char c) const;
-
- /**
- * Create a String constant.
- * @param s a list of unsigned (unicode) values this constant represents as
- * string
+ * Create a String constant from a `std::wstring`.
+ * This method does not support escape sequences as `std::wstring` already
+ * supports unicode characters.
+ * @param s the string this constant represents
* @return the String constant
*/
- Term mkString(const std::vector<uint32_t>& s) const;
-
- /**
- * Create a character constant from a given string.
- * @param s the string denoting the code point of the character (in base 16)
- * @return the character constant
- */
- Term mkChar(const std::string& s) const;
+ Term mkString(const std::wstring& s) const;
/**
* Create an empty sequence of the given element sort.
/**
* Create an abstract value constant.
+ * The given index needs to be a positive integer in base 10.
* @param index Index of the abstract value
*/
Term mkAbstractValue(const std::string& index) const;
/**
* Create an abstract value constant.
+ * The given index needs to be positive.
* @param index Index of the abstract value
*/
Term mkAbstractValue(uint64_t index) const;
# import dereference and increment operators
from cython.operator cimport dereference as deref, preincrement as inc
from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t
+from libc.stddef cimport wchar_t
from libcpp.set cimport set
from libcpp.string cimport string
from libcpp.vector cimport vector
hash()
size_t operator()(T t)
+cdef extern from "<string>" namespace "std":
+ cdef cppclass wstring:
+ wstring(const wchar_t*, size_t) except +
cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
cdef cppclass Options:
Term mkEmptySet(Sort s) except +
Term mkSepNil(Sort sort) except +
Term mkString(const string& s) except +
- Term mkString(const vector[unsigned]& s) except +
+ Term mkString(const wstring& s) except +
Term mkEmptySequence(Sort sort) except +
Term mkUniverseSet(Sort sort) except +
Term mkBitVector(uint32_t size) except +
Term operator*() except +
const_iterator begin() except +
const_iterator end() except +
- bint isInteger() except +
+ bint isIntegerValue() except +
cdef cppclass TermHashFunction:
TermHashFunction() except +
import sys
from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t
+from libc.stddef cimport wchar_t
from libcpp.pair cimport pair
from libcpp.set cimport set
from cvc5 cimport ROUND_NEAREST_TIES_TO_AWAY
from cvc5 cimport Term as c_Term
from cvc5 cimport hash as c_hash
+from cvc5 cimport wstring as c_wstring
from cvc5kinds cimport Kind as c_Kind
+cdef extern from "Python.h":
+ wchar_t* PyUnicode_AsWideCharString(object, Py_ssize_t *)
+ void PyMem_Free(void*)
+
################################## DECORATORS #################################
def expand_list_arg(num_req_args=0):
'''
term.cterm = self.csolver.mkSepNil(sort.csort)
return term
- def mkString(self, str_or_vec):
+ def mkString(self, str s):
cdef Term term = Term(self)
- cdef vector[unsigned] v
- if isinstance(str_or_vec, str):
- for u in str_or_vec:
- v.push_back(<unsigned> ord(u))
- term.cterm = self.csolver.mkString(<const vector[unsigned]&> v)
- elif isinstance(str_or_vec, list):
- for u in str_or_vec:
- if not isinstance(u, int):
- raise ValueError("List should contain ints but got: {}"
- .format(str_or_vec))
- v.push_back(<unsigned> u)
- term.cterm = self.csolver.mkString(<const vector[unsigned]&> v)
- else:
- raise ValueError("Expected string or vector of ASCII codes"
- " but got: {}".format(str_or_vec))
+ cdef Py_ssize_t size
+ cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size)
+ term.cterm = self.csolver.mkString(c_wstring(tmp, size))
+ PyMem_Free(tmp)
return term
def mkEmptySequence(self, Sort sort):
return term
def isInteger(self):
- return self.cterm.isInteger()
+ return self.cterm.isIntegerValue()
def toPythonObj(self):
'''
SymbolManager* Parser::getSymbolManager() { return d_symman; }
-std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s)
+std::wstring Parser::processAdHocStringEsc(const std::string& s)
{
std::wstring ws;
{
}
}
- std::vector<unsigned> str;
+ std::wstring res;
unsigned i = 0;
while (i < ws.size())
{
if (ws[i] != '\\')
{
// don't worry about printable here
- str.push_back(static_cast<unsigned>(ws[i]));
+ res.push_back(ws[i]);
++i;
continue;
}
{
case 'n':
{
- str.push_back(static_cast<unsigned>('\n'));
+ res.push_back('\n');
i++;
}
break;
case 't':
{
- str.push_back(static_cast<unsigned>('\t'));
+ res.push_back('\t');
i++;
}
break;
case 'v':
{
- str.push_back(static_cast<unsigned>('\v'));
+ res.push_back('\v');
i++;
}
break;
case 'b':
{
- str.push_back(static_cast<unsigned>('\b'));
+ res.push_back('\b');
i++;
}
break;
case 'r':
{
- str.push_back(static_cast<unsigned>('\r'));
+ res.push_back('\r');
i++;
}
break;
case 'f':
{
- str.push_back(static_cast<unsigned>('\f'));
+ res.push_back('\f');
i++;
}
break;
case 'a':
{
- str.push_back(static_cast<unsigned>('\a'));
+ res.push_back('\a');
i++;
}
break;
case '\\':
{
- str.push_back(static_cast<unsigned>('\\'));
+ res.push_back('\\');
i++;
}
break;
shex << ws[i + 1] << ws[i + 2];
unsigned val;
shex >> std::hex >> val;
- str.push_back(val);
+ res.push_back(val);
i += 3;
isValid = true;
}
&& ws[i + 2] < '8')
{
num = num * 8 + static_cast<unsigned>(ws[i + 2]) - 48;
- str.push_back(num);
+ res.push_back(num);
i += 3;
}
else
{
- str.push_back(num);
+ res.push_back(num);
i += 2;
}
}
else
{
- str.push_back(num);
+ res.push_back(num);
i++;
}
}
}
}
}
- return str;
+ return res;
}
api::Term Parser::mkStringConstant(const std::string& s)
return d_solver->mkString(s, true);
}
// otherwise, we must process ad-hoc escape sequences
- std::vector<unsigned> str = processAdHocStringEsc(s);
+ std::wstring str = processAdHocStringEsc(s);
return d_solver->mkString(str);
}
+api::Term Parser::mkCharConstant(const std::string& s)
+{
+ Assert(s.find_first_not_of("0123456789abcdefABCDEF", 0) == std::string::npos
+ && s.size() <= 5 && s.size() > 0)
+ << "Unexpected string for hexadecimal character " << s;
+ wchar_t val = static_cast<wchar_t>(std::stoul(s, 0, 16));
+ return d_solver->mkString(std::wstring(1, val));
+}
+
} // namespace parser
} // namespace cvc5
*/
api::Term mkStringConstant(const std::string& s);
+ /**
+ * Make string constant from a single character in hex representation
+ *
+ * This makes the string constant based on the character from the strings,
+ * represented as a hexadecimal code point.
+ */
+ api::Term mkCharConstant(const std::string& s);
+
/** ad-hoc string escaping
*
* Returns the (internal) vector of code points corresponding to processing
* \\, \x[N] and octal escape sequences of the form \[c1]([c2]([c3])?)? where
* c1, c2, c3 are digits from 0 to 7.
*/
- std::vector<unsigned> processAdHocStringEsc(const std::string& s);
+ std::wstring processAdHocStringEsc(const std::string& s);
}; /* class Parser */
} // namespace parser
| CHAR_TOK HEX_LITERAL
{
std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
- atomTerm = SOLVER->mkChar(hexStr);
+ atomTerm = PARSER_STATE->mkCharConstant(hexStr);
}
| sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
{
else if (p.d_kind == api::APPLY_SELECTOR && !p.d_expr.isNull())
{
// tuple selector case
- if (!p.d_expr.isUInt64())
+ if (!p.d_expr.isUInt64Value())
{
parseError("index of tupSel is larger than size of uint64_t");
}
- uint64_t n = p.d_expr.getUInt64();
+ uint64_t n = p.d_expr.getUInt64Value();
if (args.size() != 1)
{
parseError("tupSel should only be applied to one tuple argument");
// call Term::toString as its result depends on the output language.
// Notice that we only check for string constants. The sexprs generated by the
// parser don't contains other constants, so we can ignore them.
- if (sexpr.isString())
+ if (sexpr.isStringValue())
{
// convert std::wstring to std::string
- std::wstring wstring = sexpr.getString();
+ std::wstring wstring = sexpr.getStringValue();
return std::string(wstring.cbegin(), wstring.cend());
}
static_assert(UCHAR_MAX == 255, "Unsigned char is assumed to have 256 values.");
+String::String(const std::wstring& s)
+{
+ d_str.resize(s.size());
+ for (size_t i = 0, n = s.size(); i < n; ++i)
+ {
+ d_str[i] = static_cast<unsigned>(s[i]);
+ }
+}
+
String::String(const std::vector<unsigned> &s) : d_str(s)
{
#ifdef CVC5_ASSERTIONS
: d_str(toInternal(s, useEscSequences))
{
}
+ explicit String(const std::wstring& s);
explicit String(const char* s, bool useEscSequences = false)
: d_str(toInternal(std::string(s), useEscSequences))
{
"\"asdf\\u{5c}nasdf\"");
}
-TEST_F(TestApiBlackSolver, mkChar)
-{
- ASSERT_NO_THROW(d_solver.mkChar(std::string("0123")));
- ASSERT_NO_THROW(d_solver.mkChar("aA"));
- ASSERT_THROW(d_solver.mkChar(""), CVC5ApiException);
- ASSERT_THROW(d_solver.mkChar("0g0"), CVC5ApiException);
- ASSERT_THROW(d_solver.mkChar("100000"), CVC5ApiException);
- ASSERT_EQ(d_solver.mkChar("abc"), d_solver.mkChar("ABC"));
-}
-
TEST_F(TestApiBlackSolver, mkTerm)
{
Sort bv32 = d_solver.mkBitVectorSort(32);
ASSERT_THROW(d_solver.mkInteger("-01"), CVC5ApiException);
ASSERT_THROW(d_solver.mkInteger("-00"), CVC5ApiException);
- ASSERT_TRUE(!int1.isInt32() && !int1.isUInt32() && !int1.isInt64()
- && !int1.isUInt64() && int1.isInteger());
- ASSERT_EQ(int1.getInteger(), "-18446744073709551616");
- ASSERT_TRUE(!int2.isInt32() && !int2.isUInt32() && !int2.isInt64()
- && !int2.isUInt64() && int2.isInteger());
- ASSERT_EQ(int2.getInteger(), "-18446744073709551615");
- ASSERT_TRUE(!int3.isInt32() && !int3.isUInt32() && int3.isInt64()
- && !int3.isUInt64() && int3.isInteger());
- ASSERT_EQ(int3.getInt64(), -4294967296);
- ASSERT_EQ(int3.getInteger(), "-4294967296");
- ASSERT_TRUE(!int4.isInt32() && !int4.isUInt32() && int4.isInt64()
- && !int4.isUInt64() && int4.isInteger());
- ASSERT_EQ(int4.getInt64(), -4294967295);
- ASSERT_EQ(int4.getInteger(), "-4294967295");
- ASSERT_TRUE(int5.isInt32() && !int5.isUInt32() && int5.isInt64()
- && !int5.isUInt64() && int5.isInteger());
- ASSERT_EQ(int5.getInt32(), -10);
- ASSERT_EQ(int5.getInt64(), -10);
- ASSERT_EQ(int5.getInteger(), "-10");
- ASSERT_TRUE(int6.isInt32() && int6.isUInt32() && int6.isInt64()
- && int6.isUInt64() && int6.isInteger());
- ASSERT_EQ(int6.getInt32(), 0);
- ASSERT_EQ(int6.getUInt32(), 0);
- ASSERT_EQ(int6.getInt64(), 0);
- ASSERT_EQ(int6.getUInt64(), 0);
- ASSERT_EQ(int6.getInteger(), "0");
- ASSERT_TRUE(int7.isInt32() && int7.isUInt32() && int7.isInt64()
- && int7.isUInt64() && int7.isInteger());
- ASSERT_EQ(int7.getInt32(), 10);
- ASSERT_EQ(int7.getUInt32(), 10);
- ASSERT_EQ(int7.getInt64(), 10);
- ASSERT_EQ(int7.getUInt64(), 10);
- ASSERT_EQ(int7.getInteger(), "10");
- ASSERT_TRUE(!int8.isInt32() && int8.isUInt32() && int8.isInt64()
- && int8.isUInt64() && int8.isInteger());
- ASSERT_EQ(int8.getUInt32(), 4294967295);
- ASSERT_EQ(int8.getInt64(), 4294967295);
- ASSERT_EQ(int8.getUInt64(), 4294967295);
- ASSERT_EQ(int8.getInteger(), "4294967295");
- ASSERT_TRUE(!int9.isInt32() && !int9.isUInt32() && int9.isInt64()
- && int9.isUInt64() && int9.isInteger());
- ASSERT_EQ(int9.getInt64(), 4294967296);
- ASSERT_EQ(int9.getUInt64(), 4294967296);
- ASSERT_EQ(int9.getInteger(), "4294967296");
- ASSERT_TRUE(!int10.isInt32() && !int10.isUInt32() && !int10.isInt64()
- && int10.isUInt64() && int10.isInteger());
- ASSERT_EQ(int10.getUInt64(), 18446744073709551615ull);
- ASSERT_EQ(int10.getInteger(), "18446744073709551615");
- ASSERT_TRUE(!int11.isInt32() && !int11.isUInt32() && !int11.isInt64()
- && !int11.isUInt64() && int11.isInteger());
- ASSERT_EQ(int11.getInteger(), "18446744073709551616");
+ ASSERT_TRUE(!int1.isInt32Value() && !int1.isUInt32Value()
+ && !int1.isInt64Value() && !int1.isUInt64Value()
+ && int1.isIntegerValue());
+ ASSERT_EQ(int1.getIntegerValue(), "-18446744073709551616");
+ ASSERT_TRUE(!int2.isInt32Value() && !int2.isUInt32Value()
+ && !int2.isInt64Value() && !int2.isUInt64Value()
+ && int2.isIntegerValue());
+ ASSERT_EQ(int2.getIntegerValue(), "-18446744073709551615");
+ ASSERT_TRUE(!int3.isInt32Value() && !int3.isUInt32Value()
+ && int3.isInt64Value() && !int3.isUInt64Value()
+ && int3.isIntegerValue());
+ ASSERT_EQ(int3.getInt64Value(), -4294967296);
+ ASSERT_EQ(int3.getIntegerValue(), "-4294967296");
+ ASSERT_TRUE(!int4.isInt32Value() && !int4.isUInt32Value()
+ && int4.isInt64Value() && !int4.isUInt64Value()
+ && int4.isIntegerValue());
+ ASSERT_EQ(int4.getInt64Value(), -4294967295);
+ ASSERT_EQ(int4.getIntegerValue(), "-4294967295");
+ ASSERT_TRUE(int5.isInt32Value() && !int5.isUInt32Value()
+ && int5.isInt64Value() && !int5.isUInt64Value()
+ && int5.isIntegerValue());
+ ASSERT_EQ(int5.getInt32Value(), -10);
+ ASSERT_EQ(int5.getInt64Value(), -10);
+ ASSERT_EQ(int5.getIntegerValue(), "-10");
+ ASSERT_TRUE(int6.isInt32Value() && int6.isUInt32Value() && int6.isInt64Value()
+ && int6.isUInt64Value() && int6.isIntegerValue());
+ ASSERT_EQ(int6.getInt32Value(), 0);
+ ASSERT_EQ(int6.getUInt32Value(), 0);
+ ASSERT_EQ(int6.getInt64Value(), 0);
+ ASSERT_EQ(int6.getUInt64Value(), 0);
+ ASSERT_EQ(int6.getIntegerValue(), "0");
+ ASSERT_TRUE(int7.isInt32Value() && int7.isUInt32Value() && int7.isInt64Value()
+ && int7.isUInt64Value() && int7.isIntegerValue());
+ ASSERT_EQ(int7.getInt32Value(), 10);
+ ASSERT_EQ(int7.getUInt32Value(), 10);
+ ASSERT_EQ(int7.getInt64Value(), 10);
+ ASSERT_EQ(int7.getUInt64Value(), 10);
+ ASSERT_EQ(int7.getIntegerValue(), "10");
+ ASSERT_TRUE(!int8.isInt32Value() && int8.isUInt32Value()
+ && int8.isInt64Value() && int8.isUInt64Value()
+ && int8.isIntegerValue());
+ ASSERT_EQ(int8.getUInt32Value(), 4294967295);
+ ASSERT_EQ(int8.getInt64Value(), 4294967295);
+ ASSERT_EQ(int8.getUInt64Value(), 4294967295);
+ ASSERT_EQ(int8.getIntegerValue(), "4294967295");
+ ASSERT_TRUE(!int9.isInt32Value() && !int9.isUInt32Value()
+ && int9.isInt64Value() && int9.isUInt64Value()
+ && int9.isIntegerValue());
+ ASSERT_EQ(int9.getInt64Value(), 4294967296);
+ ASSERT_EQ(int9.getUInt64Value(), 4294967296);
+ ASSERT_EQ(int9.getIntegerValue(), "4294967296");
+ ASSERT_TRUE(!int10.isInt32Value() && !int10.isUInt32Value()
+ && !int10.isInt64Value() && int10.isUInt64Value()
+ && int10.isIntegerValue());
+ ASSERT_EQ(int10.getUInt64Value(), 18446744073709551615ull);
+ ASSERT_EQ(int10.getIntegerValue(), "18446744073709551615");
+ ASSERT_TRUE(!int11.isInt32Value() && !int11.isUInt32Value()
+ && !int11.isInt64Value() && !int11.isUInt64Value()
+ && int11.isIntegerValue());
+ ASSERT_EQ(int11.getIntegerValue(), "18446744073709551616");
}
TEST_F(TestApiBlackTerm, getString)
{
Term s1 = d_solver.mkString("abcde");
- ASSERT_TRUE(s1.isString());
- ASSERT_EQ(s1.getString(), L"abcde");
+ ASSERT_TRUE(s1.isStringValue());
+ ASSERT_EQ(s1.getStringValue(), L"abcde");
+}
+
+TEST_F(TestApiBlackTerm, getReal)
+{
+ Term real1 = d_solver.mkReal("0");
+ Term real2 = d_solver.mkReal(".0");
+ Term real3 = d_solver.mkReal("-17");
+ Term real4 = d_solver.mkReal("-3/5");
+ Term real5 = d_solver.mkReal("12.7");
+ Term real6 = d_solver.mkReal("1/4294967297");
+ Term real7 = d_solver.mkReal("4294967297");
+ Term real8 = d_solver.mkReal("1/18446744073709551617");
+ Term real9 = d_solver.mkReal("18446744073709551617");
+
+ ASSERT_TRUE(real1.isRealValue() && real1.isReal64Value()
+ && real1.isReal32Value());
+ ASSERT_TRUE(real2.isRealValue() && real2.isReal64Value()
+ && real2.isReal32Value());
+ ASSERT_TRUE(real3.isRealValue() && real3.isReal64Value()
+ && real3.isReal32Value());
+ ASSERT_TRUE(real4.isRealValue() && real4.isReal64Value()
+ && real4.isReal32Value());
+ ASSERT_TRUE(real5.isRealValue() && real5.isReal64Value()
+ && real5.isReal32Value());
+ ASSERT_TRUE(real6.isRealValue() && real6.isReal64Value());
+ ASSERT_TRUE(real7.isRealValue() && real7.isReal64Value());
+ ASSERT_TRUE(real8.isRealValue());
+ ASSERT_TRUE(real9.isRealValue());
+
+ ASSERT_EQ(std::make_pair(0, 1u), real1.getReal32Value());
+ ASSERT_EQ(std::make_pair(0l, 1ul), real1.getReal64Value());
+ ASSERT_EQ("0", real1.getRealValue());
+
+ ASSERT_EQ(std::make_pair(0, 1u), real2.getReal32Value());
+ ASSERT_EQ(std::make_pair(0l, 1ul), real2.getReal64Value());
+ ASSERT_EQ("0", real2.getRealValue());
+
+ ASSERT_EQ(std::make_pair(-17, 1u), real3.getReal32Value());
+ ASSERT_EQ(std::make_pair(-17l, 1ul), real3.getReal64Value());
+ ASSERT_EQ("-17", real3.getRealValue());
+
+ ASSERT_EQ(std::make_pair(-3, 5u), real4.getReal32Value());
+ ASSERT_EQ(std::make_pair(-3l, 5ul), real4.getReal64Value());
+ ASSERT_EQ("-3/5", real4.getRealValue());
+
+ ASSERT_EQ(std::make_pair(127, 10u), real5.getReal32Value());
+ ASSERT_EQ(std::make_pair(127l, 10ul), real5.getReal64Value());
+ ASSERT_EQ("127/10", real5.getRealValue());
+
+ ASSERT_EQ(std::make_pair(1l, 4294967297ul), real6.getReal64Value());
+ ASSERT_EQ("1/4294967297", real6.getRealValue());
+
+ ASSERT_EQ(std::make_pair(4294967297l, 1ul), real7.getReal64Value());
+ ASSERT_EQ("4294967297", real7.getRealValue());
+
+ ASSERT_EQ("1/18446744073709551617", real8.getRealValue());
+
+ ASSERT_EQ("18446744073709551617", real9.getRealValue());
+}
+
+TEST_F(TestApiBlackTerm, getConstArrayBase)
+{
+ Sort intsort = d_solver.getIntegerSort();
+ Sort arrsort = d_solver.mkArraySort(intsort, intsort);
+ Term one = d_solver.mkInteger(1);
+ Term constarr = d_solver.mkConstArray(arrsort, one);
+
+ ASSERT_TRUE(constarr.isConstArray());
+ ASSERT_EQ(one, constarr.getConstArrayBase());
+}
+
+TEST_F(TestApiBlackTerm, getBoolean)
+{
+ Term b1 = d_solver.mkBoolean(true);
+ Term b2 = d_solver.mkBoolean(false);
+
+ ASSERT_TRUE(b1.isBooleanValue());
+ ASSERT_TRUE(b2.isBooleanValue());
+ ASSERT_TRUE(b1.getBooleanValue());
+ ASSERT_FALSE(b2.getBooleanValue());
+}
+
+TEST_F(TestApiBlackTerm, getBitVector)
+{
+ Term b1 = d_solver.mkBitVector(8, 15);
+ Term b2 = d_solver.mkBitVector("00001111", 2);
+ Term b3 = d_solver.mkBitVector("15", 10);
+ Term b4 = d_solver.mkBitVector("0f", 16);
+ Term b5 = d_solver.mkBitVector(8, "00001111", 2);
+ Term b6 = d_solver.mkBitVector(8, "15", 10);
+ Term b7 = d_solver.mkBitVector(8, "0f", 16);
+
+ ASSERT_TRUE(b1.isBitVectorValue());
+ ASSERT_TRUE(b2.isBitVectorValue());
+ ASSERT_TRUE(b3.isBitVectorValue());
+ ASSERT_TRUE(b4.isBitVectorValue());
+ ASSERT_TRUE(b5.isBitVectorValue());
+ ASSERT_TRUE(b6.isBitVectorValue());
+ ASSERT_TRUE(b7.isBitVectorValue());
+
+ ASSERT_EQ("00001111", b1.getBitVectorValue(2));
+ ASSERT_EQ("15", b1.getBitVectorValue(10));
+ ASSERT_EQ("f", b1.getBitVectorValue(16));
+ ASSERT_EQ("00001111", b2.getBitVectorValue(2));
+ ASSERT_EQ("15", b2.getBitVectorValue(10));
+ ASSERT_EQ("f", b2.getBitVectorValue(16));
+ ASSERT_EQ("1111", b3.getBitVectorValue(2));
+ ASSERT_EQ("15", b3.getBitVectorValue(10));
+ ASSERT_EQ("f", b3.getBitVectorValue(16));
+ ASSERT_EQ("00001111", b4.getBitVectorValue(2));
+ ASSERT_EQ("15", b4.getBitVectorValue(10));
+ ASSERT_EQ("f", b4.getBitVectorValue(16));
+ ASSERT_EQ("00001111", b5.getBitVectorValue(2));
+ ASSERT_EQ("15", b5.getBitVectorValue(10));
+ ASSERT_EQ("f", b5.getBitVectorValue(16));
+ ASSERT_EQ("00001111", b6.getBitVectorValue(2));
+ ASSERT_EQ("15", b6.getBitVectorValue(10));
+ ASSERT_EQ("f", b6.getBitVectorValue(16));
+ ASSERT_EQ("00001111", b7.getBitVectorValue(2));
+ ASSERT_EQ("15", b7.getBitVectorValue(10));
+ ASSERT_EQ("f", b7.getBitVectorValue(16));
+}
+
+TEST_F(TestApiBlackTerm, getAbstractValue)
+{
+ Term v1 = d_solver.mkAbstractValue(1);
+ Term v2 = d_solver.mkAbstractValue("15");
+ Term v3 = d_solver.mkAbstractValue("18446744073709551617");
+
+ ASSERT_TRUE(v1.isAbstractValue());
+ ASSERT_TRUE(v2.isAbstractValue());
+ ASSERT_TRUE(v3.isAbstractValue());
+ ASSERT_EQ("1", v1.getAbstractValue());
+ ASSERT_EQ("15", v2.getAbstractValue());
+ ASSERT_EQ("18446744073709551617", v3.getAbstractValue());
+}
+
+TEST_F(TestApiBlackTerm, getTuple)
+{
+ Sort s1 = d_solver.getIntegerSort();
+ Sort s2 = d_solver.getRealSort();
+ Sort s3 = d_solver.getStringSort();
+
+ Term t1 = d_solver.mkInteger(15);
+ Term t2 = d_solver.mkReal(17, 25);
+ Term t3 = d_solver.mkString("abc");
+
+ Term tup = d_solver.mkTuple({s1, s2, s3}, {t1, t2, t3});
+
+ ASSERT_TRUE(tup.isTupleValue());
+ ASSERT_EQ(std::vector<Term>({t1, t2, t3}), tup.getTupleValue());
+}
+
+TEST_F(TestApiBlackTerm, getFloatingPoint)
+{
+ Term bvval = d_solver.mkBitVector("0000110000000011");
+ Term fp = d_solver.mkFloatingPoint(5, 11, bvval);
+
+ ASSERT_TRUE(fp.isFloatingPointValue());
+ ASSERT_FALSE(fp.isFloatingPointPosZero());
+ ASSERT_FALSE(fp.isFloatingPointNegZero());
+ ASSERT_FALSE(fp.isFloatingPointPosInf());
+ ASSERT_FALSE(fp.isFloatingPointNegInf());
+ ASSERT_FALSE(fp.isFloatingPointNaN());
+ ASSERT_EQ(std::make_tuple(5u, 11u, bvval), fp.getFloatingPointValue());
+
+ ASSERT_TRUE(d_solver.mkPosZero(5, 11).isFloatingPointPosZero());
+ ASSERT_TRUE(d_solver.mkNegZero(5, 11).isFloatingPointNegZero());
+ ASSERT_TRUE(d_solver.mkPosInf(5, 11).isFloatingPointPosInf());
+ ASSERT_TRUE(d_solver.mkNegInf(5, 11).isFloatingPointNegInf());
+ ASSERT_TRUE(d_solver.mkNaN(5, 11).isFloatingPointNaN());
+}
+
+TEST_F(TestApiBlackTerm, getSet)
+{
+ Sort s = d_solver.mkSetSort(d_solver.getIntegerSort());
+
+ Term i1 = d_solver.mkInteger(5);
+ Term i2 = d_solver.mkInteger(7);
+
+ Term s1 = d_solver.mkEmptySet(s);
+ Term s2 = d_solver.mkTerm(Kind::SINGLETON, i1);
+ Term s3 = d_solver.mkTerm(Kind::SINGLETON, i1);
+ Term s4 = d_solver.mkTerm(Kind::SINGLETON, i2);
+ Term s5 =
+ d_solver.mkTerm(Kind::UNION, s2, d_solver.mkTerm(Kind::UNION, s3, s4));
+
+ ASSERT_TRUE(s1.isSetValue());
+ ASSERT_TRUE(s2.isSetValue());
+ ASSERT_TRUE(s3.isSetValue());
+ ASSERT_TRUE(s4.isSetValue());
+ ASSERT_FALSE(s5.isSetValue());
+ s5 = d_solver.simplify(s5);
+ ASSERT_TRUE(s5.isSetValue());
+
+ ASSERT_EQ(std::set<Term>({}), s1.getSetValue());
+ ASSERT_EQ(std::set<Term>({i1}), s2.getSetValue());
+ ASSERT_EQ(std::set<Term>({i1}), s3.getSetValue());
+ ASSERT_EQ(std::set<Term>({i2}), s4.getSetValue());
+ ASSERT_EQ(std::set<Term>({i1, i2}), s5.getSetValue());
+}
+
+TEST_F(TestApiBlackTerm, getSequence)
+{
+ Sort s = d_solver.mkSequenceSort(d_solver.getIntegerSort());
+
+ Term i1 = d_solver.mkInteger(5);
+ Term i2 = d_solver.mkInteger(7);
+
+ Term s1 = d_solver.mkEmptySequence(s);
+ Term s2 = d_solver.mkTerm(Kind::SEQ_UNIT, i1);
+ Term s3 = d_solver.mkTerm(Kind::SEQ_UNIT, i1);
+ Term s4 = d_solver.mkTerm(Kind::SEQ_UNIT, i2);
+ Term s5 = d_solver.mkTerm(
+ Kind::SEQ_CONCAT, s2, d_solver.mkTerm(Kind::SEQ_CONCAT, s3, s4));
+
+ ASSERT_TRUE(s1.isSequenceValue());
+ ASSERT_TRUE(!s2.isSequenceValue());
+ ASSERT_TRUE(!s3.isSequenceValue());
+ ASSERT_TRUE(!s4.isSequenceValue());
+ ASSERT_TRUE(!s5.isSequenceValue());
+
+ s2 = d_solver.simplify(s2);
+ s3 = d_solver.simplify(s3);
+ s4 = d_solver.simplify(s4);
+ s5 = d_solver.simplify(s5);
+
+ ASSERT_EQ(std::vector<Term>({}), s1.getSequenceValue());
+ ASSERT_EQ(std::vector<Term>({i1}), s2.getSequenceValue());
+ ASSERT_EQ(std::vector<Term>({i1}), s3.getSequenceValue());
+ ASSERT_EQ(std::vector<Term>({i2}), s4.getSequenceValue());
+ ASSERT_EQ(std::vector<Term>({i1, i1, i2}), s5.getSequenceValue());
+}
+
+TEST_F(TestApiBlackTerm, getUninterpretedConst)
+{
+ Sort s = d_solver.mkUninterpretedSort("test");
+ Term t1 = d_solver.mkUninterpretedConst(s, 3);
+ Term t2 = d_solver.mkUninterpretedConst(s, 5);
+
+ ASSERT_TRUE(t1.isUninterpretedValue());
+ ASSERT_TRUE(t2.isUninterpretedValue());
+
+ ASSERT_EQ(std::make_pair(s, 3), t1.getUninterpretedValue());
+ ASSERT_EQ(std::make_pair(s, 5), t2.getUninterpretedValue());
}
TEST_F(TestApiBlackTerm, substitute)
projects / cvc5.git / commitdiff