Merge branch 'master' into lfscTestslfscTests

1 files changed, 200 insertions, 34 deletions

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 279453747..76306d443 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2,9 +2,9 @@
 /*! \file cvc4cpp.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Andres Noetzli
+ **   Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -49,6 +49,8 @@ class Result;
 
 namespace api {
 
+class Solver;
+
 /* -------------------------------------------------------------------------- */
 /* Exception                                                                  */
 /* -------------------------------------------------------------------------- */
@@ -199,10 +201,11 @@ class CVC4_PUBLIC Sort
   // migrated to the new API. !!!
   /**
    * Constructor.
+   * @param slv the associated solver object
    * @param t the internal type that is to be wrapped by this sort
    * @return the Sort
    */
-  Sort(const CVC4::Type& t);
+  Sort(const Solver* slv, const CVC4::Type& t);
 
   /**
    * Constructor.
@@ -589,6 +592,11 @@ class CVC4_PUBLIC Sort
   bool isNullHelper() const;
 
   /**
+   * The associated solver object.
+   */
+  const Solver* d_solver;
+
+  /**
    * The interal type wrapped by this sort.
    * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
    * memory allocation (CVC4::Type is already ref counted, so this could be
@@ -637,19 +645,21 @@ class CVC4_PUBLIC Op
   // migrated to the new API. !!!
   /**
    * Constructor for a single kind (non-indexed operator).
+   * @param slv the associated solver object
    * @param k the kind of this Op
    */
-  Op(const Kind k);
+  Op(const Solver* slv, const Kind k);
 
   // !!! This constructor is only temporarily public until the parser is fully
   // migrated to the new API. !!!
   /**
    * Constructor.
+   * @param slv the associated solver object
    * @param k the kind of this Op
    * @param e the internal expression that is to be wrapped by this term
    * @return the Term
    */
-  Op(const Kind k, const CVC4::Expr& e);
+  Op(const Solver* slv, const Kind k, const CVC4::Expr& e);
 
   /**
    * Destructor.
@@ -726,6 +736,11 @@ class CVC4_PUBLIC Op
    */
   bool isIndexedHelper() const;
 
+  /**
+   * The associated solver object.
+   */
+  const Solver* d_solver;
+
   /* The kind of this operator. */
   Kind d_kind;
 
@@ -758,10 +773,11 @@ class CVC4_PUBLIC Term
   // migrated to the new API. !!!
   /**
    * Constructor.
+   * @param slv the associated solver object
    * @param e the internal expression that is to be wrapped by this term
    * @return the Term
    */
-  Term(const CVC4::Expr& e);
+  Term(const Solver* slv, const CVC4::Expr& e);
 
   /**
    * Constructor.
@@ -884,6 +900,13 @@ class CVC4_PUBLIC Term
   bool isConst() const;
 
   /**
+   *  Return the base (element stored at all indices) of a constant array
+   *  throws an exception if the kind is not CONST_ARRAY
+   *  @return the base value
+   */
+  Term getConstArrayBase() const;
+
+  /**
    * Boolean negation.
    * @return the Boolean negation of this term
    */
@@ -955,10 +978,13 @@ class CVC4_PUBLIC Term
 
     /**
      * Constructor
+     * @param slv the associated solver object
      * @param e a shared pointer to the expression that we're iterating over
      * @param p the position of the iterator (e.g. which child it's on)
      */
-    const_iterator(const std::shared_ptr<CVC4::Expr>& e, uint32_t p);
+    const_iterator(const Solver* slv,
+                   const std::shared_ptr<CVC4::Expr>& e,
+                   uint32_t p);
 
     /**
      * Copy constructor.
@@ -1005,6 +1031,10 @@ class CVC4_PUBLIC Term
     Term operator*() const;
 
    private:
+    /**
+     * The associated solver object.
+     */
+    const Solver* d_solver;
     /* The original expression to be iterated over */
     std::shared_ptr<CVC4::Expr> d_orig_expr;
     /* Keeps track of the iteration position */
