From: ajreynol <reynolds@larapc05.epfl.ch>
Date: Mon, 28 Apr 2014 15:34:00 +0000 (+0200)
Subject: Optimizations for datatypes: check for clashes modulo equality.  Avoid building model... 
X-Git-Tag: cvc5-1.0.0~6958
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9b97c9144875e072da4098f102f8989be26e5cdf;p=cvc5.git

Optimizations for datatypes: check for clashes modulo equality.  Avoid building model at fullModel=false when possible.  Minor cleanup.
---

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index eef25ca80..9316c3fe8 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -49,6 +49,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
   d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes"),
   d_labels( c ),
   d_selector_apps( c ),
+  d_consEqc( c ),
   d_conflict( c, false ),
   d_collectTermsCache( c ),
   d_consTerms( c ),
@@ -59,6 +60,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
   d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
   d_equalityEngine.addFunctionKind(kind::APPLY_TESTER);
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
+
+  d_true = NodeManager::currentNM()->mkConst( true );
 }
 
 TheoryDatatypes::~TheoryDatatypes() {
@@ -99,6 +102,15 @@ TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( Node n, bool doMake
   }
 }
 
+TNode TheoryDatatypes::getEqcConstructor( TNode r ) {
+  EqcInfo * ei = getOrMakeEqcInfo( r, false );
+  if( ei && !ei->d_constructor.get().isNull() ){
+    return ei->d_constructor.get();
+  }else{
+    return r;
+  }
+}
+
 void TheoryDatatypes::check(Effort e) {
   Trace("datatypes-debug") << "Check effort " << e << std::endl;
   while(!done() && !d_conflict) {
@@ -189,7 +201,7 @@ void TheoryDatatypes::check(Effort e) {
               if( dt.getNumConstructors()==1 ){
                 Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), n );
                 d_pending.push_back( t );
-                d_pending_exp[ t ] = NodeManager::currentNM()->mkConst( true );
+                d_pending_exp[ t ] = d_true;
                 Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl;
                 d_infer.push_back( t );
               }else{
@@ -252,7 +264,7 @@ void TheoryDatatypes::flushPendingFacts(){
       if( mustCommunicateFact( fact, exp ) ){
         Trace("dt-lemma-debug") << "Assert fact " << fact << " " << exp << std::endl;
         Node lem = fact;
-        if( exp.isNull() || exp==NodeManager::currentNM()->mkConst( true ) ){
+        if( exp.isNull() || exp==d_true ){
           lem = fact;
         }else{
           Trace("dt-lemma-debug") << "Get explanation..." << std::endl;
@@ -345,7 +357,7 @@ Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) {
       Node tst = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), n[0] );
       tst = Rewriter::rewrite( tst );
       Node n_ret;
-      if( tst==NodeManager::currentNM()->mkConst( true ) ){
+      if( tst==d_true ){
         n_ret = sel;
       }else{
         if( d_exp_def_skolem.find( selector )==d_exp_def_skolem.end() ){
@@ -424,7 +436,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
       if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){
         nn = NodeManager::currentNM()->mkConst(false);
       }else{
-        nn = rew.size()==0 ? NodeManager::currentNM()->mkConst( true ) :
+        nn = rew.size()==0 ? d_true :
                   ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) );
       }
       return nn;
@@ -562,6 +574,14 @@ Node TheoryDatatypes::explain( TNode literal ){
   return mkAnd( assumptions );
 }
 
+Node TheoryDatatypes::explain( std::vector< Node >& lits ) {
+  std::vector< TNode > assumptions;
+  for( unsigned i=0; i<lits.size(); i++ ){
+    explain( lits[i], assumptions );
+  }
+  return mkAnd( assumptions );
+}
+
 /** Conflict when merging two constants */
 void TheoryDatatypes::conflict(TNode a, TNode b){
   if (a.getKind() == kind::CONST_BOOLEAN) {
@@ -578,6 +598,25 @@ void TheoryDatatypes::conflict(TNode a, TNode b){
 void TheoryDatatypes::eqNotifyNewClass(TNode t){
   if( t.getKind()==APPLY_CONSTRUCTOR ){
     getOrMakeEqcInfo( t, true );
+    //look at all equivalence classes with constructor terms
+/*
+    for( BoolMap::const_iterator it = d_consEqc.begin(); it != d_consEqc.end(); ++it ){
+      if( (*it).second ){
+        TNode r = (*it).first;
+        if( r.getType()==t.getType() ){
+          EqcInfo * ei = getOrMakeEqcInfo( r, false );
+          if( ei && !ei->d_constructor.get().isNull() && ei->d_constructor.get().getOperator()!=t.getOperator() ){
+            Node deq = ei->d_constructor.get().eqNode( t ).negate();
+            d_pending.push_back( deq );
+            d_pending_exp[ deq ] = d_true;
+            Trace("datatypes-infer") << "DtInfer : diff constructor : " << deq << std::endl;
+            d_infer.push_back( deq );
+          }
+        }
+      }
+    }
+*/
+    d_consEqc[t] = true;
   }
 }
 
@@ -615,18 +654,20 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
         //if both have constructor, then either clash or unification
         if( !cons1.isNull() && !cons2.isNull() ){
           Debug("datatypes-debug") << "Constructors : " << cons1 << " " << cons2 << std::endl;
-          if( cons1.getOperator()!=cons2.getOperator() ){
+          Node unifEq = cons1.eqNode( cons2 );
+          std::vector< Node > exp;
+          if( checkClashModEq( cons1, cons2, exp ) ){
+            exp.push_back( unifEq );
             //check for clash
-            d_conflictNode = explain( cons1.eqNode( cons2 ) );
+            d_conflictNode = explain( exp );
             Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl;
             d_out->conflict( d_conflictNode );
             d_conflict = true;
             return;
           }else{
             //do unification
-            Node unifEq = cons1.eqNode( cons2 );
             for( int i=0; i<(int)cons1.getNumChildren(); i++ ) {
-              if( cons1[i]!=cons2[i] ){
+              if( !areEqual( cons1[i], cons2[i] ) ){
                 Node eq = cons1[i].getType().isBoolean() ? cons1[i].iffNode( cons2[i] ) : cons1[i].eqNode( cons2[i] );
                 d_pending.push_back( eq );
                 d_pending_exp[ eq ] = unifEq;
@@ -634,19 +675,37 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
                 d_infer.push_back( eq );
                 d_infer_exp.push_back( unifEq );
               }
+            }    
+/*
+            std::vector< Node > rew;
+            if( DatatypesRewriter::checkClash( cons1, cons2, rew ) ){  
+              Assert(false);
+            }else{
+              for( unsigned i=0; i<rew.size(); i++ ){
+                d_pending.push_back( rew[i] );
+                d_pending_exp[ rew[i] ] = unifEq;
+                Trace("datatypes-infer") << "DtInfer : cons-inj : " << rew[i] << " by " << unifEq << std::endl;
+                d_infer.push_back( rew[i] );
+                d_infer_exp.push_back( unifEq );
+              }
             }
+*/
           }
         }
         if( !eqc1->d_inst && eqc2->d_inst ){
           eqc1->d_inst = true;
         }
-        if( cons1.isNull() && !cons2.isNull() ){
-          Debug("datatypes-debug") << "Must check if it is okay to set the constructor." << std::endl;
-          checkInst = true;
-          addConstructor( eqc2->d_constructor.get(), eqc1, t1 );
-          if( d_conflict ){
-            return;
+        if( !cons2.isNull() ){
+          if( cons1.isNull() ){
+            Debug("datatypes-debug") << "Must check if it is okay to set the constructor." << std::endl;
+            checkInst = true;
+            addConstructor( eqc2->d_constructor.get(), eqc1, t1 );
+            if( d_conflict ){
+              return;
+            }
+            d_consEqc[t1] = true;
           }
+          d_consEqc[t2] = false;
         }
       }else{
         Debug("datatypes-debug") << "No eqc info for " << t1 << ", must create" << std::endl;
@@ -939,7 +998,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
   //if( r!=rr ){
     //Node eq_exp = NodeManager::currentNM()->mkConst(true);
     //Node eq = r.getType().isBoolean() ? r.iffNode( rr ) : r.eqNode( rr );
-  if( s!=rr ){
+  if( s!=rr ){::
     Node eq_exp = c.eqNode( s[0] );
     Node eq = rr.getType().isBoolean() ? s.iffNode( rr ) : s.eqNode( rr );
 
@@ -988,14 +1047,29 @@ void TheoryDatatypes::computeCareGraph(){
             }else if( !areEqual( x, y ) ){
               Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
               //check if they are definately disequal
-              
-              if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){
-                TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES);
-                TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES);
-                Trace("dt-cg") << "Arg #" << k << " shared term is " << x_shared << " " << y_shared << std::endl;
-                //EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
-                //if( eqStatus!=EQUALITY_UNKNOWN ){
-                currentPairs.push_back(make_pair(x_shared, y_shared));
+              bool defDiseq = false;
+/*
+              TNode rx = getRepresentative( x );
+              EqcInfo* eix = getOrMakeEqcInfo( rx, false );
+              if( eix ){
+                TNode ry = getRepresentative( y );
+                EqcInfo* eiy = getOrMakeEqcInfo( ry, false );
+                if( eiy ){
+                  if( !eix->d_constructor.get().isNull() && !eiy->d_constructor.get().isNull() ){
+                    defDiseq = eix->d_constructor.get().getOperator()!=eiy->d_constructor.get().getOperator();
+                  }else{
+                  }
+                }
+              }
+*/
+              if( !defDiseq && d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){
+                EqualityStatus eqStatus = d_valuation.getEqualityStatus(x, y);
+                if( eqStatus!=EQUALITY_UNKNOWN ){
+                  TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES);
+                  TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES);
+                  Trace("dt-cg") << "Arg #" << k << " shared term is " << x_shared << " " << y_shared << std::endl;
+                  currentPairs.push_back(make_pair(x_shared, y_shared));
+                }
               }
             }
           } 
@@ -1234,7 +1308,7 @@ void TheoryDatatypes::processNewTerm( Node n ){
   if( rn!=n && !areEqual( rn, n ) ){
     Node eq = n.getType().isBoolean() ? rn.iffNode( n ) : rn.eqNode( n );
     d_pending.push_back( eq );
-    d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true );
+    d_pending_exp[ eq ] = d_true;
     Trace("datatypes-infer") << "DtInfer : rewrite : " << eq << std::endl;
     d_infer.push_back( eq );
   }
@@ -1266,7 +1340,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
     Node exp;
     Node tt;
     if( !eqc->d_constructor.get().isNull() ){
-      exp = NodeManager::currentNM()->mkConst( true );
+      exp = d_true;
       tt = eqc->d_constructor;
     }else{
       exp = getLabel( n );
@@ -1622,7 +1696,7 @@ bool TheoryDatatypes::areDisequal( TNode a, TNode b ){
   }
 }
 
-Node TheoryDatatypes::getRepresentative( TNode a ){
+TNode TheoryDatatypes::getRepresentative( TNode a ){
   if( hasTerm( a ) ){
     return d_equalityEngine.getRepresentative( a );
   }else{
@@ -1692,10 +1766,51 @@ void TheoryDatatypes::printModelDebug( const char* c ){
 
 Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) {
   if( assumptions.empty() ){
-    return NodeManager::currentNM()->mkConst( true );
+    return d_true;
   }else if( assumptions.size()==1 ){
     return assumptions[0];
   }else{
     return NodeManager::currentNM()->mkNode( AND, assumptions );
   }
 }
+
+bool TheoryDatatypes::checkClashModEq( Node n1, Node n2, std::vector< Node >& exp ) {
+  if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) ||
+      (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) ||
+      (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) {
+    if( n1.getOperator() != n2.getOperator() ) {
+      return true;
+    } else {
+      Assert( n1.getNumChildren() == n2.getNumChildren() );
+      for( int i=0; i<(int)n1.getNumChildren(); i++ ) {
+        TNode nc1 = n1[i];
+        TNode nc2 = n2[i];
+        if( DatatypesRewriter::isTermDatatype( n1[i] ) ){
+          nc1 = getEqcConstructor( n1[i] );
+          nc2 = getEqcConstructor( n2[i] );
+        }
+        if( checkClashModEq( nc1, nc2, exp ) ) {
+          if( nc1!=n1[i] ){
+            exp.push_back( nc1.eqNode( n1[i] ) );
+          }
+          if( nc2!=n2[i] ){
+            exp.push_back( nc2.eqNode( n2[i] ) );
+          }
+          return true;
+        }
+      }
+    }
+  }else if( n1!=n2 ){
+    if( n1.isConst() && n2.isConst() ){
+      return true;        
+    }else{
+      Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 );
+      if( d_equalityEngine.areDisequal( n1, n2, true ) ){
+        exp.push_back( eq.negate() );
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index eb86c3f76..1c21c63b4 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -50,7 +50,7 @@ private:
   /** inferences */
   NodeList d_infer;
   NodeList d_infer_exp;
-
+  Node d_true;
   /** mkAnd */
   Node mkAnd( std::vector< TNode >& assumptions );
 private:
@@ -156,6 +156,8 @@ private:
   NodeListMap d_labels;
   /** selector apps for eqch equivalence class */
   NodeListMap d_selector_apps;
+  /** constructor terms */
+  BoolMap d_consEqc;
   /** Are we in conflict */
   context::CDO<bool> d_conflict;
   /** The conflict node */
@@ -183,6 +185,8 @@ private:
   EqcInfo* getOrMakeEqcInfo( Node n, bool doMake = false );
   /** has eqc info */
   bool hasEqcInfo( Node n ) { return d_labels.find( n )!=d_labels.end(); }
+  /** get eqc constructor */
+  TNode getEqcConstructor( TNode r );
 protected:
   /** compute care graph */
   void computeCareGraph();
@@ -204,6 +208,7 @@ public:
   void explainPredicate( TNode p, bool polarity, std::vector<TNode>& assumptions );
   void explain( TNode literal, std::vector<TNode>& assumptions );
   Node explain( TNode literal );
+  Node explain( std::vector< Node >& lits );
   /** Conflict when merging two constants */
   void conflict(TNode a, TNode b);
   /** called when a new equivalance class is created */
@@ -263,12 +268,14 @@ private:
   bool mustSpecifyAssignment();
   /** must communicate fact */
   bool mustCommunicateFact( Node n, Node exp );
+  /** check clash mod eq */
+  bool checkClashModEq( Node n1, Node n2, std::vector< Node >& exp );
 private:
   //equality queries
   bool hasTerm( TNode a );
   bool areEqual( TNode a, TNode b );
   bool areDisequal( TNode a, TNode b );
-  Node getRepresentative( TNode a );
+  TNode getRepresentative( TNode a );
 public:
   /** get equality engine */
   eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; }
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index 972bdb2ec..4130bffee 100644
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -121,6 +121,9 @@ public:
   void getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u );
   void getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u );
   bool isGroundRange(Node f, Node v);
+
+  /** Identify this module */
+  std::string identify() const { return "BoundedIntegers"; }
 };
 
 }
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 5f7e26297..394d53d42 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -150,6 +150,8 @@ public:
     ~Statistics();
   };
   Statistics d_statistics;
+  /** Identify this module */
+  std::string identify() const { return "InstEngine"; }
 };/* class InstantiationEngine */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 8b62fc39b..d7b074acc 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -55,68 +55,74 @@ QuantifiersModule( qe ){
 
 void ModelEngine::check( Theory::Effort e ){
   if( e==Theory::EFFORT_LAST_CALL && !d_quantEngine->hasAddedLemma() ){
-    FirstOrderModel* fm = d_quantEngine->getModel();
-    //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers
     int addedLemmas = 0;
-    //quantifiers are initialized, we begin an instantiation round
-    double clSet = 0;
-    if( Trace.isOn("model-engine") ){
-      clSet = double(clock())/double(CLOCKS_PER_SEC);
-    }
-    ++(d_statistics.d_inst_rounds);
-    bool buildAtFullModel = d_builder->optBuildAtFullModel();
-    //two effort levels: first try exhaustive instantiation without axioms, then with.
-    int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0;
-    for( int effort=startEffort; effort<2; effort++ ){
-      // for effort = 0, we only instantiate non-axioms
-      // for effort = 1, we instantiate everything
-      if( addedLemmas==0 ){
-        Trace("model-engine") << "---Model Engine Round---" << std::endl;
-        //initialize the model
-        Trace("model-engine-debug") << "Build model..." << std::endl;
-        d_builder->d_considerAxioms = effort>=1;
-        d_builder->d_addedLemmas = 0;
-        d_builder->buildModel( fm, buildAtFullModel );
-        addedLemmas += (int)d_builder->d_addedLemmas;
-        //if builder has lemmas, add and return
+    bool needsBuild = true;
+    FirstOrderModel* fm = d_quantEngine->getModel();
+    if( fm->getNumAssertedQuantifiers()>0 ){
+      //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers
+      //quantifiers are initialized, we begin an instantiation round
+      double clSet = 0;
+      if( Trace.isOn("model-engine") ){
+        clSet = double(clock())/double(CLOCKS_PER_SEC);
+      }
+      ++(d_statistics.d_inst_rounds);
+      bool buildAtFullModel = d_builder->optBuildAtFullModel();
+      needsBuild = !buildAtFullModel;
+      //two effort levels: first try exhaustive instantiation without axioms, then with.
+      int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0;
+      for( int effort=startEffort; effort<2; effort++ ){
+        // for effort = 0, we only instantiate non-axioms
+        // for effort = 1, we instantiate everything
         if( addedLemmas==0 ){
-          Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
-          //let the strong solver verify that the model is minimal
-          //for debugging, this will if there are terms in the model that the strong solver was not notified of
-          if( ((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
-            Debug("fmf-model-complete") << std::endl;
-            debugPrint("fmf-model-complete");
-            //successfully built an acceptable model, now check it
-            addedLemmas += checkModel();
-          }else{
-            addedLemmas++;
+          Trace("model-engine") << "---Model Engine Round---" << std::endl;
+          //initialize the model
+          Trace("model-engine-debug") << "Build model..." << std::endl;
+          d_builder->d_considerAxioms = effort>=1;
+          d_builder->d_addedLemmas = 0;
+          d_builder->buildModel( fm, buildAtFullModel );
+          addedLemmas += (int)d_builder->d_addedLemmas;
+          //if builder has lemmas, add and return
+          if( addedLemmas==0 ){
+            Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
+            //let the strong solver verify that the model is minimal
+            //for debugging, this will if there are terms in the model that the strong solver was not notified of
+            if( ((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
+              Debug("fmf-model-complete") << std::endl;
+              debugPrint("fmf-model-complete");
+              //successfully built an acceptable model, now check it
+              addedLemmas += checkModel();
+            }else{
+              addedLemmas++;
+            }
           }
         }
-      }
-      if( addedLemmas==0 ){
-        //if we have not added lemmas yet and axiomInstMode=trust, then we are done
-        if( options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){
-          //we must return unknown if an axiom is asserted
-          if( effort==0 ){
-            d_incomplete_check = true;
+        if( addedLemmas==0 ){
+          //if we have not added lemmas yet and axiomInstMode=trust, then we are done
+          if( options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){
+            //we must return unknown if an axiom is asserted
+            if( effort==0 ){
+              d_incomplete_check = true;
+            }
+            break;
           }
-          break;
         }
       }
-    }
-    if( Trace.isOn("model-engine") ){
-      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-      Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
+      if( Trace.isOn("model-engine") ){
+        double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+        Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
+      }
+    }else{
+      Trace("model-engine-debug") << "No quantified formulas asserted." << std::endl;
     }
     if( addedLemmas==0 ){
       Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl;
       //CVC4 will answer SAT or unknown
       Trace("fmf-consistent") << std::endl;
       debugPrint("fmf-consistent");
-      if( options::produceModels() && !buildAtFullModel ){
+      if( options::produceModels() && needsBuild ){
         // finish building the model
         d_builder->buildModel( fm, true );
       }
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index cf770a7b9..3b34f7504 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -68,6 +68,8 @@ public:
     ~Statistics();
   };
   Statistics d_statistics;
+  /** Identify this module */
+  std::string identify() const { return "ModelEngine"; }
 };/* class ModelEngine */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 62bd347c7..8a0d956ac 100755
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -116,7 +116,7 @@ public:
 class QuantInfo {
 private:
   void registerNode( Node n, bool hasPol, bool pol, bool beneathQuant = false );
-  void flatten( Node n, bool beneathQuant );
+  void flatten( Node n, bool beneathQuant );
 private: //for completing match
   std::vector< int > d_unassigned;
   std::vector< TypeNode > d_unassigned_tn;
@@ -156,8 +156,8 @@ public:
   bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false );
   void revertMatch( std::vector< int >& assigned );
   void debugPrintMatch( const char * c );
-  bool isConstrainedVar( int v );
-public:
+  bool isConstrainedVar( int v );
+public:
   void getMatch( std::vector< Node >& terms );
 };
 
@@ -274,6 +274,8 @@ public:
     ~Statistics();
   };
   Statistics d_statistics;
+  /** Identify this module */
+  std::string identify() const { return "QcfEngine"; }
 };
 
 }
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index f85803617..a16a6d598 100644
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -56,7 +56,9 @@ public:
 
   void check( Theory::Effort e );
   void registerQuantifier( Node f );
-  void assertNode( Node n );
+  void assertNode( Node n );  
+  /** Identify this module */
+  std::string identify() const { return "RewriteEngine"; }
 };
 
 }
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 63697f5e7..1837a34f4 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -166,6 +166,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
       Trace("quant-engine") << "Master equality engine not consistent, return." << std::endl;
       return;
     }
+    Trace("quant-engine-debug") << "Resetting modules..." << std::endl;
     //reset relevant information
     d_hasAddedLemma = false;
     d_term_db->reset( e );
@@ -176,6 +177,8 @@ void QuantifiersEngine::check( Theory::Effort e ){
     for( int i=0; i<(int)d_modules.size(); i++ ){
       d_modules[i]->reset_round( e );
     }
+    Trace("quant-engine-debug") << "Done resetting modules." << std::endl;
+
     if( e==Theory::EFFORT_LAST_CALL ){
       //if effort is last call, try to minimize model first
       if( options::finiteModelFind() ){
@@ -188,14 +191,19 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }else if( e==Theory::EFFORT_FULL ){
       ++(d_statistics.d_instantiation_rounds);
     }
+    Trace("quant-engine-debug") << "Check with modules..." << std::endl;
     for( int i=0; i<(int)d_modules.size(); i++ ){
+      Trace("quant-engine-debug") << "Check " << d_modules[i]->identify().c_str() << "..." << std::endl;
       d_modules[i]->check( e );
     }
+    Trace("quant-engine-debug") << "Done check with modules." << std::endl;
     //build the model if not done so already
     //  this happens if no quantifiers are currently asserted and no model-building module is enabled
     if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
       if( options::produceModels() && !d_model->isModelSet() ){
+        Trace("quant-engine-debug") << "Build the model..." << std::endl;
         d_te->getModelBuilder()->buildModel( d_model, true );
+        Trace("quant-engine-debug") << "Done building the model." << std::endl;
       }
       if( Trace.isOn("inst-per-quant") ){
         for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 858093543..e7843ab95 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -59,6 +59,8 @@ public:
   virtual void propagate( Theory::Effort level ){}
   virtual Node getNextDecisionRequest() { return TNode::null(); }
   virtual Node explain(TNode n) { return TNode::null(); }
+  /** Identify this module (for debugging, dynamic configuration, etc..) */
+  virtual std::string identify() const = 0;
 };/* class QuantifiersModule */
 
 namespace quantifiers {