datatype stuff in compatibility interface implemented

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index cecc136fbbdc765e98e1b5318acf1660c16b2d95..fa5919e6abc72b1bced532afa753fe65b137b331 100644 (file)
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -24,6 +24,7 @@
 #include "util/rational.h"
 #include "util/integer.h"
 #include "util/bitvector.h"
+#include "util/hash.h"
 
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -31,11 +32,33 @@
 #include <iostream>
 #include <string>
 #include <sstream>
+#include <algorithm>
+#include <iterator>
 
 using namespace std;
 
 namespace CVC3 {
 
+static std::hash_map<Type, Expr, CVC4::TypeHashFunction> s_typeToExpr;
+static std::hash_map<Expr, Type, CVC4::ExprHashFunction> s_exprToType;
+
+static bool typeHasExpr(const Type& t) {
+  std::hash_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t);
+  return i != s_typeToExpr.end();
+}
+
+static Expr typeToExpr(const Type& t) {
+  std::hash_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t);
+  AlwaysAssert(i != s_typeToExpr.end());
+  return (*i).second;
+}
+
+static Type exprToType(const Expr& e) {
+  std::hash_map<Expr, Type, CVC4::ExprHashFunction>::const_iterator i = s_exprToType.find(e);
+  AlwaysAssert(i != s_exprToType.end());
+  return (*i).second;
+}
+
 std::string int2string(int n) {
   std::ostringstream ss;
   ss << n;
@@ -139,7 +162,13 @@ Type::Type(const Type& type) :
 }
 
 Expr Type::getExpr() const {
-  Unimplemented();
+  if(typeHasExpr(*this)) {
+    return typeToExpr(*this);
+  }
+  Expr e = getExprManager()->mkVar("compatibility-layer-expr-type", *this);
+  s_typeToExpr[*this] = e;
+  s_exprToType[e] = *this;
+  return e;
 }
 
 int Type::arity() const {
@@ -1003,14 +1032,34 @@ Type ValidityChecker::dataType(const std::string& name,
                                const std::string& constructor,
                                const std::vector<std::string>& selectors,
                                const std::vector<Expr>& types) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  AlwaysAssert(selectors.size() == types.size());
+  vector<string> cv;
+  vector< vector<string> > sv;
+  vector< vector<Expr> > tv;
+  cv.push_back(constructor);
+  sv.push_back(selectors);
+  tv.push_back(types);
+  return dataType(name, cv, sv, tv);
 }
 
 Type ValidityChecker::dataType(const std::string& name,
                                const std::vector<std::string>& constructors,
                                const std::vector<std::vector<std::string> >& selectors,
                                const std::vector<std::vector<Expr> >& types) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  AlwaysAssert(constructors.size() == selectors.size());
+  AlwaysAssert(constructors.size() == types.size());
+  vector<string> nv;
+  vector< vector<string> > cv;
+  vector< vector< vector<string> > > sv;
+  vector< vector< vector<Expr> > > tv;
+  nv.push_back(name);
+  cv.push_back(constructors);
+  sv.push_back(selectors);
+  tv.push_back(types);
+  vector<Type> dtts;
+  dataType(nv, cv, sv, tv, dtts);
+  AlwaysAssert(dtts.size() == 1);
+  return dtts[0];
 }
 
 void ValidityChecker::dataType(const std::vector<std::string>& names,
@@ -1018,7 +1067,55 @@ void ValidityChecker::dataType(const std::vector<std::string>& names,
                                const std::vector<std::vector<std::vector<std::string> > >& selectors,
                                const std::vector<std::vector<std::vector<Expr> > >& types,
                                std::vector<Type>& returnTypes) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+
+  AlwaysAssert(names.size() == constructors.size());
+  AlwaysAssert(names.size() == selectors.size());
+  AlwaysAssert(names.size() == types.size());
+  vector<CVC4::Datatype> dv;
+
+  // Set up the datatype specifications.
+  for(unsigned i = 0; i < names.size(); ++i) {
+    CVC4::Datatype dt(names[i]);
+    AlwaysAssert(constructors[i].size() == selectors[i].size());
+    AlwaysAssert(constructors[i].size() == types[i].size());
+    for(unsigned j = 0; j < constructors[i].size(); ++j) {
+      CVC4::Datatype::Constructor ctor(constructors[i][j]);
+      AlwaysAssert(selectors[i][j].size() == types[i][j].size());
+      for(unsigned k = 0; k < selectors[i][j].size(); ++k) {
+        if(types[i][j][k].getType().isString()) {
+          ctor.addArg(selectors[i][j][k], CVC4::Datatype::UnresolvedType(types[i][j][k].getConst<string>()));
+        } else {
+          ctor.addArg(selectors[i][j][k], exprToType(types[i][j][k]));
+        }
+      }
+      dt.addConstructor(ctor);
+    }
+    dv.push_back(dt);
+  }
+
+  // Make the datatypes.
+  vector<CVC4::DatatypeType> dtts = d_em->mkMutualDatatypeTypes(dv);
+
+  // Post-process to register the names of everything with this validity checker.
+  // This is necessary for the compatibility layer because cons/sel operations are
+  // constructed without appealing explicitly to the Datatype they belong to.
+  for(vector<CVC4::DatatypeType>::iterator i = dtts.begin(); i != dtts.end(); ++i) {
+    // For each datatype...
+    const CVC4::Datatype& dt = (*i).getDatatype();
+    for(CVC4::Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) {
+      // For each constructor, register its name and its selectors names.
+      AlwaysAssert(d_constructors.find((*j).getName()) == d_constructors.end(), "cannot have two constructors with the same name in a ValidityChecker");
+      d_constructors[(*j).getName()] = &dt;
+      for(CVC4::Datatype::Constructor::const_iterator k = (*j).begin(); k != (*j).end(); ++k) {
+        AlwaysAssert(d_selectors.find((*k).getName()) == d_selectors.end(), "cannot have two selectors with the same name in a ValidityChecker");
+        d_selectors[(*k).getName()] = make_pair(&dt, (*j).getName());
+      }
+    }
+  }
+
+  // Copy into the output buffer.
+  returnTypes.clear();
+  copy(dtts.begin(), dtts.end(), back_inserter(returnTypes));
 }
 
 Type ValidityChecker::arrayType(const Type& typeIndex, const Type& typeData) {
@@ -1088,7 +1185,7 @@ Expr ValidityChecker::getTypePred(const Type&t, const Expr& e) {
 }
 
 Expr ValidityChecker::stringExpr(const std::string& str) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  return d_em->mkConst(str);
 }
 
 Expr ValidityChecker::idExpr(const std::string& name) {
@@ -1669,15 +1766,29 @@ Expr ValidityChecker::tupleUpdateExpr(const Expr& tuple, int index,
 }
 
 Expr ValidityChecker::datatypeConsExpr(const std::string& constructor, const std::vector<Expr>& args) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  ConstructorMap::const_iterator i = d_constructors.find(constructor);
+  AlwaysAssert(i != d_constructors.end(), "no such constructor");
+  const CVC4::Datatype& dt = *(*i).second;
+  const CVC4::Datatype::Constructor& ctor = dt[constructor];
+  AlwaysAssert(ctor.getNumArgs() == args.size(), "arity mismatch in constructor application");
+  return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, ctor.getConstructor(), vector<CVC4::Expr>(args.begin(), args.end()));
 }
 
 Expr ValidityChecker::datatypeSelExpr(const std::string& selector, const Expr& arg) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  SelectorMap::const_iterator i = d_selectors.find(selector);
+  AlwaysAssert(i != d_selectors.end(), "no such selector");
+  const CVC4::Datatype& dt = *(*i).second.first;
+  string constructor = (*i).second.second;
+  const CVC4::Datatype::Constructor& ctor = dt[constructor];
+  return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR, ctor.getSelector(selector), arg);
 }
 
 Expr ValidityChecker::datatypeTestExpr(const std::string& constructor, const Expr& arg) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  ConstructorMap::const_iterator i = d_constructors.find(constructor);
