diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-03-03 17:50:45 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-03 16:50:45 +0000 |
commit | a02a794c383ae2381e1210f53174cefb8d94e615 (patch) | |
tree | 0eac511c22ba9eeba1925e3afa4f0542edf5cf60 /src/prop | |
parent | 6db84f6e373f9651af48df7b654e3992f68472ac (diff) |
More cleanup of includes to reduce compilation times (#6037)
Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.h | 7 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 4 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 1 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 33 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 23 | ||||
-rw-r--r-- | src/prop/prop_proof_manager.cpp | 2 | ||||
-rw-r--r-- | src/prop/prop_proof_manager.h | 2 | ||||
-rw-r--r-- | src/prop/sat_proof_manager.h | 8 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 5 |
9 files changed, 40 insertions, 45 deletions
diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index 9907b8d72..c76878da4 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -21,13 +21,16 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef BVMinisat_SimpSolver_h #define BVMinisat_SimpSolver_h -#include "context/context.h" #include "proof/clause_id.h" #include "prop/bvminisat/core/Solver.h" #include "prop/bvminisat/mtl/Queue.h" -#include "util/statistics_registry.h" namespace CVC4 { + +namespace context { +class Context; +} + namespace BVMinisat { //================================================================================================= diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 69cbb0241..92bdd66ee 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -32,7 +32,7 @@ #include "proof/proof_manager.h" #include "prop/proof_cnf_stream.h" #include "prop/registrar.h" -#include "prop/theory_proxy.h" +#include "prop/sat_solver_types.h" namespace CVC4 { @@ -41,6 +41,8 @@ class OutputManager; namespace prop { class ProofCnfStream; +class PropEngine; +class SatSolver; /** A policy for how literals for formulas are handled in cnf_stream */ enum class FormulaLitPolicy : uint32_t diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 8fa489f65..f685017a7 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -36,6 +36,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/utils/Options.h" #include "prop/sat_proof_manager.h" #include "theory/theory.h" +#include "util/resource_manager.h" namespace CVC4 { template <class Solver> class TSatProof; diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 738b4dc9c..473449179 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -32,6 +32,7 @@ #include "proof/proof_manager.h" #include "prop/cnf_stream.h" #include "prop/minisat/minisat.h" +#include "prop/prop_proof_manager.h" #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" #include "prop/theory_proxy.h" @@ -83,7 +84,7 @@ PropEngine::PropEngine(TheoryEngine* te, d_resourceManager(rm), d_outMgr(outMgr) { - Debug("prop") << "Constructing the PropEngine" << endl; + Debug("prop") << "Constructing the PropEngine" << std::endl; d_decisionEngine.reset(new DecisionEngine(satContext, userContext, rm)); d_decisionEngine->init(); // enable appropriate strategies @@ -146,7 +147,7 @@ void PropEngine::finishInit() } PropEngine::~PropEngine() { - Debug("prop") << "Destructing the PropEngine" << endl; + Debug("prop") << "Destructing the PropEngine" << std::endl; d_decisionEngine->shutdown(); d_decisionEngine.reset(nullptr); delete d_cnfStream; @@ -179,7 +180,7 @@ void PropEngine::notifyPreprocessedAssertions( void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat) << "Sat solver in solve()!"; - Debug("prop") << "assertFormula(" << node << ")" << endl; + Debug("prop") << "assertFormula(" << node << ")" << std::endl; d_decisionEngine->addAssertion(node); assertInternal(node, false, false, true); } @@ -187,7 +188,7 @@ void PropEngine::assertFormula(TNode node) { void PropEngine::assertSkolemDefinition(TNode node, TNode skolem) { Assert(!d_inCheckSat) << "Sat solver in solve()!"; - Debug("prop") << "assertFormula(" << node << ")" << endl; + Debug("prop") << "assertFormula(" << node << ")" << std::endl; d_decisionEngine->addSkolemDefinition(node, skolem); assertInternal(node, false, false, true); } @@ -235,7 +236,7 @@ void PropEngine::assertTrustedLemmaInternal(theory::TrustNode trn, bool removable) { Node node = trn.getNode(); - Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; + Debug("prop::lemmas") << "assertLemma(" << node << ")" << std::endl; bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT; Assert(!isProofEnabled() || trn.getGenerator() != nullptr); assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator()); @@ -292,7 +293,7 @@ void PropEngine::assertLemmasInternal( } void PropEngine::requirePhase(TNode n, bool phase) { - Debug("prop") << "requirePhase(" << n << ", " << phase << ")" << endl; + Debug("prop") << "requirePhase(" << n << ", " << phase << ")" << std::endl; Assert(n.getType().isBoolean()); SatLiteral lit = d_cnfStream->getLiteral(n); @@ -307,26 +308,26 @@ bool PropEngine::isDecision(Node lit) const { void PropEngine::printSatisfyingAssignment(){ const CnfStream::NodeToLiteralMap& transCache = d_cnfStream->getTranslationCache(); - Debug("prop-value") << "Literal | Value | Expr" << endl + Debug("prop-value") << "Literal | Value | Expr" << std::endl << "----------------------------------------" - << "-----------------" << endl; + << "-----------------" << std::endl; for(CnfStream::NodeToLiteralMap::const_iterator i = transCache.begin(), end = transCache.end(); i != end; ++i) { - pair<Node, SatLiteral> curr = *i; + std::pair<Node, SatLiteral> curr = *i; SatLiteral l = curr.second; if(!l.isNegated()) { Node n = curr.first; SatValue value = d_satSolver->modelValue(l); - Debug("prop-value") << "'" << l << "' " << value << " " << n << endl; + Debug("prop-value") << "'" << l << "' " << value << " " << n << std::endl; } } } Result PropEngine::checkSat() { Assert(!d_inCheckSat) << "Sat solver in solve()!"; - Debug("prop") << "PropEngine::checkSat()" << endl; + Debug("prop") << "PropEngine::checkSat()" << std::endl; // Mark that we are in the checkSat ScopedBool scopedBool(d_inCheckSat); @@ -360,7 +361,7 @@ Result PropEngine::checkSat() { printSatisfyingAssignment(); } - Debug("prop") << "PropEngine::checkSat() => " << result << endl; + Debug("prop") << "PropEngine::checkSat() => " << result << std::endl; if(result == SAT_VALUE_TRUE && d_theoryEngine->isIncomplete()) { return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE); } @@ -491,20 +492,20 @@ void PropEngine::push() { Assert(!d_inCheckSat) << "Sat solver in solve()!"; d_satSolver->push(); - Debug("prop") << "push()" << endl; + Debug("prop") << "push()" << std::endl; } void PropEngine::pop() { Assert(!d_inCheckSat) << "Sat solver in solve()!"; d_satSolver->pop(); - Debug("prop") << "pop()" << endl; + Debug("prop") << "pop()" << std::endl; } void PropEngine::resetTrail() { d_satSolver->resetTrail(); - Debug("prop") << "resetTrail()" << endl; + Debug("prop") << "resetTrail()" << std::endl; } unsigned PropEngine::getAssertionLevel() const @@ -522,7 +523,7 @@ void PropEngine::interrupt() d_interrupted = true; d_satSolver->interrupt(); - Debug("prop") << "interrupt()" << endl; + Debug("prop") << "interrupt()" << std::endl; } void PropEngine::spendResource(ResourceManager::Resource r) diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index d0c75a924..834f35d90 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -21,22 +21,11 @@ #ifndef CVC4__PROP_ENGINE_H #define CVC4__PROP_ENGINE_H -#include <sys/time.h> - -#include "base/modal_exception.h" +#include "context/cdlist.h" #include "expr/node.h" -#include "options/options.h" -#include "proof/proof_manager.h" -#include "prop/minisat/core/Solver.h" -#include "prop/minisat/minisat.h" -#include "prop/proof_cnf_stream.h" -#include "prop/prop_proof_manager.h" -#include "prop/sat_solver_types.h" +#include "theory/output_channel.h" #include "theory/trust_node.h" -#include "theory/theory_inference_manager.h" -#include "util/resource_manager.h" #include "util/result.h" -#include "util/unsafe_interrupt_exception.h" namespace CVC4 { @@ -45,16 +34,12 @@ class DecisionEngine; class OutputManager; class TheoryEngine; -namespace theory { - class TheoryRegistrar; -}/* CVC4::theory namespace */ - namespace prop { class CnfStream; class CDCLTSatSolverInterface; - -class PropEngine; +class ProofCnfStream; +class PropPfManager; /** * PropEngine is the abstraction of a Sat Solver, providing methods for diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp index 3c18dc896..c19d09bb9 100644 --- a/src/prop/prop_proof_manager.cpp +++ b/src/prop/prop_proof_manager.cpp @@ -16,6 +16,8 @@ #include "expr/proof_ensure_closed.h" #include "expr/proof_node_algorithm.h" +#include "prop/prop_proof_manager.h" +#include "prop/sat_solver.h" namespace CVC4 { namespace prop { diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h index fc0151bcd..2e0d997df 100644 --- a/src/prop/prop_proof_manager.h +++ b/src/prop/prop_proof_manager.h @@ -27,6 +27,8 @@ namespace CVC4 { namespace prop { +class CDCLTSatSolverInterface; + /** * This class is responsible for managing the proof output of PropEngine, both * building and checking it. diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h index 0555e7ba7..e05923268 100644 --- a/src/prop/sat_proof_manager.h +++ b/src/prop/sat_proof_manager.h @@ -21,10 +21,7 @@ #include "expr/buffered_proof_generator.h" #include "expr/lazy_proof_chain.h" #include "expr/node.h" -#include "expr/proof.h" -#include "expr/proof_node_manager.h" #include "prop/minisat/core/SolverTypes.h" -#include "prop/cnf_stream.h" #include "prop/sat_solver_types.h" namespace Minisat { @@ -32,8 +29,13 @@ class Solver; } namespace CVC4 { + +class ProofNodeManager; + namespace prop { +class CnfStream; + /** * This class is responsible for managing the proof production of the SAT * solver. It tracks resolutions produced during solving and stores them, diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index ac79cf967..049232868 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -23,19 +23,16 @@ // Optional blocks below will be unconditionally included #define CVC4_USE_MINISAT -#include <iosfwd> #include <unordered_set> -#include "context/cdhashmap.h" #include "context/cdqueue.h" #include "expr/node.h" #include "prop/registrar.h" -#include "prop/sat_solver.h" +#include "prop/sat_solver_types.h" #include "theory/theory.h" #include "theory/theory_preprocessor.h" #include "theory/trust_node.h" #include "util/resource_manager.h" -#include "util/statistics_registry.h" namespace CVC4 { |