Do not eliminate variables only occurring in patterns. Minor improvements to sort...

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 0f2adf3b40eff53624531e61e55ae89aecf0edcb..29640e18f196bb4124f6deecfd0b4431c68ea452 100644 (file)
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -101,6 +101,7 @@ Node CandidateGeneratorQE::getNextCandidate(){
     //get next candidate term in the uf term database
     while( d_term_iter<d_term_iter_limit ){
       Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter];
+      //Assert( d_qe->getEqualityQuery()->hasTerm( n ) );
       d_term_iter++;
       if( isLegalCandidate( n ) ){
         return n;
@@ -126,41 +127,6 @@ Node CandidateGeneratorQE::getNextCandidate(){
   return Node::null();
 }
 
-//CandidateGeneratorQEDisequal::CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc ) :
-//  d_qe( qe ), d_eq_class( eqc ){
-//  d_eci = NULL;
-//}
-//void CandidateGeneratorQEDisequal::resetInstantiationRound(){
-//
-//}
-////we will iterate over all terms that are disequal from eqc
-//void CandidateGeneratorQEDisequal::reset( Node eqc ){
-//  //Assert( !eqc.isNull() );
-//  ////begin iterating over equivalence classes that are disequal from eqc
-//  //d_eci = d_ith->getEquivalenceClassInfo( eqc );
-//  //if( d_eci ){
-//  //  d_eqci_iter = d_eci->d_disequal.begin();
-//  //}
-//}
-//Node CandidateGeneratorQEDisequal::getNextCandidate(){
-//  //if( d_eci ){
-//  //  while( d_eqci_iter != d_eci->d_disequal.end() ){
-//  //    if( (*d_eqci_iter).second ){
-//  //      //we have an equivalence class that is disequal from eqc
-//  //      d_cg->reset( (*d_eqci_iter).first );
-//  //      Node n = d_cg->getNextCandidate();
-//  //      //if there is a candidate in this equivalence class, return it
-//  //      if( !n.isNull() ){
-//  //        return n;
-//  //      }
-//  //    }
-//  //    ++d_eqci_iter;
-//  //  }
-//  //}
-//  return Node::null();
-//}
-
-
 CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) :
   d_match_pattern( mpat ), d_qe( qe ){
 

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index d58ce14b16975fd0eb754961fd3cc57fb03771e5..768ba63dec6f5f6e814f38dc8a193e88fb4ee6ae 100755 (executable)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1886,8 +1886,7 @@ Node QuantConflictFind::evaluateTerm( Node n ) {
 \r
 /** new node */\r
 void QuantConflictFind::newEqClass( Node n ) {\r
-  //Trace("qcf-proc-debug") << "QCF : newEqClass : " << n << std::endl;\r
-  //Trace("qcf-proc2-debug") << "QCF : finished newEqClass : " << n << std::endl;\r
+\r
 }\r
 \r
 /** merge */\r

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index fb7ff679bdef4b7664f925d69af2bc42195da0ea..0d338f283347dbcd1ca302304887964060e6b496 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -105,6 +105,7 @@ void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::map< Node
 }
 
 void QuantifiersRewriter::computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ) {
+  Assert( activeArgs.empty() );
   std::map< Node, bool > activeMap;
   computeArgs( args, activeMap, n );
   for( unsigned i=0; i<args.size(); i++ ){
@@ -114,6 +115,17 @@ void QuantifiersRewriter::computeArgVec( std::vector< Node >& args, std::vector<
   }
 }
 
+void QuantifiersRewriter::computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl ) {
+  Assert( activeArgs.empty() );
+  std::map< Node, bool > activeMap;
+  computeArgs( args, activeMap, n );
+  computeArgs( args, activeMap, ipl );
+  for( unsigned i=0; i<args.size(); i++ ){
+    if( activeMap[args[i]] ){
+      activeArgs.push_back( args[i] );
+    }
+  }
+}
 
 bool QuantifiersRewriter::hasArg( std::vector< Node >& args, Node n ){
   if( std::find( args.begin(), args.end(), n )!=args.end() ){
@@ -728,7 +740,7 @@ Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >&
 
 Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){
   std::vector< Node > activeArgs;
-  computeArgVec( args, activeArgs, body );
+  computeArgVec2( args, activeArgs, body, ipl );
   if( activeArgs.empty() ){
     return body;
   }else{

diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index e2137b9f4d9800eb8120bdfd8e40a9445dad1e00..901a47f79705e9097039505d1daf04795a793d19 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -40,6 +40,7 @@ private:
   static Node mkForAll( std::vector< Node >& args, Node body, Node ipl );
   static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n );
   static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n );
+  static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl );
   static bool hasArg( std::vector< Node >& args, Node n );
   static void setNestedQuantifiers( Node n, Node q );
   static void setNestedQuantifiers2( Node n, Node q, std::vector< Node >& processed );

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 392fc269af105d2294d5b7eb7e5c1102bcfd0b8d..c35adef6afe7e4bc982c362ba47eb8ef204b80d1 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -329,6 +329,7 @@ void TermDb::reset( Theory::Effort effort ){
      if( !it->second.empty() ){
        for( unsigned i=0; i<it->second.size(); i++ ){
          Node n = it->second[i];
+         //Assert( d_quantEngine->getEqualityQuery()->hasTerm( n ) );
          computeModelBasisArgAttribute( n );
          if( !n.getAttribute(NoMatchAttribute()) ){
            computeArgReps( n );
@@ -794,24 +795,6 @@ Node TermDb::getFreeVariableForInstConstant( Node n ){
   return d_free_vars[tn];
 }
 
-const std::vector<Node> & TermDb::getParents(TNode n, TNode f, int arg){
-  std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node > >,NodeHashFunction  >,NodeHashFunction  >::const_iterator
-    rn = d_parents.find( n );
-  if( rn !=d_parents.end() ){
-    std::hash_map< Node, std::hash_map< int, std::vector< Node > > , NodeHashFunction  > ::const_iterator
-      rf = rn->second.find(f);
-    if( rf != rn->second.end() ){
-      std::hash_map< int, std::vector< Node > > ::const_iterator
-        ra = rf->second.find(arg);
-      if( ra != rf->second.end() ){
-        return ra->second;
-      }
-    }
-  }
-  static std::vector<Node> empty;
-  return empty;
-}
-
 void TermDb::computeVarContains( Node n ) {
   if( d_var_contains.find( n )==d_var_contains.end() ){
     d_var_contains[n].clear();

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index e40635d4e7d90d2947850dd9ff3bf162f62988a5..1d3757d6578ec9a56f0945b91352fadcf5edf281 100644 (file)
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -170,16 +170,6 @@ public:
   TNode evaluateTerm( TNode n );
   /** is entailed (incomplete check) */
   bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol );
-public:
-  /** parent structure (for efficient E-matching):
-      n -> op -> index -> L
-      map from node "n" to a list of nodes "L", where each node n' in L
-        has operator "op", and n'["index"] = n.
-      for example, d_parents[n][f][1] = { f( t1, n ), f( t2, n ), ... }
-  */
-  /* Todo replace int by size_t */
-  std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node >  >, NodeHashFunction  > , NodeHashFunction > d_parents;
-  const std::vector<Node> & getParents(TNode n, TNode f, int arg);
 
 //for model basis
 private:

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 7fb989a5a05c39d481dab517ce43a6faca742f1d..12a169e0999c038865ffcabdfca776edd90e505b 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -92,19 +92,10 @@ void TheoryEngine::finishInit() {
 
 void TheoryEngine::eqNotifyNewClass(TNode t){
   d_quantEngine->addTermToDatabase( t );
-  if( d_logicInfo.isQuantified() && options::quantConflictFind() ){
-    d_quantEngine->getConflictFind()->newEqClass( t );
-  }
 }
 
 void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
-  //TODO: add notification to efficient E-matching
-  if( d_logicInfo.isQuantified() ){
-    //d_quantEngine->getEfficientEMatcher()->merge( t1, t2 );
-    if( options::quantConflictFind() ){
-      d_quantEngine->getConflictFind()->merge( t1, t2 );
-    }
-  }
+
 }
 
 void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){

diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
index 066ba6103bb83e9451f46f8b5e7ee4fe86b61fc9..dbd1dcd16593613cbfed7871320a221d89b5750b 100644 (file)
--- a/src/util/sort_inference.cpp
+++ b/src/util/sort_inference.cpp
@@ -171,7 +171,9 @@ bool SortInference::simplify( std::vector< Node >& assertions ){
     for( unsigned i=0; i<assertions.size(); i++ ){
       Node prev = assertions[i];
       std::map< Node, Node > var_bound;
+      Trace("sort-inference-debug") << "Rewrite " << assertions[i] << std::endl;
       assertions[i] = simplify( assertions[i], var_bound );
+      Trace("sort-inference-debug") << "Done." << std::endl;
       if( prev!=assertions[i] ){
         assertions[i] = theory::Rewriter::rewrite( assertions[i] );
         rewritten = true;
@@ -512,6 +514,7 @@ Node SortInference::getNewSymbol( Node old, TypeNode tn ){
 }
 
 Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
+  Trace("sort-inference-debug2") << "Simplify " << n << std::endl;
   std::vector< Node > children;
   if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
     //recreate based on types of variables
@@ -519,6 +522,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
     for( size_t i=0; i<n[0].getNumChildren(); i++ ){
       TypeNode tn = getOrCreateTypeForId( d_var_types[n][ n[0][i] ], n[0][i].getType() );
       Node v = getNewSymbol( n[0][i], tn );
+      Trace("sort-inference-debug2") << "Map variable " << n[0][i] << " to " << v << std::endl;
       new_children.push_back( v );
       var_bound[ n[0][i] ] = v;
     }
@@ -529,13 +533,17 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
   if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
     children.push_back( n.getOperator() );
   }
+  bool childChanged = false;
   for( size_t i=0; i<n.getNumChildren(); i++ ){
     bool processChild = true;
     if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
       processChild = options::userPatternsQuant()==theory::quantifiers::USER_PAT_MODE_IGNORE ? i==1 : i>=1;
     }
     if( processChild ){
-      children.push_back( simplify( n[i], var_bound ) );
+      Node nc = simplify( n[i], var_bound );
+      Trace("sort-inference-debug2") << "Simplify " << i << " " << n[i] << " returned " << nc << std::endl;
+      children.push_back( nc );
+      childChanged = childChanged || nc!=n[i];
     }
   }
 
@@ -543,6 +551,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
   if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
     //erase from variable bound
     for( size_t i=0; i<n[0].getNumChildren(); i++ ){
+      Trace("sort-inference-debug2") << "Remove bound for " << n[0][i] << std::endl;
       var_bound.erase( n[0][i] );
     }
     return NodeManager::currentNM()->mkNode( n.getKind(), children );
@@ -596,7 +605,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
         if( n[i].isConst() ){
           children[i+1] = getNewSymbol( n[i], tna );
         }else{
-          Trace("sort-inference-warn") << "Sort inference created bad child: " << n[i] << " " << tn << " " << tna << std::endl;
+          Trace("sort-inference-warn") << "Sort inference created bad child: " << n << " " << n[i] << " " << tn << " " << tna << std::endl;
           Assert( false );
         }
       }
@@ -616,7 +625,11 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
       //just return n, we will fix at higher scope
       return n;
     }else{
-      return NodeManager::currentNM()->mkNode( n.getKind(), children );
+      if( childChanged ){
+        return NodeManager::currentNM()->mkNode( n.getKind(), children );
+      }else{
+        return n;
+      }
     }
   }