From 86ad2ca93048844eedcafd2a2dadc43ef85dfb32 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 1 Aug 2015 17:22:11 +0200
Subject: [PATCH] Simplification/improvement to solving deltas in LRA cbqi. Bug
 fix sygus datatypes.

---
 src/parser/smt2/smt2.cpp                      |  6 +--
 src/theory/quantifiers/inst_strategy_cbqi.cpp | 43 +++----------------
 src/theory/quantifiers/inst_strategy_cbqi.h   |  2 -
 3 files changed, 7 insertions(+), 44 deletions(-)

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index cc3b09cfe..7e621f56b 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -545,11 +545,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
   std::map< Type, std::vector< DatatypeConstructorArg > > sels;
   //types for each of the variables
   for( unsigned i=0; i<sygus_vars.size(); i++ ){
-    Type t = sygus_vars[i].getType();
-    if( !t.isBoolean() && std::find( types.begin(), types.end(), t )==types.end() ){
-      Debug("parser-sygus") << "...will make grammar for " << t << std::endl;
-      types.push_back( t );
-    }
+    collectSygusGrammarTypesFor( sygus_vars[i].getType(), types, sels );
   }
   //types connected to range
   collectSygusGrammarTypesFor( range, types, sels );
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 0c4648e51..20bd71b45 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -56,16 +56,10 @@ void CegInstantiator::computeProgVars( Node n ){
         d_inelig[n] = true;
         return;
       }
-      if( d_has_delta.find( n[i] )!=d_has_delta.end() ){
-        d_has_delta[n] = true;
-      }
       for( std::map< Node, bool >::iterator it = d_prog_var[n[i]].begin(); it != d_prog_var[n[i]].end(); ++it ){
         d_prog_var[n][it->first] = true;
       }
     }
-    if( n==d_n_delta ){
-      d_has_delta[n] = true;
-    }
   }
 }
 
@@ -108,12 +102,6 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                 ns = n;
                 proc = true;
               }
-              if( d_has_delta.find( ns )!=d_has_delta.end() ){
-                //also must set delta to zero
-                ns = ns.substitute( (TNode)d_n_delta, (TNode)d_zero );
-                ns = Rewriter::rewrite( ns );
-                computeProgVars( ns );
-              }
               if( proc ){
                 //try the substitution
                 subs_proc[0][ns][pv_coeff] = true;
@@ -180,9 +168,6 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                       Trace("cegqi-si-inst-debug") << "...equality is " << eq << std::endl;
                       std::map< Node, Node > msum;
                       if( QuantArith::getMonomialSumLit( eq, msum ) ){
-                        if( !d_n_delta.isNull() ){
-                          msum.erase( d_n_delta );
-                        }
                         if( Trace.isOn("cegqi-si-inst-debug") ){
                           Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl;
                           QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" );
@@ -269,9 +254,6 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                   Trace("cegqi-si-inst-debug") << "       substituted : " << satom << ", pol = " << pol << std::endl;
                   std::map< Node, Node > msum;
                   if( QuantArith::getMonomialSumLit( satom, msum ) ){
-                    if( !d_n_delta.isNull() ){
-                      msum.erase( d_n_delta );
-                    }
                     if( Trace.isOn("cegqi-si-inst-debug") ){
                       Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl;
                       QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" );
@@ -358,6 +340,11 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
 bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars,
                                            std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
                                            unsigned i, unsigned effort ) {
+  if( styp==2 || styp==-2 ){
+    Node delta = d_qe->getTermDatabase()->getVtsDelta();
+    n = NodeManager::currentNM()->mkNode( styp==2 ? PLUS : MINUS, n, delta );
+    n = Rewriter::rewrite( n );
+  }
   //must ensure variables have been computed for n
   computeProgVars( n );
   //substitute into previous substitutions, when applicable
@@ -530,25 +517,7 @@ bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vec
 }
 
 bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ ) {
-  // do delta rationals
-  std::map< int, Node > prev;
-  for( unsigned i=0; i<subs.size(); i++ ){
-    if( subs_typ[i]==2 || subs_typ[i]==-2 ){
-      prev[i] = subs[i];
-      Node delta = d_qe->getTermDatabase()->getVtsDelta();
-      d_n_delta = delta;
-      subs[i] = NodeManager::currentNM()->mkNode( subs_typ[i]==2 ? PLUS : MINUS, subs[i], delta );
-    }
-  }
-  //check if we have already added this instantiation
-  bool success = d_out->addInstantiation( subs, subs_typ );
-  if( !success ){
-    //revert the substitution
-    for( std::map< int, Node >::iterator it = prev.begin(); it != prev.end(); ++it ){
-      subs[it->first] = it->second;
-    }
-  }
-  return success;
+  return d_out->addInstantiation( subs, subs_typ );
 }
 
 
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 99c048013..0e6227606 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -51,13 +51,11 @@ private:
   Node d_zero;
   Node d_one;
   Node d_true;
-  Node d_n_delta;
   QuantifiersEngine * d_qe;
   CegqiOutput * d_out;
   //program variable contains cache
   std::map< Node, std::map< Node, bool > > d_prog_var;
   std::map< Node, bool > d_inelig;
-  std::map< Node, bool > d_has_delta;
 private:
   //for adding instantiations during check
   void computeProgVars( Node n );
-- 
2.30.2