Fix smt2 printing of fun-def. Simplification of mbqi interface.

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index a98a106a1076e3145ae38e723ae18cb18c8dd8f9..7648a158702d2d1eb61e6125f4867506ddb5802a 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -32,6 +32,7 @@
 
 #include "theory/theory_model.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
+#include "theory/quantifiers/term_database.h"
 
 using namespace std;
 
@@ -589,9 +590,14 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::INST_PATTERN:
     break;
   case kind::INST_PATTERN_LIST:
-    // TODO user patterns
     for(unsigned i=0; i<n.getNumChildren(); i++) {
-      out << ":pattern " << n[i];
+      if( n[i].getKind()==kind::INST_ATTRIBUTE ){
+        if( n[i][0].getAttribute(theory::FunDefAttribute()) ){
+          out << ":fun-def";
+        }
+      }else{
+        out << ":pattern " << n[i];
+      }
     }
     return;
     break;

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index ea97513b879cc2077b0a4d6e1f08ec4fb66c3d7c..e1fc9e793e0e567ab660a56bad01605afe790661 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -141,9 +141,6 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) {
 bool CegInstantiation::needsModel( Theory::Effort e ) {
   return true;
 }
-bool CegInstantiation::needsFullModel( Theory::Effort e ) {
-  return true;
-}
 
 void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
   if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){

diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 786db12a9ba319d64c3598343743c2e0514b5cfd..f5077ad04f0da9d3a7ce287824b5fd14fc81e85a 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -119,7 +119,6 @@ public:
 public:
   bool needsCheck( Theory::Effort e );
   bool needsModel( Theory::Effort e );
-  bool needsFullModel( Theory::Effort e );
   /* Call during quantifier engine's check */
   void check( Theory::Effort e, unsigned quant_e );
   /* Called for new quantifiers */

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index c0a734c357a54db76b4b4983b2d79e28655efcb8..c3a723fce4c45c0a032a8b418d652fc30b9b3a2f 100644 (file)
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -325,15 +325,9 @@ QModelBuilder( c, qe ){
   d_false = NodeManager::currentNM()->mkConst(false);
 }
 
-bool FullModelChecker::optBuildAtFullModel() {
-  //need to build after full model has taken effect if we are constructing interval models
-  //  this is because we need to have a constant in all integer equivalence classes
-  return options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL;
-}
-
 void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
   FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
-  if( fullModel==optBuildAtFullModel() ){
+  if( !fullModel ){
     Trace("fmc") << "---Full Model Check reset() " << std::endl;
     fm->initialize();
     d_quant_models.clear();
@@ -514,8 +508,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
       }
       */
     }
-  }
-  if( fullModel ){
+  }else{
     //make function values
     for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){
       m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" );

diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 9a7b05090df93c005110b4cd577a7e65cd3e9110..29913d98d1930a569aa94ccafbe427486da63223 100644 (file)
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -135,9 +135,6 @@ public:
   FullModelChecker( context::Context* c, QuantifiersEngine* qe );
   ~FullModelChecker() throw() {}
 
-  bool optBuildAtFullModel();
-
-
   void debugPrintCond(const char * tr, Node n, bool dispStar = false);
   void debugPrint(const char * tr, Node n, bool dispStar = false);
 

diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index 22dac222579dcd1c0ccefd19c64b12d3df8829f7..a46aca3c8849c53a87861599deb0408194cb7b56 100644 (file)
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -46,6 +46,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
       }
       
       Node bd = TermDb::getFunDefBody( assertions[i] );
+      Trace("fmf-fun-def-debug") << "Process function " << n << ", body = " << bd << std::endl;
       Assert( !bd.isNull() );
       bd = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bd );
 

diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index a3d239d185fa1e0da1d1c30c5e907783c1f67aa5..d9ed3f0920fefc74ecf1925d1b5faec7447c101a 100644 (file)
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -42,8 +42,6 @@ public:
   virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; }
   //whether to construct model
   virtual bool optUseModel();
-  //whether to construct model at fullModel = true
-  virtual bool optBuildAtFullModel() { return false; }
   /** number of lemmas generated while building model */
   //is the exhaustive instantiation incomplete?
   bool d_incomplete_check;

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 3fa3b2a1b3bd7c17b50dd7b6a3da52739393f28d..f6645c493f2872f6b64f22b5df08ff760a6341e2 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -267,7 +267,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
   }
   bool needsCheck = !d_lemmas_waiting.empty();
   bool needsModel = false;
-  bool needsFullModel = false;
   std::vector< QuantifiersModule* > qm;
   if( d_model->checkNeeded() ){
     needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL;  //always need to check at or above last call
@@ -277,9 +276,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
         needsCheck = true;
         if( d_modules[i]->needsModel( e ) ){
           needsModel = true;
-          if( d_modules[i]->needsFullModel( e ) ){
-            needsFullModel = true;
-          }
         }
       }
     }
@@ -347,9 +343,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
       //build the model if any module requested it
       if( quant_e==QEFFORT_MODEL && needsModel ){
         Assert( d_builder!=NULL );
-        Trace("quant-engine-debug") << "Build model, fullModel = " << ( needsFullModel || d_builder->optBuildAtFullModel() ) << "..." << std::endl;
+        Trace("quant-engine-debug") << "Build model..." << std::endl;
         d_builder->d_addedLemmas = 0;
-        d_builder->buildModel( d_model, needsFullModel || d_builder->optBuildAtFullModel() );
+        d_builder->buildModel( d_model, false );
         //we are done if model building was unsuccessful
         if( d_builder->d_addedLemmas>0 ){
           success = false;
@@ -368,7 +364,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
       if( d_hasAddedLemma ){
         break;
       //otherwise, complete the model generation if necessary
-      }else if( quant_e==QEFFORT_MODEL && needsModel && options::produceModels() && !needsFullModel && !d_builder->optBuildAtFullModel() ){
+      }else if( quant_e==QEFFORT_MODEL && needsModel && options::produceModels() ){
         Trace("quant-engine-debug") << "Build completed model..." << std::endl;
         d_builder->buildModel( d_model, true );
       }