From 38988892041143d7f187af89f0d45126979278e7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 20 May 2022 12:49:57 -0500 Subject: [PATCH] More removing of unused code (#8806) --- src/CMakeLists.txt | 2 - .../arith/linear/theory_arith_private.cpp | 9 +- src/theory/arrays/union_find.cpp | 54 ------- src/theory/arrays/union_find.h | 140 ------------------ src/theory/engine_output_channel.cpp | 16 -- src/theory/engine_output_channel.h | 9 +- src/theory/inference_id.cpp | 1 + src/theory/inference_id.h | 2 + src/theory/output_channel.h | 6 - .../ematching/instantiation_engine.cpp | 2 + .../ematching/instantiation_engine.h | 5 +- src/theory/quantifiers/fmf/model_engine.cpp | 2 + src/theory/quantifiers/fmf/model_engine.h | 2 +- src/theory/quantifiers/inst_match_trie.cpp | 44 ------ src/theory/quantifiers/inst_match_trie.h | 17 --- src/theory/quantifiers/instantiate.cpp | 15 -- src/theory/quantifiers/instantiate.h | 2 - src/theory/quantifiers/sygus/synth_engine.cpp | 2 + src/theory/quantifiers/sygus/synth_engine.h | 2 +- 19 files changed, 23 insertions(+), 309 deletions(-) delete mode 100644 src/theory/arrays/union_find.cpp delete mode 100644 src/theory/arrays/union_find.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 023209605..52e3669c2 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -541,8 +541,6 @@ libcvc5_add_sources( theory/arrays/theory_arrays_type_rules.h theory/arrays/type_enumerator.h theory/arrays/type_enumerator.cpp - theory/arrays/union_find.cpp - theory/arrays/union_find.h theory/assertion.cpp theory/assertion.h theory/atom_requests.cpp diff --git a/src/theory/arith/linear/theory_arith_private.cpp b/src/theory/arith/linear/theory_arith_private.cpp index e97b32963..e58a7ce0a 100644 --- a/src/theory/arith/linear/theory_arith_private.cpp +++ b/src/theory/arith/linear/theory_arith_private.cpp @@ -1799,7 +1799,14 @@ void TheoryArithPrivate::outputPropagate(TNode lit) { void TheoryArithPrivate::outputRestart() { Trace("arith::channel") << "Arith restart!" << std::endl; - (d_containing.d_out)->demandRestart(); + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + Node restartVar = sm->mkDummySkolem( + "restartVar", + nm->booleanType(), + "A boolean variable asserted to be true to force a restart"); + d_containing.d_im.lemma( + restartVar, InferenceId::ARITH_DEMAND_RESTART, LemmaProperty::REMOVABLE); } bool TheoryArithPrivate::attemptSolveInteger(Theory::Effort effortLevel, bool emmmittedLemmaOrSplit){ diff --git a/src/theory/arrays/union_find.cpp b/src/theory/arrays/union_find.cpp deleted file mode 100644 index c42874a59..000000000 --- a/src/theory/arrays/union_find.cpp +++ /dev/null @@ -1,54 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Mathias Preiner - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Path-compressing, backtrackable union-find using an undo - * stack. Refactored from the UF union-find. - */ - -#include - -#include "expr/node.h" -#include "theory/arrays/union_find.h" - -using namespace std; - -namespace cvc5::internal { -namespace theory { -namespace arrays { - -template -void UnionFind::notify() { - Trace("arraysuf") << "arraysUF cancelling : " << d_offset << " < " << d_trace.size() << " ?" << endl; - while(d_offset < d_trace.size()) { - pair p = d_trace.back(); - if(p.second.isNull()) { - d_map.erase(p.first); - Trace("arraysuf") << "arraysUF " << d_trace.size() << " erasing " << p.first << endl; - } else { - d_map[p.first] = p.second; - Trace("arraysuf") << "arraysUF " << d_trace.size() << " replacing " << p << endl; - } - d_trace.pop_back(); - } - Trace("arraysuf") << "arraysUF cancelling finished." << endl; -} - -// The following declarations allow us to put functions in the .cpp file -// instead of the header, since we know which instantiations are needed. - -template void UnionFind>::notify(); - -template void UnionFind>::notify(); - -} // namespace arrays -} // namespace theory -} // namespace cvc5::internal diff --git a/src/theory/arrays/union_find.h b/src/theory/arrays/union_find.h deleted file mode 100644 index a449c2ea7..000000000 --- a/src/theory/arrays/union_find.h +++ /dev/null @@ -1,140 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Mathias Preiner, Aina Niemetz - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Path-compressing, backtrackable union-find using an undo - * stack. Refactored from the UF union-find. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__THEORY__ARRAYS__UNION_FIND_H -#define CVC5__THEORY__ARRAYS__UNION_FIND_H - -#include -#include -#include - -#include "expr/node.h" -#include "context/cdo.h" - -namespace cvc5::context { -class Context; -} - -namespace cvc5::internal { -namespace theory { -namespace arrays { - -// NodeType \in { Node, TNode } -template -class UnionFind : context::ContextNotifyObj -{ - /** Our underlying map type. */ - typedef std::unordered_map MapType; - - /** - * Our map of Nodes to their canonical representatives. - * If a Node is not present in the map, it is its own - * representative. - */ - MapType d_map; - - /** Our undo stack for changes made to d_map. */ - std::vector > d_trace; - - /** Our current offset in the d_trace stack (context-dependent). */ - context::CDO d_offset; - - public: - UnionFind(context::Context* ctxt) - : context::ContextNotifyObj(ctxt), d_offset(ctxt, 0) - { - } - - /** - * Return a Node's union-find representative, doing path compression. - */ - inline TNode find(TNode n); - - /** - * Return a Node's union-find representative, NOT doing path compression. - * This is useful for Assert() statements, debug checking, and similar - * things that you do NOT want to mutate the structure. - */ - inline TNode debugFind(TNode n) const; - - /** - * Set the canonical representative of n to newParent. They should BOTH - * be their own canonical representatives on entry to this funciton. - */ - inline void setCanon(TNode n, TNode newParent); - - /** - * Called by the Context when a pop occurs. Cancels everything to the - * current context level. Overrides ContextNotifyObj::notify(). - */ - void notify(); - -}; /* class UnionFind<> */ - -template -inline TNode UnionFind::debugFind(TNode n) const { - typename MapType::const_iterator i = d_map.find(n); - if(i == d_map.end()) { - return n; - } else { - return debugFind((*i).second); - } -} - -template -inline TNode UnionFind::find(TNode n) { - Trace("arraysuf") << "arraysUF find of " << n << std::endl; - typename MapType::iterator i = d_map.find(n); - if(i == d_map.end()) { - Trace("arraysuf") << "arraysUF it is rep" << std::endl; - return n; - } else { - Trace("arraysuf") << "arraysUF not rep: par is " << (*i).second << std::endl; - std::pair pr = *i; - // our iterator is invalidated by the recursive call to find(), - // since it mutates the map - TNode p = find(pr.second); - if(p == pr.second) { - return p; - } - d_trace.push_back(std::make_pair(n, pr.second)); - d_offset = d_trace.size(); - Trace("arraysuf") << "arraysUF setting canon of " << n << " : " << p << " @ " << d_trace.size() << std::endl; - pr.second = p; - d_map.insert(pr); - return p; - } -} - -template -inline void UnionFind::setCanon(TNode n, TNode newParent) { - Assert(d_map.find(n) == d_map.end()); - Assert(d_map.find(newParent) == d_map.end()); - if(n != newParent) { - Trace("arraysuf") << "arraysUF setting canon of " << n << " : " << newParent << " @ " << d_trace.size() << std::endl; - d_map[n] = newParent; - d_trace.push_back(std::make_pair(n, TNode::null())); - d_offset = d_trace.size(); - } -} - -} // namespace arrays -} // namespace theory -} // namespace cvc5::internal - -#endif /*CVC5__THEORY__ARRAYS__UNION_FIND_H */ diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp index 6995b9f75..784549d32 100644 --- a/src/theory/engine_output_channel.cpp +++ b/src/theory/engine_output_channel.cpp @@ -34,8 +34,6 @@ EngineOutputChannel::Statistics::Statistics(theory::TheoryId theory) + "lemmas")), requirePhase(smtStatisticsRegistry().registerInt(getStatsPrefix(theory) + "requirePhase")), - restartDemands(smtStatisticsRegistry().registerInt(getStatsPrefix(theory) - + "restartDemands")), trustedConflicts(smtStatisticsRegistry().registerInt( getStatsPrefix(theory) + "trustedConflicts")), trustedLemmas(smtStatisticsRegistry().registerInt(getStatsPrefix(theory) @@ -83,20 +81,6 @@ void EngineOutputChannel::conflict(TNode conflictNode) d_engine->conflict(tConf, d_theory); } -void EngineOutputChannel::demandRestart() -{ - NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); - Node restartVar = sm->mkDummySkolem( - "restartVar", - nm->booleanType(), - "A boolean variable asserted to be true to force a restart"); - Trace("theory::restart") << "EngineOutputChannel<" << d_theory - << ">::restart(" << restartVar << ")" << std::endl; - ++d_statistics.restartDemands; - lemma(restartVar, LemmaProperty::REMOVABLE); -} - void EngineOutputChannel::requirePhase(TNode n, bool phase) { Trace("theory") << "EngineOutputChannel::requirePhase(" << n << ", " << phase diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h index c24144c08..604ca2d94 100644 --- a/src/theory/engine_output_channel.h +++ b/src/theory/engine_output_channel.h @@ -53,8 +53,6 @@ class EngineOutputChannel : public theory::OutputChannel void lemma(TNode lemma, LemmaProperty p = LemmaProperty::NONE) override; - void demandRestart() override; - void requirePhase(TNode n, bool phase) override; void setIncomplete(IncompleteId id) override; @@ -85,10 +83,9 @@ class EngineOutputChannel : public theory::OutputChannel { public: Statistics(theory::TheoryId theory); - /** Number of calls to conflict, propagate, lemma, requirePhase, - * restartDemands */ - IntStat conflicts, propagations, lemmas, requirePhase, restartDemands, - trustedConflicts, trustedLemmas; + /** Number of calls to conflict, propagate, lemma, requirePhase */ + IntStat conflicts, propagations, lemmas, requirePhase, trustedConflicts, + trustedLemmas; }; /** The theory engine we're communicating with. */ TheoryEngine* d_engine; diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index fe4ff0efc..2c9c8eb04 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -57,6 +57,7 @@ const char* toString(InferenceId i) case InferenceId::ARITH_ROW_IMPL: return "ARITH_ROW_IMPL"; case InferenceId::ARITH_SPLIT_FOR_NL_MODEL: return "ARITH_SPLIT_FOR_NL_MODEL"; + case InferenceId::ARITH_DEMAND_RESTART: return "ARITH_DEMAND_RESTART"; case InferenceId::ARITH_PP_ELIM_OPERATORS: return "ARITH_PP_ELIM_OPERATORS"; case InferenceId::ARITH_PP_ELIM_OPERATORS_LEMMA: return "ARITH_PP_ELIM_OPERATORS_LEMMA"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index b56168e72..7ed9bfc26 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -94,6 +94,8 @@ enum class InferenceId // variables in a model, but those variables are inconsistent with assignments // from another theory ARITH_SPLIT_FOR_NL_MODEL, + // dummy lemma to demand a restart + ARITH_DEMAND_RESTART, //-------------------- preprocessing // equivalence of term and its preprocessed form ARITH_PP_ELIM_OPERATORS, diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 1a6827c17..5da23ee42 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -163,12 +163,6 @@ class OutputChannel { */ virtual void handleUserAttribute(const char* attr, Theory* t) {} - /** Demands that the search restart from sat search level 0. - * Using this leads to non-termination issues. - * It is appropriate for prototyping for theories. - */ - virtual void demandRestart() {} - //---------------------------- new proof /** * Let pconf be the pair (Node conf, ProofGenerator * pfg). This method diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index bf7a4eb05..bd1285aca 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -69,6 +69,8 @@ InstantiationEngine::InstantiationEngine(Env& env, InstantiationEngine::~InstantiationEngine() {} +std::string InstantiationEngine::identify() const { return "InstEngine"; } + void InstantiationEngine::presolve() { for( unsigned i=0; ipresolve(); diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index e91c25ad1..f71b2d1bc 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -47,16 +47,13 @@ class InstantiationEngine : public QuantifiersModule { bool checkCompleteFor(Node q) override; void checkOwnership(Node q) override; void registerQuantifier(Node q) override; - Node explain(TNode n) { return Node::null(); } /** add user pattern */ void addUserPattern(Node q, Node pat); void addUserNoPattern(Node q, Node pat); /** Identify this module */ - std::string identify() const override { return "InstEngine"; } + std::string identify() const override; private: - /** is the engine incomplete for this quantifier */ - bool isIncomplete(Node q); /** do instantiation round */ void doInstantiationRound(Theory::Effort effort); /** Return true if this module should process quantified formula q */ diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 641ac836f..5dc3ce955 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -51,6 +51,8 @@ ModelEngine::~ModelEngine() { } +std::string ModelEngine::identify() const { return "ModelEngine"; } + bool ModelEngine::needsCheck( Theory::Effort e ) { return e==Theory::EFFORT_LAST_CALL; } diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index 8f52ff8e7..74d0b9336 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -62,7 +62,7 @@ public: Node explain(TNode n) { return Node::null(); } void debugPrint(const char* c); /** Identify this module */ - std::string identify() const override { return "ModelEngine"; } + std::string identify() const override; private: /** Should we process quantified formula q? */ diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp index f0f1e6487..ccd932920 100644 --- a/src/theory/quantifiers/inst_match_trie.cpp +++ b/src/theory/quantifiers/inst_match_trie.cpp @@ -58,29 +58,6 @@ bool InstMatchTrie::addInstMatch(Node f, return true; } -bool InstMatchTrie::removeInstMatch(Node q, - const std::vector& m, - ImtIndexOrder* imtio, - unsigned index) -{ - Assert(index < q[0].getNumChildren()); - Assert(!imtio || index < imtio->d_order.size()); - unsigned i_index = imtio ? imtio->d_order[index] : index; - Node n = m[i_index]; - std::map::iterator it = d_data.find(n); - if (it != d_data.end()) - { - if ((index + 1) == q[0].getNumChildren() - || (imtio && (index + 1) == imtio->d_order.size())) - { - d_data.erase(n); - return true; - } - return it->second.removeInstMatch(q, m, imtio, index + 1); - } - return false; -} - void InstMatchTrie::print(std::ostream& out, Node q, std::vector& terms) const @@ -204,27 +181,6 @@ bool CDInstMatchTrie::addInstMatch(context::Context* context, return true; } -bool CDInstMatchTrie::removeInstMatch(Node q, - const std::vector& m, - unsigned index) -{ - if (index == q[0].getNumChildren()) - { - if (d_valid.get()) - { - d_valid.set(false); - return true; - } - return false; - } - std::map::iterator it = d_data.find(m[index]); - if (it != d_data.end()) - { - return it->second->removeInstMatch(q, m, index + 1); - } - return false; -} - void CDInstMatchTrie::print(std::ostream& out, Node q, std::vector& terms) const diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h index a9c7ecc5a..2f5475c6f 100644 --- a/src/theory/quantifiers/inst_match_trie.h +++ b/src/theory/quantifiers/inst_match_trie.h @@ -72,16 +72,6 @@ class InstMatchTrie ImtIndexOrder* imtio = nullptr, bool onlyExist = false, unsigned index = 0); - /** remove inst match - * - * This removes (the suffix of) m starting at the given index from this trie. - * It returns true if and only if this entry existed in this trie. - * The domain of m is the bound variables of quantified formula q. - */ - bool removeInstMatch(Node f, - const std::vector& m, - ImtIndexOrder* imtio = nullptr, - unsigned index = 0); /** * Adds the instantiations for q into insts. */ @@ -138,13 +128,6 @@ class CDInstMatchTrie const std::vector& m, unsigned index = 0, bool onlyExist = false); - /** remove inst match - * - * This removes (the suffix of) m starting at the given index from this trie. - * It returns true if and only if this entry existed in this trie. - * The domain of m is the bound variables of quantified formula q. - */ - bool removeInstMatch(Node q, const std::vector& m, unsigned index = 0); /** * Adds the instantiations for q into insts. */ diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 97b4887a7..1d9ef1dfe 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -628,21 +628,6 @@ bool Instantiate::recordInstantiationInternal(Node q, return d_inst_match_trie[q].addInstMatch(q, terms); } -bool Instantiate::removeInstantiationInternal(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->removeInstMatch(q, terms); - } - return false; - } - return d_inst_match_trie[q].removeInstMatch(q, terms); -} - void Instantiate::getInstantiatedQuantifiedFormulas(std::vector& qs) const { for (NodeInstListMap::const_iterator it = d_insts.begin(); diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 1ceda50bc..dca27c38a 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -297,8 +297,6 @@ class Instantiate : public QuantifiersUtil private: /** record instantiation, return true if it was not a duplicate */ bool recordInstantiationInternal(Node q, const std::vector& terms); - /** remove instantiation from the cache */ - bool removeInstantiationInternal(Node q, const std::vector& terms); /** * Ensure that n has type tn, return a term equivalent to it for that type * if possible. diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 44ca1ce9a..f3595a206 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -40,6 +40,8 @@ SynthEngine::SynthEngine(Env& env, SynthEngine::~SynthEngine() {} +std::string SynthEngine::identify() const { return "SynthEngine"; } + void SynthEngine::presolve() { Trace("sygus-engine") << "SynthEngine::presolve" << std::endl; diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index 95bcfc2ab..06b1d92ef 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -57,7 +57,7 @@ class SynthEngine : public QuantifiersModule /* Called for new quantifiers */ void registerQuantifier(Node q) override; /** Identify this module (for debugging, dynamic configuration, etc..) */ - std::string identify() const override { return "SynthEngine"; } + std::string identify() const override; /** get synth solutions * * This function adds entries to sol_map that map functions-to-synthesize -- 2.30.2