diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 10 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 2 | ||||
-rw-r--r-- | src/main/command_executor.cpp | 46 | ||||
-rw-r--r-- | src/main/command_executor.h | 6 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 4 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 56 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 24 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 111 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 11 | ||||
-rw-r--r-- | src/parser/tptp/Tptp.g | 24 | ||||
-rw-r--r-- | src/parser/tptp/tptp.cpp | 19 | ||||
-rw-r--r-- | src/smt/command.cpp | 1066 | ||||
-rw-r--r-- | src/smt/command.h | 495 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 2 |
14 files changed, 656 insertions, 1220 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<Type> sortVectorToTypes(const std::vector<Sort>& sorts) return types; } +std::vector<TypeNode> sortVectorToTypeNodes(const std::vector<Sort>& sorts) +{ + std::vector<TypeNode> typeNodes; + for (const Sort& sort : sorts) + { + typeNodes.push_back(TypeNode::fromType(sort.getType())); + } + return typeNodes; +} + std::set<Type> sortSetToTypes(const std::set<Sort>& sorts) { std::set<Type> 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<Expr> termVectorToExprs(const std::vector<Term>& terms); std::vector<Node> termVectorToNodes(const std::vector<Term>& terms); std::vector<Type> sortVectorToTypes(const std::vector<Sort>& sorts); +std::vector<TypeNode> sortVectorToTypeNodes(const std::vector<Sort>& sorts); std::set<Type> sortSetToTypes(const std::set<Sort>& sorts); std::vector<Term> exprVectorToTerms(const Solver* slv, const std::vector<Expr>& 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<const CheckSatCommand*>(cmd); if(cs != nullptr) { d_result = res = cs->getResult(); @@ -149,34 +149,34 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) if (status) { std::vector<std::unique_ptr<Command> > 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<api::Result> 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<QuitCommand*>(cmd) != NULL) { + if (dynamic_cast<QuitCommand*>(cmd) != NULL) + { d_quit = true; break; - } else { + } + else + { #if HAVE_LIBEDITLINE - if(dynamic_cast<DeclareFunctionCommand*>(cmd) != NULL) { - s_declarations.insert(dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol()); - } else if(dynamic_cast<DefineFunctionCommand*>(cmd) != NULL) { - s_declarations.insert(dynamic_cast<DefineFunctionCommand*>(cmd)->getSymbol()); - } else if(dynamic_cast<DeclareTypeCommand*>(cmd) != NULL) { - s_declarations.insert(dynamic_cast<DeclareTypeCommand*>(cmd)->getSymbol()); - } else if(dynamic_cast<DefineTypeCommand*>(cmd) != NULL) { - s_declarations.insert(dynamic_cast<DefineTypeCommand*>(cmd)->getSymbol()); + if (dynamic_cast<DeclareFunctionCommand*>(cmd) != NULL) + { + s_declarations.insert( + dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol()); + } + else if (dynamic_cast<DefineFunctionCommand*>(cmd) != NULL) + { + s_declarations.insert( + dynamic_cast<DefineFunctionCommand*>(cmd)->getSymbol()); + } + else if (dynamic_cast<DeclareSortCommand*>(cmd) != NULL) + { + s_declarations.insert( + dynamic_cast<DeclareSortCommand*>(cmd)->getSymbol()); + } + else if (dynamic_cast<DefineSortCommand*>(cmd) != NULL) + { + s_declarations.insert( + dynamic_cast<DefineSortCommand*>(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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<api::Term, std::string> 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<CVC4::Command>* 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<CVC4::Command> 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<CVC4::Command> 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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<CVC4::Command>* 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>(), expr.getExpr(), PARSER_STATE->getGlobalDeclarations()); + Command* c = + new DefineNamedFunctionCommand(name, + func, + std::vector<api::Term>(), + 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<Command> Smt2::SynthFunFactory::mkCommand(api::Grammar* grammar) { Debug("parser-sygus") << "...read synth fun " << d_id << std::endl; d_smt2->popScope(); - return std::unique_ptr<Command>(new SynthFunCommand( - d_smt2->d_solver, d_id, d_fun, d_sygusVars, d_sort, d_isInv, grammar)); + return std::unique_ptr<Command>( + new SynthFunCommand(d_id, d_fun, d_sygusVars, d_sort, d_isInv, grammar)); } std::unique_ptr<Command> Smt2::invConstraint( @@ -556,8 +556,7 @@ std::unique_ptr<Command> Smt2::invConstraint( terms.push_back(getVariable(name)); } - return std::unique_ptr<Command>( - new SygusInvConstraintCommand(api::termVectorToExprs(terms))); + return std::unique_ptr<Command>(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<api::Term>& boundVars, const std::vector<api::Term>& 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<api::Term>& 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<TypeNode> typeVectorToTypeNodes(const std::vector<Type>& types) -{ - std::vector<TypeNode> 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<const CommandInterrupted*>(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<Expr>& terms) +CheckSatAssumingCommand::CheckSatAssumingCommand( + const std::vector<api::Term>& terms) : d_terms(terms) { } -const std::vector<Expr>& CheckSatAssumingCommand::getTerms() const +const std::vector<api::Term>& 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<Expr> 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<Node> 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<api::Term>& 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<Expr>& predicates) + const std::vector<api::Term>& predicates) : d_predicates(predicates) { } -SygusInvConstraintCommand::SygusInvConstraintCommand(const Expr& inv, - const Expr& pre, - const Expr& trans, - const Expr& post) - : SygusInvConstraintCommand(std::vector<Expr>{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<api::Term>{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<Expr>& SygusInvConstraintCommand::getPredicates() const +const std::vector<api::Term>& 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<Type>& params, - Type t) - : DeclarationDefinitionCommand(id), d_params(params), d_type(t) +DefineSortCommand::DefineSortCommand(const std::string& id, + const std::vector<api::Sort>& params, + api::Sort sort) + : DeclarationDefinitionCommand(id), d_params(params), d_sort(sort) { } -const std::vector<Type>& DefineTypeCommand::getParameters() const +const std::vector<api::Sort>& 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<Type> 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<Expr>& formals, - Expr formula, - bool global) +DefineFunctionCommand::DefineFunctionCommand( + const std::string& id, + api::Term func, + const std::vector<api::Term>& 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<Expr>& DefineFunctionCommand::getFormals() const +api::Term DefineFunctionCommand::getFunction() const { return d_func; } +const std::vector<api::Term>& 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<Expr> 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<Expr>& formals, - Expr formula, + api::Term func, + const std::vector<api::Term>& 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<Expr> 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<api::Term>& 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<api::Term>& funcs, const std::vector<std::vector<api::Term>>& formals, const std::vector<api::Term>& 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<api::Term>& 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>& 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<api::Term>& 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<Expr>& values) - : SetUserAttributeCommand(attr, expr, values, "") + const std::string& attr, + api::Term term, + const std::vector<api::Term>& 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<Expr>& terms) +GetValueCommand::GetValueCommand(const std::vector<api::Term>& terms) : d_terms(terms) { PrettyCheckArgument( terms.size() >= 1, terms, "cannot get-value of an empty set of terms"); } -const std::vector<Expr>& GetValueCommand::getTerms() const { return d_terms; } -void GetValueCommand::invoke(SmtEngine* smtEngine) +const std::vector<api::Term>& 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<Expr> result = smtEngine->getValues(d_terms); + NodeManager* nm = solver->getNodeManager(); + smt::SmtScope scope(solver->getSmtEngine()); + std::vector<Node> 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<Expr> exportedTerms; - for (std::vector<Expr>::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<std::pair<Expr, Expr>> assignments = smtEngine->getAssignment(); + std::vector<std::pair<Expr, Expr>> assignments = + solver->getSmtEngine()->getAssignment(); vector<SExpr> 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<Expr>& terms) +BlockModelValuesCommand::BlockModelValuesCommand( + const std::vector<api::Term>& terms) : d_terms(terms) { PrettyCheckArgument(terms.size() >= 1, @@ -2197,15 +1926,15 @@ BlockModelValuesCommand::BlockModelValuesCommand(const std::vector<Expr>& terms) "cannot block-model-values of an empty set of terms"); } -const std::vector<Expr>& BlockModelValuesCommand::getTerms() const +const std::vector<api::Term>& 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<Expr> exportedTerms; - for (std::vector<Expr>::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<Node> 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<Expr> GetUnsatAssumptionsCommand::getResult() const +std::vector<api::Term> 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<Expr> v = smtEngine->getAssertions(); + const vector<api::Term> v = solver->getAssertions(); ss << "(\n"; - copy(v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n")); + copy(v.begin(), v.end(), ostream_iterator<api::Term>(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<SExpr> 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<Type>& datatypes) + const std::vector<api::Sort>& datatypes) : d_datatypes(datatypes) { } -const std::vector<Type>& DatatypeDeclarationCommand::getDatatypes() const +const std::vector<api::Sort>& 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, @@ -244,37 +244,10 @@ class CVC4_PUBLIC Command 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<Type> d_params; - Type d_type; + std::vector<api::Sort> d_params; + api::Sort d_sort; public: - DefineTypeCommand(const std::string& id, Type t); - DefineTypeCommand(const std::string& id, - const std::vector<Type>& params, - Type t); + DefineSortCommand(const std::string& id, api::Sort sort); + DefineSortCommand(const std::string& id, + const std::vector<api::Sort>& params, + api::Sort sort); - const std::vector<Type>& getParameters() const; - Type getType() const; + const std::vector<api::Sort>& 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<Expr>& formals, - Expr formula, + api::Term func, + const std::vector<api::Term>& formals, + api::Term formula, bool global); - Expr getFunction() const; - const std::vector<Expr>& getFormals() const; - Expr getFormula() const; + api::Term getFunction() const; + const std::vector<api::Term>& 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<Expr> d_formals; + std::vector<api::Term> 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<Expr>& formals, - Expr formula, + api::Term func, + const std::vector<api::Term>& 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<api::Term>& formals, api::Term formula, bool global); - DefineFunctionRecCommand(const api::Solver* solver, - const std::vector<api::Term>& funcs, + DefineFunctionRecCommand(const std::vector<api::Term>& funcs, const std::vector<std::vector<api::Term> >& formals, const std::vector<api::Term>& formula, bool global); @@ -582,9 +535,7 @@ class CVC4_PUBLIC DefineFunctionRecCommand : public Command const std::vector<std::vector<api::Term> >& getFormals() const; const std::vector<api::Term>& getFormulas() const; - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - 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<Expr>& values); + api::Term term, + const std::vector<api::Term>& 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>& expr_values, - const std::string& str_value); + api::Term term, + const std::vector<api::Term>& termValues, + const std::string& strValue); const std::string d_attr; - const Expr d_expr; - const std::vector<Expr> d_expr_values; - const std::string d_str_value; + const api::Term d_term; + const std::vector<api::Term> 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<Expr>& terms); + CheckSatAssumingCommand(api::Term term); + CheckSatAssumingCommand(const std::vector<api::Term>& terms); - const std::vector<Expr>& getTerms() const; - Result getResult() const; - void invoke(SmtEngine* smtEngine) override; + const std::vector<api::Term>& 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<Expr> d_terms; - Result d_result; + std::vector<api::Term> 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<api::Term>& 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<Expr>& predicates); - SygusInvConstraintCommand(const Expr& inv, - const Expr& pre, - const Expr& trans, - const Expr& post); + SygusInvConstraintCommand(const std::vector<api::Term>& 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<Expr>& getPredicates() const; + const std::vector<api::Term>& 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<Expr> d_predicates; + std::vector<api::Term> 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<Expr> d_terms; - Expr d_result; + std::vector<api::Term> d_terms; + api::Term d_result; public: - GetValueCommand(Expr term); - GetValueCommand(const std::vector<Expr>& terms); + GetValueCommand(api::Term term); + GetValueCommand(const std::vector<api::Term>& terms); - const std::vector<Expr>& getTerms() const; - Expr getResult() const; - void invoke(SmtEngine* smtEngine) override; + const std::vector<api::Term>& 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<Expr>& terms); + BlockModelValuesCommand(const std::vector<api::Term>& terms); - const std::vector<Expr>& getTerms() const; - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + const std::vector<api::Term>& 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<Expr> d_terms; + std::vector<api::Term> 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<Expr> getResult() const; + void invoke(api::Solver* solver) override; + std::vector<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( @@ -1349,7 +1238,7 @@ class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; protected: - std::vector<Expr> d_result; + std::vector<api::Term> 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<Type> d_datatypes; + std::vector<api::Sort> d_datatypes; public: - DatatypeDeclarationCommand(const Type& datatype); + DatatypeDeclarationCommand(const api::Sort& datatype); - DatatypeDeclarationCommand(const std::vector<Type>& datatypes); - const std::vector<Type>& getDatatypes() const; - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; + DatatypeDeclarationCommand(const std::vector<api::Sort>& datatypes); + const std::vector<api::Sort>& 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<Command*>::iterator iterator; typedef std::vector<Command*>::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<Node> exprVectorToNodes(const std::vector<Expr>& 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()? |