From 0834e9e263b1ecd014ef347d0f080ac1505fdcb4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 17 Jul 2018 17:37:03 +0200 Subject: [PATCH] sygusComp2018: update policies for solution reconstruction (#2109) --- src/options/options_handler.cpp | 58 +++++++++++++++++- src/options/options_handler.h | 3 + src/options/quantifiers_modes.h | 33 +++++++++- src/options/quantifiers_options.toml | 40 +++++++++---- .../sygus/ce_guided_conjecture.cpp | 2 +- .../sygus/ce_guided_single_inv.cpp | 43 +++++++------ .../quantifiers/sygus/ce_guided_single_inv.h | 16 +++-- .../sygus/ce_guided_single_inv_sol.cpp | 60 ++++++++++++------- .../sygus/ce_guided_single_inv_sol.h | 10 +++- .../quantifiers/sygus/sygus_grammar_cons.cpp | 17 ++---- .../quantifiers/sygus/sygus_grammar_cons.h | 2 - 11 files changed, 206 insertions(+), 78 deletions(-) diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 2b1d72802..8f179531b 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -489,6 +489,30 @@ all \n\ \n\ "; +const std::string OptionsHandler::s_cegqiSingleInvRconsHelp = + "\ +Modes for reconstruction solutions while using single invocation techniques,\ +supported by --cegqi-si-rcons:\n\ +\n\ +none \n\ ++ Do not try to reconstruct solutions in the original (user-provided) grammar\ + when using single invocation techniques. In this mode, solutions produced by\ + CVC4 may violate grammar restrictions.\n\ +\n\ +try \n\ ++ Try to reconstruct solutions in the original grammar when using single\ + invocation techniques in an incomplete (fail-fast) manner.\n\ +\n\ +all-limit \n\ ++ Try to reconstruct solutions in the original grammar, but termintate if a\ + maximum number of rounds for reconstruction is exceeded.\n\ +\n\ +all \n\ ++ Try to reconstruct solutions in the original grammar. In this mode,\ + we do not terminate until a solution is successfully reconstructed. \n\ +\n\ +"; + const std::string OptionsHandler::s_cegisSampleHelp = "\ Modes for sampling with counterexample-guided inductive synthesis (CEGIS),\ @@ -878,8 +902,6 @@ OptionsHandler::stringToCegqiSingleInvMode(std::string option, return theory::quantifiers::CEGQI_SI_MODE_NONE; } else if(optarg == "use" || optarg == "default") { return theory::quantifiers::CEGQI_SI_MODE_USE; - } else if(optarg == "all-abort") { - return theory::quantifiers::CEGQI_SI_MODE_ALL_ABORT; } else if(optarg == "all") { return theory::quantifiers::CEGQI_SI_MODE_ALL; } else if(optarg == "help") { @@ -891,6 +913,38 @@ OptionsHandler::stringToCegqiSingleInvMode(std::string option, } } +theory::quantifiers::CegqiSingleInvRconsMode +OptionsHandler::stringToCegqiSingleInvRconsMode(std::string option, + std::string optarg) +{ + if (optarg == "none") + { + return theory::quantifiers::CEGQI_SI_RCONS_MODE_NONE; + } + else if (optarg == "try") + { + return theory::quantifiers::CEGQI_SI_RCONS_MODE_TRY; + } + else if (optarg == "all") + { + return theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL; + } + else if (optarg == "all-limit") + { + return theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL_LIMIT; + } + else if (optarg == "help") + { + puts(s_cegqiSingleInvRconsHelp.c_str()); + exit(1); + } + else + { + throw OptionException(std::string("unknown option for --cegqi-si-rcons: `") + + optarg + "'. Try --cegqi-si-rcons help."); + } +} + theory::quantifiers::CegisSampleMode OptionsHandler::stringToCegisSampleMode( std::string option, std::string optarg) { diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 4cdd445ed..ab107ae78 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -108,6 +108,8 @@ public: std::string option, std::string optarg); theory::quantifiers::CegqiSingleInvMode stringToCegqiSingleInvMode( std::string option, std::string optarg); + theory::quantifiers::CegqiSingleInvRconsMode stringToCegqiSingleInvRconsMode( + std::string option, std::string optarg); theory::quantifiers::CegisSampleMode stringToCegisSampleMode( std::string option, std::string optarg); theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode( @@ -245,6 +247,7 @@ public: static const std::string s_sygusSolutionOutModeHelp; static const std::string s_cbqiBvIneqModeHelp; static const std::string s_cegqiSingleInvHelp; + static const std::string s_cegqiSingleInvRconsHelp; static const std::string s_cegisSampleHelp; static const std::string s_sygusInvTemplHelp; static const std::string s_termDbModeHelp; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index a949b97be..afb54002c 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -208,12 +208,41 @@ enum CegqiSingleInvMode { CEGQI_SI_MODE_NONE, /** use single invocation techniques */ CEGQI_SI_MODE_USE, - /** always use single invocation techniques, abort if solution reconstruction will fail */ - CEGQI_SI_MODE_ALL_ABORT, /** always use single invocation techniques */ CEGQI_SI_MODE_ALL, }; +/** Solution reconstruction modes for single invocation conjectures + * + * These modes indicate the policy when CVC4 solves a synthesis conjecture using + * single invocation techniques for a sygus problem with a user-specified + * grammar. + */ +enum CegqiSingleInvRconsMode +{ + /** + * Do not try to reconstruct solutions to single invocation conjectures. With + * this mode, solutions produced by CVC4 may violate grammar restrictions. + */ + CEGQI_SI_RCONS_MODE_NONE, + /** + * Try to reconstruct solution to single invocation conjectures in an + * incomplete (fail fast) way. + */ + CEGQI_SI_RCONS_MODE_TRY, + /** + * Reconstruct solutions to single invocation conjectures, but fail if we + * reach an upper limit on number of iterations in the enumeration + */ + CEGQI_SI_RCONS_MODE_ALL_LIMIT, + /** + * Reconstruct solutions to single invocation conjectures. This method + * relies on an expensive enumeration technique which only terminates when + * we succesfully reconstruct the solution, although it may not terminate. + */ + CEGQI_SI_RCONS_MODE_ALL, +}; + enum CegisSampleMode { /** do not use samples for CEGIS */ diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index ecdf87a47..bf514ada7 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -917,11 +917,30 @@ header = "options/quantifiers_options.h" [[option]] name = "cegqiSingleInvReconstruct" category = "regular" - long = "cegqi-si-reconstruct" + long = "cegqi-si-rcons=MODE" + type = "CVC4::theory::quantifiers::CegqiSingleInvRconsMode" + default = "CVC4::theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL_LIMIT" + handler = "stringToCegqiSingleInvRconsMode" + includes = ["options/quantifiers_modes.h"] + help = "policy for reconstructing solutions for single invocation conjectures" + +[[option]] + name = "cegqiSingleInvReconstructLimit" + category = "regular" + long = "cegqi-si-rcons-limit=N" + type = "int" + default = "10000" + read_only = true + help = "number of rounds of enumeration to use during solution reconstruction (negative means unlimited)" + +[[option]] + name = "cegqiSingleInvReconstructConst" + category = "regular" + long = "cegqi-si-reconstruct-const" type = "bool" default = "true" read_only = true - help = "reconstruct solutions for single invocation conjectures in original grammar" + help = "include constants when reconstruct solutions for single invocation conjectures in original grammar" [[option]] name = "cegqiSolMinCore" @@ -941,15 +960,6 @@ header = "options/quantifiers_options.h" read_only = true help = "minimize individual instantiations for single invocation conjectures based on unsat core" -[[option]] - name = "cegqiSingleInvReconstructConst" - category = "regular" - long = "cegqi-si-reconstruct-const" - type = "bool" - default = "true" - read_only = true - help = "include constants when reconstruct solutions for single invocation conjectures in original grammar" - [[option]] name = "cegqiSingleInvAbort" category = "regular" @@ -1118,6 +1128,14 @@ header = "options/quantifiers_options.h" includes = ["options/quantifiers_modes.h"] help = "mode for using samples in the counterexample-guided inductive synthesis loop" +[[option]] + name = "minSynthSol" + category = "regular" + long = "min-synth-sol" + type = "bool" + default = "true" + help = "Minimize synthesis solutions" + [[option]] name = "sygusEvalOpt" category = "regular" diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index 3bb0fc51a..bf973bd97 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -102,7 +102,7 @@ void CegConjecture::assign( Node q ) { // we now finalize the single invocation module, based on the syntax restrictions if (d_qe->getQuantAttributes()->isSygus(q)) { - d_ceg_si->finishInit( d_ceg_gc->isSyntaxRestricted(), d_ceg_gc->hasSyntaxITE() ); + d_ceg_si->finishInit(d_ceg_gc->isSyntaxRestricted()); } Assert( d_candidates.empty() ); diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index f568fcf3e..9a6fad52a 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -17,6 +17,7 @@ #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" @@ -49,7 +50,6 @@ CegConjectureSingleInv::CegConjectureSingleInv(QuantifiersEngine* qe, d_cosi(new CegqiOutputSingleInv(this)), d_cinst(NULL), d_c_inst_match_trie(NULL), - d_has_ites(true), d_single_invocation(false) { // third and fourth arguments set to (false,false) until we have solution // reconstruction for delta and infinity @@ -290,8 +290,9 @@ void CegConjectureSingleInv::initialize( Node q ) { } } -void CegConjectureSingleInv::finishInit( bool syntaxRestricted, bool hasItes ) { - d_has_ites = hasItes; +void CegConjectureSingleInv::finishInit(bool syntaxRestricted) +{ + Trace("cegqi-si-debug") << "Single invocation: finish init" << std::endl; // do not do single invocation if grammar is restricted and CEGQI_SI_MODE_ALL is not enabled if( options::cegqiSingleInvMode()==CEGQI_SI_MODE_USE && d_single_invocation && syntaxRestricted ){ d_single_invocation = false; @@ -458,13 +459,6 @@ struct sortSiInstanceIndices { Node CegConjectureSingleInv::postProcessSolution( Node n ){ - ////remove boolean ITE (not allowed for sygus comp 2015) - //if( n.getKind()==ITE && n.getType().isBoolean() ){ - // Node n1 = postProcessSolution( n[1] ); - // Node n2 = postProcessSolution( n[2] ); - // return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n[0], n1 ), - // NodeManager::currentNM()->mkNode( AND, n[0].negate(), n2 ) ); - //}else{ bool childChanged = false; Kind k = n.getKind(); if( n.getKind()==INTS_DIVISION_TOTAL ){ @@ -488,7 +482,6 @@ Node CegConjectureSingleInv::postProcessSolution( Node n ){ }else{ return n; } - //} } @@ -573,15 +566,34 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec //reconstruct the solution into sygus if necessary reconstructed = 0; - if( options::cegqiSingleInvReconstruct() && !dt.getSygusAllowAll() && !stn.isNull() && rconsSygus ){ + if (options::cegqiSingleInvReconstruct() != CEGQI_SI_RCONS_MODE_NONE + && !dt.getSygusAllowAll() && !stn.isNull() && rconsSygus) + { d_sol->preregisterConjecture( d_orig_conjecture ); - d_sygus_solution = d_sol->reconstructSolution( s, stn, reconstructed ); + int enumLimit = -1; + if (options::cegqiSingleInvReconstruct() == CEGQI_SI_RCONS_MODE_TRY) + { + enumLimit = 0; + } + else if (options::cegqiSingleInvReconstruct() + == CEGQI_SI_RCONS_MODE_ALL_LIMIT) + { + enumLimit = options::cegqiSingleInvReconstructLimit(); + } + d_sygus_solution = + d_sol->reconstructSolution(s, stn, reconstructed, enumLimit); if( reconstructed==1 ){ Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << d_sygus_solution << std::endl; } }else{ Trace("csi-sol") << "Post-process solution..." << std::endl; Node prev = d_solution; + if (options::minSynthSol()) + { + d_solution = + d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite( + d_solution); + } d_solution = postProcessSolution( d_solution ); if( prev!=d_solution ){ Trace("csi-sol") << "Solution (after post process) : " << d_solution << std::endl; @@ -631,11 +643,6 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec } bool CegConjectureSingleInv::needsCheck() { - if( options::cegqiSingleInvMode()==CEGQI_SI_MODE_ALL_ABORT ){ - if( !d_has_ites ){ - return d_inst.empty(); - } - } return true; } diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index b6fda18ed..b368a0689 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -146,9 +146,6 @@ class CegConjectureSingleInv { Node d_orig_solution; Node d_solution; Node d_sygus_solution; - // whether the grammar for our solution allows ITEs, this tells us when reconstruction is infeasible - bool d_has_ites; - public: // lemmas produced std::vector d_lemmas_produced; @@ -191,10 +188,13 @@ class CegConjectureSingleInv { void getInitialSingleInvLemma( std::vector< Node >& lems ); // initialize this class for synthesis conjecture q void initialize( Node q ); - // finish initialize, sets up final decisions about whether to use single invocation techniques - // syntaxRestricted is whether the syntax for solutions for the initialized conjecture is restricted - // hasItes is whether the syntax for solutions for the initialized conjecture allows ITEs - void finishInit( bool syntaxRestricted, bool hasItes ); + /** finish initialize + * + * This method sets up final decisions about whether to use single invocation + * techniques. The argument syntaxRestricted is whether the syntax for + * solutions for the initialized conjecture is restricted. + */ + void finishInit(bool syntaxRestricted); //check bool check( std::vector< Node >& lems ); //get solution @@ -202,8 +202,6 @@ class CegConjectureSingleInv { //reconstruct to syntax Node reconstructToSyntax( Node s, TypeNode stn, int& reconstructed, bool rconsSygus = true ); - // has ites - bool hasITEs() { return d_has_ites; } // is single invocation bool isSingleInvocation() const { return !d_single_inv.isNull(); } //needs check diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index 861d71946..44835cc26 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -639,7 +639,11 @@ void CegConjectureSingleInvSol::preregisterConjecture( Node q ) { registerEquivalentTerms( n ); } -Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int& reconstructed ) { +Node CegConjectureSingleInvSol::reconstructSolution(Node sol, + TypeNode stn, + int& reconstructed, + int enumLimit) +{ Trace("csi-rcons") << "Solution (pre-reconstruction) is : " << sol << std::endl; int status; d_root_id = collectReconstructNodes( sol, stn, status ); @@ -649,23 +653,34 @@ Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int Assert( !ret.isNull() ); reconstructed = 1; return ret; - }else{ - //Trace("csi-debug-sol") << "Induced solution template is : " << d_templ_solution << std::endl; - if( Trace.isOn("csi-rcons") ){ - for( std::map< TypeNode, std::map< Node, int > >::iterator it = d_rcons_to_id.begin(); it != d_rcons_to_id.end(); ++it ){ - TypeNode tn = it->first; - Assert( tn.isDatatype() ); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Trace("csi-rcons") << "Terms to reconstruct of type " << dt.getName() << " : " << std::endl; - for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - if( d_reconstruct.find( it2->second )==d_reconstruct.end() ){ - Trace("csi-rcons") << " " << it2->first << std::endl; - } + } + if (Trace.isOn("csi-rcons")) + { + for (std::map >::iterator it = + d_rcons_to_id.begin(); + it != d_rcons_to_id.end(); + ++it) + { + TypeNode tn = it->first; + Assert(tn.isDatatype()); + const Datatype& dt = static_cast(tn.toType()).getDatatype(); + Trace("csi-rcons") << "Terms to reconstruct of type " << dt.getName() + << " : " << std::endl; + for (std::map::iterator it2 = it->second.begin(); + it2 != it->second.end(); + ++it2) + { + if (d_reconstruct.find(it2->second) == d_reconstruct.end()) + { + Trace("csi-rcons") << " " << it2->first << std::endl; } - Assert( !it->second.empty() ); } + Assert(!it->second.empty()); } - unsigned index = 0; + } + if (enumLimit != 0) + { + int index = 0; std::map< TypeNode, bool > active; for( std::map< TypeNode, std::map< Node, int > >::iterator it = d_rcons_to_id.begin(); it != d_rcons_to_id.end(); ++it ){ active[it->first] = true; @@ -712,13 +727,16 @@ Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int if( index%100==0 ){ Trace("csi-rcons-stats") << "Tried " << index << " for each type." << std::endl; } - }while( !active.empty() ); - - // we ran out of elements, return null - reconstructed = -1; - Warning() << CommandFailure("Cannot get synth function: reconstruction to syntax failed."); - return Node::null(); // return sol; + } while (!active.empty() && (enumLimit < 0 || index < enumLimit)); } + + // we ran out of elements, return null + reconstructed = -1; + Warning() << CommandFailure( + "Cannot get synth function: reconstruction to syntax failed."); + // could return sol here, however, we choose to fail by returning null, since + // it indicates a failure. + return Node::null(); } int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, int& status ) { diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h index 0e5347f2e..8d18611cf 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h @@ -68,8 +68,16 @@ private: * matches the grammar corresponding to sygus datatype stn. * The value reconstructed is set to 1 if we successfully return a node, * otherwise it is set to -1. + * + * This method quickly tries to match sol to the grammar induced by stn. If + * this fails, we use enumerative techniques to try to repair the solution. + * The number of iterations for this enumeration is bounded by the argument + * enumLimit if it is positive, and unbounded otherwise. */ - Node reconstructSolution(Node sol, TypeNode stn, int& reconstructed); + Node reconstructSolution(Node sol, + TypeNode stn, + int& reconstructed, + int enumLimit); /** preregister conjecture * * q : the synthesis conjecture this class is for. diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 5bbd71fbe..efffa046f 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -33,7 +33,7 @@ namespace quantifiers { CegGrammarConstructor::CegGrammarConstructor(QuantifiersEngine* qe, CegConjecture* p) - : d_qe(qe), d_parent(p), d_is_syntax_restricted(false), d_has_ite(true) + : d_qe(qe), d_parent(p), d_is_syntax_restricted(false) { } @@ -198,6 +198,7 @@ Node CegGrammarConstructor::process(Node q, std::vector qchildren; Node qbody_subs = q[1]; std::map synth_fun_vars; + TermDbSygus* tds = d_qe->getTermDatabaseSygus(); for (unsigned i = 0, size = q[0].getNumChildren(); i < size; i++) { Node sf = q[0][i]; @@ -245,16 +246,10 @@ Node CegGrammarConstructor::process(Node q, Trace("cegqi-debug") << " body is now : " << qbody_subs << std::endl; } } - d_qe->getTermDatabaseSygus()->registerSygusType( tn ); - // check grammar restrictions - if( !d_qe->getTermDatabaseSygus()->sygusToBuiltinType( tn ).isBoolean() ){ - if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){ - d_has_ite = false; - } - } - Assert( tn.isDatatype() ); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Assert( dt.isSygus() ); + tds->registerSygusType(tn); + Assert(tn.isDatatype()); + const Datatype& dt = static_cast(tn.toType()).getDatatype(); + Assert(dt.isSygus()); if( !dt.getSygusAllowAll() ){ d_is_syntax_restricted = true; } diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index fcb4b3348..c99c431ea 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -62,8 +62,6 @@ public: const std::vector& ebvl); /** is the syntax restricted? */ bool isSyntaxRestricted() { return d_is_syntax_restricted; } - /** does the syntax allow ITE expressions? */ - bool hasSyntaxITE() { return d_has_ite; } /** make the default sygus datatype type corresponding to builtin type range * bvl is the set of free variables to include in the grammar * fun is for naming -- 2.30.2