Support for arbitrary constants/variables in Sygus grammars.

1 files changed, 11 insertions, 9 deletions

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 6c32ccb4a..62eb78679 100644
--- 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;