From b90081962840584bb9eeda368ea232a7d42a292b Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 18 Apr 2011 08:59:09 +0000
Subject: Partial merge from datatypes-merge branch:

1. Defines a new type "DatatypeType", a type-constant that holds a Datatype, describing an inductive data type.
2. CVC language parser supports datatypes.
3. CVC language printer now functional.
4. Minor other cleanups.

No performance impact is expected outside of datatypes.  I'm verifying that that is the case with a cluster job this morning.
---
 src/smt/smt_engine.cpp | 80 ++++++++++++++++++++++++++++++++------------------
 1 file changed, 52 insertions(+), 28 deletions(-)

(limited to 'src/smt')

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d821b7f4a..2467db3bb 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: dejan
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): taking, cconway
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -46,6 +46,7 @@
 #include "theory/arith/theory_arith.h"
 #include "theory/arrays/theory_arrays.h"
 #include "theory/bv/theory_bv.h"
+#include "theory/datatypes/theory_datatypes.h"
 
 
 using namespace std;
@@ -98,7 +99,7 @@ class SmtEnginePrivate {
 public:
 
   /**
-   * Pre-process an Node.  This is expected to be highly-variable,
+   * Pre-process a Node.  This is expected to be highly-variable,
    * with a lot of "source-level configurability" to add multiple
    * passes over the Node.
    */
@@ -141,6 +142,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_theoryEngine->addTheory<theory::arith::TheoryArith>();
   d_theoryEngine->addTheory<theory::arrays::TheoryArrays>();
   d_theoryEngine->addTheory<theory::bv::TheoryBV>();
+  d_theoryEngine->addTheory<theory::datatypes::TheoryDatatypes>();
   switch(Options::current()->uf_implementation) {
   case Options::TIM:
     d_theoryEngine->addTheory<theory::uf::tim::TheoryUFTim>();
@@ -442,29 +444,40 @@ Node SmtEnginePrivate::expandDefinitions(SmtEngine& smt, TNode n,
 Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode in)
   throw(NoSuchFunctionException, AssertionException) {
 
-  Node n;
-  if(!Options::current()->lazyDefinitionExpansion) {
-    Debug("expand") << "have: " << n << endl;
-    hash_map<TNode, Node, TNodeHashFunction> cache;
-    n = expandDefinitions(smt, in, cache);
-    Debug("expand") << "made: " << n << endl;
-  } else {
-    n = in;
-  }
+  try {
+    Node n;
+    if(!Options::current()->lazyDefinitionExpansion) {
+      Debug("expand") << "have: " << n << endl;
+      hash_map<TNode, Node, TNodeHashFunction> cache;
+      n = expandDefinitions(smt, in, cache);
+      Debug("expand") << "made: " << n << endl;
+    } else {
+      n = in;
+    }
 
-  // For now, don't re-statically-learn from learned facts; this could
-  // be useful though (e.g., theory T1 could learn something further
-  // from something learned previously by T2).
-  NodeBuilder<> learned(kind::AND);
-  learned << n;
-  smt.d_theoryEngine->staticLearning(n, learned);
-  if(learned.getNumChildren() == 1) {
-    learned.clear();
-  } else {
-    n = learned;
-  }
+    // For now, don't re-statically-learn from learned facts; this could
+    // be useful though (e.g., theory T1 could learn something further
+    // from something learned previously by T2).
+    NodeBuilder<> learned(kind::AND);
+    learned << n;
+    smt.d_theoryEngine->staticLearning(n, learned);
+    if(learned.getNumChildren() == 1) {
+      learned.clear();
+    } else {
+      n = learned;
+    }
 
-  return smt.d_theoryEngine->preprocess(n);
+    return smt.d_theoryEngine->preprocess(n);
+  } catch(TypeCheckingExceptionPrivate& tcep) {
+    // Calls to this function should have already weeded out any
+    // typechecking exceptions via (e.g.) ensureBoolean().  But a
+    // theory could still create a new expression that isn't
+    // well-typed, and we don't want the C++ runtime to abort our
+    // process without any error notice.
+    InternalError("A bad expression was produced.  "
+                  "Original exception follows:\n%s",
+                  tcep.toString().c_str());
+  }
 }
 
 Result SmtEngine::check() {
@@ -479,10 +492,21 @@ Result SmtEngine::quickCheck() {
 
 void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n)
   throw(NoSuchFunctionException, AssertionException) {
-  Debug("smt") << "push_back assertion " << n << endl;
-  smt.d_haveAdditions = true;
-  Node node = SmtEnginePrivate::preprocess(smt, n);
-  smt.d_propEngine->assertFormula(node);
+  try {
+    Debug("smt") << "push_back assertion " << n << endl;
+    smt.d_haveAdditions = true;
+    Node node = SmtEnginePrivate::preprocess(smt, n);
+    smt.d_propEngine->assertFormula(node);
+  } catch(TypeCheckingExceptionPrivate& tcep) {
+    // Calls to this function should have already weeded out any
+    // typechecking exceptions via (e.g.) ensureBoolean().  But a
+    // theory could still create a new expression that isn't
+    // well-typed, and we don't want the C++ runtime to abort our
+    // process without any error notice.
+    InternalError("A bad expression was produced.  "
+                  "Original exception follows:\n%s",
+                  tcep.toString().c_str());
+  }
 }
 
 void SmtEngine::ensureBoolean(const BoolExpr& e) {
-- 
cgit v1.2.3