Removing and consolidating options for uf-ss and quantifiers. Bug fix for inst gen-style MBQI.

3 files changed, 11 insertions, 158 deletions

diff --git a/src/theory/uf/options b/src/theory/uf/options
index cfa6e6c04..26f87da79 100644
--- a/src/theory/uf/options
+++ b/src/theory/uf/options
@@ -15,20 +15,14 @@ option ufssRegions /--disable-uf-ss-regions bool :default true
  disable region-based method for discovering cliques and splits in uf strong solver
 option ufssEagerSplits --uf-ss-eager-split bool :default false
  add splits eagerly for uf strong solver
-option ufssColoringSat --uf-ss-coloring-sat bool :default false
- use coloring-based SAT heuristic for uf strong solver
 option ufssTotality --uf-ss-totality bool :default false
  always use totality axioms for enforcing cardinality constraints
 option ufssTotalityLimited --uf-ss-totality-limited=N int :default -1
  apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default)
-option ufssTotalityLazy --uf-ss-totality-lazy bool :default false
- apply totality axioms lazily
 option ufssTotalitySymBreak --uf-ss-totality-sym-break bool :default false
  apply symmetry breaking for totality axioms
 option ufssAbortCardinality --uf-ss-abort-card=N int :default -1
  tells the uf strong solver a cardinality to abort at (-1 == no limit, default)
-option ufssSmartSplits --uf-ss-smart-split bool :default false
- use smart splitting heuristic for uf strong solver
 option ufssExplainedCliques --uf-ss-explained-cliques bool :default false
  use explained clique lemmas for uf strong solver
 option ufssSimpleCliques --uf-ss-simple-cliques bool :default true
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index a4cefe269..54a3075a1 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -428,12 +428,10 @@ void StrongSolverTheoryUF::SortModel::initialize( OutputChannel* out ){
 void StrongSolverTheoryUF::SortModel::newEqClass( Node n ){
   if( !d_conflict ){
     if( d_regions_map.find( n )==d_regions_map.end() ){
-      if( !options::ufssTotalityLazy() ){
-        //must generate totality axioms for every cardinality we have allocated thus far
-        for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it != d_cardinality_literal.end(); ++it ){
-          if( applyTotality( it->first ) ){
-            addTotalityAxiom( n, it->first, &d_thss->getOutputChannel() );
-          }
+      //must generate totality axioms for every cardinality we have allocated thus far
+      for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it != d_cardinality_literal.end(); ++it ){
+        if( applyTotality( it->first ) ){
+          addTotalityAxiom( n, it->first, &d_thss->getOutputChannel() );
         }
       }
       if( options::ufssTotality() ){
@@ -449,9 +447,6 @@ void StrongSolverTheoryUF::SortModel::newEqClass( Node n ){
           d_regions_index = 0;
         }
         d_regions_map[n] = d_regions_index;
-        if( options::ufssSmartSplits() ){
-          setSplitScore( n, 0 );
-        }
         Debug("uf-ss") << "StrongSolverTheoryUF: New Eq Class " << n << std::endl;
         Debug("uf-ss-debug") << d_regions_index << " " << (int)d_regions.size() << std::endl;
         if( d_regions_index<d_regions.size() ){
@@ -634,18 +629,7 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
           }
         }
       }
-      if( applyTotality( d_cardinality ) ){
-        //add totality axioms for all nodes that have not yet been equated to cardinality terms
-        if( options::ufssTotalityLazy() ){    //this should always be true
-          if( level==Theory::EFFORT_FULL ){
-            for( NodeIntMap::iterator it = d_regions_map.begin(); it != d_regions_map.end(); ++it ){
-              if( !options::ufssTotality() || d_regions_map[ (*it).first ]!=-1 ){
-                addTotalityAxiom( (*it).first, d_cardinality, &d_thss->getOutputChannel() );
-              }
-            }
-          }
-        }
-      }else{
+      if( !applyTotality( d_cardinality ) ){
         //do splitting on demand
         bool addedLemma = false;
         if( level==Theory::EFFORT_FULL || options::ufssEagerSplits() ){
@@ -1073,7 +1057,7 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
     //out->propagateAsDecision( lem[0] );
     d_thss->d_statistics.d_max_model_size.maxAssign( d_aloc_cardinality );
 
-    if( applyTotality( d_aloc_cardinality ) && !options::ufssTotalityLazy() ){
+    if( applyTotality( d_aloc_cardinality ) ){
       //must send totality axioms for each existing term
       for( NodeIntMap::iterator it = d_regions_map.begin(); it != d_regions_map.end(); ++it ){
         addTotalityAxiom( (*it).first, d_aloc_cardinality, &d_thss->getOutputChannel() );
@@ -1085,27 +1069,11 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
 int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
   Node s;
   if( r->hasSplits() ){
-    if( !options::ufssSmartSplits() ){
-      //take the first split you find
-      for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){
-        if( (*it).second ){
-          s = (*it).first;
-          break;
-        }
-      }
-    }else{
-      int maxScore = -1;
-      std::vector< Node > splits;
-      for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){
-        if( (*it).second ){
-          int score1 = d_split_score[ (*it).first[0] ];
-          int score2 = d_split_score[ (*it).first[1] ];
-          int score = score1<score2 ? score1 : score2;
-          if( score>maxScore ){
-            maxScore = -1;
-            s = (*it).first;
-          }
-        }
+    //take the first split you find
+    for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){
+      if( (*it).second ){
+        s = (*it).first;
+        break;
       }
     }
     Assert( s!=Node::null() );
@@ -1474,11 +1442,6 @@ Node StrongSolverTheoryUF::SortModel::getCardinalityLiteral( int c ) {
 StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) :
 d_out( &out ), d_th( th ), d_conflict( c, false ), d_rep_model(), d_aloc_com_card( u, 0 ), d_com_card_assertions( c )
 {
-  if( options::ufssColoringSat() ){
-    d_term_amb = new TermDisambiguator( th->getQuantifiersEngine(), c );
-  }else{
-    d_term_amb = NULL;
-  }
   if( options::ufssDiseqPropagation() ){
     d_deq_prop = new DisequalityPropagator( th->getQuantifiersEngine(), this );
   }else{
@@ -1628,13 +1591,6 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){
     if( level==Theory::EFFORT_FULL ){
       debugPrint( "uf-ss-debug" );
     }
-    if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){
-      int lemmas =  d_term_amb->disambiguateTerms( d_out );
-      d_statistics.d_disamb_term_lemmas += lemmas;
-      if( lemmas>=0 ){
-        return;
-      }
-    }
     for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
       it->second->check( level, d_out );
       if( it->second->isConflict() ){
@@ -1646,11 +1602,6 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){
     if( !d_conflict && options::ufssSymBreak() ){
       d_sym_break->check( level );
     }
-    //disambiguate terms if necessary
-    //if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){
-    //  Assert( d_term_amb!=NULL );
-    //  d_statistics.d_disamb_term_lemmas += d_term_amb->disambiguateTerms( d_out );
-    //}
     Trace("uf-ss-solver") << "Done StrongSolverTheoryUF: check " << level << std::endl;
   }
 }
@@ -1918,76 +1869,6 @@ StrongSolverTheoryUF::Statistics::~Statistics(){
 }
 
 
-int TermDisambiguator::disambiguateTerms( OutputChannel* out ){
-  Debug("uf-ss-disamb") << "Disambiguate terms." << std::endl;
-  int lemmaAdded = 0;
-  //otherwise, determine ambiguous pairs of ground terms for relevant sorts
-  quantifiers::TermDb* db = d_qe->getTermDatabase();
-  for( std::map< Node, std::vector< Node > >::iterator it = db->d_op_map.begin(); it != db->d_op_map.end(); ++it ){
-    Debug("uf-ss-disamb") << "Check " << it->first << std::endl;
-    if( it->second.size()>1 ){
-      if(involvesRelevantType( it->second[0] ) ){
-        for( int i=0; i<(int)it->second.size(); i++ ){
-          for( int j=(i+1); j<(int)it->second.size(); j++ ){
-            Kind knd = it->second[i].getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
-            Node eq = NodeManager::currentNM()->mkNode( knd, it->second[i], it->second[j] );
-            eq = Rewriter::rewrite(eq);
-            //determine if they are ambiguous
-            if( d_term_amb.find( eq )==d_term_amb.end() ){
-              Debug("uf-ss-disamb") << "Check disambiguate " << it->second[i] << " " << it->second[j] << std::endl;
-              d_term_amb[ eq ] = true;
-              //if they are equal
-              if( d_qe->getEqualityQuery()->areEqual( it->second[i], it->second[j] ) ){
-                d_term_amb[ eq ] = false;
-              }else{
-                //if an argument is disequal, then they are not ambiguous
-                for( int k=0; k<(int)it->second[i].getNumChildren(); k++ ){
-                  if( d_qe->getEqualityQuery()->areDisequal( it->second[i][k], it->second[j][k] ) ){
-                    d_term_amb[ eq ] = false;
-                    break;
-                  }
-                }
-              }
-              if( d_term_amb[ eq ] ){
-                Debug("uf-ss-disamb") << "Disambiguate " << it->second[i] << " " << it->second[j] << std::endl;
-                //must add lemma
-                std::vector< Node > children;
-                children.push_back( eq );
-                for( int k=0; k<(int)it->second[i].getNumChildren(); k++ ){
-                  Kind knd2 = it->second[i][k].getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
-                  Node eqc = NodeManager::currentNM()->mkNode( knd2, it->second[i][k], it->second[j][k] );
-                  children.push_back( eqc.notNode() );
-                }
-                Assert( children.size()>1 );
-                Node lem = NodeManager::currentNM()->mkNode( OR, children );
-                Trace( "uf-ss-lemma" ) << "*** Disambiguate lemma : " << lem << std::endl;
-                //Notice() << "*** Disambiguate lemma : " << lem << std::endl;
-                out->lemma( lem );
-                d_term_amb[ eq ] = false;
-                lemmaAdded++;
-                return lemmaAdded;
-              }
-            }
-          }
-        }
-      }
-    }
-  }
-  Debug("uf-ss-disamb") << "Done disambiguate terms. " << lemmaAdded << std::endl;
-  return lemmaAdded;
-}
-
-bool TermDisambiguator::involvesRelevantType( Node n ){
-  if( n.getKind()==APPLY_UF ){
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( n[i].getType().isSort() ){
-        return true;
-      }
-    }
-  }
-  return false;
-}
-
 DisequalityPropagator::DisequalityPropagator(QuantifiersEngine* qe, StrongSolverTheoryUF* ufss) :
   d_qe(qe), d_ufss(ufss){
   d_true = NodeManager::currentNM()->mkConst( true );
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 4f41ebf2e..3ed1ea985 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -37,7 +37,6 @@ class SubsortSymmetryBreaker;
 namespace uf {
 
 class TheoryUF;
-class TermDisambiguator;
 class DisequalityPropagator;
 
 class StrongSolverTheoryUF{
@@ -320,8 +319,6 @@ private:
   /** check */
   void checkCombinedCardinality();
 private:
-  /** term disambiguator */
-  TermDisambiguator* d_term_amb;
   /** disequality propagator */
   DisequalityPropagator* d_deq_prop;
   /** symmetry breaking techniques */
@@ -331,8 +328,6 @@ public:
   ~StrongSolverTheoryUF() {}
   /** get theory */
   TheoryUF* getTheory() { return d_th; }
-  /** term disambiguator */
-  TermDisambiguator* getTermDisambiguator() { return d_term_amb; }
   /** disequality propagator */
   DisequalityPropagator* getDisequalityPropagator() { return d_deq_prop; }
   /** symmetry breaker */
@@ -401,23 +396,6 @@ public:
   Statistics d_statistics;
 };/* class StrongSolverTheoryUF */
 
-
-class TermDisambiguator
-{
-private:
-  /** quantifiers engine */
-  QuantifiersEngine* d_qe;
-  /** whether two terms are ambiguous (indexed by equalities) */
-  context::CDHashMap<Node, bool, NodeHashFunction> d_term_amb;
-  /** involves relevant type */
-  static bool involvesRelevantType( Node n );
-public:
-  TermDisambiguator( QuantifiersEngine* qe, context::Context* c ) : d_qe( qe ), d_term_amb( c ){}
-  ~TermDisambiguator(){}
-  /** check ambiguous terms */
-  int disambiguateTerms( OutputChannel* out );
-};
-
 class DisequalityPropagator
 {
 private: