Modify the smt2 parser to use the Sygus grammar. (#4829)

1 files changed, 48 insertions, 8 deletions

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 30a0ad0a7..5d14e76a1 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -46,6 +46,7 @@ class DatatypeConstructorArg;
 class ExprManager;
 class NodeManager;
 class SmtEngine;
+class SynthFunCommand;
 class Type;
 class Options;
 class Random;
@@ -1950,6 +1951,7 @@ std::ostream& operator<<(std::ostream& out,
 class CVC4_PUBLIC Grammar
 {
   friend class Solver;
+  friend class CVC4::SynthFunCommand;
 
  public:
   /**
@@ -1960,6 +1962,13 @@ class CVC4_PUBLIC Grammar
   void addRule(Term ntSymbol, Term rule);
 
   /**
+   * Add <rules> to the set of rules corresponding to <ntSymbol>.
+   * @param ntSymbol the non-terminal to which the rules are added
+   * @param rule the rules to add
+   */
+  void addRules(Term ntSymbol, std::vector<Term> rules);
+
+  /**
    * Allow <ntSymbol> to be an arbitrary constant.
    * @param ntSymbol the non-terminal allowed to be any constant
    */
@@ -1973,11 +1982,9 @@ class CVC4_PUBLIC Grammar
   void addAnyVariable(Term ntSymbol);
 
   /**
-   * Add <rules> to the set of rules corresponding to <ntSymbol>.
-   * @param ntSymbol the non-terminal to which the rules are added
-   * @param rule the rules to add
+   * @return a string representation of this grammar.
    */
-  void addRules(Term ntSymbol, std::vector<Term> rules);
+  std::string toString() const;
 
   /**
    * Nullary constructor. Needed for the Cython API.
@@ -2072,6 +2079,14 @@ class CVC4_PUBLIC Grammar
   bool d_isResolved;
 };
 
+/**
+ * Serialize a grammar to given stream.
+ * @param out the output stream
+ * @param g the grammar to be serialized to the given output stream
+ * @return the output stream
+ */
+std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC4_PUBLIC;
+
 /* -------------------------------------------------------------------------- */
 /* Rounding Mode for Floating Points                                          */
 /* -------------------------------------------------------------------------- */
@@ -3125,7 +3140,7 @@ class CVC4_PUBLIC Solver
 
   /**
    * Get an interpolant
-   * SMT-LIB: ( get-interpol <term> )
+   * SMT-LIB: ( get-interpol <conj> )
    * 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
@@ -3136,15 +3151,40 @@ class CVC4_PUBLIC Solver
 
   /**
    * Get an interpolant
-   * SMT-LIB: ( get-interpol <term> )
+   * SMT-LIB: ( get-interpol <conj> <g> )
    * Requires to enable option 'produce-interpols'.
    * @param conj the conjecture term
-   * @param gtype the grammar for the interpolant I
+   * @param g 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;
+  bool getInterpolant(Term conj, Grammar& g, Term& output) const;
+
+  /**
+   * Get an abduct.
+   * SMT-LIB: ( get-abduct <conj> )
+   * Requires enabling option 'produce-abducts'
+   * @param conj the conjecture term
+   * @param output a term C such that A^C is satisfiable, and A^~B^C is
+   *        unsatisfiable, where A is the current set of assertions and B is
+   *        given in the input by conj
+   * @return true if it gets C successfully, false otherwise
+   */
+  bool getAbduct(Term conj, Term& output) const;
+
+  /**
+   * Get an abduct.
+   * SMT-LIB: ( get-abduct <conj> <g> )
+   * Requires enabling option 'produce-abducts'
+   * @param conj the conjecture term
+   * @param g the grammar for the abduct C
+   * @param output a term C such that A^C is satisfiable, and A^~B^C is
+   *        unsatisfiable, where A is the current set of assertions and B is
+   *        given in the input by conj
+   * @return true if it gets C successfully, false otherwise
+   */
+  bool getAbduct(Term conj, Grammar& g, Term& output) const;
 
   /**
    * Print the model of a satisfiable query to the given output stream.