Assign weight 1 for Boolean variables in SyGuS default grammars (#1948)

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 3d8052ae4054e9a51ef0486f15dc21300113a8e3..d745cb6da06eb4488f02a4ee7b7da73e6698f382 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -270,7 +270,7 @@ Node CegGrammarConstructor::process(Node q,
   }
   return nm->mkNode(kind::FORALL, qchildren);
 }
-  
+
 Node CegGrammarConstructor::convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars ){
   std::unordered_map<TNode, Node, TNodeHashFunction> visited;
   std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
@@ -451,6 +451,10 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl;
     std::vector<std::string> cnames;
     std::vector<std::vector<CVC4::Type> > cargs;
+    /* Print callbacks for each constructor */
+    std::vector<std::shared_ptr<SygusPrintCallback>> pcs;
+    /* Weights for each constructor */
+    std::vector<int> weights;
     Type unres_t = unres_types[i];
     //add variables
     for( unsigned j=0; j<sygus_vars.size(); j++ ){
@@ -461,6 +465,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         ops[i].push_back( sygus_vars[j].toExpr() );
         cnames.push_back( ss.str() );
         cargs.push_back( std::vector< CVC4::Type >() );
+        pcs.push_back(nullptr);
+        weights.push_back(-1);
       }
     }
     //add constants
@@ -482,6 +488,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       ops[i].push_back( consts[j].toExpr() );
       cnames.push_back( ss.str() );
       cargs.push_back( std::vector< CVC4::Type >() );
+      pcs.push_back(nullptr);
+      weights.push_back(-1);
     }
     //ITE
     CVC4::Kind k = kind::ITE;
@@ -492,6 +500,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     cargs.back().push_back(unres_bt);
     cargs.back().push_back(unres_t);
     cargs.back().push_back(unres_t);
+    pcs.push_back(nullptr);
+    weights.push_back(-1);
 
     if (types[i].isReal())
     {
@@ -504,6 +514,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         cargs.push_back(std::vector<CVC4::Type>());
         cargs.back().push_back(unres_t);
         cargs.back().push_back(unres_t);
+        pcs.push_back(nullptr);
+        weights.push_back(-1);
       }
       if (!types[i].isInteger())
       {
@@ -551,6 +563,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         cargs.push_back(std::vector<Type>());
         cargs.back().push_back(unres_t);
         cargs.back().push_back(unres_pos_int_t);
+        pcs.push_back(nullptr);
+        weights.push_back(-1);
       }
     }else if( types[i].isDatatype() ){
       Trace("sygus-grammar-def") << "...add for constructors" << std::endl;
@@ -565,6 +579,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
           //Assert( type_to_unres.find(crange)!=type_to_unres.end() );
           cargs.back().push_back( type_to_unres[crange] );
         }
+        pcs.push_back(nullptr);
+        weights.push_back(-1);
       }
     }else{
       std::stringstream sserr;
@@ -584,6 +600,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         cargs.push_back( std::vector< CVC4::Type >() );
         //Assert( type_to_unres.find(arg_type)!=type_to_unres.end() );
         cargs.back().push_back( type_to_unres[arg_type] );
+        pcs.push_back(nullptr);
+        weights.push_back(-1);
       }
     }
     Trace("sygus-grammar-def") << "...make datatype " << datatypes[i] << std::endl;
@@ -598,7 +616,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
           || std::find(itexc->second.begin(), itexc->second.end(), opn)
                  == itexc->second.end())
       {
-        datatypes[i].addSygusConstructor(ops[i][j], cnames[j], cargs[j]);
+        datatypes[i].addSygusConstructor(
+            ops[i][j], cnames[j], cargs[j], pcs[j], weights[j]);
       }
     }
     Trace("sygus-grammar-def")
@@ -616,6 +635,10 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
   ops.push_back(std::vector<Expr>());
   std::vector<std::string> cnames;
   std::vector<std::vector< Type > > cargs;
