New C++ API: Third batch of commands (SMT-LIB). (#2212)

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