From 5c062833d435e3dde5db3a8223c379a3e8cca520 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Tue, 22 Sep 2020 22:12:17 -0500 Subject: [PATCH] Refactor Commands to use the Public API. (#5105) This is work towards eliminating the Expr layer. This PR does the following: Replace Expr/Type with Term/Sort in the API for commands. Remove the command export functionality which is not supported. Since many commands now call the Solver functions instead of the SmtEngine ones, their behavior may be a slightly different. For example, (get-unsat-assumptions) now only works in incremental mode. In some cases, CVC4 will not recover from non-fatal errors. --- src/api/cvc4cpp.cpp | 10 + src/api/cvc4cpp.h | 2 + src/main/command_executor.cpp | 46 +- src/main/command_executor.h | 6 +- src/main/driver_unified.cpp | 4 +- src/main/interactive_shell.cpp | 56 +- src/parser/cvc/Cvc.g | 24 +- src/parser/smt2/Smt2.g | 111 +- src/parser/smt2/smt2.cpp | 11 +- src/parser/tptp/Tptp.g | 24 +- src/parser/tptp/tptp.cpp | 19 +- src/smt/command.cpp | 1066 +++++------------ src/smt/command.h | 495 +++----- src/smt/smt_engine.h | 2 - test/api/smt2_compliance.cpp | 2 +- test/regress/CMakeLists.txt | 3 +- .../smtlib/get-unsat-assumptions.smt2 | 1 + 17 files changed, 660 insertions(+), 1222 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 401f62cae..125e33ba5 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -5708,6 +5708,16 @@ std::vector sortVectorToTypes(const std::vector& sorts) return types; } +std::vector sortVectorToTypeNodes(const std::vector& sorts) +{ + std::vector typeNodes; + for (const Sort& sort : sorts) + { + typeNodes.push_back(TypeNode::fromType(sort.getType())); + } + return typeNodes; +} + std::set sortSetToTypes(const std::set& sorts) { std::set types; diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index c66113f31..841a8ee8a 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -50,6 +50,7 @@ class NodeManager; class SmtEngine; class SynthFunCommand; class Type; +class TypeNode; class Options; class Random; class Result; @@ -3413,6 +3414,7 @@ class CVC4_PUBLIC Solver std::vector termVectorToExprs(const std::vector& terms); std::vector termVectorToNodes(const std::vector& terms); std::vector sortVectorToTypes(const std::vector& sorts); +std::vector sortVectorToTypeNodes(const std::vector& sorts); std::set sortSetToTypes(const std::set& sorts); std::vector exprVectorToTerms(const Solver* slv, const std::vector& terms); diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index caae54e7a..c91b0455c 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -118,12 +118,12 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) { bool status = true; if(d_options.getVerbosity() >= -1) { - status = smtEngineInvoke(d_smtEngine, cmd, d_options.getOut()); + status = solverInvoke(d_solver.get(), cmd, d_options.getOut()); } else { - status = smtEngineInvoke(d_smtEngine, cmd, nullptr); + status = solverInvoke(d_solver.get(), cmd, nullptr); } - Result res; + api::Result res; const CheckSatCommand* cs = dynamic_cast(cmd); if(cs != nullptr) { d_result = res = cs->getResult(); @@ -149,34 +149,34 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) if (status) { std::vector > getterCommands; if (d_options.getDumpModels() - && (res.asSatisfiabilityResult() == Result::SAT - || (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE))) + && (res.isSat() + || (res.isSatUnknown() + && res.getResult().whyUnknown() == Result::INCOMPLETE))) { getterCommands.emplace_back(new GetModelCommand()); } - if (d_options.getDumpProofs() - && res.asSatisfiabilityResult() == Result::UNSAT) + if (d_options.getDumpProofs() && res.isUnsat()) { getterCommands.emplace_back(new GetProofCommand()); } if (d_options.getDumpInstantiations() && ((d_options.getInstFormatMode() != options::InstFormatMode::SZS - && (res.asSatisfiabilityResult() == Result::SAT - || (res.isUnknown() - && res.whyUnknown() == Result::INCOMPLETE))) - || res.asSatisfiabilityResult() == Result::UNSAT)) + && (res.isSat() + || (res.isSatUnknown() + && res.getResult().whyUnknown() == Result::INCOMPLETE))) + || res.isUnsat())) { getterCommands.emplace_back(new GetInstantiationsCommand()); } - if (d_options.getDumpSynth() && - res.asSatisfiabilityResult() == Result::UNSAT) { + if (d_options.getDumpSynth() && res.isUnsat()) + { getterCommands.emplace_back(new GetSynthSolutionCommand()); } - if (d_options.getDumpUnsatCores() && - res.asSatisfiabilityResult() == Result::UNSAT) { + if (d_options.getDumpUnsatCores() && res.isUnsat()) + { getterCommands.emplace_back(new GetUnsatCoreCommand()); } @@ -197,17 +197,21 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) return status; } -bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out) +bool solverInvoke(api::Solver* solver, Command* cmd, std::ostream* out) { - if(out == NULL) { - cmd->invoke(smt); - } else { - cmd->invoke(smt, *out); + if (out == NULL) + { + cmd->invoke(solver); + } + else + { + cmd->invoke(solver, *out); } // ignore the error if the command-verbosity is 0 for this command std::string commandName = std::string("command-verbosity:") + cmd->getCommandName(); - if(smt->getOption(commandName).getIntegerValue() == 0) { + if (solver->getOption(commandName) == "0") + { return true; } return !cmd->fail(); diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 92b0cd166..d7899020e 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -44,7 +44,7 @@ class CommandExecutor SmtEngine* d_smtEngine; Options& d_options; StatisticsRegistry d_stats; - Result d_result; + api::Result d_result; public: CommandExecutor(Options& options); @@ -67,7 +67,7 @@ class CommandExecutor /** Get a pointer to the solver object owned by this CommandExecutor. */ api::Solver* getSolver() { return d_solver.get(); } - Result getResult() const { return d_result; } + api::Result getResult() const { return d_result; } void reset(); StatisticsRegistry& getStatisticsRegistry() { @@ -101,7 +101,7 @@ private: }; /* class CommandExecutor */ -bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out); +bool solverInvoke(api::Solver* solver, Command* cmd, std::ostream* out); }/* CVC4::main namespace */ }/* CVC4 namespace */ diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 43529278b..9fff51b93 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -450,7 +450,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { } } - Result result; + api::Result result; if(status) { result = pExecutor->getResult(); returnValue = 0; @@ -467,7 +467,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { _exit(returnValue); #endif /* CVC4_COMPETITION_MODE */ - ReferenceStat< Result > s_statSatResult("sat/unsat", result); + ReferenceStat s_statSatResult("sat/unsat", result); RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(), &s_statSatResult); diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 121513856..b798d03ee 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -309,34 +309,56 @@ restart: CommandSequence *cmd_seq = new CommandSequence(); Command *cmd; - try { - while( (cmd = d_parser->nextCommand()) ) { + try + { + while ((cmd = d_parser->nextCommand())) + { cmd_seq->addCommand(cmd); - if(dynamic_cast(cmd) != NULL) { + if (dynamic_cast(cmd) != NULL) + { d_quit = true; break; - } else { + } + else + { #if HAVE_LIBEDITLINE - if(dynamic_cast(cmd) != NULL) { - s_declarations.insert(dynamic_cast(cmd)->getSymbol()); - } else if(dynamic_cast(cmd) != NULL) { - s_declarations.insert(dynamic_cast(cmd)->getSymbol()); - } else if(dynamic_cast(cmd) != NULL) { - s_declarations.insert(dynamic_cast(cmd)->getSymbol()); - } else if(dynamic_cast(cmd) != NULL) { - s_declarations.insert(dynamic_cast(cmd)->getSymbol()); + if (dynamic_cast(cmd) != NULL) + { + s_declarations.insert( + dynamic_cast(cmd)->getSymbol()); + } + else if (dynamic_cast(cmd) != NULL) + { + s_declarations.insert( + dynamic_cast(cmd)->getSymbol()); + } + else if (dynamic_cast(cmd) != NULL) + { + s_declarations.insert( + dynamic_cast(cmd)->getSymbol()); + } + else if (dynamic_cast(cmd) != NULL) + { + s_declarations.insert( + dynamic_cast(cmd)->getSymbol()); } #endif /* HAVE_LIBEDITLINE */ } } - } catch(ParserEndOfFileException& pe) { + } + catch (ParserEndOfFileException& pe) + { line += "\n"; goto restart; - } catch(ParserException& pe) { + } + catch (ParserException& pe) + { if (language::isOutputLang_smt2(d_options.getOutputLanguage())) { d_out << "(error \"" << pe << "\")" << endl; - } else { + } + else + { d_out << pe << endl; } // We can't really clear out the sequence and abort the current line, @@ -350,8 +372,8 @@ restart: // FIXME: does that mean e.g. that a pushed LET scope might not yet have // been popped?! // - //delete cmd_seq; - //cmd_seq = new CommandSequence(); + // delete cmd_seq; + // cmd_seq = new CommandSequence(); } return cmd_seq; diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index d1aaa3d15..5f959c660 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -704,13 +704,12 @@ mainCommand[std::unique_ptr* cmd] bool formCommaFlag = true; } /* our bread & butter */ - : ASSERT_TOK formula[f] { cmd->reset(new AssertCommand(f.getExpr())); } + : ASSERT_TOK formula[f] { cmd->reset(new AssertCommand(f)); } - | QUERY_TOK formula[f] { cmd->reset(new QueryCommand(f.getExpr())); } + | QUERY_TOK formula[f] { cmd->reset(new QueryCommand(f)); } | CHECKSAT_TOK formula[f]? { - cmd->reset(f.isNull() ? new CheckSatCommand() - : new CheckSatCommand(f.getExpr())); + cmd->reset(f.isNull() ? new CheckSatCommand() : new CheckSatCommand(f)); } /* options */ | OPTION_TOK @@ -764,7 +763,7 @@ mainCommand[std::unique_ptr* cmd] END_TOK { PARSER_STATE->popScope(); cmd->reset(new DatatypeDeclarationCommand( - api::sortVectorToTypes(PARSER_STATE->bindMutualDatatypeTypes(dts)))); + PARSER_STATE->bindMutualDatatypeTypes(dts))); } | CONTEXT_TOK @@ -789,7 +788,7 @@ mainCommand[std::unique_ptr* cmd] { UNSUPPORTED("GET_OP command"); } | GET_VALUE_TOK formula[f] - { cmd->reset(new GetValueCommand(f.getExpr())); } + { cmd->reset(new GetValueCommand(f)); } | SUBSTITUTE_TOK identifier[id,CHECK_NONE,SYM_VARIABLE] COLON type[t,CHECK_DECLARED] EQUAL_TOK formula[f] LBRACKET @@ -823,7 +822,7 @@ mainCommand[std::unique_ptr* cmd] ) | TRANSFORM_TOK formula[f] - { cmd->reset(new SimplifyCommand(f.getExpr())); } + { cmd->reset(new SimplifyCommand(f)); } | PRINT_TOK formula[f] { UNSUPPORTED("PRINT command"); } @@ -936,8 +935,7 @@ mainCommand[std::unique_ptr* cmd] PARSER_STATE->parseError("Type mismatch in definition"); } } - cmd->reset( - new DefineFunctionRecCommand(SOLVER, funcs, formals, formulas, true)); + cmd->reset(new DefineFunctionRecCommand(funcs, formals, formulas, true)); } | toplevelDeclaration[cmd] ; @@ -1059,7 +1057,7 @@ declareTypes[std::unique_ptr* cmd, // behavior here. PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_SORT); api::Sort sort = PARSER_STATE->mkSort(*i); - Command* decl = new DeclareTypeCommand(*i, 0, sort.getType()); + Command* decl = new DeclareSortCommand(*i, 0, sort); seq->addCommand(decl); } cmd->reset(seq.release()); @@ -1125,8 +1123,7 @@ declareVariables[std::unique_ptr* cmd, CVC4::api::Sort& t, if(topLevel) { api::Term func = PARSER_STATE->bindVar(*i, t, ExprManager::VAR_FLAG_GLOBAL); - Command* decl = - new DeclareFunctionCommand(*i, func.getExpr(), t.getType()); + Command* decl = new DeclareFunctionCommand(*i, func, t); seq->addCommand(decl); } else { PARSER_STATE->bindBoundVar(*i, t); @@ -1156,8 +1153,7 @@ declareVariables[std::unique_ptr* cmd, CVC4::api::Sort& t, api::Sort(SOLVER, t.getType()), ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED); PARSER_STATE->defineVar(*i, f); - Command* decl = - new DefineFunctionCommand(*i, func.getExpr(), f.getExpr(), true); + Command* decl = new DefineFunctionCommand(*i, func, f, true); seq->addCommand(decl); } } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 65f72eb28..232723fc0 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -263,10 +263,10 @@ command [std::unique_ptr* cmd] unsigned arity = AntlrInput::tokenToUnsigned(n); if(arity == 0) { api::Sort type = PARSER_STATE->mkSort(name); - cmd->reset(new DeclareTypeCommand(name, 0, type.getType())); + cmd->reset(new DeclareSortCommand(name, 0, type)); } else { api::Sort type = PARSER_STATE->mkSortConstructor(name, arity); - cmd->reset(new DeclareTypeCommand(name, arity, type.getType())); + cmd->reset(new DeclareSortCommand(name, arity, type)); } } | /* sort definition */ @@ -287,8 +287,7 @@ command [std::unique_ptr* cmd] // Do NOT call mkSort, since that creates a new sort! // This name is not its own distinct sort, it's an alias. PARSER_STATE->defineParameterizedType(name, sorts, t); - cmd->reset(new DefineTypeCommand( - name, api::sortVectorToTypes(sorts), t.getType())); + cmd->reset(new DefineSortCommand(name, sorts, t)); } | /* function declaration */ DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -314,8 +313,7 @@ command [std::unique_ptr* cmd] { api::Term func = PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true); - cmd->reset( - new DeclareFunctionCommand(name, func.getExpr(), t.getType())); + cmd->reset(new DeclareFunctionCommand(name, func, t)); } } | /* function definition */ @@ -334,8 +332,9 @@ command [std::unique_ptr* cmd] ++i) { sorts.push_back((*i).second); } - t = PARSER_STATE->mkFlatFunctionType(sorts, t, flattenVars); } + + t = PARSER_STATE->mkFlatFunctionType(sorts, t, flattenVars); PARSER_STATE->pushScope(true); terms = PARSER_STATE->bindBoundVars(sortedVarNames); } @@ -354,19 +353,15 @@ command [std::unique_ptr* cmd] // we allow overloading for function definitions api::Term func = PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_DEFINED, true); - cmd->reset( - new DefineFunctionCommand(name, - func.getExpr(), - api::termVectorToExprs(terms), - expr.getExpr(), - PARSER_STATE->getGlobalDeclarations())); + cmd->reset(new DefineFunctionCommand( + name, func, terms, expr, PARSER_STATE->getGlobalDeclarations())); } | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd] | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] | /* value query */ GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( LPAREN_TOK termList[terms,expr] RPAREN_TOK - { cmd->reset(new GetValueCommand(api::termVectorToExprs(terms))); } + { cmd->reset(new GetValueCommand(terms)); } | ~LPAREN_TOK { PARSER_STATE->parseError("The get-value command expects a list of " "terms. Perhaps you forgot a pair of " @@ -381,13 +376,13 @@ command [std::unique_ptr* cmd] { PARSER_STATE->clearLastNamedTerm(); } term[expr, expr2] { bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr; - cmd->reset(new AssertCommand(expr.getExpr(), inUnsatCore)); + cmd->reset(new AssertCommand(expr, inUnsatCore)); if(inUnsatCore) { // set the expression name, if there was a named term std::pair namedTerm = PARSER_STATE->lastNamedTerm(); - Command* csen = new SetExpressionNameCommand(namedTerm.first.getExpr(), - namedTerm.second); + Command* csen = + new SetExpressionNameCommand(namedTerm.first, namedTerm.second); csen->setMuted(true); PARSER_STATE->preemptCommand(csen); } @@ -407,12 +402,12 @@ command [std::unique_ptr* cmd] } | { expr = api::Term(); } ) - { cmd->reset(new CheckSatCommand(expr.getExpr())); } + { cmd->reset(new CheckSatCommand(expr)); } | /* check-sat-assuming */ CHECK_SAT_ASSUMING_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( LPAREN_TOK termList[terms,expr] RPAREN_TOK { - cmd->reset(new CheckSatAssumingCommand(api::termVectorToExprs(terms))); + cmd->reset(new CheckSatAssumingCommand(terms)); } | ~LPAREN_TOK { PARSER_STATE->parseError("The check-sat-assuming command expects a " @@ -558,7 +553,7 @@ sygusCommand returns [std::unique_ptr cmd] sortSymbol[t,CHECK_DECLARED] { api::Term var = PARSER_STATE->bindBoundVar(name, t); - cmd.reset(new DeclareSygusVarCommand(name, var.getExpr(), t.getType())); + cmd.reset(new DeclareSygusVarCommand(name, var, t)); } | /* synth-fun */ ( SYNTH_FUN_TOK { isInv = false; } @@ -590,7 +585,7 @@ sygusCommand returns [std::unique_ptr cmd] } term[expr, expr2] { Debug("parser-sygus") << "...read constraint " << expr << std::endl; - cmd.reset(new SygusConstraintCommand(expr.getExpr())); + cmd.reset(new SygusConstraintCommand(expr)); } | /* inv-constraint */ INV_CONSTRAINT_TOK @@ -788,7 +783,7 @@ smt25Command[std::unique_ptr* cmd] { // allow overloading here api::Term c = PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true); - cmd->reset(new DeclareFunctionCommand(name, c.getExpr(), t.getType())); } + cmd->reset(new DeclareFunctionCommand(name, c, t)); } /* get model */ | GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -831,7 +826,7 @@ smt25Command[std::unique_ptr* cmd] expr = PARSER_STATE->mkHoApply( expr, flattenVars ); } cmd->reset(new DefineFunctionRecCommand( - SOLVER, func, bvs, expr, PARSER_STATE->getGlobalDeclarations())); + func, bvs, expr, PARSER_STATE->getGlobalDeclarations())); } | DEFINE_FUNS_REC_TOK { PARSER_STATE->checkThatLogicIsSet();} @@ -894,12 +889,8 @@ smt25Command[std::unique_ptr* cmd] "Number of functions defined does not match number listed in " "define-funs-rec")); } - cmd->reset( - new DefineFunctionRecCommand(SOLVER, - funcs, - formals, - func_defs, - PARSER_STATE->getGlobalDeclarations())); + cmd->reset(new DefineFunctionRecCommand( + funcs, formals, func_defs, PARSER_STATE->getGlobalDeclarations())); } ; @@ -935,7 +926,7 @@ extendedCommand[std::unique_ptr* cmd] ( symbol[name,CHECK_UNDECLARED,SYM_SORT] { PARSER_STATE->checkUserSymbol(name); api::Sort type = PARSER_STATE->mkSort(name); - seq->addCommand(new DeclareTypeCommand(name, 0, type.getType())); + seq->addCommand(new DeclareSortCommand(name, 0, type)); } )+ RPAREN_TOK @@ -960,8 +951,7 @@ extendedCommand[std::unique_ptr* cmd] // allow overloading api::Term func = PARSER_STATE->bindVar(name, tt, ExprManager::VAR_FLAG_NONE, true); - seq->addCommand( - new DeclareFunctionCommand(name, func.getExpr(), tt.getType())); + seq->addCommand(new DeclareFunctionCommand(name, func, tt)); sorts.clear(); } )+ @@ -981,8 +971,7 @@ extendedCommand[std::unique_ptr* cmd] // allow overloading api::Term func = PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true); - seq->addCommand( - new DeclareFunctionCommand(name, func.getExpr(), t.getType())); + seq->addCommand(new DeclareFunctionCommand(name, func, t)); sorts.clear(); } )+ @@ -997,11 +986,8 @@ extendedCommand[std::unique_ptr* cmd] { api::Term func = PARSER_STATE->bindVar(name, e.getSort(), ExprManager::VAR_FLAG_DEFINED); - cmd->reset( - new DefineFunctionCommand(name, - func.getExpr(), - e.getExpr(), - PARSER_STATE->getGlobalDeclarations())); + cmd->reset(new DefineFunctionCommand( + name, func, e, PARSER_STATE->getGlobalDeclarations())); } | // (define (f (v U) ...) t) LPAREN_TOK @@ -1031,12 +1017,8 @@ extendedCommand[std::unique_ptr* cmd] } api::Term func = PARSER_STATE->bindVar(name, tt, ExprManager::VAR_FLAG_DEFINED); - cmd->reset( - new DefineFunctionCommand(name, - func.getExpr(), - api::termVectorToExprs(terms), - e.getExpr(), - PARSER_STATE->getGlobalDeclarations())); + cmd->reset(new DefineFunctionCommand( + name, func, terms, e, PARSER_STATE->getGlobalDeclarations())); } ) | // (define-const x U t) @@ -1057,23 +1039,19 @@ extendedCommand[std::unique_ptr* cmd] // permitted) api::Term func = PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_DEFINED); - cmd->reset( - new DefineFunctionCommand(name, - func.getExpr(), - api::termVectorToExprs(terms), - e.getExpr(), - PARSER_STATE->getGlobalDeclarations())); + cmd->reset(new DefineFunctionCommand( + name, func, terms, e, PARSER_STATE->getGlobalDeclarations())); } | SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); } term[e,e2] - { cmd->reset(new SimplifyCommand(e.getExpr())); } + { cmd->reset(new SimplifyCommand(e)); } | GET_QE_TOK { PARSER_STATE->checkThatLogicIsSet(); } term[e,e2] - { cmd->reset(new GetQuantifierEliminationCommand(e.getExpr(), true)); } + { cmd->reset(new GetQuantifierEliminationCommand(e, true)); } | GET_QE_DISJUNCT_TOK { PARSER_STATE->checkThatLogicIsSet(); } term[e,e2] - { cmd->reset(new GetQuantifierEliminationCommand(e.getExpr(), false)); } + { cmd->reset(new GetQuantifierEliminationCommand(e, false)); } | GET_ABDUCT_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -1083,7 +1061,7 @@ extendedCommand[std::unique_ptr* cmd] sygusGrammar[g, terms, name] )? { - cmd->reset(new GetAbductCommand(SOLVER, name, e, g)); + cmd->reset(new GetAbductCommand(name, e, g)); } | GET_INTERPOL_TOK { PARSER_STATE->checkThatLogicIsSet(); @@ -1094,7 +1072,7 @@ extendedCommand[std::unique_ptr* cmd] sygusGrammar[g, terms, name] )? { - cmd->reset(new GetInterpolCommand(SOLVER, name, e, g)); + cmd->reset(new GetInterpolCommand(name, e, g)); } | DECLARE_HEAP LPAREN_TOK sortSymbol[t, CHECK_DECLARED] @@ -1107,7 +1085,7 @@ extendedCommand[std::unique_ptr* cmd] | BLOCK_MODEL_VALUES_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( LPAREN_TOK termList[terms,e] RPAREN_TOK - { cmd->reset(new BlockModelValuesCommand(api::termVectorToExprs(terms))); } + { cmd->reset(new BlockModelValuesCommand(terms)); } | ~LPAREN_TOK { PARSER_STATE->parseError("The block-model-value command expects a list " "of terms. Perhaps you forgot a pair of " @@ -1138,8 +1116,7 @@ datatypes_2_5_DefCommand[bool isCo, std::unique_ptr* cmd] LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK { PARSER_STATE->popScope(); cmd->reset(new DatatypeDeclarationCommand( - api::sortVectorToTypes( - PARSER_STATE->bindMutualDatatypeTypes(dts, true)))); + PARSER_STATE->bindMutualDatatypeTypes(dts, true))); } ; @@ -1271,8 +1248,7 @@ datatypesDef[bool isCo, } PARSER_STATE->popScope(); cmd->reset(new DatatypeDeclarationCommand( - api::sortVectorToTypes( - PARSER_STATE->bindMutualDatatypeTypes(dts, true)))); + PARSER_STATE->bindMutualDatatypeTypes(dts, true))); } ; @@ -1847,8 +1823,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] api::Sort boolType = SOLVER->getBooleanSort(); api::Term avar = PARSER_STATE->bindVar(attr_name, boolType); retExpr = MK_TERM(api::INST_ATTRIBUTE, avar); - Command* c = new SetUserAttributeCommand( - attr_name, avar.getExpr(), api::termVectorToExprs(values)); + Command* c = new SetUserAttributeCommand(attr_name, avar, values); c->setMuted(true); PARSER_STATE->preemptCommand(c); } @@ -1858,7 +1833,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] api::Term avar = SOLVER->mkConst(boolType, sexpr.toString()); attr = std::string(":qid"); retExpr = MK_TERM(api::INST_ATTRIBUTE, avar); - Command* c = new SetUserAttributeCommand("qid", avar.getExpr()); + Command* c = new SetUserAttributeCommand("qid", avar); c->setMuted(true); PARSER_STATE->preemptCommand(c); } @@ -1868,8 +1843,12 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] api::Term func = PARSER_STATE->setNamedAttribute(expr, sexpr); std::string name = sexpr.getValue(); // bind name to expr with define-fun - Command* c = new DefineNamedFunctionCommand( - name, func.getExpr(), std::vector(), expr.getExpr(), PARSER_STATE->getGlobalDeclarations()); + Command* c = + new DefineNamedFunctionCommand(name, + func, + std::vector(), + expr, + PARSER_STATE->getGlobalDeclarations()); c->setMuted(true); PARSER_STATE->preemptCommand(c); } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 387117335..e7bb8795c 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -525,8 +525,8 @@ std::unique_ptr Smt2::SynthFunFactory::mkCommand(api::Grammar* grammar) { Debug("parser-sygus") << "...read synth fun " << d_id << std::endl; d_smt2->popScope(); - return std::unique_ptr(new SynthFunCommand( - d_smt2->d_solver, d_id, d_fun, d_sygusVars, d_sort, d_isInv, grammar)); + return std::unique_ptr( + new SynthFunCommand(d_id, d_fun, d_sygusVars, d_sort, d_isInv, grammar)); } std::unique_ptr Smt2::invConstraint( @@ -556,8 +556,7 @@ std::unique_ptr Smt2::invConstraint( terms.push_back(getVariable(name)); } - return std::unique_ptr( - new SygusInvConstraintCommand(api::termVectorToExprs(terms))); + return std::unique_ptr(new SygusInvConstraintCommand(terms)); } Command* Smt2::setLogic(std::string name, bool fromCommand) @@ -776,8 +775,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) api::Grammar* Smt2::mkGrammar(const std::vector& boundVars, const std::vector& ntSymbols) { - d_allocGrammars.emplace_back(new api::Grammar( - std::move(d_solver->mkSygusGrammar(boundVars, ntSymbols)))); + d_allocGrammars.emplace_back( + new api::Grammar(d_solver->mkSygusGrammar(boundVars, ntSymbols))); return d_allocGrammars.back().get(); } diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 050a23320..b99376685 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -161,10 +161,10 @@ parseCommand returns [CVC4::Command* cmd = NULL] } (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK { - CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr); + CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr, expr); if( !aexpr.isNull() ){ // set the expression name (e.g. used with unsat core printing) - Command* csen = new SetExpressionNameCommand(aexpr.getExpr(), name); + Command* csen = new SetExpressionNameCommand(aexpr, name); csen->setMuted(true); PARSER_STATE->preemptCommand(csen); } @@ -178,7 +178,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr); if( !aexpr.isNull() ){ // set the expression name (e.g. used with unsat core printing) - Command* csen = new SetExpressionNameCommand(aexpr.getExpr(), name); + Command* csen = new SetExpressionNameCommand(aexpr, name); csen->setMuted(true); PARSER_STATE->preemptCommand(csen); } @@ -194,7 +194,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr); if( !aexpr.isNull() ){ // set the expression name (e.g. used with unsat core printing) - Command* csen = new SetExpressionNameCommand(aexpr.getExpr(), name); + Command* csen = new SetExpressionNameCommand(aexpr, name); csen->setMuted(true); PARSER_STATE->preemptCommand(csen); } @@ -219,7 +219,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] if (!aexpr.isNull()) { // set the expression name (e.g. used with unsat core printing) - Command* csen = new SetExpressionNameCommand(aexpr.getExpr(), name); + Command* csen = new SetExpressionNameCommand(aexpr, name); csen->setMuted(true); PARSER_STATE->preemptCommand(csen); } @@ -255,7 +255,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] CVC4::api::Term aexpr = PARSER_STATE->getAssertionDistinctConstants(); if( !aexpr.isNull() ) { - seq->addCommand(new AssertCommand(aexpr.getExpr(), false)); + seq->addCommand(new AssertCommand(aexpr, false)); } std::string filename = PARSER_STATE->getInput()->getInputStreamName(); @@ -268,7 +268,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] } seq->addCommand(new SetInfoCommand("filename", SExpr(filename))); if(PARSER_STATE->hasConjecture()) { - seq->addCommand(new QueryCommand(SOLVER->mkFalse().getExpr())); + seq->addCommand(new QueryCommand(SOLVER->mkFalse())); } else { seq->addCommand(new CheckSatCommand()); } @@ -967,7 +967,7 @@ thfAtomTyping[CVC4::Command*& cmd] { // as yet, it's undeclared api::Sort atype = PARSER_STATE->mkSort(name); - cmd = new DeclareTypeCommand(name, 0, atype.getType()); + cmd = new DeclareSortCommand(name, 0, atype); } } | parseThfType[type] @@ -1007,8 +1007,7 @@ thfAtomTyping[CVC4::Command*& cmd] { freshExpr = PARSER_STATE->bindVar(name, type); } - cmd = new DeclareFunctionCommand( - name, freshExpr.getExpr(), type.getType()); + cmd = new DeclareFunctionCommand(name, freshExpr, type); } } ) @@ -1320,7 +1319,7 @@ tffTypedAtom[CVC4::Command*& cmd] } else { // as yet, it's undeclared api::Sort atype = PARSER_STATE->mkSort(name); - cmd = new DeclareTypeCommand(name, 0, atype.getType()); + cmd = new DeclareSortCommand(name, 0, atype); } } | parseType[type] @@ -1339,8 +1338,7 @@ tffTypedAtom[CVC4::Command*& cmd] } else { // as yet, it's undeclared CVC4::api::Term aexpr = PARSER_STATE->bindVar(name, type); - cmd = - new DeclareFunctionCommand(name, aexpr.getExpr(), type.getType()); + cmd = new DeclareFunctionCommand(name, aexpr, type); } } ) diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 8f75cf8d3..066970fe3 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -76,8 +76,7 @@ void Tptp::addTheory(Theory theory) { { std::string d_unsorted_name = "$$unsorted"; d_unsorted = d_solver->mkUninterpretedSort(d_unsorted_name); - preemptCommand( - new DeclareTypeCommand(d_unsorted_name, 0, d_unsorted.getType())); + preemptCommand(new DeclareSortCommand(d_unsorted_name, 0, d_unsorted)); } // propositionnal defineType("Bool", d_solver->getBooleanSort()); @@ -243,8 +242,7 @@ api::Term Tptp::parseOpToExpr(ParseOp& p) api::Sort t = p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted; expr = bindVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero - preemptCommand( - new DeclareFunctionCommand(p.d_name, expr.getExpr(), t.getType())); + preemptCommand(new DeclareFunctionCommand(p.d_name, expr, t)); } return expr; } @@ -288,8 +286,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector& args) p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted; t = d_solver->mkFunctionSort(sorts, t); v = bindVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero - preemptCommand( - new DeclareFunctionCommand(p.d_name, v.getExpr(), t.getType())); + preemptCommand(new DeclareFunctionCommand(p.d_name, v, t)); } // args might be rationals, in which case we need to create // distinct constants of the "unsorted" sort to represent them @@ -394,13 +391,11 @@ api::Term Tptp::convertRatToUnsorted(api::Term expr) // Conversion from rational to unsorted t = d_solver->mkFunctionSort(d_solver->getRealSort(), d_unsorted); d_rtu_op = d_solver->mkConst(t, "$$rtu"); - preemptCommand( - new DeclareFunctionCommand("$$rtu", d_rtu_op.getExpr(), t.getType())); + preemptCommand(new DeclareFunctionCommand("$$rtu", d_rtu_op, t)); // Conversion from unsorted to rational t = d_solver->mkFunctionSort(d_unsorted, d_solver->getRealSort()); d_utr_op = d_solver->mkConst(t, "$$utr"); - preemptCommand( - new DeclareFunctionCommand("$$utr", d_utr_op.getExpr(), t.getType())); + preemptCommand(new DeclareFunctionCommand("$$utr", d_utr_op, t)); } // Add the inverse in order to show that over the elements that // appear in the problem there is a bijection between unsorted and @@ -410,7 +405,7 @@ api::Term Tptp::convertRatToUnsorted(api::Term expr) d_r_converted.insert(expr); api::Term eq = d_solver->mkTerm( api::EQUAL, expr, d_solver->mkTerm(api::APPLY_UF, d_utr_op, ret)); - preemptCommand(new AssertCommand(eq.getExpr())); + preemptCommand(new AssertCommand(eq)); } return api::Term(ret); } @@ -506,7 +501,7 @@ Command* Tptp::makeAssertCommand(FormulaRole fr, if( expr.isNull() ){ return new EmptyCommand("Untreated role for expression"); }else{ - return new AssertCommand(expr.getExpr(), inUnsatCore); + return new AssertCommand(expr, inUnsatCore); } } diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 6d236aa47..84bc5fc99 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -105,20 +105,6 @@ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) } } -// !!! Temporary until commands are migrated to the new API !!! -std::vector typeVectorToTypeNodes(const std::vector& types) -{ - std::vector typeNodes; - typeNodes.reserve(types.size()); - - for (Type t : types) - { - typeNodes.push_back(TypeNode::fromType(t)); - } - - return typeNodes; -} - /* -------------------------------------------------------------------------- */ /* class CommandPrintSuccess */ /* -------------------------------------------------------------------------- */ @@ -151,7 +137,7 @@ std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) Command::Command() : d_commandStatus(nullptr), d_muted(false) {} Command::Command(const api::Solver* solver) - : d_solver(solver), d_commandStatus(nullptr), d_muted(false) + : d_commandStatus(nullptr), d_muted(false) { } @@ -189,15 +175,14 @@ bool Command::interrupted() const && dynamic_cast(d_commandStatus) != NULL; } -void Command::invoke(SmtEngine* smtEngine, std::ostream& out) +void Command::invoke(api::Solver* solver, std::ostream& out) { - invoke(smtEngine); + invoke(solver); if (!(isMuted() && ok())) { - printResult(out, - smtEngine->getOption("command-verbosity:" + getCommandName()) - .getIntegerValue() - .toUnsignedInt()); + printResult( + out, + std::stoul(solver->getOption("command-verbosity:" + getCommandName()))); } } @@ -230,18 +215,12 @@ void Command::printResult(std::ostream& out, uint32_t verbosity) const EmptyCommand::EmptyCommand(std::string name) : d_name(name) {} std::string EmptyCommand::getName() const { return d_name; } -void EmptyCommand::invoke(SmtEngine* smtEngine) +void EmptyCommand::invoke(api::Solver* solver) { /* empty commands have no implementation */ d_commandStatus = CommandSuccess::instance(); } -Command* EmptyCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - return new EmptyCommand(d_name); -} - Command* EmptyCommand::clone() const { return new EmptyCommand(d_name); } std::string EmptyCommand::getCommandName() const { return "empty"; } @@ -260,28 +239,21 @@ void EmptyCommand::toStream(std::ostream& out, EchoCommand::EchoCommand(std::string output) : d_output(output) {} std::string EchoCommand::getOutput() const { return d_output; } -void EchoCommand::invoke(SmtEngine* smtEngine) +void EchoCommand::invoke(api::Solver* solver) { /* we don't have an output stream here, nothing to do */ d_commandStatus = CommandSuccess::instance(); } -void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out) +void EchoCommand::invoke(api::Solver* solver, std::ostream& out) { out << d_output << std::endl; Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~" << std::endl; d_commandStatus = CommandSuccess::instance(); - printResult(out, - smtEngine->getOption("command-verbosity:" + getCommandName()) - .getIntegerValue() - .toUnsignedInt()); -} - -Command* EchoCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - return new EchoCommand(d_output); + printResult( + out, + std::stoul(solver->getOption("command-verbosity:" + getCommandName()))); } Command* EchoCommand::clone() const { return new EchoCommand(d_output); } @@ -300,17 +272,17 @@ void EchoCommand::toStream(std::ostream& out, /* class AssertCommand */ /* -------------------------------------------------------------------------- */ -AssertCommand::AssertCommand(const Expr& e, bool inUnsatCore) - : d_expr(e), d_inUnsatCore(inUnsatCore) +AssertCommand::AssertCommand(const api::Term& t, bool inUnsatCore) + : d_term(t), d_inUnsatCore(inUnsatCore) { } -Expr AssertCommand::getExpr() const { return d_expr; } -void AssertCommand::invoke(SmtEngine* smtEngine) +api::Term AssertCommand::getTerm() const { return d_term; } +void AssertCommand::invoke(api::Solver* solver) { try { - smtEngine->assertFormula(d_expr, d_inUnsatCore); + solver->getSmtEngine()->assertFormula(d_term.getExpr(), d_inUnsatCore); d_commandStatus = CommandSuccess::instance(); } catch (UnsafeInterruptException& e) @@ -323,16 +295,9 @@ void AssertCommand::invoke(SmtEngine* smtEngine) } } -Command* AssertCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - return new AssertCommand(d_expr.exportTo(exprManager, variableMap), - d_inUnsatCore); -} - Command* AssertCommand::clone() const { - return new AssertCommand(d_expr, d_inUnsatCore); + return new AssertCommand(d_term, d_inUnsatCore); } std::string AssertCommand::getCommandName() const { return "assert"; } @@ -343,18 +308,18 @@ void AssertCommand::toStream(std::ostream& out, size_t dag, OutputLanguage language) const { - Printer::getPrinter(language)->toStreamCmdAssert(out, Node::fromExpr(d_expr)); + Printer::getPrinter(language)->toStreamCmdAssert(out, d_term.getNode()); } /* -------------------------------------------------------------------------- */ /* class PushCommand */ /* -------------------------------------------------------------------------- */ -void PushCommand::invoke(SmtEngine* smtEngine) +void PushCommand::invoke(api::Solver* solver) { try { - smtEngine->push(); + solver->push(); d_commandStatus = CommandSuccess::instance(); } catch (UnsafeInterruptException& e) @@ -367,12 +332,6 @@ void PushCommand::invoke(SmtEngine* smtEngine) } } -Command* PushCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - return new PushCommand(); -} - Command* PushCommand::clone() const { return new PushCommand(); } std::string PushCommand::getCommandName() const { return "push"; } @@ -389,11 +348,11 @@ void PushCommand::toStream(std::ostream& out, /* class PopCommand */ /* -------------------------------------------------------------------------- */ -void PopCommand::invoke(SmtEngine* smtEngine) +void PopCommand::invoke(api::Solver* solver) { try { - smtEngine->pop(); + solver->pop(); d_commandStatus = CommandSuccess::instance(); } catch (UnsafeInterruptException& e) @@ -406,12 +365,6 @@ void PopCommand::invoke(SmtEngine* smtEngine) } } -Command* PopCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - return new PopCommand(); -} - Command* PopCommand::clone() const { return new PopCommand(); } std::string PopCommand::getCommandName() const { return "pop"; } @@ -428,18 +381,20 @@ void PopCommand::toStream(std::ostream& out, /* class CheckSatCommand */ /* -------------------------------------------------------------------------- */ -CheckSatCommand::CheckSatCommand() : d_expr() {} +CheckSatCommand::CheckSatCommand() : d_term() {} -CheckSatCommand::CheckSatCommand(const Expr& expr) : d_expr(expr) {} +CheckSatCommand::CheckSatCommand(const api::Term& term) : d_term(term) {} -Expr CheckSatCommand::getExpr() const { return d_expr; } -void CheckSatCommand::invoke(SmtEngine* smtEngine) +api::Term CheckSatCommand::getTerm() const { return d_term; } +void CheckSatCommand::invoke(api::Solver* solver) { Trace("dtview::command") << "* ~COMMAND: " << getCommandName() << "~" << std::endl; try { - d_result = smtEngine->checkSat(d_expr); + d_result = + d_term.isNull() ? solver->checkSat() : solver->checkSatAssuming(d_term); + d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -448,7 +403,7 @@ void CheckSatCommand::invoke(SmtEngine* smtEngine) } } -Result CheckSatCommand::getResult() const { return d_result; } +api::Result CheckSatCommand::getResult() const { return d_result; } void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const { if (!ok()) @@ -462,18 +417,9 @@ void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const } } -Command* CheckSatCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - CheckSatCommand* c = - new CheckSatCommand(d_expr.exportTo(exprManager, variableMap)); - c->d_result = d_result; - return c; -} - Command* CheckSatCommand::clone() const { - CheckSatCommand* c = new CheckSatCommand(d_expr); + CheckSatCommand* c = new CheckSatCommand(d_term); c->d_result = d_result; return c; } @@ -486,33 +432,36 @@ void CheckSatCommand::toStream(std::ostream& out, size_t dag, OutputLanguage language) const { - Printer::getPrinter(language)->toStreamCmdCheckSat(out, - Node::fromExpr(d_expr)); + Printer::getPrinter(language)->toStreamCmdCheckSat(out, d_term.getNode()); } /* -------------------------------------------------------------------------- */ /* class CheckSatAssumingCommand */ /* -------------------------------------------------------------------------- */ -CheckSatAssumingCommand::CheckSatAssumingCommand(Expr term) : d_terms({term}) {} +CheckSatAssumingCommand::CheckSatAssumingCommand(api::Term term) + : d_terms({term}) +{ +} -CheckSatAssumingCommand::CheckSatAssumingCommand(const std::vector& terms) +CheckSatAssumingCommand::CheckSatAssumingCommand( + const std::vector& terms) : d_terms(terms) { } -const std::vector& CheckSatAssumingCommand::getTerms() const +const std::vector& CheckSatAssumingCommand::getTerms() const { return d_terms; } -void CheckSatAssumingCommand::invoke(SmtEngine* smtEngine) +void CheckSatAssumingCommand::invoke(api::Solver* solver) { Trace("dtview::command") << "* ~COMMAND: (check-sat-assuming ( " << d_terms << " )~" << std::endl; try { - d_result = smtEngine->checkSat(d_terms); + d_result = solver->checkSatAssuming(d_terms); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -521,7 +470,7 @@ void CheckSatAssumingCommand::invoke(SmtEngine* smtEngine) } } -Result CheckSatAssumingCommand::getResult() const +api::Result CheckSatAssumingCommand::getResult() const { Trace("dtview::command") << "* ~RESULT: " << d_result << "~" << std::endl; return d_result; @@ -540,19 +489,6 @@ void CheckSatAssumingCommand::printResult(std::ostream& out, } } -Command* CheckSatAssumingCommand::exportTo( - ExprManager* exprManager, ExprManagerMapCollection& variableMap) -{ - vector exportedTerms; - for (const Expr& e : d_terms) - { - exportedTerms.push_back(e.exportTo(exprManager, variableMap)); - } - CheckSatAssumingCommand* c = new CheckSatAssumingCommand(exportedTerms); - c->d_result = d_result; - return c; -} - Command* CheckSatAssumingCommand::clone() const { CheckSatAssumingCommand* c = new CheckSatAssumingCommand(d_terms); @@ -571,30 +507,25 @@ void CheckSatAssumingCommand::toStream(std::ostream& out, size_t dag, OutputLanguage language) const { - std::vector nodes; - nodes.reserve(d_terms.size()); - for (const Expr& e : d_terms) - { - nodes.push_back(Node::fromExpr(e)); - } - Printer::getPrinter(language)->toStreamCmdCheckSatAssuming(out, nodes); + Printer::getPrinter(language)->toStreamCmdCheckSatAssuming( + out, api::termVectorToNodes(d_terms)); } /* -------------------------------------------------------------------------- */ /* class QueryCommand */ /* -------------------------------------------------------------------------- */ -QueryCommand::QueryCommand(const Expr& e, bool inUnsatCore) - : d_expr(e), d_inUnsatCore(inUnsatCore) +QueryCommand::QueryCommand(const api::Term& t, bool inUnsatCore) + : d_term(t), d_inUnsatCore(inUnsatCore) { } -Expr QueryCommand::getExpr() const { return d_expr; } -void QueryCommand::invoke(SmtEngine* smtEngine) +api::Term QueryCommand::getTerm() const { return d_term; } +void QueryCommand::invoke(api::Solver* solver) { try { - d_result = smtEngine->checkEntailed(d_expr); + d_result = solver->checkEntailed(d_term); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -603,7 +534,7 @@ void QueryCommand::invoke(SmtEngine* smtEngine) } } -Result QueryCommand::getResult() const { return d_result; } +api::Result QueryCommand::getResult() const { return d_result; } void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const { if (!ok()) @@ -616,18 +547,9 @@ void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const } } -Command* QueryCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap), - d_inUnsatCore); - c->d_result = d_result; - return c; -} - Command* QueryCommand::clone() const { - QueryCommand* c = new QueryCommand(d_expr, d_inUnsatCore); + QueryCommand* c = new QueryCommand(d_term, d_inUnsatCore); c->d_result = d_result; return c; } @@ -640,7 +562,7 @@ void QueryCommand::toStream(std::ostream& out, size_t dag, OutputLanguage language) const { - Printer::getPrinter(language)->toStreamCmdQuery(out, d_expr); + Printer::getPrinter(language)->toStreamCmdQuery(out, d_term.getNode()); } /* -------------------------------------------------------------------------- */ @@ -648,21 +570,21 @@ void QueryCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ DeclareSygusVarCommand::DeclareSygusVarCommand(const std::string& id, - Expr var, - Type t) - : DeclarationDefinitionCommand(id), d_var(var), d_type(t) + api::Term var, + api::Sort sort) + : DeclarationDefinitionCommand(id), d_var(var), d_sort(sort) { } -Expr DeclareSygusVarCommand::getVar() const { return d_var; } -Type DeclareSygusVarCommand::getType() const { return d_type; } +api::Term DeclareSygusVarCommand::getVar() const { return d_var; } +api::Sort DeclareSygusVarCommand::getSort() const { return d_sort; } -void DeclareSygusVarCommand::invoke(SmtEngine* smtEngine) +void DeclareSygusVarCommand::invoke(api::Solver* solver) { try { - smtEngine->declareSygusVar( - d_symbol, Node::fromExpr(d_var), TypeNode::fromType(d_type)); + solver->getSmtEngine()->declareSygusVar( + d_symbol, d_var.getNode(), TypeNode::fromType(d_sort.getType())); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -671,17 +593,9 @@ void DeclareSygusVarCommand::invoke(SmtEngine* smtEngine) } } -Command* DeclareSygusVarCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - return new DeclareSygusVarCommand(d_symbol, - d_var.exportTo(exprManager, variableMap), - d_type.exportTo(exprManager, variableMap)); -} - Command* DeclareSygusVarCommand::clone() const { - return new DeclareSygusVarCommand(d_symbol, d_var, d_type); + return new DeclareSygusVarCommand(d_symbol, d_var, d_sort); } std::string DeclareSygusVarCommand::getCommandName() const @@ -696,15 +610,14 @@ void DeclareSygusVarCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdDeclareVar( - out, Node::fromExpr(d_var), TypeNode::fromType(d_type)); + out, d_var.getNode(), TypeNode::fromType(d_sort.getType())); } /* -------------------------------------------------------------------------- */ /* class SynthFunCommand */ /* -------------------------------------------------------------------------- */ -SynthFunCommand::SynthFunCommand(const api::Solver* solver, - const std::string& id, +SynthFunCommand::SynthFunCommand(const std::string& id, api::Term fun, const std::vector& vars, api::Sort sort, @@ -717,7 +630,6 @@ SynthFunCommand::SynthFunCommand(const api::Solver* solver, d_isInv(isInv), d_grammar(g) { - d_solver = solver; } api::Term SynthFunCommand::getFunction() const { return d_fun; } @@ -732,7 +644,7 @@ bool SynthFunCommand::isInv() const { return d_isInv; } const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; } -void SynthFunCommand::invoke(SmtEngine* smtEngine) +void SynthFunCommand::invoke(api::Solver* solver) { try { @@ -741,7 +653,7 @@ void SynthFunCommand::invoke(SmtEngine* smtEngine) { vns.push_back(Node::fromExpr(t.getExpr())); } - smtEngine->declareSynthFun( + solver->getSmtEngine()->declareSynthFun( d_symbol, Node::fromExpr(d_fun.getExpr()), TypeNode::fromType(d_grammar == nullptr @@ -757,16 +669,10 @@ void SynthFunCommand::invoke(SmtEngine* smtEngine) } } -Command* SynthFunCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - Unimplemented(); -} - Command* SynthFunCommand::clone() const { return new SynthFunCommand( - d_solver, d_symbol, d_fun, d_vars, d_sort, d_isInv, d_grammar); + d_symbol, d_fun, d_vars, d_sort, d_isInv, d_grammar); } std::string SynthFunCommand::getCommandName() const @@ -794,13 +700,15 @@ void SynthFunCommand::toStream(std::ostream& out, /* class SygusConstraintCommand */ /* -------------------------------------------------------------------------- */ -SygusConstraintCommand::SygusConstraintCommand(const Expr& e) : d_expr(e) {} +SygusConstraintCommand::SygusConstraintCommand(const api::Term& t) : d_term(t) +{ +} -void SygusConstraintCommand::invoke(SmtEngine* smtEngine) +void SygusConstraintCommand::invoke(api::Solver* solver) { try { - smtEngine->assertSygusConstraint(d_expr); + solver->addSygusConstraint(d_term); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -809,17 +717,11 @@ void SygusConstraintCommand::invoke(SmtEngine* smtEngine) } } -Expr SygusConstraintCommand::getExpr() const { return d_expr; } - -Command* SygusConstraintCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - return new SygusConstraintCommand(d_expr.exportTo(exprManager, variableMap)); -} +api::Term SygusConstraintCommand::getTerm() const { return d_term; } Command* SygusConstraintCommand::clone() const { - return new SygusConstraintCommand(d_expr); + return new SygusConstraintCommand(d_term); } std::string SygusConstraintCommand::getCommandName() const @@ -833,8 +735,7 @@ void SygusConstraintCommand::toStream(std::ostream& out, size_t dag, OutputLanguage language) const { - Printer::getPrinter(language)->toStreamCmdConstraint(out, - Node::fromExpr(d_expr)); + Printer::getPrinter(language)->toStreamCmdConstraint(out, d_term.getNode()); } /* -------------------------------------------------------------------------- */ @@ -842,24 +743,24 @@ void SygusConstraintCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ SygusInvConstraintCommand::SygusInvConstraintCommand( - const std::vector& predicates) + const std::vector& predicates) : d_predicates(predicates) { } -SygusInvConstraintCommand::SygusInvConstraintCommand(const Expr& inv, - const Expr& pre, - const Expr& trans, - const Expr& post) - : SygusInvConstraintCommand(std::vector{inv, pre, trans, post}) +SygusInvConstraintCommand::SygusInvConstraintCommand(const api::Term& inv, + const api::Term& pre, + const api::Term& trans, + const api::Term& post) + : SygusInvConstraintCommand(std::vector{inv, pre, trans, post}) { } -void SygusInvConstraintCommand::invoke(SmtEngine* smtEngine) +void SygusInvConstraintCommand::invoke(api::Solver* solver) { try { - smtEngine->assertSygusInvConstraint( + solver->addSygusInvConstraint( d_predicates[0], d_predicates[1], d_predicates[2], d_predicates[3]); d_commandStatus = CommandSuccess::instance(); } @@ -869,17 +770,11 @@ void SygusInvConstraintCommand::invoke(SmtEngine* smtEngine) } } -const std::vector& SygusInvConstraintCommand::getPredicates() const +const std::vector& SygusInvConstraintCommand::getPredicates() const { return d_predicates; } -Command* SygusInvConstraintCommand::exportTo( - ExprManager* exprManager, ExprManagerMapCollection& variableMap) -{ - return new SygusInvConstraintCommand(d_predicates); -} - Command* SygusInvConstraintCommand::clone() const { return new SygusInvConstraintCommand(d_predicates); @@ -898,26 +793,25 @@ void SygusInvConstraintCommand::toStream(std::ostream& out, { Printer::getPrinter(language)->toStreamCmdInvConstraint( out, - Node::fromExpr(d_predicates[0]), - Node::fromExpr(d_predicates[1]), - Node::fromExpr(d_predicates[2]), - Node::fromExpr(d_predicates[3])); + d_predicates[0].getNode(), + d_predicates[1].getNode(), + d_predicates[2].getNode(), + d_predicates[3].getNode()); } /* -------------------------------------------------------------------------- */ /* class CheckSynthCommand */ /* -------------------------------------------------------------------------- */ -void CheckSynthCommand::invoke(SmtEngine* smtEngine) +void CheckSynthCommand::invoke(api::Solver* solver) { try { - d_result = smtEngine->checkSynth(); + d_result = solver->checkSynth(); d_commandStatus = CommandSuccess::instance(); - smt::SmtScope scope(smtEngine); d_solution.clear(); // check whether we should print the status - if (d_result.asSatisfiabilityResult() != Result::UNSAT + if (!d_result.isUnsat() || options::sygusOut() == options::SygusSolutionOutMode::STATUS_AND_DEF || options::sygusOut() == options::SygusSolutionOutMode::STATUS) { @@ -931,7 +825,7 @@ void CheckSynthCommand::invoke(SmtEngine* smtEngine) } } // check whether we should print the solution - if (d_result.asSatisfiabilityResult() == Result::UNSAT + if (d_result.isUnsat() && options::sygusOut() != options::SygusSolutionOutMode::STATUS) { // printing a synthesis solution is a non-constant @@ -939,7 +833,7 @@ void CheckSynthCommand::invoke(SmtEngine* smtEngine) // (Figure 5 of Reynolds et al. CAV 2015). // Hence, we must call here print solution here, // instead of during printResult. - smtEngine->printSynthSolution(d_solution); + solver->printSynthSolution(d_solution); } } catch (exception& e) @@ -948,7 +842,7 @@ void CheckSynthCommand::invoke(SmtEngine* smtEngine) } } -Result CheckSynthCommand::getResult() const { return d_result; } +api::Result CheckSynthCommand::getResult() const { return d_result; } void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const { if (!ok()) @@ -961,12 +855,6 @@ void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const } } -Command* CheckSynthCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - return new CheckSynthCommand(); -} - Command* CheckSynthCommand::clone() const { return new CheckSynthCommand(); } std::string CheckSynthCommand::getCommandName() const { return "check-synth"; } @@ -984,11 +872,11 @@ void CheckSynthCommand::toStream(std::ostream& out, /* class ResetCommand */ /* -------------------------------------------------------------------------- */ -void ResetCommand::invoke(SmtEngine* smtEngine) +void ResetCommand::invoke(api::Solver* solver) { try { - smtEngine->reset(); + solver->getSmtEngine()->reset(); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -997,12 +885,6 @@ void ResetCommand::invoke(SmtEngine* smtEngine) } } -Command* ResetCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - return new ResetCommand(); -} - Command* ResetCommand::clone() const { return new ResetCommand(); } std::string ResetCommand::getCommandName() const { return "reset"; } @@ -1019,11 +901,11 @@ void ResetCommand::toStream(std::ostream& out, /* class ResetAssertionsCommand */ /* -------------------------------------------------------------------------- */ -void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) +void ResetAssertionsCommand::invoke(api::Solver* solver) { try { - smtEngine->resetAssertions(); + solver->resetAssertions(); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -1032,12 +914,6 @@ void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) } } -Command* ResetAssertionsCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - return new ResetAssertionsCommand(); -} - Command* ResetAssertionsCommand::clone() const { return new ResetAssertionsCommand(); @@ -1061,18 +937,12 @@ void ResetAssertionsCommand::toStream(std::ostream& out, /* class QuitCommand */ /* -------------------------------------------------------------------------- */ -void QuitCommand::invoke(SmtEngine* smtEngine) +void QuitCommand::invoke(api::Solver* solver) { Dump("benchmark") << *this; d_commandStatus = CommandSuccess::instance(); } -Command* QuitCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - return new QuitCommand(); -} - Command* QuitCommand::clone() const { return new QuitCommand(); } std::string QuitCommand::getCommandName() const { return "exit"; } @@ -1091,18 +961,12 @@ void QuitCommand::toStream(std::ostream& out, CommentCommand::CommentCommand(std::string comment) : d_comment(comment) {} std::string CommentCommand::getComment() const { return d_comment; } -void CommentCommand::invoke(SmtEngine* smtEngine) +void CommentCommand::invoke(api::Solver* solver) { Dump("benchmark") << *this; d_commandStatus = CommandSuccess::instance(); } -Command* CommentCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - return new CommentCommand(d_comment); -} - Command* CommentCommand::clone() const { return new CommentCommand(d_comment); } std::string CommentCommand::getCommandName() const { return "comment"; } @@ -1134,11 +998,11 @@ void CommandSequence::addCommand(Command* cmd) } void CommandSequence::clear() { d_commandSequence.clear(); } -void CommandSequence::invoke(SmtEngine* smtEngine) +void CommandSequence::invoke(api::Solver* solver) { for (; d_index < d_commandSequence.size(); ++d_index) { - d_commandSequence[d_index]->invoke(smtEngine); + d_commandSequence[d_index]->invoke(solver); if (!d_commandSequence[d_index]->ok()) { // abort execution @@ -1152,11 +1016,11 @@ void CommandSequence::invoke(SmtEngine* smtEngine) d_commandStatus = CommandSuccess::instance(); } -void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) +void CommandSequence::invoke(api::Solver* solver, std::ostream& out) { for (; d_index < d_commandSequence.size(); ++d_index) { - d_commandSequence[d_index]->invoke(smtEngine, out); + d_commandSequence[d_index]->invoke(solver, out); if (!d_commandSequence[d_index]->ok()) { // abort execution @@ -1170,21 +1034,6 @@ void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) d_commandStatus = CommandSuccess::instance(); } -Command* CommandSequence::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - CommandSequence* seq = new CommandSequence(); - for (iterator i = begin(); i != end(); ++i) - { - Command* cmd_to_export = *i; - Command* cmd = cmd_to_export->exportTo(exprManager, variableMap); - seq->addCommand(cmd); - Debug("export") << "[export] so far converted: " << seq << endl; - } - seq->d_index = d_index; - return seq; -} - Command* CommandSequence::clone() const { CommandSequence* seq = new CommandSequence(); @@ -1259,18 +1108,18 @@ std::string DeclarationDefinitionCommand::getSymbol() const { return d_symbol; } /* -------------------------------------------------------------------------- */ DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, - Expr func, - Type t) + api::Term func, + api::Sort sort) : DeclarationDefinitionCommand(id), d_func(func), - d_type(t), + d_sort(sort), d_printInModel(true), d_printInModelSetByUser(false) { } -Expr DeclareFunctionCommand::getFunction() const { return d_func; } -Type DeclareFunctionCommand::getType() const { return d_type; } +api::Term DeclareFunctionCommand::getFunction() const { return d_func; } +api::Sort DeclareFunctionCommand::getSort() const { return d_sort; } bool DeclareFunctionCommand::getPrintInModel() const { return d_printInModel; } bool DeclareFunctionCommand::getPrintInModelSetByUser() const { @@ -1283,27 +1132,15 @@ void DeclareFunctionCommand::setPrintInModel(bool p) d_printInModelSetByUser = true; } -void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) +void DeclareFunctionCommand::invoke(api::Solver* solver) { d_commandStatus = CommandSuccess::instance(); } -Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - DeclareFunctionCommand* dfc = - new DeclareFunctionCommand(d_symbol, - d_func.exportTo(exprManager, variableMap), - d_type.exportTo(exprManager, variableMap)); - dfc->d_printInModel = d_printInModel; - dfc->d_printInModelSetByUser = d_printInModelSetByUser; - return dfc; -} - Command* DeclareFunctionCommand::clone() const { DeclareFunctionCommand* dfc = - new DeclareFunctionCommand(d_symbol, d_func, d_type); + new DeclareFunctionCommand(d_symbol, d_func, d_sort); dfc->d_printInModel = d_printInModel; dfc->d_printInModelSetByUser = d_printInModelSetByUser; return dfc; @@ -1321,101 +1158,82 @@ void DeclareFunctionCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdDeclareFunction( - out, d_func.toString(), TypeNode::fromType(d_type)); + out, d_func.toString(), TypeNode::fromType(d_sort.getType())); } /* -------------------------------------------------------------------------- */ -/* class DeclareTypeCommand */ +/* class DeclareSortCommand */ /* -------------------------------------------------------------------------- */ -DeclareTypeCommand::DeclareTypeCommand(const std::string& id, +DeclareSortCommand::DeclareSortCommand(const std::string& id, size_t arity, - Type t) - : DeclarationDefinitionCommand(id), d_arity(arity), d_type(t) + api::Sort sort) + : DeclarationDefinitionCommand(id), d_arity(arity), d_sort(sort) { } -size_t DeclareTypeCommand::getArity() const { return d_arity; } -Type DeclareTypeCommand::getType() const { return d_type; } -void DeclareTypeCommand::invoke(SmtEngine* smtEngine) +size_t DeclareSortCommand::getArity() const { return d_arity; } +api::Sort DeclareSortCommand::getSort() const { return d_sort; } +void DeclareSortCommand::invoke(api::Solver* solver) { d_commandStatus = CommandSuccess::instance(); } -Command* DeclareTypeCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - return new DeclareTypeCommand( - d_symbol, d_arity, d_type.exportTo(exprManager, variableMap)); -} - -Command* DeclareTypeCommand::clone() const +Command* DeclareSortCommand::clone() const { - return new DeclareTypeCommand(d_symbol, d_arity, d_type); + return new DeclareSortCommand(d_symbol, d_arity, d_sort); } -std::string DeclareTypeCommand::getCommandName() const +std::string DeclareSortCommand::getCommandName() const { return "declare-sort"; } -void DeclareTypeCommand::toStream(std::ostream& out, +void DeclareSortCommand::toStream(std::ostream& out, int toDepth, bool types, size_t dag, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdDeclareType( - out, d_type.toString(), d_arity, TypeNode::fromType(d_type)); + out, d_sort.toString(), d_arity, TypeNode::fromType(d_sort.getType())); } /* -------------------------------------------------------------------------- */ -/* class DefineTypeCommand */ +/* class DefineSortCommand */ /* -------------------------------------------------------------------------- */ -DefineTypeCommand::DefineTypeCommand(const std::string& id, Type t) - : DeclarationDefinitionCommand(id), d_params(), d_type(t) +DefineSortCommand::DefineSortCommand(const std::string& id, api::Sort sort) + : DeclarationDefinitionCommand(id), d_params(), d_sort(sort) { } -DefineTypeCommand::DefineTypeCommand(const std::string& id, - const std::vector& params, - Type t) - : DeclarationDefinitionCommand(id), d_params(params), d_type(t) +DefineSortCommand::DefineSortCommand(const std::string& id, + const std::vector& params, + api::Sort sort) + : DeclarationDefinitionCommand(id), d_params(params), d_sort(sort) { } -const std::vector& DefineTypeCommand::getParameters() const +const std::vector& DefineSortCommand::getParameters() const { return d_params; } -Type DefineTypeCommand::getType() const { return d_type; } -void DefineTypeCommand::invoke(SmtEngine* smtEngine) +api::Sort DefineSortCommand::getSort() const { return d_sort; } +void DefineSortCommand::invoke(api::Solver* solver) { d_commandStatus = CommandSuccess::instance(); } -Command* DefineTypeCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - vector params; - transform(d_params.begin(), - d_params.end(), - back_inserter(params), - ExportTransformer(exprManager, variableMap)); - Type type = d_type.exportTo(exprManager, variableMap); - return new DefineTypeCommand(d_symbol, params, type); -} - -Command* DefineTypeCommand::clone() const +Command* DefineSortCommand::clone() const { - return new DefineTypeCommand(d_symbol, d_params, d_type); + return new DefineSortCommand(d_symbol, d_params, d_sort); } -std::string DefineTypeCommand::getCommandName() const { return "define-sort"; } +std::string DefineSortCommand::getCommandName() const { return "define-sort"; } -void DefineTypeCommand::toStream(std::ostream& out, +void DefineSortCommand::toStream(std::ostream& out, int toDepth, bool types, size_t dag, @@ -1424,8 +1242,8 @@ void DefineTypeCommand::toStream(std::ostream& out, Printer::getPrinter(language)->toStreamCmdDefineType( out, d_symbol, - typeVectorToTypeNodes(d_params), - TypeNode::fromType(d_type)); + api::sortVectorToTypeNodes(d_params), + TypeNode::fromType(d_sort.getType())); } /* -------------------------------------------------------------------------- */ @@ -1433,8 +1251,8 @@ void DefineTypeCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ DefineFunctionCommand::DefineFunctionCommand(const std::string& id, - Expr func, - Expr formula, + api::Term func, + api::Term formula, bool global) : DeclarationDefinitionCommand(id), d_func(func), @@ -1444,34 +1262,34 @@ DefineFunctionCommand::DefineFunctionCommand(const std::string& id, { } -DefineFunctionCommand::DefineFunctionCommand(const std::string& id, - Expr func, - const std::vector& formals, - Expr formula, - bool global) +DefineFunctionCommand::DefineFunctionCommand( + const std::string& id, + api::Term func, + const std::vector& formals, + api::Term formula, + bool global) : DeclarationDefinitionCommand(id), d_func(func), d_formals(formals), d_formula(formula), d_global(global) - { } -Expr DefineFunctionCommand::getFunction() const { return d_func; } -const std::vector& DefineFunctionCommand::getFormals() const +api::Term DefineFunctionCommand::getFunction() const { return d_func; } +const std::vector& DefineFunctionCommand::getFormals() const { return d_formals; } -Expr DefineFunctionCommand::getFormula() const { return d_formula; } -void DefineFunctionCommand::invoke(SmtEngine* smtEngine) +api::Term DefineFunctionCommand::getFormula() const { return d_formula; } +void DefineFunctionCommand::invoke(api::Solver* solver) { try { if (!d_func.isNull()) { - smtEngine->defineFunction(d_func, d_formals, d_formula, d_global); + solver->defineFun(d_func, d_formals, d_formula, d_global); } d_commandStatus = CommandSuccess::instance(); } @@ -1481,20 +1299,6 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine) } } -Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - Expr func = d_func.exportTo( - exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED); - vector formals; - transform(d_formals.begin(), - d_formals.end(), - back_inserter(formals), - ExportTransformer(exprManager, variableMap)); - Expr formula = d_formula.exportTo(exprManager, variableMap); - return new DefineFunctionCommand(d_symbol, func, formals, formula, d_global); -} - Command* DefineFunctionCommand::clone() const { return new DefineFunctionCommand( @@ -1515,9 +1319,9 @@ void DefineFunctionCommand::toStream(std::ostream& out, Printer::getPrinter(language)->toStreamCmdDefineFunction( out, d_func.toString(), - exprVectorToNodes(d_formals), - Node::fromExpr(d_func).getType().getRangeType(), - Node::fromExpr(d_formula)); + api::termVectorToNodes(d_formals), + d_func.getNode().getType().getRangeType(), + d_formula.getNode()); } /* -------------------------------------------------------------------------- */ @@ -1525,39 +1329,26 @@ void DefineFunctionCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ DefineNamedFunctionCommand::DefineNamedFunctionCommand( + const std::string& id, - Expr func, - const std::vector& formals, - Expr formula, + api::Term func, + const std::vector& formals, + api::Term formula, bool global) : DefineFunctionCommand(id, func, formals, formula, global) { } -void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) +void DefineNamedFunctionCommand::invoke(api::Solver* solver) { - this->DefineFunctionCommand::invoke(smtEngine); - if (!d_func.isNull() && d_func.getType().isBoolean()) + this->DefineFunctionCommand::invoke(solver); + if (!d_func.isNull() && d_func.getSort().isBoolean()) { - smtEngine->addToAssignment(d_func); + solver->getSmtEngine()->addToAssignment(d_func.getExpr()); } d_commandStatus = CommandSuccess::instance(); } -Command* DefineNamedFunctionCommand::exportTo( - ExprManager* exprManager, ExprManagerMapCollection& variableMap) -{ - Expr func = d_func.exportTo(exprManager, variableMap); - vector formals; - transform(d_formals.begin(), - d_formals.end(), - back_inserter(formals), - ExportTransformer(exprManager, variableMap)); - Expr formula = d_formula.exportTo(exprManager, variableMap); - return new DefineNamedFunctionCommand( - d_symbol, func, formals, formula, d_global); -} - Command* DefineNamedFunctionCommand::clone() const { return new DefineNamedFunctionCommand( @@ -1573,9 +1364,9 @@ void DefineNamedFunctionCommand::toStream(std::ostream& out, Printer::getPrinter(language)->toStreamCmdDefineNamedFunction( out, d_func.toString(), - exprVectorToNodes(d_formals), - Node::fromExpr(d_func).getType().getRangeType(), - Node::fromExpr(d_formula)); + api::termVectorToNodes(d_formals), + TypeNode::fromType(d_func.getSort().getFunctionCodomainSort().getType()), + d_formula.getNode()); } /* -------------------------------------------------------------------------- */ @@ -1583,12 +1374,12 @@ void DefineNamedFunctionCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ DefineFunctionRecCommand::DefineFunctionRecCommand( - const api::Solver* solver, + api::Term func, const std::vector& formals, api::Term formula, bool global) - : Command(solver), d_global(global) + : d_global(global) { d_funcs.push_back(func); d_formals.push_back(formals); @@ -1596,16 +1387,12 @@ DefineFunctionRecCommand::DefineFunctionRecCommand( } DefineFunctionRecCommand::DefineFunctionRecCommand( - const api::Solver* solver, + const std::vector& funcs, const std::vector>& formals, const std::vector& formulas, bool global) - : Command(solver), - d_funcs(funcs), - d_formals(formals), - d_formulas(formulas), - d_global(global) + : d_funcs(funcs), d_formals(formals), d_formulas(formulas), d_global(global) { } @@ -1625,11 +1412,11 @@ const std::vector& DefineFunctionRecCommand::getFormulas() const return d_formulas; } -void DefineFunctionRecCommand::invoke(SmtEngine* smtEngine) +void DefineFunctionRecCommand::invoke(api::Solver* solver) { try { - d_solver->defineFunsRec(d_funcs, d_formals, d_formulas, d_global); + solver->defineFunsRec(d_funcs, d_formals, d_formulas, d_global); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -1638,16 +1425,9 @@ void DefineFunctionRecCommand::invoke(SmtEngine* smtEngine) } } -Command* DefineFunctionRecCommand::exportTo( - ExprManager* exprManager, ExprManagerMapCollection& variableMap) -{ - Unimplemented(); -} - Command* DefineFunctionRecCommand::clone() const { - return new DefineFunctionRecCommand( - d_solver, d_funcs, d_formals, d_formulas, d_global); + return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas, d_global); } std::string DefineFunctionRecCommand::getCommandName() const @@ -1681,42 +1461,45 @@ void DefineFunctionRecCommand::toStream(std::ostream& out, SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, - Expr expr, - const std::vector& expr_values, - const std::string& str_value) - : d_attr(attr), - d_expr(expr), - d_expr_values(expr_values), - d_str_value(str_value) + api::Term term, + const std::vector& termValues, + const std::string& strValue) + : d_attr(attr), d_term(term), d_termValues(termValues), d_strValue(strValue) { } SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr, - Expr expr) - : SetUserAttributeCommand(attr, expr, {}, "") + api::Term term) + : SetUserAttributeCommand(attr, term, {}, "") { } SetUserAttributeCommand::SetUserAttributeCommand( - const std::string& attr, Expr expr, const std::vector& values) - : SetUserAttributeCommand(attr, expr, values, "") + const std::string& attr, + api::Term term, + const std::vector& values) + : SetUserAttributeCommand(attr, term, values, "") { } SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr, - Expr expr, + api::Term term, const std::string& value) - : SetUserAttributeCommand(attr, expr, {}, value) + : SetUserAttributeCommand(attr, term, {}, value) { } -void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) +void SetUserAttributeCommand::invoke(api::Solver* solver) { try { - if (!d_expr.isNull()) + if (!d_term.isNull()) { - smtEngine->setUserAttribute(d_attr, d_expr, d_expr_values, d_str_value); + solver->getSmtEngine()->setUserAttribute( + d_attr, + d_term.getExpr(), + api::termVectorToExprs(d_termValues), + d_strValue); } d_commandStatus = CommandSuccess::instance(); } @@ -1726,17 +1509,9 @@ void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) } } -Command* SetUserAttributeCommand::exportTo( - ExprManager* exprManager, ExprManagerMapCollection& variableMap) -{ - Expr expr = d_expr.exportTo(exprManager, variableMap); - return new SetUserAttributeCommand(d_attr, expr, d_expr_values, d_str_value); -} - Command* SetUserAttributeCommand::clone() const { - return new SetUserAttributeCommand( - d_attr, d_expr, d_expr_values, d_str_value); + return new SetUserAttributeCommand(d_attr, d_term, d_termValues, d_strValue); } std::string SetUserAttributeCommand::getCommandName() const @@ -1751,20 +1526,20 @@ void SetUserAttributeCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdSetUserAttribute( - out, d_attr, Node::fromExpr(d_expr)); + out, d_attr, d_term.getNode()); } /* -------------------------------------------------------------------------- */ /* class SimplifyCommand */ /* -------------------------------------------------------------------------- */ -SimplifyCommand::SimplifyCommand(Expr term) : d_term(term) {} -Expr SimplifyCommand::getTerm() const { return d_term; } -void SimplifyCommand::invoke(SmtEngine* smtEngine) +SimplifyCommand::SimplifyCommand(api::Term term) : d_term(term) {} +api::Term SimplifyCommand::getTerm() const { return d_term; } +void SimplifyCommand::invoke(api::Solver* solver) { try { - d_result = smtEngine->simplify(Node::fromExpr(d_term)).toExpr(); + d_result = solver->simplify(d_term); d_commandStatus = CommandSuccess::instance(); } catch (UnsafeInterruptException& e) @@ -1777,7 +1552,7 @@ void SimplifyCommand::invoke(SmtEngine* smtEngine) } } -Expr SimplifyCommand::getResult() const { return d_result; } +api::Term SimplifyCommand::getResult() const { return d_result; } void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const { if (!ok()) @@ -1790,15 +1565,6 @@ void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const } } -Command* SimplifyCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - SimplifyCommand* c = - new SimplifyCommand(d_term.exportTo(exprManager, variableMap)); - c->d_result = d_result.exportTo(exprManager, variableMap); - return c; -} - Command* SimplifyCommand::clone() const { SimplifyCommand* c = new SimplifyCommand(d_term); @@ -1814,23 +1580,26 @@ void SimplifyCommand::toStream(std::ostream& out, size_t dag, OutputLanguage language) const { - Printer::getPrinter(language)->toStreamCmdSimplify(out, d_term); + Printer::getPrinter(language)->toStreamCmdSimplify(out, d_term.getNode()); } /* -------------------------------------------------------------------------- */ /* class ExpandDefinitionsCommand */ /* -------------------------------------------------------------------------- */ -ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) : d_term(term) {} -Expr ExpandDefinitionsCommand::getTerm() const { return d_term; } -void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) +ExpandDefinitionsCommand::ExpandDefinitionsCommand(api::Term term) + : d_term(term) +{ +} +api::Term ExpandDefinitionsCommand::getTerm() const { return d_term; } +void ExpandDefinitionsCommand::invoke(api::Solver* solver) { - Node t = Node::fromExpr(d_term); - d_result = smtEngine->expandDefinitions(t).toExpr(); + Node t = d_term.getNode(); + d_result = api::Term(solver, solver->getSmtEngine()->expandDefinitions(t)); d_commandStatus = CommandSuccess::instance(); } -Expr ExpandDefinitionsCommand::getResult() const { return d_result; } +api::Term ExpandDefinitionsCommand::getResult() const { return d_result; } void ExpandDefinitionsCommand::printResult(std::ostream& out, uint32_t verbosity) const { @@ -1844,15 +1613,6 @@ void ExpandDefinitionsCommand::printResult(std::ostream& out, } } -Command* ExpandDefinitionsCommand::exportTo( - ExprManager* exprManager, ExprManagerMapCollection& variableMap) -{ - ExpandDefinitionsCommand* c = - new ExpandDefinitionsCommand(d_term.exportTo(exprManager, variableMap)); - c->d_result = d_result.exportTo(exprManager, variableMap); - return c; -} - Command* ExpandDefinitionsCommand::clone() const { ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term); @@ -1871,45 +1631,51 @@ void ExpandDefinitionsCommand::toStream(std::ostream& out, size_t dag, OutputLanguage language) const { - Printer::getPrinter(language)->toStreamCmdExpandDefinitions( - out, Node::fromExpr(d_term)); + Printer::getPrinter(language)->toStreamCmdExpandDefinitions(out, + d_term.getNode()); } /* -------------------------------------------------------------------------- */ /* class GetValueCommand */ /* -------------------------------------------------------------------------- */ -GetValueCommand::GetValueCommand(Expr term) : d_terms() +GetValueCommand::GetValueCommand(api::Term term) : d_terms() { d_terms.push_back(term); } -GetValueCommand::GetValueCommand(const std::vector& terms) +GetValueCommand::GetValueCommand(const std::vector& terms) : d_terms(terms) { PrettyCheckArgument( terms.size() >= 1, terms, "cannot get-value of an empty set of terms"); } -const std::vector& GetValueCommand::getTerms() const { return d_terms; } -void GetValueCommand::invoke(SmtEngine* smtEngine) +const std::vector& GetValueCommand::getTerms() const +{ + return d_terms; +} +void GetValueCommand::invoke(api::Solver* solver) { try { - ExprManager* em = smtEngine->getExprManager(); - NodeManager* nm = NodeManager::fromExprManager(em); - smt::SmtScope scope(smtEngine); - vector result = smtEngine->getValues(d_terms); + NodeManager* nm = solver->getNodeManager(); + smt::SmtScope scope(solver->getSmtEngine()); + std::vector result; + for (const Expr& e : + solver->getSmtEngine()->getValues(api::termVectorToExprs(d_terms))) + { + result.push_back(Node::fromExpr(e)); + } Assert(result.size() == d_terms.size()); for (int i = 0, size = d_terms.size(); i < size; i++) { - Expr e = d_terms[i]; - Node eNode = Node::fromExpr(e); - Assert(nm == NodeManager::fromExprManager(e.getExprManager())); + api::Term t = d_terms[i]; + Node tNode = t.getNode(); Node request = options::expandDefinitions() - ? smtEngine->expandDefinitions(eNode) - : eNode; - Node value = Node::fromExpr(result[i]); + ? solver->getSmtEngine()->expandDefinitions(tNode) + : tNode; + Node value = result[i]; if (value.getType().isInteger() && request.getType() == nm->realType()) { // Need to wrap in division-by-one so that output printers know this @@ -1917,9 +1683,9 @@ void GetValueCommand::invoke(SmtEngine* smtEngine) // a rational. Necessary for SMT-LIB standards compliance. value = nm->mkNode(kind::DIVISION, value, nm->mkConst(Rational(1))); } - result[i] = nm->mkNode(kind::SEXPR, request, value).toExpr(); + result[i] = nm->mkNode(kind::SEXPR, request, value); } - d_result = em->mkExpr(kind::SEXPR, result); + d_result = api::Term(solver, nm->mkNode(kind::SEXPR, result)); d_commandStatus = CommandSuccess::instance(); } catch (RecoverableModalException& e) @@ -1936,7 +1702,7 @@ void GetValueCommand::invoke(SmtEngine* smtEngine) } } -Expr GetValueCommand::getResult() const { return d_result; } +api::Term GetValueCommand::getResult() const { return d_result; } void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const { if (!ok()) @@ -1950,21 +1716,6 @@ void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const } } -Command* GetValueCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - vector exportedTerms; - for (std::vector::const_iterator i = d_terms.begin(); - i != d_terms.end(); - ++i) - { - exportedTerms.push_back((*i).exportTo(exprManager, variableMap)); - } - GetValueCommand* c = new GetValueCommand(exportedTerms); - c->d_result = d_result.exportTo(exprManager, variableMap); - return c; -} - Command* GetValueCommand::clone() const { GetValueCommand* c = new GetValueCommand(d_terms); @@ -1981,7 +1732,7 @@ void GetValueCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdGetValue( - out, exprVectorToNodes(d_terms)); + out, api::termVectorToNodes(d_terms)); } /* -------------------------------------------------------------------------- */ @@ -1989,11 +1740,12 @@ void GetValueCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetAssignmentCommand::GetAssignmentCommand() {} -void GetAssignmentCommand::invoke(SmtEngine* smtEngine) +void GetAssignmentCommand::invoke(api::Solver* solver) { try { - std::vector> assignments = smtEngine->getAssignment(); + std::vector> assignments = + solver->getSmtEngine()->getAssignment(); vector sexprs; for (const auto& p : assignments) { @@ -2033,14 +1785,6 @@ void GetAssignmentCommand::printResult(std::ostream& out, } } -Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - GetAssignmentCommand* c = new GetAssignmentCommand(); - c->d_result = d_result; - return c; -} - Command* GetAssignmentCommand::clone() const { GetAssignmentCommand* c = new GetAssignmentCommand(); @@ -2067,12 +1811,12 @@ void GetAssignmentCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetModelCommand::GetModelCommand() : d_result(nullptr), d_smtEngine(nullptr) {} -void GetModelCommand::invoke(SmtEngine* smtEngine) +void GetModelCommand::invoke(api::Solver* solver) { try { - d_result = smtEngine->getModel(); - d_smtEngine = smtEngine; + d_result = solver->getSmtEngine()->getModel(); + d_smtEngine = solver->getSmtEngine(); d_commandStatus = CommandSuccess::instance(); } catch (RecoverableModalException& e) @@ -2107,15 +1851,6 @@ void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const } } -Command* GetModelCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - GetModelCommand* c = new GetModelCommand(); - c->d_result = d_result; - c->d_smtEngine = d_smtEngine; - return c; -} - Command* GetModelCommand::clone() const { GetModelCommand* c = new GetModelCommand(); @@ -2140,11 +1875,11 @@ void GetModelCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ BlockModelCommand::BlockModelCommand() {} -void BlockModelCommand::invoke(SmtEngine* smtEngine) +void BlockModelCommand::invoke(api::Solver* solver) { try { - smtEngine->blockModel(); + solver->getSmtEngine()->blockModel(); d_commandStatus = CommandSuccess::instance(); } catch (RecoverableModalException& e) @@ -2161,13 +1896,6 @@ void BlockModelCommand::invoke(SmtEngine* smtEngine) } } -Command* BlockModelCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - BlockModelCommand* c = new BlockModelCommand(); - return c; -} - Command* BlockModelCommand::clone() const { BlockModelCommand* c = new BlockModelCommand(); @@ -2189,7 +1917,8 @@ void BlockModelCommand::toStream(std::ostream& out, /* class BlockModelValuesCommand */ /* -------------------------------------------------------------------------- */ -BlockModelValuesCommand::BlockModelValuesCommand(const std::vector& terms) +BlockModelValuesCommand::BlockModelValuesCommand( + const std::vector& terms) : d_terms(terms) { PrettyCheckArgument(terms.size() >= 1, @@ -2197,15 +1926,15 @@ BlockModelValuesCommand::BlockModelValuesCommand(const std::vector& terms) "cannot block-model-values of an empty set of terms"); } -const std::vector& BlockModelValuesCommand::getTerms() const +const std::vector& BlockModelValuesCommand::getTerms() const { return d_terms; } -void BlockModelValuesCommand::invoke(SmtEngine* smtEngine) +void BlockModelValuesCommand::invoke(api::Solver* solver) { try { - smtEngine->blockModelValues(d_terms); + solver->getSmtEngine()->blockModelValues(api::termVectorToExprs(d_terms)); d_commandStatus = CommandSuccess::instance(); } catch (RecoverableModalException& e) @@ -2222,20 +1951,6 @@ void BlockModelValuesCommand::invoke(SmtEngine* smtEngine) } } -Command* BlockModelValuesCommand::exportTo( - ExprManager* exprManager, ExprManagerMapCollection& variableMap) -{ - vector exportedTerms; - for (std::vector::const_iterator i = d_terms.begin(); - i != d_terms.end(); - ++i) - { - exportedTerms.push_back((*i).exportTo(exprManager, variableMap)); - } - BlockModelValuesCommand* c = new BlockModelValuesCommand(exportedTerms); - return c; -} - Command* BlockModelValuesCommand::clone() const { BlockModelValuesCommand* c = new BlockModelValuesCommand(d_terms); @@ -2254,7 +1969,7 @@ void BlockModelValuesCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdBlockModelValues( - out, exprVectorToNodes(d_terms)); + out, api::termVectorToNodes(d_terms)); } /* -------------------------------------------------------------------------- */ @@ -2262,18 +1977,11 @@ void BlockModelValuesCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetProofCommand::GetProofCommand() {} -void GetProofCommand::invoke(SmtEngine* smtEngine) +void GetProofCommand::invoke(api::Solver* solver) { Unimplemented() << "Unimplemented get-proof\n"; } -Command* GetProofCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - GetProofCommand* c = new GetProofCommand(); - return c; -} - Command* GetProofCommand::clone() const { GetProofCommand* c = new GetProofCommand(); @@ -2296,11 +2004,11 @@ void GetProofCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetInstantiationsCommand::GetInstantiationsCommand() : d_smtEngine(nullptr) {} -void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) +void GetInstantiationsCommand::invoke(api::Solver* solver) { try { - d_smtEngine = smtEngine; + d_smtEngine = solver->getSmtEngine(); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -2322,15 +2030,6 @@ void GetInstantiationsCommand::printResult(std::ostream& out, } } -Command* GetInstantiationsCommand::exportTo( - ExprManager* exprManager, ExprManagerMapCollection& variableMap) -{ - GetInstantiationsCommand* c = new GetInstantiationsCommand(); - // c->d_result = d_result; - c->d_smtEngine = d_smtEngine; - return c; -} - Command* GetInstantiationsCommand::clone() const { GetInstantiationsCommand* c = new GetInstantiationsCommand(); @@ -2358,11 +2057,11 @@ void GetInstantiationsCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetSynthSolutionCommand::GetSynthSolutionCommand() : d_smtEngine(nullptr) {} -void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) +void GetSynthSolutionCommand::invoke(api::Solver* solver) { try { - d_smtEngine = smtEngine; + d_smtEngine = solver->getSmtEngine(); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -2384,14 +2083,6 @@ void GetSynthSolutionCommand::printResult(std::ostream& out, } } -Command* GetSynthSolutionCommand::exportTo( - ExprManager* exprManager, ExprManagerMapCollection& variableMap) -{ - GetSynthSolutionCommand* c = new GetSynthSolutionCommand(); - c->d_smtEngine = d_smtEngine; - return c; -} - Command* GetSynthSolutionCommand::clone() const { GetSynthSolutionCommand* c = new GetSynthSolutionCommand(); @@ -2417,21 +2108,14 @@ void GetSynthSolutionCommand::toStream(std::ostream& out, /* class GetInterpolCommand */ /* -------------------------------------------------------------------------- */ -GetInterpolCommand::GetInterpolCommand(const api::Solver* solver, - const std::string& name, - api::Term conj) - : Command(solver), d_name(name), d_conj(conj), d_resultStatus(false) +GetInterpolCommand::GetInterpolCommand(const std::string& name, api::Term conj) + : d_name(name), d_conj(conj), d_resultStatus(false) { } -GetInterpolCommand::GetInterpolCommand(const api::Solver* solver, - const std::string& name, +GetInterpolCommand::GetInterpolCommand(const std::string& name, api::Term conj, api::Grammar* g) - : Command(solver), - d_name(name), - d_conj(conj), - d_sygus_grammar(g), - d_resultStatus(false) + : d_name(name), d_conj(conj), d_sygus_grammar(g), d_resultStatus(false) { } @@ -2444,18 +2128,18 @@ const api::Grammar* GetInterpolCommand::getGrammar() const api::Term GetInterpolCommand::getResult() const { return d_result; } -void GetInterpolCommand::invoke(SmtEngine* smtEngine) +void GetInterpolCommand::invoke(api::Solver* solver) { try { - if (!d_sygus_grammar) + if (d_sygus_grammar == nullptr) { - d_resultStatus = d_solver->getInterpolant(d_conj, d_result); + d_resultStatus = solver->getInterpolant(d_conj, d_result); } else { d_resultStatus = - d_solver->getInterpolant(d_conj, *d_sygus_grammar, d_result); + solver->getInterpolant(d_conj, *d_sygus_grammar, d_result); } d_commandStatus = CommandSuccess::instance(); } @@ -2487,16 +2171,10 @@ void GetInterpolCommand::printResult(std::ostream& out, } } -Command* GetInterpolCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - Unimplemented(); -} - Command* GetInterpolCommand::clone() const { GetInterpolCommand* c = - new GetInterpolCommand(d_solver, d_name, d_conj, d_sygus_grammar); + new GetInterpolCommand(d_name, d_conj, d_sygus_grammar); c->d_result = d_result; c->d_resultStatus = d_resultStatus; return c; @@ -2524,21 +2202,14 @@ void GetInterpolCommand::toStream(std::ostream& out, /* class GetAbductCommand */ /* -------------------------------------------------------------------------- */ -GetAbductCommand::GetAbductCommand(const api::Solver* solver, - const std::string& name, - api::Term conj) - : Command(solver), d_name(name), d_conj(conj), d_resultStatus(false) +GetAbductCommand::GetAbductCommand(const std::string& name, api::Term conj) + : d_name(name), d_conj(conj), d_resultStatus(false) { } -GetAbductCommand::GetAbductCommand(const api::Solver* solver, - const std::string& name, +GetAbductCommand::GetAbductCommand(const std::string& name, api::Term conj, api::Grammar* g) - : Command(solver), - d_name(name), - d_conj(conj), - d_sygus_grammar(g), - d_resultStatus(false) + : d_name(name), d_conj(conj), d_sygus_grammar(g), d_resultStatus(false) { } @@ -2552,17 +2223,17 @@ const api::Grammar* GetAbductCommand::getGrammar() const std::string GetAbductCommand::getAbductName() const { return d_name; } api::Term GetAbductCommand::getResult() const { return d_result; } -void GetAbductCommand::invoke(SmtEngine* smtEngine) +void GetAbductCommand::invoke(api::Solver* solver) { try { - if (!d_sygus_grammar) + if (d_sygus_grammar == nullptr) { - d_resultStatus = d_solver->getAbduct(d_conj, d_result); + d_resultStatus = solver->getAbduct(d_conj, d_result); } else { - d_resultStatus = d_solver->getAbduct(d_conj, *d_sygus_grammar, d_result); + d_resultStatus = solver->getAbduct(d_conj, *d_sygus_grammar, d_result); } d_commandStatus = CommandSuccess::instance(); } @@ -2593,16 +2264,9 @@ void GetAbductCommand::printResult(std::ostream& out, uint32_t verbosity) const } } -Command* GetAbductCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - Unimplemented(); -} - Command* GetAbductCommand::clone() const { - GetAbductCommand* c = - new GetAbductCommand(d_solver, d_name, d_conj, d_sygus_grammar); + GetAbductCommand* c = new GetAbductCommand(d_name, d_conj, d_sygus_grammar); c->d_result = d_result; c->d_resultStatus = d_resultStatus; return c; @@ -2628,24 +2292,24 @@ void GetAbductCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetQuantifierEliminationCommand::GetQuantifierEliminationCommand() - : d_expr(), d_doFull(true) + : d_term(), d_doFull(true) { } GetQuantifierEliminationCommand::GetQuantifierEliminationCommand( - const Expr& expr, bool doFull) - : d_expr(expr), d_doFull(doFull) + const api::Term& term, bool doFull) + : d_term(term), d_doFull(doFull) { } -Expr GetQuantifierEliminationCommand::getExpr() const { return d_expr; } +api::Term GetQuantifierEliminationCommand::getTerm() const { return d_term; } bool GetQuantifierEliminationCommand::getDoFull() const { return d_doFull; } -void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine) +void GetQuantifierEliminationCommand::invoke(api::Solver* solver) { try { - d_result = - smtEngine->getQuantifierElimination(Node::fromExpr(d_expr), d_doFull) - .toExpr(); + d_result = api::Term(solver, + solver->getSmtEngine()->getQuantifierElimination( + d_term.getNode(), d_doFull)); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -2654,7 +2318,10 @@ void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine) } } -Expr GetQuantifierEliminationCommand::getResult() const { return d_result; } +api::Term GetQuantifierEliminationCommand::getResult() const +{ + return d_result; +} void GetQuantifierEliminationCommand::printResult(std::ostream& out, uint32_t verbosity) const { @@ -2668,19 +2335,10 @@ void GetQuantifierEliminationCommand::printResult(std::ostream& out, } } -Command* GetQuantifierEliminationCommand::exportTo( - ExprManager* exprManager, ExprManagerMapCollection& variableMap) -{ - GetQuantifierEliminationCommand* c = new GetQuantifierEliminationCommand( - d_expr.exportTo(exprManager, variableMap), d_doFull); - c->d_result = d_result; - return c; -} - Command* GetQuantifierEliminationCommand::clone() const { GetQuantifierEliminationCommand* c = - new GetQuantifierEliminationCommand(d_expr, d_doFull); + new GetQuantifierEliminationCommand(d_term, d_doFull); c->d_result = d_result; return c; } @@ -2697,7 +2355,7 @@ void GetQuantifierEliminationCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdGetQuantifierElimination( - out, Node::fromExpr(d_expr)); + out, d_term.getNode()); } /* -------------------------------------------------------------------------- */ @@ -2706,16 +2364,11 @@ void GetQuantifierEliminationCommand::toStream(std::ostream& out, GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {} -void GetUnsatAssumptionsCommand::invoke(SmtEngine* smtEngine) +void GetUnsatAssumptionsCommand::invoke(api::Solver* solver) { try { - std::vector uassumps = smtEngine->getUnsatAssumptions(); - d_result.clear(); - for (const Node& n : uassumps) - { - d_result.push_back(n.toExpr()); - } + d_result = solver->getUnsatAssumptions(); d_commandStatus = CommandSuccess::instance(); } catch (RecoverableModalException& e) @@ -2728,7 +2381,7 @@ void GetUnsatAssumptionsCommand::invoke(SmtEngine* smtEngine) } } -std::vector GetUnsatAssumptionsCommand::getResult() const +std::vector GetUnsatAssumptionsCommand::getResult() const { return d_result; } @@ -2746,14 +2399,6 @@ void GetUnsatAssumptionsCommand::printResult(std::ostream& out, } } -Command* GetUnsatAssumptionsCommand::exportTo( - ExprManager* exprManager, ExprManagerMapCollection& variableMap) -{ - GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand; - c->d_result = d_result; - return c; -} - Command* GetUnsatAssumptionsCommand::clone() const { GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand; @@ -2780,11 +2425,11 @@ void GetUnsatAssumptionsCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetUnsatCoreCommand::GetUnsatCoreCommand() {} -void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) +void GetUnsatCoreCommand::invoke(api::Solver* solver) { try { - d_result = smtEngine->getUnsatCore(); + d_result = solver->getSmtEngine()->getUnsatCore(); d_commandStatus = CommandSuccess::instance(); } catch (RecoverableModalException& e) @@ -2816,14 +2461,6 @@ const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const return d_result; } -Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - GetUnsatCoreCommand* c = new GetUnsatCoreCommand; - c->d_result = d_result; - return c; -} - Command* GetUnsatCoreCommand::clone() const { GetUnsatCoreCommand* c = new GetUnsatCoreCommand; @@ -2850,14 +2487,14 @@ void GetUnsatCoreCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetAssertionsCommand::GetAssertionsCommand() {} -void GetAssertionsCommand::invoke(SmtEngine* smtEngine) +void GetAssertionsCommand::invoke(api::Solver* solver) { try { stringstream ss; - const vector v = smtEngine->getAssertions(); + const vector v = solver->getAssertions(); ss << "(\n"; - copy(v.begin(), v.end(), ostream_iterator(ss, "\n")); + copy(v.begin(), v.end(), ostream_iterator(ss, "\n")); ss << ")\n"; d_result = ss.str(); d_commandStatus = CommandSuccess::instance(); @@ -2882,14 +2519,6 @@ void GetAssertionsCommand::printResult(std::ostream& out, } } -Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - GetAssertionsCommand* c = new GetAssertionsCommand(); - c->d_result = d_result; - return c; -} - Command* GetAssertionsCommand::clone() const { GetAssertionsCommand* c = new GetAssertionsCommand(); @@ -2925,14 +2554,13 @@ BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const return d_status; } -void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) +void SetBenchmarkStatusCommand::invoke(api::Solver* solver) { try { stringstream ss; ss << d_status; - SExpr status = SExpr(ss.str()); - smtEngine->setInfo("status", status); + solver->setInfo("status", ss.str()); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -2941,12 +2569,6 @@ void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) } } -Command* SetBenchmarkStatusCommand::exportTo( - ExprManager* exprManager, ExprManagerMapCollection& variableMap) -{ - return new SetBenchmarkStatusCommand(d_status); -} - Command* SetBenchmarkStatusCommand::clone() const { return new SetBenchmarkStatusCommand(d_status); @@ -2984,11 +2606,11 @@ SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) } std::string SetBenchmarkLogicCommand::getLogic() const { return d_logic; } -void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) +void SetBenchmarkLogicCommand::invoke(api::Solver* solver) { try { - smtEngine->setLogic(d_logic); + solver->setLogic(d_logic); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -2997,12 +2619,6 @@ void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) } } -Command* SetBenchmarkLogicCommand::exportTo( - ExprManager* exprManager, ExprManagerMapCollection& variableMap) -{ - return new SetBenchmarkLogicCommand(d_logic); -} - Command* SetBenchmarkLogicCommand::clone() const { return new SetBenchmarkLogicCommand(d_logic); @@ -3033,11 +2649,11 @@ SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) std::string SetInfoCommand::getFlag() const { return d_flag; } SExpr SetInfoCommand::getSExpr() const { return d_sexpr; } -void SetInfoCommand::invoke(SmtEngine* smtEngine) +void SetInfoCommand::invoke(api::Solver* solver) { try { - smtEngine->setInfo(d_flag, d_sexpr); + solver->getSmtEngine()->setInfo(d_flag, d_sexpr); d_commandStatus = CommandSuccess::instance(); } catch (UnrecognizedOptionException&) @@ -3051,12 +2667,6 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) } } -Command* SetInfoCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - return new SetInfoCommand(d_flag, d_sexpr); -} - Command* SetInfoCommand::clone() const { return new SetInfoCommand(d_flag, d_sexpr); @@ -3079,13 +2689,13 @@ void SetInfoCommand::toStream(std::ostream& out, GetInfoCommand::GetInfoCommand(std::string flag) : d_flag(flag) {} std::string GetInfoCommand::getFlag() const { return d_flag; } -void GetInfoCommand::invoke(SmtEngine* smtEngine) +void GetInfoCommand::invoke(api::Solver* solver) { try { vector v; v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag))); - v.push_back(smtEngine->getInfo(d_flag)); + v.emplace_back(solver->getSmtEngine()->getInfo(d_flag)); stringstream ss; if (d_flag == "all-options" || d_flag == "all-statistics") { @@ -3122,14 +2732,6 @@ void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const } } -Command* GetInfoCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - GetInfoCommand* c = new GetInfoCommand(d_flag); - c->d_result = d_result; - return c; -} - Command* GetInfoCommand::clone() const { GetInfoCommand* c = new GetInfoCommand(d_flag); @@ -3159,11 +2761,11 @@ SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) std::string SetOptionCommand::getFlag() const { return d_flag; } SExpr SetOptionCommand::getSExpr() const { return d_sexpr; } -void SetOptionCommand::invoke(SmtEngine* smtEngine) +void SetOptionCommand::invoke(api::Solver* solver) { try { - smtEngine->setOption(d_flag, d_sexpr); + solver->getSmtEngine()->setOption(d_flag, d_sexpr); d_commandStatus = CommandSuccess::instance(); } catch (UnrecognizedOptionException&) @@ -3176,12 +2778,6 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) } } -Command* SetOptionCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - return new SetOptionCommand(d_flag, d_sexpr); -} - Command* SetOptionCommand::clone() const { return new SetOptionCommand(d_flag, d_sexpr); @@ -3204,12 +2800,11 @@ void SetOptionCommand::toStream(std::ostream& out, GetOptionCommand::GetOptionCommand(std::string flag) : d_flag(flag) {} std::string GetOptionCommand::getFlag() const { return d_flag; } -void GetOptionCommand::invoke(SmtEngine* smtEngine) +void GetOptionCommand::invoke(api::Solver* solver) { try { - SExpr res = smtEngine->getOption(d_flag); - d_result = res.toString(); + d_result = solver->getOption(d_flag); d_commandStatus = CommandSuccess::instance(); } catch (UnrecognizedOptionException&) @@ -3235,14 +2830,6 @@ void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const } } -Command* GetOptionCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - GetOptionCommand* c = new GetOptionCommand(d_flag); - c->d_result = d_result; - return c; -} - Command* GetOptionCommand::clone() const { GetOptionCommand* c = new GetOptionCommand(d_flag); @@ -3265,28 +2852,21 @@ void GetOptionCommand::toStream(std::ostream& out, /* class SetExpressionNameCommand */ /* -------------------------------------------------------------------------- */ -SetExpressionNameCommand::SetExpressionNameCommand(Expr expr, std::string name) - : d_expr(expr), d_name(name) +SetExpressionNameCommand::SetExpressionNameCommand(api::Term term, + std::string name) + : d_term(term), d_name(name) { } -void SetExpressionNameCommand::invoke(SmtEngine* smtEngine) +void SetExpressionNameCommand::invoke(api::Solver* solver) { - smtEngine->setExpressionName(d_expr, d_name); + solver->getSmtEngine()->setExpressionName(d_term.getExpr(), d_name); d_commandStatus = CommandSuccess::instance(); } -Command* SetExpressionNameCommand::exportTo( - ExprManager* exprManager, ExprManagerMapCollection& variableMap) -{ - SetExpressionNameCommand* c = new SetExpressionNameCommand( - d_expr.exportTo(exprManager, variableMap), d_name); - return c; -} - Command* SetExpressionNameCommand::clone() const { - SetExpressionNameCommand* c = new SetExpressionNameCommand(d_expr, d_name); + SetExpressionNameCommand* c = new SetExpressionNameCommand(d_term, d_name); return c; } @@ -3302,42 +2882,36 @@ void SetExpressionNameCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdSetExpressionName( - out, Node::fromExpr(d_expr), d_name); + out, d_term.getNode(), d_name); } /* -------------------------------------------------------------------------- */ /* class DatatypeDeclarationCommand */ /* -------------------------------------------------------------------------- */ -DatatypeDeclarationCommand::DatatypeDeclarationCommand(const Type& datatype) +DatatypeDeclarationCommand::DatatypeDeclarationCommand( + const api::Sort& datatype) : d_datatypes() { d_datatypes.push_back(datatype); } DatatypeDeclarationCommand::DatatypeDeclarationCommand( - const std::vector& datatypes) + const std::vector& datatypes) : d_datatypes(datatypes) { } -const std::vector& DatatypeDeclarationCommand::getDatatypes() const +const std::vector& DatatypeDeclarationCommand::getDatatypes() const { return d_datatypes; } -void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) +void DatatypeDeclarationCommand::invoke(api::Solver* solver) { d_commandStatus = CommandSuccess::instance(); } -Command* DatatypeDeclarationCommand::exportTo( - ExprManager* exprManager, ExprManagerMapCollection& variableMap) -{ - throw ExportUnsupportedException( - "export of DatatypeDeclarationCommand unsupported"); -} - Command* DatatypeDeclarationCommand::clone() const { return new DatatypeDeclarationCommand(d_datatypes); @@ -3355,7 +2929,7 @@ void DatatypeDeclarationCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration( - out, typeVectorToTypeNodes(d_datatypes)); + out, api::sortVectorToTypeNodes(d_datatypes)); } } // namespace CVC4 diff --git a/src/smt/command.h b/src/smt/command.h index 40853d323..32cf70602 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -200,8 +200,8 @@ class CVC4_PUBLIC Command virtual ~Command(); - virtual void invoke(SmtEngine* smtEngine) = 0; - virtual void invoke(SmtEngine* smtEngine, std::ostream& out); + virtual void invoke(api::Solver* solver) = 0; + virtual void invoke(api::Solver* solver, std::ostream& out); virtual void toStream( std::ostream& out, @@ -243,38 +243,11 @@ class CVC4_PUBLIC Command const CommandStatus* getCommandStatus() const { return d_commandStatus; } virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const; - /** - * Maps this Command into one for a different ExprManager, using - * variableMap for the translation and extending it with any new - * mappings. - */ - virtual Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) = 0; - /** * Clone this Command (make a shallow copy). */ virtual Command* clone() const = 0; - protected: - class ExportTransformer - { - ExprManager* d_exprManager; - ExprManagerMapCollection& d_variableMap; - - public: - ExportTransformer(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) - : d_exprManager(exprManager), d_variableMap(variableMap) - { - } - 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. */ - const 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 @@ -301,9 +274,7 @@ class CVC4_PUBLIC EmptyCommand : public Command public: EmptyCommand(std::string name = ""); std::string getName() const; - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -324,10 +295,9 @@ class CVC4_PUBLIC EchoCommand : public Command std::string getOutput() const; - void invoke(SmtEngine* smtEngine) override; - void invoke(SmtEngine* smtEngine, std::ostream& out) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, std::ostream& out) override; + Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -344,17 +314,16 @@ class CVC4_PUBLIC EchoCommand : public Command class CVC4_PUBLIC AssertCommand : public Command { protected: - Expr d_expr; + api::Term d_term; bool d_inUnsatCore; public: - AssertCommand(const Expr& e, bool inUnsatCore = true); + AssertCommand(const api::Term& t, bool inUnsatCore = true); - Expr getExpr() const; + api::Term getTerm() const; + + void invoke(api::Solver* solver) override; - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -368,9 +337,7 @@ class CVC4_PUBLIC AssertCommand : public Command class CVC4_PUBLIC PushCommand : public Command { public: - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -384,9 +351,7 @@ class CVC4_PUBLIC PushCommand : public Command class CVC4_PUBLIC PopCommand : public Command { public: - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -405,29 +370,27 @@ class CVC4_PUBLIC DeclarationDefinitionCommand : public Command public: DeclarationDefinitionCommand(const std::string& id); - void invoke(SmtEngine* smtEngine) override = 0; + void invoke(api::Solver* solver) override = 0; std::string getSymbol() const; }; /* class DeclarationDefinitionCommand */ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand { protected: - Expr d_func; - Type d_type; + api::Term d_func; + api::Sort d_sort; bool d_printInModel; bool d_printInModelSetByUser; public: - DeclareFunctionCommand(const std::string& id, Expr func, Type type); - Expr getFunction() const; - Type getType() const; + DeclareFunctionCommand(const std::string& id, api::Term func, api::Sort sort); + api::Term getFunction() const; + api::Sort getSort() const; bool getPrintInModel() const; bool getPrintInModelSetByUser() const; void setPrintInModel(bool p); - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -438,21 +401,19 @@ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DeclareFunctionCommand */ -class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand +class CVC4_PUBLIC DeclareSortCommand : public DeclarationDefinitionCommand { protected: size_t d_arity; - Type d_type; + api::Sort d_sort; public: - DeclareTypeCommand(const std::string& id, size_t arity, Type t); + DeclareSortCommand(const std::string& id, size_t arity, api::Sort sort); size_t getArity() const; - Type getType() const; + api::Sort getSort() const; - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -461,26 +422,24 @@ class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand bool types = false, size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; -}; /* class DeclareTypeCommand */ +}; /* class DeclareSortCommand */ -class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand +class CVC4_PUBLIC DefineSortCommand : public DeclarationDefinitionCommand { protected: - std::vector d_params; - Type d_type; + std::vector d_params; + api::Sort d_sort; public: - DefineTypeCommand(const std::string& id, Type t); - DefineTypeCommand(const std::string& id, - const std::vector& params, - Type t); + DefineSortCommand(const std::string& id, api::Sort sort); + DefineSortCommand(const std::string& id, + const std::vector& params, + api::Sort sort); - const std::vector& getParameters() const; - Type getType() const; + const std::vector& getParameters() const; + api::Sort getSort() const; - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -489,28 +448,26 @@ class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand bool types = false, size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; -}; /* class DefineTypeCommand */ +}; /* class DefineSortCommand */ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand { public: DefineFunctionCommand(const std::string& id, - Expr func, - Expr formula, + api::Term func, + api::Term formula, bool global); DefineFunctionCommand(const std::string& id, - Expr func, - const std::vector& formals, - Expr formula, + api::Term func, + const std::vector& formals, + api::Term formula, bool global); - Expr getFunction() const; - const std::vector& getFormals() const; - Expr getFormula() const; + api::Term getFunction() const; + const std::vector& getFormals() const; + api::Term getFormula() const; - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -522,11 +479,11 @@ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand protected: /** The function we are defining */ - Expr d_func; + api::Term d_func; /** The formal arguments for the function we are defining */ - std::vector d_formals; + std::vector d_formals; /** The formula corresponding to the body of the function we are defining */ - Expr d_formula; + api::Term d_formula; /** * Stores whether this definition is global (i.e. should persist when * popping the user context. @@ -543,13 +500,11 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand { public: DefineNamedFunctionCommand(const std::string& id, - Expr func, - const std::vector& formals, - Expr formula, + api::Term func, + const std::vector& formals, + api::Term formula, bool global); - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; void toStream( std::ostream& out, @@ -567,13 +522,11 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand class CVC4_PUBLIC DefineFunctionRecCommand : public Command { public: - DefineFunctionRecCommand(const api::Solver* solver, - api::Term func, + DefineFunctionRecCommand(api::Term func, const std::vector& formals, api::Term formula, bool global); - DefineFunctionRecCommand(const api::Solver* solver, - const std::vector& funcs, + DefineFunctionRecCommand(const std::vector& funcs, const std::vector >& formals, const std::vector& formula, bool global); @@ -582,9 +535,7 @@ class CVC4_PUBLIC DefineFunctionRecCommand : public Command const std::vector >& getFormals() const; const std::vector& getFormulas() const; - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -615,17 +566,15 @@ class CVC4_PUBLIC DefineFunctionRecCommand : public Command class CVC4_PUBLIC SetUserAttributeCommand : public Command { public: - SetUserAttributeCommand(const std::string& attr, Expr expr); + SetUserAttributeCommand(const std::string& attr, api::Term term); SetUserAttributeCommand(const std::string& attr, - Expr expr, - const std::vector& values); + api::Term term, + const std::vector& values); SetUserAttributeCommand(const std::string& attr, - Expr expr, + api::Term term, const std::string& value); - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -637,14 +586,14 @@ class CVC4_PUBLIC SetUserAttributeCommand : public Command private: SetUserAttributeCommand(const std::string& attr, - Expr expr, - const std::vector& expr_values, - const std::string& str_value); + api::Term term, + const std::vector& termValues, + const std::string& strValue); const std::string d_attr; - const Expr d_expr; - const std::vector d_expr_values; - const std::string d_str_value; + const api::Term d_term; + const std::vector d_termValues; + const std::string d_strValue; }; /* class SetUserAttributeCommand */ /** @@ -655,14 +604,12 @@ class CVC4_PUBLIC CheckSatCommand : public Command { public: CheckSatCommand(); - CheckSatCommand(const Expr& expr); + CheckSatCommand(const api::Term& term); - Expr getExpr() const; - Result getResult() const; - void invoke(SmtEngine* smtEngine) override; + api::Term getTerm() const; + api::Result getResult() const; + void invoke(api::Solver* solver) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -673,8 +620,8 @@ class CVC4_PUBLIC CheckSatCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; private: - Expr d_expr; - Result d_result; + api::Term d_term; + api::Result d_result; }; /* class CheckSatCommand */ /** @@ -685,15 +632,13 @@ class CVC4_PUBLIC CheckSatCommand : public Command class CVC4_PUBLIC CheckSatAssumingCommand : public Command { public: - CheckSatAssumingCommand(Expr term); - CheckSatAssumingCommand(const std::vector& terms); + CheckSatAssumingCommand(api::Term term); + CheckSatAssumingCommand(const std::vector& terms); - const std::vector& getTerms() const; - Result getResult() const; - void invoke(SmtEngine* smtEngine) override; + const std::vector& getTerms() const; + api::Result getResult() const; + void invoke(api::Solver* solver) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -704,26 +649,24 @@ class CVC4_PUBLIC CheckSatAssumingCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; private: - std::vector d_terms; - Result d_result; + std::vector d_terms; + api::Result d_result; }; /* class CheckSatAssumingCommand */ class CVC4_PUBLIC QueryCommand : public Command { protected: - Expr d_expr; - Result d_result; + api::Term d_term; + api::Result d_result; bool d_inUnsatCore; public: - QueryCommand(const Expr& e, bool inUnsatCore = true); + QueryCommand(const api::Term& t, bool inUnsatCore = true); - Expr getExpr() const; - Result getResult() const; - void invoke(SmtEngine* smtEngine) override; + api::Term getTerm() const; + api::Result getResult() const; + void invoke(api::Solver* solver) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -740,20 +683,17 @@ class CVC4_PUBLIC QueryCommand : public Command class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand { public: - DeclareSygusVarCommand(const std::string& id, Expr var, Type type); + DeclareSygusVarCommand(const std::string& id, api::Term var, api::Sort sort); /** returns the declared variable */ - Expr getVar() const; - /** returns the declared variable's type */ - Type getType() const; + api::Term getVar() const; + /** returns the declared variable's sort */ + api::Sort getSort() const; /** invokes this command * * The declared sygus variable is communicated to the SMT engine in case a * synthesis conjecture is built later on. */ - void invoke(SmtEngine* smtEngine) override; - /** exports command to given expression manager */ - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -768,9 +708,9 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand protected: /** the declared variable */ - Expr d_var; - /** the declared variable's type */ - Type d_type; + api::Term d_var; + /** the declared variable's sort */ + api::Sort d_sort; }; /** Declares a sygus function-to-synthesize @@ -781,8 +721,7 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand { public: - SynthFunCommand(const api::Solver* solver, - const std::string& id, + SynthFunCommand(const std::string& id, api::Term fun, const std::vector& vars, api::Sort sort, @@ -804,10 +743,7 @@ class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand * The declared function-to-synthesize is communicated to the SMT engine in * case a synthesis conjecture is built later on. */ - void invoke(SmtEngine* smtEngine) override; - /** exports command to given expression manager */ - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -837,18 +773,15 @@ class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand class CVC4_PUBLIC SygusConstraintCommand : public Command { public: - SygusConstraintCommand(const Expr& e); + SygusConstraintCommand(const api::Term& t); /** returns the declared constraint */ - Expr getExpr() const; + api::Term getTerm() const; /** invokes this command * * The declared constraint is communicated to the SMT engine in case a * synthesis conjecture is built later on. */ - void invoke(SmtEngine* smtEngine) override; - /** exports command to given expression manager */ - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -863,7 +796,7 @@ class CVC4_PUBLIC SygusConstraintCommand : public Command protected: /** the declared constraint */ - Expr d_expr; + api::Term d_term; }; /** Declares a sygus invariant constraint @@ -879,23 +812,20 @@ class CVC4_PUBLIC SygusConstraintCommand : public Command class CVC4_PUBLIC SygusInvConstraintCommand : public Command { public: - SygusInvConstraintCommand(const std::vector& predicates); - SygusInvConstraintCommand(const Expr& inv, - const Expr& pre, - const Expr& trans, - const Expr& post); + SygusInvConstraintCommand(const std::vector& predicates); + SygusInvConstraintCommand(const api::Term& inv, + const api::Term& pre, + const api::Term& trans, + const api::Term& post); /** returns the place holder predicates */ - const std::vector& getPredicates() const; + const std::vector& getPredicates() const; /** invokes this command * * The place holders are communicated to the SMT engine and the actual * invariant constraint is built, in case an actual synthesis conjecture is * built later on. */ - void invoke(SmtEngine* smtEngine) override; - /** exports command to given expression manager */ - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -912,7 +842,7 @@ class CVC4_PUBLIC SygusInvConstraintCommand : public Command /** the place holder predicates with which to build the actual constraint * (i.e. the invariant, precondition, transition relation and postcondition) */ - std::vector d_predicates; + std::vector d_predicates; }; /** Declares a synthesis conjecture */ @@ -921,7 +851,7 @@ class CVC4_PUBLIC CheckSynthCommand : public Command public: CheckSynthCommand(){}; /** returns the result of the check-synth call */ - Result getResult() const; + api::Result getResult() const; /** prints the result of the check-synth-call */ void printResult(std::ostream& out, uint32_t verbosity = 2) const override; /** invokes this command @@ -932,10 +862,7 @@ class CVC4_PUBLIC CheckSynthCommand : public Command * and then perform a satisfiability check, whose result is stored in * d_result. */ - void invoke(SmtEngine* smtEngine) override; - /** exports command to given expression manager */ - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -950,7 +877,7 @@ class CVC4_PUBLIC CheckSynthCommand : public Command protected: /** result of the check-synth call */ - Result d_result; + api::Result d_result; /** string stream that stores the output of the solution */ std::stringstream d_solution; }; @@ -961,18 +888,16 @@ class CVC4_PUBLIC CheckSynthCommand : public Command class CVC4_PUBLIC SimplifyCommand : public Command { protected: - Expr d_term; - Expr d_result; + api::Term d_term; + api::Term d_result; public: - SimplifyCommand(Expr term); + SimplifyCommand(api::Term term); - Expr getTerm() const; - Expr getResult() const; - void invoke(SmtEngine* smtEngine) override; + api::Term getTerm() const; + api::Term getResult() const; + void invoke(api::Solver* solver) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -986,18 +911,16 @@ class CVC4_PUBLIC SimplifyCommand : public Command class CVC4_PUBLIC ExpandDefinitionsCommand : public Command { protected: - Expr d_term; - Expr d_result; + api::Term d_term; + api::Term d_result; public: - ExpandDefinitionsCommand(Expr term); + ExpandDefinitionsCommand(api::Term term); - Expr getTerm() const; - Expr getResult() const; - void invoke(SmtEngine* smtEngine) override; + api::Term getTerm() const; + api::Term getResult() const; + void invoke(api::Solver* solver) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1011,19 +934,17 @@ class CVC4_PUBLIC ExpandDefinitionsCommand : public Command class CVC4_PUBLIC GetValueCommand : public Command { protected: - std::vector d_terms; - Expr d_result; + std::vector d_terms; + api::Term d_result; public: - GetValueCommand(Expr term); - GetValueCommand(const std::vector& terms); + GetValueCommand(api::Term term); + GetValueCommand(const std::vector& terms); - const std::vector& getTerms() const; - Expr getResult() const; - void invoke(SmtEngine* smtEngine) override; + const std::vector& getTerms() const; + api::Term getResult() const; + void invoke(api::Solver* solver) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1043,10 +964,8 @@ class CVC4_PUBLIC GetAssignmentCommand : public Command GetAssignmentCommand(); SExpr getResult() const; - void invoke(SmtEngine* smtEngine) override; + void invoke(api::Solver* solver) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1064,10 +983,8 @@ class CVC4_PUBLIC GetModelCommand : public Command // Model is private to the library -- for now // Model* getResult() const ; - void invoke(SmtEngine* smtEngine) override; + void invoke(api::Solver* solver) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1088,9 +1005,7 @@ class CVC4_PUBLIC BlockModelCommand : public Command public: BlockModelCommand(); - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1105,12 +1020,10 @@ class CVC4_PUBLIC BlockModelCommand : public Command class CVC4_PUBLIC BlockModelValuesCommand : public Command { public: - BlockModelValuesCommand(const std::vector& terms); + BlockModelValuesCommand(const std::vector& terms); - const std::vector& getTerms() const; - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + const std::vector& getTerms() const; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1122,7 +1035,7 @@ class CVC4_PUBLIC BlockModelValuesCommand : public Command protected: /** The terms we are blocking */ - std::vector d_terms; + std::vector d_terms; }; /* class BlockModelValuesCommand */ class CVC4_PUBLIC GetProofCommand : public Command @@ -1130,9 +1043,7 @@ class CVC4_PUBLIC GetProofCommand : public Command public: GetProofCommand(); - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1148,10 +1059,8 @@ class CVC4_PUBLIC GetInstantiationsCommand : public Command public: GetInstantiationsCommand(); - void invoke(SmtEngine* smtEngine) override; + void invoke(api::Solver* solver) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1170,10 +1079,8 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command public: GetSynthSolutionCommand(); - void invoke(SmtEngine* smtEngine) override; + void invoke(api::Solver* solver) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1199,14 +1106,9 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command class CVC4_PUBLIC GetInterpolCommand : public Command { public: - GetInterpolCommand(const api::Solver* solver, - const std::string& name, - api::Term conj); + GetInterpolCommand(const std::string& name, api::Term conj); /** The argument g is the grammar of the interpolation query */ - GetInterpolCommand(const api::Solver* solver, - const std::string& name, - api::Term conj, - api::Grammar* g); + GetInterpolCommand(const std::string& name, api::Term conj, api::Grammar* g); /** Get the conjecture of the interpolation query */ api::Term getConjecture() const; @@ -1216,10 +1118,8 @@ class CVC4_PUBLIC GetInterpolCommand : public Command * query. */ api::Term getResult() const; - void invoke(SmtEngine* smtEngine) override; + void invoke(api::Solver* solver) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1257,13 +1157,8 @@ class CVC4_PUBLIC GetInterpolCommand : public Command class CVC4_PUBLIC GetAbductCommand : public Command { public: - GetAbductCommand(const api::Solver* solver, - const std::string& name, - api::Term conj); - GetAbductCommand(const api::Solver* solver, - const std::string& name, - api::Term conj, - api::Grammar* g); + GetAbductCommand(const std::string& name, api::Term conj); + GetAbductCommand(const std::string& name, api::Term conj, api::Grammar* g); /** Get the conjecture of the abduction query */ api::Term getConjecture() const; @@ -1275,10 +1170,8 @@ class CVC4_PUBLIC GetAbductCommand : public Command */ api::Term getResult() const; - void invoke(SmtEngine* smtEngine) override; + void invoke(api::Solver* solver) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1304,22 +1197,20 @@ class CVC4_PUBLIC GetAbductCommand : public Command class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command { protected: - Expr d_expr; + api::Term d_term; bool d_doFull; - Expr d_result; + api::Term d_result; public: GetQuantifierEliminationCommand(); - GetQuantifierEliminationCommand(const Expr& expr, bool doFull); + GetQuantifierEliminationCommand(const api::Term& term, bool doFull); - Expr getExpr() const; + api::Term getTerm() const; bool getDoFull() const; - void invoke(SmtEngine* smtEngine) override; - Expr getResult() const; + void invoke(api::Solver* solver) override; + api::Term getResult() const; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1334,11 +1225,9 @@ class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command { public: GetUnsatAssumptionsCommand(); - void invoke(SmtEngine* smtEngine) override; - std::vector getResult() const; + void invoke(api::Solver* solver) override; + std::vector getResult() const; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1349,7 +1238,7 @@ class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; protected: - std::vector d_result; + std::vector d_result; }; /* class GetUnsatAssumptionsCommand */ class CVC4_PUBLIC GetUnsatCoreCommand : public Command @@ -1358,11 +1247,9 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command GetUnsatCoreCommand(); const UnsatCore& getUnsatCore() const; - void invoke(SmtEngine* smtEngine) override; + void invoke(api::Solver* solver) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1385,11 +1272,9 @@ class CVC4_PUBLIC GetAssertionsCommand : public Command public: GetAssertionsCommand(); - void invoke(SmtEngine* smtEngine) override; + void invoke(api::Solver* solver) override; std::string getResult() const; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1410,9 +1295,7 @@ class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command BenchmarkStatus getStatus() const; - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1432,9 +1315,7 @@ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command SetBenchmarkLogicCommand(std::string logic); std::string getLogic() const; - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1457,9 +1338,7 @@ class CVC4_PUBLIC SetInfoCommand : public Command std::string getFlag() const; SExpr getSExpr() const; - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1482,10 +1361,8 @@ class CVC4_PUBLIC GetInfoCommand : public Command std::string getFlag() const; std::string getResult() const; - void invoke(SmtEngine* smtEngine) override; + void invoke(api::Solver* solver) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1508,9 +1385,7 @@ class CVC4_PUBLIC SetOptionCommand : public Command std::string getFlag() const; SExpr getSExpr() const; - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1533,10 +1408,8 @@ class CVC4_PUBLIC GetOptionCommand : public Command std::string getFlag() const; std::string getResult() const; - void invoke(SmtEngine* smtEngine) override; + void invoke(api::Solver* solver) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1557,15 +1430,13 @@ class CVC4_PUBLIC GetOptionCommand : public Command class CVC4_PUBLIC SetExpressionNameCommand : public Command { protected: - Expr d_expr; + api::Term d_term; std::string d_name; public: - SetExpressionNameCommand(Expr expr, std::string name); + SetExpressionNameCommand(api::Term term, std::string name); - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1579,16 +1450,14 @@ class CVC4_PUBLIC SetExpressionNameCommand : public Command class CVC4_PUBLIC DatatypeDeclarationCommand : public Command { private: - std::vector d_datatypes; + std::vector d_datatypes; public: - DatatypeDeclarationCommand(const Type& datatype); + DatatypeDeclarationCommand(const api::Sort& datatype); - DatatypeDeclarationCommand(const std::vector& datatypes); - const std::vector& getDatatypes() const; - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + DatatypeDeclarationCommand(const std::vector& datatypes); + const std::vector& getDatatypes() const; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1603,9 +1472,7 @@ class CVC4_PUBLIC ResetCommand : public Command { public: ResetCommand() {} - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1620,9 +1487,7 @@ class CVC4_PUBLIC ResetAssertionsCommand : public Command { public: ResetAssertionsCommand() {} - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1637,9 +1502,7 @@ class CVC4_PUBLIC QuitCommand : public Command { public: QuitCommand() {} - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1659,9 +1522,7 @@ class CVC4_PUBLIC CommentCommand : public Command std::string getComment() const; - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + void invoke(api::Solver* solver) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1687,8 +1548,8 @@ class CVC4_PUBLIC CommandSequence : public Command void addCommand(Command* cmd); void clear(); - void invoke(SmtEngine* smtEngine) override; - void invoke(SmtEngine* smtEngine, std::ostream& out) override; + void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, std::ostream& out) override; typedef std::vector::iterator iterator; typedef std::vector::const_iterator const_iterator; @@ -1699,8 +1560,6 @@ class CVC4_PUBLIC CommandSequence : public Command iterator begin(); iterator end(); - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; Command* clone() const override; std::string getCommandName() const override; void toStream( diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index ce17ffc82..1b8789513 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -133,8 +133,6 @@ namespace theory { class Rewriter; }/* CVC4::theory namespace */ -std::vector exprVectorToNodes(const std::vector& exprs); - // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the // hood): use a type parameter and have check() delegate, or subclass // SmtEngine and override check()? diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp index 6f474e24f..e5781cfaa 100644 --- a/test/api/smt2_compliance.cpp +++ b/test/api/smt2_compliance.cpp @@ -68,7 +68,7 @@ void testGetInfo(api::Solver* solver, const char* s) assert(c != NULL); cout << c << endl; stringstream ss; - c->invoke(solver->getSmtEngine(), ss); + c->invoke(solver, ss); assert(p->nextCommand() == NULL); delete p; delete c; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 40a5e5ded..d118690ed 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1390,7 +1390,6 @@ set(regress_1_tests regress1/ho/issue4092-sinf.smt2 regress1/ho/issue4134-sinf.smt2 regress1/ho/nested_lambdas-AGT034^2.smt2 - regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 regress1/ho/NUM638^1.smt2 regress1/ho/NUM925^1.p regress1/ho/soundness_fmf_SYO362^5-delta.p @@ -2491,6 +2490,8 @@ set(regression_disabled_tests regress1/crash_burn_locusts.smt2 # regress1/ho/hoa0102.smt2 results in an assertion failure (see issue #1650). regress1/ho/hoa0102.smt2 + # unknown after update to commands + regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 # issue1048-arrays-int-real.smt2 -- different errors on debug and production. regress1/issue1048-arrays-int-real.smt2 # times out after update to tangent planes diff --git a/test/regress/regress0/smtlib/get-unsat-assumptions.smt2 b/test/regress/regress0/smtlib/get-unsat-assumptions.smt2 index 7a8113d8f..ba53610b3 100644 --- a/test/regress/regress0/smtlib/get-unsat-assumptions.smt2 +++ b/test/regress/regress0/smtlib/get-unsat-assumptions.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --incremental ; EXPECT: unsat ; EXPECT: (x x) ; SCRUBBER: sed -e 's/a[1-2]/x/g' -- 2.30.2