diff options
author | lianah <lianahady@gmail.com> | 2013-05-02 14:14:48 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-05-02 14:14:48 -0400 |
commit | aa61950ed5b3370647980c87e95dfbddb366acb5 (patch) | |
tree | 6dee72e317a0051eb6dba47c57517625aaba84a0 /src | |
parent | a0cf1089d3d9c36b4493de3e0498464bb50d950b (diff) | |
parent | 9427bfc0cef9b62146f1b6cff01a8103df97103f (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/attribute.h | 2 | ||||
-rw-r--r-- | src/expr/attribute_internals.h | 14 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 4 | ||||
-rw-r--r-- | src/smt/boolean_terms.cpp | 70 | ||||
-rw-r--r-- | src/smt/boolean_terms.h | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 19 |
6 files changed, 99 insertions, 12 deletions
diff --git a/src/expr/attribute.h b/src/expr/attribute.h index b155b3a1c..70f04be85 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -570,9 +570,11 @@ inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) { while (it != it_end){ uint64_t id = (*it).first.first; + /* Debug("attrgc") << "id " << id << " node_value: " << ((*it).first.second) << std::endl; + */ if(traits_t::cleanup[id] != NULL) { traits_t::cleanup[id]((*it).second); } diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index d7a61e32c..4893075c3 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -294,11 +294,13 @@ public: if(i == super::end()) { return BitIterator(); } + /* Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (unsigned long long)((*i).second), unsigned(k.first)); + */ return BitIterator(*i, k.first); } @@ -316,11 +318,13 @@ public: if(i == super::end()) { return ConstBitIterator(); } + /* Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (unsigned long long)((*i).second), unsigned(k.first)); + */ return ConstBitIterator(*i, k.first); } @@ -409,9 +413,11 @@ class CDAttrHash<bool> : d_key(key), d_word(word), d_bit(bit) { + /* Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor(%p, %p, %016llx, %u)\n", &map, key, (unsigned long long) word, bit); + */ } BitAccessor& operator=(bool b) { @@ -419,25 +425,31 @@ class CDAttrHash<bool> : // set the bit d_word |= (1 << d_bit); d_map.insert(d_key, d_word); + /* Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor::set(%p, %p, %016llx, %u)\n", &d_map, d_key, (unsigned long long) d_word, d_bit); + */ } else { // clear the bit d_word &= ~(1 << d_bit); d_map.insert(d_key, d_word); + /* Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor::clr(%p, %p, %016llx, %u)\n", &d_map, d_key, (unsigned long long) d_word, d_bit); + */ } return *this; } operator bool() const { + /* Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor::toBool(%p, %p, %016llx, %u)\n", &d_map, d_key, (unsigned long long) d_word, d_bit); + */ return (d_word & (1 << d_bit)) ? true : false; } };/* class CDAttrHash<bool>::BitAccessor */ @@ -503,10 +515,12 @@ public: if(i == super::end()) { return ConstBitIterator(); } + /* Debug.printf("cdboolattr", "underlying word at address looks like 0x%016llx, bit is %u\n", (unsigned long long)((*i).second), unsigned(k.first)); + */ return ConstBitIterator(*i, k.first); } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 722d2604b..c59df6269 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -824,11 +824,11 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr const Datatype & d = i->getDatatype(); - out << "(" << d.getName() << " "; + out << "(" << maybeQuoteSymbol(d.getName()) << " "; for(Datatype::const_iterator ctor = d.begin(), ctor_end = d.end(); ctor != ctor_end; ++ctor){ if( ctor!=d.begin() ) out << " "; - out << "(" << ctor->getName(); + out << "(" << maybeQuoteSymbol(ctor->getName()); for(DatatypeConstructor::const_iterator arg = ctor->begin(), arg_end = ctor->end(); arg != arg_end; ++arg){ diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index f8f2330e1..0063035ff 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -111,6 +111,52 @@ static inline bool isBoolean(TNode top, unsigned i) { } } +// This function rewrites "in" as an "as"---this is actually expected +// to be for model-substitution, so the "in" is a Boolean-term-converted +// node, and "as" is the original. See how it's used in function +// handling, below. +Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { + if(in.getType() == as) { + return in; + } + if(in.getType().isBoolean()) { + Assert(d_tt.getType() == as); + return NodeManager::currentNM()->mkNode(kind::ITE, in, d_tt, d_ff); + } + if(as.isBoolean() && in.getType().isBitVector() && in.getType().getBitVectorSize() == 1) { + return NodeManager::currentNM()->mkNode(kind::EQUAL, NodeManager::currentNM()->mkConst(BitVector(1u, 1u)), in); + } + if(in.getType().isDatatype()) { + if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) { + return NodeManager::currentNM()->mkNode(kind::EQUAL, d_ttDt, in); + } + Assert(as.isDatatype()); + const Datatype* dt2 = &as.getDatatype(); + const Datatype* dt1 = d_datatypeCache[dt2]; + Assert(dt1 != NULL, "expected datatype in cache"); + Assert(*dt1 == in.getType().getDatatype(), "improper rewriteAs() between datatypes"); + Node out; + for(size_t i = 0; i < dt1->getNumConstructors(); ++i) { + DatatypeConstructor ctor = (*dt1)[i]; + NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR); + appctorb << (*dt2)[i].getConstructor(); + for(size_t j = 0; j < ctor.getNumArgs(); ++j) { + appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType())); + } + Node appctor = appctorb; + if(i == 0) { + out = appctor; + } else { + Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out); + out = newOut; + } + } + return out; + } + + Unhandled(in); +} + const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw() { const Datatype*& out = d_datatypeCache[&dt]; if(out != NULL) { @@ -392,12 +438,20 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa } else if(mk == kind::metakind::VARIABLE) { TypeNode t = top.getType(); if(t.isFunction()) { - for(unsigned i = 0; i < t.getNumChildren() - 1; ++i) { + for(unsigned i = 0; i < t.getNumChildren(); ++i) { TypeNode newType = convertType(t[i], false); - if(newType != t[i]) { + // is this the return type? (allowed to be Bool) + bool returnType = (i == t.getNumChildren() - 1); + if(newType != t[i] && (!t[i].isBoolean() || !returnType)) { vector<TypeNode> argTypes = t.getArgTypes(); - replace(argTypes.begin(), argTypes.end(), t[i], d_tt.getType()); - TypeNode newType = nm->mkFunctionType(argTypes, t.getRangeType()); + for(unsigned j = 0; j < argTypes.size(); ++j) { + argTypes[j] = convertType(argTypes[j], false); + } + TypeNode rangeType = t.getRangeType(); + if(!rangeType.isBoolean()) { + rangeType = convertType(rangeType, false); + } + TypeNode newType = nm->mkFunctionType(argTypes, rangeType); Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "__boolterm__", newType, "a function introduced by Boolean-term conversion", NodeManager::SKOLEM_EXACT_NAME); @@ -409,14 +463,18 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa for(unsigned j = 0; j < t.getNumChildren() - 1; ++j) { Node var = nm->mkBoundVar(t[j]); boundVarsBuilder << var; - if(t[j].isBoolean()) { - bodyBuilder << nm->mkNode(kind::ITE, var, d_tt, d_ff); + if(t[j] != argTypes[j]) { + bodyBuilder << rewriteAs(var, argTypes[j]); } else { bodyBuilder << var; } } Node boundVars = boundVarsBuilder; Node body = bodyBuilder; + if(t.getRangeType() != rangeType) { + Node convbody = rewriteAs(body, t.getRangeType()); + body = convbody; + } Node lam = nm->mkNode(kind::LAMBDA, boundVars, body); Debug("boolean-terms") << "substituting " << top << " ==> " << lam << endl; d_smt.d_theoryEngine->getModel()->addSubstitution(top, lam); diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h index e5f18b68d..904d47b5f 100644 --- a/src/smt/boolean_terms.h +++ b/src/smt/boolean_terms.h @@ -65,6 +65,8 @@ class BooleanTermConverter { /** The cache used during Boolean term datatype conversion */ BooleanTermDatatypeCache d_datatypeCache; + Node rewriteAs(TNode in, TypeNode as) throw(); + /** * Scan a datatype for and convert as necessary. */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 78f6e3dae..0d473a1a1 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -235,7 +235,7 @@ class SmtEnginePrivate : public NodeManagerListener { unsigned d_realAssertionsEnd; /** The converter for Boolean terms -> BITVECTOR(1). */ - BooleanTermConverter d_booleanTermConverter; + BooleanTermConverter* d_booleanTermConverter; /** A circuit propagator for non-clausal propositional deduction */ booleans::CircuitPropagator d_propagator; @@ -390,7 +390,7 @@ public: d_assertionsToPreprocess(), d_nonClausalLearnedLiterals(), d_realAssertionsEnd(0), - d_booleanTermConverter(d_smt), + d_booleanTermConverter(NULL), d_propagator(d_nonClausalLearnedLiterals, true, true), d_propagatorNeedsFinish(false), d_assertionsToCheck(), @@ -412,6 +412,10 @@ public: d_propagator.finish(); d_propagatorNeedsFinish = false; } + if(d_booleanTermConverter != NULL) { + delete d_booleanTermConverter; + d_booleanTermConverter = NULL; + } d_smt.d_nodeManager->unsubscribeEvents(this); } @@ -1213,7 +1217,8 @@ void SmtEngine::defineFunction(Expr func, stringstream ss; ss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump.getStream())) << func; - Dump("declarations") << DefineFunctionCommand(ss.str(), func, formals, formula); + DefineFunctionCommand c(ss.str(), func, formals, formula); + addToModelCommandAndDump(c, false, true, "declarations"); } SmtScope smts(this); @@ -2680,8 +2685,14 @@ void SmtEnginePrivate::processAssertions() { { Chat() << "rewriting Boolean terms..." << endl; TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime); + if(d_booleanTermConverter == NULL) { + // This needs to be initialized _after_ the whole SMT framework is in place, subscribed + // to ExprManager notifications, etc. Otherwise we might miss the "BooleanTerm" datatype + // definition, and not dump it properly. + d_booleanTermConverter = new BooleanTermConverter(d_smt); + } for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) { - Node n = d_booleanTermConverter.rewriteBooleanTerms(d_assertionsToPreprocess[i]); + Node n = d_booleanTermConverter->rewriteBooleanTerms(d_assertionsToPreprocess[i]); if(n != d_assertionsToPreprocess[i]) { switch(booleans::BooleanTermConversionMode mode = options::booleanTermConversionMode()) { case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS: |