From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 24 Jul 2018 17:11:24 +0000 (-0700)
Subject:  New C++ API: First batch of commands (SMT-LIB and non-SMT-LIB). (#2199)
X-Git-Tag: cvc5-1.0.0~4872
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f270410e420d4c464c94c249e107451c5f1341ee;p=cvc5.git

 New C++ API: First batch of commands (SMT-LIB and non-SMT-LIB). (#2199)
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 53b87f2fa..dbaac4f8c 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2248,6 +2248,96 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2)
   return res;
 }
 
+/* Non-SMT-LIB commands                                                       */
+/* -------------------------------------------------------------------------- */
+
+Term Solver::simplify(const Term& t)
+{
+  return d_smtEngine->simplify(*t.d_expr);
+}
+
+Result Solver::checkValid(void) const
+{
+  // CHECK:
+  // if d_queryMade -> incremental enabled
+  CVC4::Result r = d_smtEngine->query();
+  return Result(r);
+}
+
+Result Solver::checkValidAssuming(Term assumption) const
+{
+  // CHECK:
+  // if assumptions.size() > 0:  incremental enabled?
+  CVC4::Result r = d_smtEngine->query(*assumption.d_expr);
+  return Result(r);
+}
+
+Result Solver::checkValidAssuming(const std::vector<Term>& assumptions) const
+{
+  // CHECK:
+  // if assumptions.size() > 0:  incremental enabled?
+  std::vector<Expr> eassumptions = termVectorToExprs(assumptions);
+  CVC4::Result r = d_smtEngine->query(eassumptions);
+  return Result(r);
+}
+
+/* SMT-LIB commands                                                           */
+/* -------------------------------------------------------------------------- */
+
+/**
+ *  ( assert <term> )
+ */
+void Solver::assertFormula(Term term) const
+{
+  // CHECK:
+  // NodeManager::fromExprManager(d_exprMgr)
+  // == NodeManager::fromExprManager(expr.getExprManager())
+  d_smtEngine->assertFormula(*term.d_expr);
+}
+
+/**
+ *  ( check-sat )
+ */
+Result Solver::checkSat(void) const
+{
+  // CHECK:
+  // if d_queryMade -> incremental enabled
+  CVC4::Result r = d_smtEngine->checkSat();
+  return Result(r);
+}
+
+/**
+ *  ( check-sat-assuming ( <prop_literal> ) )
+ */
+Result Solver::checkSatAssuming(Term assumption) const
+{
+  // CHECK:
+  // if assumptions.size() > 0:  incremental enabled?
+  CVC4::Result r = d_smtEngine->checkSat(*assumption.d_expr);
+  return Result(r);
+}
+
+/**
+ *  ( check-sat-assuming ( <prop_literal>* ) )
+ */
+Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
+{
+  // CHECK:
+  // if assumptions.size() > 0:  incremental enabled?
+  std::vector<Expr> eassumptions = termVectorToExprs(assumptions);
+  CVC4::Result r = d_smtEngine->checkSat(eassumptions);
+  return Result(r);
+}
+
+/**
+ *  ( declare-const <symbol> <sort> )
+ */
+Term Solver::declareConst(const std::string& symbol, Sort sort) const
+{
+  // CHECK: sort exists
+  return d_exprMgr->mkVar(symbol, *sort.d_type);
+}
+
 /**
  *  ( declare-datatype <symbol> <datatype_decl> )
  */