Support for arbitrary constants/variables in Sygus grammars.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index c7c82b2d84ca5789aaf4bc13c1bd9646fa39a268..57ef44df04e8f92ddeb86fdcf56979b067fcd357 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -488,6 +488,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
   Type t, range;
   std::vector<Expr> terms;
   std::vector<Type> sorts;
+  std::vector<Expr> sygus_vars;
   std::vector<std::pair<std::string, Type> > sortedVarNames;
   SExpr sexpr;
   CommandSequence* seq;
@@ -495,6 +496,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
   std::vector< std::vector<Expr> > ops;
   std::vector< std::vector< std::string > > cnames;
   std::vector< std::vector< std::vector< CVC4::Type > > > cargs;
+  bool allow_const;
 }
   : /* set the logic */
     SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT]
@@ -584,7 +586,9 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
             sortedVarNames.begin(), iend = sortedVarNames.end();
           i != iend;
           ++i) {
-        terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
+        Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second);
+        terms.push_back( v );
+        sygus_vars.push_back( v );
       }
       Expr bvl;
       if( !terms.empty() ){
@@ -603,7 +607,6 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
         std::string dname = ss.str();
         sorts.push_back(t);
         datatypes.push_back(Datatype(dname));
-        datatypes.back().setSygus( t, terms[0] );
         ops.push_back(std::vector<Expr>());
         cnames.push_back(std::vector<std::string>());
         cargs.push_back(std::vector<std::vector<CVC4::Type> >());
@@ -611,12 +614,14 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
           // if not unresolved, must be undeclared
           PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
         }
+        allow_const = false;
       }
       // Note the official spec for NTDef is missing the ( parens )
       // but they are necessary to parse SyGuS examples
-      LPAREN_TOK sygusGTerm[fun, ops.back(), cnames.back(), cargs.back()]+ RPAREN_TOK
+      LPAREN_TOK sygusGTerm[fun, ops.back(), cnames.back(), cargs.back(), sygus_vars, allow_const]+ RPAREN_TOK
       RPAREN_TOK
-      { PARSER_STATE->mkSygusDatatype( datatypes.back(), ops.back(), cnames.back(), cargs.back() );
+      { datatypes.back().setSygus( t, terms[0], allow_const );
+        PARSER_STATE->mkSygusDatatype( datatypes.back(), ops.back(), cnames.back(), cargs.back() );
         PARSER_STATE->popScope(); }
     )+
     RPAREN_TOK
@@ -705,7 +710,10 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
 
 // SyGuS grammar term
 // fun is the name of the synth-fun this grammar term is for
-sygusGTerm[std::string& fun, std::vector<CVC4::Expr>& ops, std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs]
+// this adds N operators to ops, N names to cnames and N type argument vectors to cargs (where typically N=1)
+sygusGTerm[std::string& fun, std::vector<CVC4::Expr>& ops, std::vector<std::string>& cnames, 
+           std::vector< std::vector< CVC4::Type > >& cargs, std::vector<CVC4::Expr>& sygus_vars,
+           bool& allow_const]
 @declarations {
   std::string name;
   Kind k;
@@ -713,6 +721,8 @@ sygusGTerm[std::string& fun, std::vector<CVC4::Expr>& ops, std::vector<std::stri
   CVC4::DatatypeConstructor* ctor = NULL;
   unsigned count = 0;
   std::string sname;
+  // 0 an operator, 1 any constant, 2 any variable
+  unsigned gtermType = 0;
 }
   : LPAREN_TOK
     ( builtinOp[k]
@@ -725,35 +735,49 @@ sygusGTerm[std::string& fun, std::vector<CVC4::Expr>& ops, std::vector<std::stri
       }
     | symbol[name,CHECK_NONE,SYM_VARIABLE]
       { 
-        bool isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name);
-        if(isBuiltinOperator) {
-          Kind k = PARSER_STATE->getOperatorKind(name);
-          if( k==CVC4::kind::BITVECTOR_UDIV ){
-            k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
-          }
-          ops.push_back(EXPR_MANAGER->operatorOf(k));
-          name = kind::kindToString(k);
+        if(name=="Constant"){
+          gtermType = 1;
+          Debug("parser-sygus") << "Sygus grammar constant." << std::endl;
+        }else if(name=="Variable"){
+          gtermType = 2;
+          allow_const = true;
+          Debug("parser-sygus") << "Sygus grammar variable." << std::endl;
         }else{
-          // what is this sygus term trying to accomplish here, if the
-          // symbol isn't yet declared?!  probably the following line will
-          // fail, but we need an operator to continue here..
-          Debug("parser-sygus") << "Sygus grammar " << fun;
-          Debug("parser-sygus") << " : op (declare=" <<  PARSER_STATE->isDeclared(name) << ", define=" << PARSER_STATE->isDefinedFunction(name) << ") : " << name << std::endl;
-          if( !PARSER_STATE->isDefinedFunction(name) ){
-            PARSER_STATE->parseError(std::string("Functions in sygus grammars must be defined."));
+          bool isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name);
+          if(isBuiltinOperator) {
+            Kind k = PARSER_STATE->getOperatorKind(name);
+            if( k==CVC4::kind::BITVECTOR_UDIV ){
+              k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
+            }
+            ops.push_back(EXPR_MANAGER->operatorOf(k));
+            name = kind::kindToString(k);
+          }else{
+            // what is this sygus term trying to accomplish here, if the
+            // symbol isn't yet declared?!  probably the following line will
+            // fail, but we need an operator to continue here..
+            Debug("parser-sygus") << "Sygus grammar " << fun;
+            Debug("parser-sygus") << " : op (declare=" <<  PARSER_STATE->isDeclared(name) << ", define=" << PARSER_STATE->isDefinedFunction(name) << ") : " << name << std::endl;
+            if( !PARSER_STATE->isDefinedFunction(name) ){
+              PARSER_STATE->parseError(std::string("Functions in sygus grammars must be defined."));
+            }
+            ops.push_back( PARSER_STATE->getVariable(name) );
           }
-          ops.push_back( PARSER_STATE->getVariable(name) );
         }
       }
     )
-    { cnames.push_back( name );
+    { if( gtermType==0 ){
+        cnames.push_back( name );
+      }
       cargs.push_back( std::vector< CVC4::Type >() );
     }
     ( //sortSymbol[t,CHECK_NONE]
       symbol[sname,CHECK_NONE,SYM_VARIABLE]
-      { std::stringstream ss;
-        ss << fun << "_" << sname;
-        sname = ss.str();
+      { 
+        if( gtermType==0 ){
+          std::stringstream ss;
+          ss << fun << "_" << sname;
+          sname = ss.str();
+        }
         if( PARSER_STATE->isDeclared(sname, SYM_SORT) ) {
           t = PARSER_STATE->getSort(sname);
         } else {
@@ -761,6 +785,40 @@ sygusGTerm[std::string& fun, std::vector<CVC4::Expr>& ops, std::vector<std::stri
         }
         cargs.back().push_back(t);
       } )+ RPAREN_TOK
+      {
+        if( gtermType==1 || gtermType==2 ){
+          if( cargs.back().size()!=1 ){
+            PARSER_STATE->parseError(std::string("Must provide single sort for constant/variable Sygus constructor."));
+          }
+          Type t = cargs.back()[0];
+          cargs.pop_back();
+          Debug("parser-sygus") << "Make constructors for Constant/Variable of type " << t << std::endl;
+          if( gtermType==1 ){
+            //PARSER_STATE->parseError(std::string("Constant/Variable in sygus not supported."));
+            std::vector< Expr > consts;
+            PARSER_STATE->mkSygusConstantsForType( t, consts );
+            for( unsigned i=0; i<consts.size(); i++ ){
+              std::stringstream ss;
+              ss << consts[i];
+              Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
+              ops.push_back( consts[i] );
+              cnames.push_back( ss.str() );
+              cargs.push_back( std::vector< CVC4::Type >() );
+            }
+          }else if( gtermType==2 ){
+            for( unsigned i=0; i<sygus_vars.size(); i++ ){
+              if( sygus_vars[i].getType()==t ){
+                std::stringstream ss;
+                ss << sygus_vars[i];
+                Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
+                ops.push_back( sygus_vars[i] );
+                cnames.push_back( ss.str() );
+                cargs.push_back( std::vector< CVC4::Type >() );
+              }
+            }
+          }
+        }
+      }
   | INTEGER_LITERAL
     { Debug("parser-sygus") << "Sygus grammar " << fun << " : integer literal " << AntlrInput::tokenText($INTEGER_LITERAL) << std::endl;
       ops.push_back(MK_CONST(Rational(AntlrInput::tokenText($INTEGER_LITERAL))));

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index bf0e57eca0bbbf3104394bc311b7d893237f3eda..10e742d4505a6538ff559cbcad15b1dd0df8687e 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -21,6 +21,8 @@
 #include "parser/smt2/smt2.h"
 #include "parser/antlr_input.h"
 
+#include "util/bitvector.h"
+
 // ANTLR defines these, which is really bad!
 #undef true
 #undef false
@@ -495,8 +497,21 @@ void Smt2::includeFile(const std::string& filename) {
 }
 
 
+void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) {
+  if( type.isInteger() ){
+    ops.push_back(getExprManager()->mkConst(Rational(0)));
+    ops.push_back(getExprManager()->mkConst(Rational(1)));
+  }else if( type.isBitVector() ){
+    unsigned sz = ((BitVectorType)type).getSize();
+    BitVector bval0(sz, (unsigned int)0);
+    ops.push_back( getExprManager()->mkConst(bval0) );
+    BitVector bval1(sz, (unsigned int)1);
+    ops.push_back( getExprManager()->mkConst(bval1) );
+  }
+  //TODO : others?
+}
 
- void Smt2::defineSygusFuns() {
+void Smt2::defineSygusFuns() {
   // only define each one once
   while(d_nextSygusFun < d_sygusFuns.size()) {
     std::pair<std::string, Expr> p = d_sygusFuns[d_nextSygusFun];

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index ed6a5128b5cee522479368f7b347fa99e79501c4..67c019d50c006c5eeeb7248cc499b58ff0f6f627 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -178,6 +178,8 @@ public:
     return e;
   }
 
+  void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops );
+  
   void addSygusFun(const std::string& fun, Expr eval) {
     d_sygusFuns.push_back(std::make_pair(fun, eval));
   }

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 6c32ccb4a66588e2f34460d26f7e7024608c4231..62eb786797661bb8a1930a32c79b529f5df209f6 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1586,16 +1586,18 @@ Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn ) {
     const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
     Assert( dt.isSygus() );
     Node sc;
-    int carg = getOpArg( tn, c );
-    if( carg!=-1 ){
-      sc = Node::fromExpr( dt[carg].getSygusOp() );
+    // if we are not interested in reconstructing constants, or the grammar allows them, return a proxy
+    if( !options::cegqiSingleInvReconstructConst() || dt.getSygusAllowConst() ){
+      Node k = NodeManager::currentNM()->mkSkolem( "sy", tn, "sygus proxy" );
+      SygusProxyAttribute spa;
+      k.setAttribute(spa,c);
+      sc = k;
     }else{
-      //TODO
-      if( !options::cegqiSingleInvReconstructConst() ){
-        Node k = NodeManager::currentNM()->mkSkolem( "sy", tn, "sygus proxy" );
-        SygusProxyAttribute spa;
-        k.setAttribute(spa,c);
-        sc = k;
+      int carg = getOpArg( tn, c );
+      if( carg!=-1 ){
+        sc = Node::fromExpr( dt[carg].getSygusOp() );
+      }else{
+        //TODO
       }
     }
     d_builtin_const_to_sygus[tn][c] = sc;

diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 1e310251cd5ff01880b38cc91ff7ae8dc9be1abf..18ef25e7fd63353cce5018a59ddd206d5b4b3341 100644 (file)
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -134,11 +134,12 @@ void Datatype::addConstructor(const DatatypeConstructor& c) {
 }
 
 
-void Datatype::setSygus( Type st, Expr bvl ){
+void Datatype::setSygus( Type st, Expr bvl, bool allow_const ){
   CheckArgument(!d_resolved, this,
                 "cannot set sygus type to a finalized Datatype");
   d_sygus_type = st;
   d_sygus_bvl = bvl;
+  d_sygus_allow_const = allow_const;
 }
 
 
@@ -470,6 +471,10 @@ Expr Datatype::getSygusVarList() const {
   return d_sygus_bvl;
 }
 
+bool Datatype::getSygusAllowConst() const {
+  return d_sygus_allow_const;
+}
+
 bool Datatype::involvesExternalType() const{
   return d_involvesExt;
 }

diff --git a/src/util/datatype.h b/src/util/datatype.h
index 6e7e09fa089a255b5972a1ce748f4ed3ef25d174..79e7bf7d7eecb0719b4a1a3cf080eb45a27a2c7a 100644 (file)
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -456,6 +456,7 @@ private:
   /** information for sygus */
   Type d_sygus_type;
   Expr d_sygus_bvl;  
+  bool d_sygus_allow_const;
 
   // "mutable" because computing the cardinality can be expensive,
   // and so it's computed just once, on demand---this is the cache
@@ -534,8 +535,9 @@ public:
   /** set the sygus information of this datatype
    *    st : the builtin type for this grammar
    *    bvl : the list of arguments for the synth-fun
+   *    allow_const : whether all constants are (implicitly) included in the grammar
    */
-  void setSygus( Type st, Expr bvl );
+  void setSygus( Type st, Expr bvl, bool allow_const );
   
   /** Get the name of this Datatype. */
   inline std::string getName() const throw();
@@ -664,6 +666,8 @@ public:
   Type getSygusType() const;
   /** get sygus var list */
   Expr getSygusVarList() const;
+  /** does it allow constants */
+  bool getSygusAllowConst() const;
 
   /**
    * Get whether this datatype involves an external type.  If so,

diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index efa656e7bb86c2c0ff84365434fc4b804a7296aa..4f9d233fd751210ac78ffdf5b5a423afc00e15af 100644 (file)
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -28,7 +28,8 @@ TESTS = commutative.sy \
        twolets1.sy \
        array_search_2.sy \        
        hd-01-d1-prog.sy \
-        icfp_28_10.sy
+        icfp_28_10.sy \
+        const-var-test.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \