added option --model-u-dt-enum for outputting uninterpreted sorts as datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts

6 files changed, 30 insertions, 21 deletions

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index dcd7a1b79..85a96f90a 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -103,12 +103,12 @@ void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
   }
 }
 
-void InstMatch::makeInternalRepresentative( QuantifiersEngine* qe ){
-  EqualityQueryQuantifiersEngine* eqqe = (EqualityQueryQuantifiersEngine*)qe->getEqualityQuery();
-  for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
-    d_map[ it->first ] = eqqe->getInternalRepresentative( it->second );
-  }
-}
+//void InstMatch::makeInternalRepresentative( QuantifiersEngine* qe ){
+//  EqualityQueryQuantifiersEngine* eqqe = (EqualityQueryQuantifiersEngine*)qe->getEqualityQuery();
+//  for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
+//    d_map[ it->first ] = eqqe->getInternalRepresentative( it->second );
+//  }
+//}
 
 void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
   for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 8b2d9726b..b9e61be20 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -58,7 +58,7 @@ public:
   /** make complete */
   void makeComplete( Node f, QuantifiersEngine* qe );
   /** make internal representative */
-  void makeInternalRepresentative( QuantifiersEngine* qe );
+  //void makeInternalRepresentative( QuantifiersEngine* qe );
   /** make representative */
   void makeRepresentative( QuantifiersEngine* qe );
   /** get value */
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 53977ee4f..75cc10615 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -84,16 +84,18 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
         //add cbqi lemma
         //get the counterexample literal
         Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f );
-        //require any decision on cel to be phase=true
-        d_quantEngine->getOutputChannel().requirePhase( ceLit, true );
-        Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
-        //add counterexample lemma
-        NodeBuilder<> nb(kind::OR);
-        nb << f << ceLit;
-        Node lem = nb;
-        Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl;
-        d_quantEngine->getOutputChannel().lemma( lem );
-        addedLemma = true;
+        if( !ceLit.isNull() ){
+          //require any decision on cel to be phase=true
+          d_quantEngine->getOutputChannel().requirePhase( ceLit, true );
+          Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
+          //add counterexample lemma
+          NodeBuilder<> nb(kind::OR);
+          nb << f << ceLit;
+          Node lem = nb;
+          Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl;
+          d_quantEngine->getOutputChannel().lemma( lem );
+          addedLemma = true;
+        }
       }
     }
     if( addedLemma ){
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index bf6ea11f0..39377d11c 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -73,9 +73,8 @@ void ModelEngine::check( Theory::Effort e ){
         if( addedLemmas==0 ){
           Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
           //let the strong solver verify that the model is minimal
-          uf::StrongSolverTheoryUf* uf_ss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
           //for debugging, this will if there are terms in the model that the strong solver was not notified of
-          uf_ss->debugModel( fm );
+          ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm );
           Trace("model-engine-debug") << "Check model..." << std::endl;
           d_incomplete_check = false;
           //print debug
@@ -164,7 +163,7 @@ int ModelEngine::checkModel( int checkOption ){
         Trace("model-engine-debug") << "   ";
         for( size_t i=0; i<it->second.size(); i++ ){
           //Trace("model-engine-debug") << it->second[i] << "  ";
-          Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getInternalRepresentative( it->second[i] );
+          Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getRepresentative( it->second[i] );
           Trace("model-engine-debug") << r << " ";
         }
         Trace("model-engine-debug") << std::endl;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index eace177b7..6b204eb60 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -71,7 +71,7 @@ option userPatternsQuant /--ignore-user-patterns bool :default true
 option flipDecision --flip-decision/ bool :default false
  turns on flip decision heuristic
 
-option internalReps --disable-quant-internal-reps/ bool :default true
+option internalReps /--disable-quant-internal-reps bool :default true
  disables instantiating with representatives chosen by quantifiers engine
 
 option finiteModelFind --finite-model-find bool :default false
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 78109ea37..65624686a 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -338,6 +338,14 @@ Node TermDb::getInstConstantBody( Node f ){
 Node TermDb::getCounterexampleLiteral( Node f ){
   if( d_ce_lit.find( f )==d_ce_lit.end() ){
     Node ceBody = getInstConstantBody( f );
+    //check if any variable are of bad types, and fail if so
+    for( size_t i=0; i<d_inst_constants[f].size(); i++ ){
+      if( d_inst_constants[f][i].getType().isBoolean() ){
+        d_ce_lit[ f ] = Node::null();
+        return Node::null();
+      }
+    }
+    //otherwise, ensure literal
     Node ceLit = d_quantEngine->getValuation().ensureLiteral( ceBody.notNode() );
     d_ce_lit[ f ] = ceLit;
     setInstantiationConstantAttr( ceLit, f );