Tuples and records merge. Resolves bug 270.

Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together.

(this commit was certified error- and warning-free by the test-and-commit script.)

5 files changed, 159 insertions, 14 deletions

diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 5555a6190..82601e3c3 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -8,6 +8,8 @@ noinst_LTLIBRARIES = libsmt.la
 libsmt_la_SOURCES = \
 	smt_engine.cpp \
 	smt_engine.h \
+	model_postprocessor.cpp \
+	model_postprocessor.h \
 	smt_engine_scope.cpp \
 	smt_engine_scope.h \
 	command_list.cpp \
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
new file mode 100644
index 000000000..38fd3ab8b
--- /dev/null
+++ b/src/smt/model_postprocessor.cpp
@@ -0,0 +1,52 @@
+/*********************                                                        */
+/*! \file model_postprocessor.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  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief 
+ **
+ ** 
+ **/
+
+#include "smt/model_postprocessor.h"
+
+using namespace CVC4;
+using namespace CVC4::smt;
+
+void ModelPostprocessor::visit(TNode current, TNode parent) {
+  Debug("tuprec") << "visiting " << current << std::endl;
+  Assert(!alreadyVisited(current, TNode::null()));
+  if(current.getType().hasAttribute(expr::DatatypeTupleAttr())) {
+    Assert(current.getKind() == kind::APPLY_CONSTRUCTOR);
+    NodeBuilder<> b(kind::TUPLE);
+    for(TNode::iterator i = current.begin(); i != current.end(); ++i) {
+      Assert(alreadyVisited(*i, TNode::null()));
+      TNode n = d_nodes[*i];
+      b << (n.isNull() ? *i : n);
+    }
+    d_nodes[current] = b;
+    Debug("tuprec") << "returning " << d_nodes[current] << std::endl;
+  } else if(current.getType().hasAttribute(expr::DatatypeRecordAttr())) {
+    Assert(current.getKind() == kind::APPLY_CONSTRUCTOR);
+    NodeBuilder<> b(kind::RECORD);
+    b << current.getType().getAttribute(expr::DatatypeRecordAttr());
+    for(TNode::iterator i = current.begin(); i != current.end(); ++i) {
+      Assert(alreadyVisited(*i, TNode::null()));
+      TNode n = d_nodes[*i];
+      b << (n.isNull() ? *i : n);
+    }
+    d_nodes[current] = b;
+    Debug("tuprec") << "returning " << d_nodes[current] << std::endl;
+  } else {
+    Debug("tuprec") << "returning self" << std::endl;
+    // rewrite to self
+    d_nodes[current] = Node::null();
+  }
+}/* ModelPostprocessor::visit() */
+
diff --git a/src/smt/model_postprocessor.h b/src/smt/model_postprocessor.h
new file mode 100644
index 000000000..08e6168d9
--- /dev/null
+++ b/src/smt/model_postprocessor.h
@@ -0,0 +1,50 @@
+/*********************                                                        */
+/*! \file model_postprocessor.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  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief 
+ **
+ ** 
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__MODEL_POSTPROCESSOR_H
+#define __CVC4__MODEL_POSTPROCESSOR_H
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace smt {
+
+class ModelPostprocessor {
+public:
+  typedef Node return_type;
+  std::hash_map<TNode, Node, TNodeHashFunction> d_nodes;
+
+  bool alreadyVisited(TNode current, TNode parent) {
+    return d_nodes.find(current) != d_nodes.end();
+  }
+
+  void visit(TNode current, TNode parent);
+
+  void start(TNode n) { }
+
+  Node done(TNode n) {
+    Assert(alreadyVisited(n, TNode::null()));
+    TNode retval = d_nodes[n];
+    return retval.isNull() ? n : retval;
+  }
+};/* class ModelPostprocessor */
+
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__MODEL_POSTPROCESSOR_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5ea16f20f..07e3439fc 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -40,11 +40,13 @@
 #include "smt/modal_exception.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/model_postprocessor.h"
 #include "theory/theory_engine.h"
 #include "theory/bv/theory_bv_rewriter.h"
 #include "proof/proof_manager.h"
 #include "util/proof.h"
 #include "util/boolean_simplification.h"
