// which is equivalent to consList["cons"].getConstructor(). Note that
// "nil" is a constructor too, so it needs to be applied with
// APPLY_CONSTRUCTOR, even though it has no arguments.
- Term t = slv.mkTerm(consList.getConstructorTerm("cons"),
- slv.mkReal(0),
- slv.mkTerm(consList.getConstructorTerm("nil")));
+ Term t = slv.mkTerm(
+ APPLY_CONSTRUCTOR,
+ consList.getConstructorTerm("cons"),
+ slv.mkReal(0),
+ slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
std::cout << "t is " << t << std::endl
<< "sort of cons is "
// Here we first get the DatatypeConstructor for cons (with
// consList["cons"]) in order to get the "head" selector symbol
// to apply.
- Term t2 = slv.mkTerm(consList["cons"].getSelectorTerm("head"), t);
+ Term t2 =
+ slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t);
std::cout << "t2 is " << t2 << std::endl
<< "simplify(t2) is " << slv.simplify(t2) << std::endl
Term a = slv.mkConst(paramConsIntListSort, "a");
std::cout << "term " << a << " is of sort " << a.getSort() << std::endl;
- Term head_a = slv.mkTerm(paramConsList["cons"].getSelectorTerm("head"), a);
+ 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::endl
<< "sort of cons is "
bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; }
+/** Returns true if the internal kind is one where the API term structure
+ * differs from internal structure. This happens for APPLY_* kinds.
+ * The API takes a "higher-order" perspective and treats functions as well
+ * as datatype constructors/selectors/testers as terms
+ * but interally they are not
+ */
+bool isApplyKind(CVC4::Kind k)
+{
+ return (k == CVC4::Kind::APPLY_UF || k == CVC4::Kind::APPLY_CONSTRUCTOR
+ || k == CVC4::Kind::APPLY_SELECTOR || k == CVC4::Kind::APPLY_TESTER);
+}
+
#ifdef CVC4_ASSERTIONS
bool isDefinedIntKind(CVC4::Kind k)
{
{
Assert(isDefinedKind(k));
Assert(isDefinedIntKind(extToIntKind(k)));
- return CVC4::ExprManager::maxArity(extToIntKind(k));
+ uint32_t max = CVC4::ExprManager::maxArity(extToIntKind(k));
+
+ // special cases for API level
+ // higher-order logic perspective at API
+ // functions/constructors/selectors/testers are terms
+ if (isApplyKind(extToIntKind(k))
+ && max != std::numeric_limits<uint32_t>::max()) // be careful not to
+ // overflow
+ {
+ max++;
+ }
+ return max;
}
+
} // namespace
std::string kindToString(Kind k)
CVC4_API_CHECK_NOT_NULL;
CVC4_API_CHECK(d_expr->hasOperator())
<< "Expecting Term to have an Op when calling getOp()";
- CVC4::Expr op = d_expr->getOperator();
- CVC4::Type t = op.getType();
- // special cases for Datatype operators
- if (t.isSelector())
+ // special cases for parameterized operators that are not indexed operators
+ // the API level differs from the internal structure
+ // indexed operators are stored in Ops
+ // whereas functions and datatype operators are terms, and the Op
+ // is one of the APPLY_* kinds
+ if (isApplyKind(d_expr->getKind()))
{
- return Op(APPLY_SELECTOR, op);
+ return Op(intToExtKind(d_expr->getKind()));
}
- else if (t.isConstructor())
+ else if (d_expr->isParameterized())
{
- return Op(APPLY_CONSTRUCTOR, op);
- }
- else if (t.isTester())
- {
- return Op(APPLY_TESTER, op);
+ // it's an indexed operator
+ // so we should return the indexed op
+ CVC4::Expr op = d_expr->getOperator();
+ return Op(intToExtKind(d_expr->getKind()), op);
}
else
{
- return Op(intToExtKind(op.getKind()), op);
+ return Op(intToExtKind(d_expr->getKind()));
}
}
bool Term::isNull() const { return isNullHelper(); }
-bool Term::isParameterized() const
-{
- CVC4_API_CHECK_NOT_NULL;
- return d_expr->isParameterized();
-}
-
Term Term::notTerm() const
{
CVC4_API_CHECK_NOT_NULL;
Term Term::const_iterator::operator*() const
{
Assert(d_orig_expr != nullptr);
- if (!d_pos && (d_orig_expr->getKind() == CVC4::Kind::APPLY_UF))
+ // this term has an extra child (mismatch between API and internal structure)
+ // the extra child will be the first child
+ bool extra_child = isApplyKind(d_orig_expr->getKind());
+
+ if (!d_pos && extra_child)
{
return Term(d_orig_expr->getOperator());
}
else
{
uint32_t idx = d_pos;
- if (d_orig_expr->getKind() == CVC4::Kind::APPLY_UF)
+ if (extra_child)
{
Assert(idx > 0);
--idx;
Term::const_iterator Term::end() const
{
int endpos = d_expr->getNumChildren();
- if (d_expr->getKind() == CVC4::Kind::APPLY_UF)
+ // special cases for APPLY_*
+ // the API differs from the internal structure
+ // the API takes a "higher-order" perspective and the applied
+ // function or datatype constructor/selector/tester is a Term
+ // which means it needs to be one of the children, even though
+ // internally it is not
+ if (isApplyKind(d_expr->getKind()))
{
// one more child if this is a UF application (count the UF as a child)
++endpos;
bool DatatypeSelector::isResolved() const { return d_stor->isResolved(); }
-Op DatatypeSelector::getSelectorTerm() const
+Term DatatypeSelector::getSelectorTerm() const
{
CVC4_API_CHECK(isResolved()) << "Expected resolved datatype selector.";
- CVC4::Expr sel = d_stor->getSelector();
- return Op(APPLY_SELECTOR, sel);
+ Term sel = d_stor->getSelector();
+ return sel;
}
std::string DatatypeSelector::toString() const
bool DatatypeConstructor::isResolved() const { return d_ctor->isResolved(); }
-Op DatatypeConstructor::getConstructorTerm() const
+Term DatatypeConstructor::getConstructorTerm() const
{
CVC4_API_CHECK(isResolved()) << "Expected resolved datatype constructor.";
- CVC4::Expr ctor = d_ctor->getConstructor();
- return Op(APPLY_CONSTRUCTOR, ctor);
+ Term ctor = d_ctor->getConstructor();
+ return ctor;
}
DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const
return (*d_ctor)[name];
}
-Op DatatypeConstructor::getSelectorTerm(const std::string& name) const
+Term DatatypeConstructor::getSelectorTerm(const std::string& name) const
{
// CHECK: cons with name exists?
// CHECK: is resolved?
- CVC4::Expr sel = d_ctor->getSelector(name);
- return Op(APPLY_SELECTOR, sel);
+ Term sel = d_ctor->getSelector(name);
+ return sel;
}
DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
return (*d_dtype)[name];
}
-Op Datatype::getConstructorTerm(const std::string& name) const
+Term Datatype::getConstructorTerm(const std::string& name) const
{
// CHECK: cons with name exists?
// CHECK: is resolved?
- CVC4::Expr ctor = d_dtype->getConstructor(name);
- return Op(APPLY_CONSTRUCTOR, ctor);
+ Term ctor = d_dtype->getConstructor(name);
+ return ctor;
}
size_t Datatype::getNumConstructors() const
*/
bool isNull() const;
- /**
- * @return true if this expression is parameterized.
- *
- * !!! The below documentation is not accurate until we have a way of getting
- * operators from terms.
- *
- * In detail, a term that is parameterized is one that has an operator that
- * must be provided in addition to its kind to construct it. For example,
- * say we want to re-construct a Term t where its children a1, ..., an are
- * replaced by b1 ... bn. Then there are two cases:
- * (1) If t is parametric, call:
- * mkTerm(t.getKind(), t.getOperator(), b1, ..., bn )
- * (2) If t is not parametric, call:
- * mkTerm(t.getKind(), b1, ..., bn )
- */
- bool isParameterized() const;
-
/**
* Boolean negation.
* @return the Boolean negation of this term
/**
* Get the selector operator of this datatype selector.
- * @return the selector operator
+ * @return the selector term
*/
- Op getSelectorTerm() const;
+ Term getSelectorTerm() const;
/**
* @return a string representation of this datatype selector
/**
* Get the constructor operator of this datatype constructor.
- * @return the constructor operator
+ * @return the constructor term
*/
- Op getConstructorTerm() const;
+ Term 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
*/
- Op getSelectorTerm(const std::string& name) const;
+ Term getSelectorTerm(const std::string& name) const;
/**
* @return a string representation of this datatype constructor
* similarly-named constructors, the
* first is returned.
*/
- Op getConstructorTerm(const std::string& name) const;
+ Term getConstructorTerm(const std::string& name) const;
/** Get the number of constructors for this Datatype. */
size_t getNumConstructors() const;
Term c = d_solver->mkConst(intListSort, "c");
Datatype list = listSort.getDatatype();
// list datatype constructor and selector operator terms
- Op consTerm1 = list.getConstructorTerm("cons");
- Op consTerm2 = list.getConstructor("cons").getConstructorTerm();
- Op nilTerm1 = list.getConstructorTerm("nil");
- Op nilTerm2 = list.getConstructor("nil").getConstructorTerm();
- Op headTerm1 = list["cons"].getSelectorTerm("head");
- Op headTerm2 = list["cons"].getSelector("head").getSelectorTerm();
- Op tailTerm1 = list["cons"].getSelectorTerm("tail");
- Op tailTerm2 = list["cons"]["tail"].getSelectorTerm();
-
- // mkTerm(Kind kind, Op op) const
- TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(nilTerm1));
- TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(nilTerm2));
- TS_ASSERT_THROWS(d_solver->mkTerm(consTerm1), CVC4ApiException&);
- TS_ASSERT_THROWS(d_solver->mkTerm(consTerm2), CVC4ApiException&);
+ Term consTerm1 = list.getConstructorTerm("cons");
+ Term consTerm2 = list.getConstructor("cons").getConstructorTerm();
+ Term nilTerm1 = list.getConstructorTerm("nil");
+ Term nilTerm2 = list.getConstructor("nil").getConstructorTerm();
+ Term headTerm1 = list["cons"].getSelectorTerm("head");
+ Term headTerm2 = list["cons"].getSelector("head").getSelectorTerm();
+ Term tailTerm1 = list["cons"].getSelectorTerm("tail");
+ Term tailTerm2 = list["cons"]["tail"].getSelectorTerm();
+
+ // mkTerm(Op op, Term term) 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_SELECTOR, nilTerm1),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, consTerm1),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm2),
+ CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&);
- TS_ASSERT_THROWS(d_solver->mkTerm(headTerm1), CVC4ApiException&);
- TS_ASSERT_THROWS(d_solver->mkTerm(tailTerm2), CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, headTerm1),
+ CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&);
- // mkTerm(Kind kind, Op op, Term child) const
+ // mkTerm(Op op, Term child) const
TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a));
TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm2, d_solver->mkReal(1)));
- TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(headTerm1, c));
- TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(tailTerm2, c));
+ 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(opterm2, a), CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, Term()), CVC4ApiException&);
- TS_ASSERT_THROWS(d_solver->mkTerm(consTerm1, d_solver->mkReal(0)),
- CVC4ApiException&);
+ TS_ASSERT_THROWS(
+ d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0)),
+ CVC4ApiException&);
- // mkTerm(Kind kind, Op op, Term child1, Term child2) const
+ // mkTerm(Op op, Term child1, Term child2) const
TS_ASSERT_THROWS_NOTHING(
d_solver->mkTerm(opterm3, d_solver->mkReal(1), d_solver->mkReal(2)));
- TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(
- consTerm1, d_solver->mkReal(0), d_solver->mkTerm(nilTerm1)));
+ 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(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)),
CVC4ApiException&);
- // mkTerm(Kind kind, Op op, Term child1, Term child2, Term child3)
+ // mkTerm(Op op, Term child1, Term child2, Term child3)
// const
TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(
opterm3, d_solver->mkReal(1), d_solver->mkReal(1), d_solver->mkReal(2)));
Sort consListSort = d_solver->mkDatatypeSort(consListSpec);
Datatype consList = consListSort.getDatatype();
- Op consTerm = consList.getConstructorTerm("cons");
- Op nilTerm = consList.getConstructorTerm("nil");
- Op headTerm = consList["cons"].getSelectorTerm("head");
-
- TS_ASSERT(consTerm.getKind() == APPLY_CONSTRUCTOR);
- TS_ASSERT(nilTerm.getKind() == APPLY_CONSTRUCTOR);
- TS_ASSERT(headTerm.getKind() == APPLY_SELECTOR);
+ Term consTerm = consList.getConstructorTerm("cons");
+ Term nilTerm = consList.getConstructorTerm("nil");
+ Term headTerm = consList["cons"].getSelectorTerm("head");
- Term listnil = d_solver->mkTerm(nilTerm);
- Term listcons1 = d_solver->mkTerm(consTerm, d_solver->mkReal(1), listnil);
- Term listhead = d_solver->mkTerm(headTerm, listcons1);
+ Term listnil = d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm);
+ Term listcons1 = d_solver->mkTerm(
+ APPLY_CONSTRUCTOR, consTerm, d_solver->mkReal(1), listnil);
+ Term listhead = d_solver->mkTerm(APPLY_SELECTOR, headTerm, listcons1);
TS_ASSERT(listnil.hasOp());
- TS_ASSERT_EQUALS(listnil.getOp(), nilTerm);
+ TS_ASSERT_EQUALS(listnil.getOp(), APPLY_CONSTRUCTOR);
TS_ASSERT(listcons1.hasOp());
- TS_ASSERT_EQUALS(listcons1.getOp(), consTerm);
+ TS_ASSERT_EQUALS(listcons1.getOp(), APPLY_CONSTRUCTOR);
TS_ASSERT(listhead.hasOp());
- TS_ASSERT_EQUALS(listhead.getOp(), headTerm);
+ TS_ASSERT_EQUALS(listhead.getOp(), APPLY_SELECTOR);
}
void SolverBlack::testPush1()
TS_ASSERT(i1 == d_solver->simplify(i3));
Datatype consList = consListSort.getDatatype();
- Term dt1 =
- d_solver->mkTerm(consList.getConstructorTerm("cons"),
- d_solver->mkReal(0),
- d_solver->mkTerm(consList.getConstructorTerm("nil")));
+ Term dt1 = d_solver->mkTerm(
+ APPLY_CONSTRUCTOR,
+ consList.getConstructorTerm("cons"),
+ d_solver->mkReal(0),
+ d_solver->mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt1));
- Term dt2 = d_solver->mkTerm(consList["cons"].getSelectorTerm("head"), dt1);
+ Term dt2 = d_solver->mkTerm(
+ APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), dt1);
TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt2));
Term b1 = d_solver->mkVar(bvSort, "b1");
void testGetId();
void testGetKind();
void testGetSort();
+ void testGetOp();
void testIsNull();
- void testIsParameterized();
void testNotTerm();
void testAndTerm();
void testOrTerm();
TS_ASSERT(p_f_y.getSort() == boolSort);
}
+void TermBlack::testGetOp()
+{
+ Sort intsort = d_solver.getIntegerSort();
+ Sort bvsort = d_solver.mkBitVectorSort(8);
+ Sort arrsort = d_solver.mkArraySort(bvsort, intsort);
+ Sort funsort = d_solver.mkFunctionSort(intsort, bvsort);
+
+ Term x = d_solver.mkConst(intsort, "x");
+ Term a = d_solver.mkConst(arrsort, "a");
+ Term b = d_solver.mkConst(bvsort, "b");
+
+ TS_ASSERT(!x.hasOp());
+ TS_ASSERT_THROWS(x.getOp(), CVC4ApiException&);
+
+ Term ab = d_solver.mkTerm(SELECT, a, b);
+ Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
+ Term extb = d_solver.mkTerm(ext, b);
+
+ TS_ASSERT(ab.hasOp());
+ TS_ASSERT_EQUALS(ab.getOp(), Op(SELECT));
+ TS_ASSERT(!ab.getOp().isIndexed());
+ // can compare directly to a Kind (will invoke Op constructor)
+ TS_ASSERT_EQUALS(ab.getOp(), SELECT);
+ TS_ASSERT(extb.hasOp());
+ TS_ASSERT(extb.getOp().isIndexed());
+ TS_ASSERT_EQUALS(extb.getOp(), ext);
+
+ Term f = d_solver.mkConst(funsort, "f");
+ Term fx = d_solver.mkTerm(APPLY_UF, f, x);
+
+ TS_ASSERT(!f.hasOp());
+ TS_ASSERT_THROWS(f.getOp(), CVC4ApiException&);
+ TS_ASSERT(fx.hasOp());
+ TS_ASSERT_EQUALS(fx.getOp(), APPLY_UF);
+ std::vector<Term> children(fx.begin(), fx.end());
+ // testing rebuild from op and children
+ TS_ASSERT_EQUALS(fx, d_solver.mkTerm(fx.getOp(), children));
+
+ // Test Datatypes Ops
+ Sort sort = d_solver.mkParamSort("T");
+ DatatypeDecl listDecl = d_solver.mkDatatypeDecl("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.mkConst(intListSort, "c");
+ Datatype list = listSort.getDatatype();
+ // list datatype constructor and selector operator terms
+ Term consOpTerm = list.getConstructorTerm("cons");
+ Term nilOpTerm = list.getConstructorTerm("nil");
+ Term headOpTerm = list["cons"].getSelectorTerm("head");
+ Term tailOpTerm = list["cons"].getSelectorTerm("tail");
+
+ Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilOpTerm);
+ Term consTerm = d_solver.mkTerm(
+ APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkReal(0), nilTerm);
+ Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, headOpTerm, consTerm);
+ Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, tailOpTerm, consTerm);
+
+ TS_ASSERT(nilTerm.hasOp());
+ TS_ASSERT(consTerm.hasOp());
+ TS_ASSERT(headTerm.hasOp());
+ TS_ASSERT(tailTerm.hasOp());
+
+ TS_ASSERT_EQUALS(nilTerm.getOp(), APPLY_CONSTRUCTOR);
+ TS_ASSERT_EQUALS(consTerm.getOp(), APPLY_CONSTRUCTOR);
+ TS_ASSERT_EQUALS(headTerm.getOp(), APPLY_SELECTOR);
+ TS_ASSERT_EQUALS(tailTerm.getOp(), APPLY_SELECTOR);
+
+ // Test rebuilding
+ children.clear();
+ children.insert(children.begin(), headTerm.begin(), headTerm.end());
+ TS_ASSERT_EQUALS(headTerm, d_solver.mkTerm(headTerm.getOp(), children));
+}
+
void TermBlack::testIsNull()
{
Term x;
TS_ASSERT_THROWS_NOTHING(p_f_x.notTerm());
}
-void TermBlack::testIsParameterized()
-{
- Term n;
- TS_ASSERT_THROWS(n.isParameterized(), CVC4ApiException&);
- Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x");
- TS_ASSERT_THROWS_NOTHING(x.isParameterized());
-}
-
void TermBlack::testAndTerm()
{
Sort bvSort = d_solver.mkBitVectorSort(8);
projects / cvc5.git / commitdiff