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.
<< "Expecting terms of comparable sort in substitute";
}
- std::vector<Node> nodes = termVectorToNodes(es);
- std::vector<Node> nodeReplacements = termVectorToNodes(replacements);
+ std::vector<Node> nodes = Term::termVectorToNodes(es);
+ std::vector<Node> nodeReplacements = Term::termVectorToNodes(replacements);
return Term(d_solver,
d_node->substitute(nodes.begin(),
nodes.end(),
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())
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 {
{
return d_node->getKind() == CVC4::Kind::CONST_STRING;
}
+
std::wstring Term::getString() const
{
CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::CONST_STRING)
return d_node->getConst<CVC4::String>().toWString();
}
+std::vector<Node> Term::termVectorToNodes(const std::vector<Term>& terms)
+{
+ std::vector<Node> 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();
// 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);
}
const CVC4::Kind int_kind = extToIntKind(op.d_kind);
- std::vector<Node> echildren = termVectorToNodes(children);
+ std::vector<Node> echildren = Term::termVectorToNodes(children);
NodeBuilder<> nb(int_kind);
nb << *op.d_node;
CVC4_API_ARG_CHECK_NOT_NULL(term);
}
- std::vector<Node> exprs = termVectorToNodes(terms);
+ std::vector<Node> exprs = Term::termVectorToNodes(terms);
CVC4::Result r = d_smtEngine->checkEntailed(exprs);
return Result(r);
CVC4_API_SOLVER_CHECK_TERM(term);
CVC4_API_ARG_CHECK_NOT_NULL(term);
}
- std::vector<Node> eassumptions = termVectorToNodes(assumptions);
+ std::vector<Node> eassumptions = Term::termVectorToNodes(assumptions);
CVC4::Result r = d_smtEngine->checkSat(eassumptions);
return Result(r);
CVC4_API_SOLVER_TRY_CATCH_END;
type = nm->mkFunctionType(domain_types, type);
}
Node fun = Node::fromExpr(d_exprMgr->mkVar(symbol, type.toType()));
- std::vector<Node> ebound_vars = termVectorToNodes(bound_vars);
+ std::vector<Node> 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;
CVC4_API_SOLVER_CHECK_TERM(term);
- std::vector<Node> ebound_vars = termVectorToNodes(bound_vars);
+ std::vector<Node> 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;
type = nm->mkFunctionType(domain_types, type);
}
Node fun = Node::fromExpr(d_exprMgr->mkVar(symbol, type.toType()));
- std::vector<Node> ebound_vars = termVectorToNodes(bound_vars);
+ std::vector<Node> ebound_vars = Term::termVectorToNodes(bound_vars);
d_smtEngine->defineFunctionRec(
fun, ebound_vars, term.d_node->toExpr(), global);
return Term(this, fun);
}
CVC4_API_SOLVER_CHECK_TERM(term);
- std::vector<Node> ebound_vars = termVectorToNodes(bound_vars);
+ std::vector<Node> ebound_vars = Term::termVectorToNodes(bound_vars);
d_smtEngine->defineFunctionRec(
*fun.d_node, ebound_vars, *term.d_node, global);
return fun;
<< "function or nullary symbol";
}
}
- std::vector<Node> efuns = termVectorToNodes(funs);
+ std::vector<Node> efuns = Term::termVectorToNodes(funs);
std::vector<std::vector<Node>> ebound_vars;
for (const auto& v : bound_vars)
{
- ebound_vars.push_back(termVectorToNodes(v));
+ ebound_vars.push_back(Term::termVectorToNodes(v));
}
- std::vector<Node> exprs = termVectorToNodes(terms);
- d_smtEngine->defineFunctionsRec(efuns, ebound_vars, exprs, global);
+ std::vector<Node> nodes = Term::termVectorToNodes(terms);
+ d_smtEngine->defineFunctionsRec(efuns, ebound_vars, nodes, global);
CVC4_API_SOLVER_TRY_CATCH_END;
}
<< "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;
}
Node fun = getNodeManager()->mkBoundVar(symbol, funType);
(void)fun.getType(true); /* kick off type checking */
- std::vector<Node> bvns = termVectorToNodes(boundVars);
+ std::vector<Node> bvns = Term::termVectorToNodes(boundVars);
d_smtEngine->declareSynthFun(
fun, g == nullptr ? funType : *g->resolve().d_type, isInv, bvns);
return exprs;
}
-std::vector<Node> termVectorToNodes(const std::vector<Term>& terms)
-{
- std::vector<Node> res;
- for (const Term& t : terms)
- {
- res.push_back(t.getNode());
- }
- return res;
-}
-
-std::vector<Term> exprVectorToTerms(const Solver* slv,
- const std::vector<Expr>& exprs)
-{
- std::vector<Term> terms;
- for (size_t i = 0, esize = exprs.size(); i < esize; i++)
- {
- terms.push_back(Term(slv, exprs[i]));
- }
- return terms;
-}
-
} // namespace api
/* -------------------------------------------------------------------------- */
template <bool ref_count>
class NodeTemplate;
typedef NodeTemplate<true> 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;
*/
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.
*/
*/
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;
/**
// 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;
const Solver* d_solver;
private:
+ /* Helper to convert a vector of Terms to internal Nodes. */
+ std::vector<Node> static termVectorToNodes(const std::vector<Term>& 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
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;
};
class Solver;
+
/**
* A CVC4 datatype declaration.
*/
const std::vector<Term>& 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();
Term term,
const std::unordered_map<Term, Sort, TermHashFunction>& 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 <ntsToUnres>) are replaced by fresh variables. For
// !!! Only temporarily public until the parser is fully migrated to the
// new API. !!!
std::vector<Expr> termVectorToExprs(const std::vector<Term>& terms);
-std::vector<Node> termVectorToNodes(const std::vector<Term>& terms);
-std::vector<Term> exprVectorToTerms(const Solver* slv,
- const std::vector<Expr>& terms);
} // namespace api
OutputLanguage language) const
{
Printer::getPrinter(language)->toStreamCmdCheckSatAssuming(
- out, api::termVectorToNodes(d_terms));
+ out, api::Term::termVectorToNodes(d_terms));
}
/* -------------------------------------------------------------------------- */
size_t dag,
OutputLanguage language) const
{
- std::vector<Node> nodeVars = termVectorToNodes(d_vars);
+ std::vector<Node> nodeVars = api::Term::termVectorToNodes(d_vars);
Printer::getPrinter(language)->toStreamCmdSynthFun(
out,
d_fun.getNode(),
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());
}
formals.reserve(d_formals.size());
for (const std::vector<api::Term>& 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 */
solver->getSmtEngine()->setUserAttribute(
d_attr,
d_term.getNode(),
- api::termVectorToNodes(d_termValues),
+ api::Term::termVectorToNodes(d_termValues),
d_strValue);
}
d_commandStatus = CommandSuccess::instance();
OutputLanguage language) const
{
Printer::getPrinter(language)->toStreamCmdGetValue(
- out, api::termVectorToNodes(d_terms));
+ out, api::Term::termVectorToNodes(d_terms));
}
/* -------------------------------------------------------------------------- */
OutputLanguage language) const
{
Printer::getPrinter(language)->toStreamCmdBlockModelValues(
- out, api::termVectorToNodes(d_terms));
+ out, api::Term::termVectorToNodes(d_terms));
}
/* -------------------------------------------------------------------------- */
if (options::dumpUnsatCoresFull())
{
// use the assertions
- UnsatCore ucr(api::termVectorToNodes(d_result));
+ UnsatCore ucr(api::Term::termVectorToNodes(d_result));
ucr.toStream(out);
}
else
projects / cvc5.git / commitdiff