+#include "util/node_visitor.h"
 #include "util/configuration.h"
 #include "util/exception.h"
 #include "smt/command_list.h"
@@ -366,14 +368,14 @@ public:
     d_smt.addToModelCommandAndDump(c);
   }
 
-  void nmNotifyNewVar(TNode n) {
+  void nmNotifyNewVar(TNode n, bool isGlobal) {
     DeclareFunctionCommand c(n.getAttribute(expr::VarNameAttr()),
                              n.toExpr(),
                              n.getType().toType());
-    d_smt.addToModelCommandAndDump(c);
+    d_smt.addToModelCommandAndDump(c, isGlobal);
   }
 
-  void nmNotifyNewSkolem(TNode n, const std::string& comment) {
+  void nmNotifyNewSkolem(TNode n, const std::string& comment, bool isGlobal) {
     std::string id = n.getAttribute(expr::VarNameAttr());
     DeclareFunctionCommand c(id,
                              n.toExpr(),
@@ -381,7 +383,7 @@ public:
     if(Dump.isOn("skolems") && comment != "") {
       Dump("skolems") << CommentCommand(id + " is " + comment);
     }
-    d_smt.addToModelCommandAndDump(c, false, "skolems");
+    d_smt.addToModelCommandAndDump(c, isGlobal, false, "skolems");
   }
 
   Node applySubstitutions(TNode node) const {
@@ -502,6 +504,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_definedFunctions(NULL),
   d_assertionList(NULL),
   d_assignments(NULL),
+  d_modelGlobalCommands(),
   d_modelCommands(NULL),
   d_dumpCommands(),
   d_logic(),
@@ -2020,7 +2023,6 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node,
   return false;
 }
 
-
 void SmtEnginePrivate::processAssertions() {
   Assert(d_smt.d_fullyInited);
   Assert(d_smt.d_pendingPops == 0);
@@ -2389,6 +2391,9 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
 
   // Add the formula
   d_problemExtended = true;
+  if(d_assertionList != NULL) {
+    d_assertionList->push_back(e.notExpr());
+  }
   d_private->addFormula(e.getNode().notNode());
 
   // Run the check
@@ -2440,6 +2445,12 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log
   return quickCheck().asValidityResult();
 }
 
+Node SmtEngine::postprocess(TNode node) {
+  ModelPostprocessor mpost;
+  NodeVisitor<ModelPostprocessor> visitor;
+  return visitor.run(mpost, node);
+}
+
 Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException) {
   Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
@@ -2458,7 +2469,9 @@ Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicExcep
 
   // Make sure all preprocessing is done
   d_private->processAssertions();
-  return d_private->simplify(Node::fromExpr(e)).toExpr();
+  Node n = d_private->simplify(Node::fromExpr(e));
+  n = postprocess(n);
+  return n.toExpr();
 }
 
 Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, LogicException) {
@@ -2478,7 +2491,9 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L
     Dump("benchmark") << ExpandDefinitionsCommand(e);
   }
   hash_map<Node, Node, NodeHashFunction> cache;
-  return d_private->expandDefinitions(Node::fromExpr(e), cache).toExpr();
+  Node n = d_private->expandDefinitions(Node::fromExpr(e), cache);
+  n = postprocess(n);
+  return n.toExpr();
 }
 
 Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, LogicException) {
@@ -2520,10 +2535,12 @@ Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, LogicException) {
   Trace("smt") << "--- getting value of " << n << endl;
   TheoryModel* m = d_theoryEngine->getModel();
   Node resultNode;
-  if( m ){
-    resultNode = m->getValue( n );
+  if(m != NULL) {
+    resultNode = m->getValue(n);
   }
   Trace("smt") << "--- got value " << n << " = " << resultNode << endl;
+  resultNode = postprocess(resultNode);
+  Trace("smt") << "--- model-post returned " << resultNode << endl;
 
   // type-check the result we got
   Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(n.getType()));
@@ -2630,7 +2647,7 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
   return SExpr(sexprs);
 }
 
