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);
}
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())
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;
}
}
-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)
DatatypeDecl::DatatypeDecl(const Solver* slv,
const std::string& name,
- Sort param,
+ const Sort& param,
bool isCoDatatype)
: d_solver(slv),
d_dtype(new CVC4::DType(
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())
}
}
-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";
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";
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";
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";
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
}
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
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.
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);
/* 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;
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;
}
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;
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;
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;
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;
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;
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;
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(),
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)
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)
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";
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";
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";
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());
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";
/* 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;
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;
/* 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;
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});
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;
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);
}
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());
/**
* ( 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);
/**
* ( 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());
*/
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)
*/
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;
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;
*/
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());
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());
/**
* ( 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);
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);
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);
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(
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());
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());
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());
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());
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);
Term Solver::synthFun(const std::string& symbol,
const std::vector<Term>& boundVars,
- Sort sort) const
+ const Sort& sort) const
{
return synthFunHelper(symbol, boundVars, sort);
}
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());
* 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
/**
* @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;
/**
* @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
*/
DatatypeDecl(const Solver* slv,
const std::string& name,
- Sort param,
+ const Sort& param,
bool isCoDatatype = false);
/**
* @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.
* @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.
*/
void addSygusConstructorTerm(
DatatypeDecl& dt,
- Term term,
+ const Term& term,
const std::unordered_map<Term, Sort, TermHashFunction>& ntsToUnres) const;
/**
* @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;
* @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;
* @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.
* @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
* @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
* @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.
* @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.
* @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.
* @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.
* @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.
* @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.
* @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.
* @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.
* @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.
* @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.
* @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
* @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.
* @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.
* @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
* @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.
* @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.
* @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
* @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 */
* SMT-LIB: ( assert <term> )
* @param term the formula to assert
*/
- void assertFormula(Term term) const;
+ void assertFormula(const Term& term) const;
/**
* Check satisfiability.
* @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.
* @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
*/
Term declareFun(const std::string& symbol,
const std::vector<Sort>& sorts,
- Sort sort) const;
+ const Sort& sort) const;
/**
* Declare uninterpreted sort.
*/
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.
* 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;
/**
*/
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;
/**
* 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;
/**
* @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>+ ) )
* - 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
* 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
* @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.
* 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
* 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.
* 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.
* 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
* @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
*/
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.
* 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
/** 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
* @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
projects / cvc5.git / commitdiff