From 07799f0b077d63b261dd0550b188c1c900c69b1d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 19 May 2022 12:30:05 -0500 Subject: [PATCH] Minor deleting of unused code (#8800) Towards improving coverage. --- src/smt/command.cpp | 15 --- src/smt/command.h | 13 --- src/theory/arith/linear/normal_form.cpp | 46 --------- src/theory/arith/linear/normal_form.h | 9 -- .../ematching/inst_match_generator_multi.cpp | 2 +- .../inst_strategy_e_matching_user.cpp | 23 ----- .../ematching/inst_strategy_e_matching_user.h | 4 - src/theory/quantifiers/inst_match_trie.cpp | 97 +++---------------- src/theory/quantifiers/inst_match_trie.h | 36 ++----- src/theory/quantifiers/instantiate.cpp | 12 +-- src/theory/quantifiers/instantiate.h | 5 +- src/theory/quantifiers/quantifiers_state.cpp | 34 +------ src/theory/sets/theory_sets_private.cpp | 37 +------ src/theory/uf/theory_uf_model.cpp | 56 +++-------- src/theory/uf/theory_uf_model.h | 3 +- 15 files changed, 45 insertions(+), 347 deletions(-) diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 885b79182..eb37c0c21 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -124,21 +124,6 @@ ostream& operator<<(ostream& out, const CommandStatus* s) return out; } -/* output stream insertion operator for benchmark statuses */ -std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) -{ - switch (status) - { - case SMT_SATISFIABLE: return out << "sat"; - - case SMT_UNSATISFIABLE: return out << "unsat"; - - case SMT_UNKNOWN: return out << "unknown"; - - default: return out << "BenchmarkStatus::[UNKNOWNSTATUS!]"; - } -} - /* -------------------------------------------------------------------------- */ /* class CommandPrintSuccess */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.h b/src/smt/command.h index 66854a03b..0af8b4b48 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -58,19 +58,6 @@ std::ostream& operator<<(std::ostream&, const Command*) CVC5_EXPORT; std::ostream& operator<<(std::ostream&, const CommandStatus&) CVC5_EXPORT; std::ostream& operator<<(std::ostream&, const CommandStatus*) CVC5_EXPORT; -/** The status an SMT benchmark can have */ -enum BenchmarkStatus -{ - /** Benchmark is satisfiable */ - SMT_SATISFIABLE, - /** Benchmark is unsatisfiable */ - SMT_UNSATISFIABLE, - /** The status of the benchmark is unknown */ - SMT_UNKNOWN -}; /* enum BenchmarkStatus */ - -std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) CVC5_EXPORT; - /** * IOStream manipulator to print success messages or not. * diff --git a/src/theory/arith/linear/normal_form.cpp b/src/theory/arith/linear/normal_form.cpp index 41d6db897..90a96a874 100644 --- a/src/theory/arith/linear/normal_form.cpp +++ b/src/theory/arith/linear/normal_form.cpp @@ -35,38 +35,6 @@ Constant Constant::mkConstant(const Rational& rat) return Constant(nm->mkConstRealOrInt(rat)); } -size_t Variable::getComplexity() const{ - return 1u; -} - -size_t VarList::getComplexity() const{ - if(empty()){ - return 1; - }else if(singleton()){ - return 1; - }else{ - return size() + 1; - } -} - -size_t Monomial::getComplexity() const{ - return getConstant().getComplexity() + getVarList().getComplexity(); -} - -size_t Polynomial::getComplexity() const{ - size_t cmp = 0; - iterator i = begin(), e = end(); - for(; i != e; ++i){ - Monomial m = *i; - cmp += m.getComplexity(); - } - return cmp; -} - -size_t Constant::getComplexity() const{ - return getValue().complexity(); -} - bool Variable::isLeafMember(Node n){ return (!isRelationOperator(n.getKind())) && (Theory::isLeafOf(n, theory::THEORY_ARITH)); @@ -941,20 +909,6 @@ bool Comparison::rightIsConstant() const { return k == kind::CONST_RATIONAL || k == kind::CONST_INTEGER; } -size_t Comparison::getComplexity() const{ - switch(comparisonKind()){ - case kind::CONST_BOOLEAN: return 1; - case kind::LT: - case kind::LEQ: - case kind::DISTINCT: - case kind::EQUAL: - case kind::GT: - case kind::GEQ: - return getLeft().getComplexity() + getRight().getComplexity(); - default: Unhandled() << comparisonKind(); return -1; - } -} - Polynomial Comparison::getLeft() const { TNode left; Kind k = comparisonKind(); diff --git a/src/theory/arith/linear/normal_form.h b/src/theory/arith/linear/normal_form.h index 83a7fd536..1829a20f6 100644 --- a/src/theory/arith/linear/normal_form.h +++ b/src/theory/arith/linear/normal_form.h @@ -341,7 +341,6 @@ public: bool operator==(const Variable& v) const { return getNode() == v.getNode();} - size_t getComplexity() const; };/* class Variable */ class Constant : public NodeWrapper { @@ -429,8 +428,6 @@ public: return getValue().getNumerator().length(); } - size_t getComplexity() const; - };/* class Constant */ @@ -609,7 +606,6 @@ public: } return true; } - size_t getComplexity() const; private: bool isSorted(iterator start, iterator end); @@ -788,7 +784,6 @@ public: void print() const; static void printList(const std::vector& list); - size_t getComplexity() const; };/* class Monomial */ class SumPair; @@ -1130,8 +1125,6 @@ public: return getHead().getVarList(); } - size_t getComplexity() const; - friend class SumPair; friend class Comparison; @@ -1445,8 +1438,6 @@ public: return parse.isNormalForm(); } - size_t getComplexity() const; - SumPair toSumPair() const; Polynomial normalizedVariablePart() const; diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp index f0b01fe63..efc8b9f38 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp @@ -181,7 +181,7 @@ void InstMatchGeneratorMulti::processNewMatch(InstMatch& m, uint64_t& addedLemmas) { // see if these produce new matches - d_children_trie[fromChildIndex].addInstMatch(d_qstate, d_quant, m.get()); + d_children_trie[fromChildIndex].addInstMatch(d_quant, m.get()); // possibly only do the following if we know that new matches will be // produced? the issue is that instantiations are filtered in quantifiers // engine, and so there is no guarentee that diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp index b86e0aafc..ffb8932cc 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp @@ -38,29 +38,6 @@ InstStrategyUserPatterns::InstStrategyUserPatterns( } InstStrategyUserPatterns::~InstStrategyUserPatterns() {} -size_t InstStrategyUserPatterns::getNumUserGenerators(Node q) const -{ - std::map >::const_iterator it = - d_user_gen.find(q); - if (it == d_user_gen.end()) - { - return 0; - } - return it->second.size(); -} - -Trigger* InstStrategyUserPatterns::getUserGenerator(Node q, size_t i) const -{ - std::map >::const_iterator it = - d_user_gen.find(q); - if (it == d_user_gen.end()) - { - return nullptr; - } - Assert(i < it->second.size()); - return it->second[i]; -} - std::string InstStrategyUserPatterns::identify() const { return std::string("UserPatterns"); diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h index f6a43d550..f3c5f9a16 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h @@ -44,10 +44,6 @@ class InstStrategyUserPatterns : public InstStrategy ~InstStrategyUserPatterns(); /** add pattern */ void addUserPattern(Node q, Node pat); - /** get num patterns */ - size_t getNumUserGenerators(Node q) const; - /** get user pattern */ - inst::Trigger* getUserGenerator(Node q, size_t i) const; /** identify */ std::string identify() const override; diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp index 1244edc31..f0f1e6487 100644 --- a/src/theory/quantifiers/inst_match_trie.cpp +++ b/src/theory/quantifiers/inst_match_trie.cpp @@ -15,32 +15,22 @@ #include "theory/quantifiers/inst_match_trie.h" -#include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/quant_util.h" -#include "theory/quantifiers/quantifiers_state.h" -#include "theory/quantifiers/term_database.h" -#include "theory/uf/equality_engine_iterator.h" - using namespace cvc5::context; namespace cvc5::internal { namespace theory { namespace quantifiers { -bool InstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs, - Node q, +bool InstMatchTrie::existsInstMatch(Node q, const std::vector& m, - bool modEq, ImtIndexOrder* imtio, unsigned index) { - return !addInstMatch(qs, q, m, modEq, imtio, true, index); + return !addInstMatch(q, m, imtio, true, index); } -bool InstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs, - Node f, +bool InstMatchTrie::addInstMatch(Node f, const std::vector& m, - bool modEq, ImtIndexOrder* imtio, bool onlyExist, unsigned index) @@ -55,41 +45,15 @@ bool InstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs, std::map::iterator it = d_data.find(n); if (it != d_data.end()) { - bool ret = - it->second.addInstMatch(qs, f, m, modEq, imtio, onlyExist, index + 1); + bool ret = it->second.addInstMatch(f, m, imtio, onlyExist, index + 1); if (!onlyExist || !ret) { return ret; } } - if (modEq) - { - // check modulo equality if any other instantiation match exists - if (!n.isNull() && qs.hasTerm(n)) - { - eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine()); - while (!eqc.isFinished()) - { - Node en = (*eqc); - if (en != n) - { - std::map::iterator itc = d_data.find(en); - if (itc != d_data.end()) - { - if (itc->second.addInstMatch( - qs, f, m, modEq, imtio, true, index + 1)) - { - return false; - } - } - } - ++eqc; - } - } - } if (!onlyExist) { - d_data[n].addInstMatch(qs, f, m, modEq, imtio, false, index + 1); + d_data[n].addInstMatch(f, m, imtio, false, index + 1); } return true; } @@ -190,20 +154,16 @@ CDInstMatchTrie::~CDInstMatchTrie() } bool CDInstMatchTrie::existsInstMatch(context::Context* context, - quantifiers::QuantifiersState& qs, Node q, const std::vector& m, - bool modEq, unsigned index) { - return !addInstMatch(context, qs, q, m, modEq, index, true); + return !addInstMatch(context, q, m, index, true); } bool CDInstMatchTrie::addInstMatch(context::Context* context, - quantifiers::QuantifiersState& qs, Node f, const std::vector& m, - bool modEq, unsigned index, bool onlyExist) { @@ -228,45 +188,18 @@ bool CDInstMatchTrie::addInstMatch(context::Context* context, std::map::iterator it = d_data.find(n); if (it != d_data.end()) { - bool ret = - it->second->addInstMatch(context, qs, f, m, modEq, index + 1, onlyExist); + bool ret = it->second->addInstMatch(context, f, m, index + 1, onlyExist); if (!onlyExist || !ret) { return reset || ret; } } - if (modEq) - { - // check modulo equality if any other instantiation match exists - if (!n.isNull() && qs.hasTerm(n)) - { - eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine()); - while (!eqc.isFinished()) - { - Node en = (*eqc); - if (en != n) - { - std::map::iterator itc = d_data.find(en); - if (itc != d_data.end()) - { - if (itc->second->addInstMatch( - context, qs, f, m, modEq, index + 1, true)) - { - return false; - } - } - } - ++eqc; - } - } - } - if (!onlyExist) { CDInstMatchTrie* imt = new CDInstMatchTrie(context); Assert(d_data.find(n) == d_data.end()); d_data[n] = imt; - imt->addInstMatch(context, qs, f, m, modEq, index + 1, false); + imt->addInstMatch(context, f, m, index + 1, false); } return true; } @@ -356,20 +289,14 @@ void CDInstMatchTrie::print(std::ostream& out, Node q) const print(out, q, terms); } -bool InstMatchTrieOrdered::addInstMatch(quantifiers::QuantifiersState& qs, - Node q, - const std::vector& m, - bool modEq) +bool InstMatchTrieOrdered::addInstMatch(Node q, const std::vector& m) { - return d_imt.addInstMatch(qs, q, m, modEq, d_imtio); + return d_imt.addInstMatch(q, m, d_imtio); } -bool InstMatchTrieOrdered::existsInstMatch(quantifiers::QuantifiersState& qs, - Node q, - const std::vector& m, - bool modEq) +bool InstMatchTrieOrdered::existsInstMatch(Node q, const std::vector& m) { - return d_imt.existsInstMatch(qs, q, m, modEq, d_imtio); + return d_imt.existsInstMatch(q, m, d_imtio); } } // namespace quantifiers diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h index 903d6af19..a9c7ecc5a 100644 --- a/src/theory/quantifiers/inst_match_trie.h +++ b/src/theory/quantifiers/inst_match_trie.h @@ -56,13 +56,9 @@ class InstMatchTrie * This method considers the entry given by m, starting at the given index. * The domain of m is the bound variables of quantified formula q. * It returns true if (the suffix) of m exists in this trie. - * If modEq is true, we check for duplication modulo equality the current - * equalities in the equality engine of qs. */ - bool existsInstMatch(QuantifiersState& qs, - Node q, + bool existsInstMatch(Node q, const std::vector& m, - bool modEq = false, ImtIndexOrder* imtio = nullptr, unsigned index = 0); /** add inst match @@ -70,13 +66,9 @@ class InstMatchTrie * This method adds (the suffix of) m starting at the given index to this * trie, and returns true if and only if m did not already occur in this trie. * The domain of m is the bound variables of quantified formula q. - * If modEq is true, we check for duplication modulo equality the current - * equalities in the equality engine of qs. */ - bool addInstMatch(QuantifiersState& qs, - Node f, + bool addInstMatch(Node f, const std::vector& m, - bool modEq = false, ImtIndexOrder* imtio = nullptr, bool onlyExist = false, unsigned index = 0); @@ -128,30 +120,22 @@ class CDInstMatchTrie * This method considers the entry given by m, starting at the given index. * The domain of m is the bound variables of quantified formula q. * It returns true if (the suffix) of m exists in this trie. - * If modEq is true, we check for duplication modulo equality the current - * equalities in the equality engine of qs. * It additionally takes a context c, for which the entry is valid in. */ bool existsInstMatch(context::Context* context, - QuantifiersState& qs, Node q, const std::vector& m, - bool modEq = false, unsigned index = 0); /** add inst match * * This method adds (the suffix of) m starting at the given index to this * trie, and returns true if and only if m did not already occur in this trie. * The domain of m is the bound variables of quantified formula q. - * If modEq is true, we check for duplication modulo equality the current - * equalities in the equality engine of qs. * It additionally takes a context c, for which the entry is valid in. */ bool addInstMatch(context::Context* context, - QuantifiersState& qs, Node q, const std::vector& m, - bool modEq = false, unsigned index = 0, bool onlyExist = false); /** remove inst match @@ -201,23 +185,15 @@ class InstMatchTrieOrdered /** add match m for quantified formula q * * This method returns true if the match m was not previously added to this - * class. If modEq is true, we consider duplicates modulo the current - * equalities stored in the equality engine of qs. + * class. */ - bool addInstMatch(QuantifiersState& qs, - Node q, - const std::vector& m, - bool modEq = false); + bool addInstMatch(Node q, const std::vector& m); /** returns true if this trie contains m * * This method returns true if the match m exists in this - * class. If modEq is true, we consider duplicates modulo the current - * equalities stored in the equality engine of qs. + * class. */ - bool existsInstMatch(QuantifiersState& qs, - Node q, - const std::vector& m, - bool modEq = false); + bool existsInstMatch(Node q, const std::vector& m); private: /** the ordering */ diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 842357f68..97b4887a7 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -522,16 +522,14 @@ void Instantiate::recordInstantiation(Node q, d_recordedInst[q].push_back(inst); } -bool Instantiate::existsInstantiation(Node q, - const std::vector& terms, - bool modEq) +bool Instantiate::existsInstantiation(Node q, const std::vector& terms) { if (options().base.incrementalSolving) { std::map::iterator it = d_c_inst_match_trie.find(q); if (it != d_c_inst_match_trie.end()) { - return it->second->existsInstMatch(userContext(), d_qstate, q, terms, modEq); + return it->second->existsInstMatch(userContext(), q, terms); } } else @@ -539,7 +537,7 @@ bool Instantiate::existsInstantiation(Node q, std::map::iterator it = d_inst_match_trie.find(q); if (it != d_inst_match_trie.end()) { - return it->second.existsInstMatch(d_qstate, q, terms, modEq); + return it->second.existsInstMatch(q, terms); } } return false; @@ -624,10 +622,10 @@ bool Instantiate::recordInstantiationInternal(Node q, res.first->second = new CDInstMatchTrie(userContext()); } d_c_inst_match_trie_dom.insert(q); - return res.first->second->addInstMatch(userContext(), d_qstate, q, terms); + return res.first->second->addInstMatch(userContext(), q, terms); } Trace("inst-add-debug") << "Adding into inst trie" << std::endl; - return d_inst_match_trie[q].addInstMatch(d_qstate, q, terms); + return d_inst_match_trie[q].addInstMatch(q, terms); } bool Instantiate::removeInstantiationInternal(Node q, diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 81f0d8af5..1ceda50bc 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -209,11 +209,8 @@ class Instantiate : public QuantifiersUtil * * Returns true if and only if the instantiation already was added or * recorded by this class. - * modEq : whether to check for duplication modulo equality */ - bool existsInstantiation(Node q, - const std::vector& terms, - bool modEq = false); + bool existsInstantiation(Node q, const std::vector& terms); //--------------------------------------general utilities /** get instantiation * diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp index 8bb4ad4eb..9a970a342 100644 --- a/src/theory/quantifiers/quantifiers_state.cpp +++ b/src/theory/quantifiers/quantifiers_state.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/quantifiers_state.h" #include "options/quantifiers_options.h" +#include "theory/uf/equality_engine.h" #include "theory/uf/equality_engine_iterator.h" namespace cvc5::internal { @@ -120,39 +121,10 @@ void QuantifiersState::debugPrintEqualityEngine(const char* c) const std::map tnum; while (!eqcs_i.isFinished()) { - TNode r = (*eqcs_i); - TypeNode tr = r.getType(); - if (tnum.find(tr) == tnum.end()) - { - tnum[tr] = 0; - } - tnum[tr]++; - bool firstTime = true; - Trace(c) << " " << r; - Trace(c) << " : { "; - eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee); - while (!eqc_i.isFinished()) - { - TNode n = (*eqc_i); - if (r != n) - { - if (firstTime) - { - Trace(c) << std::endl; - firstTime = false; - } - Trace(c) << " " << n << std::endl; - } - ++eqc_i; - } - if (!firstTime) - { - Trace(c) << " "; - } - Trace(c) << "}" << std::endl; + tnum[(*eqcs_i).getType()]++; ++eqcs_i; } - Trace(c) << std::endl; + Trace(c) << ee->debugPrintEqc() << std::endl; for (const std::pair& t : tnum) { Trace(c) << "# eqc for " << t.first << " : " << t.second << std::endl; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 393bcc415..253159361 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -897,40 +897,6 @@ bool TheorySetsPrivate::isCareArg(Node n, unsigned a) return false; } -/******************** Model generation ********************/ -/******************** Model generation ********************/ -/******************** Model generation ********************/ - -namespace { -/** - * This function is a helper function to print sets as - * Set A = { a0, a1, a2, } - * instead of - * (union (singleton a0) (union (singleton a1) (singleton a2))) - */ -void traceSetElementsRecursively(stringstream& stream, const Node& set) -{ - Assert(set.getType().isSet()); - if (set.getKind() == SET_SINGLETON) - { - stream << set[0] << ", "; - } - if (set.getKind() == SET_UNION) - { - traceSetElementsRecursively(stream, set[0]); - traceSetElementsRecursively(stream, set[1]); - } -} - -std::string traceElements(const Node& set) -{ - std::stringstream stream; - traceSetElementsRecursively(stream, set); - return stream.str(); -} - -} // namespace - bool TheorySetsPrivate::collectModelValues(TheoryModel* m, const std::set& termSet) { @@ -1009,8 +975,7 @@ bool TheorySetsPrivate::collectModelValues(TheoryModel* m, m->assertSkeleton(el); } - Trace("sets-model") << "Set " << eqc << " = { " << traceElements(rep) - << " }" << std::endl; + Trace("sets-model") << "Set " << eqc << " = " << els << std::endl; } } diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index d3e87bda2..f8cbc65e8 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -59,13 +59,13 @@ void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int Node UfModelTreeNode::getFunctionValue(const std::vector& args, int index, - Node argDefaultValue, - bool simplify) + Node argDefaultValue) { if(!d_data.empty()) { Node defaultValue = argDefaultValue; if(d_data.find(Node::null()) != d_data.end()) { - defaultValue = d_data[Node::null()].getFunctionValue(args, index + 1, argDefaultValue, simplify); + defaultValue = d_data[Node::null()].getFunctionValue( + args, index + 1, argDefaultValue); } std::vector caseArgs; @@ -75,8 +75,7 @@ Node UfModelTreeNode::getFunctionValue(const std::vector& args, { if (!p.first.isNull()) { - Node val = - p.second.getFunctionValue(args, index + 1, defaultValue, simplify); + Node val = p.second.getFunctionValue(args, index + 1, defaultValue); caseArgs.push_back(p.first); caseValues[p.first] = val; } @@ -84,44 +83,19 @@ Node UfModelTreeNode::getFunctionValue(const std::vector& args, NodeManager* nm = NodeManager::currentNM(); Node retNode = defaultValue; - - if(!simplify) { - // "non-simplifying" mode - expand function values to things like: - // IF (x=0 AND y=0 AND z=0) THEN value1 - // ELSE IF (x=0 AND y=0 AND z=1) THEN value2 - // [...etc...] - for(int i = (int)caseArgs.size() - 1; i >= 0; --i) { - Node val = caseValues[ caseArgs[ i ] ]; - if(val.getKind() == ITE) { - // use a stack to reverse the order, since we're traversing outside-in - std::stack stk; - do { - stk.push(val); - val = val[2]; - } while(val.getKind() == ITE); - AlwaysAssert(val == defaultValue) - << "default values don't match when constructing function " - "definition!"; - while(!stk.empty()) { - val = stk.top(); - stk.pop(); - retNode = nm->mkNode(ITE, nm->mkNode(AND, args[index].eqNode(caseArgs[i]), val[0]), val[1], retNode); - } - } else { - retNode = nm->mkNode(ITE, args[index].eqNode(caseArgs[i]), caseValues[caseArgs[i]], retNode); - } - } - } else { - // "simplifying" mode - condense function values - for(int i = (int)caseArgs.size() - 1; i >= 0; --i) { - retNode = nm->mkNode(ITE, args[index].eqNode(caseArgs[i]), caseValues[caseArgs[i]], retNode); - } + // condense function values + for (size_t i = 0, cargs = caseArgs.size(); i < cargs; i++) + { + size_t ii = cargs - i - 1; + retNode = nm->mkNode(ITE, + args[index].eqNode(caseArgs[ii]), + caseValues[caseArgs[ii]], + retNode); } return retNode; - } else { - Assert(!d_value.isNull()); - return d_value; } + Assert(!d_value.isNull()); + return d_value; } //update function @@ -228,7 +202,7 @@ void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector Node UfModelTree::getFunctionValue(const std::vector& args, Rewriter* r) { - Node body = d_tree.getFunctionValue(args, 0, Node::null(), r != nullptr); + Node body = d_tree.getFunctionValue(args, 0, Node::null()); if (r != nullptr) { body = r->rewrite(body); diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 607bf2033..0f01a798a 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -48,8 +48,7 @@ public: /** getFunctionValue */ Node getFunctionValue(const std::vector& args, int index, - Node argDefaultValue, - bool simplify = true); + Node argDefaultValue); /** update function */ void update( TheoryModel* m ); /** simplify function */ -- 2.30.2