diff options
Diffstat (limited to 'src/api/cvc4cpp.h')
| -rw-r--r-- | src/api/cvc4cpp.h | 132 |
1 files changed, 66 insertions, 66 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 5a8f62983..8e5ddf28d 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -30,7 +30,7 @@ #include <unordered_set> #include <vector> -namespace CVC4 { +namespace CVC5 { template <bool ref_count> class NodeTemplate; @@ -201,14 +201,14 @@ class CVC4_EXPORT Result * @param r the internal result that is to be wrapped by this result * @return the Result */ - Result(const CVC4::Result& r); + Result(const CVC5::Result& r); /** * The interal result wrapped by this result. - * Note: This is a shared_ptr rather than a unique_ptr since CVC4::Result is + * Note: This is a shared_ptr rather than a unique_ptr since CVC5::Result is * not ref counted. */ - std::shared_ptr<CVC4::Result> d_result; + std::shared_ptr<CVC5::Result> d_result; }; /** @@ -239,16 +239,16 @@ class Datatype; */ class CVC4_EXPORT Sort { - friend class CVC4::DatatypeDeclarationCommand; - friend class CVC4::DeclareFunctionCommand; - friend class CVC4::DeclareHeapCommand; - friend class CVC4::DeclareSortCommand; - friend class CVC4::DeclareSygusVarCommand; - friend class CVC4::DefineSortCommand; - friend class CVC4::GetAbductCommand; - friend class CVC4::GetInterpolCommand; - friend class CVC4::GetModelCommand; - friend class CVC4::SynthFunCommand; + friend class CVC5::DatatypeDeclarationCommand; + friend class CVC5::DeclareFunctionCommand; + friend class CVC5::DeclareHeapCommand; + friend class CVC5::DeclareSortCommand; + friend class CVC5::DeclareSygusVarCommand; + friend class CVC5::DefineSortCommand; + friend class CVC5::GetAbductCommand; + friend class CVC5::GetInterpolCommand; + friend class CVC5::GetModelCommand; + friend class CVC5::SynthFunCommand; friend class DatatypeConstructor; friend class DatatypeConstructorDecl; friend class DatatypeSelector; @@ -700,7 +700,7 @@ class CVC4_EXPORT Sort private: /** @return the internal wrapped TypeNode of this sort. */ - const CVC4::TypeNode& getTypeNode(void) const; + const CVC5::TypeNode& getTypeNode(void) const; /** Helper to convert a set of Sorts to internal TypeNodes. */ std::set<TypeNode> static sortSetToTypeNodes(const std::set<Sort>& sorts); @@ -717,7 +717,7 @@ class CVC4_EXPORT Sort * @param t the internal type that is to be wrapped by this sort * @return the Sort */ - Sort(const Solver* slv, const CVC4::TypeNode& t); + Sort(const Solver* slv, const CVC5::TypeNode& t); /** * Helper for isNull checks. This prevents calling an API function with @@ -733,10 +733,10 @@ class CVC4_EXPORT Sort /** * The interal type wrapped by this sort. * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due - * to memory allocation (CVC4::Type is already ref counted, so this + * to memory allocation (CVC5::Type is already ref counted, so this * could be a unique_ptr instead). */ - std::shared_ptr<CVC4::TypeNode> d_type; + std::shared_ptr<CVC5::TypeNode> d_type; }; /** @@ -847,7 +847,7 @@ class CVC4_EXPORT Op * @param n the internal node that is to be wrapped by this term * @return the Term */ - Op(const Solver* slv, const Kind k, const CVC4::Node& n); + Op(const Solver* slv, const Kind k, const CVC5::Node& n); /** * Helper for isNull checks. This prevents calling an API function with @@ -874,10 +874,10 @@ class CVC4_EXPORT Op /** * The internal node wrapped by this operator. * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due - * to memory allocation (CVC4::Node is already ref counted, so this + * to memory allocation (CVC5::Node is already ref counted, so this * could be a unique_ptr instead). */ - std::shared_ptr<CVC4::Node> d_node; + std::shared_ptr<CVC5::Node> d_node; }; /* -------------------------------------------------------------------------- */ @@ -889,25 +889,25 @@ class CVC4_EXPORT Op */ class CVC4_EXPORT Term { - friend class CVC4::AssertCommand; - friend class CVC4::BlockModelValuesCommand; - friend class CVC4::CheckSatCommand; - friend class CVC4::CheckSatAssumingCommand; - friend class CVC4::DeclareSygusVarCommand; - friend class CVC4::DefineFunctionCommand; - friend class CVC4::DefineFunctionRecCommand; - friend class CVC4::GetAbductCommand; - friend class CVC4::GetInterpolCommand; - friend class CVC4::GetModelCommand; - friend class CVC4::GetQuantifierEliminationCommand; - friend class CVC4::GetUnsatCoreCommand; - friend class CVC4::GetValueCommand; - friend class CVC4::SetUserAttributeCommand; - friend class CVC4::SimplifyCommand; - friend class CVC4::SygusConstraintCommand; - friend class CVC4::SygusInvConstraintCommand; - friend class CVC4::SynthFunCommand; - friend class CVC4::QueryCommand; + friend class CVC5::AssertCommand; + friend class CVC5::BlockModelValuesCommand; + friend class CVC5::CheckSatCommand; + friend class CVC5::CheckSatAssumingCommand; + friend class CVC5::DeclareSygusVarCommand; + friend class CVC5::DefineFunctionCommand; + friend class CVC5::DefineFunctionRecCommand; + friend class CVC5::GetAbductCommand; + friend class CVC5::GetInterpolCommand; + friend class CVC5::GetModelCommand; + friend class CVC5::GetQuantifierEliminationCommand; + friend class CVC5::GetUnsatCoreCommand; + friend class CVC5::GetValueCommand; + friend class CVC5::SetUserAttributeCommand; + friend class CVC5::SimplifyCommand; + friend class CVC5::SygusConstraintCommand; + friend class CVC5::SygusInvConstraintCommand; + friend class CVC5::SynthFunCommand; + friend class CVC5::QueryCommand; friend class Datatype; friend class DatatypeConstructor; friend class DatatypeSelector; @@ -1116,7 +1116,7 @@ class CVC4_EXPORT Term * @param p the position of the iterator (e.g. which child it's on) */ const_iterator(const Solver* slv, - const std::shared_ptr<CVC4::Node>& e, + const std::shared_ptr<CVC5::Node>& e, uint32_t p); /** @@ -1169,7 +1169,7 @@ class CVC4_EXPORT Term */ const Solver* d_solver; /** The original node to be iterated over. */ - std::shared_ptr<CVC4::Node> d_origNode; + std::shared_ptr<CVC5::Node> d_origNode; /** Keeps track of the iteration position. */ uint32_t d_pos; }; @@ -1259,10 +1259,10 @@ class CVC4_EXPORT Term * @param n the internal node that is to be wrapped by this term * @return the Term */ - Term(const Solver* slv, const CVC4::Node& n); + Term(const Solver* slv, const CVC5::Node& n); /** @return the internal wrapped Node of this term. */ - const CVC4::Node& getNode(void) const; + const CVC5::Node& getNode(void) const; /** * Helper for isNull checks. This prevents calling an API function with @@ -1285,10 +1285,10 @@ class CVC4_EXPORT Term /** * The internal node wrapped by this term. * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due - * to memory allocation (CVC4::Node is already ref counted, so this + * to memory allocation (CVC5::Node is already ref counted, so this * could be a unique_ptr instead). */ - std::shared_ptr<CVC4::Node> d_node; + std::shared_ptr<CVC5::Node> d_node; }; /** @@ -1445,9 +1445,9 @@ class CVC4_EXPORT DatatypeConstructorDecl * The internal (intermediate) datatype constructor wrapped by this * datatype constructor declaration. * Note: This is a shared_ptr rather than a unique_ptr since - * CVC4::DTypeConstructor is not ref counted. + * CVC5::DTypeConstructor is not ref counted. */ - std::shared_ptr<CVC4::DTypeConstructor> d_ctor; + std::shared_ptr<CVC5::DTypeConstructor> d_ctor; }; class Solver; @@ -1534,7 +1534,7 @@ class CVC4_EXPORT DatatypeDecl bool isCoDatatype = false); /** @return the internal wrapped Dtype of this datatype declaration. */ - CVC4::DType& getDatatype(void) const; + CVC5::DType& getDatatype(void) const; /** * Helper for isNull checks. This prevents calling an API function with @@ -1550,10 +1550,10 @@ class CVC4_EXPORT DatatypeDecl /** * The internal (intermediate) datatype wrapped by this datatype * declaration. - * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is + * Note: This is a shared_ptr rather than a unique_ptr since CVC5::DType is * not ref counted. */ - std::shared_ptr<CVC4::DType> d_dtype; + std::shared_ptr<CVC5::DType> d_dtype; }; /** @@ -1604,7 +1604,7 @@ class CVC4_EXPORT DatatypeSelector * @param stor the internal datatype selector to be wrapped * @return the DatatypeSelector */ - DatatypeSelector(const Solver* slv, const CVC4::DTypeSelector& stor); + DatatypeSelector(const Solver* slv, const CVC5::DTypeSelector& stor); /** * Helper for isNull checks. This prevents calling an API function with @@ -1619,10 +1619,10 @@ class CVC4_EXPORT DatatypeSelector /** * The internal datatype selector wrapped by this datatype selector. - * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is + * Note: This is a shared_ptr rather than a unique_ptr since CVC5::DType is * not ref counted. */ - std::shared_ptr<CVC4::DTypeSelector> d_stor; + std::shared_ptr<CVC5::DTypeSelector> d_stor; }; /** @@ -1785,7 +1785,7 @@ class CVC4_EXPORT DatatypeConstructor * @param true if this is a begin() iterator */ const_iterator(const Solver* slv, - const CVC4::DTypeConstructor& ctor, + const CVC5::DTypeConstructor& ctor, bool begin); /** @@ -1823,7 +1823,7 @@ class CVC4_EXPORT DatatypeConstructor * @param ctor the internal datatype constructor to be wrapped * @return the DatatypeConstructor */ - DatatypeConstructor(const Solver* slv, const CVC4::DTypeConstructor& ctor); + DatatypeConstructor(const Solver* slv, const CVC5::DTypeConstructor& ctor); /** * Return selector for name. @@ -1845,10 +1845,10 @@ class CVC4_EXPORT DatatypeConstructor /** * The internal datatype constructor wrapped by this datatype constructor. - * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is + * Note: This is a shared_ptr rather than a unique_ptr since CVC5::DType is * not ref counted. */ - std::shared_ptr<CVC4::DTypeConstructor> d_ctor; + std::shared_ptr<CVC5::DTypeConstructor> d_ctor; }; /* @@ -2007,7 +2007,7 @@ class CVC4_EXPORT Datatype * @param dtype the internal datatype to iterate over * @param true if this is a begin() iterator */ - const_iterator(const Solver* slv, const CVC4::DType& dtype, bool begin); + const_iterator(const Solver* slv, const CVC5::DType& dtype, bool begin); /** * The associated solver object. @@ -2044,7 +2044,7 @@ class CVC4_EXPORT Datatype * @param dtype the internal datatype to be wrapped * @return the Datatype */ - Datatype(const Solver* slv, const CVC4::DType& dtype); + Datatype(const Solver* slv, const CVC5::DType& dtype); /** * Return constructor for name. @@ -2066,10 +2066,10 @@ class CVC4_EXPORT Datatype /** * The internal datatype wrapped by this datatype. - * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is + * Note: This is a shared_ptr rather than a unique_ptr since CVC5::DType is * not ref counted. */ - std::shared_ptr<CVC4::DType> d_dtype; + std::shared_ptr<CVC5::DType> d_dtype; }; /** @@ -2135,9 +2135,9 @@ std::ostream& operator<<(std::ostream& out, */ class CVC4_EXPORT Grammar { - friend class CVC4::GetAbductCommand; - friend class CVC4::GetInterpolCommand; - friend class CVC4::SynthFunCommand; + friend class CVC5::GetAbductCommand; + friend class CVC5::GetInterpolCommand; + friend class CVC5::SynthFunCommand; friend class Solver; public: @@ -3704,5 +3704,5 @@ class CVC4_EXPORT Solver }; } // namespace api -} // namespace CVC4 +} // namespace CVC5 #endif |