diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-10-06 18:53:27 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-10-06 18:53:27 +0000 |
commit | 4e883ffc0b88256a966183ac6b87bb5767154cdf (patch) | |
tree | a193f12035e4417834ef08312f50739ae0b39a87 /src/prop | |
parent | 99cad5495be99efae434177d1537d4cfac35581c (diff) |
* Clean up some options documentation
* Remove defunct --no-theory-registration option
* Point people to Wiki tutorial
* Modernize the cut-release script
* Misc cleanup, documentation
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/theory_proxy.cpp | 3 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 6 |
2 files changed, 8 insertions, 1 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 9ed2202fe..1434cf6c7 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -28,6 +28,7 @@ #include "decision/options.h" #include "util/lemma_input_channel.h" #include "util/lemma_output_channel.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace prop { @@ -170,11 +171,11 @@ SatLiteral TheoryProxy::getNextReplayDecision() { Expr e = options::replayStream()->nextExpr(); if(!e.isNull()) { // we get null node when out of decisions to replay // convert & return + ++d_replayedDecisions; return d_cnfStream->getLiteral(e); } } #endif /* CVC4_REPLAY */ - //FIXME! return undefSatLiteral; } diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 96332217e..5fa133122 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -71,6 +71,12 @@ class TheoryProxy { */ std::hash_set<Node, NodeHashFunction> d_shared; + /** + * Statistic: the number of replayed decisions (via --replay). + */ + KEEP_STATISTIC(IntStat, d_replayedDecisions, + "prop::theoryproxy::replayedDecisions", 0); + public: TheoryProxy(PropEngine* propEngine, TheoryEngine* theoryEngine, |