@@ -1025,6 +1055,12 @@ class CVC4_PUBLIC Term
   // to the new API. !!!
   CVC4::Expr getExpr(void) const;
 
+ protected:
+  /**
+   * The associated solver object.
+   */
+  const Solver* d_solver;
+
  private:
   /**
    * Helper for isNull checks. This prevents calling an API function with
@@ -1138,14 +1174,13 @@ class DatatypeIterator;
 class CVC4_PUBLIC DatatypeConstructorDecl
 {
   friend class DatatypeDecl;
+  friend class Solver;
 
  public:
   /**
-   * Constructor.
-   * @param name the name of the datatype constructor
-   * @return the DatatypeConstructorDecl
+   * Nullary constructor for Cython.
    */
-  DatatypeConstructorDecl(const std::string& name);
+  DatatypeConstructorDecl();
 
   /**
    * Add datatype selector declaration.
@@ -1170,6 +1205,19 @@ class CVC4_PUBLIC DatatypeConstructorDecl
 
  private:
   /**
+   * Constructor.
+   * @param slv the associated solver object
+   * @param name the name of the datatype constructor
+   * @return the DatatypeConstructorDecl
+   */
+  DatatypeConstructorDecl(const Solver* slv, const std::string& name);
+
+  /**
+   * The associated solver object.
+   */
+  const Solver* d_solver;
+
+  /**
    * The internal (intermediate) datatype constructor wrapped by this
    * datatype constructor declaration.
    * This is a shared_ptr rather than a unique_ptr since
@@ -1190,7 +1238,7 @@ class CVC4_PUBLIC DatatypeDecl
 
  public:
   /**
-   * Nullary constructor for Cython
+   * Nullary constructor for Cython.
    */
   DatatypeDecl();
 
@@ -1211,6 +1259,9 @@ class CVC4_PUBLIC DatatypeDecl
   /** Is this Datatype declaration parametric? */
   bool isParametric() const;
 
+  /**
+   * @return true if this DatatypeDecl is a null object
+   */
   bool isNull() const;
 
   /**
@@ -1228,24 +1279,24 @@ class CVC4_PUBLIC DatatypeDecl
  private:
   /**
    * Constructor.
-   * @param s the solver that created this datatype declaration
+   * @param slv the associated solver object
    * @param name the name of the datatype
    * @param isCoDatatype true if a codatatype is to be constructed
    * @return the DatatypeDecl
    */
