CVC4_API_CHECK(isDefinedKind(kind)) \
<< "Invalid kind '" << kindToString(kind) << "'";
+#define CVC4_API_SORT_CHECK_SOLVER(sort)
+
#define CVC4_API_KIND_CHECK_EXPECTED(cond, kind) \
CVC4_PREDICT_TRUE(cond) \
? (void)0 \
/* Sort */
/* -------------------------------------------------------------------------- */
-Sort::Sort(const CVC4::Type& t) : d_type(new CVC4::Type(t)) {}
+Sort::Sort(const Solver* slv, const CVC4::Type& t)
+ : d_solver(slv), d_type(new CVC4::Type(t))
+{
+}
-Sort::Sort() : d_type(new CVC4::Type()) {}
+Sort::Sort() : d_solver(nullptr), d_type(new CVC4::Type()) {}
Sort::~Sort() {}
Datatype Sort::getDatatype() const
{
CVC4_API_CHECK(isDatatype()) << "Expected datatype sort.";
- return DatatypeType(*d_type).getDatatype();
+ return Datatype(d_solver, DatatypeType(*d_type).getDatatype());
}
Sort Sort::instantiate(const std::vector<Sort>& params) const
}
if (d_type->isDatatype())
{
- return DatatypeType(*d_type).instantiate(tparams);
+ return Sort(d_solver, DatatypeType(*d_type).instantiate(tparams));
}
Assert(d_type->isSortConstructor());
- return SortConstructorType(*d_type).instantiate(tparams);
+ return Sort(d_solver, SortConstructorType(*d_type).instantiate(tparams));
}
std::string Sort::toString() const { return d_type->toString(); }
{
CVC4_API_CHECK(isConstructor()) << "Not a function sort.";
std::vector<CVC4::Type> types = ConstructorType(*d_type).getArgTypes();
- return typeVectorToSorts(types);
+ return typeVectorToSorts(d_solver, types);
}
Sort Sort::getConstructorCodomainSort() const
{
CVC4_API_CHECK(isConstructor()) << "Not a function sort.";
- return ConstructorType(*d_type).getRangeType();
+ return Sort(d_solver, ConstructorType(*d_type).getRangeType());
}
/* Function sort ------------------------------------------------------- */
{
CVC4_API_CHECK(isFunction()) << "Not a function sort.";
std::vector<CVC4::Type> types = FunctionType(*d_type).getArgTypes();
- return typeVectorToSorts(types);
+ return typeVectorToSorts(d_solver, types);
}
Sort Sort::getFunctionCodomainSort() const
{
CVC4_API_CHECK(isFunction()) << "Not a function sort.";
- return FunctionType(*d_type).getRangeType();
+ return Sort(d_solver, FunctionType(*d_type).getRangeType());
}
/* Array sort ---------------------------------------------------------- */
Sort Sort::getArrayIndexSort() const
{
CVC4_API_CHECK(isArray()) << "Not an array sort.";
- return ArrayType(*d_type).getIndexType();
+ return Sort(d_solver, ArrayType(*d_type).getIndexType());
}
Sort Sort::getArrayElementSort() const
{
CVC4_API_CHECK(isArray()) << "Not an array sort.";
- return ArrayType(*d_type).getConstituentType();
+ return Sort(d_solver, ArrayType(*d_type).getConstituentType());
}
/* Set sort ------------------------------------------------------------ */
Sort Sort::getSetElementSort() const
{
CVC4_API_CHECK(isSet()) << "Not a set sort.";
- return SetType(*d_type).getElementType();
+ return Sort(d_solver, SetType(*d_type).getElementType());
}
/* Uninterpreted sort -------------------------------------------------- */
{
CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
std::vector<CVC4::Type> types = SortType(*d_type).getParamTypes();
- return typeVectorToSorts(types);
+ return typeVectorToSorts(d_solver, types);
}
/* Sort constructor sort ----------------------------------------------- */
{
CVC4_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort.";
std::vector<CVC4::Type> types = DatatypeType(*d_type).getParamTypes();
- return typeVectorToSorts(types);
+ return typeVectorToSorts(d_solver, types);
}
size_t Sort::getDatatypeArity() const
{
CVC4_API_CHECK(isTuple()) << "Not a tuple sort.";
std::vector<CVC4::Type> types = DatatypeType(*d_type).getTupleTypes();
- return typeVectorToSorts(types);
+ return typeVectorToSorts(d_solver, types);
}
/* --------------------------------------------------------------------- */
Op::Op() : d_kind(NULL_EXPR), d_expr(new CVC4::Expr()) {}
-Op::Op(const Kind k) : d_kind(k), d_expr(new CVC4::Expr()) {}
+Op::Op(const Solver* slv, const Kind k)
+ : d_solver(slv), d_kind(k), d_expr(new CVC4::Expr())
+{
+}
-Op::Op(const Kind k, const CVC4::Expr& e) : d_kind(k), d_expr(new CVC4::Expr(e))
+Op::Op(const Solver* slv, const Kind k, const CVC4::Expr& e)
+ : d_solver(slv), d_kind(k), d_expr(new CVC4::Expr(e))
{
}
/* Term */
/* -------------------------------------------------------------------------- */
-Term::Term() : d_expr(new CVC4::Expr()) {}
+Term::Term() : d_solver(nullptr), d_expr(new CVC4::Expr()) {}
-Term::Term(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {}
+Term::Term(const Solver* slv, const CVC4::Expr& e)
+ : d_solver(slv), d_expr(new CVC4::Expr(e))
+{
+}
Term::~Term() {}
-/* Helpers */
-/* -------------------------------------------------------------------------- */
-
-/* Split out to avoid nested API calls (problematic with API tracing). */
-/* .......................................................................... */
-
-bool Term::isNullHelper() const { return d_expr->isNull(); }
+bool Term::isNullHelper() const
+{
+ /* Split out to avoid nested API calls (problematic with API tracing). */
+ return d_expr->isNull();
+}
bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; }
if (index == 0)
{
// return the operator
- return api::Term(d_expr->getOperator());
+ return Term(d_solver, d_expr->getOperator());
}
// otherwise we are looking up child at (index-1)
index--;
}
- return api::Term((*d_expr)[index]);
+ return Term(d_solver, (*d_expr)[index]);
}
uint64_t Term::getId() const
Sort Term::getSort() const
{
CVC4_API_CHECK_NOT_NULL;
- return Sort(d_expr->getType());
+ return Sort(d_solver, d_expr->getType());
}
Term Term::substitute(Term e, Term replacement) const
<< "Expected non-null term as replacement in substitute";
CVC4_API_CHECK(e.getSort().isComparableTo(replacement.getSort()))
<< "Expecting terms of comparable sort in substitute";
- return api::Term(d_expr->substitute(e.getExpr(), replacement.getExpr()));
+ return Term(d_solver, d_expr->substitute(e.getExpr(), replacement.getExpr()));
}
Term Term::substitute(const std::vector<Term> es,
CVC4_API_CHECK(es[i].getSort().isComparableTo(replacements[i].getSort()))
<< "Expecting terms of comparable sort in substitute";
}
- return api::Term(d_expr->substitute(termVectorToExprs(es),
- termVectorToExprs(replacements)));
+ return Term(d_solver,
+ d_expr->substitute(termVectorToExprs(es),
+ termVectorToExprs(replacements)));
}
bool Term::hasOp() const
// is one of the APPLY_* kinds
if (isApplyKind(d_expr->getKind()))
{
- return Op(intToExtKind(d_expr->getKind()));
+ return Op(d_solver, intToExtKind(d_expr->getKind()));
}
else if (d_expr->isParameterized())
{
// it's an indexed operator
// so we should return the indexed op
CVC4::Expr op = d_expr->getOperator();
- return Op(intToExtKind(d_expr->getKind()), op);
+ return Op(d_solver, intToExtKind(d_expr->getKind()), op);
}
else
{
- return Op(intToExtKind(d_expr->getKind()));
+ return Op(d_solver, intToExtKind(d_expr->getKind()));
}
}
CVC4_API_CHECK_NOT_NULL;
try
{
- Term res = d_expr->notExpr();
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_expr->notExpr();
+ (void)res.getType(true); /* kick off type checking */
+ return Term(d_solver, res);
}
catch (const CVC4::TypeCheckingException& e)
{
CVC4_API_ARG_CHECK_NOT_NULL(t);
try
{
- Term res = d_expr->andExpr(*t.d_expr);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_expr->andExpr(*t.d_expr);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(d_solver, res);
}
catch (const CVC4::TypeCheckingException& e)
{
CVC4_API_ARG_CHECK_NOT_NULL(t);
try
{
- Term res = d_expr->orExpr(*t.d_expr);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_expr->orExpr(*t.d_expr);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(d_solver, res);
}
catch (const CVC4::TypeCheckingException& e)
{
CVC4_API_ARG_CHECK_NOT_NULL(t);
try
{
- Term res = d_expr->xorExpr(*t.d_expr);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_expr->xorExpr(*t.d_expr);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(d_solver, res);
}
catch (const CVC4::TypeCheckingException& e)
{
CVC4_API_ARG_CHECK_NOT_NULL(t);
try
{
- Term res = d_expr->eqExpr(*t.d_expr);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_expr->eqExpr(*t.d_expr);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(d_solver, res);
}
catch (const CVC4::TypeCheckingException& e)
{
CVC4_API_ARG_CHECK_NOT_NULL(t);
try
{
- Term res = d_expr->impExpr(*t.d_expr);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_expr->impExpr(*t.d_expr);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(d_solver, res);
}
catch (const CVC4::TypeCheckingException& e)
{
CVC4_API_ARG_CHECK_NOT_NULL(else_t);
try
{
- Term res = d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(d_solver, res);
}
catch (const CVC4::TypeCheckingException& e)
{
std::string Term::toString() const { return d_expr->toString(); }
-Term::const_iterator::const_iterator() : d_orig_expr(nullptr), d_pos(0) {}
+Term::const_iterator::const_iterator()
+ : d_solver(nullptr), d_orig_expr(nullptr), d_pos(0)
+{
+}
-Term::const_iterator::const_iterator(const std::shared_ptr<CVC4::Expr>& e,
+Term::const_iterator::const_iterator(const Solver* slv,
+ const std::shared_ptr<CVC4::Expr>& e,
uint32_t p)
- : d_orig_expr(e), d_pos(p)
+ : d_solver(slv), d_orig_expr(e), d_pos(p)
{
}
if (!d_pos && extra_child)
{
- return Term(d_orig_expr->getOperator());
+ return Term(d_solver, d_orig_expr->getOperator());
}
else
{
--idx;
}
Assert(idx >= 0);
- return Term((*d_orig_expr)[idx]);
+ return Term(d_solver, (*d_orig_expr)[idx]);
}
}
Term::const_iterator Term::begin() const
{
- return Term::const_iterator(d_expr, 0);
+ return Term::const_iterator(d_solver, d_expr, 0);
}
Term::const_iterator Term::end() const
// one more child if this is a UF application (count the UF as a child)
++endpos;
}
- return Term::const_iterator(d_expr, endpos);
+ return Term::const_iterator(d_solver, d_expr, endpos);
}
// !!! This is only temporarily available until the parser is fully migrated
/* DatatypeDecl ------------------------------------------------------------- */
-DatatypeDecl::DatatypeDecl(const Solver* s,
+DatatypeDecl::DatatypeDecl(const Solver* slv,
const std::string& name,
bool isCoDatatype)
- : d_dtype(new CVC4::Datatype(s->getExprManager(), name, isCoDatatype))
+ : d_dtype(new CVC4::Datatype(slv->getExprManager(), name, isCoDatatype))
{
}
-DatatypeDecl::DatatypeDecl(const Solver* s,
+DatatypeDecl::DatatypeDecl(const Solver* slv,
const std::string& name,
Sort param,
bool isCoDatatype)
- : d_dtype(new CVC4::Datatype(s->getExprManager(),
+ : d_dtype(new CVC4::Datatype(slv->getExprManager(),
name,
std::vector<Type>{*param.d_type},
isCoDatatype))
{
}
-DatatypeDecl::DatatypeDecl(const Solver* s,
+DatatypeDecl::DatatypeDecl(const Solver* slv,
const std::string& name,
const std::vector<Sort>& params,
bool isCoDatatype)
tparams.push_back(*p.d_type);
}
d_dtype = std::shared_ptr<CVC4::Datatype>(
- new CVC4::Datatype(s->getExprManager(), name, tparams, isCoDatatype));
+ new CVC4::Datatype(slv->getExprManager(), name, tparams, isCoDatatype));
}
bool DatatypeDecl::isNullHelper() const { return !d_dtype; }
DatatypeSelector::DatatypeSelector() { d_stor = nullptr; }
-DatatypeSelector::DatatypeSelector(const CVC4::DatatypeConstructorArg& stor)
- : d_stor(new CVC4::DatatypeConstructorArg(stor))
+DatatypeSelector::DatatypeSelector(const Solver* slv,
+ const CVC4::DatatypeConstructorArg& stor)
+ : d_solver(slv), d_stor(new CVC4::DatatypeConstructorArg(stor))
{
CVC4_API_CHECK(d_stor->isResolved()) << "Expected resolved datatype selector";
}
Term DatatypeSelector::getSelectorTerm() const
{
- Term sel = d_stor->getSelector();
+ Term sel = Term(d_solver, d_stor->getSelector());
return sel;
}
Sort DatatypeSelector::getRangeSort() const
{
- return Sort(d_stor->getRangeType());
+ return Sort(d_solver, d_stor->getRangeType());
}
std::string DatatypeSelector::toString() const
/* DatatypeConstructor ------------------------------------------------------ */
-DatatypeConstructor::DatatypeConstructor() { d_ctor = nullptr; }
+DatatypeConstructor::DatatypeConstructor() : d_solver(nullptr), d_ctor(nullptr)
+{
+}
-DatatypeConstructor::DatatypeConstructor(const CVC4::DatatypeConstructor& ctor)
- : d_ctor(new CVC4::DatatypeConstructor(ctor))
+DatatypeConstructor::DatatypeConstructor(const Solver* slv,
+ const CVC4::DatatypeConstructor& ctor)
+ : d_solver(slv), d_ctor(new CVC4::DatatypeConstructor(ctor))
{
CVC4_API_CHECK(d_ctor->isResolved())
<< "Expected resolved datatype constructor";
Term DatatypeConstructor::getConstructorTerm() const
{
- Term ctor = d_ctor->getConstructor();
+ Term ctor = Term(d_solver, d_ctor->getConstructor());
return ctor;
}
Term DatatypeConstructor::getTesterTerm() const
{
- Term tst = d_ctor->getTester();
+ Term tst = Term(d_solver, d_ctor->getTester());
return tst;
}
DatatypeSelector DatatypeConstructor::operator[](size_t index) const
{
- return (*d_ctor)[index];
+ return DatatypeSelector(d_solver, (*d_ctor)[index]);
}
DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const
DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
{
- return DatatypeConstructor::const_iterator(*d_ctor, true);
+ return DatatypeConstructor::const_iterator(d_solver, *d_ctor, true);
}
DatatypeConstructor::const_iterator DatatypeConstructor::end() const
{
- return DatatypeConstructor::const_iterator(*d_ctor, false);
+ return DatatypeConstructor::const_iterator(d_solver, *d_ctor, false);
}
DatatypeConstructor::const_iterator::const_iterator(
- const CVC4::DatatypeConstructor& ctor, bool begin)
+ const Solver* slv, const CVC4::DatatypeConstructor& ctor, bool begin)
{
+ d_solver = slv;
d_int_stors = ctor.getArgs();
+
const std::vector<CVC4::DatatypeConstructorArg>* sels =
static_cast<const std::vector<CVC4::DatatypeConstructorArg>*>(
d_int_stors);
for (const auto& s : *sels)
{
/* Can not use emplace_back here since constructor is private. */
- d_stors.push_back(DatatypeSelector(s));
+ d_stors.push_back(DatatypeSelector(d_solver, s));
}
d_idx = begin ? 0 : sels->size();
}
-// Nullary constructor for Cython
-DatatypeConstructor::const_iterator::const_iterator() {}
+DatatypeConstructor::const_iterator::const_iterator()
+ : d_solver(nullptr), d_int_stors(nullptr), d_idx(0)
+{
+}
DatatypeConstructor::const_iterator&
DatatypeConstructor::const_iterator::operator=(
const DatatypeConstructor::const_iterator& it)
{
+ d_solver = it.d_solver;
d_int_stors = it.d_int_stors;
d_stors = it.d_stors;
d_idx = it.d_idx;
}
CVC4_API_CHECK(foundSel) << "No selector " << name << " for constructor "
<< getName() << " exists";
- return (*d_ctor)[index];
+ return DatatypeSelector(d_solver, (*d_ctor)[index]);
}
std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor)
/* Datatype ----------------------------------------------------------------- */
-Datatype::Datatype(const CVC4::Datatype& dtype)
- : d_dtype(new CVC4::Datatype(dtype))
+Datatype::Datatype(const Solver* slv, const CVC4::Datatype& dtype)
+ : d_solver(slv), d_dtype(new CVC4::Datatype(dtype))
{
CVC4_API_CHECK(d_dtype->isResolved()) << "Expected resolved datatype";
}
-// Nullary constructor for Cython
-Datatype::Datatype() {}
+Datatype::Datatype() : d_solver(nullptr), d_dtype(nullptr) {}
Datatype::~Datatype() {}
DatatypeConstructor Datatype::operator[](size_t idx) const
{
CVC4_API_CHECK(idx < getNumConstructors()) << "Index out of bounds.";
- return (*d_dtype)[idx];
+ return DatatypeConstructor(d_solver, (*d_dtype)[idx]);
}
DatatypeConstructor Datatype::operator[](const std::string& name) const
Datatype::const_iterator Datatype::begin() const
{
- return Datatype::const_iterator(*d_dtype, true);
+ return Datatype::const_iterator(d_solver, *d_dtype, true);
}
Datatype::const_iterator Datatype::end() const
{
- return Datatype::const_iterator(*d_dtype, false);
+ return Datatype::const_iterator(d_solver, *d_dtype, false);
}
// !!! This is only temporarily available until the parser is fully migrated
}
CVC4_API_CHECK(foundCons) << "No constructor " << name << " for datatype "
<< getName() << " exists";
- return (*d_dtype)[index];
+ return DatatypeConstructor(d_solver, (*d_dtype)[index]);
}
-Datatype::const_iterator::const_iterator(const CVC4::Datatype& dtype,
+Datatype::const_iterator::const_iterator(const Solver* slv,
+ const CVC4::Datatype& dtype,
bool begin)
+ : d_solver(slv), d_int_ctors(dtype.getConstructors())
{
- d_int_ctors = dtype.getConstructors();
const std::vector<CVC4::DatatypeConstructor>* cons =
static_cast<const std::vector<CVC4::DatatypeConstructor>*>(d_int_ctors);
for (const auto& c : *cons)
{
/* Can not use emplace_back here since constructor is private. */
- d_ctors.push_back(DatatypeConstructor(c));
+ d_ctors.push_back(DatatypeConstructor(d_solver, c));
}
d_idx = begin ? 0 : cons->size();
}
-Datatype::const_iterator::const_iterator() {}
+Datatype::const_iterator::const_iterator()
+ : d_solver(nullptr), d_int_ctors(nullptr), d_idx(0)
+{
+}
Datatype::const_iterator& Datatype::const_iterator::operator=(
const Datatype::const_iterator& it)
{
+ d_solver = it.d_solver;
d_int_ctors = it.d_int_ctors;
d_ctors = it.d_ctors;
d_idx = it.d_idx;
/* -------------------------------------------------------------------------- */
/* Grammar */
/* -------------------------------------------------------------------------- */
-Grammar::Grammar(const Solver* s,
+Grammar::Grammar(const Solver* slv,
const std::vector<Term>& sygusVars,
const std::vector<Term>& ntSymbols)
- : d_s(s),
+ : d_solver(slv),
d_sygusVars(sygusVars),
d_ntSyms(ntSymbols),
d_ntsToTerms(ntSymbols.size()),
if (!d_sygusVars.empty())
{
- bvl = d_s->getExprManager()->mkExpr(CVC4::kind::BOUND_VAR_LIST,
- termVectorToExprs(d_sygusVars));
+ bvl = Term(d_solver,
+ d_solver->getExprManager()->mkExpr(
+ CVC4::kind::BOUND_VAR_LIST, termVectorToExprs(d_sygusVars)));
}
std::unordered_map<Term, Sort, TermHashFunction> ntsToUnres(d_ntSyms.size());
{
// make the unresolved type, used for referencing the final version of
// the ntsymbol's datatype
- ntsToUnres[ntsymbol] = d_s->getExprManager()->mkSort(ntsymbol.toString());
+ ntsToUnres[ntsymbol] =
+ Sort(d_solver, d_solver->getExprManager()->mkSort(ntsymbol.toString()));
}
std::vector<CVC4::Datatype> datatypes;
for (const Term& ntSym : d_ntSyms)
{
// make the datatype, which encodes terms generated by this non-terminal
- DatatypeDecl dtDecl(d_s, ntSym.toString());
+ DatatypeDecl dtDecl(d_solver, ntSym.toString());
for (const Term& consTerm : d_ntsToTerms[ntSym])
{
if (d_allowVars.find(ntSym) != d_allowVars.cend())
{
- addSygusConstructorVariables(dtDecl, ntSym.d_expr->getType());
+ addSygusConstructorVariables(dtDecl,
+ Sort(d_solver, ntSym.d_expr->getType()));
}
bool aci = d_allowConst.find(ntSym) != d_allowConst.end();
}
std::vector<DatatypeType> datatypeTypes =
- d_s->getExprManager()->mkMutualDatatypeTypes(
+ d_solver->getExprManager()->mkMutualDatatypeTypes(
datatypes, unresTypes, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
// return is the first datatype
- return datatypeTypes[0];
+ return Sort(d_solver, datatypeTypes[0]);
}
void Grammar::addSygusConstructorTerm(
*op.d_expr, termVectorToExprs(args));
if (!args.empty())
{
- Term lbvl = d_s->getExprManager()->mkExpr(CVC4::kind::BOUND_VAR_LIST,
- termVectorToExprs(args));
+ Term lbvl = Term(d_solver,
+ d_solver->getExprManager()->mkExpr(
+ CVC4::kind::BOUND_VAR_LIST, termVectorToExprs(args)));
// its operator is a lambda
- op = d_s->getExprManager()->mkExpr(CVC4::kind::LAMBDA,
- {*lbvl.d_expr, *op.d_expr});
+ op = Term(d_solver,
+ d_solver->getExprManager()->mkExpr(CVC4::kind::LAMBDA,
+ {*lbvl.d_expr, *op.d_expr}));
}
dt.d_dtype->addSygusConstructor(
*op.d_expr, ssCName.str(), sortVectorToTypes(cargs), spc);
ntsToUnres.find(term);
if (itn != ntsToUnres.cend())
{
- Term ret = d_s->getExprManager()->mkBoundVar(term.d_expr->getType());
+ Term ret =
+ Term(d_solver,
+ d_solver->getExprManager()->mkBoundVar(term.d_expr->getType()));
args.push_back(ret);
cargs.push_back(itn->second);
return ret;
bool childChanged = false;
for (unsigned i = 0, nchild = term.d_expr->getNumChildren(); i < nchild; i++)
{
- Term ptermc = purifySygusGTerm((*term.d_expr)[i], args, cargs, ntsToUnres);
+ Term ptermc = purifySygusGTerm(
+ Term(d_solver, (*term.d_expr)[i]), args, cargs, ntsToUnres);
pchildren.push_back(ptermc);
childChanged = childChanged || *ptermc.d_expr != (*term.d_expr)[i];
}
return term;
}
- Term nret;
+ Expr nret;
if (term.d_expr->isParameterized())
{
// it's an indexed operator so we should provide the op
- nret = d_s->getExprManager()->mkExpr(term.d_expr->getKind(),
- term.d_expr->getOperator(),
- termVectorToExprs(pchildren));
+ nret = d_solver->getExprManager()->mkExpr(term.d_expr->getKind(),
+ term.d_expr->getOperator(),
+ termVectorToExprs(pchildren));
}
else
{
- nret = d_s->getExprManager()->mkExpr(term.d_expr->getKind(),
- termVectorToExprs(pchildren));
+ nret = d_solver->getExprManager()->mkExpr(term.d_expr->getKind(),
+ termVectorToExprs(pchildren));
}
- return nret;
+ return Term(d_solver, nret);
}
void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, Sort sort) const
template <typename T>
Term Solver::mkValHelper(T t) const
{
- Term res = d_exprMgr->mkConst(t);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_exprMgr->mkConst(t);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
}
Term Solver::mkRealFromStrHelper(const std::string& s) const
kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind)
<< "PI or REGEXP_EMPTY or REGEXP_SIGMA";
- Term res;
+ Expr res;
if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
{
CVC4::Kind k = extToIntKind(kind);
Assert(kind == PI);
res = d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
}
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
Assert(isDefinedIntKind(k))
<< "Not a defined internal kind : " << k << " " << kind;
- Term res;
+ Expr res;
if (echildren.size() > 2)
{
if (kind == INTS_DIVISION || kind == XOR || kind == MINUS
res = d_exprMgr->mkExpr(k, echildren);
}
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
std::vector<Sort> retTypes;
for (CVC4::DatatypeType t : dtypes)
{
- retTypes.push_back(Sort(t));
+ retTypes.push_back(Sort(this, t));
}
return retTypes;
Sort Solver::getNullSort(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return Type();
+ return Sort(this, Type());
CVC4_API_SOLVER_TRY_CATCH_END;
}
Sort Solver::getBooleanSort(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->booleanType();
+ return Sort(this, d_exprMgr->booleanType());
CVC4_API_SOLVER_TRY_CATCH_END;
}
Sort Solver::getIntegerSort(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->integerType();
+ return Sort(this, d_exprMgr->integerType());
CVC4_API_SOLVER_TRY_CATCH_END;
}
Sort Solver::getRealSort(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->realType();
+ return Sort(this, d_exprMgr->realType());
CVC4_API_SOLVER_TRY_CATCH_END;
}
Sort Solver::getRegExpSort(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->regExpType();
+ return Sort(this, d_exprMgr->regExpType());
CVC4_API_SOLVER_TRY_CATCH_END;
}
Sort Solver::getStringSort(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->stringType();
+ return Sort(this, d_exprMgr->stringType());
CVC4_API_SOLVER_TRY_CATCH_END;
}
Sort Solver::getRoundingmodeSort(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->roundingModeType();
+ return Sort(this, d_exprMgr->roundingModeType());
CVC4_API_SOLVER_TRY_CATCH_END;
}
CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
<< "non-null element sort";
- return d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type);
+ return Sort(this,
+ d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type));
CVC4_API_SOLVER_TRY_CATCH_END;
}
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "size > 0";
- return d_exprMgr->mkBitVectorType(size);
+ return Sort(this, d_exprMgr->mkBitVectorType(size));
CVC4_API_SOLVER_TRY_CATCH_END;
}
CVC4_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "exponent size > 0";
CVC4_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "significand size > 0";
- return d_exprMgr->mkFloatingPointType(exp, sig);
+ return Sort(this, d_exprMgr->mkFloatingPointType(exp, sig));
CVC4_API_SOLVER_TRY_CATCH_END;
}
CVC4_API_ARG_CHECK_EXPECTED(dtypedecl.getNumConstructors() > 0, dtypedecl)
<< "a datatype declaration with at least one constructor";
- return d_exprMgr->mkDatatypeType(*dtypedecl.d_dtype);
+ return Sort(this, d_exprMgr->mkDatatypeType(*dtypedecl.d_dtype));
CVC4_API_SOLVER_TRY_CATCH_END;
}
<< "first-class sort as codomain sort for function sort";
Assert(!codomain.isFunction()); /* A function sort is not first-class. */
- return d_exprMgr->mkFunctionType(*domain.d_type, *codomain.d_type);
+ return Sort(this,
+ d_exprMgr->mkFunctionType(*domain.d_type, *codomain.d_type));
CVC4_API_SOLVER_TRY_CATCH_END;
}
Assert(!codomain.isFunction()); /* A function sort is not first-class. */
std::vector<Type> argTypes = sortVectorToTypes(sorts);
- return d_exprMgr->mkFunctionType(argTypes, *codomain.d_type);
+ return Sort(this, d_exprMgr->mkFunctionType(argTypes, *codomain.d_type));
CVC4_API_SOLVER_TRY_CATCH_END;
}
Sort Solver::mkParamSort(const std::string& symbol) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->mkSort(symbol, ExprManager::SORT_FLAG_PLACEHOLDER);
+ return Sort(this,
+ d_exprMgr->mkSort(symbol, ExprManager::SORT_FLAG_PLACEHOLDER));
CVC4_API_SOLVER_TRY_CATCH_END;
}
}
std::vector<Type> types = sortVectorToTypes(sorts);
- return d_exprMgr->mkPredicateType(types);
+ return Sort(this, d_exprMgr->mkPredicateType(types));
CVC4_API_SOLVER_TRY_CATCH_END;
}
f.emplace_back(p.first, *p.second.d_type);
}
- return d_exprMgr->mkRecordType(Record(f));
+ return Sort(this, d_exprMgr->mkRecordType(Record(f)));
CVC4_API_SOLVER_TRY_CATCH_END;
}
CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
<< "non-null element sort";
- return d_exprMgr->mkSetType(*elemSort.d_type);
+ return Sort(this, d_exprMgr->mkSetType(*elemSort.d_type));
CVC4_API_SOLVER_TRY_CATCH_END;
}
Sort Solver::mkUninterpretedSort(const std::string& symbol) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->mkSort(symbol);
+ return Sort(this, d_exprMgr->mkSort(symbol));
CVC4_API_SOLVER_TRY_CATCH_END;
}
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(arity > 0, arity) << "an arity > 0";
- return d_exprMgr->mkSortConstructor(symbol, arity);
+ return Sort(this, d_exprMgr->mkSortConstructor(symbol, arity));
CVC4_API_SOLVER_TRY_CATCH_END;
}
}
std::vector<Type> types = sortVectorToTypes(sorts);
- return d_exprMgr->mkTupleType(types);
+ return Sort(this, d_exprMgr->mkTupleType(types));
CVC4_API_SOLVER_TRY_CATCH_END;
}
Term Solver::mkTrue(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->mkConst<bool>(true);
+ return Term(this, d_exprMgr->mkConst<bool>(true));
CVC4_API_SOLVER_TRY_CATCH_END;
}
Term Solver::mkFalse(void) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->mkConst<bool>(false);
+ return Term(this, d_exprMgr->mkConst<bool>(false));
CVC4_API_SOLVER_TRY_CATCH_END;
}
Term Solver::mkBoolean(bool val) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- return d_exprMgr->mkConst<bool>(val);
+ return Term(this, d_exprMgr->mkConst<bool>(val));
CVC4_API_SOLVER_TRY_CATCH_END;
}
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- Term res =
+ Expr res =
d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- Term res =
+ Expr res =
d_exprMgr->mkExpr(CVC4::kind::REGEXP_EMPTY, std::vector<CVC4::Expr>());
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- Term res =
+ Expr res =
d_exprMgr->mkExpr(CVC4::kind::REGEXP_SIGMA, std::vector<CVC4::Expr>());
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
- Term res = d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
- Term res =
+ Expr res =
d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET);
// TODO(#2771): Reenable?
- // (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ // (void)res->getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
CVC4::Integer idx(index, 10);
CVC4_API_ARG_CHECK_EXPECTED(idx > 0, index)
<< "a string representing an integer > 0";
- return d_exprMgr->mkConst(CVC4::AbstractValue(idx));
+ return Term(this, d_exprMgr->mkConst(CVC4::AbstractValue(idx)));
// do not call getType(), for abstract values, type can not be computed
// until it is substituted away
CVC4_API_SOLVER_TRY_CATCH_END;
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(index > 0, index) << "an integer > 0";
- return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(index)));
+ return Term(this, d_exprMgr->mkConst(CVC4::AbstractValue(Integer(index))));
// do not call getType(), for abstract values, type can not be computed
// until it is substituted away
CVC4_API_SOLVER_TRY_CATCH_END;
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
- Term res = symbol.empty() ? d_exprMgr->mkVar(*sort.d_type)
+ Expr res = symbol.empty() ? d_exprMgr->mkVar(*sort.d_type)
: d_exprMgr->mkVar(symbol, *sort.d_type);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
- Term res = symbol.empty() ? d_exprMgr->mkBoundVar(*sort.d_type)
+ Expr res = symbol.empty() ? d_exprMgr->mkBoundVar(*sort.d_type)
: d_exprMgr->mkBoundVar(symbol, *sort.d_type);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
checkMkTerm(kind, 1);
- Term res = d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ Expr res = d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
checkMkTerm(kind, 2);
- Term res =
+ Expr res =
d_exprMgr->mkExpr(extToIntKind(kind), *child1.d_expr, *child2.d_expr);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
if (op.isIndexedHelper())
{
const CVC4::Kind int_kind = extToIntKind(op.d_kind);
- res = d_exprMgr->mkExpr(int_kind, *op.d_expr);
+ res = Term(this, d_exprMgr->mkExpr(int_kind, *op.d_expr));
}
else
{
CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
const CVC4::Kind int_kind = extToIntKind(op.d_kind);
- Term res;
+ Expr res;
if (op.isIndexedHelper())
{
res = d_exprMgr->mkExpr(int_kind, *op.d_expr, *child.d_expr);
res = d_exprMgr->mkExpr(int_kind, *child.d_expr);
}
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
const CVC4::Kind int_kind = extToIntKind(op.d_kind);
- Term res;
+ Expr res;
if (op.isIndexedHelper())
{
res =
res = d_exprMgr->mkExpr(int_kind, *child1.d_expr, *child2.d_expr);
}
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term";
const CVC4::Kind int_kind = extToIntKind(op.d_kind);
- Term res;
+ Expr res;
if (op.isIndexedHelper())
{
res = d_exprMgr->mkExpr(
int_kind, *child1.d_expr, *child2.d_expr, *child3.d_expr);
}
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
const CVC4::Kind int_kind = extToIntKind(op.d_kind);
std::vector<Expr> echildren = termVectorToExprs(children);
- Term res;
+ Expr res;
if (op.isIndexedHelper())
{
res = d_exprMgr->mkExpr(int_kind, *op.d_expr, echildren);
res = d_exprMgr->mkExpr(int_kind, echildren);
}
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
Sort s = mkTupleSort(sorts);
Datatype dt = s.getDatatype();
- Term res = d_exprMgr->mkExpr(extToIntKind(APPLY_CONSTRUCTOR),
+ Expr res = d_exprMgr->mkExpr(extToIntKind(APPLY_CONSTRUCTOR),
*dt[0].getConstructorTerm().d_expr,
args);
- (void)res.d_expr->getType(true); /* kick off type checking */
- return res;
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_CHECK(s_indexed_kinds.find(kind) == s_indexed_kinds.end())
<< "Expected a kind for a non-indexed operator.";
- return Op(kind);
+ return Op(this, kind);
CVC4_API_SOLVER_TRY_CATCH_END
}
if (kind == RECORD_UPDATE)
{
res = Op(
+ this,
kind,
*mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get());
}
* as invalid. */
CVC4_API_ARG_CHECK_EXPECTED(arg != ".", arg)
<< "a string representing an integer, real or rational value.";
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::Divisible>(CVC4::Divisible(CVC4::Integer(arg)))
.d_expr.get());
}
{
case DIVISIBLE:
res =
- Op(kind,
+ Op(this,
+ kind,
*mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get());
break;
case BITVECTOR_REPEAT:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
.d_expr.get());
break;
case BITVECTOR_ZERO_EXTEND:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::BitVectorZeroExtend>(
CVC4::BitVectorZeroExtend(arg))
.d_expr.get());
break;
case BITVECTOR_SIGN_EXTEND:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::BitVectorSignExtend>(
CVC4::BitVectorSignExtend(arg))
.d_expr.get());
break;
case BITVECTOR_ROTATE_LEFT:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::BitVectorRotateLeft>(
CVC4::BitVectorRotateLeft(arg))
.d_expr.get());
break;
case BITVECTOR_ROTATE_RIGHT:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::BitVectorRotateRight>(
CVC4::BitVectorRotateRight(arg))
.d_expr.get());
break;
case INT_TO_BITVECTOR:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
.d_expr.get());
break;
case FLOATINGPOINT_TO_UBV:
res = Op(
+ this,
kind,
*mkValHelper<CVC4::FloatingPointToUBV>(CVC4::FloatingPointToUBV(arg))
.d_expr.get());
break;
case FLOATINGPOINT_TO_SBV:
res = Op(
+ this,
kind,
*mkValHelper<CVC4::FloatingPointToSBV>(CVC4::FloatingPointToSBV(arg))
.d_expr.get());
break;
case TUPLE_UPDATE:
res = Op(
+ this,
kind,
*mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get());
break;
case REGEXP_REPEAT:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::RegExpRepeat>(CVC4::RegExpRepeat(arg))
.d_expr.get());
break;
switch (kind)
{
case BITVECTOR_EXTRACT:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::BitVectorExtract>(
CVC4::BitVectorExtract(arg1, arg2))
.d_expr.get());
break;
case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>(
CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2))
.d_expr.get());
break;
case FLOATINGPOINT_TO_FP_FLOATINGPOINT:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::FloatingPointToFPFloatingPoint>(
CVC4::FloatingPointToFPFloatingPoint(arg1, arg2))
.d_expr.get());
break;
case FLOATINGPOINT_TO_FP_REAL:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::FloatingPointToFPReal>(
CVC4::FloatingPointToFPReal(arg1, arg2))
.d_expr.get());
break;
case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::FloatingPointToFPSignedBitVector>(
CVC4::FloatingPointToFPSignedBitVector(arg1, arg2))
.d_expr.get());
break;
case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2))
.d_expr.get());
break;
case FLOATINGPOINT_TO_FP_GENERIC:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::FloatingPointToFPGeneric>(
CVC4::FloatingPointToFPGeneric(arg1, arg2))
.d_expr.get());
break;
case REGEXP_LOOP:
- res = Op(kind,
+ res = Op(this,
+ kind,
*mkValHelper<CVC4::RegExpLoop>(CVC4::RegExpLoop(arg1, arg2))
.d_expr.get());
break;
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_NOT_NULL(t);
- return d_smtEngine->simplify(*t.d_expr);
+ return Term(this, d_smtEngine->simplify(*t.d_expr));
CVC4_API_SOLVER_TRY_CATCH_END;
}
{
dtdecl.addConstructor(ctor);
}
- return d_exprMgr->mkDatatypeType(*dtdecl.d_dtype);
+ return Sort(this, d_exprMgr->mkDatatypeType(*dtdecl.d_dtype));
}
/**
std::vector<Type> types = sortVectorToTypes(sorts);
type = d_exprMgr->mkFunctionType(types, type);
}
- return d_exprMgr->mkVar(symbol, type);
+ return Term(this, d_exprMgr->mkVar(symbol, type));
}
/**
*/
Sort Solver::declareSort(const std::string& symbol, uint32_t arity) const
{
- if (arity == 0) return d_exprMgr->mkSort(symbol);
- return d_exprMgr->mkSortConstructor(symbol, arity);
+ if (arity == 0) return Sort(this, d_exprMgr->mkSort(symbol));
+ return Sort(this, d_exprMgr->mkSortConstructor(symbol, arity));
}
/**
Expr fun = d_exprMgr->mkVar(symbol, type);
std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
d_smtEngine->defineFunction(fun, ebound_vars, *term.d_expr);
- return fun;
+ return Term(this, fun);
}
Term Solver::defineFun(Term fun,
Expr fun = d_exprMgr->mkVar(symbol, type);
std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
d_smtEngine->defineFunctionRec(fun, ebound_vars, *term.d_expr);
- return fun;
+ return Term(this, fun);
}
Term Solver::defineFunRec(Term fun,
std::vector<Term> res;
for (const Expr& e : assertions)
{
- res.push_back(Term(e));
+ res.push_back(Term(this, e));
}
return res;
}
std::vector<std::pair<Term, Term>> res;
for (const auto& p : assignment)
{
- res.emplace_back(Term(p.first), Term(p.second));
+ res.emplace_back(Term(this, p.first), Term(this, p.second));
}
return res;
}
std::vector<Term> res;
for (const Expr& e : uassumptions)
{
- res.push_back(Term(e));
+ res.push_back(Term(this, e));
}
return res;
}
std::vector<Term> res;
for (const Expr& e : core)
{
- res.push_back(Term(e));
+ res.push_back(Term(this, e));
}
return res;
}
// CHECK:
// NodeManager::fromExprManager(d_exprMgr)
// == NodeManager::fromExprManager(expr.getExprManager())
- return d_smtEngine->getValue(*term.d_expr);
+ return Term(this, d_smtEngine->getValue(*term.d_expr));
}
/**
for (const Term& t : terms)
{
/* Can not use emplace_back here since constructor is private. */
- res.push_back(Term(d_smtEngine->getValue(*t.d_expr)));
+ res.push_back(Term(this, d_smtEngine->getValue(*t.d_expr)));
}
return res;
}
// constructors. We do this cast using division with 1. This has the
// advantage wrt using TO_REAL since (constant) division is always included
// in the theory.
- res = Term(d_exprMgr->mkExpr(extToIntKind(DIVISION),
+ res = Term(this,
+ d_exprMgr->mkExpr(extToIntKind(DIVISION),
*res.d_expr,
d_exprMgr->mkConst(CVC4::Rational(1))));
}
d_smtEngine->declareSygusVar(symbol, res, *sort.d_type);
- return res;
+ return Term(this, res);
CVC4_API_SOLVER_TRY_CATCH_END;
}
Term Solver::synthInv(const std::string& symbol,
const std::vector<Term>& boundVars) const
{
- return synthFunHelper(symbol, boundVars, d_exprMgr->booleanType(), true);
+ return synthFunHelper(
+ symbol, boundVars, Sort(this, d_exprMgr->booleanType()), true);
}
Term Solver::synthInv(const std::string& symbol,
const std::vector<Term>& boundVars,
Grammar& g) const
{
- return synthFunHelper(symbol, boundVars, d_exprMgr->booleanType(), true, &g);
+ return synthFunHelper(
+ symbol, boundVars, Sort(this, d_exprMgr->booleanType()), true, &g);
}
Term Solver::synthFunHelper(const std::string& symbol,
isInv,
termVectorToExprs(boundVars));
- return fun;
+ return Term(this, fun);
CVC4_API_SOLVER_TRY_CATCH_END;
}
CVC4_API_CHECK(it != map.cend()) << "Synth solution not found for given term";
- return it->second;
+ return Term(this, it->second);
}
std::vector<Term> Solver::getSynthSolutions(
CVC4_API_CHECK(it != map.cend())
<< "Synth solution not found for term at index " << i;
- synthSolution.push_back(it->second);
+ synthSolution.push_back(Term(this, it->second));
}
return synthSolution;
return types;
}
-std::vector<Term> exprVectorToTerms(const std::vector<Expr>& exprs)
+std::vector<Term> exprVectorToTerms(const Solver* slv,
+ const std::vector<Expr>& exprs)
{
std::vector<Term> terms;
for (size_t i = 0, esize = exprs.size(); i < esize; i++)
{
- terms.push_back(Term(exprs[i]));
+ terms.push_back(Term(slv, exprs[i]));
}
return terms;
}
-std::vector<Sort> typeVectorToSorts(const std::vector<Type>& types)
+std::vector<Sort> typeVectorToSorts(const Solver* slv,
+ const std::vector<Type>& types)
{
std::vector<Sort> sorts;
for (size_t i = 0, tsize = types.size(); i < tsize; i++)
{
- sorts.push_back(Sort(types[i]));
+ sorts.push_back(Sort(slv, types[i]));
}
return sorts;
}
projects / cvc5.git / commitdiff