isconstant predicate.

2 files changed, 77 insertions, 4 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 848fc6359..186156781 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -161,6 +161,57 @@ Node SygusSymBreakNew::getTermOrderPredicate( Node n1, Node n2 ) {
 
   return nm->mkNode(kind::OR, comm_disj);
 }
+
+Node SygusSymBreakNew::getIsConstantPredicate( TNode n )
+{
+  TypeNode tn = n.getType();
+  Node constPred;
+  TNode x = getFreeVar( tn );
+  std::map< TypeNode, Node >::iterator itcp = d_isconst_pred.find(tn);
+  if( itcp==d_isconst_pred.end() )
+  {
+    const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+    std::vector<Node> exp_const;
+    int anyc_cons_num = d_tds->getAnyConstantConsNum(tn);
+    for (unsigned k = 0, ncons = dt.getNumConstructors(); k < ncons; k++)
+    {
+      Kind nck = d_tds->getConsNumKind(tn, k);
+      bool is_const = false;
+      if( static_cast<int>(k) == anyc_cons_num )
+      {
+        is_const = true;
+      }
+      else if( nck==UNDEFINED_KIND )
+      {
+        Node cc = d_tds->getConsNumConst(tn, k);
+        if (!cc.isNull())
+        {
+          is_const = true;
+        }
+      }
+      if (is_const)
+      {
+        Node tester = DatatypesRewriter::mkTester(x, k, dt);
+        exp_const.push_back(tester);
+      }
+    }
+    if( !exp_const.empty() )
+    {
+      NodeManager * nm = NodeManager::currentNM();
+      constPred = exp_const.size()==1 ? exp_const[0] : nm->mkNode(OR,exp_const);
+    }
+    d_isconst_pred[tn] = constPred;
+  }
+  else
+  {
+    constPred = itcp->second;
+  }
+  if( constPred.isNull() )
+  {
+    return constPred;
+  }
+  return constPred.substitute(x,n);
+}
   
 void SygusSymBreakNew::registerTerm( Node n, std::vector< Node >& lemmas ) {
   if( d_is_top_level.find( n )==d_is_top_level.end() ){
@@ -851,6 +902,10 @@ Node SygusSymBreakNew::registerSearchValue(
         //store rewritten values, regardless of whether it will be considered
         d_cache[a].d_search_val[tn][bvr] = nv;
         d_cache[a].d_search_val_sz[tn][bvr] = sz;
+        if( bvr.isConst() )
+        {
+          d_cache[a].d_search_val_consts[tn].insert(bvr);
+        }
       }else{
         bad_val_bvr = bvr;
         if( Trace.isOn("sygus-sb-exc") ){
@@ -943,9 +998,8 @@ Node SygusSymBreakNew::registerSearchValue(
         } 
         Assert( d_tds->getSygusTermSize( bad_val )==sz );
 
-        Node x = getFreeVar( tn );
-        
-        // do analysis of the evaluation  FIXME: does not work (evaluation is non-constant)
+        // generalize the explanation for why the analog of bad_val 
+        // is equivalent to bvr
         quantifiers::EquivSygusInvarianceTest eset;
         eset.init(d_tds, tn, aconj, a, bvr);
 
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index fe8b0ee14..a3f07f175 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -205,6 +205,11 @@ private:
     /** the size of terms in the range of d_search val. */
     std::map<TypeNode, std::unordered_map<Node, unsigned, NodeHashFunction>>
         d_search_val_sz;
+    /** 
+     * For each type tn, this stores all builtin constants in the domain of 
+     * d_search_val[tn]. 
+     */
+    std::map< TypeNode, std::unordered_set<Node, NodeHashFunction>  > d_search_val_consts;
     /** For each term, whether this cache has processed that term */
     std::unordered_set<Node, NodeHashFunction> d_search_val_proc;
   };
@@ -429,7 +434,21 @@ private:
    *   ( DT_SIZE n1 ) >= ( DT_SIZE n2 )
    */
   Node getTermOrderPredicate( Node n1, Node n2 );
-
+  /** get is-constant predicate 
+   * 
+   * Given a term n of sygus datatype type, this returns a predicate that holds
+   * iff the builtin version of n is a (possibly symbolic) constant. For
+   * example, for:
+   *   A -> 0 | 1 | x | A+A
+   * this returns the predicate is-0( n ) V is-1( n ).
+   */
+  Node getIsConstantPredicate( TNode n );
+  /** the is-constant predicate, per sygus datatype type 
+   * 
+   * For each sygus datatype tn, this predicate states that x is a sygus 
+   * datatype value corresponding to a constant, where x is getFreeVar( tn ).
+   */
+  std::map< TypeNode, Node > d_isconst_pred;
  private:
   /**
    * Map from registered variables to whether they are a sygus enumerator.