From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 9 Mar 2021 23:10:40 +0000 (-0800)
Subject: New C++ Api: Use const ref for arguments when possible. (#6092)
X-Git-Tag: cvc5-1.0.0~2122
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=080601a885e256040e5662ef02c2ef7ee42ab264;p=cvc5.git

New C++ Api: Use const ref for arguments when possible. (#6092)
---

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<Term> es,
+Term Term::substitute(const std::vector<Term>& es,
                       const std::vector<Term>& 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<Term> rules)
+void Grammar::addRules(const Term& ntSymbol, const std::vector<Term>& 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<Term> 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<Term, Sort, TermHashFunction>& 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<Term>& args,
     std::vector<Sort>& cargs,
     const std::unordered_map<Term, Sort, TermHashFunction>& 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>(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<Sort> Solver::mkDatatypeSorts(
-    std::vector<DatatypeDecl>& dtypedecls) const
+    const std::vector<DatatypeDecl>& dtypedecls) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   std::set<Sort> unresolvedSorts;
@@ -3860,7 +3866,7 @@ std::vector<Sort> 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<Sort>& sorts, Sort codomain) const
+Sort Solver::mkFunctionSort(const std::vector<Sort>& 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<Term>{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<Term>{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<Term>{child1, child2, child3});
@@ -4565,7 +4575,7 @@ Term Solver::mkTerm(Kind kind, const std::vector<Term>& 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<Term>{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<Term>{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<Term>{child1, child2, child3});
 }
 
-Term Solver::mkTerm(Op op, const std::vector<Term>& children) const
+Term Solver::mkTerm(const Op& op, const std::vector<Term>& 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<Term>& terms) const
 /**
  *  ( assert <term> )
  */
-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 ( <prop_literal> ) )
  */
-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<Sort>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& bound_vars,
-                          Term term,
+                          const Term& term,
                           bool global) const
 {
   NodeManagerScope scope(getNodeManager());
@@ -5503,7 +5516,7 @@ std::vector<Term> Solver::getUnsatCore(void) const
 /**
  *  ( get-value ( <term> ) )
  */
-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<Term> Solver::getValue(const std::vector<Term>& 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<Term>& boundVars,
 
 Term Solver::synthFun(const std::string& symbol,
                       const std::vector<Term>& 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<Term> es,
+  Term substitute(const std::vector<Term>& es,
                   const std::vector<Term>& 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 <rules> to the set of rules corresponding to <ntSymbol>.
    * @param ntSymbol the non-terminal to which the rules are added
    * @param rule the rules to add
    */
-  void addRules(Term ntSymbol, std::vector<Term> rules);
+  void addRules(const Term& ntSymbol, const std::vector<Term>& rules);
 
   /**
    * Allow <ntSymbol> 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 <ntSymbol> to be any input variable to corresponding
    * synth-fun/synth-inv with the same sort as <ntSymbol>.
    * @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<Term, Sort, TermHashFunction>& ntsToUnres) const;
 
   /**
@@ -2193,7 +2193,7 @@ class CVC4_PUBLIC Grammar
    * @return the purfied term
    */
   Term purifySygusGTerm(
-      Term term,
+      const Term& term,
       std::vector<Term>& args,
       std::vector<Sort>& cargs,
       const std::unordered_map<Term, Sort, TermHashFunction>& 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<Sort> mkDatatypeSorts(
-      std::vector<DatatypeDecl>& dtypedecls) const;
+      const std::vector<DatatypeDecl>& 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<Sort>& sorts, Sort codomain) const;
+  Sort mkFunctionSort(const std::vector<Sort>& 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<Term>& children) const;
+  Term mkTerm(const Op& op, const std::vector<Term>& 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 <term> )
    * @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<Sort>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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 ( <term>+ ) )
@@ -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<Term>& 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 <term> )
    * @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