summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/bvminisat/simp/SimpSolver.h7
-rw-r--r--src/prop/cnf_stream.h4
-rw-r--r--src/prop/minisat/core/Solver.h1
-rw-r--r--src/prop/prop_engine.cpp33
-rw-r--r--src/prop/prop_engine.h23
-rw-r--r--src/prop/prop_proof_manager.cpp2
-rw-r--r--src/prop/prop_proof_manager.h2
-rw-r--r--src/prop/sat_proof_manager.h8
-rw-r--r--src/prop/theory_proxy.h5
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 {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback