From 0deb883f8c5ba550fda8b90501890940fd916a1b Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sun, 6 Nov 2011 02:09:06 +0000 Subject: [PATCH] datatype stuff in compatibility interface implemented --- src/compat/cvc3_compat.cpp | 129 +++++++++++++++++++++++++++-- src/compat/cvc3_compat.h | 10 ++- src/expr/expr_manager_template.cpp | 27 ++++++ src/expr/expr_manager_template.h | 13 +++ src/util/datatype.cpp | 11 +++ 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 #include #include +#include +#include using namespace std; namespace CVC3 { +static std::hash_map s_typeToExpr; +static std::hash_map s_exprToType; + +static bool typeHasExpr(const Type& t) { + std::hash_map::const_iterator i = s_typeToExpr.find(t); + return i != s_typeToExpr.end(); +} + +static Expr typeToExpr(const Type& t) { + std::hash_map::const_iterator i = s_typeToExpr.find(t); + AlwaysAssert(i != s_typeToExpr.end()); + return (*i).second; +} + +static Type exprToType(const Expr& e) { + std::hash_map::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& selectors, const std::vector& types) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + AlwaysAssert(selectors.size() == types.size()); + vector cv; + vector< vector > sv; + vector< vector > 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& constructors, const std::vector >& selectors, const std::vector >& types) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + AlwaysAssert(constructors.size() == selectors.size()); + AlwaysAssert(constructors.size() == types.size()); + vector nv; + vector< vector > cv; + vector< vector< vector > > sv; + vector< vector< vector > > tv; + nv.push_back(name); + cv.push_back(constructors); + sv.push_back(selectors); + tv.push_back(types); + vector dtts; + dataType(nv, cv, sv, tv, dtts); + AlwaysAssert(dtts.size() == 1); + return dtts[0]; } void ValidityChecker::dataType(const std::vector& names, @@ -1018,7 +1067,55 @@ void ValidityChecker::dataType(const std::vector& names, const std::vector > >& selectors, const std::vector > >& types, std::vector& 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 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())); + } else { + ctor.addArg(selectors[i][j][k], exprToType(types[i][j][k])); + } + } + dt.addConstructor(ctor); + } + dv.push_back(dt); + } + + // Make the datatypes. + vector 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::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& 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(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& 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 ConstructorMap; + typedef std::hash_map, 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& children) { } } +Expr ExprManager::mkExpr(Kind kind, Expr child1, const std::vector& 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 nodes; + nodes.push_back(child1.getNode()); + + vector::const_iterator it = otherChildren.begin(); + vector::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 @@ -193,6 +193,19 @@ public: */ Expr mkExpr(Kind kind, const std::vector& 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& otherChildren); + /** * Make a nullary parameterized expression with the given operator. * 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 -- 2.30.2