Branch data Line data Source code
1 : : /****************************************************************************** 2 : : * Top contributors (to current version): 3 : : * Andrew Reynolds, Aina Niemetz, Mathias Preiner 4 : : * 5 : : * This file is part of the cvc5 project. 6 : : * 7 : : * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS 8 : : * in the top-level source directory and their institutional affiliations. 9 : : * All rights reserved. See the file COPYING in the top-level source 10 : : * directory for licensing information. 11 : : * **************************************************************************** 12 : : * 13 : : * The preprocessing pass context for passes. 14 : : */ 15 : : 16 : : #include "preprocessing/preprocessing_pass_context.h" 17 : : 18 : : #include "expr/node_algorithm.h" 19 : : #include "options/base_options.h" 20 : : #include "prop/prop_engine.h" 21 : : #include "smt/env.h" 22 : : #include "theory/theory_engine.h" 23 : : #include "theory/theory_model.h" 24 : : 25 : : namespace cvc5::internal { 26 : : namespace preprocessing { 27 : : 28 : 49906 : PreprocessingPassContext::PreprocessingPassContext( 29 : : Env& env, 30 : : TheoryEngine* te, 31 : : prop::PropEngine* pe, 32 : 49906 : theory::booleans::CircuitPropagator* circuitPropagator) 33 : : : EnvObj(env), 34 : : d_theoryEngine(te), 35 : : d_propEngine(pe), 36 : : d_circuitPropagator(circuitPropagator), 37 : : d_llm(env), 38 : 49906 : d_symsInAssertions(userContext()) 39 : : { 40 : 49906 : } 41 : : 42 : : theory::TrustSubstitutionMap& 43 : 81299 : PreprocessingPassContext::getTopLevelSubstitutions() const 44 : : { 45 : 81299 : return d_env.getTopLevelSubstitutions(); 46 : : } 47 : : 48 : 1284850 : TheoryEngine* PreprocessingPassContext::getTheoryEngine() const 49 : : { 50 : 1284850 : return d_theoryEngine; 51 : : } 52 : 35681 : prop::PropEngine* PreprocessingPassContext::getPropEngine() const 53 : : { 54 : 35681 : return d_propEngine; 55 : : } 56 : : 57 : 586234 : void PreprocessingPassContext::spendResource(Resource r) 58 : : { 59 : 586234 : d_env.getResourceManager()->spendResource(r); 60 : 586234 : } 61 : 19437 : void PreprocessingPassContext::recordSymbolsInAssertions( 62 : : const std::vector<Node>& assertions) 63 : : { 64 : 38874 : std::unordered_set<TNode> visited; 65 : 38874 : std::unordered_set<Node> syms; 66 [ + + ]: 91484 : for (TNode cn : assertions) 67 : : { 68 : 72047 : expr::getSymbols(cn, syms, visited); 69 : : } 70 [ + + ]: 68636 : for (const Node& s : syms) 71 : : { 72 : 49199 : d_symsInAssertions.insert(s); 73 : : } 74 : 19437 : } 75 : : 76 : 233655 : void PreprocessingPassContext::notifyLearnedLiteral(TNode lit) 77 : : { 78 : 233655 : d_llm.notifyLearnedLiteral(lit); 79 : 233655 : } 80 : : 81 : 16 : std::vector<Node> PreprocessingPassContext::getLearnedLiterals() const 82 : : { 83 : 16 : return d_llm.getLearnedLiterals(); 84 : : } 85 : : 86 : 1324 : void PreprocessingPassContext::addSubstitution(const Node& lhs, 87 : : const Node& rhs, 88 : : ProofGenerator* pg) 89 : : { 90 : 1324 : d_propEngine->notifyTopLevelSubstitution(lhs, rhs); 91 : 1324 : d_env.getTopLevelSubstitutions().addSubstitution(lhs, rhs, pg); 92 : 1324 : } 93 : : 94 : 0 : void PreprocessingPassContext::addSubstitution(const Node& lhs, 95 : : const Node& rhs, 96 : : ProofRule id, 97 : : const std::vector<Node>& args) 98 : : { 99 : 0 : d_propEngine->notifyTopLevelSubstitution(lhs, rhs); 100 : 0 : d_env.getTopLevelSubstitutions().addSubstitution(lhs, rhs, id, {}, args); 101 : 0 : } 102 : : 103 : 36904 : void PreprocessingPassContext::addSubstitutions( 104 : : theory::TrustSubstitutionMap& tm) 105 : : { 106 : 73808 : std::unordered_map<Node, Node> subs = tm.get().getSubstitutions(); 107 [ + + ]: 92501 : for (const std::pair<const Node, Node>& s : subs) 108 : : { 109 : 55597 : d_propEngine->notifyTopLevelSubstitution(s.first, s.second); 110 : : } 111 : 36904 : d_env.getTopLevelSubstitutions().addSubstitutions(tm); 112 : 36904 : } 113 : : 114 : : } // namespace preprocessing 115 : : } // namespace cvc5::internal