From eee182ae7479d688aec42f630d2aa6b2636cc2f9 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 18 Sep 2015 14:21:13 +0200
Subject: [PATCH] More work mixing UF and sygus.

---
 src/parser/smt2/Smt2.g       |  2 ++
 src/parser/smt2/smt2.cpp     | 13 +++++++++----
 src/smt/smt_engine.cpp       |  3 +++
 src/theory/datatypes/options |  2 +-
 4 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 4e5c27e3d..cfcc7df99 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -396,6 +396,7 @@ command returns [CVC4::Command* cmd = NULL]
     { cmd = new GetUnsatCoreCommand(PARSER_STATE->getUnsatCoreNames()); }
   | /* push */
     PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    { if( PARSER_STATE->sygus() ){ PARSER_STATE->parseError("Sygus does not support push command."); } }
     ( k=INTEGER_LITERAL
       { unsigned n = AntlrInput::tokenToUnsigned(k);
         if(n == 0) {
@@ -425,6 +426,7 @@ command returns [CVC4::Command* cmd = NULL]
         }
       } )
   | POP_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    { if( PARSER_STATE->sygus() ){ PARSER_STATE->parseError("Sygus does not support pop command."); } }
     ( k=INTEGER_LITERAL
       { unsigned n = AntlrInput::tokenToUnsigned(k);
         if(n > PARSER_STATE->scopeLevel()) {
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 7e621f56b..d3af9143a 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -344,6 +344,8 @@ void Smt2::setLogic(std::string name) {
       name = "UFLIRA";
     } else if(name == "BV") {
       name = "UFBV";
+    } else if(name == "ALL_SUPPORTED") {
+      //no change
     } else {
       std::stringstream ss;
       ss << "Unknown SyGuS background logic `" << name << "'";
@@ -513,7 +515,7 @@ Expr Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed)
 }
 
 void collectSygusGrammarTypesFor( Type range, std::vector< Type >& types, std::map< Type, std::vector< DatatypeConstructorArg > >& sels ){
-  if( range.isInteger() || range.isBitVector() || range.isDatatype() ){
+  if( !range.isBoolean() ){
     if( std::find( types.begin(), types.end(), range )==types.end() ){
       Debug("parser-sygus") << "...will make grammar for " << range << std::endl;
       types.push_back( range );
@@ -534,9 +536,9 @@ void collectSygusGrammarTypesFor( Type range, std::vector< Type >& types, std::m
 void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes,
                                   std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars, int& startIndex ) {
 
-  if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){
-    parseError("No default grammar for type.");
-  }
+  //if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){
+  //  parseError("No default grammar for type.");
+  //}
   startIndex = -1;
   Debug("parser-sygus") << "Construct default grammar for " << fun << " " << range << std::endl;
   std::map< CVC4::Type, CVC4::Type > sygus_to_builtin;
@@ -628,6 +630,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
         cargs.push_back( std::vector< CVC4::Type >() );
         for( unsigned j=0; j<dt[k].getNumArgs(); j++ ){
           Type crange = ((SelectorType)dt[k][j].getType()).getRangeType();
+          //Assert( type_to_unres.find(crange)!=type_to_unres.end() );
           cargs.back().push_back( type_to_unres[crange] );
         }
       }
@@ -645,6 +648,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
         ops[i].push_back( sels[types[i]][j].getSelector() );
         cnames.push_back( sels[types[i]][j].getName() );
         cargs.push_back( std::vector< CVC4::Type >() );
+        //Assert( type_to_unres.find(arg_type)!=type_to_unres.end() );
         cargs.back().push_back( type_to_unres[arg_type] );
       }
     }
@@ -1324,6 +1328,7 @@ void Smt2::addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::
   CVC4::DatatypeConstructor c(name, testerId );
   c.setSygus( op, let_body, let_args, let_num_input_args );
   for( unsigned j=0; j<cargs.size(); j++ ){
+    Debug("parser-sygus-debug") << "  arg " << j << " : " << cargs[j] << std::endl;
     std::stringstream sname;
     sname << name << "_" << j;
     c.addArg(sname.str(), cargs[j]);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0af5c7fc1..519f330df 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1419,6 +1419,9 @@ void SmtEngine::setDefaults() {
     if( !options::bitvectorDivByZeroConst.wasSetByUser() ){
       options::bitvectorDivByZeroConst.set( true );
     }
+    if( !options::dtRewriteErrorSel.wasSetByUser() ){
+      options::dtRewriteErrorSel.set( true );
+    }
     //do not miniscope
     if( !options::miniscopeQuant.wasSetByUser() ){
       options::miniscopeQuant.set( false );
diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options
index 592e9e67e..6da0fe244 100644
--- a/src/theory/datatypes/options
+++ b/src/theory/datatypes/options
@@ -9,7 +9,7 @@ module DATATYPES "theory/datatypes/options.h" Datatypes theory
 # then we do not rewrite such a selector term to an arbitrary ground term.  
 # For example, by default cvc4 considers cdr( nil ) = nil.  If this option is set, then
 # cdr( nil ) has no set value.
-expert-option dtRewriteErrorSel --dt-rewrite-error-sel bool :default false
+expert-option dtRewriteErrorSel --dt-rewrite-error-sel bool :default false :read-write
  rewrite incorrectly applied selectors to arbitrary ground term
 option dtForceAssignment --dt-force-assignment bool :default false :read-write
  force the datatypes solver to give specific values to all datatypes terms before answering sat
-- 
2.30.2