diff options
59 files changed, 97 insertions, 121 deletions
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 657298491..4c93e5727 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -171,7 +171,7 @@ bool DType::resolve(const std::map<std::string, TypeNode>& resolutions, d_involvesExt = false; d_involvesUt = false; - for (const std::shared_ptr<DTypeConstructor> ctor : d_constructors) + for (const std::shared_ptr<DTypeConstructor>& ctor : d_constructors) { if (ctor->involvesExternalType()) { diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp index 5c096767b..2bce4337e 100644 --- a/src/expr/lazy_proof_chain.cpp +++ b/src/expr/lazy_proof_chain.cpp @@ -40,7 +40,7 @@ const std::map<Node, std::shared_ptr<ProofNode>> LazyCDProofChain::getLinks() const { std::map<Node, std::shared_ptr<ProofNode>> links; - for (const std::pair<const Node, ProofGenerator*>& link : d_gens) + for (const std::pair<const Node, ProofGenerator* const>& link : d_gens) { Assert(link.second); std::shared_ptr<ProofNode> pfn = link.second->getProofFor(link.first); @@ -268,7 +268,7 @@ void LazyCDProofChain::addLazyStep(Node expected, std::shared_ptr<ProofNode> pfn = pg->getProofFor(expected); std::vector<Node> allowedLeaves{assumptions.begin(), assumptions.end()}; // add all current links in the chain - for (const std::pair<const Node, ProofGenerator*>& link : d_gens) + for (const std::pair<const Node, ProofGenerator* const>& link : d_gens) { allowedLeaves.push_back(link.first); } diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp index f82845fe3..283682ccd 100644 --- a/src/expr/symbol_manager.cpp +++ b/src/expr/symbol_manager.cpp @@ -227,9 +227,8 @@ void SymbolManager::Implementation::reset() // ---------------------------------------------- SymbolManager -SymbolManager::SymbolManager(api::Solver* s) - : d_solver(s), - d_implementation(new SymbolManager::Implementation()), +SymbolManager::SymbolManager() + : d_implementation(new SymbolManager::Implementation()), d_globalDeclarations(false) { } diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h index 06b01da8b..37dd51ef8 100644 --- a/src/expr/symbol_manager.h +++ b/src/expr/symbol_manager.h @@ -38,7 +38,7 @@ namespace CVC4 { class CVC4_PUBLIC SymbolManager { public: - SymbolManager(api::Solver* s); + SymbolManager(); ~SymbolManager(); /** Get the underlying symbol table */ SymbolTable* getSymbolTable(); @@ -136,8 +136,6 @@ class CVC4_PUBLIC SymbolManager bool getGlobalDeclarations() const; private: - /** The API Solver object. */ - api::Solver* d_solver; /** * The declaration scope that is "owned" by this symbol manager. */ diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index b1a7c70b5..d99cd8df8 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -50,7 +50,7 @@ void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString CommandExecutor::CommandExecutor(Options& options) : d_solver(new api::Solver(&options)), - d_symman(new SymbolManager(d_solver.get())), + d_symman(new SymbolManager()), d_smtEngine(d_solver->getSmtEngine()), d_options(options), d_stats("driver"), diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index fe37e9363..ceef3ae4a 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -67,7 +67,7 @@ void throwLazyBBUnsupported(options::SatSolverMode m) } // namespace -OptionsHandler::OptionsHandler(Options* options) : d_options(options) { } +OptionsHandler::OptionsHandler() {} unsigned long OptionsHandler::limitHandler(std::string option, std::string optarg) diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 07e629976..847bc9e10 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -42,10 +42,11 @@ namespace options { */ class OptionsHandler { public: - OptionsHandler(Options* options); + OptionsHandler(); - void unsignedGreater0(const std::string& option, unsigned value) { - options::greater(0)(option, value); + void unsignedGreater0(const std::string& option, unsigned value) + { + options::greater(0)(option, value); } void unsignedLessEqual2(const std::string& option, unsigned value) { @@ -114,9 +115,6 @@ public: private: - /** Pointer to the containing Options object.*/ - Options* d_options; - /* Help strings */ static const std::string s_instFormatHelp; diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index af74fd31e..c1b814895 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -225,7 +225,7 @@ void runBoolPredicates(T, std::string option, bool b, options::OptionsHandler* h Options::Options(OptionsListener* ol) : d_holder(new options::OptionsHolder()), - d_handler(new options::OptionsHandler(this)), + d_handler(new options::OptionsHandler()), d_olisten(ol) {} diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 6eb3d8061..c3deabbb7 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -88,7 +88,7 @@ namespace CVC4 { class Term; class Sort; } - + }/* CVC4 namespace */ }/* @parser::includes */ diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp index 89fbe786d..cf2635172 100644 --- a/src/printer/dagification_visitor.cpp +++ b/src/printer/dagification_visitor.cpp @@ -59,7 +59,7 @@ bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) { // search for variables that start with the let prefix std::unordered_set<TNode, TNodeHashFunction> vs; expr::getVariables(current, vs); - for (const TNode v : vs) + for (const TNode& v : vs) { const std::string name = v.getAttribute(expr::VarNameAttr()); if (name.compare(0, d_letVarPrefix.size(), d_letVarPrefix) == 0) diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index fa31eb41c..90368ac15 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -271,16 +271,17 @@ MinisatSatSolver::Statistics::~Statistics() { d_registry->unregisterStat(&d_statTotLiterals); } -void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){ - d_statStarts.setData(d_minisat->starts); - d_statDecisions.setData(d_minisat->decisions); - d_statRndDecisions.setData(d_minisat->rnd_decisions); - d_statPropagations.setData(d_minisat->propagations); - d_statConflicts.setData(d_minisat->conflicts); - d_statClausesLiterals.setData(d_minisat->clauses_literals); - d_statLearntsLiterals.setData(d_minisat->learnts_literals); - d_statMaxLiterals.setData(d_minisat->max_literals); - d_statTotLiterals.setData(d_minisat->tot_literals); +void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat) +{ + d_statStarts.setData(minisat->starts); + d_statDecisions.setData(minisat->decisions); + d_statRndDecisions.setData(minisat->rnd_decisions); + d_statPropagations.setData(minisat->propagations); + d_statConflicts.setData(minisat->conflicts); + d_statClausesLiterals.setData(minisat->clauses_literals); + d_statLearntsLiterals.setData(minisat->learnts_literals); + d_statMaxLiterals.setData(minisat->max_literals); + d_statTotLiterals.setData(minisat->tot_literals); } } /* namespace CVC4::prop */ diff --git a/src/prop/proof_post_processor.cpp b/src/prop/proof_post_processor.cpp index 441805758..555d72300 100644 --- a/src/prop/proof_post_processor.cpp +++ b/src/prop/proof_post_processor.cpp @@ -21,8 +21,8 @@ namespace CVC4 { namespace prop { ProofPostprocessCallback::ProofPostprocessCallback( - ProofNodeManager* pnm, ProofCnfStream* proofCnfStream) - : d_pnm(pnm), d_proofCnfStream(proofCnfStream) + ProofCnfStream* proofCnfStream) + : d_proofCnfStream(proofCnfStream) { } @@ -88,7 +88,7 @@ bool ProofPostprocessCallback::update(Node res, ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm, ProofCnfStream* proofCnfStream) - : d_cb(pnm, proofCnfStream), d_pnm(pnm) + : d_cb(proofCnfStream), d_pnm(pnm) { } diff --git a/src/prop/proof_post_processor.h b/src/prop/proof_post_processor.h index ced3e5b92..18ae8073e 100644 --- a/src/prop/proof_post_processor.h +++ b/src/prop/proof_post_processor.h @@ -36,8 +36,7 @@ namespace prop { class ProofPostprocessCallback : public ProofNodeUpdaterCallback { public: - ProofPostprocessCallback(ProofNodeManager* pnm, - ProofCnfStream* proofCnfStream); + ProofPostprocessCallback(ProofCnfStream* proofCnfStream); ~ProofPostprocessCallback() {} /** * Initialize, called once for each new ProofNode to process. This initializes @@ -72,8 +71,6 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback bool& continueUpdate) override; private: - /** The proof node manager */ - ProofNodeManager* d_pnm; /** The cnf stream proof generator */ ProofCnfStream* d_proofCnfStream; //---------------------------------reset at the begining of each update diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp index aa58ffa2c..00cd96b01 100644 --- a/src/prop/prop_proof_manager.cpp +++ b/src/prop/prop_proof_manager.cpp @@ -23,8 +23,7 @@ PropPfManager::PropPfManager(context::UserContext* userContext, ProofNodeManager* pnm, SatProofManager* satPM, ProofCnfStream* cnfProof) - : d_pnm(pnm), - d_pfpp(new ProofPostproccess(pnm, cnfProof)), + : d_pfpp(new ProofPostproccess(pnm, cnfProof)), d_satPM(satPM), d_assertions(userContext) { diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h index f3deee5bc..2696b2bda 100644 --- a/src/prop/prop_proof_manager.h +++ b/src/prop/prop_proof_manager.h @@ -73,8 +73,6 @@ class PropPfManager void checkProof(context::CDList<Node>* assertions); private: - /** A node manager */ - ProofNodeManager* d_pnm; /** The proof post-processor */ std::unique_ptr<prop::ProofPostproccess> d_pfpp; /** diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index e3cbea152..8b6ca3021 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -39,7 +39,7 @@ namespace smt { class Assertions; class SmtEngineState; class Preprocessor; -class SmtEngineStatistics; +struct SmtEngineStatistics; /** * A solver for SMT queries. diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index ea0739235..2c3c55f45 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -29,6 +29,7 @@ namespace theory { namespace arith { namespace nl { +#ifdef CVC4_POLY_IMP CadSolver::CadSolver(InferenceManager& im, NlModel& model) : d_foundSatisfiability(false), d_im(im), d_model(model) { @@ -38,6 +39,9 @@ CadSolver::CadSolver(InferenceManager& im, NlModel& model) "", NodeManager::SKOLEM_EXACT_NAME); } +#else +CadSolver::CadSolver(InferenceManager& im, NlModel& model) {} +#endif CadSolver::~CadSolver() {} diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h index 4d537213f..344b0bb12 100644 --- a/src/theory/arith/nl/cad_solver.h +++ b/src/theory/arith/nl/cad_solver.h @@ -71,17 +71,17 @@ class CadSolver bool constructModelIfAvailable(std::vector<Node>& assertions); private: +#ifdef CVC4_POLY_IMP /** * The variable used to encode real algebraic numbers to nodes. */ Node d_ranVariable; -#ifdef CVC4_POLY_IMP /** * The object implementing the actual decision procedure. */ cad::CDCAC d_CAC; -#endif + /** * Indicates whether we found satisfiability in the last call to * checkFullRefine. @@ -92,6 +92,7 @@ class CadSolver InferenceManager& d_im; /** Reference to the non-linear model object */ NlModel& d_model; +#endif }; /* class CadSolver */ } // namespace nl diff --git a/src/theory/arith/nl/iand_table.cpp b/src/theory/arith/nl/iand_table.cpp index 050e6baed..e9a812e25 100644 --- a/src/theory/arith/nl/iand_table.cpp +++ b/src/theory/arith/nl/iand_table.cpp @@ -191,7 +191,8 @@ void IAndTable::addDefaultValue( { counters[i] = 0; } - for (const std::pair<std::pair<int64_t, int64_t>, uint64_t>& element : table) + for (const std::pair<const std::pair<int64_t, int64_t>, uint64_t>& element : + table) { uint64_t result = element.second; counters[result]++; diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 22a69cadb..9abe11afe 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -38,7 +38,6 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, eq::EqualityEngine* ee) : d_containing(containing), d_im(containing.getInferenceManager()), - d_ee(ee), d_needsLastCall(false), d_checkCounter(0), d_extTheoryCb(ee), diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index b563384a5..89370608a 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -226,8 +226,6 @@ class NonlinearExtension // The theory of arithmetic containing this extension. TheoryArith& d_containing; InferenceManager& d_im; - // pointer to used equality engine - eq::EqualityEngine* d_ee; /** The statistics class */ NlStats d_stats; // needs last call effort diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 3e59aebe6..efc2eb3fe 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1752,7 +1752,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) Trace("arrays-crl")<<"Arrays::checkLemmas done.\n"; } -void TheoryArrays::propagate(RowLemmaType lem) +void TheoryArrays::propagateLemma(RowLemmaType lem) { Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. options::arraysPropagate() = " << options::arraysPropagate() << std::endl; @@ -1839,7 +1839,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) // If propagating, check propagations int prop = options::arraysPropagate(); if (prop > 0) { - propagate(lem); + propagateLemma(lem); } // Prefer equality between indexes so as not to introduce new read terms @@ -1969,7 +1969,7 @@ bool TheoryArrays::dischargeLemmas() int prop = options::arraysPropagate(); if (prop > 0) { - propagate(l); + propagateLemma(l); if (d_state.isInConflict()) { return true; diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 5236324bc..87b629067 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -442,7 +442,7 @@ class TheoryArrays : public Theory { void checkStore(TNode a); void checkRowForIndex(TNode i, TNode a); void checkRowLemmas(TNode a, TNode b); - void propagate(RowLemmaType lem); + void propagateLemma(RowLemmaType lem); void queueRowLemma(RowLemmaType lem); bool dischargeLemmas(); diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp index 4d18ad926..4e5242c8a 100644 --- a/src/theory/bags/inference_manager.cpp +++ b/src/theory/bags/inference_manager.cpp @@ -24,7 +24,7 @@ namespace bags { InferenceManager::InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, s, pnm), d_state(s) + : InferenceManagerBuffered(t, s, pnm) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h index 4b4edbaef..dc641e86f 100644 --- a/src/theory/bags/inference_manager.h +++ b/src/theory/bags/inference_manager.h @@ -42,12 +42,6 @@ class InferenceManager : public InferenceManagerBuffered /** constants */ Node d_true; Node d_false; - /** - * Reference to the state object for the theory of bags. We store the - * (derived) state here, since it has additional methods required in this - * class. - */ - SolverState& d_state; }; } // namespace bags diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp index 60beef29f..e30444bd7 100644 --- a/src/theory/bags/term_registry.cpp +++ b/src/theory/bags/term_registry.cpp @@ -21,10 +21,8 @@ namespace CVC4 { namespace theory { namespace bags { -TermRegistry::TermRegistry(SolverState& state, InferenceManager& im) - : d_im(im), - d_proxy(state.getUserContext()), - d_proxy_to_term(state.getUserContext()) +TermRegistry::TermRegistry(SolverState& state) + : d_proxy(state.getUserContext()), d_proxy_to_term(state.getUserContext()) { } diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h index d284126ee..79d575425 100644 --- a/src/theory/bags/term_registry.h +++ b/src/theory/bags/term_registry.h @@ -37,7 +37,7 @@ class TermRegistry typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap; public: - TermRegistry(SolverState& state, InferenceManager& im); + TermRegistry(SolverState& state); /** * Returns the existing empty bag for type tn @@ -46,8 +46,6 @@ class TermRegistry Node getEmptyBag(TypeNode tn); private: - /** The inference manager */ - InferenceManager& d_im; /** Map from bag terms to their proxy variables */ NodeMap d_proxy; /** Backwards map of above */ diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp index bc4e0c8ae..7370d3816 100644 --- a/src/theory/booleans/proof_circuit_propagator.cpp +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -426,7 +426,6 @@ ProofCircuitPropagatorForward::ProofCircuitPropagatorForward( ProofNodeManager* pnm, Node child, bool childAssignment, Node parent) : ProofCircuitPropagator{pnm}, d_child(child), - d_childAssignment(childAssignment), d_parent(parent) { } diff --git a/src/theory/booleans/proof_circuit_propagator.h b/src/theory/booleans/proof_circuit_propagator.h index cc0aaad36..cebe3d751 100644 --- a/src/theory/booleans/proof_circuit_propagator.h +++ b/src/theory/booleans/proof_circuit_propagator.h @@ -200,8 +200,6 @@ class ProofCircuitPropagatorForward : public ProofCircuitPropagator private: /** The current child that triggered the propagations */ Node d_child; - /** The assignment of d_child */ - bool d_childAssignment; /** The parent node used for propagation */ Node d_parent; }; diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index dbee65d8c..4f42217aa 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -142,7 +142,10 @@ Node mkAnd(const std::vector<NodeTemplate<ref_count>>& conjunctions) if (all.size() == 1) { return conjunctions[0]; } NodeBuilder<> conjunction(kind::AND); - for (const Node& n : all) { conjunction << n; } + for (const TNode& n : all) + { + conjunction << n; + } return conjunction; } @@ -161,7 +164,10 @@ Node mkOr(const std::vector<NodeTemplate<ref_count>>& nodes) if (all.size() == 1) { return nodes[0]; } NodeBuilder<> disjunction(kind::OR); - for (const Node& n : all) { disjunction << n; } + for (const TNode& n : all) + { + disjunction << n; + } return disjunction; } /* Create node of kind XOR. */ diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index fde28fd26..18b75e631 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -1196,7 +1196,7 @@ void SygusExtension::registerSymBreakLemma( TypeNode tn, Node lem, unsigned sz, sca.d_search_terms[tn].find(d); if (itt != sca.d_search_terms[tn].end()) { - for (const TNode& t : itt->second) + for (const Node& t : itt->second) { if (!options::sygusSymBreakLazy() || d_active_terms.find(t) != d_active_terms.end()) @@ -1469,7 +1469,7 @@ void SygusExtension::incrementCurrentSearchSize( Node m, std::vector< Node >& le int new_depth = ((int)itsz->second->d_curr_search_size) - ((int)sz); std::map< unsigned, std::vector< Node > >::iterator itt = itc->second.d_search_terms[tn].find( new_depth ); if( itt!=itc->second.d_search_terms[tn].end() ){ - for (const TNode& t : itt->second) + for (const Node& t : itt->second) { if (!options::sygusSymBreakLazy() || (d_active_terms.find(t) != d_active_terms.end() diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index eeaa678d4..e13902077 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -905,7 +905,7 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in d_conj_count++; }else{ std::vector< Node > bvs; - for (const std::pair<TypeNode, unsigned>& lhs_pattern : + for (const std::pair<const TypeNode, unsigned>& lhs_pattern : d_pattern_var_id[lhs]) { for (unsigned j = 0; j <= lhs_pattern.second; j++) diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 6d7275fac..e62f1dbdf 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1200,7 +1200,7 @@ bool QuantifiersRewriter::getVarElimIneq(Node body, std::vector<Node> inactive_vars; std::map<Node, std::map<int, bool> > visited; std::map<Node, int> exclude; - for (const std::pair<Node, bool>& pr : qpr.d_phase_reqs) + for (const std::pair<const Node, bool>& pr : qpr.d_phase_reqs) { if (pr.first.getKind() == GEQ) { @@ -1274,7 +1274,7 @@ bool QuantifiersRewriter::getVarElimIneq(Node body, } while (!evisit.empty() && !elig_vars.empty()); bool ret = false; - for (const std::pair<Node, bool>& ev : elig_vars) + for (const std::pair<const Node, bool>& ev : elig_vars) { Node v = ev.first; Trace("var-elim-ineq-debug") diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp index 55beea4ca..79891cb42 100644 --- a/src/theory/quantifiers/query_generator.cpp +++ b/src/theory/quantifiers/query_generator.cpp @@ -83,7 +83,7 @@ bool QueryGenerator::addTerm(Node n, std::ostream& out) } if (threshCount < 2) { - for (const std::pair<Node, std::vector<unsigned>>& etp : ev_to_pt) + for (const std::pair<const Node, std::vector<unsigned>>& etp : ev_to_pt) { if (etp.second.size() < d_deqThresh) { diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index 098af62a7..360476399 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -88,7 +88,7 @@ void EnumStreamPermutation::reset(Node value) d_var_classes[ti.getSubclassForVar(var)].push_back(var); } } - for (const std::pair<unsigned, std::vector<Node>>& p : d_var_classes) + for (const std::pair<const unsigned, std::vector<Node>>& p : d_var_classes) { d_perm_state_class.push_back(PermutationState(p.second)); if (Trace.isOn("synth-stream-concrete")) @@ -383,7 +383,7 @@ void EnumStreamSubstitution::resetValue(Node value) d_curr_ind = 0; d_comb_state_class.clear(); Trace("synth-stream-concrete") << " ..combining vars :"; - for (const std::pair<unsigned, std::vector<Node>>& p : d_var_classes) + for (const std::pair<const unsigned, std::vector<Node>>& p : d_var_classes) { // ignore classes without variables being permuted unsigned perm_var_class_sz = d_stream_permutations.getVarClassSize(p.first); diff --git a/src/theory/quantifiers/sygus/example_infer.cpp b/src/theory/quantifiers/sygus/example_infer.cpp index a2f388cb8..eae5a79e8 100644 --- a/src/theory/quantifiers/sygus/example_infer.cpp +++ b/src/theory/quantifiers/sygus/example_infer.cpp @@ -24,10 +24,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -ExampleInfer::ExampleInfer(TermDbSygus* tds) : d_tds(tds) -{ - d_isExamples = false; -} +ExampleInfer::ExampleInfer() { d_isExamples = false; } ExampleInfer::~ExampleInfer() {} diff --git a/src/theory/quantifiers/sygus/example_infer.h b/src/theory/quantifiers/sygus/example_infer.h index 88d3ebc6d..79a70b15e 100644 --- a/src/theory/quantifiers/sygus/example_infer.h +++ b/src/theory/quantifiers/sygus/example_infer.h @@ -41,7 +41,7 @@ namespace quantifiers { class ExampleInfer { public: - ExampleInfer(TermDbSygus* tds); + ExampleInfer(); ~ExampleInfer(); /** initialize * @@ -112,8 +112,6 @@ class ExampleInfer std::unordered_set<Node, NodeHashFunction>>& visited, bool hasPol, bool pol); - /** Pointer to the sygus term database */ - TermDbSygus* d_tds; /** is this an examples conjecture for all functions-to-synthesize? */ bool d_isExamples; /** diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp index 1a92cfc7f..d2fb68586 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp @@ -25,7 +25,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SygusQePreproc::SygusQePreproc(QuantifiersEngine* qe) {} +SygusQePreproc::SygusQePreproc() {} Node SygusQePreproc::preprocess(Node q) { diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h index daee1762f..545b35af0 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h @@ -40,17 +40,13 @@ namespace quantifiers { class SygusQePreproc { public: - SygusQePreproc(QuantifiersEngine* qe); + SygusQePreproc(); ~SygusQePreproc() {} /** * Preprocess. Returns a lemma of the form q = nq where nq is obtained * by the quantifier elimination technique outlined above. */ Node preprocess(Node q); - - private: - /** Pointer to quantifiers engine */ - QuantifiersEngine* d_quantEngine; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index b8700f7f6..6135015db 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -53,7 +53,7 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe, d_ceg_proc(new SynthConjectureProcess(qe)), d_ceg_gc(new CegGrammarConstructor(qe, this)), d_sygus_rconst(new SygusRepairConst(qe)), - d_exampleInfer(new ExampleInfer(d_tds)), + d_exampleInfer(new ExampleInfer()), d_ceg_pbe(new SygusPbe(qe, this)), d_ceg_cegis(new Cegis(qe, this)), d_ceg_cegisUnif(new CegisUnif(qe, this)), diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 3e40d6654..cc82164b2 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -34,7 +34,7 @@ SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c) : QuantifiersModule(qe), d_tds(qe->getTermDatabaseSygus()), d_conj(nullptr), - d_sqp(qe) + d_sqp() { d_conjs.push_back(std::unique_ptr<SynthConjecture>( new SynthConjecture(d_quantEngine, d_statistics))); diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 92754ebfe..22c2ac142 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -126,7 +126,7 @@ void SygusSampler::initializeSygus(TermDbSygus* tds, { TypeNode svt = sv.getType(); // is it equivalent to a previous variable? - for (const std::pair<Node, unsigned>& v : var_to_type_id) + for (const std::pair<const Node, unsigned>& v : var_to_type_id) { Node svc = v.first; if (svc.getType() == svt) diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 42677fa3f..332230613 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -276,14 +276,14 @@ void TermDb::computeUfEqcTerms( TNode f ) { ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end()); } eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); - for (const Node& ff : ops) + for (const TNode& ff : ops) { - for (const TNode& n : d_op_map[ff]) + for (const Node& n : d_op_map[ff]) { if (hasTermCurrent(n) && isTermActive(n)) { computeArgReps(n); - TNode r = ee->hasTerm(n) ? ee->getRepresentative(n) : n; + TNode r = ee->hasTerm(n) ? ee->getRepresentative(n) : TNode(n); d_func_map_eqc_trie[f].d_data[r].addTerm(n, d_arg_reps[n]); } } @@ -312,7 +312,7 @@ void TermDb::computeUfTerms( TNode f ) { unsigned relevantCount = 0; eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); NodeManager* nm = NodeManager::currentNM(); - for (const Node& ff : ops) + for (const TNode& ff : ops) { std::map<Node, std::vector<Node> >::iterator it = d_op_map.find(ff); if (it == d_op_map.end()) diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 4a7f4367e..383d3d16d 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -755,7 +755,8 @@ void TheorySep::postCheck(Effort level) // get model values std::map<int, Node> mvals; - for (const std::pair<int, Node>& sub_element : d_label_map[satom][slbl]) + for (const std::pair<const int, Node>& sub_element : + d_label_map[satom][slbl]) { int sub_index = sub_element.first; Node sub_lbl = sub_element.second; diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index cb0540b86..228f2cd3f 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -165,7 +165,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t) const std::map<Node, Node>& negativeMembers = d_state.getNegativeMembers(representative); - for (const std::pair<Node, Node>& negativeMember : negativeMembers) + for (const std::pair<const Node, Node>& negativeMember : negativeMembers) { Node member = nm->mkNode(MEMBER, negativeMember.first, univ); // negativeMember.second is the reason for the negative membership and diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index e44c3c7a6..d435c641c 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1163,7 +1163,8 @@ bool TheorySetsPrivate::collectModelValues(TheoryModel* m, { const std::map<TypeNode, std::vector<TNode> >& slackElements = d_cardSolver->getFiniteTypeSlackElements(); - for (const std::pair<TypeNode, std::vector<TNode> >& pair : slackElements) + for (const std::pair<const TypeNode, std::vector<TNode> >& pair : + slackElements) { const std::vector<Node>& members = d_cardSolver->getFiniteTypeMembers(pair.first); diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index edd00c954..48116bc24 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -2575,7 +2575,7 @@ bool CoreSolver::processInferInfo(CoreInferInfo& cii) addNormalFormPair(cii.d_nfPair[0], cii.d_nfPair[1]); } // send phase requirements - for (const std::pair<const Node, bool> pp : cii.d_pendingPhase) + for (const std::pair<const Node, bool>& pp : cii.d_pendingPhase) { Node ppr = Rewriter::rewrite(pp.first); d_im.addPendingPhaseRequirement(ppr, pp.second); diff --git a/src/theory/strings/normal_form.cpp b/src/theory/strings/normal_form.cpp index 7724b5137..7fdf3ff76 100644 --- a/src/theory/strings/normal_form.cpp +++ b/src/theory/strings/normal_form.cpp @@ -61,9 +61,9 @@ void NormalForm::splitConstant(unsigned index, Node c1, Node c2) // notice this is not critical for soundness: not doing the below incrementing // will only lead to overapproximating when antecedants are required in // explanations - for (const std::pair<Node, std::map<bool, unsigned> >& pe : d_expDep) + for (const std::pair<const Node, std::map<bool, unsigned> >& pe : d_expDep) { - for (const std::pair<bool, unsigned>& pep : pe.second) + for (const std::pair<const bool, unsigned>& pep : pe.second) { // See if this can be incremented: it can if this literal is not relevant // to the current index, and hence it is not relevant for both c1 and c2. diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index e771f8bb8..450b319c9 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1869,7 +1869,7 @@ theory::TrustNode TheoryEngine::getExplanation( if (Trace.isOn("te-proof-exp")) { Trace("te-proof-exp") << "Explanation is:" << std::endl; - for (const Node& e : exp) + for (const TNode& e : exp) { Trace("te-proof-exp") << " " << e << std::endl; } diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp index aaa3b44f7..903627794 100644 --- a/src/theory/trust_substitutions.cpp +++ b/src/theory/trust_substitutions.cpp @@ -26,7 +26,6 @@ TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c, MethodId ids) : d_ctx(c), d_subs(c), - d_pnm(pnm), d_tsubs(c), d_tspb(pnm ? new TheoryProofStepBuffer(pnm->getChecker()) : nullptr), d_subsPg( diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h index c316f08c5..26d152194 100644 --- a/src/theory/trust_substitutions.h +++ b/src/theory/trust_substitutions.h @@ -98,8 +98,6 @@ class TrustSubstitutionMap context::Context* d_ctx; /** The substitution map */ SubstitutionMap d_subs; - /** The proof node manager */ - ProofNodeManager* d_pnm; /** A context-dependent list of trust nodes */ context::CDList<TrustNode> d_tsubs; /** Theory proof step buffer */ diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index f04ebbb60..637cd05b7 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -1286,7 +1286,7 @@ void EqualityEngine::explainLit(TNode lit, std::vector<TNode>& assumptions) explainPredicate(atom, polarity, tassumptions); } // ensure that duplicates are removed - for (const TNode a : tassumptions) + for (const TNode& a : tassumptions) { if (std::find(assumptions.begin(), assumptions.end(), a) == assumptions.end()) diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index 6377f78b6..529179bbb 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -518,7 +518,7 @@ void ProofEqEngine::explainWithProof(Node lit, } Trace("pfee-proof") << "...got " << tassumps << std::endl; // avoid duplicates - for (const TNode a : tassumps) + for (const TNode& a : tassumps) { if (a == lit) { diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index c4d6c9c82..ea87eff2b 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -594,7 +594,7 @@ bool SymmetryBreaker::invariantByPermutations(const Permutation& p) { subs.push_back(p1); repls.push_back(p1); repls.push_back(p0); - for (const Node nn : d_phi) + for (const Node& nn : d_phi) { Node s = nn.substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); @@ -629,7 +629,7 @@ bool SymmetryBreaker::invariantByPermutations(const Permutation& p) { subs.clear(); repls.clear(); bool first = true; - for (const Node& nn : p) + for (const TNode& nn : p) { subs.push_back(nn); if(!first) { diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp index efca53ab3..71048ffe4 100644 --- a/test/api/ouroborous.cpp +++ b/test/api/ouroborous.cpp @@ -111,7 +111,7 @@ void runTestString(std::string instr, InputLanguage instrlang = input::LANG_SMTL int runTest() { std::unique_ptr<api::Solver> solver = std::unique_ptr<api::Solver>(new api::Solver()); - std::unique_ptr<SymbolManager> symman(new SymbolManager(solver.get())); + std::unique_ptr<SymbolManager> symman(new SymbolManager()); psr = ParserBuilder(solver.get(), symman.get(), "internal-buffer") .withStringInput(declarations) .withInputLanguage(input::LANG_SMTLIB_V2) diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp index 3738bd1b6..a7e62e078 100644 --- a/test/api/smt2_compliance.cpp +++ b/test/api/smt2_compliance.cpp @@ -60,7 +60,7 @@ int main() void testGetInfo(api::Solver* solver, const char* s) { - std::unique_ptr<SymbolManager> symman(new SymbolManager(solver)); + std::unique_ptr<SymbolManager> symman(new SymbolManager()); ParserBuilder pb(solver, symman.get(), "<internal>", solver->getOptions()); Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build(); diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h index df6a79bd8..7a003c6c6 100644 --- a/test/unit/main/interactive_shell_black.h +++ b/test/unit/main/interactive_shell_black.h @@ -45,7 +45,7 @@ class InteractiveShellBlack : public CxxTest::TestSuite d_options.set(options::inputLanguage, language::input::LANG_CVC4); d_symman.reset(nullptr); d_solver.reset(new api::Solver(&d_options)); - d_symman.reset(new SymbolManager(d_solver.get())); + d_symman.reset(new SymbolManager()); } void tearDown() override diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index ef8f2e3cf..768fd8d6a 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -70,7 +70,7 @@ class ParserBlack // Debug.on("parser-extra"); // cerr << "Testing good input: <<" << goodInput << ">>" << endl; // istringstream stream(goodInputs[i]); - d_symman.reset(new SymbolManager(d_solver.get())); + d_symman.reset(new SymbolManager()); Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test") .withStringInput(goodInput) .withOptions(d_options) @@ -102,7 +102,7 @@ class ParserBlack // cerr << "Testing bad input: '" << badInput << "'\n"; // Debug.on("parser"); - d_symman.reset(new SymbolManager(d_solver.get())); + d_symman.reset(new SymbolManager()); Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test") .withStringInput(badInput) .withOptions(d_options) @@ -134,7 +134,7 @@ class ParserBlack // Debug.on("parser"); // istringstream stream(context + goodBooleanExprs[i]); - d_symman.reset(new SymbolManager(d_solver.get())); + d_symman.reset(new SymbolManager()); Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test") .withStringInput(goodExpr) .withOptions(d_options) @@ -182,7 +182,7 @@ class ParserBlack // Debug.on("parser-extra"); // cout << "Testing bad expr: '" << badExpr << "'\n"; - d_symman.reset(new SymbolManager(d_solver.get())); + d_symman.reset(new SymbolManager()); Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test") .withStringInput(badExpr) .withOptions(d_options) diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h index c101542d0..53ba78ed6 100644 --- a/test/unit/parser/parser_builder_black.h +++ b/test/unit/parser/parser_builder_black.h @@ -43,7 +43,7 @@ class ParserBuilderBlack : public CxxTest::TestSuite // ensure the old symbol manager is deleted d_symman.reset(nullptr); d_solver.reset(new api::Solver()); - d_symman.reset(new SymbolManager(d_solver.get())); + d_symman.reset(new SymbolManager()); } void tearDown() override {} |