Minor additions for sygus (#1419)

5 files changed, 60 insertions, 41 deletions

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 8b6384dcc..f96066e80 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -181,17 +181,19 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
   d_sygus_allow_all = allow_all;
 }
 
-void Datatype::addSygusConstructor(CVC4::Expr op,
+void Datatype::addSygusConstructor(Expr op,
                                    std::string& cname,
-                                   std::vector<CVC4::Type>& cargs,
-                                   std::shared_ptr<SygusPrintCallback> spc)
+                                   std::vector<Type>& cargs,
+                                   std::shared_ptr<SygusPrintCallback> spc,
+                                   int weight)
 {
   Debug("dt-sygus") << "--> Add constructor " << cname << " to " << getName() << std::endl;
   Debug("dt-sygus") << "    sygus op : " << op << std::endl;
   std::string name = getName() + "_" + cname;
   std::string testerId("is-");
   testerId.append(name);
-  CVC4::DatatypeConstructor c(name, testerId );
+  unsigned cweight = weight >= 0 ? weight : (cargs.empty() ? 0 : 1);
+  DatatypeConstructor c(name, testerId, cweight);
   c.setSygus(op, spc);
   for( unsigned j=0; j<cargs.size(); j++ ){
     Debug("parser-sygus-debug") << "  arg " << j << " : " << cargs[j] << std::endl;
@@ -770,12 +772,15 @@ DatatypeConstructor::DatatypeConstructor(std::string name)
       d_name(name + '\0' + "is_" + name),  // default tester name is "is_FOO"
       d_tester(),
       d_args(),
-      d_sygus_pc(nullptr)
+      d_sygus_pc(nullptr),
+      d_weight(1)
 {
   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
 }
 
-DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester)
+DatatypeConstructor::DatatypeConstructor(std::string name,
+                                         std::string tester,
+                                         unsigned weight)
     :  // We don't want to introduce a new data member, because eventually
        // we're going to be a constant stuffed inside a node.  So we stow
        // the tester name away inside the constructor name until
@@ -783,7 +788,8 @@ DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester)
       d_name(name + '\0' + tester),
       d_tester(),
       d_args(),
-      d_sygus_pc(nullptr)
+      d_sygus_pc(nullptr),
+      d_weight(weight)
 {
   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
   PrettyCheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
@@ -879,6 +885,13 @@ bool DatatypeConstructor::isSygusIdFunc() const {
           && d_sygus_op[0][0] == d_sygus_op[1]);
 }
 
+unsigned DatatypeConstructor::getWeight() const
+{
+  PrettyCheckArgument(
+      isResolved(), this, "this datatype constructor is not yet resolved");
+  return d_weight;
+}
+
 std::shared_ptr<SygusPrintCallback> DatatypeConstructor::getSygusPrintCallback() const
 {
   PrettyCheckArgument(
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index b899b0099..b3c81911f 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -229,8 +229,13 @@ class CVC4_PUBLIC DatatypeConstructor {
    * Create a new Datatype constructor with the given name for the
    * constructor and the given name for the tester.  The actual
    * constructor and tester aren't created until resolution time.
+   * weight is the value that this constructor carries when computing size.
+   * For example, if A, B, C have weights 0, 1, and 3 respectively, then
+   * C( B( A() ), B( A() ) ) has size 5.
    */
-  DatatypeConstructor(std::string name, std::string tester);
+  DatatypeConstructor(std::string name,
+                      std::string tester,
+                      unsigned weight = 1);
 
   ~DatatypeConstructor() {}
   /**
@@ -295,12 +300,19 @@ class CVC4_PUBLIC DatatypeConstructor {
    */
   bool isSygusIdFunc() const;
   /** get sygus print callback
+   *
    * This class stores custom ways of printing
    * sygus datatype constructors, for instance,
    * to handle defined or let expressions that
    * appear in user-provided grammars.
    */
   std::shared_ptr<SygusPrintCallback> getSygusPrintCallback() const;
+  /** get weight
+   *
+   * Get the weight of this constructor. This value is used when computing the
+   * size of datatype terms that involve this constructor.
+   */
+  unsigned getWeight() const;
 
   /**
    * Get the tester name for this Datatype constructor.
@@ -446,6 +458,8 @@ class CVC4_PUBLIC DatatypeConstructor {
   Expr d_sygus_op;
   /** sygus print callback */
   std::shared_ptr<SygusPrintCallback> d_sygus_pc;
+  /** weight */
+  unsigned d_weight;
 
   /** shared selectors for each type
    *
@@ -659,11 +673,17 @@ public:
    * encode the arguments of op. For example, a sygus constructor
    * with op = PLUS should be such that cargs.size()>=2 and
    * the sygus type of cargs[i] is Real/Int for each i.
+   *
+   * weight denotes the value added by the constructor when computing the size
+   * of datatype terms. Passing a value <0 denotes the default weight for the
+   * constructor, which is 0 for nullary constructors and 1 for non-nullary
+   * constructors.
    */
-  void addSygusConstructor(CVC4::Expr op,
+  void addSygusConstructor(Expr op,
                            std::string& cname,
-                           std::vector<CVC4::Type>& cargs,
-                           std::shared_ptr<SygusPrintCallback> spc = nullptr);
+                           std::vector<Type>& cargs,
+                           std::shared_ptr<SygusPrintCallback> spc = nullptr,
+                           int weight = -1);
 
   /** set that this datatype is a tuple */
   void setTuple();
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 49e8a6888..4fcb6d718 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -159,13 +159,15 @@ public:
             children.push_back( NodeManager::currentNM()->mkNode( kind::DT_SIZE, in[0][i] ) );
           }
         }
-        Node res;
-        if( !children.empty() ){
-          children.push_back( NodeManager::currentNM()->mkConst( Rational(1) ) );
-          res = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::PLUS, children );
-        }else{
-          res = NodeManager::currentNM()->mkConst( Rational(0) );
-        }
+        TNode constructor = in[0].getOperator();
+        size_t constructorIndex = Datatype::indexOf(constructor.toExpr());
+        const Datatype& dt = Datatype::datatypeOf(constructor.toExpr());
+        const DatatypeConstructor& c = dt[constructorIndex];
+        unsigned weight = c.getWeight();
+        children.push_back(NodeManager::currentNM()->mkConst(Rational(weight)));
+        Node res = children.size() == 1
+                       ? children[0]
+                       : NodeManager::currentNM()->mkNode(kind::PLUS, children);
         Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: rewrite size " << in << " to " << res << std::endl;
         return RewriteResponse(REWRITE_AGAIN_FULL, res );
       }