+  /* Print callbacks for each constructor */
+  std::vector<std::shared_ptr<SygusPrintCallback>> pcs;
+  /* Weights for each constructor */
+  std::vector<int> weights;
   Trace("sygus-grammar-def") << "Make grammar for " << btype << " " << datatypes.back() << std::endl;
   //add variables
   for( unsigned i=0; i<sygus_vars.size(); i++ ){
@@ -626,6 +649,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       ops.back().push_back( sygus_vars[i].toExpr() );
       cnames.push_back( ss.str() );
       cargs.push_back( std::vector< CVC4::Type >() );
+      pcs.push_back(nullptr);
+      weights.push_back(1);
     }
   }
   //add constants
@@ -640,6 +665,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     ops.back().push_back(consts[j].toExpr());
     cnames.push_back(ss.str());
     cargs.push_back(std::vector<CVC4::Type>());
+    pcs.push_back(nullptr);
+    weights.push_back(-1);
   }
   //add operators
   for (unsigned i = 0; i < 4; i++)
@@ -667,6 +694,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         cargs.back().push_back(unres_bt);
       }
     }
+    pcs.push_back(nullptr);
+    weights.push_back(-1);
   }
   //add predicates for types
   for( unsigned i=0; i<types.size(); i++ ){
@@ -681,6 +710,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     cargs.push_back( std::vector< CVC4::Type >() );
     cargs.back().push_back(unres_types[i]);
     cargs.back().push_back(unres_types[i]);
+    pcs.push_back(nullptr);
+    weights.push_back(-1);
     //type specific predicates
     if (types[i].isReal())
     {
@@ -691,6 +722,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       cargs.push_back( std::vector< CVC4::Type >() );
       cargs.back().push_back(unres_types[i]);
       cargs.back().push_back(unres_types[i]);
+      pcs.push_back(nullptr);
+      weights.push_back(-1);
     }else if( types[i].isDatatype() ){
       //add for testers
       Trace("sygus-grammar-def") << "...add for testers" << std::endl;
@@ -701,6 +734,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         cnames.push_back(dt[k].getTesterName());
         cargs.push_back( std::vector< CVC4::Type >() );
         cargs.back().push_back(unres_types[i]);
+        pcs.push_back(nullptr);
+        weights.push_back(-1);
       }
     }
   }
@@ -710,11 +745,12 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
   Trace("sygus-grammar-def") << "...make datatype " << datatypes.back() << std::endl;
   datatypes.back().setSygus( btype.toType(), bvl.toExpr(), true, true );
   for( unsigned j=0; j<ops.back().size(); j++ ){
-    datatypes.back().addSygusConstructor( ops.back()[j], cnames[j], cargs[j] );
+    datatypes.back().addSygusConstructor(
+        ops.back()[j], cnames[j], cargs[j], pcs[j], weights[j]);
   }
   //sorts.push_back( btype );
   Trace("sygus-grammar-def") << "...finished make default grammar for " << fun << " " << range << std::endl;
-  
+
   if( startIndex>0 ){
     CVC4::Datatype tmp_dt = datatypes[0];
     datatypes[0] = datatypes[startIndex];
@@ -751,7 +787,7 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType(
   return TypeNode::fromType( types[0] );
 }
 
-TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, 
+TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl,
                                               const std::string& fun, unsigned& tcount ) {
   if( templ==templ_arg ){
     //Assert( templ_arg.getType()==sygusToBuiltinType( templ_arg_sygus_type ) );
@@ -791,7 +827,7 @@ TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_a
   }
 }
 
-TypeNode CegGrammarConstructor::mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, 
+TypeNode CegGrammarConstructor::mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl,
                                                      const std::string& fun ) {
   unsigned tcount = 0;
   return mkSygusTemplateTypeRec( templ, templ_arg, templ_arg_sygus_type, bvl, fun, tcount );