diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-07-26 10:00:21 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-26 10:00:21 -0700 |
commit | ce4a59429f6cdf6d98bd7b28d51a2bb28d34a2c6 (patch) | |
tree | 5981c07f78d3a9f4ff37a249cd90868e5a547f5e /src/api | |
parent | c7be9ef42f06a721ba87ad2b0f0e4e3b66d45e06 (diff) |
New C++ API: Third batch of commands (SMT-LIB). (#2212)
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cvc4cpp.cpp | 201 |
1 files changed, 201 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index eefa8f7e1..10c0c8e26 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -23,6 +23,7 @@ #include "expr/type.h" #include "options/main_options.h" #include "options/options.h" +#include "smt/model.h" #include "smt/smt_engine.h" #include "util/random.h" #include "util/result.h" @@ -2576,5 +2577,205 @@ void Solver::defineFunsRec(const std::vector<Term>& funs, d_smtEngine->defineFunctionsRec(efuns, ebound_vars, exprs); } +/** + * ( echo <std::string> ) + */ +void Solver::echo(std::ostream& out, const std::string& str) const +{ + out << str; +} + +/** + * ( get-assertions ) + */ +std::vector<Term> Solver::getAssertions(void) const +{ + std::vector<Expr> assertions = d_smtEngine->getAssertions(); + /* Can not use + * return std::vector<Term>(assertions.begin(), assertions.end()); + * here since constructor is private */ + std::vector<Term> res; + for (const Expr& e : assertions) + { + res.push_back(Term(e)); + } + return res; +} + +/** + * ( get-assignment ) + */ +std::vector<std::pair<Term, Term>> Solver::getAssignment(void) const +{ + // CHECK: produce-models set + // CHECK: result sat + std::vector<std::pair<Expr, Expr>> assignment = d_smtEngine->getAssignment(); + std::vector<std::pair<Term, Term>> res; + for (const auto& p : assignment) + { + res.emplace_back(Term(p.first), Term(p.second)); + } + return res; +} + +/** + * ( get-info <info_flag> ) + */ +std::string Solver::getInfo(const std::string& flag) const +{ + // CHECK: flag valid? + return d_smtEngine->getInfo(flag).toString(); +} + +/** + * ( get-option <keyword> ) + */ +std::string Solver::getOption(const std::string& option) const +{ + // CHECK: option exists? + SExpr res = d_smtEngine->getOption(option); + return res.toString(); +} + +/** + * ( get-unsat-assumptions ) + */ +std::vector<Term> Solver::getUnsatAssumptions(void) const +{ + // CHECK: incremental? + // CHECK: option produce-unsat-assumptions set? + // CHECK: last check sat/valid result is unsat/invalid + std::vector<Expr> uassumptions = d_smtEngine->getUnsatAssumptions(); + /* Can not use + * return std::vector<Term>(uassumptions.begin(), uassumptions.end()); + * here since constructor is private */ + std::vector<Term> res; + for (const Expr& e : uassumptions) + { + res.push_back(Term(e)); + } + return res; +} + +/** + * ( get-unsat-core ) + */ +std::vector<Term> Solver::getUnsatCore(void) const +{ + // CHECK: result unsat? + UnsatCore core = d_smtEngine->getUnsatCore(); + /* Can not use + * return std::vector<Term>(core.begin(), core.end()); + * here since constructor is private */ + std::vector<Term> res; + for (const Expr& e : core) + { + res.push_back(Term(e)); + } + return res; +} + +/** + * ( get-value ( <term> ) ) + */ +Term Solver::getValue(Term term) const +{ + // CHECK: + // NodeManager::fromExprManager(d_exprMgr) + // == NodeManager::fromExprManager(expr.getExprManager()) + return d_smtEngine->getValue(*term.d_expr); +} + +/** + * ( get-value ( <term>+ ) ) + */ +std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const +{ + // CHECK: + // for e in exprs: + // NodeManager::fromExprManager(d_exprMgr) + // == NodeManager::fromExprManager(e.getExprManager()) + std::vector<Term> res; + for (const Term& t : terms) + { + /* Can not use emplace_back here since constructor is private. */ + res.push_back(Term(d_smtEngine->getValue(*t.d_expr))); + } + return res; +} + +/** + * ( pop <numeral> ) + */ +void Solver::pop(uint32_t nscopes) const +{ + // CHECK: incremental enabled? + // CHECK: nscopes <= d_smtEngine->d_userLevels.size() + for (uint32_t n = 0; n < nscopes; ++n) + { + d_smtEngine->pop(); + } +} + +void Solver::printModel(std::ostream& out) const +{ + // CHECK: produce-models? + out << *d_smtEngine->getModel(); +} + +/** + * ( push <numeral> ) + */ +void Solver::push(uint32_t nscopes) const +{ + // CHECK: incremental enabled? + for (uint32_t n = 0; n < nscopes; ++n) + { + d_smtEngine->push(); + } +} + +/** + * ( reset ) + */ +void Solver::reset(void) const { d_smtEngine->reset(); } + +/** + * ( reset-assertions ) + */ +void Solver::resetAssertions(void) const { d_smtEngine->resetAssertions(); } + +/** + * ( set-info <attribute> ) + */ +void Solver::setInfo(const std::string& keyword, const std::string& value) const +{ + // CHECK: + // if keyword == "cvc4-logic": value must be string + // if keyword == "status": must be sat, unsat or unknown + // if keyword == "smt-lib-version": supported? + d_smtEngine->setInfo(keyword, value); +} + +/** + * ( set-logic <symbol> ) + */ +void Solver::setLogic(const std::string& logic) const +{ + // CHECK: !d_smtEngine->d_fullyInited + d_smtEngine->setLogic(logic); +} + +/** + * ( set-option <option> ) + */ +void Solver::setOption(const std::string& option, + const std::string& value) const +{ + // CHECK: option exists? + // CHECK: !d_smtEngine->d_fullInited, else option can't be set + d_smtEngine->setOption(option, value); +} + } // namespace api } // namespace CVC4 |