From 4180569420806f06fdfd7b9ab24f4d3d7724959e Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 4 Mar 2021 12:07:13 -0800 Subject: [PATCH] New C++ Api: Clean up usage of internal types in Term. (#6054) This disables the temporarily available internals of Term. Note: getExpr() is still available and will be disabled when the API is fully converted to Nodes. --- src/api/cvc4cpp.cpp | 74 ++++++++++-------------- src/api/cvc4cpp.h | 135 +++++++++++++++++++++++++++----------------- src/smt/command.cpp | 20 +++---- 3 files changed, 125 insertions(+), 104 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 380a427ff..6f226b295 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1826,8 +1826,8 @@ Term Term::substitute(const std::vector es, << "Expecting terms of comparable sort in substitute"; } - std::vector nodes = termVectorToNodes(es); - std::vector nodeReplacements = termVectorToNodes(replacements); + std::vector nodes = Term::termVectorToNodes(es); + std::vector nodeReplacements = Term::termVectorToNodes(replacements); return Term(d_solver, d_node->substitute(nodes.begin(), nodes.end(), @@ -2124,8 +2124,8 @@ Term::const_iterator Term::end() const return Term::const_iterator(d_solver, d_node, endpos); } -// !!! This is only temporarily available until the parser is fully migrated -// to the new API. !!! +//// !!! This is only temporarily available until the parser is fully migrated +//// to the new API. !!! CVC4::Expr Term::getExpr(void) const { if (d_node->isNull()) @@ -2136,8 +2136,6 @@ CVC4::Expr Term::getExpr(void) const return d_node->toExpr(); } -// !!! This is only temporarily available until the parser is fully migrated -// to the new API. !!! const CVC4::Node& Term::getNode(void) const { return *d_node; } namespace detail { @@ -2233,6 +2231,7 @@ bool Term::isString() const { return d_node->getKind() == CVC4::Kind::CONST_STRING; } + std::wstring Term::getString() const { CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::CONST_STRING) @@ -2240,6 +2239,16 @@ std::wstring Term::getString() const return d_node->getConst().toWString(); } +std::vector Term::termVectorToNodes(const std::vector& terms) +{ + std::vector res; + for (const Term& t : terms) + { + res.push_back(t.getNode()); + } + return res; +} + std::ostream& operator<<(std::ostream& out, const Term& t) { out << t.toString(); @@ -3198,13 +3207,13 @@ Term Grammar::purifySygusGTerm( // it's an indexed operator so we should provide the op NodeBuilder<> nb(term.d_node->getKind()); nb << term.d_node->getOperator(); - nb.append(termVectorToNodes(pchildren)); + nb.append(Term::termVectorToNodes(pchildren)); nret = nb.constructNode(); } else { - nret = d_solver->getNodeManager()->mkNode(term.d_node->getKind(), - termVectorToNodes(pchildren)); + nret = d_solver->getNodeManager()->mkNode( + term.d_node->getKind(), Term::termVectorToNodes(pchildren)); } return Term(d_solver, nret); @@ -4530,7 +4539,7 @@ Term Solver::mkTermHelper(const Op& op, const std::vector& children) const } const CVC4::Kind int_kind = extToIntKind(op.d_kind); - std::vector echildren = termVectorToNodes(children); + std::vector echildren = Term::termVectorToNodes(children); NodeBuilder<> nb(int_kind); nb << *op.d_node; @@ -4856,7 +4865,7 @@ Result Solver::checkEntailed(const std::vector& terms) const CVC4_API_ARG_CHECK_NOT_NULL(term); } - std::vector exprs = termVectorToNodes(terms); + std::vector exprs = Term::termVectorToNodes(terms); CVC4::Result r = d_smtEngine->checkEntailed(exprs); return Result(r); @@ -4927,7 +4936,7 @@ Result Solver::checkSatAssuming(const std::vector& assumptions) const CVC4_API_SOLVER_CHECK_TERM(term); CVC4_API_ARG_CHECK_NOT_NULL(term); } - std::vector eassumptions = termVectorToNodes(assumptions); + std::vector eassumptions = Term::termVectorToNodes(assumptions); CVC4::Result r = d_smtEngine->checkSat(eassumptions); return Result(r); CVC4_API_SOLVER_TRY_CATCH_END; @@ -5043,7 +5052,7 @@ Term Solver::defineFun(const std::string& symbol, type = nm->mkFunctionType(domain_types, type); } Node fun = Node::fromExpr(d_exprMgr->mkVar(symbol, type.toType())); - std::vector ebound_vars = termVectorToNodes(bound_vars); + std::vector ebound_vars = Term::termVectorToNodes(bound_vars); d_smtEngine->defineFunction(fun, ebound_vars, *term.d_node, global); return Term(this, fun); CVC4_API_SOLVER_TRY_CATCH_END; @@ -5093,7 +5102,7 @@ Term Solver::defineFun(Term fun, CVC4_API_SOLVER_CHECK_TERM(term); - std::vector ebound_vars = termVectorToNodes(bound_vars); + std::vector ebound_vars = Term::termVectorToNodes(bound_vars); d_smtEngine->defineFunction(*fun.d_node, ebound_vars, *term.d_node, global); return fun; CVC4_API_SOLVER_TRY_CATCH_END; @@ -5151,7 +5160,7 @@ Term Solver::defineFunRec(const std::string& symbol, type = nm->mkFunctionType(domain_types, type); } Node fun = Node::fromExpr(d_exprMgr->mkVar(symbol, type.toType())); - std::vector ebound_vars = termVectorToNodes(bound_vars); + std::vector ebound_vars = Term::termVectorToNodes(bound_vars); d_smtEngine->defineFunctionRec( fun, ebound_vars, term.d_node->toExpr(), global); return Term(this, fun); @@ -5209,7 +5218,7 @@ Term Solver::defineFunRec(Term fun, } CVC4_API_SOLVER_CHECK_TERM(term); - std::vector ebound_vars = termVectorToNodes(bound_vars); + std::vector ebound_vars = Term::termVectorToNodes(bound_vars); d_smtEngine->defineFunctionRec( *fun.d_node, ebound_vars, *term.d_node, global); return fun; @@ -5287,14 +5296,14 @@ void Solver::defineFunsRec(const std::vector& funs, << "function or nullary symbol"; } } - std::vector efuns = termVectorToNodes(funs); + std::vector efuns = Term::termVectorToNodes(funs); std::vector> ebound_vars; for (const auto& v : bound_vars) { - ebound_vars.push_back(termVectorToNodes(v)); + ebound_vars.push_back(Term::termVectorToNodes(v)); } - std::vector exprs = termVectorToNodes(terms); - d_smtEngine->defineFunctionsRec(efuns, ebound_vars, exprs, global); + std::vector nodes = Term::termVectorToNodes(terms); + d_smtEngine->defineFunctionsRec(efuns, ebound_vars, nodes, global); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -5617,7 +5626,7 @@ void Solver::blockModelValues(const std::vector& terms) const << "a term associated to this solver object"; } CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); - d_smtEngine->blockModelValues(termVectorToNodes(terms)); + d_smtEngine->blockModelValues(Term::termVectorToNodes(terms)); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -5872,7 +5881,7 @@ Term Solver::synthFunHelper(const std::string& symbol, Node fun = getNodeManager()->mkBoundVar(symbol, funType); (void)fun.getType(true); /* kick off type checking */ - std::vector bvns = termVectorToNodes(boundVars); + std::vector bvns = Term::termVectorToNodes(boundVars); d_smtEngine->declareSynthFun( fun, g == nullptr ? funType : *g->resolve().d_type, isInv, bvns); @@ -6060,27 +6069,6 @@ std::vector termVectorToExprs(const std::vector& terms) return exprs; } -std::vector termVectorToNodes(const std::vector& terms) -{ - std::vector res; - for (const Term& t : terms) - { - res.push_back(t.getNode()); - } - return res; -} - -std::vector exprVectorToTerms(const Solver* slv, - const std::vector& exprs) -{ - std::vector terms; - for (size_t i = 0, esize = exprs.size(); i < esize; i++) - { - terms.push_back(Term(slv, exprs[i])); - } - return terms; -} - } // namespace api /* -------------------------------------------------------------------------- */ diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 00326204e..d343bc5a1 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -39,26 +39,41 @@ namespace CVC4 { template class NodeTemplate; typedef NodeTemplate Node; + +class AssertCommand; +class BlockModelValuesCommand; +class CheckSatCommand; +class CheckSatAssumingCommand; class Expr; class DatatypeDeclarationCommand; class DeclareFunctionCommand; class DeclareHeapCommand; class DeclareSortCommand; class DeclareSygusVarCommand; +class DefineFunctionCommand; +class DefineFunctionRecCommand; class DefineSortCommand; class DType; class DTypeConstructor; class DTypeSelector; class ExprManager; class GetAbductCommand; -class GetModelCommand; class GetInterpolCommand; +class GetModelCommand; +class GetQuantifierEliminationCommand; +class GetUnsatCoreCommand; +class GetValueCommand; class NodeManager; +class SetUserAttributeCommand; +class SimplifyCommand; class SmtEngine; +class SygusConstraintCommand; +class SygusInvConstraintCommand; class SynthFunCommand; class Type; class TypeNode; class Options; +class QueryCommand; class Random; class Result; @@ -890,33 +905,33 @@ class CVC4_PUBLIC Op */ class CVC4_PUBLIC 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 Datatype; friend class DatatypeConstructor; + friend class DatatypeSelector; friend class Solver; friend class Grammar; friend struct TermHashFunction; public: - // !!! This constructor is only temporarily public until the parser is fully - // migrated to the new API. !!! - /** - * Constructor. - * @param slv the associated solver object - * @param e the internal expression that is to be wrapped by this term - * @return the Term - */ - Term(const Solver* slv, const CVC4::Expr& e); - - // !!! This constructor is only temporarily public until the parser is fully - // migrated to the new API. !!! - /** - * Constructor. - * @param slv the associated solver object - * @param n the internal node that is to be wrapped by this term - * @return the Term - */ - Term(const Solver* slv, const CVC4::Node& n); - /** * Constructor. */ @@ -973,11 +988,7 @@ class CVC4_PUBLIC Term */ bool operator>=(const Term& t) const; - /** - * Returns the number of children of this term. - * - * @return the number of term - */ + /** @return the number of children of this term */ size_t getNumChildren() const; /** @@ -1193,60 +1204,62 @@ class CVC4_PUBLIC Term // to the new API. !!! CVC4::Expr getExpr(void) const; - // !!! This is only temporarily available until the parser is fully migrated - // to the new API. !!! - const CVC4::Node& getNode(void) const; - /** - * Returns true if the term is an integer that fits within std::int32_t. + * @return true if the term is an integer that fits within std::int32_t. */ bool isInt32() const; /** - * Returns the stored integer as a std::int32_t. Asserts isInt32(). + * @return the stored integer as a std::int32_t. + * Note: Asserts isInt32(). */ std::int32_t getInt32() const; /** - * Returns true if the term is an integer that fits within std::uint32_t. + * @return true if the term is an integer that fits within std::uint32_t. */ bool isUInt32() const; /** - * Returns the stored integer as a std::uint32_t. Asserts isUInt32(). + * @return the stored integer as a std::uint32_t. + * Note: Asserts isUInt32(). */ std::uint32_t getUInt32() const; /** - * Returns true if the term is an integer that fits within std::int64_t. + * @return true if the term is an integer that fits within std::int64_t. */ bool isInt64() const; /** - * Returns the stored integer as a std::int64_t. Asserts isInt64(). + * @return the stored integer as a std::int64_t. + * Note: Asserts isInt64(). */ std::int64_t getInt64() const; /** - * Returns true if the term is an integer that fits within std::uint64_t. + * @return true if the term is an integer that fits within std::uint64_t. */ bool isUInt64() const; /** - * Returns the stored integer as a std::uint64_t. Asserts isUInt64(). + * @return the stored integer as a std::uint64_t. + * Note: Asserts isUInt64(). */ std::uint64_t getUInt64() const; /** - * Returns true if the term is an integer. + * @return true if the term is an integer. */ bool isInteger() const; /** - * Returns the stored integer in (decimal) string representation. Asserts - * isInteger(). + * @return the stored integer in (decimal) string representation. + * Note: Asserts isInteger(). */ std::string getInteger() const; /** - * Returns true if the term is a string constant. + * @return true if the term is a string constant. */ bool isString() const; /** - * Returns the stored string constant. This method is not to be confused with - * toString() which returns the term in some string representation, whatever - * data it may hold. Asserts isString(). + * @return the stored string constant. + * + * Note: This method is not to be confused with toString() which returns the + * term in some string representation, whatever data it may hold. + * Asserts isString(). */ std::wstring getString() const; @@ -1257,6 +1270,28 @@ class CVC4_PUBLIC Term const Solver* d_solver; private: + /* Helper to convert a vector of Terms to internal Nodes. */ + std::vector static termVectorToNodes(const std::vector& terms); + + /** + * Constructor. + * @param slv the associated solver object + * @param e the internal expression that is to be wrapped by this term + * @return the Term + */ + Term(const Solver* slv, const CVC4::Expr& e); + + /** + * Constructor. + * @param slv the associated solver object + * @param n the internal node that is to be wrapped by this term + * @return the Term + */ + Term(const Solver* slv, const CVC4::Node& n); + + /** @return the internal wrapped Node of this term. */ + const CVC4::Node& getNode(void) const; + /** * Helper for isNull checks. This prevents calling an API function with * CVC4_API_CHECK_NOT_NULL @@ -1271,7 +1306,7 @@ class CVC4_PUBLIC Term Kind getKindHelper() const; /** - * returns true if the current term is a constant integer that is casted into + * @return true if the current term is a constant integer that is casted into * real using the operator CAST_TO_REAL, and returns false otherwise */ bool isCastedReal() const; @@ -1439,6 +1474,7 @@ class CVC4_PUBLIC DatatypeConstructorDecl }; class Solver; + /** * A CVC4 datatype declaration. */ @@ -2160,7 +2196,6 @@ class CVC4_PUBLIC Grammar const std::vector& ntSymbols); /** - * Returns the resolved datatype of the Start symbol of the grammar. * @return the resolved datatype of the Start symbol of the grammar */ Sort resolve(); @@ -2187,7 +2222,8 @@ class CVC4_PUBLIC Grammar Term term, const std::unordered_map& ntsToUnres) const; - /** Purify sygus grammar term + /** + * Purify SyGuS grammar term. * * This returns a term where all occurrences of non-terminal symbols (those * in the domain of ) are replaced by fresh variables. For @@ -3646,9 +3682,6 @@ class CVC4_PUBLIC Solver // !!! Only temporarily public until the parser is fully migrated to the // new API. !!! std::vector termVectorToExprs(const std::vector& terms); -std::vector termVectorToNodes(const std::vector& terms); -std::vector exprVectorToTerms(const Solver* slv, - const std::vector& terms); } // namespace api diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 3b723de1f..a6b528661 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -532,7 +532,7 @@ void CheckSatAssumingCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdCheckSatAssuming( - out, api::termVectorToNodes(d_terms)); + out, api::Term::termVectorToNodes(d_terms)); } /* -------------------------------------------------------------------------- */ @@ -678,7 +678,7 @@ void SynthFunCommand::toStream(std::ostream& out, size_t dag, OutputLanguage language) const { - std::vector nodeVars = termVectorToNodes(d_vars); + std::vector nodeVars = api::Term::termVectorToNodes(d_vars); Printer::getPrinter(language)->toStreamCmdSynthFun( out, d_fun.getNode(), @@ -1289,7 +1289,7 @@ void DefineFunctionCommand::toStream(std::ostream& out, Printer::getPrinter(language)->toStreamCmdDefineFunction( out, d_func.toString(), - api::termVectorToNodes(d_formals), + api::Term::termVectorToNodes(d_formals), d_func.getNode().getType().getRangeType(), d_formula.getNode()); } @@ -1369,14 +1369,14 @@ void DefineFunctionRecCommand::toStream(std::ostream& out, formals.reserve(d_formals.size()); for (const std::vector& formal : d_formals) { - formals.push_back(api::termVectorToNodes(formal)); + formals.push_back(api::Term::termVectorToNodes(formal)); } Printer::getPrinter(language)->toStreamCmdDefineFunctionRec( out, - api::termVectorToNodes(d_funcs), + api::Term::termVectorToNodes(d_funcs), formals, - api::termVectorToNodes(d_formulas)); + api::Term::termVectorToNodes(d_formulas)); } /* -------------------------------------------------------------------------- */ /* class DeclareHeapCommand */ @@ -1456,7 +1456,7 @@ void SetUserAttributeCommand::invoke(api::Solver* solver, SymbolManager* sm) solver->getSmtEngine()->setUserAttribute( d_attr, d_term.getNode(), - api::termVectorToNodes(d_termValues), + api::Term::termVectorToNodes(d_termValues), d_strValue); } d_commandStatus = CommandSuccess::instance(); @@ -1617,7 +1617,7 @@ void GetValueCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdGetValue( - out, api::termVectorToNodes(d_terms)); + out, api::Term::termVectorToNodes(d_terms)); } /* -------------------------------------------------------------------------- */ @@ -1870,7 +1870,7 @@ void BlockModelValuesCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdBlockModelValues( - out, api::termVectorToNodes(d_terms)); + out, api::Term::termVectorToNodes(d_terms)); } /* -------------------------------------------------------------------------- */ @@ -2374,7 +2374,7 @@ void GetUnsatCoreCommand::printResult(std::ostream& out, if (options::dumpUnsatCoresFull()) { // use the assertions - UnsatCore ucr(api::termVectorToNodes(d_result)); + UnsatCore ucr(api::Term::termVectorToNodes(d_result)); ucr.toStream(out); } else -- 2.30.2