size_t Sort::getConstructorArity() const
{
- CVC4_API_CHECK(isConstructor()) << "Not a function sort.";
+ CVC4_API_CHECK(isConstructor()) << "Not a function sort: " << (*this);
return ConstructorType(*d_type).getArity();
}
std::vector<Sort> Sort::getConstructorDomainSorts() const
{
- CVC4_API_CHECK(isConstructor()) << "Not a function sort.";
+ CVC4_API_CHECK(isConstructor()) << "Not a function sort: " << (*this);
std::vector<CVC4::Type> types = ConstructorType(*d_type).getArgTypes();
return typeVectorToSorts(d_solver, types);
}
Sort Sort::getConstructorCodomainSort() const
{
- CVC4_API_CHECK(isConstructor()) << "Not a function sort.";
+ CVC4_API_CHECK(isConstructor()) << "Not a function sort: " << (*this);
return Sort(d_solver, ConstructorType(*d_type).getRangeType());
}
size_t Sort::getFunctionArity() const
{
- CVC4_API_CHECK(isFunction()) << "Not a function sort.";
+ CVC4_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
return FunctionType(*d_type).getArity();
}
std::vector<Sort> Sort::getFunctionDomainSorts() const
{
- CVC4_API_CHECK(isFunction()) << "Not a function sort.";
+ CVC4_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
std::vector<CVC4::Type> types = FunctionType(*d_type).getArgTypes();
return typeVectorToSorts(d_solver, types);
}
Sort Sort::getFunctionCodomainSort() const
{
- CVC4_API_CHECK(isFunction()) << "Not a function sort.";
+ CVC4_API_CHECK(isFunction()) << "Not a function sort" << (*this);
return Sort(d_solver, FunctionType(*d_type).getRangeType());
}
Options* o = opts == nullptr ? new Options() : opts;
d_exprMgr.reset(new ExprManager(*o));
d_smtEngine.reset(new SmtEngine(d_exprMgr.get()));
+ d_smtEngine->setSolver(this);
d_rng.reset(new Random((*o)[options::seed]));
if (opts == nullptr) delete o;
}
bool global) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function";
- std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
- size_t size = bound_vars.size();
- CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bound_vars)
- << "'" << domain_sorts.size() << "'";
- for (size_t i = 0; i < size; ++i)
+
+ if (fun.getSort().isFunction())
{
- CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
- this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
- << "bound variable associated to this solver object";
- CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
- bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
- "bound variable",
- bound_vars[i],
- i)
- << "a bound variable";
- CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
- domain_sorts[i] == bound_vars[i].getSort(),
- "sort of parameter",
- bound_vars[i],
- i)
- << "'" << domain_sorts[i] << "'";
+ std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
+ size_t size = bound_vars.size();
+ CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bound_vars)
+ << "'" << domain_sorts.size() << "'";
+ for (size_t i = 0; i < size; ++i)
+ {
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
+ << "bound variable associated to this solver object";
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+ "bound variable",
+ bound_vars[i],
+ i)
+ << "a bound variable";
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ domain_sorts[i] == bound_vars[i].getSort(),
+ "sort of parameter",
+ bound_vars[i],
+ i)
+ << "'" << domain_sorts[i] << "'";
+ }
+ Sort codomain = fun.getSort().getFunctionCodomainSort();
+ CVC4_API_CHECK(codomain == term.getSort())
+ << "Invalid sort of function body '" << term << "', expected '"
+ << codomain << "'";
+ }
+ else
+ {
+ CVC4_API_ARG_CHECK_EXPECTED(bound_vars.size() == 0, fun)
+ << "function or nullary symbol";
}
- Sort codomain = fun.getSort().getFunctionCodomainSort();
+
CVC4_API_SOLVER_CHECK_TERM(term);
- CVC4_API_CHECK(codomain == term.getSort())
- << "Invalid sort of function body '" << term << "', expected '"
- << codomain << "'";
std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
d_smtEngine->defineFunction(*fun.d_expr, ebound_vars, *term.d_expr, global);
bool global) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+
+ CVC4_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified())
+ << "recursive function definitions require a logic with quantifiers";
+ CVC4_API_CHECK(
+ d_smtEngine->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF))
+ << "recursive function definitions require a logic with uninterpreted "
+ "functions";
+
CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)
<< "first-class sort as function codomain sort";
Assert(!sort.isFunction()); /* A function sort is not first-class. */
bool global) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function";
- std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
- size_t size = bound_vars.size();
- CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bound_vars)
- << "'" << domain_sorts.size() << "'";
- for (size_t i = 0; i < size; ++i)
+
+ CVC4_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified())
+ << "recursive function definitions require a logic with quantifiers";
+ CVC4_API_CHECK(
+ d_smtEngine->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF))
+ << "recursive function definitions require a logic with uninterpreted "
+ "functions";
+
+ if (fun.getSort().isFunction())
{
- CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
- this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
- << "bound variable associated to this solver object";
- CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
- bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
- "bound variable",
- bound_vars[i],
- i)
- << "a bound variable";
- CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
- domain_sorts[i] == bound_vars[i].getSort(),
- "sort of parameter",
- bound_vars[i],
- i)
- << "'" << domain_sorts[i] << "'";
+ std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
+ size_t size = bound_vars.size();
+ CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bound_vars)
+ << "'" << domain_sorts.size() << "'";
+ for (size_t i = 0; i < size; ++i)
+ {
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
+ << "bound variable associated to this solver object";
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+ "bound variable",
+ bound_vars[i],
+ i)
+ << "a bound variable";
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ domain_sorts[i] == bound_vars[i].getSort(),
+ "sort of parameter",
+ bound_vars[i],
+ i)
+ << "'" << domain_sorts[i] << "'";
+ }
+ Sort codomain = fun.getSort().getFunctionCodomainSort();
+ CVC4_API_CHECK(codomain == term.getSort())
+ << "Invalid sort of function body '" << term << "', expected '"
+ << codomain << "'";
}
+ else
+ {
+ CVC4_API_ARG_CHECK_EXPECTED(bound_vars.size() == 0, fun)
+ << "function or nullary symbol";
+ }
+
CVC4_API_SOLVER_CHECK_TERM(term);
- Sort codomain = fun.getSort().getFunctionCodomainSort();
- CVC4_API_CHECK(codomain == term.getSort())
- << "Invalid sort of function body '" << term << "', expected '"
- << codomain << "'";
std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
d_smtEngine->defineFunctionRec(
*fun.d_expr, ebound_vars, *term.d_expr, global);
bool global) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+
+ CVC4_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified())
+ << "recursive function definitions require a logic with quantifiers";
+ CVC4_API_CHECK(
+ d_smtEngine->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF))
+ << "recursive function definitions require a logic with uninterpreted "
+ "functions";
+
size_t funs_size = funs.size();
CVC4_API_ARG_SIZE_CHECK_EXPECTED(funs_size == bound_vars.size(), bound_vars)
<< "'" << funs_size << "'";
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
this == fun.d_solver, "function", fun, j)
<< "function associated to this solver object";
- CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function";
CVC4_API_SOLVER_CHECK_TERM(term);
- std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
- size_t size = bvars.size();
- CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bvars)
- << "'" << domain_sorts.size() << "'";
- for (size_t i = 0; i < size; ++i)
+ if (fun.getSort().isFunction())
{
- for (size_t k = 0, nbvars = bvars.size(); k < nbvars; ++k)
+ std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
+ size_t size = bvars.size();
+ CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bvars)
+ << "'" << domain_sorts.size() << "'";
+ for (size_t i = 0; i < size; ++i)
{
+ for (size_t k = 0, nbvars = bvars.size(); k < nbvars; ++k)
+ {
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ this == bvars[k].d_solver, "bound variable", bvars[k], k)
+ << "bound variable associated to this solver object";
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ bvars[k].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+ "bound variable",
+ bvars[k],
+ k)
+ << "a bound variable";
+ }
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
- this == bvars[k].d_solver, "bound variable", bvars[k], k)
- << "bound variable associated to this solver object";
- CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
- bvars[k].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
- "bound variable",
- bvars[k],
- k)
- << "a bound variable";
+ domain_sorts[i] == bvars[i].getSort(),
+ "sort of parameter",
+ bvars[i],
+ i)
+ << "'" << domain_sorts[i] << "' in parameter bound_vars[" << j
+ << "]";
}
+ Sort codomain = fun.getSort().getFunctionCodomainSort();
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
- domain_sorts[i] == bvars[i].getSort(),
- "sort of parameter",
- bvars[i],
- i)
- << "'" << domain_sorts[i] << "' in parameter bound_vars[" << j << "]";
+ codomain == term.getSort(), "sort of function body", term, j)
+ << "'" << codomain << "'";
+ }
+ else
+ {
+ CVC4_API_ARG_CHECK_EXPECTED(bvars.size() == 0, fun)
+ << "function or nullary symbol";
}
- Sort codomain = fun.getSort().getFunctionCodomainSort();
- CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
- codomain == term.getSort(), "sort of function body", term, j)
- << "'" << codomain << "'";
}
std::vector<Expr> efuns = termVectorToExprs(funs);
std::vector<std::vector<Expr>> ebound_vars;
PARSER_STATE->parseError("Type mismatch in definition");
}
}
- std::vector<std::vector<Expr>> eformals;
- for (unsigned i=0, fsize = formals.size(); i<fsize; i++)
- {
- eformals.push_back(api::termVectorToExprs(formals[i]));
- }
cmd->reset(
- new DefineFunctionRecCommand(api::termVectorToExprs(funcs),
- eformals,
- api::termVectorToExprs(formulas), true));
+ new DefineFunctionRecCommand(SOLVER, funcs, formals, formulas, true));
}
| toplevelDeclaration[cmd]
;
expr = PARSER_STATE->mkHoApply( expr, flattenVars );
}
cmd->reset(new DefineFunctionRecCommand(
- func.getExpr(), api::termVectorToExprs(bvs), expr.getExpr(), PARSER_STATE->getGlobalDeclarations()));
+ SOLVER, func, bvs, expr, PARSER_STATE->getGlobalDeclarations()));
}
| DEFINE_FUNS_REC_TOK
{ PARSER_STATE->checkThatLogicIsSet();}
"Number of functions defined does not match number listed in "
"define-funs-rec"));
}
- std::vector<std::vector<Expr>> eformals;
- for (unsigned i=0, fsize = formals.size(); i<fsize; i++)
- {
- eformals.push_back(api::termVectorToExprs(formals[i]));
- }
cmd->reset(
- new DefineFunctionRecCommand(api::termVectorToExprs(funcs),
- eformals,
- api::termVectorToExprs(func_defs), PARSER_STATE->getGlobalDeclarations()));
+ new DefineFunctionRecCommand(SOLVER,
+ funcs,
+ formals,
+ func_defs,
+ PARSER_STATE->getGlobalDeclarations()));
}
;
#include <typeinfo>
#include <vector>
+#include "api/cvc4cpp.h"
#include "expr/dtype.h"
#include "expr/node_manager_attributes.h"
#include "expr/node_visitor.h"
static void toStream(std::ostream& out, const DefineFunctionRecCommand* c)
{
- const vector<Expr>& funcs = c->getFunctions();
- const vector<vector<Expr> >& formals = c->getFormals();
+ const vector<api::Term>& funcs = c->getFunctions();
+ const vector<vector<api::Term> >& formals = c->getFormals();
out << "(define-fun";
if (funcs.size() > 1)
{
}
out << funcs[i] << " (";
// print its type signature
- vector<Expr>::const_iterator itf = formals[i].begin();
+ vector<api::Term>::const_iterator itf = formals[i].begin();
for (;;)
{
- out << "(" << (*itf) << " " << (*itf).getType() << ")";
+ out << "(" << (*itf) << " " << (*itf).getSort() << ")";
++itf;
if (itf != formals[i].end())
{
break;
}
}
- Type type = funcs[i].getType();
- type = static_cast<FunctionType>(type).getRangeType();
+ api::Sort type = funcs[i].getSort();
+ type = type.getFunctionCodomainSort();
out << ") " << type;
if (funcs.size() > 1)
{
{
out << ") (";
}
- const vector<Expr>& formulas = c->getFormulas();
+ const vector<api::Term>& formulas = c->getFormulas();
for (unsigned i = 0, size = formulas.size(); i < size; i++)
{
if (i > 0)
#include <utility>
#include <vector>
+#include "api/cvc4cpp.h"
#include "base/check.h"
#include "base/output.h"
#include "expr/expr_iomanip.h"
/* class Command */
/* -------------------------------------------------------------------------- */
-Command::Command() : d_commandStatus(NULL), d_muted(false) {}
+Command::Command() : d_commandStatus(nullptr), d_muted(false) {}
+
+Command::Command(api::Solver* solver)
+ : d_solver(solver), d_commandStatus(nullptr), d_muted(false)
+{
+}
+
Command::Command(const Command& cmd)
{
d_commandStatus =
/* -------------------------------------------------------------------------- */
DefineFunctionRecCommand::DefineFunctionRecCommand(
- Expr func, const std::vector<Expr>& formals, Expr formula, bool global)
- : d_global(global)
+ api::Solver* solver,
+ api::Term func,
+ const std::vector<api::Term>& formals,
+ api::Term formula,
+ bool global)
+ : Command(solver), d_global(global)
{
d_funcs.push_back(func);
d_formals.push_back(formals);
}
DefineFunctionRecCommand::DefineFunctionRecCommand(
- const std::vector<Expr>& funcs,
- const std::vector<std::vector<Expr>>& formals,
- const std::vector<Expr>& formulas,
+ api::Solver* solver,
+ const std::vector<api::Term>& funcs,
+ const std::vector<std::vector<api::Term>>& formals,
+ const std::vector<api::Term>& formulas,
bool global)
- : d_funcs(funcs), d_formals(formals), d_formulas(formulas), d_global(global)
+ : Command(solver),
+ d_funcs(funcs),
+ d_formals(formals),
+ d_formulas(formulas),
+ d_global(global)
{
}
-const std::vector<Expr>& DefineFunctionRecCommand::getFunctions() const
+const std::vector<api::Term>& DefineFunctionRecCommand::getFunctions() const
{
return d_funcs;
}
-const std::vector<std::vector<Expr>>& DefineFunctionRecCommand::getFormals()
- const
+const std::vector<std::vector<api::Term>>&
+DefineFunctionRecCommand::getFormals() const
{
return d_formals;
}
-const std::vector<Expr>& DefineFunctionRecCommand::getFormulas() const
+const std::vector<api::Term>& DefineFunctionRecCommand::getFormulas() const
{
return d_formulas;
}
{
try
{
- smtEngine->defineFunctionsRec(d_funcs, d_formals, d_formulas, d_global);
+ d_solver->defineFunsRec(d_funcs, d_formals, d_formulas, d_global);
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
Command* DefineFunctionRecCommand::exportTo(
ExprManager* exprManager, ExprManagerMapCollection& variableMap)
{
- std::vector<Expr> funcs;
- for (unsigned i = 0, size = d_funcs.size(); i < size; i++)
- {
- Expr func = d_funcs[i].exportTo(
- exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED);
- funcs.push_back(func);
- }
- std::vector<std::vector<Expr>> formals;
- for (unsigned i = 0, size = d_formals.size(); i < size; i++)
- {
- std::vector<Expr> formals_c;
- transform(d_formals[i].begin(),
- d_formals[i].end(),
- back_inserter(formals_c),
- ExportTransformer(exprManager, variableMap));
- formals.push_back(formals_c);
- }
- std::vector<Expr> formulas;
- for (unsigned i = 0, size = d_formulas.size(); i < size; i++)
- {
- Expr formula = d_formulas[i].exportTo(exprManager, variableMap);
- formulas.push_back(formula);
- }
- return new DefineFunctionRecCommand(funcs, formals, formulas, d_global);
+ Unimplemented();
}
Command* DefineFunctionRecCommand::clone() const
{
- return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas, d_global);
+ return new DefineFunctionRecCommand(
+ d_solver, d_funcs, d_formals, d_formulas, d_global);
}
std::string DefineFunctionRecCommand::getCommandName() const
namespace CVC4 {
+namespace api {
+class Solver;
+class Term;
+} // namespace api
+
class SmtEngine;
class Command;
class CommandStatus;
class CVC4_PUBLIC Command
{
- protected:
- /**
- * This field contains a command status if the command has been
- * invoked, or NULL if it has not. This field is either a
- * dynamically-allocated pointer, or it's a pointer to the singleton
- * CommandSuccess instance. Doing so is somewhat asymmetric, but
- * it avoids the need to dynamically allocate memory in the common
- * case of a successful command.
- */
- const CommandStatus* d_commandStatus;
-
- /**
- * True if this command is "muted"---i.e., don't print "success" on
- * successful execution.
- */
- bool d_muted;
-
public:
typedef CommandPrintSuccess printsuccess;
Command();
+ Command(api::Solver* solver);
Command(const Command& cmd);
virtual ~Command();
Expr operator()(Expr e) { return e.exportTo(d_exprManager, d_variableMap); }
Type operator()(Type t) { return t.exportTo(d_exprManager, d_variableMap); }
}; /* class Command::ExportTransformer */
+
+ /** The solver instance that this command is associated with. */
+ api::Solver* d_solver;
+
+ /**
+ * This field contains a command status if the command has been
+ * invoked, or NULL if it has not. This field is either a
+ * dynamically-allocated pointer, or it's a pointer to the singleton
+ * CommandSuccess instance. Doing so is somewhat asymmetric, but
+ * it avoids the need to dynamically allocate memory in the common
+ * case of a successful command.
+ */
+ const CommandStatus* d_commandStatus;
+
+ /**
+ * True if this command is "muted"---i.e., don't print "success" on
+ * successful execution.
+ */
+ bool d_muted;
}; /* class Command */
/**
class CVC4_PUBLIC DefineFunctionRecCommand : public Command
{
public:
- DefineFunctionRecCommand(Expr func,
- const std::vector<Expr>& formals,
- Expr formula,
+ DefineFunctionRecCommand(api::Solver* solver,
+ api::Term func,
+ const std::vector<api::Term>& formals,
+ api::Term formula,
bool global);
- DefineFunctionRecCommand(const std::vector<Expr>& funcs,
- const std::vector<std::vector<Expr> >& formals,
- const std::vector<Expr>& formula,
+ DefineFunctionRecCommand(api::Solver* solver,
+ const std::vector<api::Term>& funcs,
+ const std::vector<std::vector<api::Term> >& formals,
+ const std::vector<api::Term>& formula,
bool global);
- const std::vector<Expr>& getFunctions() const;
- const std::vector<std::vector<Expr> >& getFormals() const;
- const std::vector<Expr>& getFormulas() const;
+ const std::vector<api::Term>& getFunctions() const;
+ const std::vector<std::vector<api::Term> >& getFormals() const;
+ const std::vector<api::Term>& getFormulas() const;
void invoke(SmtEngine* smtEngine) override;
Command* exportTo(ExprManager* exprManager,
protected:
/** functions we are defining */
- std::vector<Expr> d_funcs;
+ std::vector<api::Term> d_funcs;
/** formal arguments for each of the functions we are defining */
- std::vector<std::vector<Expr> > d_formals;
+ std::vector<std::vector<api::Term> > d_formals;
/** formulas corresponding to the bodies of the functions we are defining */
- std::vector<Expr> d_formulas;
+ std::vector<api::Term> d_formulas;
/**
* Stores whether this definition is global (i.e. should persist when
* popping the user context.
#include <utility>
#include <vector>
+#include "api/cvc4cpp.h"
#include "base/check.h"
#include "base/configuration.h"
#include "base/configuration_private.h"
"finished initializing.");
}
d_logic = logic;
+ d_userLogic = logic;
setLogicInternal();
}
LogicInfo SmtEngine::getLogicInfo() const {
return d_logic;
}
+LogicInfo SmtEngine::getUserLogicInfo() const
+{
+ // Lock the logic to make sure that this logic can be queried. We create a
+ // copy of the user logic here to keep this method const.
+ LogicInfo res = d_userLogic;
+ res.lock();
+ return res;
+}
void SmtEngine::setFilename(std::string filename) { d_filename = filename; }
std::string SmtEngine::getFilename() const { return d_filename; }
void SmtEngine::setLogicInternal()
<< "setting logic in SmtEngine but the engine has already"
" finished initializing for this run";
d_logic.lock();
+ d_userLogic.lock();
}
void SmtEngine::setProblemExtended()
if (Dump.isOn("raw-benchmark"))
{
+ std::vector<api::Term> tFuncs = api::exprVectorToTerms(d_solver, funcs);
+ std::vector<std::vector<api::Term>> tFormals;
+ for (const std::vector<Expr>& formal : formals)
+ {
+ tFormals.emplace_back(api::exprVectorToTerms(d_solver, formal));
+ }
+ std::vector<api::Term> tFormulas =
+ api::exprVectorToTerms(d_solver, formulas);
Dump("raw-benchmark") << DefineFunctionRecCommand(
- funcs, formals, formulas, global);
+ d_solver, tFuncs, tFormals, tFormulas, global);
}
ExprManager* em = getExprManager();
/* -------------------------------------------------------------------------- */
+namespace api {
+class Solver;
+} // namespace api
+
+/* -------------------------------------------------------------------------- */
+
namespace context {
class Context;
class UserContext;
class CVC4_PUBLIC SmtEngine
{
+ friend class ::CVC4::api::Solver;
// TODO (Issue #1096): Remove this friend relationship.
friend class ::CVC4::preprocessing::PreprocessingPassContext;
friend class ::CVC4::smt::SmtEnginePrivate;
/** Get the logic information currently set. */
LogicInfo getLogicInfo() const;
+ /** Get the logic information set by the user. */
+ LogicInfo getUserLogicInfo() const;
+
/**
* Set information about the script executing.
* @throw OptionException, ModalException
SmtEngine(const SmtEngine&) = delete;
SmtEngine& operator=(const SmtEngine&) = delete;
+ /** Set solver instance that owns this SmtEngine. */
+ void setSolver(api::Solver* solver) { d_solver = solver; }
+
/** Get a pointer to the TheoryEngine owned by this SmtEngine. */
TheoryEngine* getTheoryEngine() { return d_theoryEngine.get(); }
/* Members -------------------------------------------------------------- */
+ /** Solver instance that owns this SmtEngine instance. */
+ api::Solver* d_solver = nullptr;
+
/** Expr manager context */
std::unique_ptr<context::Context> d_context;
/** User level context */
std::vector<Command*> d_defineCommands;
/**
- * The logic we're in.
+ * The logic we're in. This logic may be an extension of the logic set by the
+ * user.
*/
LogicInfo d_logic;
+ /** The logic set by the user. */
+ LogicInfo d_userLogic;
+
/**
* Keep a copy of the original option settings (for reset()).
*/
regress0/simplification_bug2.smtv1.smt2
regress0/smallcnf.cvc
regress0/smt2output.smt2
+ regress0/smtlib/define-fun-rec-logic.smt2
regress0/smtlib/get-unsat-assumptions.smt2
regress0/smtlib/global-decls.smt2
regress0/smtlib/issue4028.smt2
--- /dev/null
+; EXPECT: unsat
+; EXPECT: (error "recursive function definitions require a logic with quantifiers")
+; EXIT: 1
+(set-logic UFBV)
+(define-funs-rec ((f ((b Bool)) Bool) (g ((b Bool)) Bool)) (b b))
+(assert (g false))
+(check-sat)
+(reset)
+(set-logic QF_BV)
+(define-funs-rec ((f ((b Bool)) Bool) (g ((b Bool)) Bool)) (b b))
+(assert (g false))
+(check-sat)
void testDefineFun();
void testDefineFunGlobal();
void testDefineFunRec();
+ void testDefineFunRecWrongLogic();
void testDefineFunRecGlobal();
void testDefineFunsRec();
+ void testDefineFunsRecWrongLogic();
void testDefineFunsRecGlobal();
void testUFIteration();
CVC4ApiException&);
}
+void SolverBlack::testDefineFunRecWrongLogic()
+{
+ d_solver->setLogic("QF_BV");
+ Sort bvSort = d_solver->mkBitVectorSort(32);
+ Sort funSort = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
+ Term b = d_solver->mkVar(bvSort, "b");
+ Term v = d_solver->mkConst(bvSort, "v");
+ Term f = d_solver->mkConst(funSort, "f");
+ TS_ASSERT_THROWS(d_solver->defineFunRec("f", {}, bvSort, v),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(d_solver->defineFunRec(f, {b, b}, v), CVC4ApiException&);
+}
+
void SolverBlack::testDefineFunRecGlobal()
{
Sort bSort = d_solver->getBooleanSort();
CVC4ApiException&);
}
+void SolverBlack::testDefineFunsRecWrongLogic()
+{
+ d_solver->setLogic("QF_BV");
+ Sort uSort = d_solver->mkUninterpretedSort("u");
+ Sort bvSort = d_solver->mkBitVectorSort(32);
+ Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
+ Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort());
+ Term b = d_solver->mkVar(bvSort, "b");
+ Term u = d_solver->mkVar(uSort, "u");
+ Term v1 = d_solver->mkConst(bvSort, "v1");
+ Term v2 = d_solver->mkConst(d_solver->getIntegerSort(), "v2");
+ Term f1 = d_solver->mkConst(funSort1, "f1");
+ Term f2 = d_solver->mkConst(funSort2, "f2");
+ TS_ASSERT_THROWS(d_solver->defineFunsRec({f1, f2}, {{b, b}, {u}}, {v1, v2}),
+ CVC4ApiException&);
+}
+
void SolverBlack::testDefineFunsRecGlobal()
{
Sort bSort = d_solver->getBooleanSort();
projects / cvc5.git / commitdiff