diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 48 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 12 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.h | 2 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 133 | ||||
| -rw-r--r-- | src/smt/command.cpp | 88 | ||||
| -rw-r--r-- | src/smt/command.h | 33 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 159 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 63 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 7 | ||||
| -rw-r--r-- | src/theory/theory_engine.h | 21 |
10 files changed, 439 insertions, 127 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 5351bae15..1135d6dd4 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1151,10 +1151,10 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] 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; @@ -1198,41 +1198,24 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] 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] @@ -1242,7 +1225,6 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] { 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) @@ -1265,7 +1247,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] } bvs.clear(); PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[0], funcs[0], - flattenVarsList[0], func_app, bvs, true); + flattenVarsList[0], bvs, true); } ( term[expr,expr2] @@ -1275,26 +1257,14 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] 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); } } )+ @@ -1304,7 +1274,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] "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 diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 032fdc673..381a60fa8 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -373,7 +373,6 @@ void Smt2::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) { @@ -391,17 +390,6 @@ void Smt2::pushDefineFunRecScope( } 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() { diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 835ff2b58..4832fc6b5 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -127,13 +127,11 @@ public: * (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); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 19adba6da..c13c519ae 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1113,38 +1113,39 @@ void Smt2Printer::toStream(std::ostream& out, 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; } @@ -1501,6 +1502,74 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) 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; diff --git a/src/smt/command.cpp b/src/smt/command.cpp index aea6365b7..ad7fd9af0 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -890,6 +890,94 @@ Command* DefineNamedFunctionCommand::clone() const { 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( diff --git a/src/smt/command.h b/src/smt/command.h index 33f58aa99..ba7baa738 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -464,6 +464,39 @@ public: };/* 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) */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3cbb3252e..12f822503 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2263,12 +2263,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const { } } -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; @@ -2279,25 +2275,13 @@ void SmtEngine::defineFunction(Expr func, 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 @@ -2326,6 +2310,36 @@ void SmtEngine::defineFunction(Expr func, 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(), @@ -2343,6 +2357,97 @@ void SmtEngine::defineFunction(Expr func, 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; @@ -5684,7 +5789,11 @@ void SmtEngine::safeFlushStatistics(int fd) const { 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++ ){ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 18fc39857..404c9ebe1 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -380,7 +380,24 @@ class CVC4_PUBLIC SmtEngine { //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. @@ -436,10 +453,15 @@ public: 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, @@ -448,6 +470,32 @@ public: /** 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 @@ -769,7 +817,10 @@ public: * 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 diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d01bd537e..944185b31 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -2193,8 +2193,11 @@ void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions) 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++ ){ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 91a88274e..179530240 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -855,17 +855,20 @@ private: 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. */ @@ -877,7 +880,7 @@ public: */ void checkTheoryAssertionsWithModel(bool hardFailure); -private: + private: IntStat d_arithSubstitutionsAdded; };/* class TheoryEngine */ |