From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 4 Nov 2021 23:50:55 +0000 (-0500)
Subject: Add -o sygus-grammar to print auto-generated SyGuS grammars (#7573)
X-Git-Tag: cvc5-1.0.0~887
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f9d59828ebd150797682f1fbf5267aca7d15bb54;p=cvc5.git

Add -o sygus-grammar to print auto-generated SyGuS grammars (#7573)

Fixes #5341.
---

diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index ec3bd870d..8255da027 100644
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -169,6 +169,11 @@ name   = "Base"
   help = "print enumerated terms and candidates generated by the sygus solver"
   description = "With ``-o sygus``, cvc5 prints information about the internal SyGuS solver including enumerated terms and generated candidates."
   example-file = "regress0/sygus/print-debug.sy"
+[[option.mode.SYGUS_GRAMMAR]]
+  name = "sygus-grammar"
+  help = "print grammars automatically generated by the sygus solver"
+  description = "With ``-o sygus-grammar``, cvc5 prints the grammar it generates for a function-to-synthesize when no grammar was provided."
+  example-file = "regress0/sygus/print-grammar.sy"
 [[option.mode.TRIGGER]]
   name = "trigger"
   help = "print selected triggers for quantified formulas"
@@ -242,4 +247,4 @@ name   = "Base"
 [[option]]
   name       = "resourceWeightHolder"
   category   = "undocumented"
-  type       = "std::vector<std::string>"
\ No newline at end of file
+  type       = "std::vector<std::string>"
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 51458d66e..e68570919 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1772,8 +1772,9 @@ void Smt2Printer::toStreamCmdEcho(std::ostream& out,
    --------------------------------------------------------------------------
 */
 
-static void toStreamSygusGrammar(std::ostream& out, const TypeNode& t)
+std::string Smt2Printer::sygusGrammarString(const TypeNode& t)
 {
+  std::stringstream out;
   if (!t.isNull() && t.isDatatype() && t.getDType().isSygus())
   {
     std::stringstream types_predecl, types_list;
@@ -1828,6 +1829,7 @@ static void toStreamSygusGrammar(std::ostream& out, const TypeNode& t)
 
     out << "\n(" << types_predecl.str() << ")\n(" << types_list.str() << ')';
   }
+  return out.str();
 }
 
 void Smt2Printer::toStreamCmdSynthFun(std::ostream& out,
@@ -1861,7 +1863,7 @@ void Smt2Printer::toStreamCmdSynthFun(std::ostream& out,
   // print grammar, if any
   if (!sygusType.isNull())
   {
-    toStreamSygusGrammar(out, sygusType);
+    out << sygusGrammarString(sygusType);
   }
   out << ')' << std::endl;
 }
@@ -1903,8 +1905,7 @@ void Smt2Printer::toStreamCmdGetInterpol(std::ostream& out,
   out << "(get-interpol " << cvc5::quoteSymbol(name) << ' ' << conj;
   if (!sygusType.isNull())
   {
-    out << ' ';
-    toStreamSygusGrammar(out, sygusType);
+    out << ' ' << sygusGrammarString(sygusType);
   }
   out << ')' << std::endl;
 }
@@ -1921,7 +1922,7 @@ void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out,
   // print grammar, if any
   if (!sygusType.isNull())
   {
-    toStreamSygusGrammar(out, sygusType);
+    out << sygusGrammarString(sygusType);
   }
   out << ')' << std::endl;
 }
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 2af17ed59..4ee333f67 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -247,6 +247,10 @@ class Smt2Printer : public cvc5::Printer
    * the SMT-LIB format (with variant v).
    */
   static std::string smtKindString(Kind k, Variant v = smt2_6_variant);
+  /**
+   * Get the string corresponding to the sygus datatype t printed as a grammar.
+   */
+  static std::string sygusGrammarString(const TypeNode& t);
 
  private:
   /**
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index fce0b9f38..a9b5ed9c6 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -21,6 +21,7 @@
 #include "expr/ascription_type.h"
 #include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
+#include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
@@ -34,6 +35,7 @@
 #include "theory/strings/word.h"
 #include "util/floatingpoint.h"
 #include "util/string.h"
+#include "printer/smt2/smt2_printer.h"
 
 using namespace cvc5::kind;
 
@@ -41,9 +43,10 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-CegGrammarConstructor::CegGrammarConstructor(TermDbSygus* tds,
+CegGrammarConstructor::CegGrammarConstructor(Env& env,
+                                             TermDbSygus* tds,
                                              SynthConjecture* p)
-    : d_tds(tds), d_parent(p), d_is_syntax_restricted(false)
+    : EnvObj(env), d_tds(tds), d_parent(p), d_is_syntax_restricted(false)
 {
 }
 
@@ -170,6 +173,14 @@ Node CegGrammarConstructor::process(Node q,
                               exc_cons,
                               inc_cons,
                               term_irlv);
+      // print the grammar
+      if (isOutputOn(OutputTag::SYGUS_GRAMMAR))
+      {
+        output(OutputTag::SYGUS_GRAMMAR)
+            << "(sygus-grammar " << ss.str()
+            << printer::smt2::Smt2Printer::sygusGrammarString(tn) << ")"
+            << std::endl;
+      }
     }
     // sfvl may be null for constant synthesis functions
     Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is "
@@ -231,7 +242,7 @@ Node CegGrammarConstructor::process(Node q,
       Assert(!templ_arg.isNull());
       // if there is a template for this argument, make a sygus type on top of
       // it
-      if (!options::sygusTemplEmbedGrammar())
+      if (!options().quantifiers.sygusTemplEmbedGrammar)
       {
         // otherwise, apply it as a preprocessing pass
         Trace("cegqi-debug") << "Template for " << sf << " is : " << templ
@@ -272,7 +283,7 @@ Node CegGrammarConstructor::process(Node q,
   qchildren.push_back(nm->mkNode(kind::BOUND_VAR_LIST, ebvl));
   if( qbody_subs!=q[1] ){
     Trace("cegqi") << "...rewriting : " << qbody_subs << std::endl;
-    qbody_subs = Rewriter::rewrite( qbody_subs );
+    qbody_subs = rewrite(qbody_subs);
     Trace("cegqi") << "...got : " << qbody_subs << std::endl;
   }
   qchildren.push_back(convertToEmbedding(qbody_subs));
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index a743bed2f..b8c782431 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -25,6 +25,7 @@
 #include "expr/attribute.h"
 #include "expr/node.h"
 #include "expr/sygus_datatype.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 namespace theory {
@@ -58,10 +59,10 @@ class TermDbSygus;
  * Utility for constructing datatypes that correspond to syntactic restrictions,
  * and applying the deep embedding from Section 4 of Reynolds et al CAV 2015.
  */
-class CegGrammarConstructor
+class CegGrammarConstructor : protected EnvObj
 {
 public:
- CegGrammarConstructor(TermDbSygus* tds, SynthConjecture* p);
+ CegGrammarConstructor(Env& env, TermDbSygus* tds, SynthConjecture* p);
  ~CegGrammarConstructor() {}
  /** process
   *
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 1fde43913..d068438ba 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -62,7 +62,7 @@ SynthConjecture::SynthConjecture(Env& env,
       d_ceg_si(new CegSingleInv(env, tr, s)),
       d_templInfer(new SygusTemplateInfer),
       d_ceg_proc(new SynthConjectureProcess),
-      d_ceg_gc(new CegGrammarConstructor(d_tds, this)),
+      d_ceg_gc(new CegGrammarConstructor(env, d_tds, this)),
       d_sygus_rconst(new SygusRepairConst(env, d_tds)),
       d_exampleInfer(new ExampleInfer(d_tds)),
       d_ceg_pbe(new SygusPbe(env, qs, qim, d_tds, this)),
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3bd5e33f0..25f61c27c 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1308,6 +1308,7 @@ set(regress_0_tests
   regress0/sygus/pLTL-sygus-syntax-err.sy
   regress0/sygus/print-debug.sy
   regress0/sygus/print-define-fun.sy
+  regress0/sygus/print-grammar.sy
   regress0/sygus/real-si-all.sy
   regress0/sygus/setFeature.sy
   regress0/sygus/strings-unconstrained.sy
diff --git a/test/regress/regress0/sygus/print-grammar.sy b/test/regress/regress0/sygus/print-grammar.sy
new file mode 100644
index 000000000..0db057a71
--- /dev/null
+++ b/test/regress/regress0/sygus/print-grammar.sy
@@ -0,0 +1,16 @@
+; REQUIRES: no-competition
+; COMMAND-LINE: -o sygus-grammar
+; EXPECT: (sygus-grammar f
+; EXPECT: ((f_Int Int) (f_Bool Bool) )
+; EXPECT: ((f_Int Int ((Constant Int) x y 0 1 (+ f_Int f_Int) (- f_Int f_Int) (ite f_Bool f_Int f_Int) ))
+; EXPECT: (f_Bool Bool ((Constant Bool) true false (= f_Int f_Int) (<= f_Int f_Int) (not f_Bool) (and f_Bool f_Bool) (or f_Bool f_Bool) ))
+; EXPECT: ))
+; EXPECT: (
+; EXPECT: (define-fun f ((x Int) (y Int)) Int 0)
+; EXPECT: )
+
+(set-logic LIA)
+
+(synth-fun f ((x Int) (y Int)) Int)
+
+(check-synth)