+  AlwaysAssert(i != d_constructors.end(), "no such constructor");
+  const CVC4::Datatype& dt = *(*i).second;
+  const CVC4::Datatype::Constructor& ctor = dt[constructor];
+  return d_em->mkExpr(CVC4::kind::APPLY_TESTER, ctor.getTester(), arg);
 }
 
 Expr ValidityChecker::boundVarExpr(const std::string& name, const std::string& uid,
@@ -1799,7 +1910,7 @@ QueryResult ValidityChecker::restart(const Expr& e) {
 }
 
 void ValidityChecker::returnFromCheck() {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  // CVC4 has this behavior by default
 }
 
 void ValidityChecker::getUserAssumptions(std::vector<Expr>& assumptions) {

diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h
index 1e4511ba51586bbab57c663182921f8601a9ef08..71bea5cf835f6bc38dacf4d40d96110cde0d0569 100644 (file)
--- a/src/compat/cvc3_compat.h
+++ b/src/compat/cvc3_compat.h
@@ -16,7 +16,9 @@
  ** CVC3 compatibility layer for CVC4.  This version was derived from
  ** the following CVS revisions of the following files in CVC3.  If
  ** those files have a later revision, then this file might be out of
- ** date.
+ ** date.  Note that this compatibility layer is not safe for use in
+ ** multithreaded contexts where multiple threads are accessing this
+ ** compatibility layer functionality.
  **
  ** src/include/vc.h 1.36
  ** src/include/expr.h 1.39
@@ -466,6 +468,12 @@ class CVC4_PUBLIC ValidityChecker {
   CVC4::SmtEngine* d_smt;
   CVC4::parser::Parser* d_parserContext;
 
+  typedef std::hash_map<std::string, const CVC4::Datatype*, CVC4::StringHashFunction> ConstructorMap;
+  typedef std::hash_map<std::string, std::pair<const CVC4::Datatype*, std::string>, CVC4::StringHashFunction> SelectorMap;
+
+  ConstructorMap d_constructors;
+  SelectorMap d_selectors;
+
   ValidityChecker(const CLFlags& clflags);
 
   void setUpOptions(CVC4::Options& options, const CLFlags& clflags);

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 624fbd9a2ccde6eba83199c5a72e460606f8ec72..12a60021e176fa868e1a277ab7b231b5187ed4d6 100644 (file)
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -268,6 +268,33 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
   }
 }
 
+Expr ExprManager::mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherChildren) {
+  const unsigned n = otherChildren.size() - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0) + 1;
+  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+                "Exprs with kind %s must have at least %u children and "
+                "at most %u children (the one under construction has %u)",
+                kind::kindToString(kind).c_str(),
+                minArity(kind), maxArity(kind), n);
+
+  NodeManagerScope nms(d_nodeManager);
+
+  vector<Node> nodes;
+  nodes.push_back(child1.getNode());
+
+  vector<Expr>::const_iterator it = otherChildren.begin();
+  vector<Expr>::const_iterator it_end = otherChildren.end();
+  while(it != it_end) {
+    nodes.push_back(it->getNode());
+    ++it;
+  }
+  try {
+    INC_STAT(kind);
+    return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
 Expr ExprManager::mkExpr(Expr opExpr) {
   const unsigned n = 0;
   Kind kind = kind::operatorKindToKind(opExpr.getKind());

diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 18455688763d806f2401bdb3a602313a555cd50a..ade9a334d36cdd5f800e9b5c7bc798ad39529bdd 100644 (file)
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -193,6 +193,19 @@ public:
    */
   Expr mkExpr(Kind kind, const std::vector<Expr>& children);
 
+  /**
+   * Make an n-ary expression of given kind given a first arg and
+   * a vector of its remaining children (this can be useful where the
+   * kind is parameterized operator, so the first arg is really an
+   * arg to the kind to construct an operator)
+   *
+   * @param kind the kind of expression to build
+   * @param child1 the first subexpression
+   * @param children the remaining subexpressions
+   * @return the n-ary expression
+   */
+  Expr mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherChildren);
+
   /**
    * Make a nullary parameterized expression with the given operator.
    *

diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 7d7c654bf72e5760493b9a159e965012cb0b04e1..19415769e22d7c42ce23661b871a40f65ac82603 100644 (file)
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -471,6 +471,17 @@ Type Datatype::Constructor::doParametricSubstitution( Type range,
   }
 }
 
+Datatype::Constructor::Constructor(std::string name) :
+  // We don't want to introduce a new data member, because eventually
+  // we're going to be a constant stuffed inside a node.  So we stow
+  // the tester name away inside the constructor name until
+  // resolution.
+  d_name(name + '\0' + "is_" + name), // default tester name is "is_FOO"
+  d_tester(),
+  d_args() {
+  CheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
+}
+
 Datatype::Constructor::Constructor(std::string name, std::string tester) :
   // We don't want to introduce a new data member, because eventually
   // we're going to be a constant stuffed inside a node.  So we stow