-void SmtEngine::addToModelCommandAndDump(const Command& c, bool userVisible, const char* dumpTag) {
+void SmtEngine::addToModelCommandAndDump(const Command& c, bool isGlobal, bool userVisible, const char* dumpTag) {
   Trace("smt") << "SMT addToModelCommandAndDump(" << c << ")" << endl;
   SmtScope smts(this);
   // If we aren't yet fully inited, the user might still turn on
@@ -2643,7 +2660,11 @@ void SmtEngine::addToModelCommandAndDump(const Command& c, bool userVisible, con
   // and expects to find their cardinalities in the model.
   if(/* userVisible && */ (!d_fullyInited || options::produceModels())) {
     doPendingPops();
-    d_modelCommands->push_back(c.clone());
+    if(isGlobal) {
+      d_modelGlobalCommands.push_back(c.clone());
+    } else {
+      d_modelCommands->push_back(c.clone());
+    }
   }
   if(Dump.isOn(dumpTag)) {
     if(d_fullyInited) {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 2590bc8e2..b6fb156f6 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -87,6 +87,10 @@ namespace smt {
   typedef context::CDList<Command*, CommandCleanup> CommandList;
 }/* CVC4::smt namespace */
 
+namespace theory {
+  class TheoryModel;
+}/* CVC4::theory namespace */
+
 namespace stats {
   StatisticsRegistry* getStatisticsRegistry(SmtEngine*);
 }/* CVC4::stats namespace */
@@ -144,8 +148,16 @@ class CVC4_PUBLIC SmtEngine {
   AssignmentSet* d_assignments;
 
   /**
-   * A list of commands that should be in the Model.  Only maintained
-   * if produce-models option is on.
+   * A list of commands that should be in the Model globally (i.e.,
+   * regardless of push/pop).  Only maintained if produce-models option
+   * is on.
+   */
+  std::vector<Command*> d_modelGlobalCommands;
+
+  /**
+   * A list of commands that should be in the Model locally (i.e.,
+   * it is context-dependent on push/pop).  Only maintained if
+   * produce-models option is on.
    */
   smt::CommandList* d_modelCommands;
 
@@ -232,6 +244,13 @@ class CVC4_PUBLIC SmtEngine {
   void checkModel(bool hardFailure = true);
 
   /**
+   * Postprocess a value for output to the user.  Involves doing things
+   * like turning datatypes back into tuples, length-1-bitvectors back
+   * into booleans, etc.
+   */
+  Node postprocess(TNode n);
+
+  /**
    * This is something of an "init" procedure, but is idempotent; call
    * as often as you like.  Should be called whenever the final options
    * and logic for the problem are set (at least, those options that are
@@ -293,6 +312,7 @@ class CVC4_PUBLIC SmtEngine {
   friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
   // to access d_modelCommands
   friend class ::CVC4::Model;
+  friend class ::CVC4::theory::TheoryModel;
   // to access getModel(), which is private (for now)
   friend class GetModelCommand;
 
@@ -304,7 +324,7 @@ class CVC4_PUBLIC SmtEngine {
    * Add to Model command.  This is used for recording a command
    * that should be reported during a get-model call.
    */
-  void addToModelCommandAndDump(const Command& c, bool userVisible = true, const char* dumpTag = "declarations");
+  void addToModelCommandAndDump(const Command& c, bool isGlobal = false, bool userVisible = true, const char* dumpTag = "declarations");
 
   /**
    * Get the model (only if immediately preceded by a SAT