diff --git a/src/theory/quantifiers/ce_guided_pbe.cpp b/src/theory/quantifiers/ce_guided_pbe.cpp
index d46fed686..bee19daeb 100644
--- a/src/theory/quantifiers/ce_guided_pbe.cpp
+++ b/src/theory/quantifiers/ce_guided_pbe.cpp
@@ -1054,6 +1054,7 @@ void CegConjecturePbe::staticLearnRedundantOps(
 // ------------------------------------------- solution construction from enumeration
 
 void CegConjecturePbe::getCandidateList( std::vector< Node >& candidates, std::vector< Node >& clist ) {
+  Valuation& valuation = d_qe->getValuation();
   for( unsigned i=0; i<candidates.size(); i++ ){
     Node v = candidates[i];
     std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( v );
@@ -1062,7 +1063,9 @@ void CegConjecturePbe::getCandidateList( std::vector< Node >& candidates, std::v
         Node e = it->second.d_esym_list[j];
         std::map< Node, EnumInfo >::iterator it = d_einfo.find( e );
         Assert( it != d_einfo.end() );
-        if( getGuardStatus( it->second.d_active_guard )==1 ){
+        Node gstatus = valuation.getSatValue(it->second.d_active_guard);
+        if (!gstatus.isNull() && gstatus.getConst<bool>())
+        {
           clist.push_back( e );
         }
       }
@@ -1112,7 +1115,9 @@ bool CegConjecturePbe::constructCandidates( std::vector< Node >& enums, std::vec
 void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& lems ) {
   std::map< Node, EnumInfo >::iterator it = d_einfo.find( x );
   Assert( it != d_einfo.end() );
-  if( getGuardStatus( it->second.d_active_guard )==1 ){
+  Node gstatus = d_qe->getValuation().getSatValue(it->second.d_active_guard);
+  if (!gstatus.isNull() && gstatus.getConst<bool>())
+  {
     Assert( std::find( it->second.d_enum_vals.begin(), it->second.d_enum_vals.end(), v )==it->second.d_enum_vals.end() );
     Node c = it->second.d_parent_candidate;
     Node exp_exc;
@@ -2356,19 +2361,6 @@ bool CegConjecturePbe::UnifContext::isStringSolved(
   return true;
 }
 
-int CegConjecturePbe::getGuardStatus( Node g ) {
-  bool value;
-  if( d_qe->getValuation().hasSatValue( g, value ) ) {
-    if( value ){
-      return 1;
-    }else{
-      return -1;
-    }
-  }else{
-    return 0;
-  }
-}
-
 CegConjecturePbe::StrategyNode::~StrategyNode()
 {
   for (unsigned j = 0, size = d_strats.size(); j < size; j++)
diff --git a/src/theory/quantifiers/ce_guided_pbe.h b/src/theory/quantifiers/ce_guided_pbe.h
index 1abdda6a6..8cfed253c 100644
--- a/src/theory/quantifiers/ce_guided_pbe.h
+++ b/src/theory/quantifiers/ce_guided_pbe.h
@@ -742,14 +742,6 @@ class CegConjecturePbe {
                                     std::map< Node, std::vector< unsigned > > incr,
                                     UnifContext& x );
   //------------------------------ end constructing solutions
-
-  /** get guard status
-   *
-   * Returns 1 if g is asserted true in the SAT solver.
-   * Returns -1 if g is asserted false in the SAT solver.
-   * Returns 0 otherwise.
-   */
-  int getGuardStatus(Node g);
 };
 
 }/* namespace CVC4::theory::quantifiers */