cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_SBV),
KIND_ENUM(FLOATINGPOINT_TO_FP_FROM_UBV,
cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_UBV),
- KIND_ENUM(FLOATINGPOINT_TO_FP_GENERIC,
- cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC),
KIND_ENUM(FLOATINGPOINT_TO_UBV, cvc5::Kind::FLOATINGPOINT_TO_UBV),
KIND_ENUM(FLOATINGPOINT_TO_SBV, cvc5::Kind::FLOATINGPOINT_TO_SBV),
KIND_ENUM(FLOATINGPOINT_TO_REAL, cvc5::Kind::FLOATINGPOINT_TO_REAL),
FLOATINGPOINT_TO_FP_FROM_UBV},
{cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_UBV,
FLOATINGPOINT_TO_FP_FROM_UBV},
- {cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP,
- FLOATINGPOINT_TO_FP_GENERIC},
- {cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC, FLOATINGPOINT_TO_FP_GENERIC},
{cvc5::Kind::FLOATINGPOINT_TO_UBV_OP, FLOATINGPOINT_TO_UBV},
{cvc5::Kind::FLOATINGPOINT_TO_UBV, FLOATINGPOINT_TO_UBV},
{cvc5::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP, INTERNAL_KIND},
FLOATINGPOINT_TO_FP_FROM_FP,
FLOATINGPOINT_TO_FP_FROM_REAL,
FLOATINGPOINT_TO_FP_FROM_SBV,
- FLOATINGPOINT_TO_FP_FROM_UBV,
- FLOATINGPOINT_TO_FP_GENERIC});
+ FLOATINGPOINT_TO_FP_FROM_UBV});
namespace {
case FLOATINGPOINT_TO_FP_FROM_REAL: size = 2; break;
case FLOATINGPOINT_TO_FP_FROM_SBV: size = 2; break;
case FLOATINGPOINT_TO_FP_FROM_UBV: size = 2; break;
- case FLOATINGPOINT_TO_FP_GENERIC: size = 2; break;
case REGEXP_LOOP: size = 2; break;
case TUPLE_PROJECT:
size = d_node->getConst<TupleProjectOp>().getIndices().size();
: d_solver->mkRationalValHelper(ext.getSize().significandWidth());
break;
}
- case FLOATINGPOINT_TO_FP_GENERIC:
- {
- cvc5::FloatingPointToFPGeneric ext =
- d_node->getConst<FloatingPointToFPGeneric>();
- t = index == 0
- ? d_solver->mkRationalValHelper(ext.getSize().exponentWidth())
- : d_solver->mkRationalValHelper(ext.getSize().significandWidth());
- break;
- }
case REGEXP_LOOP:
{
cvc5::RegExpLoop ext = d_node->getConst<RegExpLoop>();
cvc5::FloatingPointToFPUnsignedBitVector(arg1, arg2))
.d_node);
break;
- case FLOATINGPOINT_TO_FP_GENERIC:
- res = Op(this,
- kind,
- *mkValHelper<cvc5::FloatingPointToFPGeneric>(
- cvc5::FloatingPointToFPGeneric(arg1, arg2))
- .d_node);
- break;
case REGEXP_LOOP:
res = Op(
this,
* - FLOATINGPOINT_TO_FP_FROM_REAL
* - FLOATINGPOINT_TO_FP_FROM_SBV
* - FLOATINGPOINT_TO_FP_FROM_UBV
- * - FLOATINGPOINT_TO_FP_GENERIC
* See enum Kind for a description of the parameters.
* @param kind the kind of the operator
* @param arg1 the first uint32_t argument to this operator
* - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
*/
FLOATINGPOINT_TO_FP_FROM_UBV,
- /**
- * Operator for a generic to_fp.
- *
- * Parameters:
- * - 1: exponent size
- * - 2: Significand size
- *
- * Create with:
- * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const`
- *
- * Generic conversion to floating-point, used in parsing only.
- *
- * Parameters:
- *
- * For conversion from IEEE bit-vector:
- * - 1: Op of kind FLOATINGPOINT_TO_FP_GENERIC
- * - 2: Term of bit-vector sort
- *
- * For conversion from floating-point:
- * - 1: Op of kind FLOATINGPOINT_TO_FP_GENERIC
- * - 2: Term of sort RoundingMode
- * - 3: Term of floating-point sort
- *
- * For conversion from Real:
- * - 1: Op of kind FLOATINGPOINT_TO_FP_GENERIC
- * - 2: Term of sort RoundingMode
- * - 3: Term of sort Real
- *
- * For conversion from (un)signed bit-vector:
- * - 1: Op of kind FLOATINGPOINT_TO_FP_GENERIC
- * - 2: Term of sort RoundingMode
- * - 3: Term of bit-vector sort
- *
- * Create with:
- * - `Solver::mkTerm(const Op& op, const Term& child) const`
- * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
- * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
- */
- FLOATINGPOINT_TO_FP_GENERIC,
/**
* Operator for to_ubv.
*
* - FLOATINGPOINT_TO_FP_FROM_REAL
* - FLOATINGPOINT_TO_FP_FROM_SBV
* - FLOATINGPOINT_TO_FP_FROM_UBV
- * - FLOATINGPOINT_TO_FP_GENERIC
* See enum Kind for a description of the parameters.
* @param kind the kind of the operator
* @param arg1 the first unsigned int argument to this operator
{
out << " :name " << p.d_name;
}
+ if (!p.d_indices.empty())
+ {
+ out << " :indices [";
+ bool first = true;
+ for (uint32_t index : p.d_indices)
+ {
+ if (!first)
+ {
+ out << ", ";
+ }
+ first = false;
+ out << index;
+ }
+ out << "]";
+ }
out << ")";
return os << out.str();
}
#define CVC5__PARSER__PARSE_OP_H
#include <string>
+#include <vector>
#include "api/cpp/cvc5.h"
api::Sort d_type;
/** The operator associated with the parsed operator, if it exists */
api::Op d_op;
+ /**
+ * The indices if the operator is indexed, but api::Op is the null operator.
+ * This is the case for operator symbols that cannot be resolved to a kind
+ * without parsing the arguments. This is currently only the case for
+ * `to_fp`.
+ */
+ std::vector<uint32_t> d_indices;
/* Return true if this is equal to 'p'. */
bool operator==(const ParseOp& p) const
{
return d_kind == p.d_kind && d_name == p.d_name && d_expr == p.d_expr
- && d_type == p.d_type && d_op == p.d_op;
+ && d_type == p.d_type && d_op == p.d_op && d_indices == p.d_indices;
}
};
{
std::string opName = AntlrInput::tokenText($sym);
api::Kind k = PARSER_STATE->getIndexedOpKind(opName);
- if (k == api::APPLY_SELECTOR || k == api::APPLY_UPDATER)
+ if (k == api::UNDEFINED_KIND)
+ {
+ // We don't know which kind to use until we know the type of the
+ // arguments
+ p.d_name = opName;
+ // convert uint64_t to uint32_t
+ for(uint32_t numeral : numerals)
+ {
+ p.d_indices.push_back(numeral);
+ }
+ }
+ else if (k == api::APPLY_SELECTOR || k == api::APPLY_UPDATER)
{
// we adopt a special syntax (_ tuple_select n) and (_ tuple_update n)
// for tuple selectors and updaters
addOperator(api::FLOATINGPOINT_IS_POS, "fp.isPositive");
addOperator(api::FLOATINGPOINT_TO_REAL, "fp.to_real");
- addIndexedOperator(api::FLOATINGPOINT_TO_FP_GENERIC, "to_fp");
+ addIndexedOperator(api::UNDEFINED_KIND, "to_fp");
addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_UBV, "to_fp_unsigned");
addIndexedOperator(api::FLOATINGPOINT_TO_UBV, "fp.to_ubv");
addIndexedOperator(api::FLOATINGPOINT_TO_SBV, "fp.to_sbv");
d_indexedOpKindMap[name] = tKind;
}
+bool Smt2::isIndexedOperatorEnabled(const std::string& name) const
+{
+ return d_indexedOpKindMap.find(name) != d_indexedOpKindMap.end();
+}
+
api::Kind Smt2::getOperatorKind(const std::string& name) const
{
// precondition: isOperatorEnabled(name)
// it was given an operator
op = p.d_op;
}
+ else if (isIndexedOperatorEnabled(p.d_name))
+ {
+ // Resolve indexed symbols that cannot be resolved without knowing the type
+ // of the arguments. This is currently limited to `to_fp`.
+ Assert(p.d_name == "to_fp");
+ size_t nchildren = args.size();
+ if (nchildren == 1)
+ {
+ op = d_solver->mkOp(api::FLOATINGPOINT_TO_FP_FROM_IEEE_BV,
+ p.d_indices[0],
+ p.d_indices[1]);
+ }
+ else if (nchildren > 2)
+ {
+ std::stringstream ss;
+ ss << "Wrong number of arguments for indexed operator to_fp, expected "
+ "1 or 2, got "
+ << nchildren;
+ parseError(ss.str());
+ }
+ else if (!args[0].getSort().isRoundingMode())
+ {
+ std::stringstream ss;
+ ss << "Expected a rounding mode as the first argument, got "
+ << args[0].getSort();
+ parseError(ss.str());
+ }
+ else
+ {
+ api::Sort t = args[1].getSort();
+
+ if (t.isFloatingPoint())
+ {
+ op = d_solver->mkOp(
+ api::FLOATINGPOINT_TO_FP_FROM_FP, p.d_indices[0], p.d_indices[1]);
+ }
+ else if (t.isInteger() || t.isReal())
+ {
+ op = d_solver->mkOp(
+ api::FLOATINGPOINT_TO_FP_FROM_REAL, p.d_indices[0], p.d_indices[1]);
+ }
+ else
+ {
+ op = d_solver->mkOp(
+ api::FLOATINGPOINT_TO_FP_FROM_SBV, p.d_indices[0], p.d_indices[1]);
+ }
+ }
+ }
else
{
isBuiltinOperator = isOperatorEnabled(p.d_name);
* Registers an indexed function symbol.
*
* @param tKind The kind of the term that uses the operator kind (e.g.
- * BITVECTOR_EXTRACT).
+ * BITVECTOR_EXTRACT). If an indexed function symbol is
+ * overloaded (e.g., `to_fp`), this argument should
+ * be`UNDEFINED_KIND`.
* @param name The name of the symbol (e.g. "extract")
*/
void addIndexedOperator(api::Kind tKind,
const std::string& name);
+ /**
+ * Checks whether an indexed operator is enabled. All indexed operators in
+ * the current logic are considered to be enabled. This includes operators
+ * such as `to_fp`, which do not correspond to a single kind.
+ *
+ * @param name The name of the indexed operator.
+ * @return true if the indexed operator is enabled.
+ */
+ bool isIndexedOperatorEnabled(const std::string& name) const;
api::Kind getOperatorKind(const std::string& name) const;
.significandWidth()
<< ")";
break;
- case kind::FLOATINGPOINT_TO_FP_GENERIC_OP:
- out << "(_ to_fp "
- << n.getConst<FloatingPointToFPGeneric>().getSize().exponentWidth()
- << ' '
- << n.getConst<FloatingPointToFPGeneric>().getSize().significandWidth()
- << ")";
- break;
case kind::FLOATINGPOINT_TO_UBV_OP:
out << "(_ fp.to_ubv "
<< n.getConst<FloatingPointToUBV>().d_bv_size.d_size << ")";
case kind::FLOATINGPOINT_TO_FP_FROM_REAL:
case kind::FLOATINGPOINT_TO_FP_FROM_SBV:
case kind::FLOATINGPOINT_TO_FP_FROM_UBV:
- case kind::FLOATINGPOINT_TO_FP_GENERIC:
case kind::FLOATINGPOINT_TO_UBV:
case kind::FLOATINGPOINT_TO_SBV:
out << n.getOperator() << ' ';
case kind::FLOATINGPOINT_TO_FP_FROM_REAL: return "to_fp";
case kind::FLOATINGPOINT_TO_FP_FROM_SBV: return "to_fp";
case kind::FLOATINGPOINT_TO_FP_FROM_UBV: return "to_fp_unsigned";
- case kind::FLOATINGPOINT_TO_FP_GENERIC: return "to_fp_unsigned";
case kind::FLOATINGPOINT_TO_UBV: return "fp.to_ubv";
case kind::FLOATINGPOINT_TO_UBV_TOTAL: return "fp.to_ubv_total";
case kind::FLOATINGPOINT_TO_SBV: return "fp.to_sbv";
|| k == FLOATINGPOINT_TO_FP_FROM_FP
|| k == FLOATINGPOINT_TO_FP_FROM_IEEE_BV
|| k == FLOATINGPOINT_TO_FP_FROM_SBV
- || k == FLOATINGPOINT_TO_FP_FROM_REAL
- || k == FLOATINGPOINT_TO_FP_GENERIC || k == APPLY_UPDATER
+ || k == FLOATINGPOINT_TO_FP_FROM_REAL || k == APPLY_UPDATER
|| k == APPLY_TESTER;
}
indices.push_back(nm->mkConstInt(fr.getSize().significandWidth()));
}
break;
- case FLOATINGPOINT_TO_FP_GENERIC:
- {
- const FloatingPointToFPGeneric& fg =
- n.getConst<FloatingPointToFPGeneric>();
- indices.push_back(nm->mkConstInt(fg.getSize().exponentWidth()));
- indices.push_back(nm->mkConstInt(fg.getSize().significandWidth()));
- }
- break;
case APPLY_TESTER:
{
unsigned index = DType::indexOf(n);
{
opName << "to_fp_real";
}
- else if (k == FLOATINGPOINT_TO_FP_GENERIC)
- {
- opName << "to_fp_generic";
- }
else
{
opName << printer::smt2::Smt2Printer::smtKindString(k);
-constant FLOATINGPOINT_TO_FP_GENERIC_OP \
- class \
- FloatingPointToFPGeneric \
- "::cvc5::FloatingPointConvertSortHashFunction<0x11>" \
- "util/floatingpoint.h" \
- "operator for a generic to_fp"
-typerule FLOATINGPOINT_TO_FP_GENERIC_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule
-
-
-parameterized FLOATINGPOINT_TO_FP_GENERIC FLOATINGPOINT_TO_FP_GENERIC_OP 1:2 "a generic conversion to floating-point, used in parsing only"
-typerule FLOATINGPOINT_TO_FP_GENERIC ::cvc5::theory::fp::FloatingPointToFPGenericTypeRule
-
-
-
-
-
constant FLOATINGPOINT_TO_UBV_OP \
class \
FloatingPointToUBV \
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_FROM_REAL);
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_FROM_SBV);
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_FROM_UBV);
- // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_GENERIC); //
- // Needed in parsing, should be rewritten away
// d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_UBV); // Removed
// d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_SBV); // Removed
Trace("fp-registerTerm") << "TheoryFp::registerTerm(): " << node << std::endl;
Kind k = node.getKind();
- Assert(k != kind::FLOATINGPOINT_TO_FP_GENERIC && k != kind::FLOATINGPOINT_SUB
- && k != kind::FLOATINGPOINT_EQ && k != kind::FLOATINGPOINT_GEQ
- && k != kind::FLOATINGPOINT_GT);
+ Assert(k != kind::FLOATINGPOINT_SUB && k != kind::FLOATINGPOINT_EQ
+ && k != kind::FLOATINGPOINT_GEQ && k != kind::FLOATINGPOINT_GT);
// Add to the equality engine, always. This is required to ensure
// getEqualityStatus works as expected when theory combination is enabled.
<< ") found in expression?";
}
- RewriteResponse removeToFPGeneric(TNode node, bool isPreRewrite)
- {
- Assert(!isPreRewrite);
- Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC);
-
- FloatingPointToFPGeneric info =
- node.getOperator().getConst<FloatingPointToFPGeneric>();
-
- uint32_t children = node.getNumChildren();
-
- Node op;
- NodeManager* nm = NodeManager::currentNM();
-
- if (children == 1)
- {
- op = nm->mkConst(FloatingPointToFPIEEEBitVector(info));
- return RewriteResponse(REWRITE_AGAIN, nm->mkNode(op, node[0]));
- }
- Assert(children == 2);
- Assert(node[0].getType().isRoundingMode());
-
- TypeNode t = node[1].getType();
-
- if (t.isFloatingPoint())
- {
- op = nm->mkConst(FloatingPointToFPFloatingPoint(info));
- }
- else if (t.isReal())
- {
- op = nm->mkConst(FloatingPointToFPReal(info));
- }
- else
- {
- Assert(t.isBitVector());
- op = nm->mkConst(FloatingPointToFPSignedBitVector(info));
- }
-
- return RewriteResponse(REWRITE_AGAIN, nm->mkNode(op, node[0], node[1]));
- }
-
RewriteResponse removeDoubleNegation(TNode node, bool isPreRewrite)
{
Assert(node.getKind() == kind::FLOATINGPOINT_NEG);
d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_REAL] = rewrite::identity;
d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] = rewrite::identity;
d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_UBV] = rewrite::identity;
- d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::identity;
d_preRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
d_preRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
d_preRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] =
rewrite::toFPSignedBV;
d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_UBV] = rewrite::identity;
- d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] =
- rewrite::removeToFPGeneric;
d_postRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
d_postRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
d_postRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
return nodeManager->mkFloatingPointType(info.getSize());
}
-TypeNode FloatingPointToFPGenericTypeRule::computeType(NodeManager* nodeManager,
- TNode n,
- bool check)
-{
- TRACE("FloatingPointToFPGenericTypeRule");
-
- FloatingPointToFPGeneric info =
- n.getOperator().getConst<FloatingPointToFPGeneric>();
-
- if (check)
- {
- uint32_t nchildren = n.getNumChildren();
- if (nchildren == 1)
- {
- if (!n[0].getType(check).isBitVector())
- {
- throw TypeCheckingExceptionPrivate(
- n, "first argument must be a bit-vector");
- }
- }
- else
- {
- Assert(nchildren == 2);
- if (!n[0].getType(check).isRoundingMode())
- {
- throw TypeCheckingExceptionPrivate(
- n, "first argument must be a roundingmode");
- }
- TypeNode tn = n[1].getType(check);
- if (!tn.isBitVector() && !tn.isFloatingPoint() && !tn.isReal())
- {
- throw TypeCheckingExceptionPrivate(
- n, "second argument must be a bit-vector, floating-point or Real");
- }
- }
- }
- return nodeManager->mkFloatingPointType(info.getSize());
-}
-
TypeNode FloatingPointToUBVTypeRule::computeType(NodeManager* nodeManager,
TNode n,
bool check)
static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
};
-/** Generic type rule for floating-point to_fp conversion. */
-class FloatingPointToFPGenericTypeRule
-{
- public:
- static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
-};
-
/** Type rule for conversion from floating-point to unsigned bit-vector. */
class FloatingPointToUBVTypeRule
{
}
};
-class FloatingPointToFPGeneric : public FloatingPointConvertSort
-{
- public:
- /** Constructors. */
- FloatingPointToFPGeneric(uint32_t _e, uint32_t _s)
- : FloatingPointConvertSort(_e, _s)
- {
- }
- FloatingPointToFPGeneric(const FloatingPointConvertSort& old)
- : FloatingPointConvertSort(old)
- {
- }
-};
-
/**
* Base type for floating-point to bit-vector conversion.
*/
Op toFpFromReal = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 7, 6);
Op toFpFromSbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 9, 8);
Op toFpFromUbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 11, 10);
- Op toFpGen = d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 13, 12);
Op regexpLoop = d_solver.mkOp(REGEXP_LOOP, 15, 14);
ASSERT_EQ(2, bvExtract.getNumIndices());
ASSERT_EQ(2, toFpFromReal.getNumIndices());
ASSERT_EQ(2, toFpFromSbv.getNumIndices());
ASSERT_EQ(2, toFpFromUbv.getNumIndices());
- ASSERT_EQ(2, toFpGen.getNumIndices());
ASSERT_EQ(2, regexpLoop.getNumIndices());
// Operators with n indices
Op toFpFromReal = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 7, 6);
Op toFpFromSbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 9, 8);
Op toFpFromUbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 11, 10);
- Op toFpGen = d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 13, 12);
Op regexpLoop = d_solver.mkOp(REGEXP_LOOP, 15, 14);
ASSERT_EQ(1, bvExtract[0].getUInt32Value());
ASSERT_EQ(8, toFpFromSbv[1].getUInt32Value());
ASSERT_EQ(11, toFpFromUbv[0].getUInt32Value());
ASSERT_EQ(10, toFpFromUbv[1].getUInt32Value());
- ASSERT_EQ(13, toFpGen[0].getUInt32Value());
- ASSERT_EQ(12, toFpGen[1].getUInt32Value());
ASSERT_EQ(15, regexpLoop[0].getUInt32Value());
ASSERT_EQ(14, regexpLoop[1].getUInt32Value());
Op toFpFromReal = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 7, 6);
Op toFpFromSbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 9, 8);
Op toFpFromUbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 11, 10);
- Op toFpGen = d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 13, 12);
Op regexpLoop = d_solver.mkOp(REGEXP_LOOP, 15, 14);
assertEquals(2, bvExtract.getNumIndices());
assertEquals(2, toFpFromReal.getNumIndices());
assertEquals(2, toFpFromSbv.getNumIndices());
assertEquals(2, toFpFromUbv.getNumIndices());
- assertEquals(2, toFpGen.getNumIndices());
assertEquals(2, regexpLoop.getNumIndices());
// Operators with n indices
Op toFpFromReal = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 7, 6);
Op toFpFromSbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 9, 8);
Op toFpFromUbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 11, 10);
- Op toFpGen = d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 13, 12);
Op regexpLoop = d_solver.mkOp(REGEXP_LOOP, 15, 14);
assertEquals(1, bvExtract.get(0).getIntegerValue().intValue());
assertEquals(8, toFpFromSbv.get(1).getIntegerValue().intValue());
assertEquals(11, toFpFromUbv.get(0).getIntegerValue().intValue());
assertEquals(10, toFpFromUbv.get(1).getIntegerValue().intValue());
- assertEquals(13, toFpGen.get(0).getIntegerValue().intValue());
- assertEquals(12, toFpGen.get(1).getIntegerValue().intValue());
assertEquals(15, regexpLoop.get(0).getIntegerValue().intValue());
assertEquals(14, regexpLoop.get(1).getIntegerValue().intValue());
floatingpoint_to_fp_from_real = solver.mkOp(Kind.FPToFpFromReal, 4, 25)
floatingpoint_to_fp_from_sbv = solver.mkOp(Kind.FPToFpFromSbv, 4, 25)
floatingpoint_to_fp_from_ubv = solver.mkOp(Kind.FPToFpFromUbv, 4, 25)
- floatingpoint_to_fp_generic = solver.mkOp(Kind.FPToFpGeneric, 4, 25)
regexp_loop = solver.mkOp(Kind.RegexpLoop, 2, 3)
assert 2 == bitvector_extract.getNumIndices()
assert 2 == floatingpoint_to_fp_from_real.getNumIndices()
assert 2 == floatingpoint_to_fp_from_sbv.getNumIndices()
assert 2 == floatingpoint_to_fp_from_ubv.getNumIndices()
- assert 2 == floatingpoint_to_fp_generic.getNumIndices()
assert 2 == regexp_loop.getNumIndices()
# Operators with n indices
floatingpoint_to_fp_from_real = solver.mkOp(Kind.FPToFpFromReal, 7, 6)
floatingpoint_to_fp_from_sbv = solver.mkOp(Kind.FPToFpFromSbv, 9, 8)
floatingpoint_to_fp_from_ubv = solver.mkOp(Kind.FPToFpFromUbv, 11, 10)
- floatingpoint_to_fp_generic = solver.mkOp(Kind.FPToFpGeneric, 13, 12)
regexp_loop = solver.mkOp(Kind.RegexpLoop, 15, 14)
assert 1 == bitvector_extract[0].getIntegerValue()
assert 8 == floatingpoint_to_fp_from_sbv[1].getIntegerValue()
assert 11 == floatingpoint_to_fp_from_ubv[0].getIntegerValue()
assert 10 == floatingpoint_to_fp_from_ubv[1].getIntegerValue()
- assert 13 == floatingpoint_to_fp_generic[0].getIntegerValue()
- assert 12 == floatingpoint_to_fp_generic[1].getIntegerValue()
assert 15 == regexp_loop[0].getIntegerValue()
assert 14 == regexp_loop[1].getIntegerValue()
projects / cvc5.git / commitdiff