SExpr sexpr;
Type t;
Expr func;
- Expr func_app;
std::vector<Expr> bvs;
std::vector< std::vector<std::pair<std::string, Type> > > sortedVarNamesList;
std::vector<std::vector<Expr>> flattenVarsList;
+ std::vector<std::vector<Expr>> formals;
std::vector<Expr> funcs;
std::vector<Expr> func_defs;
Expr aexpr;
PARSER_STATE->resetAssertions();
}
| DEFINE_FUN_REC_TOK
- { PARSER_STATE->checkThatLogicIsSet();
- seq.reset(new CVC4::CommandSequence());
- }
+ { PARSER_STATE->checkThatLogicIsSet(); }
symbol[fname,CHECK_NONE,SYM_VARIABLE]
{ PARSER_STATE->checkUserSymbol(fname); }
LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
sortSymbol[t,CHECK_DECLARED]
{
func = PARSER_STATE->mkDefineFunRec(fname, sortedVarNames, t, flattenVars);
- seq->addCommand(new DeclareFunctionCommand(fname, func, t));
- PARSER_STATE->pushDefineFunRecScope(sortedVarNames, func, flattenVars, func_app, bvs, true );
+ PARSER_STATE->pushDefineFunRecScope(sortedVarNames, func, flattenVars, bvs, true );
}
term[expr, expr2]
{ PARSER_STATE->popScope();
if( !flattenVars.empty() ){
expr = PARSER_STATE->mkHoApply( expr, flattenVars );
}
- Expr as = MK_EXPR( kind::EQUAL, func_app, expr);
- if( !bvs.empty() ){
- std::string attr_name("fun-def");
- aexpr = MK_EXPR(kind::INST_ATTRIBUTE, func_app);
- aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr);
- //set the attribute to denote this is a function definition
- seq->addCommand( new SetUserAttributeCommand( attr_name, func_app ) );
- //assert it
- Expr boundVars = EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs);
- as = EXPR_MANAGER->mkExpr(kind::FORALL, boundVars, as, aexpr);
- }
- seq->addCommand( new AssertCommand(as, false) );
- cmd->reset(seq.release());
+ cmd->reset(new DefineFunctionRecCommand(func,bvs,expr));
}
| DEFINE_FUNS_REC_TOK
- { PARSER_STATE->checkThatLogicIsSet();
- seq.reset(new CVC4::CommandSequence());
- }
+ { PARSER_STATE->checkThatLogicIsSet();}
LPAREN_TOK
( LPAREN_TOK
symbol[fname,CHECK_UNDECLARED,SYM_VARIABLE]
{
flattenVars.clear();
func = PARSER_STATE->mkDefineFunRec( fname, sortedVarNames, t, flattenVars );
- seq->addCommand(new DeclareFunctionCommand(fname, func, t));
funcs.push_back( func );
// add to lists (need to remember for when parsing the bodies)
}
bvs.clear();
PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[0], funcs[0],
- flattenVarsList[0], func_app, bvs, true);
+ flattenVarsList[0], bvs, true);
}
(
term[expr,expr2]
expr = PARSER_STATE->mkHoApply( expr, flattenVarsList[j] );
}
func_defs.push_back( expr );
+ formals.push_back(bvs);
j++;
- Expr as = MK_EXPR( kind::EQUAL, func_app, expr );
- if( !bvs.empty() ){
- std::string attr_name("fun-def");
- aexpr = MK_EXPR(kind::INST_ATTRIBUTE, func_app);
- aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr );
- //set the attribute to denote these are function definitions
- seq->addCommand( new SetUserAttributeCommand( attr_name, func_app ) );
- //assert it
- as = EXPR_MANAGER->mkExpr( kind::FORALL,
- EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs),
- as, aexpr);
- }
- seq->addCommand( new AssertCommand(as, false) );
//set up the next scope
PARSER_STATE->popScope();
if( func_defs.size()<funcs.size() ){
bvs.clear();
PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[j], funcs[j],
- flattenVarsList[j], func_app, bvs, true);
+ flattenVarsList[j], bvs, true);
}
}
)+
"Number of functions defined does not match number listed in "
"define-funs-rec"));
}
- cmd->reset(seq.release());
+ cmd->reset( new DefineFunctionRecCommand(funcs,formals,func_defs));
}
// CHECK_SAT_ASSUMING still being discussed
// GET_UNSAT_ASSUMPTIONS
const std::vector<std::pair<std::string, Type> >& sortedVarNames,
Expr func,
const std::vector<Expr>& flattenVars,
- Expr& func_app,
std::vector<Expr>& bvs,
bool bindingLevel)
{
}
bvs.insert(bvs.end(), flattenVars.begin(), flattenVars.end());
-
- // make the function application
- if (bvs.empty())
- {
- // it has no arguments
- func_app = func;
- }
- else
- {
- func_app = getExprManager()->mkExpr(kind::APPLY_UF, f_app);
- }
}
void Smt2::reset() {
* (1) Calls Parser::pushScope(bindingLevel).
* (2) Computes the bound variable list for the quantified formula
* that defined this definition and stores it in bvs.
- * (3) Sets func_app to the APPLY_UF with func applied to bvs.
*/
void pushDefineFunRecScope(
const std::vector<std::pair<std::string, Type> >& sortedVarNames,
Expr func,
const std::vector<Expr>& flattenVars,
- Expr& func_app,
std::vector<Expr>& bvs,
bool bindingLevel = false);
expr::ExprPrintTypes::Scope ptScope(out, types);
expr::ExprDag::Scope dagScope(out, dag);
- if(tryToStream<AssertCommand>(out, c) ||
- tryToStream<PushCommand>(out, c) ||
- tryToStream<PopCommand>(out, c) ||
- tryToStream<CheckSatCommand>(out, c) ||
- tryToStream<QueryCommand>(out, c) ||
- tryToStream<ResetCommand>(out, c) ||
- tryToStream<ResetAssertionsCommand>(out, c) ||
- tryToStream<QuitCommand>(out, c) ||
- tryToStream<DeclarationSequence>(out, c) ||
- tryToStream<CommandSequence>(out, c) ||
- tryToStream<DeclareFunctionCommand>(out, c) ||
- tryToStream<DeclareTypeCommand>(out, c) ||
- tryToStream<DefineTypeCommand>(out, c) ||
- tryToStream<DefineNamedFunctionCommand>(out, c) ||
- tryToStream<DefineFunctionCommand>(out, c) ||
- tryToStream<SimplifyCommand>(out, c) ||
- tryToStream<GetValueCommand>(out, c) ||
- tryToStream<GetModelCommand>(out, c) ||
- tryToStream<GetAssignmentCommand>(out, c) ||
- tryToStream<GetAssertionsCommand>(out, c) ||
- tryToStream<GetProofCommand>(out, c) ||
- tryToStream<GetUnsatCoreCommand>(out, c) ||
- tryToStream<SetBenchmarkStatusCommand>(out, c, d_variant) ||
- tryToStream<SetBenchmarkLogicCommand>(out, c, d_variant) ||
- tryToStream<SetInfoCommand>(out, c, d_variant) ||
- tryToStream<GetInfoCommand>(out, c) ||
- tryToStream<SetOptionCommand>(out, c) ||
- tryToStream<GetOptionCommand>(out, c) ||
- tryToStream<DatatypeDeclarationCommand>(out, c, d_variant) ||
- tryToStream<CommentCommand>(out, c, d_variant) ||
- tryToStream<EmptyCommand>(out, c) ||
- tryToStream<EchoCommand>(out, c, d_variant)) {
+ if (tryToStream<AssertCommand>(out, c) || tryToStream<PushCommand>(out, c)
+ || tryToStream<PopCommand>(out, c)
+ || tryToStream<CheckSatCommand>(out, c)
+ || tryToStream<QueryCommand>(out, c)
+ || tryToStream<ResetCommand>(out, c)
+ || tryToStream<ResetAssertionsCommand>(out, c)
+ || tryToStream<QuitCommand>(out, c)
+ || tryToStream<DeclarationSequence>(out, c)
+ || tryToStream<CommandSequence>(out, c)
+ || tryToStream<DeclareFunctionCommand>(out, c)
+ || tryToStream<DeclareTypeCommand>(out, c)
+ || tryToStream<DefineTypeCommand>(out, c)
+ || tryToStream<DefineNamedFunctionCommand>(out, c)
+ || tryToStream<DefineFunctionCommand>(out, c)
+ || tryToStream<DefineFunctionRecCommand>(out, c)
+ || tryToStream<SimplifyCommand>(out, c)
+ || tryToStream<GetValueCommand>(out, c)
+ || tryToStream<GetModelCommand>(out, c)
+ || tryToStream<GetAssignmentCommand>(out, c)
+ || tryToStream<GetAssertionsCommand>(out, c)
+ || tryToStream<GetProofCommand>(out, c)
+ || tryToStream<GetUnsatCoreCommand>(out, c)
+ || tryToStream<SetBenchmarkStatusCommand>(out, c, d_variant)
+ || tryToStream<SetBenchmarkLogicCommand>(out, c, d_variant)
+ || tryToStream<SetInfoCommand>(out, c, d_variant)
+ || tryToStream<GetInfoCommand>(out, c)
+ || tryToStream<SetOptionCommand>(out, c)
+ || tryToStream<GetOptionCommand>(out, c)
+ || tryToStream<DatatypeDeclarationCommand>(out, c, d_variant)
+ || tryToStream<CommentCommand>(out, c, d_variant)
+ || tryToStream<EmptyCommand>(out, c)
+ || tryToStream<EchoCommand>(out, c, d_variant))
+ {
return;
}
out << ") " << type << " " << formula << ")";
}
+static void toStream(std::ostream& out, const DefineFunctionRecCommand* c)
+{
+ const vector<Expr>& funcs = c->getFunctions();
+ const vector<vector<Expr> >& formals = c->getFormals();
+ out << "(define-fun";
+ if (funcs.size() > 1)
+ {
+ out << "s";
+ }
+ out << "-rec ";
+ if (funcs.size() > 1)
+ {
+ out << "(";
+ }
+ for (unsigned i = 0, size = funcs.size(); i < size; i++)
+ {
+ if (funcs.size() > 1)
+ {
+ if (i > 0)
+ {
+ out << " ";
+ }
+ out << "(";
+ }
+ out << funcs[i] << " (";
+ // print its type signature
+ vector<Expr>::const_iterator itf = formals[i].begin();
+ for (;;)
+ {
+ out << "(" << (*itf) << " " << (*itf).getType() << ")";
+ ++itf;
+ if (itf != formals[i].end())
+ {
+ out << " ";
+ }
+ else
+ {
+ break;
+ }
+ }
+ Type type = funcs[i].getType();
+ type = static_cast<FunctionType>(type).getRangeType();
+ out << ") " << type;
+ if (funcs.size() > 1)
+ {
+ out << ")";
+ }
+ }
+ if (funcs.size() > 1)
+ {
+ out << ") (";
+ }
+ const vector<Expr>& formulas = c->getFormulas();
+ for (unsigned i = 0, size = formulas.size(); i < size; i++)
+ {
+ if (i > 0)
+ {
+ out << " ";
+ }
+ out << formulas[i];
+ }
+ if (funcs.size() > 1)
+ {
+ out << ")";
+ }
+ out << ")";
+}
+
static void toStreamRational(std::ostream& out, const Rational& r, bool decimal)
{
bool neg = r.sgn() < 0;
return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula);
}
+/* class DefineFunctionRecCommand */
+
+DefineFunctionRecCommand::DefineFunctionRecCommand(
+ Expr func, const std::vector<Expr>& formals, Expr formula) throw()
+{
+ d_funcs.push_back(func);
+ d_formals.push_back(formals);
+ d_formulas.push_back(formula);
+}
+
+DefineFunctionRecCommand::DefineFunctionRecCommand(
+ const std::vector<Expr>& funcs,
+ const std::vector<std::vector<Expr> >& formals,
+ const std::vector<Expr>& formulas) throw()
+{
+ d_funcs.insert(d_funcs.end(), funcs.begin(), funcs.end());
+ d_formals.insert(d_formals.end(), formals.begin(), formals.end());
+ d_formulas.insert(d_formulas.end(), formulas.begin(), formulas.end());
+}
+
+const std::vector<Expr>& DefineFunctionRecCommand::getFunctions() const throw()
+{
+ return d_funcs;
+}
+
+const std::vector<std::vector<Expr> >& DefineFunctionRecCommand::getFormals()
+ const throw()
+{
+ return d_formals;
+}
+
+const std::vector<Expr>& DefineFunctionRecCommand::getFormulas() const throw()
+{
+ return d_formulas;
+}
+
+void DefineFunctionRecCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
+ smtEngine->defineFunctionsRec(d_funcs, d_formals, d_formulas);
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+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);
+}
+
+Command* DefineFunctionRecCommand::clone() const
+{
+ return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas);
+}
+
+std::string DefineFunctionRecCommand::getCommandName() const throw()
+{
+ return "define-fun-rec";
+}
+
/* class SetUserAttribute */
SetUserAttributeCommand::SetUserAttributeCommand(
Command* clone() const;
};/* class DefineNamedFunctionCommand */
+/**
+ * The command when parsing define-fun-rec or define-funs-rec.
+ * This command will assert a set of quantified formulas that specify
+ * the (mutually recursive) function definitions provided to it.
+ */
+class CVC4_PUBLIC DefineFunctionRecCommand : public Command
+{
+ public:
+ DefineFunctionRecCommand(Expr func,
+ const std::vector<Expr>& formals,
+ Expr formula) throw();
+ DefineFunctionRecCommand(const std::vector<Expr>& funcs,
+ const std::vector<std::vector<Expr> >& formals,
+ const std::vector<Expr>& formula) throw();
+ ~DefineFunctionRecCommand() throw() {}
+ const std::vector<Expr>& getFunctions() const throw();
+ const std::vector<std::vector<Expr> >& getFormals() const throw();
+ const std::vector<Expr>& getFormulas() const throw();
+ void invoke(SmtEngine* smtEngine) override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const throw() override;
+
+ protected:
+ /** functions we are defining */
+ std::vector<Expr> d_funcs;
+ /** formal arguments for each of the functions we are defining */
+ std::vector<std::vector<Expr> > d_formals;
+ /** formulas corresponding to the bodies of the functions we are defining */
+ std::vector<Expr> d_formulas;
+}; /* class DefineFunctionRecCommand */
+
/**
* The command when an attribute is set by a user. In SMT-LIBv2 this is done
* via the syntax (! expr :attr)
}
}
-void SmtEngine::defineFunction(Expr func,
- const std::vector<Expr>& formals,
- Expr formula) {
- SmtScope smts(this);
- doPendingPops();
- Trace("smt") << "SMT defineFunction(" << func << ")" << endl;
+void SmtEngine::debugCheckFormals(const std::vector<Expr>& formals, Expr func)
+{
for(std::vector<Expr>::const_iterator i = formals.begin(); i != formals.end(); ++i) {
if((*i).getKind() != kind::BOUND_VARIABLE) {
stringstream ss;
throw TypeCheckingException(func, ss.str());
}
}
+}
- stringstream ss;
- ss << language::SetLanguage(language::SetLanguage::getLanguage(Dump.getStream()))
- << func;
- DefineFunctionCommand c(ss.str(), func, formals, formula);
- addToModelCommandAndDump(c, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
-
-
- PROOF( if (options::checkUnsatCores()) {
- d_defineCommands.push_back(c.clone());
- });
-
-
- // Substitute out any abstract values in formula
- Expr form = d_private->substituteAbstractValues(Node::fromExpr(formula)).toExpr();
-
- // type check body
- Type formulaType = form.getType(options::typeChecking());
-
+void SmtEngine::debugCheckFunctionBody(Expr formula,
+ const std::vector<Expr>& formals,
+ Expr func)
+{
+ Type formulaType = formula.getType(options::typeChecking());
Type funcType = func.getType();
// We distinguish here between definitions of constants and functions,
// because the type checking for them is subtly different. Perhaps we
throw TypeCheckingException(func, ss.str());
}
}
+}
+
+void SmtEngine::defineFunction(Expr func,
+ const std::vector<Expr>& formals,
+ Expr formula)
+{
+ SmtScope smts(this);
+ doPendingPops();
+ Trace("smt") << "SMT defineFunction(" << func << ")" << endl;
+ debugCheckFormals(formals, func);
+
+ stringstream ss;
+ ss << language::SetLanguage(
+ language::SetLanguage::getLanguage(Dump.getStream()))
+ << func;
+ DefineFunctionCommand c(ss.str(), func, formals, formula);
+ addToModelCommandAndDump(
+ c, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
+
+ PROOF(if (options::checkUnsatCores()) {
+ d_defineCommands.push_back(c.clone());
+ });
+
+ // type check body
+ debugCheckFunctionBody(formula, formals, func);
+
+ // Substitute out any abstract values in formula
+ Expr form =
+ d_private->substituteAbstractValues(Node::fromExpr(formula)).toExpr();
+
TNode funcNode = func.getTNode();
vector<Node> formalsNodes;
for(vector<Expr>::const_iterator i = formals.begin(),
d_definedFunctions->insert(funcNode, def);
}
+void SmtEngine::defineFunctionsRec(
+ const std::vector<Expr>& funcs,
+ const std::vector<std::vector<Expr> >& formals,
+ const std::vector<Expr>& formulas)
+{
+ SmtScope smts(this);
+ finalOptionsAreSet();
+ doPendingPops();
+ Trace("smt") << "SMT defineFunctionsRec(...)" << endl;
+
+ if (funcs.size() != formals.size() && funcs.size() != formulas.size())
+ {
+ stringstream ss;
+ ss << "Number of functions, formals, and function bodies passed to "
+ "defineFunctionsRec do not match:"
+ << "\n"
+ << " #functions : " << funcs.size() << "\n"
+ << " #arg lists : " << formals.size() << "\n"
+ << " #function bodies : " << formulas.size() << "\n";
+ throw ModalException(ss.str());
+ }
+ for (unsigned i = 0, size = funcs.size(); i < size; i++)
+ {
+ // check formal argument list
+ debugCheckFormals(formals[i], funcs[i]);
+ // type check body
+ debugCheckFunctionBody(formulas[i], formals[i], funcs[i]);
+ }
+
+ if (Dump.isOn("raw-benchmark"))
+ {
+ Dump("raw-benchmark") << DefineFunctionRecCommand(funcs, formals, formulas);
+ }
+
+ ExprManager* em = getExprManager();
+ for (unsigned i = 0, size = funcs.size(); i < size; i++)
+ {
+ // we assert a quantified formula
+ Expr func_app;
+ // make the function application
+ if (formals[i].empty())
+ {
+ // it has no arguments
+ func_app = funcs[i];
+ }
+ else
+ {
+ std::vector<Expr> children;
+ children.push_back(funcs[i]);
+ children.insert(children.end(), formals[i].begin(), formals[i].end());
+ func_app = em->mkExpr(kind::APPLY_UF, children);
+ }
+ Expr lem = em->mkExpr(kind::EQUAL, func_app, formulas[i]);
+ if (!formals[i].empty())
+ {
+ // set the attribute to denote this is a function definition
+ std::string attr_name("fun-def");
+ Expr aexpr = em->mkExpr(kind::INST_ATTRIBUTE, func_app);
+ aexpr = em->mkExpr(kind::INST_PATTERN_LIST, aexpr);
+ std::vector<Expr> expr_values;
+ std::string str_value;
+ setUserAttribute(attr_name, func_app, expr_values, str_value);
+ // make the quantified formula
+ Expr boundVars = em->mkExpr(kind::BOUND_VAR_LIST, formals[i]);
+ lem = em->mkExpr(kind::FORALL, boundVars, lem, aexpr);
+ }
+ // assert the quantified formula
+ // notice we don't call assertFormula directly, since this would
+ // duplicate the output on raw-benchmark.
+ Expr e = d_private->substituteAbstractValues(Node::fromExpr(lem)).toExpr();
+ if (d_assertionList != NULL)
+ {
+ d_assertionList->push_back(e);
+ }
+ d_private->addFormula(e.getNode(), false);
+ }
+}
+
+void SmtEngine::defineFunctionRec(Expr func,
+ const std::vector<Expr>& formals,
+ Expr formula)
+{
+ std::vector<Expr> funcs;
+ funcs.push_back(func);
+ std::vector<std::vector<Expr> > formals_multi;
+ formals_multi.push_back(formals);
+ std::vector<Expr> formulas;
+ formulas.push_back(formula);
+ defineFunctionsRec(funcs, formals_multi, formulas);
+}
+
bool SmtEngine::isDefinedFunction( Expr func ){
Node nf = Node::fromExpr( func );
Debug("smt") << "isDefined function " << nf << "?" << std::endl;
d_statisticsRegistry->safeFlushInformation(fd);
}
-void SmtEngine::setUserAttribute(const std::string& attr, Expr expr, std::vector<Expr> expr_values, std::string str_value) {
+void SmtEngine::setUserAttribute(const std::string& attr,
+ Expr expr,
+ const std::vector<Expr>& expr_values,
+ const std::string& str_value)
+{
SmtScope smts(this);
std::vector<Node> node_values;
for( unsigned i=0; i<expr_values.size(); i++ ){
//check satisfiability (for query and check-sat)
Result checkSatisfiability(const Expr& e, bool inUnsatCore, bool isQuery);
-public:
+
+ /**
+ * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is
+ * the function that the formal argument list is for. This method is used
+ * as a helper function when defining (recursive) functions.
+ */
+ void debugCheckFormals(const std::vector<Expr>& formals, Expr func);
+
+ /**
+ * Checks whether formula is a valid function body for func whose formal
+ * argument list is stored in formals. This method is
+ * used as a helper function when defining (recursive) functions.
+ */
+ void debugCheckFunctionBody(Expr formula,
+ const std::vector<Expr>& formals,
+ Expr func);
+
+ public:
/**
* Construct an SmtEngine with the given expression manager.
throw(OptionException);
/**
- * Add a formula to the current context: preprocess, do per-theory
- * setup, use processAssertionList(), asserting to T-solver for
- * literals and conjunction of literals. Returns false if
- * immediately determined to be inconsistent.
+ * Define function func in the current context to be:
+ * (lambda (formals) formula)
+ * This adds func to the list of defined functions, which indicates that
+ * all occurrences of func should be expanded during expandDefinitions.
+ * This method expects input such that:
+ * - func : a variable of function type that expects the arguments in
+ * formals,
+ * - formals : a list of BOUND_VARIABLE expressions,
+ * - formula does not contain func.
*/
void defineFunction(Expr func,
const std::vector<Expr>& formals,
/** is defined function */
bool isDefinedFunction(Expr func);
+ /** Define functions recursive
+ *
+ * For each i, this constrains funcs[i] in the current context to be:
+ * (lambda (formals[i]) formulas[i])
+ * where formulas[i] may contain variables from funcs. Unlike defineFunction
+ * above, we do not add funcs[i] to the set of defined functions. Instead,
+ * we consider funcs[i] to be a free uninterpreted function, and add:
+ * forall formals[i]. f(formals[i]) = formulas[i]
+ * to the set of assertions in the current context.
+ * This method expects input such that for each i:
+ * - func[i] : a variable of function type that expects the arguments in
+ * formals[i], and
+ * - formals[i] : a list of BOUND_VARIABLE expressions.
+ */
+ void defineFunctionsRec(const std::vector<Expr>& funcs,
+ const std::vector<std::vector<Expr> >& formals,
+ const std::vector<Expr>& formulas);
+
+ /** Define function recursive
+ *
+ * Same as above, but for a single function.
+ */
+ void defineFunctionRec(Expr func,
+ const std::vector<Expr>& formals,
+ Expr formula);
+
/**
* Add a formula to the current context: preprocess, do per-theory
* setup, use processAssertionList(), asserting to T-solver for
* This function is called when an attribute is set by a user.
* In SMT-LIBv2 this is done via the syntax (! expr :attr)
*/
- void setUserAttribute(const std::string& attr, Expr expr, std::vector<Expr> expr_values, std::string str_value);
+ void setUserAttribute(const std::string& attr,
+ Expr expr,
+ const std::vector<Expr>& expr_values,
+ const std::string& str_value);
/**
* Set print function in model
d_unconstrainedSimp->processAssertions(assertions);
}
-
-void TheoryEngine::setUserAttribute(const std::string& attr, Node n, std::vector<Node>& node_values, std::string str_value) {
+void TheoryEngine::setUserAttribute(const std::string& attr,
+ Node n,
+ const std::vector<Node>& node_values,
+ const std::string& str_value)
+{
Trace("te-attr") << "set user attribute " << attr << " " << n << endl;
if( d_attr_handle.find( attr )!=d_attr_handle.end() ){
for( size_t i=0; i<d_attr_handle[attr].size(); i++ ){
std::set< std::string > d_theoryAlternatives;
std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;
-public:
- /**
- * Set user attribute.
- * This function is called when an attribute is set by a user. In SMT-LIBv2 this is done
- * via the syntax (! n :attr)
+ public:
+ /** Set user attribute.
+ *
+ * This function is called when an attribute is set by a user. In SMT-LIBv2
+ * this is done via the syntax (! n :attr)
*/
- void setUserAttribute(const std::string& attr, Node n, std::vector<Node>& node_values, std::string str_value);
+ void setUserAttribute(const std::string& attr,
+ Node n,
+ const std::vector<Node>& node_values,
+ const std::string& str_value);
- /**
- * Handle user attribute.
+ /** Handle user attribute.
+ *
* Associates theory t with the attribute attr. Theory t will be
* notified whenever an attribute of name attr is set.
*/
*/
void checkTheoryAssertionsWithModel(bool hardFailure);
-private:
+ private:
IntStat d_arithSubstitutionsAdded;
};/* class TheoryEngine */
projects / cvc5.git / commitdiff