From d95e5257f452d765aa67931f0b2af7b178f2e986 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 23 Mar 2018 12:20:23 -0500 Subject: [PATCH] Enable post-condition strenghtening by default for non-syntax restricted invariant synthesis (#1703) --- src/options/quantifiers_options.toml | 13 +++++++-- .../sygus/ce_guided_single_inv.cpp | 29 +++++++++++++++++-- .../quantifiers/sygus/sygus_grammar_cons.cpp | 19 ++++++++++++ .../quantifiers/sygus/sygus_grammar_cons.h | 8 ++++- 4 files changed, 63 insertions(+), 6 deletions(-) diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 8f07384d6..ab74fbc79 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1017,11 +1017,20 @@ header = "options/quantifiers_options.h" category = "regular" long = "sygus-inv-templ=MODE" type = "CVC4::theory::quantifiers::SygusInvTemplMode" - default = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE" + default = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST" handler = "stringToSygusInvTemplMode" includes = ["options/quantifiers_modes.h"] read_only = true - help = "template mode for sygus invariant synthesis" + help = "template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)" + +[[option]] + name = "sygusInvTemplWhenSyntax" + category = "regular" + long = "sygus-inv-templ-when-sg" + type = "bool" + default = "false" + read_only = false + help = "use invariant templates (with solution reconstruction) for syntax guided problems" [[option]] name = "sygusInvAutoUnfold" diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index d59f1f370..a951ec867 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -16,6 +16,7 @@ #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" +#include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" @@ -154,7 +155,26 @@ void CegConjectureSingleInv::initialize( Node q ) { //check if it is single invocation if (!d_sip->isPurelySingleInvocation()) { - if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){ + SygusInvTemplMode tmode = options::sygusInvTemplMode(); + if (tmode != SYGUS_INV_TEMPL_MODE_NONE) + { + // currently only works for single predicate synthesis + if (q[0].getNumChildren() > 1 || !q[0][0].getType().isPredicate()) + { + tmode = SYGUS_INV_TEMPL_MODE_NONE; + } + else if (!options::sygusInvTemplWhenSyntax()) + { + // only use invariant templates if no syntactic restrictions + if (CegGrammarConstructor::hasSyntaxRestrictions(q)) + { + tmode = SYGUS_INV_TEMPL_MODE_NONE; + } + } + } + + if (tmode != SYGUS_INV_TEMPL_MODE_NONE) + { //if we are doing invariant templates, then construct the template Trace("cegqi-si") << "- Do transition inference..." << std::endl; d_ti[q].process( qq ); @@ -234,12 +254,15 @@ void CegConjectureSingleInv::initialize( Node q ) { } } } + Trace("cegqi-inv") << "Make the template... " << tmode << " " + << templ << std::endl; if( templ.isNull() ){ - if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){ + if (tmode == SYGUS_INV_TEMPL_MODE_PRE) + { //d_templ[prog] = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant ), d_trans_post[prog] ); templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], d_templ_arg[prog] ); }else{ - Assert( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST ); + Assert(tmode == SYGUS_INV_TEMPL_MODE_POST); //d_templ[prog] = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant ) ); templ = NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], d_templ_arg[prog] ); } diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 1ca774c5d..08b0dc837 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -36,6 +36,25 @@ CegGrammarConstructor::CegGrammarConstructor(QuantifiersEngine* qe, { } +bool CegGrammarConstructor::hasSyntaxRestrictions(Node q) +{ + Assert(q.getKind() == FORALL); + for (const Node& f : q[0]) + { + Node gv = f.getAttribute(SygusSynthGrammarAttribute()); + if (!gv.isNull()) + { + TypeNode tn = gv.getType(); + if (tn.isDatatype() + && static_cast(tn.toType()).getDatatype().isSygus()) + { + return true; + } + } + } + return false; +} + void CegGrammarConstructor::collectTerms( Node n, std::map< TypeNode, std::vector< Node > >& consts ){ std::unordered_map visited; std::unordered_map::iterator it; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 4e486f88f..d8a77848b 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -83,7 +83,13 @@ public: * fun is for naming */ static TypeNode mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun ); -private: + /** + * Returns true iff there are syntax restrictions on the + * functions-to-synthesize of sygus conjecture q. + */ + static bool hasSyntaxRestrictions(Node q); + + private: /** reference to quantifier engine */ QuantifiersEngine * d_qe; /** parent conjecture -- 2.30.2