summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/compat/cvc3_compat.cpp129
-rw-r--r--src/compat/cvc3_compat.h10
-rw-r--r--src/expr/expr_manager_template.cpp27
-rw-r--r--src/expr/expr_manager_template.h13
-rw-r--r--src/util/datatype.cpp11
5 files changed, 180 insertions, 10 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index cecc136fb..fa5919e6a 100644
--- 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 1e4511ba5..71bea5cf8 100644
--- 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 624fbd9a2..12a60021e 100644
--- 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 184556887..ade9a334d 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -194,6 +194,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.
*
* @param opExpr the operator expression
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 7d7c654bf..19415769e 100644
--- 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback