\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),\
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") {
}
}
+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)
{
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(
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;
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 */
[[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"
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"
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"
// 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() );
#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"
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
}
}
-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;
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 ){
}else{
return n;
}
- //}
}
//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;
}
bool CegConjectureSingleInv::needsCheck() {
- if( options::cegqiSingleInvMode()==CEGQI_SI_MODE_ALL_ABORT ){
- if( !d_has_ites ){
- return d_inst.empty();
- }
- }
return true;
}
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<Node> d_lemmas_produced;
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
//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
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 );
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<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 = static_cast<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;
}
- 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;
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 ) {
* 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.
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)
{
}
std::vector<Node> qchildren;
Node qbody_subs = q[1];
std::map<Node, Node> synth_fun_vars;
+ TermDbSygus* tds = d_qe->getTermDatabaseSygus();
for (unsigned i = 0, size = q[0].getNumChildren(); i < size; i++)
{
Node sf = q[0][i];
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<DatatypeType>(tn.toType()).getDatatype();
+ Assert(dt.isSygus());
if( !dt.getSygusAllowAll() ){
d_is_syntax_restricted = true;
}
const std::vector<Node>& 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
projects / cvc5.git / commitdiff