diff options
| -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 | ||||
| -rw-r--r-- | test/regress/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/bug507.smt2 | 78 |
9 files changed, 180 insertions, 13 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: diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am index f0cfe4301..532d70143 100644 --- a/test/regress/Makefile.am +++ b/test/regress/Makefile.am @@ -23,5 +23,6 @@ regress test: check units systemtests: EXTRA_DIST = \ + Makefile.levels \ run_regression \ README diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index b1e2f6491..12d7ab397 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -148,7 +148,8 @@ BUG_TESTS = \ bug480.smt2 \ bug484.smt2 \ bug486.cvc \ - bug497.cvc + bug497.cvc \ + bug507.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug507.smt2 b/test/regress/regress0/bug507.smt2 new file mode 100644 index 000000000..75a63e328 --- /dev/null +++ b/test/regress/regress0/bug507.smt2 @@ -0,0 +1,78 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status sat) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Datatype declarations +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(declare-datatypes () + ((ColorType (ColorType_Red) (ColorType_Black)) +)) + +(declare-datatypes () + ((RBTree (RBTree_Leaf) (RBTree_Node (destRBTree_Node RBTree_Node_recd))) + + (RBTree_Node_recd (RBTree_Node_recd (RBTree_Node_recd_color ColorType) + (RBTree_Node_recd_left RBTree) (RBTree_Node_recd_elem Int) + (RBTree_Node_recd_right RBTree))) +)) + +(declare-datatypes () + ((BoolColor (BoolColor (BoolColor_res Bool) (BoolColor_color ColorType))) +)) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Uninterpreted symbols +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(declare-fun v0 () Int) +(declare-fun t () RBTree) +;; (declare-fun NoTwoRedsFn (RBTree) BoolColor) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Defined symbols +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-fun assembleFn ((ll RBTree) (le Int) (lr RBTree) (e Int) (rl RBTree) (re Int) (rr RBTree)) RBTree + (RBTree_Node (RBTree_Node_recd ColorType_Red (RBTree_Node (RBTree_Node_recd ColorType_Black ll le lr)) e (RBTree_Node (RBTree_Node_recd ColorType_Black rl re rr))))) + +(define-fun balanceFn ((c ColorType) (left RBTree) (elem Int) (right RBTree)) RBTree + (ite (= c ColorType_Black) (ite (not (ite (is-RBTree_Leaf left) false (ite (not (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) true false))) (ite (is-RBTree_Leaf (RBTree_Node_recd_right (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) ColorType_Red)) true false)) true))) (ite (is-RBTree_Leaf right) (ite (is-RBTree_Leaf left) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (not (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) true false))) (ite (is-RBTree_Leaf (RBTree_Node_recd_right (destRBTree_Node left))) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node left)) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) elem right) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite (not (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node right))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node right)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) ColorType_Red)) true false))) (ite (is-RBTree_Leaf (RBTree_Node_recd_right (destRBTree_Node right))) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node right))) (ite (is-RBTree_Leaf left) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (not (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) true false))) (ite (is-RBTree_Leaf (RBTree_Node_recd_right (destRBTree_Node left))) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node left)) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) elem right) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node right)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) ColorType_Red)) (assembleFn left elem (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) (RBTree_Node_recd_elem (destRBTree_Node right)) (RBTree_Node_recd_right (destRBTree_Node right))) (ite (is-RBTree_Leaf left) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (not (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) true false))) (ite (is-RBTree_Leaf (RBTree_Node_recd_right (destRBTree_Node left))) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node left)) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) elem right) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node right)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node right)))) ColorType_Red)) (assembleFn left elem (RBTree_Node_recd_left (destRBTree_Node right)) (RBTree_Node_recd_elem (destRBTree_Node right)) (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node right)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node right)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node right))))) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node right))) (ite (is-RBTree_Leaf left) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (not (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) true false))) (ite (is-RBTree_Leaf (RBTree_Node_recd_right (destRBTree_Node left))) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node left)) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) elem right) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node right)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) ColorType_Red)) (assembleFn left elem (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) (RBTree_Node_recd_elem (destRBTree_Node right)) (RBTree_Node_recd_right (destRBTree_Node right))) (ite (is-RBTree_Leaf left) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (not (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) true false))) (ite (is-RBTree_Leaf (RBTree_Node_recd_right (destRBTree_Node left))) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node left)) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) elem right) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))))))) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node right))) (ite (is-RBTree_Leaf left) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (not (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) true false))) (ite (is-RBTree_Leaf (RBTree_Node_recd_right (destRBTree_Node left))) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node left)) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) elem right) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node right)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) ColorType_Red)) (assembleFn left elem (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) (RBTree_Node_recd_elem (destRBTree_Node right)) (RBTree_Node_recd_right (destRBTree_Node right))) (ite (is-RBTree_Leaf left) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (not (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) true false))) (ite (is-RBTree_Leaf (RBTree_Node_recd_right (destRBTree_Node left))) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node left)) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) elem right) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))))))) (ite (is-RBTree_Leaf left) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (not (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) true false))) (ite (is-RBTree_Leaf (RBTree_Node_recd_right (destRBTree_Node left))) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node left)) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) elem right) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite (is-RBTree_Leaf (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right))))))) (RBTree_Node (RBTree_Node_recd c left elem right)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Catamorphisms +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +( declare-fun memberFn ( Int RBTree ) Bool ) + +( declare-fun EqualBlackPathsFn ( RBTree ) Int ) + +( declare-fun insFn ( Int RBTree ) RBTree ) + +( declare-fun insertFn ( Int RBTree ) RBTree ) + +( declare-fun NoTwoRedsFn ( RBTree ) BoolColor ) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Goals +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;(push) +(assert (and (is-RBTree_Leaf t) + (and (not (is-RBTree_Leaf (insertFn v0 t))) + (not (BoolColor_res (NoTwoRedsFn (RBTree_Node_recd_left (destRBTree_Node (insertFn v0 t))))))))) + +;;(pop) + +( assert ( = ( insertFn v0 t ) ( ite ( is-RBTree_Leaf ( insFn v0 t ) ) ( insFn v0 t ) ( RBTree_Node ( RBTree_Node_recd ColorType_Black ( RBTree_Node_recd_left ( destRBTree_Node ( insFn v0 t ) ) ) ( RBTree_Node_recd_elem ( destRBTree_Node ( insFn v0 t ) ) ) ( RBTree_Node_recd_right ( destRBTree_Node ( insFn v0 t ) ) ) ) ) ) ) ) +( assert ( = ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 t ) ) ) ) ( ite ( is-RBTree_Leaf ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 t ) ) ) ) ( BoolColor true ColorType_Black ) ( BoolColor ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ( or ( not ( = ( RBTree_Node_recd_color ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ColorType_Red ) ) ( and ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ColorType_Red ) ) ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ColorType_Red ) ) ) ) ) ) ( RBTree_Node_recd_color ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ) ) +( assert ( = ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 t ) ) ) ) ( ite ( is-RBTree_Leaf ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 t ) ) ) ) ( BoolColor true ColorType_Black ) ( BoolColor ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ( or ( not ( = ( RBTree_Node_recd_color ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ColorType_Red ) ) ( and ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ColorType_Red ) ) ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ColorType_Red ) ) ) ) ) ) ( RBTree_Node_recd_color ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ) ) +( assert ( = ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ( ite ( is-RBTree_Leaf ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ( BoolColor true ColorType_Black ) ( BoolColor ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ( or ( not ( = ( RBTree_Node_recd_color ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ColorType_Red ) ) ( and ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ColorType_Red ) ) ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ColorType_Red ) ) ) ) ) ) ( RBTree_Node_recd_color ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ) ) +( assert ( = ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ( ite ( is-RBTree_Leaf ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ( BoolColor true ColorType_Black ) ( BoolColor ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ( or ( not ( = ( RBTree_Node_recd_color ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ColorType_Red ) ) ( and ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ColorType_Red ) ) ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ColorType_Red ) ) ) ) ) ) ( RBTree_Node_recd_color ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ) ) +( assert ( = ( insertFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ( ite ( is-RBTree_Leaf ( insFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ( insFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ( RBTree_Node ( RBTree_Node_recd ColorType_Black ( RBTree_Node_recd_left ( destRBTree_Node ( insFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ( RBTree_Node_recd_elem ( destRBTree_Node ( insFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ( RBTree_Node_recd_right ( destRBTree_Node ( insFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ) ) ) ) +( assert ( = ( NoTwoRedsFn ( insertFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ( ite ( is-RBTree_Leaf ( insertFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ( BoolColor true ColorType_Black ) ( BoolColor ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ) ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ) ( or ( not ( = ( RBTree_Node_recd_color ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ColorType_Red ) ) ( and ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ) ColorType_Red ) ) ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ) ColorType_Red ) ) ) ) ) ) ( RBTree_Node_recd_color ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ) ) ) +( assert ( = ( insertFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ( ite ( is-RBTree_Leaf ( insFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ( insFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ( RBTree_Node ( RBTree_Node_recd ColorType_Black ( RBTree_Node_recd_left ( destRBTree_Node ( insFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ( RBTree_Node_recd_elem ( destRBTree_Node ( insFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ( RBTree_Node_recd_right ( destRBTree_Node ( insFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ) ) ) ) +( assert ( = ( NoTwoRedsFn ( insertFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ( ite ( is-RBTree_Leaf ( insertFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ( BoolColor true ColorType_Black ) ( BoolColor ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ) ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ) ( or ( not ( = ( RBTree_Node_recd_color ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ColorType_Red ) ) ( and ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ) ColorType_Red ) ) ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ) ColorType_Red ) ) ) ) ) ) ( RBTree_Node_recd_color ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ) ) ) +( check-sat ) |