Mark datatypes as sygus. Add option to normalize sygus terms in search. Add sygus regressions.

7 files changed, 115 insertions, 16 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index d2f38cc82..a83299d3b 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -600,6 +600,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
         std::string dname = ss.str();
         sorts.push_back(t);
         datatypes.push_back(Datatype(dname));
+        datatypes.back().setSygusType( t );
         ops.push_back(std::vector<Expr>());
         cnames.push_back(std::vector<std::string>());
         cargs.push_back(std::vector<std::vector<CVC4::Type> >());
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 077f385b0..c6c3a896c 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -534,7 +534,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
     testerId.append(name);
     checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
     checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
-    CVC4::DatatypeConstructor c(name, testerId);
+    CVC4::DatatypeConstructor c(name, testerId, ops[i] );
     for( unsigned j=0; j<cargs[i].size(); j++ ){
       std::stringstream sname;
       sname << name << "_" << j;
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index bf986a138..8db9435ed 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -238,11 +238,16 @@ void TheoryDatatypes::check(Effort e) {
                 }else{
                   Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
                   std::vector< Node > children;
-                  for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-                    Node test = DatatypesRewriter::mkTester( n, i, dt );
-                    children.push_back( test );
+                  if( dt.isSygus() && options::sygusNormalForm() ){
+                    getSygusSplits( n, dt, children );
+                  }else{
+                    for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+                      Node test = DatatypesRewriter::mkTester( n, i, dt );
+                      children.push_back( test );
+                    }
                   }
-                  Node lemma = NodeManager::currentNM()->mkNode( kind::OR, children );
+                  Assert( !children.empty() );
+                  Node lemma = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::OR, children );
                   d_out->lemma( lemma );
                 }
                 return;
@@ -294,10 +299,10 @@ void TheoryDatatypes::flushPendingFacts(){
       Node exp = d_pending_exp[ fact ];
       //check to see if we have to communicate it to the rest of the system
       if( mustCommunicateFact( fact, exp ) ){
-        Trace("dt-lemma-debug") << "Assert fact " << fact << " " << exp << std::endl;
+        Trace("dt-lemma-debug") << "Assert fact " << fact << " with explanation " << exp << std::endl;
         Node lem = fact;
         if( exp.isNull() || exp==d_true ){
-          lem = fact;
+          Trace("dt-lemma-debug") << "Trivial explanation." << std::endl;
         }else{
           Trace("dt-lemma-debug") << "Get explanation..." << std::endl;
           Node ee_exp = explain( exp );
@@ -394,12 +399,7 @@ Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) {
       if( tst==d_true ){
         n_ret = sel;
       }else{
-        if( d_exp_def_skolem.find( selector )==d_exp_def_skolem.end() ){
-          std::stringstream ss;
-          ss << selector << "_uf";
-          d_exp_def_skolem[ selector ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(),
-                                            NodeManager::currentNM()->mkFunctionType( n[0].getType(), n.getType() ) );
-        }
+        mkExpDefSkolem( selector, n[0].getType(), n.getType() );
         Node sk = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[ selector ], n[0]  );
         if( tst==NodeManager::currentNM()->mkConst( false ) ){
           n_ret = sk;
@@ -694,7 +694,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
         if( !cons1.isNull() && !cons2.isNull() ){
           Debug("datatypes-debug") << "Constructors : " << cons1 << " " << cons2 << std::endl;
           Node unifEq = cons1.eqNode( cons2 );
-#if 0
+          /*
           std::vector< Node > exp;
           std::vector< std::pair< TNode, TNode > > deq_cand;
           bool conf = checkClashModEq( cons1, cons2, exp, deq_cand );
@@ -711,11 +711,10 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
           if( conf ){
             exp.push_back( unifEq );
             d_conflictNode = explain( exp );
-#else
+         */
           std::vector< Node > rew;
           if( DatatypesRewriter::checkClash( cons1, cons2, rew ) ){
             d_conflictNode = explain( unifEq );
-#endif
             Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl;
             d_out->conflict( d_conflictNode );
             d_conflict = true;
@@ -864,6 +863,15 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >
   }
 }
 
+void TheoryDatatypes::mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ) {
+  if( d_exp_def_skolem.find( sel )==d_exp_def_skolem.end() ){
+    std::stringstream ss;
+    ss << sel << "_uf";
+    d_exp_def_skolem[ sel ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(),
+                                  NodeManager::currentNM()->mkFunctionType( dt, rt ) );
+  }
+}
+
 void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){
   Debug("datatypes-debug") << "Add tester : " << t << " to eqc(" << n << ")" << std::endl;
   Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl;
@@ -1032,8 +1040,15 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
 }
 
 void TheoryDatatypes::collapseSelector( Node s, Node c ) {
+  Assert( c.getKind()==APPLY_CONSTRUCTOR );
+  Trace("dt-collapse-sel") << "collapse selector : " << s << " " << c << std::endl;
   Node r;
   if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){
+    //Trace("dt-collapse-sel") << "Indices : " << Datatype::indexOf(c.getOperator().toExpr()) << " " << Datatype::cindexOf(s.getOperator().toExpr()) << std::endl;
+    //if( Datatype::indexOf(c.getOperator().toExpr())!=Datatype::cindexOf(s.getOperator().toExpr()) ){
+    //  mkExpDefSkolem( s.getOperator(), s[0].getType(), s.getType() );
+    //  r = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[s.getOperator().toExpr()], s[0] );
+    //}else{
     r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c );
   }else if( s.getKind()==kind::DT_SIZE ){
     r = NodeManager::currentNM()->mkNode( kind::DT_SIZE, c );
@@ -1901,3 +1916,39 @@ bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >&
   return false;
 }
 
+void TheoryDatatypes::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits ) {
+  Assert( dt.isSygus() );
+  Trace("sygus-split") << "Get sygus splits " << n << std::endl;
+  if( n.getKind()==APPLY_SELECTOR_TOTAL ){
+    Node op = n.getOperator();
+    std::map< Node, std::vector< bool > >::iterator it = d_sygus_splits.find( op );
+    if( it==d_sygus_splits.end() ){
+      Expr selectorExpr = op.toExpr();
+      int csIndex = Datatype::cindexOf(selectorExpr);
+      int sIndex = Datatype::indexOf(selectorExpr);
+      Trace("sygus-split") << "  Constructor, selector index : " << csIndex << " " << sIndex << std::endl;
+      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+        Expr sop = dt[i].getSygusOp();
+        Kind sk = NodeManager::operatorToKind( Node::fromExpr( sop ) );
+        Trace("sygus-split") << "  Operator #" << i << " : " << sop << ", kind = " << sk << std::endl;
+        bool addSplit = true;
+        //TODO
+        
+        d_sygus_splits[op].push_back( addSplit );
+      }
+    }
+    for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+      if( d_sygus_splits[op][i] ){
+        Node test = DatatypesRewriter::mkTester( n, i, dt );
+        splits.push_back( test );
+      }
+    }
+    Assert( !splits.empty() );
+  }else{
+    for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+      Node test = DatatypesRewriter::mkTester( n, i, dt );
+      splits.push_back( test );
+    }
+  }
+}
+
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 30b0140a9..2f0ec20ec 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -133,6 +133,8 @@ private:
   bool hasTester( Node n );
   /** get the possible constructors for n */
   void getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& cons );
+  /** mkExpDefSkolem */
+  void mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt );
 private:
   /** The notify class */
   NotifyClass d_notify;
@@ -178,6 +180,8 @@ private:
   unsigned d_dtfCounter;
   /** expand definition skolem functions */
   std::map< Node, Node > d_exp_def_skolem;
+  /** sygus splits */
+  std::map< Node, std::vector< bool > > d_sygus_splits;
 private:
   /** assert fact */
   void assertFact( Node fact, Node exp );
