Plug solver API object into parser. (#2240)

2 files changed, 172 insertions, 53 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 19d7840a8..bc696a057 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -95,6 +95,10 @@ std::string Result::getUnknownExplanation(void) const
 
 std::string Result::toString(void) const { return d_result->toString(); }
 
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::Result Result::getResult(void) const { return *d_result; }
+
 std::ostream& operator<<(std::ostream& out, const Result& r)
 {
   out << r.toString();
@@ -801,6 +805,10 @@ std::string Sort::toString() const
   return d_type->toString();
 }
 
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::Type Sort::getType(void) const { return *d_type; }
+
 std::ostream& operator<<(std::ostream& out, const Sort& s)
 {
   out << s.toString();
@@ -942,6 +950,10 @@ Term::const_iterator Term::end() const
   return Term::const_iterator(new CVC4::Expr::const_iterator(d_expr->end()));
 }
 
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::Expr Term::getExpr(void) const { return *d_expr; }
+
 std::ostream& operator<<(std::ostream& out, const Term& t)
 {
   out << t.toString();
@@ -1029,6 +1041,10 @@ bool OpTerm::isNull() const { return d_expr->isNull(); }
 
 std::string OpTerm::toString() const { return d_expr->toString(); }
 
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::Expr OpTerm::getExpr(void) const { return *d_expr; }
+
 std::ostream& operator<<(std::ostream& out, const OpTerm& t)
 {
   out << t.toString();
@@ -1097,6 +1113,14 @@ std::string DatatypeConstructorDecl::toString() const
   return ss.str();
 }
 
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::DatatypeConstructor DatatypeConstructorDecl::getDatatypeConstructor(
+    void) const
+{
+  return *d_ctor;
+}
+
 std::ostream& operator<<(std::ostream& out,
                          const DatatypeConstructorDecl& ctordecl)
 {
@@ -1146,6 +1170,10 @@ std::string DatatypeDecl::toString() const
   return ss.str();
 }
 
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::Datatype DatatypeDecl::getDatatype(void) const { return *d_dtype; }
+
 std::ostream& operator<<(std::ostream& out,
                          const DatatypeSelectorDecl& stordecl)
 {
@@ -1171,6 +1199,14 @@ std::string DatatypeSelector::toString() const
   return ss.str();
 }
 
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::DatatypeConstructorArg DatatypeSelector::getDatatypeConstructorArg(
+    void) const
+{
+  return *d_stor;
+}
+
 std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor)
 {
   out << stor.toString();
@@ -1287,6 +1323,14 @@ std::string DatatypeConstructor::toString() const
   return ss.str();
 }
 
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::DatatypeConstructor DatatypeConstructor::getDatatypeConstructor(
+    void) const
+{
+  return *d_ctor;
+}
+
 std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor)
 {
   out << ctor.toString();
@@ -1333,6 +1377,10 @@ Datatype::const_iterator Datatype::end() const
   return Datatype::const_iterator(*d_dtype, false);
 }
 
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::Datatype Datatype::getDatatype(void) const { return *d_dtype; }
+
 Datatype::const_iterator::const_iterator(const CVC4::Datatype& dtype,
                                          bool begin)
 {
@@ -1431,10 +1479,11 @@ size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const
 
 Solver::Solver(Options* opts)
 {
-  d_exprMgr = std::unique_ptr<ExprManager>(
-      opts == nullptr ? new ExprManager(Options()) : new ExprManager(*opts));
-  d_smtEngine = std::unique_ptr<SmtEngine>(new SmtEngine(d_exprMgr.get()));
-  d_rng = std::unique_ptr<Random>(new Random((*opts)[options::seed]));
+  Options* o = opts == nullptr ?  new Options() : opts;
+  d_exprMgr.reset(new ExprManager(*o));
+  d_smtEngine.reset(new SmtEngine(d_exprMgr.get()));
+  d_rng.reset(new Random((*o)[options::seed]));
+  if (opts == nullptr) delete o;
 }
 
 Solver::~Solver() {}
@@ -2777,5 +2826,17 @@ void Solver::setOption(const std::string& option,
   d_smtEngine->setOption(option, value);
 }
 
+/**
+ * !!! This is only temporarily available until the parser is fully migrated to
+ * the new API. !!!
+ */
+ExprManager* Solver::getExprManager(void) const { return d_exprMgr.get(); }
+
+/**
+ * !!! This is only temporarily available until the parser is fully migrated to
+ * the new API. !!!
+ */
+SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); }
+
 }  // namespace api
 }  // namespace CVC4
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 0d05c9b19..b1a1e2abd 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -56,6 +56,15 @@ class CVC4_PUBLIC Result
   friend class Solver;
 
  public:
