From c82720479efcf922136f0919f6fc26a502b2515a Mon Sep 17 00:00:00 2001
From: makaimann <makaim@stanford.edu>
Date: Wed, 19 Feb 2020 13:54:17 -0800
Subject: Add Python bindings using Cython -- see below for more details
 (#2879)

---
 src/api/cvc4cpp.h | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'src/api/cvc4cpp.h')

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index f7f16832a..79c02c031 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -1095,6 +1095,11 @@ class CVC4_PUBLIC DatatypeDecl
   friend class DatatypeConstructorArg;
   friend class Solver;
  public:
+  /**
+   * Nullary constructor for Cython
+   */
+  DatatypeDecl();
+
   /**
    * Destructor.
    */
@@ -1112,6 +1117,8 @@ class CVC4_PUBLIC DatatypeDecl
   /** Is this Datatype declaration parametric? */
   bool isParametric() const;
 
+  bool isNull() const;
+
   /**
    * @return a string representation of this datatype declaration
    */
@@ -1158,6 +1165,10 @@ class CVC4_PUBLIC DatatypeDecl
                const std::string& name,
                const std::vector<Sort>& params,
                bool isCoDatatype = false);
+
+  // helper for isNull() to avoid calling API functions from other API functions
+  bool isNullHelper() const;
+
   /* The internal (intermediate) datatype wrapped by this datatype
    * declaration
    * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
@@ -1295,6 +1306,9 @@ class CVC4_PUBLIC DatatypeConstructor
     friend class DatatypeConstructor;  // to access constructor
 
    public:
+    /** Nullary constructor (required for Cython). */
+    const_iterator();
+
     /**
      * Assignment operator.
      * @param it the iterator to assign to
@@ -1398,6 +1412,9 @@ class CVC4_PUBLIC Datatype
    */
   Datatype(const CVC4::Datatype& dtype);
 
+  // Nullary constructor for Cython
+  Datatype();
+
   /**
    * Destructor.
    */
@@ -1447,6 +1464,9 @@ class CVC4_PUBLIC Datatype
     friend class Datatype;  // to access constructor
 
    public:
+    /** Nullary constructor (required for Cython). */
+    const_iterator();
+
     /**
      * Assignment operator.
      * @param it the iterator to assign to
-- 
cgit v1.2.3