From 080601a885e256040e5662ef02c2ef7ee42ab264 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 9 Mar 2021 15:10:40 -0800 Subject: [PATCH] New C++ Api: Use const ref for arguments when possible. (#6092) --- src/api/cvc4cpp.cpp | 144 ++++++++++++++++++++++++-------------------- src/api/cvc4cpp.h | 138 ++++++++++++++++++++++-------------------- 2 files changed, 152 insertions(+), 130 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 2af24c89b..3006eff71 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1152,9 +1152,12 @@ bool Sort::isFirstClass() const { return d_type->isFirstClass(); } bool Sort::isFunctionLike() const { return d_type->isFunctionLike(); } -bool Sort::isSubsortOf(Sort s) const { return d_type->isSubtypeOf(*s.d_type); } +bool Sort::isSubsortOf(const Sort& s) const +{ + return d_type->isSubtypeOf(*s.d_type); +} -bool Sort::isComparableTo(Sort s) const +bool Sort::isComparableTo(const Sort& s) const { return d_type->isComparableTo(*s.d_type); } @@ -1823,7 +1826,7 @@ Sort Term::getSort() const return Sort(d_solver, d_node->getType()); } -Term Term::substitute(Term e, Term replacement) const +Term Term::substitute(const Term& e, const Term& replacement) const { CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(!e.isNull()) @@ -1836,7 +1839,7 @@ Term Term::substitute(Term e, Term replacement) const d_node->substitute(TNode(*e.d_node), TNode(*replacement.d_node))); } -Term Term::substitute(const std::vector es, +Term Term::substitute(const std::vector& es, const std::vector& replacements) const { CVC4_API_CHECK_NOT_NULL; @@ -2336,7 +2339,8 @@ DatatypeConstructorDecl::~DatatypeConstructorDecl() } } -void DatatypeConstructorDecl::addSelector(const std::string& name, Sort sort) +void DatatypeConstructorDecl::addSelector(const std::string& name, + const Sort& sort) { NodeManagerScope scope(d_solver->getNodeManager()); CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) @@ -2384,7 +2388,7 @@ DatatypeDecl::DatatypeDecl(const Solver* slv, DatatypeDecl::DatatypeDecl(const Solver* slv, const std::string& name, - Sort param, + const Sort& param, bool isCoDatatype) : d_solver(slv), d_dtype(new CVC4::DType( @@ -2537,7 +2541,8 @@ Term DatatypeConstructor::getConstructorTerm() const return ctor; } -Term DatatypeConstructor::getSpecializedConstructorTerm(Sort retSort) const +Term DatatypeConstructor::getSpecializedConstructorTerm( + const Sort& retSort) const { NodeManagerScope scope(d_solver->getNodeManager()); CVC4_API_CHECK(d_ctor->isResolved()) @@ -2915,7 +2920,7 @@ Grammar::Grammar(const Solver* slv, } } -void Grammar::addRule(Term ntSymbol, Term rule) +void Grammar::addRule(const Term& ntSymbol, const Term& rule) { CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing " "it as an argument to synthFun/synthInv"; @@ -2931,7 +2936,7 @@ void Grammar::addRule(Term ntSymbol, Term rule) d_ntsToTerms[ntSymbol].push_back(rule); } -void Grammar::addRules(Term ntSymbol, std::vector rules) +void Grammar::addRules(const Term& ntSymbol, const std::vector& rules) { CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing " "it as an argument to synthFun/synthInv"; @@ -2955,7 +2960,7 @@ void Grammar::addRules(Term ntSymbol, std::vector rules) d_ntsToTerms[ntSymbol].cend(), rules.cbegin(), rules.cend()); } -void Grammar::addAnyConstant(Term ntSymbol) +void Grammar::addAnyConstant(const Term& ntSymbol) { CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing " "it as an argument to synthFun/synthInv"; @@ -2968,7 +2973,7 @@ void Grammar::addAnyConstant(Term ntSymbol) d_allowConst.insert(ntSymbol); } -void Grammar::addAnyVariable(Term ntSymbol) +void Grammar::addAnyVariable(const Term& ntSymbol) { CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing " "it as an argument to synthFun/synthInv"; @@ -3123,7 +3128,7 @@ Sort Grammar::resolve() void Grammar::addSygusConstructorTerm( DatatypeDecl& dt, - Term term, + const Term& term, const std::unordered_map& ntsToUnres) const { // At this point, we should know that dt is well founded, and that its @@ -3155,7 +3160,7 @@ void Grammar::addSygusConstructorTerm( } Term Grammar::purifySygusGTerm( - Term term, + const Term& term, std::vector& args, std::vector& cargs, const std::unordered_map& ntsToUnres) const @@ -3204,7 +3209,8 @@ Term Grammar::purifySygusGTerm( return Term(d_solver, nret); } -void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, Sort sort) const +void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, + const Sort& sort) const { Assert(!sort.isNull()); // each variable of appropriate type becomes a sygus constructor in dt. @@ -3400,7 +3406,7 @@ Term Solver::mkCharFromStrHelper(const std::string& s) const return mkValHelper(CVC4::String(cpts)); } -Term Solver::getValueHelper(Term term) const +Term Solver::getValueHelper(const Term& term) const { Node value = d_smtEngine->getValue(*term.d_node); Term res = Term(this, value); @@ -3786,7 +3792,7 @@ Sort Solver::getRoundingModeSort(void) const /* Create sorts ------------------------------------------------------- */ -Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const +Sort Solver::mkArraySort(const Sort& indexSort, const Sort& elemSort) const { NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -3828,7 +3834,7 @@ Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const CVC4_API_SOLVER_TRY_CATCH_END; } -Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const +Sort Solver::mkDatatypeSort(const DatatypeDecl& dtypedecl) const { NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -3843,7 +3849,7 @@ Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const } std::vector Solver::mkDatatypeSorts( - std::vector& dtypedecls) const + const std::vector& dtypedecls) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; std::set unresolvedSorts; @@ -3860,7 +3866,7 @@ std::vector Solver::mkDatatypeSorts( CVC4_API_SOLVER_TRY_CATCH_END; } -Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const +Sort Solver::mkFunctionSort(const Sort& domain, const Sort& codomain) const { NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -3880,7 +3886,8 @@ Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const CVC4_API_SOLVER_TRY_CATCH_END; } -Sort Solver::mkFunctionSort(const std::vector& sorts, Sort codomain) const +Sort Solver::mkFunctionSort(const std::vector& sorts, + const Sort& codomain) const { NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -3971,7 +3978,7 @@ Sort Solver::mkRecordSort( CVC4_API_SOLVER_TRY_CATCH_END; } -Sort Solver::mkSetSort(Sort elemSort) const +Sort Solver::mkSetSort(const Sort& elemSort) const { NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -3984,7 +3991,7 @@ Sort Solver::mkSetSort(Sort elemSort) const CVC4_API_SOLVER_TRY_CATCH_END; } -Sort Solver::mkBagSort(Sort elemSort) const +Sort Solver::mkBagSort(const Sort& elemSort) const { NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -3997,7 +4004,7 @@ Sort Solver::mkBagSort(Sort elemSort) const CVC4_API_SOLVER_TRY_CATCH_END; } -Sort Solver::mkSequenceSort(Sort elemSort) const +Sort Solver::mkSequenceSort(const Sort& elemSort) const { NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -4121,7 +4128,7 @@ Term Solver::mkReal(const std::string& s) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::ensureRealSort(const Term t) const +Term Solver::ensureRealSort(const Term& t) const { CVC4_API_ARG_CHECK_EXPECTED( t.getSort() == getIntegerSort() || t.getSort() == getRealSort(), @@ -4174,7 +4181,7 @@ Term Solver::mkRegexpSigma() const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkEmptySet(Sort s) const +Term Solver::mkEmptySet(const Sort& s) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isSet(), s) @@ -4187,7 +4194,7 @@ Term Solver::mkEmptySet(Sort s) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkEmptyBag(Sort s) const +Term Solver::mkEmptyBag(const Sort& s) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isBag(), s) @@ -4201,7 +4208,7 @@ Term Solver::mkEmptyBag(Sort s) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkSepNil(Sort sort) const +Term Solver::mkSepNil(const Sort& sort) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; @@ -4243,7 +4250,7 @@ Term Solver::mkChar(const std::string& s) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkEmptySequence(Sort sort) const +Term Solver::mkEmptySequence(const Sort& sort) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; @@ -4256,7 +4263,7 @@ Term Solver::mkEmptySequence(Sort sort) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkUniverseSet(Sort sort) const +Term Solver::mkUniverseSet(const Sort& sort) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; @@ -4294,7 +4301,7 @@ Term Solver::mkBitVector(uint32_t size, CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkConstArray(Sort sort, Term val) const +Term Solver::mkConstArray(const Sort& sort, const Term& val) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); @@ -4387,7 +4394,7 @@ Term Solver::mkRoundingMode(RoundingMode rm) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const +Term Solver::mkUninterpretedConst(const Sort& sort, int32_t index) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; @@ -4450,7 +4457,7 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const /* Create constants */ /* -------------------------------------------------------------------------- */ -Term Solver::mkConst(Sort sort, const std::string& symbol) const +Term Solver::mkConst(const Sort& sort, const std::string& symbol) const { NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -4465,7 +4472,7 @@ Term Solver::mkConst(Sort sort, const std::string& symbol) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkConst(Sort sort) const +Term Solver::mkConst(const Sort& sort) const { NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -4483,7 +4490,7 @@ Term Solver::mkConst(Sort sort) const /* Create variables */ /* -------------------------------------------------------------------------- */ -Term Solver::mkVar(Sort sort, const std::string& symbol) const +Term Solver::mkVar(const Sort& sort, const std::string& symbol) const { NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -4544,17 +4551,20 @@ Term Solver::mkTerm(Kind kind) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkTerm(Kind kind, Term child) const +Term Solver::mkTerm(Kind kind, const Term& child) const { return mkTermHelper(kind, std::vector{child}); } -Term Solver::mkTerm(Kind kind, Term child1, Term child2) const +Term Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const { return mkTermHelper(kind, std::vector{child1, child2}); } -Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const +Term Solver::mkTerm(Kind kind, + const Term& child1, + const Term& child2, + const Term& child3) const { // need to use internal term call to check e.g. associative construction return mkTermHelper(kind, std::vector{child1, child2, child3}); @@ -4565,7 +4575,7 @@ Term Solver::mkTerm(Kind kind, const std::vector& children) const return mkTermHelper(kind, children); } -Term Solver::mkTerm(Op op) const +Term Solver::mkTerm(const Op& op) const { NodeManagerScope scope(getNodeManager()); CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -4586,22 +4596,25 @@ Term Solver::mkTerm(Op op) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkTerm(Op op, Term child) const +Term Solver::mkTerm(const Op& op, const Term& child) const { return mkTermHelper(op, std::vector{child}); } -Term Solver::mkTerm(Op op, Term child1, Term child2) const +Term Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const { return mkTermHelper(op, std::vector{child1, child2}); } -Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const +Term Solver::mkTerm(const Op& op, + const Term& child1, + const Term& child2, + const Term& child3) const { return mkTermHelper(op, std::vector{child1, child2, child3}); } -Term Solver::mkTerm(Op op, const std::vector& children) const +Term Solver::mkTerm(const Op& op, const std::vector& children) const { return mkTermHelper(op, children); } @@ -4923,7 +4936,7 @@ Term Solver::simplify(const Term& term) CVC4_API_SOLVER_TRY_CATCH_END; } -Result Solver::checkEntailed(Term term) const +Result Solver::checkEntailed(const Term& term) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); @@ -4967,7 +4980,7 @@ Result Solver::checkEntailed(const std::vector& terms) const /** * ( assert ) */ -void Solver::assertFormula(Term term) const +void Solver::assertFormula(const Term& term) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_TERM(term); @@ -4995,7 +5008,7 @@ Result Solver::checkSat(void) const /** * ( check-sat-assuming ( ) ) */ -Result Solver::checkSatAssuming(Term assumption) const +Result Solver::checkSatAssuming(const Term& assumption) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); @@ -5060,7 +5073,7 @@ Sort Solver::declareDatatype( */ Term Solver::declareFun(const std::string& symbol, const std::vector& sorts, - Sort sort) const + const Sort& sort) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; for (size_t i = 0, size = sorts.size(); i < size; ++i) @@ -5105,8 +5118,8 @@ Sort Solver::declareSort(const std::string& symbol, uint32_t arity) const */ Term Solver::defineFun(const std::string& symbol, const std::vector& bound_vars, - Sort sort, - Term term, + const Sort& sort, + const Term& term, bool global) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -5147,9 +5160,9 @@ Term Solver::defineFun(const std::string& symbol, CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::defineFun(Term fun, +Term Solver::defineFun(const Term& fun, const std::vector& bound_vars, - Term term, + const Term& term, bool global) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -5202,8 +5215,8 @@ Term Solver::defineFun(Term fun, */ Term Solver::defineFunRec(const std::string& symbol, const std::vector& bound_vars, - Sort sort, - Term term, + const Sort& sort, + const Term& term, bool global) const { NodeManagerScope scope(getNodeManager()); @@ -5255,9 +5268,9 @@ Term Solver::defineFunRec(const std::string& symbol, CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::defineFunRec(Term fun, +Term Solver::defineFunRec(const Term& fun, const std::vector& bound_vars, - Term term, + const Term& term, bool global) const { NodeManagerScope scope(getNodeManager()); @@ -5503,7 +5516,7 @@ std::vector Solver::getUnsatCore(void) const /** * ( get-value ( ) ) */ -Term Solver::getValue(Term term) const +Term Solver::getValue(const Term& term) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_TERM(term); @@ -5536,7 +5549,7 @@ std::vector Solver::getValue(const std::vector& terms) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::getQuantifierElimination(api::Term q) const +Term Solver::getQuantifierElimination(const Term& q) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_NOT_NULL(q); @@ -5547,7 +5560,7 @@ Term Solver::getQuantifierElimination(api::Term q) const CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::getQuantifierEliminationDisjunct(api::Term q) const +Term Solver::getQuantifierEliminationDisjunct(const Term& q) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_NOT_NULL(q); @@ -5558,7 +5571,8 @@ Term Solver::getQuantifierEliminationDisjunct(api::Term q) const CVC4_API_SOLVER_TRY_CATCH_END; } -void Solver::declareSeparationHeap(api::Sort locSort, api::Sort dataSort) const +void Solver::declareSeparationHeap(const Sort& locSort, + const Sort& dataSort) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK( @@ -5623,7 +5637,7 @@ void Solver::pop(uint32_t nscopes) const CVC4_API_SOLVER_TRY_CATCH_END; } -bool Solver::getInterpolant(Term conj, Term& output) const +bool Solver::getInterpolant(const Term& conj, Term& output) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); @@ -5637,7 +5651,7 @@ bool Solver::getInterpolant(Term conj, Term& output) const CVC4_API_SOLVER_TRY_CATCH_END; } -bool Solver::getInterpolant(Term conj, Grammar& g, Term& output) const +bool Solver::getInterpolant(const Term& conj, Grammar& g, Term& output) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); @@ -5652,7 +5666,7 @@ bool Solver::getInterpolant(Term conj, Grammar& g, Term& output) const CVC4_API_SOLVER_TRY_CATCH_END; } -bool Solver::getAbduct(Term conj, Term& output) const +bool Solver::getAbduct(const Term& conj, Term& output) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); @@ -5666,7 +5680,7 @@ bool Solver::getAbduct(Term conj, Term& output) const CVC4_API_SOLVER_TRY_CATCH_END; } -bool Solver::getAbduct(Term conj, Grammar& g, Term& output) const +bool Solver::getAbduct(const Term& conj, Grammar& g, Term& output) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); @@ -5808,7 +5822,7 @@ void Solver::setOption(const std::string& option, CVC4_API_SOLVER_TRY_CATCH_END; } -Term Solver::mkSygusVar(Sort sort, const std::string& symbol) const +Term Solver::mkSygusVar(const Sort& sort, const std::string& symbol) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_NOT_NULL(sort); @@ -5869,7 +5883,7 @@ Grammar Solver::mkSygusGrammar(const std::vector& boundVars, Term Solver::synthFun(const std::string& symbol, const std::vector& boundVars, - Sort sort) const + const Sort& sort) const { return synthFunHelper(symbol, boundVars, sort); } @@ -5897,7 +5911,7 @@ Term Solver::synthInv(const std::string& symbol, symbol, boundVars, Sort(this, getNodeManager()->booleanType()), true, &g); } -void Solver::addSygusConstraint(Term term) const +void Solver::addSygusConstraint(const Term& term) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 43f79b480..938449f3f 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -489,14 +489,14 @@ class CVC4_PUBLIC Sort * Is this sort a subsort of the given sort? * @return true if this sort is a subsort of s */ - bool isSubsortOf(Sort s) const; + bool isSubsortOf(const Sort& s) const; /** * Is this sort comparable to the given sort (i.e., do they share * a common ancestor in the subsort tree)? * @return true if this sort is comparable to s */ - bool isComparableTo(Sort s) const; + bool isComparableTo(const Sort& s) const; /** * @return the underlying datatype of a datatype sort @@ -1002,13 +1002,13 @@ class CVC4_PUBLIC Term /** * @return the result of replacing "e" by "replacement" in this term */ - Term substitute(Term e, Term replacement) const; + Term substitute(const Term& e, const Term& replacement) const; /** * @return the result of simulatenously replacing "es" by "replacements" in * this term */ - Term substitute(const std::vector es, + Term substitute(const std::vector& es, const std::vector& replacements) const; /** @@ -1406,7 +1406,7 @@ class CVC4_PUBLIC DatatypeConstructorDecl * @param name the name of the datatype selector declaration to add * @param sort the range sort of the datatype selector declaration to add */ - void addSelector(const std::string& name, Sort sort); + void addSelector(const std::string& name, const Sort& sort); /** * Add datatype selector declaration whose range type is the datatype itself. * @param name the name of the datatype selector declaration to add @@ -1508,7 +1508,7 @@ class CVC4_PUBLIC DatatypeDecl */ DatatypeDecl(const Solver* slv, const std::string& name, - Sort param, + const Sort& param, bool isCoDatatype = false); /** @@ -1656,7 +1656,7 @@ class CVC4_PUBLIC DatatypeConstructor * @param retSort the desired return sort of the constructor * @return the constructor term */ - Term getSpecializedConstructorTerm(Sort retSort) const; + Term getSpecializedConstructorTerm(const Sort& retSort) const; /** * Get the tester operator of this datatype constructor. @@ -2104,27 +2104,27 @@ class CVC4_PUBLIC Grammar * @param ntSymbol the non-terminal to which the rule is added * @param rule the rule to add */ - void addRule(Term ntSymbol, Term rule); + void addRule(const Term& ntSymbol, const Term& rule); /** * Add to the set of rules corresponding to . * @param ntSymbol the non-terminal to which the rules are added * @param rule the rules to add */ - void addRules(Term ntSymbol, std::vector rules); + void addRules(const Term& ntSymbol, const std::vector& rules); /** * Allow to be an arbitrary constant. * @param ntSymbol the non-terminal allowed to be any constant */ - void addAnyConstant(Term ntSymbol); + void addAnyConstant(const Term& ntSymbol); /** * Allow to be any input variable to corresponding * synth-fun/synth-inv with the same sort as . * @param ntSymbol the non-terminal allowed to be any input constant */ - void addAnyVariable(Term ntSymbol); + void addAnyVariable(const Term& ntSymbol); /** * @return a string representation of this grammar. @@ -2171,7 +2171,7 @@ class CVC4_PUBLIC Grammar */ void addSygusConstructorTerm( DatatypeDecl& dt, - Term term, + const Term& term, const std::unordered_map& ntsToUnres) const; /** @@ -2193,7 +2193,7 @@ class CVC4_PUBLIC Grammar * @return the purfied term */ Term purifySygusGTerm( - Term term, + const Term& term, std::vector& args, std::vector& cargs, const std::unordered_map& ntsToUnres) const; @@ -2206,7 +2206,7 @@ class CVC4_PUBLIC Grammar * @param dt the non-terminal's datatype to which the constructors are added * @param sort the sort of the sygus variables to add */ - void addSygusConstructorVariables(DatatypeDecl& dt, Sort sort) const; + void addSygusConstructorVariables(DatatypeDecl& dt, const Sort& sort) const; /** The solver that created this grammar. */ const Solver* d_solver; @@ -2349,7 +2349,7 @@ class CVC4_PUBLIC Solver * @param elemSort the array element sort * @return the array sort */ - Sort mkArraySort(Sort indexSort, Sort elemSort) const; + Sort mkArraySort(const Sort& indexSort, const Sort& elemSort) const; /** * Create a bit-vector sort. @@ -2370,7 +2370,7 @@ class CVC4_PUBLIC Solver * @param dtypedecl the datatype declaration from which the sort is created * @return the datatype sort */ - Sort mkDatatypeSort(DatatypeDecl dtypedecl) const; + Sort mkDatatypeSort(const DatatypeDecl& dtypedecl) const; /** * Create a vector of datatype sorts. The names of the datatype declarations @@ -2380,7 +2380,7 @@ class CVC4_PUBLIC Solver * @return the datatype sorts */ std::vector mkDatatypeSorts( - std::vector& dtypedecls) const; + const std::vector& dtypedecls) const; /** * Create a vector of datatype sorts using unresolved sorts. The names of @@ -2410,7 +2410,7 @@ class CVC4_PUBLIC Solver * @param codomain the sort of the function return value * @return the function sort */ - Sort mkFunctionSort(Sort domain, Sort codomain) const; + Sort mkFunctionSort(const Sort& domain, const Sort& codomain) const; /** * Create function sort. @@ -2418,7 +2418,8 @@ class CVC4_PUBLIC Solver * @param codomain the sort of the function return value * @return the function sort */ - Sort mkFunctionSort(const std::vector& sorts, Sort codomain) const; + Sort mkFunctionSort(const std::vector& sorts, + const Sort& codomain) const; /** * Create a sort parameter. @@ -2447,21 +2448,21 @@ class CVC4_PUBLIC Solver * @param elemSort the sort of the set elements * @return the set sort */ - Sort mkSetSort(Sort elemSort) const; + Sort mkSetSort(const Sort& elemSort) const; /** * Create a bag sort. * @param elemSort the sort of the bag elements * @return the bag sort */ - Sort mkBagSort(Sort elemSort) const; + Sort mkBagSort(const Sort& elemSort) const; /** * Create a sequence sort. * @param elemSort the sort of the sequence elements * @return the sequence sort */ - Sort mkSequenceSort(Sort elemSort) const; + Sort mkSequenceSort(const Sort& elemSort) const; /** * Create an uninterpreted sort. @@ -2502,7 +2503,7 @@ class CVC4_PUBLIC Solver * @param child the child of the term * @return the Term */ - Term mkTerm(Kind kind, Term child) const; + Term mkTerm(Kind kind, const Term& child) const; /** * Create binary term of given kind. @@ -2511,7 +2512,7 @@ class CVC4_PUBLIC Solver * @param child2 the second child of the term * @return the Term */ - Term mkTerm(Kind kind, Term child1, Term child2) const; + Term mkTerm(Kind kind, const Term& child1, const Term& child2) const; /** * Create ternary term of given kind. @@ -2521,7 +2522,10 @@ class CVC4_PUBLIC Solver * @param child3 the third child of the term * @return the Term */ - Term mkTerm(Kind kind, Term child1, Term child2, Term child3) const; + Term mkTerm(Kind kind, + const Term& child1, + const Term& child2, + const Term& child3) const; /** * Create n-ary term of given kind. @@ -2537,7 +2541,7 @@ class CVC4_PUBLIC Solver * @param the operator * @return the Term */ - Term mkTerm(Op op) const; + Term mkTerm(const Op& op) const; /** * Create unary term of given kind from a given operator. @@ -2546,7 +2550,7 @@ class CVC4_PUBLIC Solver * @child the child of the term * @return the Term */ - Term mkTerm(Op op, Term child) const; + Term mkTerm(const Op& op, const Term& child) const; /** * Create binary term of given kind from a given operator. @@ -2556,7 +2560,7 @@ class CVC4_PUBLIC Solver * @child2 the second child of the term * @return the Term */ - Term mkTerm(Op op, Term child1, Term child2) const; + Term mkTerm(const Op& op, const Term& child1, const Term& child2) const; /** * Create ternary term of given kind from a given operator. @@ -2567,7 +2571,10 @@ class CVC4_PUBLIC Solver * @child3 the third child of the term * @return the Term */ - Term mkTerm(Op op, Term child1, Term child2, Term child3) const; + Term mkTerm(const Op& op, + const Term& child1, + const Term& child2, + const Term& child3) const; /** * Create n-ary term of given kind from a given operator. @@ -2576,7 +2583,7 @@ class CVC4_PUBLIC Solver * @children the children of the term * @return the Term */ - Term mkTerm(Op op, const std::vector& children) const; + Term mkTerm(const Op& op, const std::vector& children) const; /** * Create a tuple term. Terms are automatically converted if sorts are @@ -2740,21 +2747,21 @@ class CVC4_PUBLIC Solver * @param s the sort of the set elements. * @return the empty set constant */ - Term mkEmptySet(Sort s) const; + Term mkEmptySet(const Sort& s) const; /** * Create a constant representing an empty bag of the given sort. * @param s the sort of the bag elements. * @return the empty bag constant */ - Term mkEmptyBag(Sort s) const; + Term mkEmptyBag(const Sort& s) const; /** * Create a separation logic nil term. * @param sort the sort of the nil term * @return the separation logic nil term */ - Term mkSepNil(Sort sort) const; + Term mkSepNil(const Sort& sort) const; /** * Create a String constant. @@ -2791,14 +2798,14 @@ class CVC4_PUBLIC Solver * @param sort The element sort of the sequence. * @return the empty sequence with given element sort. */ - Term mkEmptySequence(Sort sort) const; + Term mkEmptySequence(const Sort& sort) const; /** * Create a universe set of the given sort. * @param sort the sort of the set elements * @return the universe set constant */ - Term mkUniverseSet(Sort sort) const; + Term mkUniverseSet(const Sort& sort) const; /** * Create a bit-vector constant of given size and value. @@ -2840,7 +2847,7 @@ class CVC4_PUBLIC Solver * @param val the constant value to store (must match the sort's element sort) * @return the constant array term */ - Term mkConstArray(Sort sort, Term val) const; + Term mkConstArray(const Sort& sort, const Term& val) const; /** * Create a positive infinity floating-point constant. Requires CVC4 to be @@ -2898,7 +2905,7 @@ class CVC4_PUBLIC Solver * @param arg1 Sort of the constant * @param arg2 Index of the constant */ - Term mkUninterpretedConst(Sort sort, int32_t index) const; + Term mkUninterpretedConst(const Sort& sort, int32_t index) const; /** * Create an abstract value constant. @@ -2934,7 +2941,7 @@ class CVC4_PUBLIC Solver * @param symbol the name of the constant * @return the first-order constant */ - Term mkConst(Sort sort, const std::string& symbol) const; + Term mkConst(const Sort& sort, const std::string& symbol) const; /** * Create (first-order) constant (0-arity function symbol), with a default * symbol name. @@ -2942,7 +2949,7 @@ class CVC4_PUBLIC Solver * @param sort the sort of the constant * @return the first-order constant */ - Term mkConst(Sort sort) const; + Term mkConst(const Sort& sort) const; /** * Create a bound variable to be used in a binder (i.e. a quantifier, a @@ -2951,7 +2958,7 @@ class CVC4_PUBLIC Solver * @param symbol the name of the variable * @return the variable */ - Term mkVar(Sort sort, const std::string& symbol = std::string()) const; + Term mkVar(const Sort& sort, const std::string& symbol = std::string()) const; /* .................................................................... */ /* Create datatype constructor declarations */ @@ -3015,7 +3022,7 @@ class CVC4_PUBLIC Solver * SMT-LIB: ( assert ) * @param term the formula to assert */ - void assertFormula(Term term) const; + void assertFormula(const Term& term) const; /** * Check satisfiability. @@ -3030,7 +3037,7 @@ class CVC4_PUBLIC Solver * @param assumption the formula to assume * @return the result of the satisfiability check. */ - Result checkSatAssuming(Term assumption) const; + Result checkSatAssuming(const Term& assumption) const; /** * Check satisfiability assuming the given formulas. @@ -3045,7 +3052,7 @@ class CVC4_PUBLIC Solver * @param term the formula to check entailment for * @return the result of the entailment check. */ - Result checkEntailed(Term term) const; + Result checkEntailed(const Term& term) const; /** * Check entailment of the given set of given formulas w.r.t. the current @@ -3075,7 +3082,7 @@ class CVC4_PUBLIC Solver */ Term declareFun(const std::string& symbol, const std::vector& sorts, - Sort sort) const; + const Sort& sort) const; /** * Declare uninterpreted sort. @@ -3099,8 +3106,8 @@ class CVC4_PUBLIC Solver */ Term defineFun(const std::string& symbol, const std::vector& bound_vars, - Sort sort, - Term term, + const Sort& sort, + const Term& term, bool global = false) const; /** * Define n-ary function. @@ -3113,9 +3120,9 @@ class CVC4_PUBLIC Solver * when popping the context) * @return the function */ - Term defineFun(Term fun, + Term defineFun(const Term& fun, const std::vector& bound_vars, - Term term, + const Term& term, bool global = false) const; /** @@ -3131,8 +3138,8 @@ class CVC4_PUBLIC Solver */ Term defineFunRec(const std::string& symbol, const std::vector& bound_vars, - Sort sort, - Term term, + const Sort& sort, + const Term& term, bool global = false) const; /** @@ -3146,9 +3153,9 @@ class CVC4_PUBLIC Solver * when popping the context) * @return the function */ - Term defineFunRec(Term fun, + Term defineFunRec(const Term& fun, const std::vector& bound_vars, - Term term, + const Term& term, bool global = false) const; /** @@ -3219,7 +3226,7 @@ class CVC4_PUBLIC Solver * @param term the term for which the value is queried * @return the value of the given term */ - Term getValue(Term term) const; + Term getValue(const Term& term) const; /** * Get the values of the given terms. * SMT-LIB: ( get-value ( + ) ) @@ -3242,7 +3249,7 @@ class CVC4_PUBLIC Solver * - ret is quantifier-free formula containing only free variables in * y1...yn. */ - Term getQuantifierElimination(api::Term q) const; + Term getQuantifierElimination(const Term& q) const; /** * Do partial quantifier elimination, which can be used for incrementally @@ -3268,7 +3275,7 @@ class CVC4_PUBLIC Solver * where ret^Q_i is the same as above. In either case, we have * that ret^Q_j will eventually be true or false, for some finite j. */ - Term getQuantifierEliminationDisjunct(api::Term q) const; + Term getQuantifierEliminationDisjunct(const Term& q) const; /** * When using separation logic, this sets the location sort and the @@ -3277,7 +3284,7 @@ class CVC4_PUBLIC Solver * @param locSort The location sort of the heap * @param dataSort The data sort of the heap */ - void declareSeparationHeap(api::Sort locSort, api::Sort dataSort) const; + void declareSeparationHeap(const Sort& locSort, const Sort& dataSort) const; /** * When using separation logic, obtain the term for the heap. @@ -3307,7 +3314,7 @@ class CVC4_PUBLIC Solver * current set of assertions and B is given in the input by conj. * @return true if it gets I successfully, false otherwise. */ - bool getInterpolant(Term conj, Term& output) const; + bool getInterpolant(const Term& conj, Term& output) const; /** * Get an interpolant @@ -3319,7 +3326,7 @@ class CVC4_PUBLIC Solver * current set of assertions and B is given in the input by conj. * @return true if it gets I successfully, false otherwise. */ - bool getInterpolant(Term conj, Grammar& g, Term& output) const; + bool getInterpolant(const Term& conj, Grammar& g, Term& output) const; /** * Get an abduct. @@ -3331,7 +3338,7 @@ class CVC4_PUBLIC Solver * given in the input by conj * @return true if it gets C successfully, false otherwise */ - bool getAbduct(Term conj, Term& output) const; + bool getAbduct(const Term& conj, Term& output) const; /** * Get an abduct. @@ -3344,7 +3351,7 @@ class CVC4_PUBLIC Solver * given in the input by conj * @return true if it gets C successfully, false otherwise */ - bool getAbduct(Term conj, Grammar& g, Term& output) const; + bool getAbduct(const Term& conj, Grammar& g, Term& output) const; /** * Block the current model. Can be called only if immediately preceded by a @@ -3422,7 +3429,8 @@ class CVC4_PUBLIC Solver * @param symbol the name of the universal variable * @return the universal variable */ - Term mkSygusVar(Sort sort, const std::string& symbol = std::string()) const; + Term mkSygusVar(const Sort& sort, + const std::string& symbol = std::string()) const; /** * Create a Sygus grammar. The first non-terminal is treated as the starting @@ -3445,7 +3453,7 @@ class CVC4_PUBLIC Solver */ Term synthFun(const std::string& symbol, const std::vector& boundVars, - Sort sort) const; + const Sort& sort) const; /** * Synthesize n-ary function following specified syntactic constraints. @@ -3490,7 +3498,7 @@ class CVC4_PUBLIC Solver * SyGuS v2: ( constraint ) * @param term the formula to add as a constraint */ - void addSygusConstraint(Term term) const; + void addSygusConstraint(const Term& term) const; /** * Add a set of Sygus constraints to the current state that correspond to an @@ -3570,7 +3578,7 @@ class CVC4_PUBLIC Solver /** Helper for mkChar functions that take a string as argument. */ Term mkCharFromStrHelper(const std::string& s) const; /** Get value helper, which accounts for subtyping */ - Term getValueHelper(Term term) const; + Term getValueHelper(const Term& term) const; /** * Helper function that ensures that a given term is of sort real (as opposed @@ -3578,7 +3586,7 @@ class CVC4_PUBLIC Solver * @param t a term of sort integer or real * @return a term of sort real */ - Term ensureRealSort(Term t) const; + Term ensureRealSort(const Term& t) const; /** * Create n-ary term of given kind. This handles the cases of left/right -- 2.30.2