#include "expr/datatype.h"
#include "options/quantifiers_options.h"
+#include "theory/quantifiers/ce_guided_conjecture.h"
#include "theory/quantifiers/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
namespace theory {
namespace quantifiers {
-
-CegGrammarConstructor::CegGrammarConstructor( QuantifiersEngine * qe ) :
-d_qe( qe ), d_is_syntax_restricted(false), d_has_ite(true){
-
+CegGrammarConstructor::CegGrammarConstructor(QuantifiersEngine* qe,
+ CegConjecture* p)
+ : d_qe(qe), d_parent(p), d_is_syntax_restricted(false), d_has_ite(true)
+{
}
void CegGrammarConstructor::collectTerms( Node n, std::map< TypeNode, std::vector< Node > >& consts ){
Node sfvl = sf.getAttribute(SygusSynthFunVarListAttribute());
// sfvl may be null for constant synthesis functions
Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " << sfvl << std::endl;
+
TypeNode tn;
std::stringstream ss;
ss << sf;
if( v.getType().isDatatype() && ((DatatypeType)v.getType().toType()).getDatatype().isSygus() ){
tn = v.getType();
}else{
+ // check which arguments are irrelevant
+ std::unordered_set<unsigned> arg_irrelevant;
+ // TODO (#1210) : get arg irrelevant based on conjecture-specific analysis
+ std::unordered_set<Node, NodeHashFunction> term_irrelevant;
+ // convert to term
+ for (std::unordered_set<unsigned>::iterator ita = arg_irrelevant.begin();
+ ita != arg_irrelevant.end();
+ ++ita)
+ {
+ unsigned arg = *ita;
+ Assert(arg < sfvl.getNumChildren());
+ term_irrelevant.insert(sfvl[arg]);
+ }
+
// make the default grammar
- tn = mkSygusDefaultType( v.getType(), sfvl, ss.str(), extra_cons );
+ tn = mkSygusDefaultType(
+ v.getType(), sfvl, ss.str(), extra_cons, term_irrelevant);
}
// check if there is a template
std::map< Node, Node >::iterator itt = templates.find( sf );
}
}
-void CegGrammarConstructor::mkSygusDefaultGrammar( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons,
- std::vector< CVC4::Datatype >& datatypes, std::set<Type>& unres ) {
+void CegGrammarConstructor::mkSygusDefaultGrammar(
+ TypeNode range,
+ Node bvl,
+ const std::string& fun,
+ std::map<TypeNode, std::vector<Node> >& extra_cons,
+ std::unordered_set<Node, NodeHashFunction>& term_irrelevant,
+ std::vector<CVC4::Datatype>& datatypes,
+ std::set<Type>& unres)
+{
+ Trace("sygus-grammar-def") << "Construct default grammar for " << fun << " "
+ << range << std::endl;
// collect the variables
std::vector<Node> sygus_vars;
if( !bvl.isNull() ){
for( unsigned i=0; i<bvl.getNumChildren(); i++ ){
- sygus_vars.push_back( bvl[i] );
+ if (term_irrelevant.find(bvl[i]) == term_irrelevant.end())
+ {
+ sygus_vars.push_back(bvl[i]);
+ }
+ else
+ {
+ Trace("sygus-grammar-def") << "...synth var " << bvl[i]
+ << " has been marked irrelevant."
+ << std::endl;
+ }
}
}
//if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){
//}
std::vector< std::vector< Expr > > ops;
int startIndex = -1;
- Trace("sygus-grammar-def") << "Construct default grammar for " << fun << " " << range << std::endl;
std::map< Type, Type > sygus_to_builtin;
std::vector< TypeNode > types;
}
}
-
-TypeNode CegGrammarConstructor::mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun,
- std::map< TypeNode, std::vector< Node > >& extra_cons ) {
+TypeNode CegGrammarConstructor::mkSygusDefaultType(
+ TypeNode range,
+ Node bvl,
+ const std::string& fun,
+ std::map<TypeNode, std::vector<Node> >& extra_cons,
+ std::unordered_set<Node, NodeHashFunction>& term_irrelevant)
+{
Trace("sygus-grammar-def") << "*** Make sygus default type " << range << ", make datatypes..." << std::endl;
for( std::map< TypeNode, std::vector< Node > >::iterator it = extra_cons.begin(); it != extra_cons.end(); ++it ){
Trace("sygus-grammar-def") << " ...using " << it->second.size() << " extra constants for " << it->first << std::endl;
}
std::set<Type> unres;
std::vector< CVC4::Datatype > datatypes;
- mkSygusDefaultGrammar( range, bvl, fun, extra_cons, datatypes, unres );
+ mkSygusDefaultGrammar(
+ range, bvl, fun, extra_cons, term_irrelevant, datatypes, unres);
Trace("sygus-grammar-def") << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl;
Assert( !datatypes.empty() );
std::vector<DatatypeType> types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(datatypes, unres);
namespace theory {
namespace quantifiers {
+class CegConjecture;
+
/** 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
{
public:
- CegGrammarConstructor( QuantifiersEngine * qe );
- ~CegGrammarConstructor(){}
- /** convert node n based on deep embedding (Section 4 of Reynolds et al CAV 2015) */
- Node process( Node q, std::map< Node, Node >& templates, std::map< Node, Node >& templates_arg );
- /** 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
- // extra_cons is a set of extra constant symbols to include in the grammar
- static TypeNode mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons );
- // make the default sygus datatype type corresponding to builtin type range
- static TypeNode mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun ){
- std::map< TypeNode, std::vector< Node > > extra_cons;
- return mkSygusDefaultType( range, bvl, fun, extra_cons );
+ CegGrammarConstructor(QuantifiersEngine* qe, CegConjecture* p);
+ ~CegGrammarConstructor() {}
+ /** process
+ * This converts node q based on its deep embedding
+ * (Section 4 of Reynolds et al CAV 2015).
+ * The syntactic restrictions are associated with
+ * the functions-to-synthesize using the attribute
+ * SygusSynthGrammarAttribute.
+ * The arguments templates and template_args
+ * indicate templates for the function to synthesize,
+ * in particular the solution for the i^th function
+ * to synthesis must be of the form
+ * templates[i]{ templates_arg[i] -> t }
+ * for some t if !templates[i].isNull().
+ */
+ Node process(Node q,
+ std::map<Node, Node>& templates,
+ std::map<Node, Node>& templates_arg);
+ /** 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
+ * extra_cons is a set of extra constant symbols to include in the grammar
+ * term_irrelevant is a set of terms that should not be included in the
+ * grammar.
+ */
+ static TypeNode mkSygusDefaultType(
+ TypeNode range,
+ Node bvl,
+ const std::string& fun,
+ std::map<TypeNode, std::vector<Node> >& extra_cons,
+ std::unordered_set<Node, NodeHashFunction>& term_irrelevant);
+ /** make the default sygus datatype type corresponding to builtin type range */
+ static TypeNode mkSygusDefaultType(TypeNode range,
+ Node bvl,
+ const std::string& fun)
+ {
+ std::map<TypeNode, std::vector<Node> > extra_cons;
+ std::unordered_set<Node, NodeHashFunction> term_irrelevant;
+ return mkSygusDefaultType(range, bvl, fun, extra_cons, term_irrelevant);
}
- // make the sygus datatype type that encodes the solution space (lambda templ_arg. templ[templ_arg]) where templ_arg
- // has syntactic restrictions encoded by sygus type templ_arg_sygus_type
- // bvl is the set of free variables to include in the frammar
- // fun is for naming
+ /** make the sygus datatype type that encodes the solution space (lambda
+ * templ_arg. templ[templ_arg]) where templ_arg
+ * has syntactic restrictions encoded by sygus type templ_arg_sygus_type
+ * bvl is the set of free variables to include in the grammar
+ * fun is for naming
+ */
static TypeNode mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun );
private:
/** reference to quantifier engine */
QuantifiersEngine * d_qe;
+ /** parent conjecture
+ * This contains global information about the synthesis conjecture.
+ */
+ CegConjecture* d_parent;
/** is the syntax restricted? */
bool d_is_syntax_restricted;
/** does the syntax allow ITE expressions? */
static void mkSygusConstantsForType( TypeNode type, std::vector<CVC4::Node>& ops );
// collect the list of types that depend on type range
static void collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels );
- // helper function for function mkSygusDefaultGrammar
- // collects a set of mutually recursive datatypes "datatypes" corresponding to encoding type "range" to SyGuS
- // unres is used for the resulting call to mkMutualDatatypeTypes
- static void mkSygusDefaultGrammar( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons,
- std::vector< CVC4::Datatype >& datatypes, std::set<Type>& unres );
+ /** helper function for function mkSygusDefaultType
+ * Collects a set of mutually recursive datatypes "datatypes" corresponding to
+ * encoding type "range" to SyGuS.
+ * unres is used for the resulting call to mkMutualDatatypeTypes
+ */
+ static void mkSygusDefaultGrammar(
+ TypeNode range,
+ Node bvl,
+ const std::string& fun,
+ std::map<TypeNode, std::vector<Node> >& extra_cons,
+ std::unordered_set<Node, NodeHashFunction>& term_irrelevant,
+ std::vector<CVC4::Datatype>& datatypes,
+ std::set<Type>& unres);
// helper function for mkSygusTemplateType
static TypeNode mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl,
const std::string& fun, unsigned& tcount );
projects / cvc5.git / commitdiff