@@ -276,6 +280,8 @@ private:
   bool mustCommunicateFact( Node n, Node exp );
   /** check clash mod eq */
   bool checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand );
+  /** get sygus splits */
+  void getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits );
 private:
   //equality queries
   bool hasTerm( TNode a );
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index fc59b22b7..ad1508716 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -200,6 +200,8 @@ option sygusMinGrammar --sygus-min-grammar bool :default false
   minimize sygus grammars
 option sygusDecompose --sygus-decompose bool :default false
   decompose single invocation synthesis conjectures
+option sygusNormalForm --sygus-normal-form bool :default true
+  only search for sygus builtin terms that are in normal form
  
 
 option localTheoryExt --local-t-ext bool :default false
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 7813626a7..c15e103f9 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -140,6 +140,14 @@ void Datatype::addConstructor(const DatatypeConstructor& c) {
   d_constructors.push_back(c);
 }
 
+
+void Datatype::setSygusType( Type st ){
+  CheckArgument(!d_resolved, this,
+                "cannot set sygus type to a finalized Datatype");
+  d_sygus_type = st;
+}
+
+
 Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype is not yet resolved");
 
@@ -543,6 +551,15 @@ DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) :
   CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
 }
 
+DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester, Expr sygus_op) :
+  d_name(name + '\0' + tester),
+  d_tester(),
+  d_args(),
+  d_sygus_op(sygus_op) {
+  CheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
+  CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
+}
+
 void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
   // 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
@@ -611,6 +628,11 @@ Expr DatatypeConstructor::getTester() const {
   return d_tester;
 }
 
+Expr DatatypeConstructor::getSygusOp() const {
+  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  return d_sygus_op;
+}
+
 Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 32fae8235..084202956 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -185,6 +185,8 @@ private:
   Expr d_constructor;
   Expr d_tester;
   std::vector<DatatypeConstructorArg> d_args;
+  /** the operator associated with this constructor (for sygus) */
+  Expr d_sygus_op;
 
   void resolve(ExprManager* em, DatatypeType self,
                const std::map<std::string, DatatypeType>& resolutions,
@@ -223,6 +225,7 @@ public:
    * constructor and tester aren't created until resolution time.
    */
   DatatypeConstructor(std::string name, std::string tester);
+  DatatypeConstructor(std::string name, std::string tester, Expr sygus_op);
 
   /**
    * Add an argument (i.e., a data field) of the given name and type
@@ -268,6 +271,9 @@ public:
    * Datatype must be resolved.
    */
   Expr getTester() const;
+  
+  /** get sygus op */
+  Expr getSygusOp() const;
 
   /**
    * Get the tester name for this Datatype constructor.
@@ -453,6 +459,7 @@ private:
   bool d_resolved;
   Type d_self;
   bool d_involvesExt;
+  Type d_sygus_type;
 
   // "mutable" because computing the cardinality can be expensive,
   // and so it's computed just once, on demand---this is the cache
@@ -510,6 +517,9 @@ public:
    */
   void addConstructor(const DatatypeConstructor& c);
 
+  /** set the sygus type of this datatype */
+  void setSygusType( Type st );
+  
   /** Get the name of this Datatype. */
   inline std::string getName() const throw();
 
@@ -530,6 +540,9 @@ public:
 
   /** is this a co-datatype? */
   inline bool isCodatatype() const;
+  
+  /** is this a sygus datatype? */
+  inline bool isSygus() const;
 
   /**
    * Return the cardinality of this datatype (the sum of the
@@ -720,6 +733,10 @@ inline bool Datatype::isCodatatype() const {
   return d_isCo;
 }
 
+inline bool Datatype::isSygus() const {
+  return !d_sygus_type.isNull();
+}
+
 inline bool Datatype::operator!=(const Datatype& other) const throw() {
   return !(*this == other);
 }