-  DatatypeDecl(const Solver* s,
+  DatatypeDecl(const Solver* slv,
                const std::string& name,
                bool isCoDatatype = false);
 
   /**
    * Constructor for parameterized datatype declaration.
    * Create sorts parameter with Solver::mkParamSort().
-   * @param s the solver that created this datatype declaration
+   * @param slv the associated solver object
    * @param name the name of the datatype
    * @param param the sort parameter
    * @param isCoDatatype true if a codatatype is to be constructed
    */
-  DatatypeDecl(const Solver* s,
+  DatatypeDecl(const Solver* slv,
                const std::string& name,
                Sort param,
                bool isCoDatatype = false);
@@ -1253,19 +1304,27 @@ class CVC4_PUBLIC DatatypeDecl
   /**
    * Constructor for parameterized datatype declaration.
    * Create sorts parameter with Solver::mkParamSort().
-   * @param s the solver that created this datatype declaration
+   * @param slv the associated solver object
    * @param name the name of the datatype
    * @param params a list of sort parameters
    * @param isCoDatatype true if a codatatype is to be constructed
    */
-  DatatypeDecl(const Solver* s,
+  DatatypeDecl(const Solver* slv,
                const std::string& name,
                const std::vector<Sort>& params,
                bool isCoDatatype = false);
 
-  // helper for isNull() to avoid calling API functions from other API functions
+  /**
+   * Helper for isNull checks. This prevents calling an API function with
+   * CVC4_API_CHECK_NOT_NULL
+   */
   bool isNullHelper() const;
 
+  /**
+   * The associated solver object.
+   */
+  const Solver* d_solver;
+
   /* The internal (intermediate) datatype wrapped by this datatype
    * declaration
    * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
@@ -1292,10 +1351,11 @@ class CVC4_PUBLIC DatatypeSelector
   // migrated to the new API. !!!
   /**
    * Constructor.
+   * @param slv the associated solver object
    * @param stor the internal datatype selector to be wrapped
    * @return the DatatypeSelector
    */
-  DatatypeSelector(const CVC4::DatatypeConstructorArg& stor);
+  DatatypeSelector(const Solver* slv, const CVC4::DatatypeConstructorArg& stor);
 
   /**
    * Destructor.
@@ -1325,6 +1385,11 @@ class CVC4_PUBLIC DatatypeSelector
 
  private:
   /**
+   * The associated solver object.
+   */
+  const Solver* d_solver;
+
+  /**
    * The internal datatype selector wrapped by this datatype selector.
    * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
    * not ref counted.
@@ -1353,7 +1418,7 @@ class CVC4_PUBLIC DatatypeConstructor
    * @param ctor the internal datatype constructor to be wrapped
    * @return the DatatypeConstructor
    */
-  DatatypeConstructor(const CVC4::DatatypeConstructor& ctor);
+  DatatypeConstructor(const Solver* slv, const CVC4::DatatypeConstructor& ctor);
 
   /**
    * Destructor.
@@ -1466,16 +1531,27 @@ class CVC4_PUBLIC DatatypeConstructor
    private:
     /**
      * Constructor.
+     * @param slv the associated Solver object
      * @param ctor the internal datatype constructor to iterate over
      * @param true if this is a begin() iterator
      */
-    const_iterator(const CVC4::DatatypeConstructor& ctor, bool begin);
+    const_iterator(const Solver* slv,
+                   const CVC4::DatatypeConstructor& ctor,
+                   bool begin);
+
+    /**
+     * The associated solver object.
+     */
+    const Solver* d_solver;
+
     /* A pointer to the list of selectors of the internal datatype
      * constructor to iterate over.
      * This pointer is maintained for operators == and != only. */
     const void* d_int_stors;
+
     /* The list of datatype selector (wrappers) to iterate over. */
     std::vector<DatatypeSelector> d_stors;
+
     /* The current index of the iterator. */
     size_t d_idx;
   };
@@ -1501,6 +1577,12 @@ class CVC4_PUBLIC DatatypeConstructor
    * @return the selector object for the name
    */
   DatatypeSelector getSelectorForName(const std::string& name) const;
+
+  /**
+   * The associated solver object.
+   */
+  const Solver* d_solver;
+
   /**
    * The internal datatype constructor wrapped by this datatype constructor.
    * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
@@ -1525,7 +1607,7 @@ class CVC4_PUBLIC Datatype
    * @param dtype the internal datatype to be wrapped
    * @return the Datatype
    */
-  Datatype(const CVC4::Datatype& dtype);
+  Datatype(const Solver* slv, const CVC4::Datatype& dtype);
 
   // Nullary constructor for Cython
   Datatype();
@@ -1591,6 +1673,17 @@ class CVC4_PUBLIC Datatype
   bool isWellFounded() const;
 
   /**
+   * Does this datatype have nested recursion? This method returns false if a
+   * value of this datatype includes a subterm of its type that is nested
+   * beneath a non-datatype type constructor. For example, a datatype
+   * T containing a constructor having a selector with range type (Set T) has
+   * nested recursion.
+   *
+   * @return true if this datatype has nested recursion
+   */
+  bool hasNestedRecursion() const;
+
+  /**
    * @return a string representation of this datatype
    */
   std::string toString() const;
@@ -1654,16 +1747,25 @@ class CVC4_PUBLIC Datatype
    private:
     /**
      * Constructor.
+     * @param slv the associated Solver object
      * @param dtype the internal datatype to iterate over
      * @param true if this is a begin() iterator
      */
-    const_iterator(const CVC4::Datatype& dtype, bool begin);
+    const_iterator(const Solver* slv, const CVC4::Datatype& dtype, bool begin);
+
+    /**
+     * The associated solver object.
+     */
+    const Solver* d_solver;
+
     /* A pointer to the list of constructors of the internal datatype
      * to iterate over.
      * This pointer is maintained for operators == and != only. */
     const void* d_int_ctors;
+
     /* The list of datatype constructor (wrappers) to iterate over. */
     std::vector<DatatypeConstructor> d_ctors;
+
     /* The current index of the iterator. */
     size_t d_idx;
   };
@@ -1689,6 +1791,12 @@ class CVC4_PUBLIC Datatype
    * @return the constructor object for the name
    */
   DatatypeConstructor getConstructorForName(const std::string& name) const;
+
+  /**
+   * The associated solver object.
+   */
+  const Solver* d_solver;
+
   /**
    * The internal datatype wrapped by this datatype.
    * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
@@ -1793,11 +1901,11 @@ class CVC4_PUBLIC Grammar
  private:
   /**
    * Constructor.
-   * @param s the solver that created this grammar
+   * @param slv the solver that created this grammar
    * @param sygusVars the input variables to synth-fun/synth-var
    * @param ntSymbols the non-terminals of this grammar
    */
-  Grammar(const Solver* s,
+  Grammar(const Solver* slv,
           const std::vector<Term>& sygusVars,
           const std::vector<Term>& ntSymbols);
 
@@ -1863,7 +1971,7 @@ class CVC4_PUBLIC Grammar
   void addSygusConstructorVariables(DatatypeDecl& dt, Sort sort) const;
 
   /** The solver that created this grammar. */
-  const Solver* d_s;
+  const Solver* d_solver;
   /** Input variables to the corresponding function/invariant to synthesize.*/
   std::vector<Term> d_sygusVars;
   /** The non-terminal symbols of this grammar. */
@@ -2613,6 +2721,12 @@ class CVC4_PUBLIC Solver
   Term mkVar(Sort sort, const std::string& symbol = std::string()) const;
 
   /* .................................................................... */
+  /* Create datatype constructor declarations                             */
+  /* .................................................................... */
+
+  DatatypeConstructorDecl mkDatatypeConstructorDecl(const std::string& name);
+
+  /* .................................................................... */
   /* Create datatype declarations                                         */
   /* .................................................................... */
 
@@ -2746,12 +2860,15 @@ class CVC4_PUBLIC Solver
    * @param bound_vars the parameters to this function
    * @param sort the sort of the return value of this function
    * @param term the function body
+   * @param global determines whether this definition is global (i.e. persists
+   *               when popping the context)
    * @return the function
    */
   Term defineFun(const std::string& symbol,
                  const std::vector<Term>& bound_vars,
                  Sort sort,
-                 Term term) const;
+                 Term term,
+                 bool global = false) const;
   /**
    * Define n-ary function.
    * SMT-LIB: ( define-fun <function_def> )
@@ -2759,11 +2876,14 @@ class CVC4_PUBLIC Solver
    * @param fun the sorted function
    * @param bound_vars the parameters to this function
    * @param term the function body
+   * @param global determines whether this definition is global (i.e. persists
+   *               when popping the context)
    * @return the function
    */
   Term defineFun(Term fun,
                  const std::vector<Term>& bound_vars,
-                 Term term) const;
+                 Term term,
+                 bool global = false) const;
 
   /**
    * Define recursive function.
@@ -2772,12 +2892,15 @@ class CVC4_PUBLIC Solver
    * @param bound_vars the parameters to this function
    * @param sort the sort of the return value of this function
    * @param term the function body
+   * @param global determines whether this definition is global (i.e. persists
+   *               when popping the context)
    * @return the function
    */
   Term defineFunRec(const std::string& symbol,
                     const std::vector<Term>& bound_vars,
                     Sort sort,
-                    Term term) const;
+                    Term term,
+                    bool global = false) const;
 
   /**
    * Define recursive function.
@@ -2786,11 +2909,14 @@ class CVC4_PUBLIC Solver
    * @param fun the sorted function
    * @param bound_vars the parameters to this function
    * @param term the function body
+   * @param global determines whether this definition is global (i.e. persists
+   *               when popping the context)
    * @return the function
    */
   Term defineFunRec(Term fun,
                     const std::vector<Term>& bound_vars,
-                    Term term) const;
+                    Term term,
+                    bool global = false) const;
 
   /**
    * Define recursive functions.
@@ -2799,11 +2925,14 @@ class CVC4_PUBLIC Solver
    * @param funs the sorted functions
    * @param bound_vars the list of parameters to the functions
    * @param term the list of function bodies of the functions
+   * @param global determines whether this definition is global (i.e. persists
+   *               when popping the context)
    * @return the function
    */
   void defineFunsRec(const std::vector<Term>& funs,
                      const std::vector<std::vector<Term>>& bound_vars,
-                     const std::vector<Term>& terms) const;
+                     const std::vector<Term>& terms,
+                     bool global = false) const;
 
   /**
    * Echo a given string to the given output stream.
@@ -2875,6 +3004,18 @@ class CVC4_PUBLIC Solver
   std::vector<Term> getValue(const std::vector<Term>& terms) const;
 
   /**
+   * When using separation logic, obtain the term for the heap.
+   * @return The term for the heap
+   */
+  Term getSeparationHeap() const;
+
+  /**
+   * When using separation logic, obtain the term for nil.
+   * @return The term for nil
+   */
+  Term getSeparationNilTerm() const;
+
+  /**
    * Pop (a) level(s) from the assertion stack.
    * SMT-LIB: ( pop <numeral> )
    * @param nscopes the number of levels to pop
@@ -2882,6 +3023,29 @@ class CVC4_PUBLIC Solver
   void pop(uint32_t nscopes = 1) const;
 
   /**
+   * Get an interpolant
+   * SMT-LIB: ( get-interpol <term> )
+   * Requires to enable option 'produce-interpols'.
+   * @param conj the conjecture term
+   * @param output a Term I such that A->I and I->B are valid, where A is the
+   *        current set of assertions and B is given in the input by conj.
+   * @return true if it gets I successfully, false otherwise.
+   */
+  bool getInterpolant(Term conj, Term& output) const;
+
+  /**
+   * Get an interpolant
+   * SMT-LIB: ( get-interpol <term> )
+   * Requires to enable option 'produce-interpols'.
+   * @param conj the conjecture term
+   * @param gtype the grammar for the interpolant I
+   * @param output a Term I such that A->I and I->B are valid, where A is the
+   *        current set of assertions and B is given in the input by conj.
+   * @return true if it gets I successfully, false otherwise.
+   */
+  bool getInterpolant(Term conj, const Type& gtype, Term& output) const;
+
+  /**
    * Print the model of a satisfiable query to the given output stream.
    * Requires to enable option 'produce-models'.
    * @param out the output stream
@@ -3142,9 +3306,11 @@ class CVC4_PUBLIC Solver
 // new API. !!!
 std::vector<Expr> termVectorToExprs(const std::vector<Term>& terms);
 std::vector<Type> sortVectorToTypes(const std::vector<Sort>& sorts);
-std::vector<Term> exprVectorToTerms(const std::vector<Expr>& terms);
-std::vector<Sort> typeVectorToSorts(const std::vector<Type>& sorts);
 std::set<Type> sortSetToTypes(const std::set<Sort>& sorts);
+std::vector<Term> exprVectorToTerms(const Solver* slv,
+                                    const std::vector<Expr>& terms);
+std::vector<Sort> typeVectorToSorts(const Solver* slv,
+                                    const std::vector<Type>& sorts);
 
 }  // namespace api