Minor fixes to cbqi, purify-quant. Better error checking in addInstantiation.

5 files changed, 64 insertions, 29 deletions

diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 2530402ff..47281819f 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -321,8 +321,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
             bool pol = lit.getKind()!=NOT;
             if( pvtn.isReal() ){
               //arithmetic inequalities and disequalities
-              if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol ) ){
-                Assert( atom[0].getType().isInteger() || atom[0].getType().isReal() );
+              if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ){
                 Assert( atom.getKind()!=GEQ || atom[1].isConst() );
                 Node atom_lhs;
                 Node atom_rhs;
@@ -664,6 +663,7 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int b
   }
   //must ensure variables have been computed for n
   computeProgVars( n );
+  Assert( d_inelig.find( n )==d_inelig.end() );
 
   //substitute into previous substitutions, when applicable
   std::vector< Node > a_subs;
@@ -681,6 +681,7 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int b
   std::map< int, Node > prev_coeff;
   std::map< int, Node > prev_sym_subs;
   std::vector< Node > new_has_coeff;
+  Trace("cbqi-inst-debug2") << "Applying substitutions..." << std::endl;
   for( unsigned j=0; j<sf.d_subs.size(); j++ ){
     Assert( d_prog_var.find( sf.d_subs[j] )!=d_prog_var.end() );
     if( d_prog_var[sf.d_subs[j]].find( pv )!=d_prog_var[sf.d_subs[j]].end() ){
@@ -705,12 +706,16 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int b
         }
         if( sf.d_subs[j]!=prev_subs[j] ){
           computeProgVars( sf.d_subs[j] );
+          Assert( d_inelig.find( sf.d_subs[j] )==d_inelig.end() );
         }
+        Trace("cbqi-inst-debug2") << "Subs " << j << " " << sf.d_subs[j] << std::endl;
       }else{
-        Trace("cbqi-inst-debug") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl;
+        Trace("cbqi-inst-debug2") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl;
         success = false;
         break;
       }
+    }else{
+      Trace("cbqi-inst-debug2") << "Skip " << j << " " << sf.d_subs[j] << std::endl;
     }
     if( options::cbqiSymLia() && pv_coeff.isNull() ){
       //apply simple substitutions also to sym_subs
@@ -1483,7 +1488,13 @@ int CegInstantiator::isolate( Node pv, Node atom, Node& veq_c, Node& val, Node&
     ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() );
     if( ires!=0 ){
       Node realPart;
-      Trace("cbqi-inst-debug") << "Isolate : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl;
+      if( Trace.isOn("cbqi-inst-debug") ){
+        Trace("cbqi-inst-debug") << "Isolate : ";
+        if( !veq_c.isNull() ){
+          Trace("cbqi-inst-debug") << veq_c << " * ";
+        }
+        Trace("cbqi-inst-debug") << pv << " " << atom.getKind() << " " << val << std::endl;
+      }
       if( options::cbqiAll() ){
         // when not pure LIA/LRA, we must check whether the lhs contains pv
         if( TermDb::containsTerm( val, pv ) ){
@@ -1529,8 +1540,9 @@ int CegInstantiator::isolate( Node pv, Node atom, Node& veq_c, Node& val, Node&
         Trace("cbqi-inst-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl;
         Trace("cbqi-inst-debug") << "                 real part : " << realPart << std::endl;
         if( ires!=0 ){
-          val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires==-1 ? PLUS : MINUS,
-                                    NodeManager::currentNM()->mkNode( ires==-1 ? MINUS : PLUS, val, realPart ),
+          int ires_use = ( msum[pv].isNull() || msum[pv].getConst<Rational>().sgn()==1 ) ? 1 : -1;
+          val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires_use==-1 ? PLUS : MINUS,
+                                    NodeManager::currentNM()->mkNode( ires_use==-1 ? MINUS : PLUS, val, realPart ),
                                     NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) );
           Trace("cbqi-inst-debug") << "result : " << val << std::endl;
           Assert( val.getType().isInteger() );
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 39cde56e8..b26f24c63 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -621,8 +621,12 @@ bool InstStrategyCegqi::addLemma( Node lem ) {
 
 bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
   if( n.getKind()==INST_CONSTANT || n.getKind()==SKOLEM ){
-    //only legal if current quantified formula contains n
-    return TermDb::containsTerm( d_curr_quant, n );
+    if( n.getKind()==SKOLEM && d_quantEngine->getTermDatabase()->containsVtsTerm( n ) ){
+      return true;
+    }else{
+      //only legal if current quantified formula contains n
+      return TermDb::containsTerm( d_curr_quant, n );
+    }
   }else{
     return true;
   }
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index dcf58e692..8f055473d 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -83,10 +83,10 @@ bool QuantifiersRewriter::isCube( Node n ){
   }
 }
 
-int QuantifiersRewriter::getPurifyId( Node n ){
+int QuantifiersRewriter::getPurifyId( Node n, std::vector< Node >& args ){
   if( inst::Trigger::isAtomicTriggerKind( n.getKind() ) ){
     return 1;
-  }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL ){
+  }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL || n.getKind()==BOUND_VARIABLE || !TermDb::containsTerms( n, args ) ){
     return 0;
   }else{
     return -1;
@@ -196,7 +196,6 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
 
 RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
   Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl;
-  Trace("quantifiers-rewrite-debug") << "Attributes : " << std::endl;
   if( !options::quantRewriteRules() || !TermDb::isRewriteRule( in ) ){
     RewriteStatus status = REWRITE_DONE;
     Node ret = in;
@@ -769,7 +768,7 @@ Node QuantifiersRewriter::computeProcessIte( Node body, Node ipl ){
   return body;
 }
 
-bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent ) {
+bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ) {
   if( TermDb::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){
     return false;
   }else{
@@ -777,7 +776,7 @@ bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::map< Node, std::v
       std::map< Node, std::vector< int > >::iterator it = var_parent.find( v );
       if( it!=var_parent.end() ){
         Assert( !it->second.empty() );
-        int id = getPurifyId( s );
+        int id = getPurifyId( s, args );
         return it->second.size()==1 && it->second[0]==id;
       }
     }
@@ -791,7 +790,8 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto
     for( unsigned i=0; i<2; i++ ){
       std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit[i] );
       if( ita!=args.end() ){
-        if( isVariableElim( lit[i], lit[1-i], var_parent ) ){
+        if( isVariableElim( lit[i], lit[1-i], args, var_parent ) ){
+          Trace("var-elim-quant") << "Variable eliminate based on equality : " << lit[i] << " -> " << lit[1-i] << std::endl;
           vars.push_back( lit[i] );
           subs.push_back( lit[1-i] );
           args.erase( ita );
@@ -809,7 +809,8 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto
             Node veq_c;
             Node val;
             int ires = QuantArith::isolate( itm->first, msum, veq_c, val, EQUAL );
-            if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val, var_parent ) ){
+            if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val, args, var_parent ) ){
+              Trace("var-elim-quant") << "Variable eliminate based on solved equality : " << itm->first << " -> " << val << std::endl;
               vars.push_back( itm->first );
               subs.push_back( val );
               args.erase( ita );
@@ -873,7 +874,7 @@ Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >
     }
   }
   if( !vars.empty() ){
-    Trace("var-elim-quant") << "VE " << vars.size() << "/" << args.size() << std::endl;
+    Trace("var-elim-quant-debug") << "VE " << vars.size() << "/" << args.size() << std::endl;
     //remake with eliminated nodes
     body = body.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
     body = Rewriter::rewrite( body );
@@ -1688,12 +1689,24 @@ Node QuantifiersRewriter::computePurify2( Node body, std::vector< Node >& args,
     return it->second;
   }else{
     Node ret = body;
-    if( body.getNumChildren()>0 && body.getKind()!=FORALL ){
+    if( body.getNumChildren()>0 && body.getKind()!=FORALL && TermDb::containsTerms( ret, args ) ){
       std::vector< Node > children;
       bool childrenChanged = false;
-      int id = getPurifyId( body );
+      int id = getPurifyId( body, args );
       for( unsigned i=0; i<body.getNumChildren(); i++ ){
-        Node bi = computePurify2( body[i], args, visited, var_to_term, var_parent, id );
+        Node bi;
+        if( body.getKind()==EQUAL && i==1 ){
+          int cid = getPurifyId( children[0], args );
+          bi = computePurify2( body[i], args, visited, var_to_term, var_parent, cid );
+          if( children[0].getKind()==BOUND_VARIABLE ){
+            cid = getPurifyId( bi, args );
+            if( cid!=0 && std::find( var_parent[children[0]].begin(), var_parent[children[0]].end(), cid )==var_parent[children[0]].end() ){
+              var_parent[children[0]].push_back( id );
+            }
+          }
+        }else{
+          bi = computePurify2( body[i], args, visited, var_to_term, var_parent, id );
+        }
         childrenChanged = childrenChanged || bi!=body[i];
         children.push_back( bi );
         if( id!=0 && bi.getKind()==BOUND_VARIABLE ){
@@ -1709,13 +1722,10 @@ Node QuantifiersRewriter::computePurify2( Node body, std::vector< Node >& args,
         ret = NodeManager::currentNM()->mkNode( body.getKind(), children );
       }
       if( parentId!=0 && parentId!=id ){
-        //must purify if this has a bound variable
-        if( TermDb::containsTerms( ret, args ) ){
-          Node v = NodeManager::currentNM()->mkBoundVar( ret.getType() );
-          var_to_term[v] = Rewriter::rewrite( v.eqNode( ret ) );
-          ret = v;
-          args.push_back( v );
-        }
+        Node v = NodeManager::currentNM()->mkBoundVar( ret.getType() );
+        var_to_term[v] = Rewriter::rewrite( v.eqNode( ret ) );
+        ret = v;
+        args.push_back( v );
       }
     }
     visited[body] = ret;
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index daf5a8bad..607fd9191 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -31,7 +31,7 @@ public:
   static bool isClause( Node n );
   static bool isLiteral( Node n );
   static bool isCube( Node n );
-  static int getPurifyId( Node n );
+  static int getPurifyId( Node n, std::vector< Node >& args );
 private:
   static void addNodeToOrBuilder( Node n, NodeBuilder<>& t );
   static Node mkForAll( std::vector< Node >& args, Node body, Node ipl );
@@ -41,7 +41,7 @@ private:
   static Node computeClause( Node n );
   static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj );
   static bool isConditionalVariableElim( Node n, int pol=0 );
-  static bool isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent );
+  static bool isVariableElim( Node v, Node s, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent );
   static bool computeVariableElimLit( Node n, bool pol, std::vector< Node >& args, std::vector< Node >& var, std::vector< Node >& subs,
                                       std::map< Node, std::vector< int > >& var_parent );
   static Node computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term,
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 990d3389e..584295c17 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -709,7 +709,16 @@ bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& v
         Trace("inst") << std::endl;
       }
       if( options::cbqi() ){
-        if( quantifiers::TermDb::getInstConstAttr(terms[i])==f ){
+        Node icf = quantifiers::TermDb::getInstConstAttr(terms[i]);
+        bool bad_inst = false;
+        if( !icf.isNull() ){
+          if( icf==f ){
+            bad_inst = true;
+          }else{
+            bad_inst = quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[f] );
+          }
+        }
+        if( bad_inst ){
           Trace("inst")<< "***& Bad Instantiate " << f << " with " << std::endl;
           for( unsigned i=0; i<terms.size(); i++ ){
             Trace("inst") << "   " << terms[i] << std::endl;