From f9d59828ebd150797682f1fbf5267aca7d15bb54 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 4 Nov 2021 18:50:55 -0500 Subject: [PATCH] Add -o sygus-grammar to print auto-generated SyGuS grammars (#7573) Fixes #5341. --- src/options/base_options.toml | 7 ++++++- src/printer/smt2/smt2_printer.cpp | 11 ++++++----- src/printer/smt2/smt2_printer.h | 4 ++++ .../quantifiers/sygus/sygus_grammar_cons.cpp | 19 +++++++++++++++---- .../quantifiers/sygus/sygus_grammar_cons.h | 5 +++-- .../quantifiers/sygus/synth_conjecture.cpp | 2 +- test/regress/CMakeLists.txt | 1 + test/regress/regress0/sygus/print-grammar.sy | 16 ++++++++++++++++ 8 files changed, 52 insertions(+), 13 deletions(-) create mode 100644 test/regress/regress0/sygus/print-grammar.sy 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" \ No newline at end of file + type = "std::vector" 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) -- 2.30.2