+  // !!! This constructor is only temporarily public until the parser is fully
+  // migrated to the new API. !!!
+  /**
+   * Constructor.
+   * @param r the internal result that is to be wrapped by this result
+   * @return the Result
+   */
+  Result(const CVC4::Result& r);
+
   /**
    * Return true if query was a satisfiable checkSat() or checkSatAssuming()
    * query.
@@ -116,14 +125,11 @@ class CVC4_PUBLIC Result
    */
   std::string toString() const;
 
- private:
-  /**
-   * Constructor.
-   * @param r the internal result that is to be wrapped by this result
-   * @return the Result
-   */
-  Result(const CVC4::Result& r);
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  CVC4::Result getResult(void) const;
 
+ private:
   /**
    * The interal result wrapped by this result.
    * This is a shared_ptr rather than a unique_ptr since CVC4::Result is
@@ -160,6 +166,15 @@ class CVC4_PUBLIC Sort
   friend class Term;
 
  public:
+  // !!! This constructor is only temporarily public until the parser is fully
+  // migrated to the new API. !!!
+  /**
+   * Constructor.
+   * @param t the internal type that is to be wrapped by this sort
+   * @return the Sort
+   */
+  Sort(const CVC4::Type& t);
+
   /**
    * Destructor.
    */
@@ -313,14 +328,11 @@ class CVC4_PUBLIC Sort
    */
   std::string toString() const;
 
- private:
-  /**
-   * Constructor.
-   * @param t the internal type that is to be wrapped by this sort
-   * @return the Sort
-   */
-  Sort(const CVC4::Type& t);
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  CVC4::Type getType(void) const;
 
+ private:
   /**
    * The interal type wrapped by this sort.
    * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
@@ -361,6 +373,15 @@ class CVC4_PUBLIC Term
   friend struct TermHashFunction;
 
  public:
+  // !!! This constructor is only temporarily public until the parser is fully
+  // migrated to the new API. !!!
+  /**
+   * Constructor.
+   * @param e the internal expression that is to be wrapped by this term
+   * @return the Term
+   */
+  Term(const CVC4::Expr& e);
+
   /**
    * Constructor.
    */
@@ -545,14 +566,11 @@ class CVC4_PUBLIC Term
    */
   const_iterator end() const;
 
- private:
-  /**
-   * Constructor.
-   * @param e the internal expression that is to be wrapped by this term
-   * @return the Term
-   */
-  Term(const CVC4::Expr& e);
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  CVC4::Expr getExpr(void) const;
 
+ private:
   /**
    * The internal expression wrapped by this term.
    * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
@@ -650,6 +668,15 @@ class CVC4_PUBLIC OpTerm
    */
   OpTerm();
 
+  // !!! This constructor is only temporarily public until the parser is fully
+  // migrated to the new API. !!!
+  /**
+   * Constructor.
+   * @param e the internal expression that is to be wrapped by this term
+   * @return the Term
+   */
+  OpTerm(const CVC4::Expr& e);
+
   /**
    * Destructor.
    */
@@ -701,14 +728,11 @@ class CVC4_PUBLIC OpTerm
    */
   std::string toString() const;
 
- private:
-  /**
-   * Constructor.
-   * @param e the internal expression that is to be wrapped by this term
-   * @return the Term
-   */
-  OpTerm(const CVC4::Expr& e);
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  CVC4::Expr getExpr(void) const;
 
