diff options
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/command.cpp | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 3b723de1f..a6b528661 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -532,7 +532,7 @@ void CheckSatAssumingCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdCheckSatAssuming( - out, api::termVectorToNodes(d_terms)); + out, api::Term::termVectorToNodes(d_terms)); } /* -------------------------------------------------------------------------- */ @@ -678,7 +678,7 @@ void SynthFunCommand::toStream(std::ostream& out, size_t dag, OutputLanguage language) const { - std::vector<Node> nodeVars = termVectorToNodes(d_vars); + std::vector<Node> nodeVars = api::Term::termVectorToNodes(d_vars); Printer::getPrinter(language)->toStreamCmdSynthFun( out, d_fun.getNode(), @@ -1289,7 +1289,7 @@ void DefineFunctionCommand::toStream(std::ostream& out, Printer::getPrinter(language)->toStreamCmdDefineFunction( out, d_func.toString(), - api::termVectorToNodes(d_formals), + api::Term::termVectorToNodes(d_formals), d_func.getNode().getType().getRangeType(), d_formula.getNode()); } @@ -1369,14 +1369,14 @@ void DefineFunctionRecCommand::toStream(std::ostream& out, formals.reserve(d_formals.size()); for (const std::vector<api::Term>& formal : d_formals) { - formals.push_back(api::termVectorToNodes(formal)); + formals.push_back(api::Term::termVectorToNodes(formal)); } Printer::getPrinter(language)->toStreamCmdDefineFunctionRec( out, - api::termVectorToNodes(d_funcs), + api::Term::termVectorToNodes(d_funcs), formals, - api::termVectorToNodes(d_formulas)); + api::Term::termVectorToNodes(d_formulas)); } /* -------------------------------------------------------------------------- */ /* class DeclareHeapCommand */ @@ -1456,7 +1456,7 @@ void SetUserAttributeCommand::invoke(api::Solver* solver, SymbolManager* sm) solver->getSmtEngine()->setUserAttribute( d_attr, d_term.getNode(), - api::termVectorToNodes(d_termValues), + api::Term::termVectorToNodes(d_termValues), d_strValue); } d_commandStatus = CommandSuccess::instance(); @@ -1617,7 +1617,7 @@ void GetValueCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdGetValue( - out, api::termVectorToNodes(d_terms)); + out, api::Term::termVectorToNodes(d_terms)); } /* -------------------------------------------------------------------------- */ @@ -1870,7 +1870,7 @@ void BlockModelValuesCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdBlockModelValues( - out, api::termVectorToNodes(d_terms)); + out, api::Term::termVectorToNodes(d_terms)); } /* -------------------------------------------------------------------------- */ @@ -2374,7 +2374,7 @@ void GetUnsatCoreCommand::printResult(std::ostream& out, if (options::dumpUnsatCoresFull()) { // use the assertions - UnsatCore ucr(api::termVectorToNodes(d_result)); + UnsatCore ucr(api::Term::termVectorToNodes(d_result)); ucr.toStream(out); } else |