diff options
| -rw-r--r-- | src/api/cvc4cpp.cpp | 224 | ||||
| -rw-r--r-- | src/util/utility.h | 1 |
2 files changed, 225 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 968102f5d..80af4199b 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -16,9 +16,13 @@ #include "api/cvc4cpp.h" +#include "base/cvc4_assert.h" +#include "expr/expr.h" +#include "expr/expr_manager.h" #include "expr/kind.h" #include "expr/type.h" #include "util/result.h" +#include "util/utility.h" #include <sstream> @@ -92,6 +96,7 @@ std::ostream& operator<<(std::ostream& out, const Result& r) return out; } + /* -------------------------------------------------------------------------- */ /* Kind */ /* -------------------------------------------------------------------------- */ @@ -623,6 +628,7 @@ std::ostream& operator<<(std::ostream& out, Kind k) size_t KindHashFunction::operator()(Kind k) const { return k; } + /* -------------------------------------------------------------------------- */ /* Sort */ /* -------------------------------------------------------------------------- */ @@ -799,5 +805,223 @@ size_t SortHashFunction::operator()(const Sort& s) const { return TypeHashFunction()(*s.d_type); } + +/* -------------------------------------------------------------------------- */ +/* Term */ +/* -------------------------------------------------------------------------- */ + +Term::Term() : d_expr(new CVC4::Expr()) +{ +} + +Term::Term(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) +{ +} + +Term::~Term() +{ +} + +Term& Term::operator=(const Term& t) +{ + // CHECK: expr managers must match + if (this != &t) + { + *d_expr = *t.d_expr; + } + return *this; +} + +bool Term::operator==(const Term& t) const +{ + // CHECK: expr managers must match + return *d_expr == *t.d_expr; +} + +bool Term::operator!=(const Term& t) const +{ + // CHECK: expr managers must match + return *d_expr != *t.d_expr; +} + +Kind Term::getKind() const +{ + return intToExtKind(d_expr->getKind()); +} + +Sort Term::getSort() const +{ + return Sort(d_expr->getType()); +} + +bool Term::isNull() const +{ + return d_expr->isNull(); +} + +Term Term::notTerm() const +{ + return d_expr->notExpr(); +} + +Term Term::andTerm(const Term& t) const +{ + return d_expr->andExpr(*t.d_expr); +} + +Term Term::orTerm(const Term& t) const +{ + return d_expr->orExpr(*t.d_expr); +} + +Term Term::xorTerm(const Term& t) const +{ + return d_expr->xorExpr(*t.d_expr); +} + +Term Term::iffTerm(const Term& t) const +{ + return d_expr->iffExpr(*t.d_expr); +} + +Term Term::impTerm(const Term& t) const +{ + return d_expr->impExpr(*t.d_expr); +} + +Term Term::iteTerm(const Term& then_t, const Term& else_t) const +{ + return d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr); +} + +std::string Term::toString() const +{ + return d_expr->toString(); +} + +Term::const_iterator::const_iterator() : d_iterator(nullptr) +{ +} + +Term::const_iterator::const_iterator(void* it) : d_iterator(it) +{ +} + +Term::const_iterator::const_iterator(const const_iterator& it) + : d_iterator(nullptr) +{ + if (it.d_iterator != nullptr) + { + d_iterator = new CVC4::Expr::const_iterator( + *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator)); + } +} + +Term::const_iterator& Term::const_iterator::operator=(const const_iterator& it) +{ + delete static_cast<CVC4::Expr::const_iterator*>(d_iterator); + d_iterator = new CVC4::Expr::const_iterator( + *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator)); + return *this; +} + +Term::const_iterator::~const_iterator() +{ + delete static_cast<CVC4::Expr::const_iterator*>(d_iterator); +} + +bool Term::const_iterator::operator==(const const_iterator& it) const +{ + if (d_iterator == nullptr || it.d_iterator == nullptr) + { + return false; + } + return *static_cast<CVC4::Expr::const_iterator*>(d_iterator) + == *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator); +} + +bool Term::const_iterator::operator!=(const const_iterator& it) const +{ + return !(*this == it); +} + +Term::const_iterator& Term::const_iterator::operator++() +{ + Assert(d_iterator != nullptr); + ++*static_cast<CVC4::Expr::const_iterator*>(d_iterator); + return *this; +} + +Term::const_iterator Term::const_iterator::operator++(int) +{ + Assert(d_iterator != nullptr); + const_iterator it = *this; + ++*static_cast<CVC4::Expr::const_iterator*>(d_iterator); + return it; +} + +Term Term::const_iterator::operator*() const +{ + Assert(d_iterator != nullptr); + return Term(**static_cast<CVC4::Expr::const_iterator*>(d_iterator)); +} + +Term::const_iterator Term::begin() const +{ + return Term::const_iterator(new CVC4::Expr::const_iterator(d_expr->begin())); +} + +Term::const_iterator Term::end() const +{ + return Term::const_iterator(new CVC4::Expr::const_iterator(d_expr->end())); +} + +std::ostream& operator<< (std::ostream& out, const Term& t) +{ + out << t.toString(); + return out; +} + +std::ostream& operator<<(std::ostream& out, const std::vector<Term>& vector) +{ + container_to_stream(out, vector); + return out; +} + +std::ostream& operator<<(std::ostream& out, const std::set<Term>& set) +{ + container_to_stream(out, set); + return out; +} + +std::ostream& operator<<( + std::ostream& out, + const std::unordered_set<Term, TermHashFunction>& unordered_set) +{ + container_to_stream(out, unordered_set); + return out; +} + +template <typename V> +std::ostream& operator<<(std::ostream& out, const std::map<Term, V>& map) +{ + container_to_stream(out, map); + return out; +} + +template <typename V> +std::ostream& operator<<( + std::ostream& out, + const std::unordered_map<Term, V, TermHashFunction>& unordered_map) +{ + container_to_stream(out, unordered_map); + return out; +} + +size_t TermHashFunction::operator()(const Term& t) const +{ + return ExprHashFunction()(*t.d_expr); +} + } // namespace api } // namespace CVC4 diff --git a/src/util/utility.h b/src/util/utility.h index bfe8e66c9..a9a9a29c3 100644 --- a/src/util/utility.h +++ b/src/util/utility.h @@ -19,6 +19,7 @@ #ifndef __CVC4__UTILITY_H #define __CVC4__UTILITY_H +#include <algorithm> #include <utility> #include <functional> |