+ private:
   /**
    * The internal expression wrapped by this operator term.
    * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
@@ -812,6 +836,10 @@ class CVC4_PUBLIC DatatypeConstructorDecl
    */
   std::string toString() const;
 
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  CVC4::DatatypeConstructor getDatatypeConstructor(void) const;
+
  private:
   /**
    * The internal (intermediate) datatype constructor wrapped by this
@@ -875,6 +903,10 @@ class CVC4_PUBLIC DatatypeDecl
    */
   std::string toString() const;
 
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  CVC4::Datatype getDatatype(void) const;
+
  private:
   /* The internal (intermediate) datatype wrapped by this datatype
    * declaration
@@ -898,6 +930,15 @@ class CVC4_PUBLIC DatatypeSelector
    */
   DatatypeSelector();
 
+  // !!! This constructor is only temporarily public until the parser is fully
+  // migrated to the new API. !!!
+  /**
+   * Constructor.
+   * @param stor the internal datatype selector to be wrapped
+   * @return the DatatypeSelector
+   */
+  DatatypeSelector(const CVC4::DatatypeConstructorArg& stor);
+
   /**
    * Destructor.
    */
@@ -908,14 +949,11 @@ class CVC4_PUBLIC DatatypeSelector
    */
   std::string toString() const;
 
- private:
-  /**
-   * Constructor.
-   * @param stor the internal datatype selector to be wrapped
-   * @return the DatatypeSelector
-   */
-  DatatypeSelector(const CVC4::DatatypeConstructorArg& stor);
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  CVC4::DatatypeConstructorArg getDatatypeConstructorArg(void) const;
 
+ private:
   /**
    * The internal datatype selector wrapped by this datatype selector.
    * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
@@ -938,6 +976,15 @@ class CVC4_PUBLIC DatatypeConstructor
    */
   DatatypeConstructor();
 
+  // !!! This constructor is only temporarily public until the parser is fully
+  // migrated to the new API. !!!
+  /**
+   * Constructor.
+   * @param ctor the internal datatype constructor to be wrapped
+   * @return thte DatatypeConstructor
+   */
+  DatatypeConstructor(const CVC4::DatatypeConstructor& ctor);
+
   /**
    * Destructor.
    */
@@ -1048,14 +1095,11 @@ class CVC4_PUBLIC DatatypeConstructor
    */
   const_iterator end() const;
 
- private:
-  /**
-   * Constructor.
-   * @param ctor the internal datatype constructor to be wrapped
-   * @return thte DatatypeConstructor
-   */
-  DatatypeConstructor(const CVC4::DatatypeConstructor& ctor);
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  CVC4::DatatypeConstructor getDatatypeConstructor(void) const;
 
+ private:
   /**
    * The internal datatype constructor wrapped by this datatype constructor.
    * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
@@ -1073,6 +1117,15 @@ class CVC4_PUBLIC Datatype
   friend class Sort;
 
  public:
+  // !!! This constructor is only temporarily public until the parser is fully
+  // migrated to the new API. !!!
+  /**
+   * Constructor.
+   * @param dtype the internal datatype to be wrapped
+   * @return the Datatype
+   */
+  Datatype(const CVC4::Datatype& dtype);
+
   /**
    * Destructor.
    */
@@ -1181,14 +1234,11 @@ class CVC4_PUBLIC Datatype
    */
   const_iterator end() const;
 
- private:
-  /**
-   * Constructor.
-   * @param dtype the internal datatype to be wrapped
-   * @return the Datatype
-   */
-  Datatype(const CVC4::Datatype& dtype);
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  CVC4::Datatype getDatatype(void) const;
 
+ private:
   /**
    * The internal datatype wrapped by this datatype.
    * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
@@ -2349,6 +2399,14 @@ class CVC4_PUBLIC Solver
    */
   void setOption(const std::string& option, const std::string& value) const;
 
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  ExprManager* getExprManager(void) const;
+
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  SmtEngine* getSmtEngine(void) const;
+
  private:
   /* Helper to convert a vector of internal types to sorts. */
   std::vector<Type> sortVectorToTypes(const std::vector<Sort>& vector) const;