merge from fmf-devel branch. more updates to models: now with collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models

7 files changed, 154 insertions, 33 deletions

diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 9bfc9680a..333c887ee 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -12,7 +12,9 @@ libsmt_la_SOURCES = \
 	smt_engine_scope.h \
 	modal_exception.h \
 	simplification_mode.h \
-	simplification_mode.cpp
+	simplification_mode.cpp \
+	model_format_mode.h \
+	model_format_mode.cpp
 
 nodist_libsmt_la_SOURCES = \
 	smt_options.cpp
diff --git a/src/smt/model_format_mode.cpp b/src/smt/model_format_mode.cpp
new file mode 100644
index 000000000..ffaa3df95
--- /dev/null
+++ b/src/smt/model_format_mode.cpp
@@ -0,0 +1,39 @@
+/*********************                                                        */
+/*! \file model_format_mode.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "smt/model_format_mode.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) {
+  switch(mode) {
+  case MODEL_FORMAT_MODE_DEFAULT:
+    out << "MODEL_FORMAT_MODE_DEFAULT";
+    break;
+  case MODEL_FORMAT_MODE_TABLE:
+    out << "MODEL_FORMAT_MODE_TABLE";
+    break;
+  default:
+    out << "ModelFormatMode:UNKNOWN![" << unsigned(mode) << "]";
+  }
+
+  return out;
+}
+
+}/* CVC4 namespace */
diff --git a/src/smt/model_format_mode.h b/src/smt/model_format_mode.h
new file mode 100644
index 000000000..3c0a3569e
--- /dev/null
+++ b/src/smt/model_format_mode.h
@@ -0,0 +1,41 @@
+/*********************                                                        */
+/*! \file model_format_mode.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SMT__MODEL_FORMAT_MODE_H
+#define __CVC4__SMT__MODEL_FORMAT_MODE_H
+
+#include <iostream>
+
+namespace CVC4 {
+
+/** Enumeration of model_format modes (how to print models from get-model command). */
+typedef enum {
+  /** default mode (print expressions in the output language format) */
+  MODEL_FORMAT_MODE_DEFAULT,
+  /** print functional values in a table format */
+  MODEL_FORMAT_MODE_TABLE,
+} ModelFormatMode;
+
+std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__MODEL_FORMAT_H */
diff --git a/src/smt/options b/src/smt/options
index fea609bb5..bb0cf1a00 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -34,6 +34,8 @@ common-option produceModels produce-models -m --produce-models bool :predicate C
  support the get-value and get-model commands
 common-option produceAssignments produce-assignments --produce-assignments bool
  support the get-assignment command
+option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::smt::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "smt/model_format_mode.h" :handler-include "smt/options_handlers.h"
+ print format mode for models, see --model-format=help
 
 # This could go in src/main/options, but by SMT-LIBv2 spec, "interactive"
 # is a mode in which the assertion list must be kept.  So it belongs here.
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 925f86d48..fb6cd84d8 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -150,6 +150,16 @@ none\n\
 + do not perform nonclausal simplification\n\
 ";
 
+static const std::string modelFormatHelp = "\
+Model format modes currently supported by the --model-format option:\n\
+\n\
+default \n\
++ Print model as expressions in the output language format.\n\
+\n\
+table\n\
++ Print functional expressions over finite domains in a table format.\n\
+";
+
 inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
 #ifdef CVC4_DUMPING
   char* optargPtr = strdup(optarg.c_str());
@@ -231,6 +241,20 @@ inline SimplificationMode stringToSimplificationMode(std::string option, std::st
   }
 }
 
