Introducing internal commands for SyGuS commands (#2627)

1 files changed, 233 insertions, 7 deletions

diff --git a/src/smt/command.h b/src/smt/command.h
index be6d84305..f7824c1aa 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -613,29 +613,255 @@ class CVC4_PUBLIC QueryCommand : public Command
   std::string getCommandName() const override;
 }; /* class QueryCommand */
 
-class CVC4_PUBLIC CheckSynthCommand : public Command
+/* ------------------- sygus commands  ------------------ */
+
+/** Declares a sygus universal variable */
+class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand
+{
+ public:
+  DeclareSygusVarCommand(const std::string& id, Expr var, Type type);
+  /** returns the declared variable */
+  Expr getVar() const;
+  /** returns the declared variable's type */
+  Type getType() const;
+  /** invokes this command
+   *
+   * The declared sygus variable is communicated to the SMT engine in case a
+   * synthesis conjecture is built later on.
+   */
+  void invoke(SmtEngine* smtEngine) override;
+  /** exports command to given expression manager */
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  /** creates a copy of this command */
+  Command* clone() const override;
+  /** returns this command's name */
+  std::string getCommandName() const override;
+
+ protected:
+  /** the declared variable */
+  Expr d_var;
+  /** the declared variable's type */
+  Type d_type;
+};
+
+/** Declares a sygus primed variable, for invariant problems
+ *
+ * We do not actually build expressions for the declared variables because they
+ * are unnecessary for building SyGuS problems.
+ */
+class CVC4_PUBLIC DeclareSygusPrimedVarCommand
+    : public DeclarationDefinitionCommand
+{
+ public:
+  DeclareSygusPrimedVarCommand(const std::string& id, Type type);
+  /** returns the declared primed variable's type */
+  Type getType() const;
+
+  /** invokes this command
+   *
+   * The type of the primed variable is communicated to the SMT engine for
+   * debugging purposes when a synthesis conjecture is built later on.
+   */
+  void invoke(SmtEngine* smtEngine) override;
+  /** exports command to given expression manager */
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  /** creates a copy of this command */
+  Command* clone() const override;
+  /** returns this command's name */
+  std::string getCommandName() const override;
+
+ protected:
+  /** the type of the declared primed variable */
+  Type d_type;
+};
+
+/** Declares a sygus universal function variable */
+class CVC4_PUBLIC DeclareSygusFunctionCommand
+    : public DeclarationDefinitionCommand
+{
+ public:
+  DeclareSygusFunctionCommand(const std::string& id, Expr func, Type type);
+  /** returns the declared function variable */
+  Expr getFunction() const;
+  /** returns the declared function variable's type */
+  Type getType() const;
+  /** invokes this command
+   *
+   * The declared sygus function variable is communicated to the SMT engine in
+   * case a synthesis conjecture is built later on.
+   */
+  void invoke(SmtEngine* smtEngine) override;
+  /** exports command to given expression manager */
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  /** creates a copy of this command */
+  Command* clone() const override;
+  /** returns this command's name */
+  std::string getCommandName() const override;
+
+ protected:
+  /** the declared function variable */
+  Expr d_func;
+  /** the declared function variable's type */
+  Type d_type;
+};
+
+/** Declares a sygus function-to-synthesize
+ *
+ * This command is also used for the special case in which we are declaring an
+ * invariant-to-synthesize
+ */
+class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand
 {
  public:
-  CheckSynthCommand();
-  CheckSynthCommand(const Expr& expr);
+  SynthFunCommand(const std::string& id,
+                  Expr func,
+                  Type sygusType,
+                  bool isInv,
+                  const std::vector<Expr>& vars);
+  SynthFunCommand(const std::string& id, Expr func, Type sygusType, bool isInv);
+  /** returns the function-to-synthesize */
+  Expr getFunction() const;
+  /** returns the input variables of the function-to-synthesize */
+  const std::vector<Expr>& getVars() const;
+  /** returns the sygus type of the function-to-synthesize */
+  Type getSygusType() const;
+  /** returns whether the function-to-synthesize should be an invariant */
+  bool isInv() const;
+
+  /** invokes this command
+   *
+   * The declared function-to-synthesize is communicated to the SMT engine in
+   * case a synthesis conjecture is built later on.
+   */
+  void invoke(SmtEngine* smtEngine) override;
+  /** exports command to given expression manager */
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  /** creates a copy of this command */
+  Command* clone() const override;
+  /** returns this command's name */
+  std::string getCommandName() const override;
+
+ protected:
+  /** the function-to-synthesize */
+  Expr d_func;
+  /** sygus type of the function-to-synthesize
+   *
+   * If this type is a "sygus datatype" then it encodes a grammar for the
+   * possible varlues of the function-to-sytnhesize
+   */
+  Type d_sygusType;
+  /** whether the function-to-synthesize should be an invariant */
+  bool d_isInv;
+  /** the input variables of the function-to-synthesize */
+  std::vector<Expr> d_vars;
+};
 
+/** Declares a sygus constraint */
+class CVC4_PUBLIC SygusConstraintCommand : public Command
+{
+ public:
+  SygusConstraintCommand(const Expr& e);
+  /** returns the declared constraint */
   Expr getExpr() const;
-  Result getResult() const;
+  /** invokes this command
+   *
+   * The declared constraint is communicated to the SMT engine in case a
+   * synthesis conjecture is built later on.
+   */
   void invoke(SmtEngine* smtEngine) override;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  /** exports command to given expression manager */
   Command* exportTo(ExprManager* exprManager,
                     ExprManagerMapCollection& variableMap) override;
+  /** creates a copy of this command */
   Command* clone() const override;
+  /** returns this command's name */
   std::string getCommandName() const override;
 
  protected:
-  /** the assertion of check-synth */
+  /** the declared constraint */
   Expr d_expr;
+};
+
+/** Declares a sygus invariant constraint
+ *
+ * Invarint constraints are declared in a somewhat implicit manner in the SyGuS
+ * language: they are declared in terms of the previously declared
+ * invariant-to-synthesize, precondition, transition relation and condition.
+ *
+ * The actual constraint must be built such that the invariant is not stronger
+ * than the precondition, not weaker than the postcondition and inductive
+ * w.r.t. the transition relation.
+ */
+class CVC4_PUBLIC SygusInvConstraintCommand : public Command
+{
+ public:
+  SygusInvConstraintCommand(const std::vector<Expr>& predicates);
+  SygusInvConstraintCommand(const Expr& inv,
+                            const Expr& pre,
+                            const Expr& trans,
+                            const Expr& post);
+  /** returns the place holder predicates */
+  const std::vector<Expr>& getPredicates() const;
+  /** invokes this command
+   *
+   * The place holders are communicated to the SMT engine and the actual
+   * invariant constraint is built, in case an actual synthesis conjecture is
+   * built later on.
+   */
+  void invoke(SmtEngine* smtEngine) override;
+  /** exports command to given expression manager */
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  /** creates a copy of this command */
+  Command* clone() const override;
+  /** returns this command's name */
+  std::string getCommandName() const override;
+
+ protected:
+  /** the place holder predicates with which to build the actual constraint
+   * (i.e. the invariant, precondition, transition relation and postcondition)
+   */
+  std::vector<Expr> d_predicates;
+};
+
+/** Declares a synthesis conjecture */
+class CVC4_PUBLIC CheckSynthCommand : public Command
+{
+ public:
+  CheckSynthCommand(){};
+  /** returns the result of the check-synth call */
+  Result getResult() const;
+  /** prints the result of the check-synth-call */
+  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  /** invokes this command
+   *
+   * This invocation makes the SMT engine build a synthesis conjecture based on
+   * previously declared information (such as universal variables,
+   * functions-to-synthesize and so on), set up attributes to guide the solving,
+   * and then perform a satisfiability check, whose result is stored in
+   * d_result.
+   */
+  void invoke(SmtEngine* smtEngine) override;
+  /** exports command to given expression manager */
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  /** creates a copy of this command */
+  Command* clone() const override;
+  /** returns this command's name */
+  std::string getCommandName() const override;
+
+ protected:
   /** result of the check-synth call */
   Result d_result;
   /** string stream that stores the output of the solution */
   std::stringstream d_solution;
-}; /* class CheckSynthCommand */
+};
+
+/* ------------------- sygus commands  ------------------ */
 
 // this is TRANSFORM in the CVC presentation language
 class CVC4_PUBLIC SimplifyCommand : public Command