summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--NEWS11
-rw-r--r--src/api/cvc4cpp.cpp93
-rw-r--r--src/api/cvc4cpp.h4
-rw-r--r--src/expr/expr_template.cpp3
-rw-r--r--src/expr/expr_template.h2
-rw-r--r--src/proof/bitvector_proof.cpp2
-rw-r--r--test/unit/api/term_black.h522
7 files changed, 615 insertions, 22 deletions
diff --git a/NEWS b/NEWS
index 038b02026..0cc8cab44 100644
--- a/NEWS
+++ b/NEWS
@@ -1,5 +1,16 @@
This file contains a summary of important user-visible changes.
+Changes since 1.6
+=================
+
+New Features:
+
+Improvements:
+
+Changes:
+* API change: Expr::iffExpr() is renamed to Expr::eqExpr() to reflect its
+ actual behavior.
+
Changes since 1.5
=================
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 68b0301ec..cd604a25c 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1007,27 +1007,102 @@ bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; }
bool Term::operator!=(const Term& t) const { return *d_expr != *t.d_expr; }
-Kind Term::getKind() const { return intToExtKind(d_expr->getKind()); }
+Kind Term::getKind() const
+{
+ CVC4_API_CHECK_NOT_NULL;
+ return intToExtKind(d_expr->getKind());
+}
-Sort Term::getSort() const { return Sort(d_expr->getType()); }
+Sort Term::getSort() const
+{
+ CVC4_API_CHECK_NOT_NULL;
+ return Sort(d_expr->getType());
+}
bool Term::isNull() const { return d_expr->isNull(); }
-Term Term::notTerm() const { return d_expr->notExpr(); }
+Term Term::notTerm() const
+{
+ try
+ {
+ return d_expr->notExpr();
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
+}
-Term Term::andTerm(const Term& t) const { return d_expr->andExpr(*t.d_expr); }
+Term Term::andTerm(const Term& t) const
+{
+ try
+ {
+ return d_expr->andExpr(*t.d_expr);
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
+}
-Term Term::orTerm(const Term& t) const { return d_expr->orExpr(*t.d_expr); }
+Term Term::orTerm(const Term& t) const
+{
+ try
+ {
+ return d_expr->orExpr(*t.d_expr);
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
+}
-Term Term::xorTerm(const Term& t) const { return d_expr->xorExpr(*t.d_expr); }
+Term Term::xorTerm(const Term& t) const
+{
+ try
+ {
+ return d_expr->xorExpr(*t.d_expr);
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
+}
-Term Term::iffTerm(const Term& t) const { return d_expr->iffExpr(*t.d_expr); }
+Term Term::eqTerm(const Term& t) const
+{
+ try
+ {
+ return d_expr->eqExpr(*t.d_expr);
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
+}
-Term Term::impTerm(const Term& t) const { return d_expr->impExpr(*t.d_expr); }
+Term Term::impTerm(const Term& t) const
+{
+ try
+ {
+ return d_expr->impExpr(*t.d_expr);
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
+}
Term Term::iteTerm(const Term& then_t, const Term& else_t) const
{
- return d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr);
+ try
+ {
+ return d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr);
+ }
+ catch (TypeCheckingException& e)
+ {
+ throw CVC4ApiException(e.getMessage());
+ }
}
std::string Term::toString() const { return d_expr->toString(); }
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index aebeffb0d..d06955a05 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -607,11 +607,11 @@ class CVC4_PUBLIC Term
Term xorTerm(const Term& t) const;
/**
- * Boolean if-and-only-if.
+ * Equality.
* @param t a Boolean term
* @return the Boolean equivalence of this term and the given term
*/
- Term iffTerm(const Term& t) const;
+ Term eqTerm(const Term& t) const;
/**
* Boolean implication.
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 61568e411..96bdb2d04 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -595,7 +595,8 @@ Expr Expr::xorExpr(const Expr& e) const {
return d_exprManager->mkExpr(XOR, *this, e);
}
-Expr Expr::iffExpr(const Expr& e) const {
+Expr Expr::eqExpr(const Expr& e) const
+{
Assert(d_exprManager != NULL,
"Don't have an expression manager for this expression!");
PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 324915b1d..da9d22389 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -391,7 +391,7 @@ public:
* Returns the Boolean equivalence of this expression and
* the given expression.
*/
- Expr iffExpr(const Expr& e) const;
+ Expr eqExpr(const Expr& e) const;
/**
* Returns the implication of this expression and
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 9eb39e2e2..ba3533cc3 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -68,7 +68,7 @@ void BitVectorProof::registerAtomBB(Expr atom, Expr atom_bb) {
Debug("pf::bv") << "BitVectorProof::registerAtomBB( " << atom
<< ", " << atom_bb << " )" << std::endl;
- Expr def = atom.iffExpr(atom_bb);
+ Expr def = atom.eqExpr(atom_bb);
d_bbAtoms.insert(std::make_pair(atom, def));
registerTerm(atom);
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index c2ca1cb08..ae1dfe7ba 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -2,7 +2,7 @@
/*! \file term_black.h
** \verbatim
** Top contributors (to current version):
- ** Andres Noetzli
+ ** Aina Niemetz, Andres Noetzli
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
@@ -24,14 +24,520 @@ class TermBlack : public CxxTest::TestSuite
void setUp() override {}
void tearDown() override {}
- void testTermAssignment()
- {
- Term t1 = d_solver.mkReal(1);
- Term t2 = t1;
- t2 = d_solver.mkReal(2);
- TS_ASSERT_EQUALS(t1, d_solver.mkReal(1));
- }
+ void testEq();
+ void testGetKind();
+ void testGetSort();
+ void testIsNull();
+ void testNotTerm();
+ void testAndTerm();
+ void testOrTerm();
+ void testXorTerm();
+ void testEqTerm();
+ void testImpTerm();
+ void testIteTerm();
+
+ void testTermAssignment();
private:
Solver d_solver;
};
+
+void TermBlack::testEq()
+{
+ Sort uSort = d_solver.mkUninterpretedSort("u");
+ Term x = d_solver.mkVar("x", uSort);
+ Term y = d_solver.mkVar("y", uSort);
+ Term z;
+
+ TS_ASSERT(x == x);
+ TS_ASSERT(!(x != x));
+ TS_ASSERT(!(x == y));
+ TS_ASSERT(x != y);
+ TS_ASSERT(!(x == z));
+ TS_ASSERT(x != z);
+}
+
+void TermBlack::testGetKind()
+{
+ Sort uSort = d_solver.mkUninterpretedSort("u");
+ Sort intSort = d_solver.getIntegerSort();
+ Sort boolSort = d_solver.getBooleanSort();
+ Sort funSort1 = d_solver.mkFunctionSort(uSort, intSort);
+ Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+ Term n;
+ TS_ASSERT_THROWS(n.getKind(), CVC4ApiException&);
+ Term x = d_solver.mkVar("x", uSort);
+ TS_ASSERT_THROWS_NOTHING(x.getKind());
+ Term y = d_solver.mkVar("y", uSort);
+ TS_ASSERT_THROWS_NOTHING(y.getKind());
+
+ Term f = d_solver.mkVar("f", funSort1);
+ TS_ASSERT_THROWS_NOTHING(f.getKind());
+ Term p = d_solver.mkVar("p", funSort2);
+ TS_ASSERT_THROWS_NOTHING(p.getKind());
+
+ Term zero = d_solver.mkInteger(0);
+ TS_ASSERT_THROWS_NOTHING(zero.getKind());
+
+ Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+ TS_ASSERT_THROWS_NOTHING(f_x.getKind());
+ Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
+ TS_ASSERT_THROWS_NOTHING(f_y.getKind());
+ Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
+ TS_ASSERT_THROWS_NOTHING(sum.getKind());
+ Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+ TS_ASSERT_THROWS_NOTHING(p_0.getKind());
+ Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
+ TS_ASSERT_THROWS_NOTHING(p_f_y.getKind());
+}
+
+void TermBlack::testGetSort()
+{
+ Sort bvSort = d_solver.mkBitVectorSort(8);
+ Sort intSort = d_solver.getIntegerSort();
+ Sort boolSort = d_solver.getBooleanSort();
+ Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+ Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+ Term n;
+ TS_ASSERT_THROWS(n.getSort(), CVC4ApiException&);
+ Term x = d_solver.mkVar("x", bvSort);
+ TS_ASSERT_THROWS_NOTHING(x.getSort());
+ TS_ASSERT(x.getSort() == bvSort);
+ Term y = d_solver.mkVar("y", bvSort);
+ TS_ASSERT_THROWS_NOTHING(y.getSort());
+ TS_ASSERT(y.getSort() == bvSort);
+
+ Term f = d_solver.mkVar("f", funSort1);
+ TS_ASSERT_THROWS_NOTHING(f.getSort());
+ TS_ASSERT(f.getSort() == funSort1);
+ Term p = d_solver.mkVar("p", funSort2);
+ TS_ASSERT_THROWS_NOTHING(p.getSort());
+ TS_ASSERT(p.getSort() == funSort2);
+
+ Term zero = d_solver.mkInteger(0);
+ TS_ASSERT_THROWS_NOTHING(zero.getSort());
+ TS_ASSERT(zero.getSort() == intSort);
+
+ Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+ TS_ASSERT_THROWS_NOTHING(f_x.getSort());
+ TS_ASSERT(f_x.getSort() == intSort);
+ Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
+ TS_ASSERT_THROWS_NOTHING(f_y.getSort());
+ TS_ASSERT(f_y.getSort() == intSort);
+ Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
+ TS_ASSERT_THROWS_NOTHING(sum.getSort());
+ TS_ASSERT(sum.getSort() == intSort);
+ Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+ TS_ASSERT_THROWS_NOTHING(p_0.getSort());
+ TS_ASSERT(p_0.getSort() == boolSort);
+ Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
+ TS_ASSERT_THROWS_NOTHING(p_f_y.getSort());
+ TS_ASSERT(p_f_y.getSort() == boolSort);
+}
+
+void TermBlack::testIsNull()
+{
+ Term x;
+ TS_ASSERT(x.isNull());
+ x = d_solver.mkVar("x", d_solver.mkBitVectorSort(4));
+ TS_ASSERT(!x.isNull());
+}
+
+void TermBlack::testNotTerm()
+{
+ Sort bvSort = d_solver.mkBitVectorSort(8);
+ Sort intSort = d_solver.getIntegerSort();
+ Sort boolSort = d_solver.getBooleanSort();
+ Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+ Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+ Term b = d_solver.mkTrue();
+ TS_ASSERT_THROWS_NOTHING(b.notTerm());
+ Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+ TS_ASSERT_THROWS(x.notTerm(), CVC4ApiException&);
+ Term f = d_solver.mkVar("f", funSort1);
+ TS_ASSERT_THROWS(f.notTerm(), CVC4ApiException&);
+ Term p = d_solver.mkVar("p", funSort2);
+ TS_ASSERT_THROWS(p.notTerm(), CVC4ApiException&);
+ Term zero = d_solver.mkInteger(0);
+ TS_ASSERT_THROWS(zero.notTerm(), CVC4ApiException&);
+ Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+ TS_ASSERT_THROWS(f_x.notTerm(), CVC4ApiException&);
+ Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+ TS_ASSERT_THROWS(sum.notTerm(), CVC4ApiException&);
+ Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+ TS_ASSERT_THROWS_NOTHING(p_0.notTerm());
+ Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+ TS_ASSERT_THROWS_NOTHING(p_f_x.notTerm());
+}
+
+void TermBlack::testAndTerm()
+{
+ Sort bvSort = d_solver.mkBitVectorSort(8);
+ Sort intSort = d_solver.getIntegerSort();
+ Sort boolSort = d_solver.getBooleanSort();
+ Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+ Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+ Term b = d_solver.mkTrue();
+ TS_ASSERT_THROWS_NOTHING(b.andTerm(b));
+ Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+ TS_ASSERT_THROWS(x.andTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(x.andTerm(x), CVC4ApiException&);
+ Term f = d_solver.mkVar("f", funSort1);
+ TS_ASSERT_THROWS(f.andTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(f.andTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(f.andTerm(f), CVC4ApiException&);
+ Term p = d_solver.mkVar("p", funSort2);
+ TS_ASSERT_THROWS(p.andTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(p.andTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p.andTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(p.andTerm(p), CVC4ApiException&);
+ Term zero = d_solver.mkInteger(0);
+ TS_ASSERT_THROWS(zero.andTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.andTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.andTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.andTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.andTerm(zero), CVC4ApiException&);
+ Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+ TS_ASSERT_THROWS(f_x.andTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.andTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.andTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.andTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.andTerm(zero), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.andTerm(f_x), CVC4ApiException&);
+ Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+ TS_ASSERT_THROWS(sum.andTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.andTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.andTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.andTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.andTerm(zero), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.andTerm(f_x), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.andTerm(sum), CVC4ApiException&);
+ Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+ TS_ASSERT_THROWS_NOTHING(p_0.andTerm(b));
+ TS_ASSERT_THROWS(p_0.andTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.andTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.andTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.andTerm(zero), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.andTerm(f_x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.andTerm(sum), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(p_0.andTerm(p_0));
+ Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+ TS_ASSERT_THROWS_NOTHING(p_f_x.andTerm(b));
+ TS_ASSERT_THROWS(p_f_x.andTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.andTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.andTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.andTerm(zero), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.andTerm(f_x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.andTerm(sum), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(p_f_x.andTerm(p_0));
+ TS_ASSERT_THROWS_NOTHING(p_f_x.andTerm(p_f_x));
+}
+
+void TermBlack::testOrTerm()
+{
+ Sort bvSort = d_solver.mkBitVectorSort(8);
+ Sort intSort = d_solver.getIntegerSort();
+ Sort boolSort = d_solver.getBooleanSort();
+ Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+ Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+ Term b = d_solver.mkTrue();
+ TS_ASSERT_THROWS_NOTHING(b.orTerm(b));
+ Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+ TS_ASSERT_THROWS(x.orTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(x.orTerm(x), CVC4ApiException&);
+ Term f = d_solver.mkVar("f", funSort1);
+ TS_ASSERT_THROWS(f.orTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(f.orTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(f.orTerm(f), CVC4ApiException&);
+ Term p = d_solver.mkVar("p", funSort2);
+ TS_ASSERT_THROWS(p.orTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(p.orTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p.orTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(p.orTerm(p), CVC4ApiException&);
+ Term zero = d_solver.mkInteger(0);
+ TS_ASSERT_THROWS(zero.orTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.orTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.orTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.orTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.orTerm(zero), CVC4ApiException&);
+ Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+ TS_ASSERT_THROWS(f_x.orTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.orTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.orTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.orTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.orTerm(zero), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.orTerm(f_x), CVC4ApiException&);
+ Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+ TS_ASSERT_THROWS(sum.orTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.orTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.orTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.orTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.orTerm(zero), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.orTerm(f_x), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.orTerm(sum), CVC4ApiException&);
+ Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+ TS_ASSERT_THROWS_NOTHING(p_0.orTerm(b));
+ TS_ASSERT_THROWS(p_0.orTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.orTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.orTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.orTerm(zero), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.orTerm(f_x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.orTerm(sum), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(p_0.orTerm(p_0));
+ Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+ TS_ASSERT_THROWS_NOTHING(p_f_x.orTerm(b));
+ TS_ASSERT_THROWS(p_f_x.orTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.orTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.orTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.orTerm(zero), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.orTerm(f_x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.orTerm(sum), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(p_f_x.orTerm(p_0));
+ TS_ASSERT_THROWS_NOTHING(p_f_x.orTerm(p_f_x));
+}
+
+void TermBlack::testXorTerm()
+{
+ Sort bvSort = d_solver.mkBitVectorSort(8);
+ Sort intSort = d_solver.getIntegerSort();
+ Sort boolSort = d_solver.getBooleanSort();
+ Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+ Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+ Term b = d_solver.mkTrue();
+ TS_ASSERT_THROWS_NOTHING(b.xorTerm(b));
+ Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+ TS_ASSERT_THROWS(x.xorTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(x.xorTerm(x), CVC4ApiException&);
+ Term f = d_solver.mkVar("f", funSort1);
+ TS_ASSERT_THROWS(f.xorTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(f.xorTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(f.xorTerm(f), CVC4ApiException&);
+ Term p = d_solver.mkVar("p", funSort2);
+ TS_ASSERT_THROWS(p.xorTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(p.xorTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p.xorTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(p.xorTerm(p), CVC4ApiException&);
+ Term zero = d_solver.mkInteger(0);
+ TS_ASSERT_THROWS(zero.xorTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.xorTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.xorTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.xorTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.xorTerm(zero), CVC4ApiException&);
+ Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+ TS_ASSERT_THROWS(f_x.xorTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.xorTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.xorTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.xorTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.xorTerm(zero), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.xorTerm(f_x), CVC4ApiException&);
+ Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+ TS_ASSERT_THROWS(sum.xorTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.xorTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.xorTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.xorTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.xorTerm(zero), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.xorTerm(f_x), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.xorTerm(sum), CVC4ApiException&);
+ Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+ TS_ASSERT_THROWS_NOTHING(p_0.xorTerm(b));
+ TS_ASSERT_THROWS(p_0.xorTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.xorTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.xorTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.xorTerm(zero), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.xorTerm(f_x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.xorTerm(sum), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(p_0.xorTerm(p_0));
+ Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+ TS_ASSERT_THROWS_NOTHING(p_f_x.xorTerm(b));
+ TS_ASSERT_THROWS(p_f_x.xorTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.xorTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.xorTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.xorTerm(zero), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.xorTerm(f_x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.xorTerm(sum), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(p_f_x.xorTerm(p_0));
+ TS_ASSERT_THROWS_NOTHING(p_f_x.xorTerm(p_f_x));
+}
+
+void TermBlack::testEqTerm()
+{
+ Sort bvSort = d_solver.mkBitVectorSort(8);
+ Sort intSort = d_solver.getIntegerSort();
+ Sort boolSort = d_solver.getBooleanSort();
+ Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+ Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+ Term b = d_solver.mkTrue();
+ TS_ASSERT_THROWS_NOTHING(b.eqTerm(b));
+ Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+ TS_ASSERT_THROWS(x.eqTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(x.eqTerm(x));
+ Term f = d_solver.mkVar("f", funSort1);
+ TS_ASSERT_THROWS(f.eqTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(f.eqTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(f.eqTerm(f));
+ Term p = d_solver.mkVar("p", funSort2);
+ TS_ASSERT_THROWS(p.eqTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(p.eqTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p.eqTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(p.eqTerm(p));
+ Term zero = d_solver.mkInteger(0);
+ TS_ASSERT_THROWS(zero.eqTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.eqTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.eqTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.eqTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(zero.eqTerm(zero));
+ Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+ TS_ASSERT_THROWS(f_x.eqTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.eqTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.eqTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.eqTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(f_x.eqTerm(zero));
+ TS_ASSERT_THROWS_NOTHING(f_x.eqTerm(f_x));
+ Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+ TS_ASSERT_THROWS(sum.eqTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.eqTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.eqTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.eqTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(sum.eqTerm(zero));
+ TS_ASSERT_THROWS_NOTHING(sum.eqTerm(f_x));
+ TS_ASSERT_THROWS_NOTHING(sum.eqTerm(sum));
+ Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+ TS_ASSERT_THROWS_NOTHING(p_0.eqTerm(b));
+ TS_ASSERT_THROWS(p_0.eqTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.eqTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.eqTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.eqTerm(zero), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.eqTerm(f_x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.eqTerm(sum), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(p_0.eqTerm(p_0));
+ Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+ TS_ASSERT_THROWS_NOTHING(p_f_x.eqTerm(b));
+ TS_ASSERT_THROWS(p_f_x.eqTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.eqTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.eqTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.eqTerm(zero), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.eqTerm(f_x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.eqTerm(sum), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(p_f_x.eqTerm(p_0));
+ TS_ASSERT_THROWS_NOTHING(p_f_x.eqTerm(p_f_x));
+}
+
+void TermBlack::testImpTerm()
+{
+ Sort bvSort = d_solver.mkBitVectorSort(8);
+ Sort intSort = d_solver.getIntegerSort();
+ Sort boolSort = d_solver.getBooleanSort();
+ Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+ Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+ Term b = d_solver.mkTrue();
+ TS_ASSERT_THROWS_NOTHING(b.impTerm(b));
+ Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+ TS_ASSERT_THROWS(x.impTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(x.impTerm(x), CVC4ApiException&);
+ Term f = d_solver.mkVar("f", funSort1);
+ TS_ASSERT_THROWS(f.impTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(f.impTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(f.impTerm(f), CVC4ApiException&);
+ Term p = d_solver.mkVar("p", funSort2);
+ TS_ASSERT_THROWS(p.impTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(p.impTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p.impTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(p.impTerm(p), CVC4ApiException&);
+ Term zero = d_solver.mkInteger(0);
+ TS_ASSERT_THROWS(zero.impTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.impTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.impTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.impTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.impTerm(zero), CVC4ApiException&);
+ Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+ TS_ASSERT_THROWS(f_x.impTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.impTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.impTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.impTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.impTerm(zero), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.impTerm(f_x), CVC4ApiException&);
+ Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+ TS_ASSERT_THROWS(sum.impTerm(b), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.impTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.impTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.impTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.impTerm(zero), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.impTerm(f_x), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.impTerm(sum), CVC4ApiException&);
+ Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+ TS_ASSERT_THROWS_NOTHING(p_0.impTerm(b));
+ TS_ASSERT_THROWS(p_0.impTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.impTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.impTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.impTerm(zero), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.impTerm(f_x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_0.impTerm(sum), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(p_0.impTerm(p_0));
+ Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+ TS_ASSERT_THROWS_NOTHING(p_f_x.impTerm(b));
+ TS_ASSERT_THROWS(p_f_x.impTerm(x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.impTerm(f), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.impTerm(p), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.impTerm(zero), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.impTerm(f_x), CVC4ApiException&);
+ TS_ASSERT_THROWS(p_f_x.impTerm(sum), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(p_f_x.impTerm(p_0));
+ TS_ASSERT_THROWS_NOTHING(p_f_x.impTerm(p_f_x));
+}
+
+void TermBlack::testIteTerm()
+{
+ Sort bvSort = d_solver.mkBitVectorSort(8);
+ Sort intSort = d_solver.getIntegerSort();
+ Sort boolSort = d_solver.getBooleanSort();
+ Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+ Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+ Term b = d_solver.mkTrue();
+ TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b));
+ Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+ TS_ASSERT_THROWS_NOTHING(b.iteTerm(x, x));
+ TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b));
+ TS_ASSERT_THROWS(b.iteTerm(x, b), CVC4ApiException&);
+ TS_ASSERT_THROWS(x.iteTerm(x, x), CVC4ApiException&);
+ TS_ASSERT_THROWS(x.iteTerm(x, b), CVC4ApiException&);
+ Term f = d_solver.mkVar("f", funSort1);
+ TS_ASSERT_THROWS(f.iteTerm(b, b), CVC4ApiException&);
+ TS_ASSERT_THROWS(x.iteTerm(b, x), CVC4ApiException&);
+ Term p = d_solver.mkVar("p", funSort2);
+ TS_ASSERT_THROWS(p.iteTerm(b, b), CVC4ApiException&);
+ TS_ASSERT_THROWS(p.iteTerm(x, b), CVC4ApiException&);
+ Term zero = d_solver.mkInteger(0);
+ TS_ASSERT_THROWS(zero.iteTerm(x, x), CVC4ApiException&);
+ TS_ASSERT_THROWS(zero.iteTerm(x, b), CVC4ApiException&);
+ Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+ TS_ASSERT_THROWS(f_x.iteTerm(b, b), CVC4ApiException&);
+ TS_ASSERT_THROWS(f_x.iteTerm(b, x), CVC4ApiException&);
+ Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+ TS_ASSERT_THROWS(sum.iteTerm(x, x), CVC4ApiException&);
+ TS_ASSERT_THROWS(sum.iteTerm(b, x), CVC4ApiException&);
+ Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+ TS_ASSERT_THROWS_NOTHING(p_0.iteTerm(b, b));
+ TS_ASSERT_THROWS_NOTHING(p_0.iteTerm(x, x));
+ TS_ASSERT_THROWS(p_0.iteTerm(x, b), CVC4ApiException&);
+ Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+ TS_ASSERT_THROWS_NOTHING(p_f_x.iteTerm(b, b));
+ TS_ASSERT_THROWS_NOTHING(p_f_x.iteTerm(x, x));
+ TS_ASSERT_THROWS(p_f_x.iteTerm(x, b), CVC4ApiException&);
+}
+
+void TermBlack::testTermAssignment()
+{
+ Term t1 = d_solver.mkReal(1);
+ Term t2 = t1;
+ t2 = d_solver.mkReal(2);
+ TS_ASSERT_EQUALS(t1, d_solver.mkReal(1));
+}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback