merging fmf-devel branch, includes refactored datatype theory, updates to model.h/cpp to prepare for release, and major refactoring of quantifiers/finite model finding. Note that new datatype theory does not insist upon any interpretation for selectors applied to incorrect constructors and consequently some answers may differ with previous version

1 files changed, 21 insertions, 50 deletions

diff --git a/src/theory/inst_match.cpp b/src/theory/inst_match.cpp
index 4f1bfe67e..c90483fa3 100644
--- a/src/theory/inst_match.cpp
+++ b/src/theory/inst_match.cpp
@@ -17,8 +17,8 @@
 #include "theory/inst_match.h"
 #include "theory/theory_engine.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/candidate_generator.h"
 #include "theory/uf/theory_uf_instantiator.h"
-#include "theory/uf/theory_uf_candidate_generator.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/quantifiers/model_engine.h"
 #include "theory/quantifiers/term_database.h"
@@ -33,38 +33,6 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::inst;
 
 
-bool CandidateGenerator::isLegalCandidate( Node n ){
-  return ( !n.getAttribute(NoMatchAttribute()) && ( !Options::current()->cbqi || !n.hasAttribute(InstConstantAttribute()) ) ) ||
-         ( Options::current()->finiteModelFind && n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1 );
-}
-
-void CandidateGeneratorQueue::addCandidate( Node n ) {
-  if( isLegalCandidate( n ) ){
-    d_candidates.push_back( n );
-  }
-}
-
-void CandidateGeneratorQueue::reset( Node eqc ){
-  if( d_candidate_index>0 ){
-    d_candidates.erase( d_candidates.begin(), d_candidates.begin() + d_candidate_index );
-    d_candidate_index = 0;
-  }
-  if( !eqc.isNull() ){
-    d_candidates.push_back( eqc );
-  }
-}
-Node CandidateGeneratorQueue::getNextCandidate(){
-  if( d_candidate_index<(int)d_candidates.size() ){
-    Node n = d_candidates[d_candidate_index];
-    d_candidate_index++;
-    return n;
-  }else{
-    d_candidate_index = 0;
-    d_candidates.clear();
-    return Node::null();
-  }
-}
-
 InstMatch::InstMatch() {
 }
 
@@ -130,18 +98,21 @@ void InstMatch::debugPrint( const char* c ){
 
 void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
   for( int i=0; i<(int)qe->getTermDatabase()->d_inst_constants[f].size(); i++ ){
-    if( d_map.find( qe->getTermDatabase()->d_inst_constants[f][i] )==d_map.end() ){
-      d_map[ qe->getTermDatabase()->d_inst_constants[f][i] ] = qe->getTermDatabase()->getFreeVariableForInstConstant( qe->getTermDatabase()->d_inst_constants[f][i] );
+    Node ic = qe->getTermDatabase()->d_inst_constants[f][i];
+    if( d_map.find( ic )==d_map.end() ){
+      d_map[ ic ] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
     }
   }
 }
 
 void InstMatch::makeInternal( QuantifiersEngine* qe ){
-  for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
-    if( Options::current()->cbqi && it->second.hasAttribute(InstConstantAttribute()) ){
-      d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second );
-      if( Options::current()->cbqi && it->second.hasAttribute(InstConstantAttribute()) ){
-        d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first );
+  if( Options::current()->cbqi ){
+    for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
+      if( it->second.hasAttribute(InstConstantAttribute()) ){
+        d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second );
+        if( it->second.hasAttribute(InstConstantAttribute()) ){
+          d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first );
+        }
       }
     }
   }
@@ -203,9 +174,9 @@ bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m
     }
     if( modEq ){
       //check modulo equality if any other instantiation match exists
-      if( ((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine()->hasTerm( n ) ){
-        eq::EqClassIterator eqc( ((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine()->getRepresentative( n ),
-                                ((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine() );
+      if( qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
+        eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
+                                 qe->getEqualityQuery()->getEngine() );
         while( !eqc.isFinished() ){
           Node en = (*eqc);
           if( en!=n ){
@@ -310,10 +281,10 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){
     //we will be producing candidates via literal matching heuristics
     if( d_pattern.getKind()!=NOT ){
       //candidates will be all equalities
-      d_cg = new uf::inst::CandidateGeneratorTheoryUfLitEq( ith, d_match_pattern );
+      d_cg = new inst::CandidateGeneratorQELitEq( qe, d_match_pattern );
     }else{
       //candidates will be all disequalities
-      d_cg = new uf::inst::CandidateGeneratorTheoryUfLitDeq( ith, d_match_pattern );
+      d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern );
     }
   }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || d_pattern.getKind()==NOT ){
     Assert( d_matchPolicy==MATCH_GEN_DEFAULT );
@@ -322,7 +293,7 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){
     }else{
       Assert( Trigger::isAtomicTrigger( d_match_pattern ) );
       //we are matching only in a particular equivalence class
-      d_cg = new uf::inst::CandidateGeneratorTheoryUf( ith, d_match_pattern.getOperator() );
+      d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
       //store the equivalence class that we will call d_cg->reset( ... ) on
       d_eq_class = d_pattern[1];
     }
@@ -331,7 +302,7 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){
       //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl;
     //}
     //we will be scanning lists trying to find d_match_pattern.getOperator()
-    d_cg = new uf::inst::CandidateGeneratorTheoryUf( ith, d_match_pattern.getOperator() );
+    d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
   }else{
     d_cg = new CandidateGeneratorQueue;
     if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){
@@ -785,9 +756,9 @@ void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, I
       }
       if( modEq ){
         //check modulo equality for other possible instantiations
-        if( ((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine()->hasTerm( n ) ){
-          eq::EqClassIterator eqc( qe->getEqualityQuery()->getRepresentative( n ),
-                                  ((uf::TheoryUF*)qe->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine() );
+        if( qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
+          eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
+                                   qe->getEqualityQuery()->getEngine() );
           while( !eqc.isFinished() ){
             Node en = (*eqc);
             if( en!=n ){