diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-07-04 18:36:22 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-07-04 18:36:22 +0000 |
commit | 693d70847d0ed753a4f035dd3c88eb32607e2081 (patch) | |
tree | 0076edc5a7fe9eaf6605bef8bb6804e6a48e4d85 /src/prop | |
parent | 0679a64a1c1017d8ef0e26e40a476f2559e6bba3 (diff) |
Considerably simplified the way output streams are used. This commit
should have no impact on production performance and speed up debug
performance considerably, while making the code much cleaner. On some
benchmarks, debug builds now run _much_ faster.
We no longer have to sprinkle our code with things like:
if(debugTagIsOn("context")) {
Debug("context") << theContext << std::endl;
}
which we had to do to get around performance problems previously.
Now just writing:
Debug("context") << theContext << std::endl;
does the same in production and debug builds. That is, if "context"
debugging is off, theContext isn't converted to a string, nor is it
output to a "/dev/null" ostream. I've confirmed this. In production
builds, the whole statement inlines to nothing. I've confirmed this
too.
Also, "Debug" is no longer a #definition, so you can use it directly
in production builds where you couldn't previously, e.g.
if(Debug.isOn("paranoid:check_tableau")) {
checkTableau();
}
I'm leaving debugTagIsOn() for now, but marking it as deprecated.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/prop_engine.cpp | 2 | ||||
-rw-r--r-- | src/prop/sat.h | 17 |
2 files changed, 10 insertions, 9 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 7cccca177..c49d5f38a 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -122,7 +122,7 @@ Result PropEngine::checkSat() { // Check the problem bool result = d_satSolver->solve(); - if( result && debugTagIsOn("prop") ) { + if( result && Debug.isOn("prop") ) { printSatisfyingAssignment(); } diff --git a/src/prop/sat.h b/src/prop/sat.h index 9e09727e3..c58a198b3 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -237,7 +237,7 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, d_minisat->polarity_mode = minisat::SimpSolver::polarity_user; // No random choices - if(debugTagIsOn("no_rnd_decisions")){ + if(Debug.isOn("no_rnd_decisions")){ d_minisat->random_var_freq = 0; } @@ -271,13 +271,15 @@ SatSolver::SatLiteralHashFunction::operator()(const SatLiteral& literal) const { return hashSatLiteral(literal); } -inline std::ostream& operator <<(std::ostream& out, SatLiteral lit) { - const char * s = (literalSign(lit)) ? "~" : " "; - out << s << literalToVariable(lit); +}/* CVC4::prop namespace */ + +inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) { + const char * s = (prop::literalSign(lit)) ? "~" : " "; + out << s << prop::literalToVariable(lit); return out; } -inline std::ostream& operator <<(std::ostream& out, const SatClause& clause) { +inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) { out << "clause:"; for(int i = 0; i < clause.size(); ++i) { out << " " << clause[i]; @@ -286,12 +288,11 @@ inline std::ostream& operator <<(std::ostream& out, const SatClause& clause) { return out; } -inline std::ostream& operator <<(std::ostream& out, const SatLiteralValue& val) { - out << stringOfLiteralValue(val); +inline std::ostream& operator <<(std::ostream& out, prop::SatLiteralValue val) { + out << prop::stringOfLiteralValue(val); return out; } -}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* __CVC4__PROP__SAT_H */ |