+inline ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "default") {
+    return MODEL_FORMAT_MODE_DEFAULT;
+  } else if(optarg == "table") {
+    return MODEL_FORMAT_MODE_TABLE;
+  } else if(optarg == "help") {
+    puts(modelFormatHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --model-format: `") +
+                          optarg + "'.  Try --model-format help.");
+  }
+}
+
 // This macro is used for setting :regular-output-channel and :diagnostic-output-channel
 // to redirect a stream.  It maintains all attributes set on the stream.
 #define __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(__channel_get, __channel_set) \
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d450319b1..832779944 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -60,6 +60,8 @@
 #include "theory/booleans/circuit_propagator.h"
 #include "util/ite_removal.h"
 #include "theory/model.h"
+#include "printer/printer.h"
+#include "prop/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -488,7 +490,9 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
     bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
     bool quantifiers = d_logic.isQuantified();
     Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat && !quantifiers) << std::endl;
-    options::simplificationMode.set(qf_sat || quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
+    //simplifaction=none works better for SMT LIB benchmarks with quantifiers, not others
+    //options::simplificationMode.set(qf_sat || quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
+    options::simplificationMode.set(qf_sat ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
   }
 
   // If in arrays, set the UF handler to arrays
@@ -617,6 +621,21 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
     options::decisionMode.set(decMode);
     options::decisionStopOnly.set(stoponly);
   }
+
+  //for finite model finding
+  if( ! options::instWhenMode.wasSetByUser()){
+    if( options::fmfInstEngine() ){
+      Trace("smt") << "setting inst when mode to LAST_CALL" << std::endl;
+      options::instWhenMode.set( INST_WHEN_LAST_CALL );
+    }
+  }
+
+  //until bug 371 is fixed
+  if( ! options::minisatUseElim.wasSetByUser()){
+    if( d_logic.isQuantified() ){
+      options::minisatUseElim.set( false );
+    }
+  }
 }
 
 void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
@@ -1727,11 +1746,10 @@ Expr SmtEngine::getValue(const Expr& e)
     throw ModalException(msg);
   }
 
-  // Apply what was learned from preprocessing
-  Node n = d_private->applySubstitutions(e.getNode());
+  // do not need to apply preprocessing substitutions (should be recorded in model already)
 
   // Normalize for the theories
-  n = Rewriter::rewrite(n);
+  Node n = Rewriter::rewrite( e.getNode() );
 
   Trace("smt") << "--- getting value of " << n << endl;
   theory::TheoryModel* m = d_theoryEngine->getModel();
@@ -1835,34 +1853,19 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException)
 }
 
 
-void SmtEngine::addToModelType( Type& t ){
-  Trace("smt") << "SMT addToModelType(" << t << ")" << endl;
-  SmtScope smts(this);
-  finalOptionsAreSet();
-  if( options::produceModels() ) {
-    d_theoryEngine->getModel()->addDefineType( TypeNode::fromType( t ) );
-  }
-}
-
-void SmtEngine::addToModelFunction( Expr& e ){
-  Trace("smt") << "SMT addToModelFunction(" << e << ")" << endl;
+void SmtEngine::addToModelCommand( Command* c, int c_type ){
+  Trace("smt") << "SMT addToModelCommand(" << c << ", " << c_type << ")" << endl;
   SmtScope smts(this);
   finalOptionsAreSet();
   if( options::produceModels() ) {
-    d_theoryEngine->getModel()->addDefineFunction( e.getNode() );
+    d_theoryEngine->getModel()->addCommand( c, c_type );
   }
 }
 
-
 Model* SmtEngine::getModel() throw(ModalException, AssertionException){
   Trace("smt") << "SMT getModel()" << endl;
   SmtScope smts(this);
 
-  if(!options::produceModels()) {
-    const char* msg =
-      "Cannot get model when produce-models options is off.";
-    throw ModalException(msg);
-  }
   if(d_status.isNull() ||
      d_status.asSatisfiabilityResult() == Result::UNSAT  ||
      d_problemExtended) {
@@ -1871,7 +1874,11 @@ Model* SmtEngine::getModel() throw(ModalException, AssertionException){
       "preceded by SAT/INVALID or UNKNOWN response.";
     throw ModalException(msg);
   }
-
+  if(!options::produceModels()) {
+    const char* msg =
+      "Cannot get model when produce-models options is off.";
+    throw ModalException(msg);
+  }
   return d_theoryEngine->getModel();
 }
 
@@ -2066,7 +2073,13 @@ StatisticsRegistry* SmtEngine::getStatisticsRegistry() const {
 
 void SmtEngine::printModel( std::ostream& out, Model* m ){
   SmtScope smts(this);
-  m->toStream(out);
+  Printer::getPrinter(options::outputLanguage())->toStream( out, m );
+  //m->toStream(out);
+}
+
+void SmtEngine::setUserAttribute( std::string& attr, Expr expr ){
+  SmtScope smts(this);
+  d_theoryEngine->setUserAttribute( attr, expr.getNode() );
 }
 
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 25800f5b3..234814245 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -389,16 +389,10 @@ public:
   CVC4::SExpr getAssignment() throw(ModalException, AssertionException);
 
   /**
-   * Add to Model Type.  This is used for recording which types should be reported
+   * Add to Model command.  This is used for recording a command that should be reported
    * during a get-model call.
    */
-  void addToModelType( Type& t );
-
-  /**
-   * Add to Model Function.  This is used for recording which functions should be reported
-   * during a get-model call.
-   */
-  void addToModelFunction( Expr& e );
+  void addToModelCommand( Command* c, int c_type );
 
   /**
    * Get the model (only if immediately preceded by a SAT
@@ -565,6 +559,12 @@ public:
    */
   void printModel( std::ostream& out, Model* m );
 
+  /** Set user attribute
+    * This function is called when an attribute is set by a user.  In SMT-LIBv2 this is done
+    *  via the syntax (! expr :attr)
+    */
+  void setUserAttribute( std::string& attr, Expr expr );
+
 };/* class SmtEngine */
 
 }/* CVC4 namespace */