This required fixing the OpTerm handling for mkTerm functions in the API.
int main()
{
-
Solver slv;
- slv.setLogic("QF_BV"); // Set the logic
+ slv.setLogic("QF_BV"); // Set the logic
// The following example has been adapted from the book A Hacker's Delight by
// Henry S. Warren.
slv.assertFormula(assumption);
// Introduce a new variable for the new value of x after assignment.
- Term new_x = slv.mkVar("new_x", bitvector32); // x after executing code (0)
- Term new_x_ = slv.mkVar("new_x_", bitvector32); // x after executing code (1) or (2)
+ Term new_x = slv.mkVar("new_x", bitvector32); // x after executing code (0)
+ Term new_x_ =
+ slv.mkVar("new_x_", bitvector32); // x after executing code (1) or (2)
// Encoding code (0)
// new_x = x == a ? b : a;
cout << " Expect invalid. " << endl;
cout << " CVC4: " << slv.checkValidAssuming(v) << endl;
- // Assert that a is odd
+ // Assert that a is odd
OpTerm extract_op = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0);
- Term lsb_of_a = slv.mkTerm(extract_op, a);
+ Term lsb_of_a = slv.mkTerm(BITVECTOR_EXTRACT, extract_op, a);
cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl;
Term a_odd = slv.mkTerm(EQUAL, lsb_of_a, slv.mkBitVector(1u, 1u));
cout << "Assert " << a_odd << endl;
slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t);
std::cout << "t2 is " << t2 << std::endl
- << "simplify(t2) is " << slv.simplify(t2)
- << std::endl << std::endl;
+ << "simplify(t2) is " << slv.simplify(t2) << std::endl
+ << std::endl;
// You can also iterate over a Datatype to get all its constructors,
// and over a DatatypeConstructor to get all its "args" (selectors)
- for (Datatype::const_iterator i = consList.begin();
- i != consList.end();
- ++i)
+ for (Datatype::const_iterator i = consList.begin(); i != consList.end(); ++i)
{
std::cout << "ctor: " << *i << std::endl;
- for (DatatypeConstructor::const_iterator j = (*i).begin();
- j != (*i).end();
+ for (DatatypeConstructor::const_iterator j = (*i).begin(); j != (*i).end();
++j)
{
std::cout << " + arg: " << *j << std::endl;
// This example builds a simple parameterized list of sort T, with one
// constructor "cons".
Sort sort = slv.mkParamSort("T");
- DatatypeDecl paramConsListSpec("paramlist", sort); // give the datatype a name
+ DatatypeDecl paramConsListSpec("paramlist",
+ sort); // give the datatype a name
DatatypeConstructorDecl paramCons("cons");
DatatypeConstructorDecl paramNil("nil");
DatatypeSelectorDecl paramHead("head", sort);
Term head_a = slv.mkTerm(
APPLY_SELECTOR, paramConsList["cons"].getSelectorTerm("head"), a);
- std::cout << "head_a is " << head_a << " of sort " << head_a.getSort()
+ std::cout << "head_a is " << head_a << " of sort " << head_a.getSort()
<< std::endl
<< "sort of cons is "
<< paramConsList.getConstructorTerm("cons").getSort() << std::endl
// Second, it is "resolved" to an actual sort, at which point function
// symbols are assigned to its constructors, selectors, and testers.
- DatatypeDecl consListSpec("list"); // give the datatype a name
+ DatatypeDecl consListSpec("list"); // give the datatype a name
DatatypeConstructorDecl cons("cons");
DatatypeSelectorDecl head("head", slv.getIntegerSort());
DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
DatatypeConstructorDecl nil("nil");
consListSpec.addConstructor(nil);
- std::cout << "spec is:" << std::endl
- << consListSpec << std::endl;
+ std::cout << "spec is:" << std::endl << consListSpec << std::endl;
// Keep in mind that "DatatypeDecl" is the specification class for
// datatypes---"DatatypeDecl" is not itself a CVC4 Sort.
test(slv, consListSort);
- std::cout << std::endl << ">>> Alternatively, use declareDatatype" << std::endl;
+ std::cout << std::endl
+ << ">>> Alternatively, use declareDatatype" << std::endl;
std::cout << std::endl;
- std::vector<DatatypeConstructorDecl> ctors = { cons, nil };
+ std::vector<DatatypeConstructorDecl> ctors = {cons, nil};
Sort consListSort2 = slv.declareDatatype("list2", ctors);
test(slv, consListSort2);
-
return 0;
}
Term x = slv.mkVar("a", bitvector32);
OpTerm ext_31_1 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1);
- Term x_31_1 = slv.mkTerm(ext_31_1, x);
+ Term x_31_1 = slv.mkTerm(BITVECTOR_EXTRACT, ext_31_1, x);
OpTerm ext_30_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 30, 0);
- Term x_30_0 = slv.mkTerm(ext_30_0, x);
+ Term x_30_0 = slv.mkTerm(BITVECTOR_EXTRACT, ext_30_0, x);
OpTerm ext_31_31 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 31);
- Term x_31_31 = slv.mkTerm(ext_31_31, x);
+ Term x_31_31 = slv.mkTerm(BITVECTOR_EXTRACT, ext_31_31, x);
OpTerm ext_0_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0);
- Term x_0_0 = slv.mkTerm(ext_0_0, x);
+ Term x_0_0 = slv.mkTerm(BITVECTOR_EXTRACT, ext_0_0, x);
Term eq = slv.mkTerm(EQUAL, x_31_1, x_30_0);
cout << " Asserting: " << eq << endl;
DatatypeSelector::~DatatypeSelector() {}
+bool DatatypeSelector::isResolved() const { return d_stor->isResolved(); }
+
+OpTerm DatatypeSelector::getSelectorTerm() const
+{
+ CVC4_API_CHECK(isResolved()) << "Expected resolved datatype selector.";
+ return d_stor->getSelector();
+}
+
std::string DatatypeSelector::toString() const
{
std::stringstream ss;
bool DatatypeConstructor::isResolved() const { return d_ctor->isResolved(); }
-Term DatatypeConstructor::getConstructorTerm() const
+OpTerm DatatypeConstructor::getConstructorTerm() const
{
CVC4_API_CHECK(isResolved()) << "Expected resolved datatype constructor.";
- return Term(d_ctor->getConstructor());
+ return OpTerm(d_ctor->getConstructor());
}
DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const
return (*d_ctor)[name];
}
-Term DatatypeConstructor::getSelectorTerm(const std::string& name) const
+OpTerm DatatypeConstructor::getSelectorTerm(const std::string& name) const
{
// CHECK: cons with name exists?
// CHECK: is resolved?
return (*d_dtype)[name];
}
-Term Datatype::getConstructorTerm(const std::string& name) const
+OpTerm Datatype::getConstructorTerm(const std::string& name) const
{
// CHECK: cons with name exists?
// CHECK: is resolved?
<< "Only operator-style terms are created with mkTerm(), "
"to create variables and constants see mkVar(), mkBoundVar(), "
"and mkConst().";
- if (nchildren)
- {
- const uint32_t n =
- nchildren - (mk == CVC4::kind::metakind::PARAMETERIZED ? 1 : 0);
- CVC4_API_KIND_CHECK_EXPECTED(n >= minArity(kind) && n <= maxArity(kind),
- kind)
- << "Terms with kind " << kindToString(kind) << " must have at least "
- << minArity(kind) << " children and at most " << maxArity(kind)
- << " children (the one under construction has " << n << ")";
- }
+ CVC4_API_KIND_CHECK_EXPECTED(
+ nchildren >= minArity(kind) && nchildren <= maxArity(kind), kind)
+ << "Terms with kind " << kindToString(kind) << " must have at least "
+ << minArity(kind) << " children and at most " << maxArity(kind)
+ << " children (the one under construction has " << nchildren << ")";
}
-void Solver::checkMkOpTerm(OpTerm opTerm, uint32_t nchildren) const
+void Solver::checkMkOpTerm(Kind kind, OpTerm opTerm, uint32_t nchildren) const
{
- const Kind kind = opTerm.getKind();
Assert(isDefinedIntKind(extToIntKind(kind)));
const CVC4::Kind int_kind = extToIntKind(kind);
- const CVC4::Kind int_op_kind =
+ const CVC4::Kind int_op_kind = opTerm.d_expr->getKind();
+ const CVC4::Kind int_op_to_kind =
NodeManager::operatorToKind(opTerm.d_expr->getNode());
- CVC4_API_ARG_CHECK_EXPECTED(int_kind == kind::BUILTIN
- || CVC4::kind::metaKindOf(int_op_kind)
- == kind::metakind::PARAMETERIZED,
- opTerm)
+ CVC4_API_ARG_CHECK_EXPECTED(
+ int_kind == int_op_to_kind
+ || (kind == APPLY_CONSTRUCTOR
+ && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND)
+ || (kind == APPLY_SELECTOR
+ && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND)
+ || (kind == APPLY_UF && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND),
+ kind)
+ << "kind that matches kind associated with given operator term";
+ CVC4_API_ARG_CHECK_EXPECTED(
+ int_op_kind == CVC4::kind::BUILTIN
+ || CVC4::kind::metaKindOf(int_kind) == kind::metakind::PARAMETERIZED,
+ opTerm)
<< "This term constructor is for parameterized kinds only";
- if (nchildren)
- {
- uint32_t min_arity = ExprManager::minArity(int_op_kind);
- uint32_t max_arity = ExprManager::maxArity(int_op_kind);
- CVC4_API_KIND_CHECK_EXPECTED(
- nchildren >= min_arity && nchildren <= max_arity, kind)
- << "Terms with kind " << kindToString(kind) << " must have at least "
- << min_arity << " children and at most " << max_arity
- << " children (the one under construction has " << nchildren << ")";
- }
+ uint32_t min_arity = ExprManager::minArity(int_kind);
+ uint32_t max_arity = ExprManager::maxArity(int_kind);
+ CVC4_API_KIND_CHECK_EXPECTED(nchildren >= min_arity && nchildren <= max_arity,
+ kind)
+ << "Terms with kind " << kindToString(kind) << " must have at least "
+ << min_arity << " children and at most " << max_arity
+ << " children (the one under construction has " << nchildren << ")";
}
Term Solver::mkTerm(Kind kind) const
}
}
-Term Solver::mkTerm(OpTerm opTerm, Term child) const
+Term Solver::mkTerm(Kind kind, OpTerm opTerm) const
+{
+ try
+ {
+ checkMkOpTerm(kind, opTerm, 0);
+ const CVC4::Kind int_kind = extToIntKind(kind);
+ Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr);
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (const CVC4::TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
+}
+
+Term Solver::mkTerm(Kind kind, OpTerm opTerm, Term child) const
{
try
{
CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
- checkMkOpTerm(opTerm, 1);
- Term res = d_exprMgr->mkExpr(*opTerm.d_expr, *child.d_expr);
+ checkMkOpTerm(kind, opTerm, 1);
+ const CVC4::Kind int_kind = extToIntKind(kind);
+ Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, *child.d_expr);
(void)res.d_expr->getType(true); /* kick off type checking */
return res;
}
}
}
-Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2) const
+Term Solver::mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const
{
try
{
CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
- checkMkOpTerm(opTerm, 2);
- Term res =
- d_exprMgr->mkExpr(*opTerm.d_expr, *child1.d_expr, *child2.d_expr);
+ checkMkOpTerm(kind, opTerm, 2);
+ const CVC4::Kind int_kind = extToIntKind(kind);
+ Term res = d_exprMgr->mkExpr(
+ int_kind, *opTerm.d_expr, *child1.d_expr, *child2.d_expr);
(void)res.d_expr->getType(true); /* kick off type checking */
return res;
}
}
}
-Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const
+Term Solver::mkTerm(
+ Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) const
{
try
{
CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term";
- checkMkOpTerm(opTerm, 3);
- Term res = d_exprMgr->mkExpr(
- *opTerm.d_expr, *child1.d_expr, *child2.d_expr, *child3.d_expr);
+ checkMkOpTerm(kind, opTerm, 3);
+ const CVC4::Kind int_kind = extToIntKind(kind);
+ Term res = d_exprMgr->mkExpr(int_kind,
+ *opTerm.d_expr,
+ *child1.d_expr,
+ *child2.d_expr,
+ *child3.d_expr);
(void)res.d_expr->getType(true); /* kick off type checking */
return res;
}
}
}
-Term Solver::mkTerm(OpTerm opTerm, const std::vector<Term>& children) const
+Term Solver::mkTerm(Kind kind,
+ OpTerm opTerm,
+ const std::vector<Term>& children) const
{
try
{
!children[i].isNull(), "parameter term", children[i], i)
<< "non-null term";
}
- checkMkOpTerm(opTerm, children.size());
+ checkMkOpTerm(kind, opTerm, children.size());
+ const CVC4::Kind int_kind = extToIntKind(kind);
std::vector<Expr> echildren = termVectorToExprs(children);
- Term res = d_exprMgr->mkExpr(*opTerm.d_expr, echildren);
+ Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, echildren);
(void)res.d_expr->getType(true); /* kick off type checking */
return res;
}
{
CVC4_API_CHECK(sorts.size() == terms.size())
<< "Expected the same number of sorts and elements";
- std::vector<Term> args;
- for (size_t i = 0, size = sorts.size(); i < size; i++)
+ try
{
- args.push_back(ensureTermSort(terms[i], sorts[i]));
- }
+ std::vector<CVC4::Expr> args;
+ for (size_t i = 0, size = sorts.size(); i < size; i++)
+ {
+ args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_expr);
+ }
- Sort s = mkTupleSort(sorts);
- Datatype dt = s.getDatatype();
- args.insert(args.begin(), dt[0].getConstructorTerm());
- return mkTerm(APPLY_CONSTRUCTOR, args);
+ Sort s = mkTupleSort(sorts);
+ Datatype dt = s.getDatatype();
+ Term res = d_exprMgr->mkExpr(extToIntKind(APPLY_CONSTRUCTOR),
+ *dt[0].getConstructorTerm().d_expr,
+ args);
+ (void)res.d_expr->getType(true); /* kick off type checking */
+ return res;
+ }
+ catch (const CVC4::TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
std::vector<Expr> Solver::termVectorToExprs(
}
}
-Term Solver::ensureTermSort(const Term& t, const Sort& s) const
+Term Solver::ensureTermSort(const Term& term, const Sort& sort) const
{
- CVC4_API_CHECK(t.getSort() == s || (t.getSort().isInteger() && s.isReal()))
+ CVC4_API_CHECK(term.getSort() == sort
+ || (term.getSort().isInteger() && sort.isReal()))
<< "Expected conversion from Int to Real";
- if (t.getSort() == s)
+ Sort t = term.getSort();
+ if (term.getSort() == sort)
{
- return t;
+ return term;
}
// Integers are reals, too
- Assert(t.getSort().isReal());
- Term res = t;
- if (t.getSort().isInteger())
+ Assert(t.isReal());
+ Term res = term;
+ if (t.isInteger())
{
// Must cast to Real to ensure correct type is passed to parametric type
// constructors. We do this cast using division with 1. This has the
// advantage wrt using TO_REAL since (constant) division is always included
// in the theory.
- res = mkTerm(DIVISION, *t.d_expr, mkReal(1));
+ res = Term(d_exprMgr->mkExpr(extToIntKind(DIVISION),
+ *res.d_expr,
+ d_exprMgr->mkConst(CVC4::Rational(1))));
}
- Assert(res.getSort() == s);
+ Assert(res.getSort() == sort);
return res;
}
*/
~DatatypeSelector();
+ /**
+ * @return true if this datatype selector has been resolved.
+ */
+ bool isResolved() const;
+
+ /**
+ * Get the selector operator of this datatype selector.
+ * @return the selector operator
+ */
+ OpTerm getSelectorTerm() const;
+
/**
* @return a string representation of this datatype selector
*/
* Get the constructor operator of this datatype constructor.
* @return the constructor operator
*/
- Term getConstructorTerm() const;
+ OpTerm getConstructorTerm() const;
/**
* Get the datatype selector with the given name.
* @param name the name of the datatype selector
* @return a term representing the datatype selector with the given name
*/
- Term getSelectorTerm(const std::string& name) const;
+ OpTerm getSelectorTerm(const std::string& name) const;
/**
* @return a string representation of this datatype constructor
* similarly-named constructors, the
* first is returned.
*/
- Term getConstructorTerm(const std::string& name) const;
+ OpTerm getConstructorTerm(const std::string& name) const;
/** Get the number of constructors for this Datatype. */
size_t getNumConstructors() const;
Term mkTerm(Kind kind, const std::vector<Term>& children) const;
/**
- * Create unary term from a given operator term.
+ * Create nullary term of given kind from a given operator term.
+ * Create operator terms with mkOpTerm().
+ * @param kind the kind of the term
+ * @param the operator term
+ * @return the Term
+ */
+ Term mkTerm(Kind kind, OpTerm opTerm) const;
+
+ /**
+ * Create unary term of given kind from a given operator term.
* Create operator terms with mkOpTerm().
+ * @param kind the kind of the term
* @param the operator term
* @child the child of the term
* @return the Term
*/
- Term mkTerm(OpTerm opTerm, Term child) const;
+ Term mkTerm(Kind kind, OpTerm opTerm, Term child) const;
/**
- * Create binary term from a given operator term.
+ * Create binary term of given kind from a given operator term.
+ * @param kind the kind of the term
* Create operator terms with mkOpTerm().
* @param the operator term
* @child1 the first child of the term
* @child2 the second child of the term
* @return the Term
*/
- Term mkTerm(OpTerm opTerm, Term child1, Term child2) const;
+ Term mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const;
/**
- * Create ternary term from a given operator term.
+ * Create ternary term of given kind from a given operator term.
* Create operator terms with mkOpTerm().
+ * @param kind the kind of the term
* @param the operator term
* @child1 the first child of the term
* @child2 the second child of the term
* @child3 the third child of the term
* @return the Term
*/
- Term mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const;
+ Term mkTerm(
+ Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) const;
/**
- * Create n-ary term from a given operator term.
+ * Create n-ary term of given kind from a given operator term.
* Create operator terms with mkOpTerm().
+ * @param kind the kind of the term
* @param the operator term
* @children the children of the term
* @return the Term
*/
- Term mkTerm(OpTerm opTerm, const std::vector<Term>& children) const;
+ Term mkTerm(Kind kind,
+ OpTerm opTerm,
+ const std::vector<Term>& children) const;
/**
* Create a tuple term. Terms are automatically converted if sorts are
/* Helper to convert a vector of sorts to internal types. */
std::vector<Expr> termVectorToExprs(const std::vector<Term>& vector) const;
/* Helper to check for API misuse in mkTerm functions. */
- void checkMkOpTerm(OpTerm opTerm, uint32_t nchildren) const;
+ void checkMkOpTerm(Kind kind, OpTerm opTerm, uint32_t nchildren) const;
/* Helper to check for API misuse in mkOpTerm functions. */
void checkMkTerm(Kind kind, uint32_t nchildren) const;
/* Helper for mk-functions that call d_exprMgr->mkConst(). */
/**
* Constructor application.
* Paramters: n > 0
- * -[1]: Constructor
+ * -[1]: Constructor (operator term)
* -[2]..[n]: Parameters to the constructor
* Create with:
- * mkTerm(Kind kind)
- * mkTerm(Kind kind, Term child)
- * mkTerm(Kind kind, Term child1, Term child2)
- * mkTerm(Kind kind, Term child1, Term child2, Term child3)
- * mkTerm(Kind kind, const std::vector<Term>& children)
+ * mkTerm(Kind kind, OpTerm opTerm)
+ * mkTerm(Kind kind, OpTerm opTerm, Term child)
+ * mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2)
+ * mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3)
+ * mkTerm(Kind kind, OpTerm opTerm, const std::vector<Term>& children)
*/
- APPLY_SELECTOR,
+ APPLY_CONSTRUCTOR,
/**
* Datatype selector application.
* Parameters: 1
- * -[1]: Datatype term (undefined if mis-applied)
+ * -[1]: Selector (operator term)
+ * -[2]: Datatype term (undefined if mis-applied)
* Create with:
- * mkTerm(Kind kind, Term child)
+ * mkTerm(Kind kind, OpTerm opTerm, Term child)
*/
- APPLY_CONSTRUCTOR,
+ APPLY_SELECTOR,
/**
* Datatype selector application.
* Parameters: 1
- * -[1]: Datatype term (defined rigidly if mis-applied)
+ * -[1]: Selector (operator term)
+ * -[2]: Datatype term (defined rigidly if mis-applied)
* Create with:
- * mkTerm(Kind kind, Term child)
+ * mkTerm(Kind kind, OpTerm opTerm, Term child)
*/
APPLY_SELECTOR_TOTAL,
/**
}
}
-Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
+Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children)
+{
+ const size_t nchildren = children.size();
const kind::MetaKind mk = kind::metaKindOf(kind);
- const unsigned n = children.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
PrettyCheckArgument(
- mk == kind::metakind::PARAMETERIZED ||
- mk == kind::metakind::OPERATOR, kind,
+ mk == kind::metakind::PARAMETERIZED || mk == kind::metakind::OPERATOR,
+ kind,
"Only operator-style expressions are made with mkExpr(); "
"to make variables and constants, see mkVar(), mkBoundVar(), "
"and mkConst().");
PrettyCheckArgument(
- n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
+ mk != kind::metakind::PARAMETERIZED || nchildren > 0,
+ kind,
+ "Terms with kind %s must have an operator expression as first argument",
+ kind::kindToString(kind).c_str());
+ const size_t n = nchildren - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
+ PrettyCheckArgument(n >= minArity(kind) && n <= maxArity(kind),
+ kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind),
+ maxArity(kind),
+ n);
NodeManagerScope nms(d_nodeManager);
void testMkSepNil();
void testMkString();
void testMkTerm();
+ void testMkTermFromOpTerm();
void testMkTrue();
void testMkTuple();
void testMkUninterpretedConst();
std::vector<Term> v3 = {a, d_solver->mkTrue()};
std::vector<Term> v4 = {d_solver->mkReal(1), d_solver->mkReal(2)};
std::vector<Term> v5 = {d_solver->mkReal(1), Term()};
- OpTerm opterm1 = d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 2, 1);
- OpTerm opterm2 = d_solver->mkOpTerm(DIVISIBLE_OP, 1);
- OpTerm opterm3 = d_solver->mkOpTerm(CHAIN_OP, EQUAL);
+ std::vector<Term> v6 = {};
// mkTerm(Kind kind) const
TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(PI));
TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(EQUAL, v1));
TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, v2), CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, v3), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(DISTINCT, v6), CVC4ApiException&);
+}
- // mkTerm(OpTerm opTerm, Term child) const
- TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a));
- TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, a), CVC4ApiException&);
- TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, Term()), CVC4ApiException&);
+void SolverBlack::testMkTermFromOpTerm()
+{
+ Sort bv32 = d_solver->mkBitVectorSort(32);
+ Term a = d_solver->mkVar("a", bv32);
+ Term b = d_solver->mkVar("b", bv32);
+ std::vector<Term> v1 = {d_solver->mkReal(1), d_solver->mkReal(2)};
+ std::vector<Term> v2 = {d_solver->mkReal(1), Term()};
+ std::vector<Term> v3 = {};
+ // simple operator terms
+ OpTerm opterm1 = d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 2, 1);
+ OpTerm opterm2 = d_solver->mkOpTerm(DIVISIBLE_OP, 1);
+ OpTerm opterm3 = d_solver->mkOpTerm(CHAIN_OP, EQUAL);
+ // list datatype
+ Sort sort = d_solver->mkParamSort("T");
+ DatatypeDecl listDecl("paramlist", sort);
+ DatatypeConstructorDecl cons("cons");
+ DatatypeConstructorDecl nil("nil");
+ DatatypeSelectorDecl head("head", sort);
+ DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
+ cons.addSelector(head);
+ cons.addSelector(tail);
+ listDecl.addConstructor(cons);
+ listDecl.addConstructor(nil);
+ Sort listSort = d_solver->mkDatatypeSort(listDecl);
+ Sort intListSort =
+ listSort.instantiate(std::vector<Sort>{d_solver->getIntegerSort()});
+ Term c = d_solver->declareFun("c", intListSort);
+ Datatype list = listSort.getDatatype();
+ // list datatype constructor and selector operator terms
+ OpTerm consTerm1 = list.getConstructorTerm("cons");
+ OpTerm consTerm2 = list.getConstructor("cons").getConstructorTerm();
+ OpTerm nilTerm1 = list.getConstructorTerm("nil");
+ OpTerm nilTerm2 = list.getConstructor("nil").getConstructorTerm();
+ OpTerm headTerm1 = list["cons"].getSelectorTerm("head");
+ OpTerm headTerm2 = list["cons"].getSelector("head").getSelectorTerm();
+ OpTerm tailTerm1 = list["cons"].getSelectorTerm("tail");
+ OpTerm tailTerm2 = list["cons"]["tail"].getSelectorTerm();
+
+ // mkTerm(Kind kind, OpTerm opTerm) const
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1));
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm2));
+ TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm2),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, opterm1),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, headTerm1),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1),
+ CVC4ApiException&);
- // mkTerm(OpTerm opTerm, Term child1, Term child2) const
+ // mkTerm(Kind kind, OpTerm opTerm, Term child) const
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a));
TS_ASSERT_THROWS_NOTHING(
- d_solver->mkTerm(opterm3, d_solver->mkReal(1), d_solver->mkReal(2)));
- TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&);
- TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, d_solver->mkReal(1), Term()),
- CVC4ApiException&);
- TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, Term(), d_solver->mkReal(1)),
+ d_solver->mkTerm(DIVISIBLE, opterm2, d_solver->mkReal(1)));
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, headTerm1, c));
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2, c));
+ TS_ASSERT_THROWS(d_solver->mkTerm(DIVISIBLE, opterm1, a), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(DIVISIBLE, opterm2, a), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, Term()),
CVC4ApiException&);
+ TS_ASSERT_THROWS(
+ d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0)),
+ CVC4ApiException&);
- // mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const
+ // mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const
TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(
- opterm3, d_solver->mkReal(1), d_solver->mkReal(1), d_solver->mkReal(2)));
- TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b, a), CVC4ApiException&);
+ CHAIN, opterm3, d_solver->mkReal(1), d_solver->mkReal(2)));
+ TS_ASSERT_THROWS_NOTHING(
+ d_solver->mkTerm(APPLY_CONSTRUCTOR,
+ consTerm1,
+ d_solver->mkReal(0),
+ d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));
+ TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a, b),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(
+ d_solver->mkTerm(CHAIN, opterm3, d_solver->mkReal(1), Term()),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(
+ d_solver->mkTerm(CHAIN, opterm3, Term(), d_solver->mkReal(1)),
+ CVC4ApiException&);
+
+ // mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3)
+ // const
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(CHAIN,
+ opterm3,
+ d_solver->mkReal(1),
+ d_solver->mkReal(1),
+ d_solver->mkReal(2)));
+ TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a, b, a),
+ CVC4ApiException&);
TS_ASSERT_THROWS(
d_solver->mkTerm(
- opterm3, d_solver->mkReal(1), d_solver->mkReal(1), Term()),
+ CHAIN, opterm3, d_solver->mkReal(1), d_solver->mkReal(1), Term()),
CVC4ApiException&);
// mkTerm(OpTerm opTerm, const std::vector<Term>& children) const
- TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm3, v4));
- TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, v5), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(CHAIN, opterm3, v1));
+ TS_ASSERT_THROWS(d_solver->mkTerm(CHAIN, opterm3, v2), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(CHAIN, opterm3, v3), CVC4ApiException&);
}
void SolverBlack::testMkTrue()
projects / cvc5.git / commitdiff