diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-11-27 19:02:50 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-11-27 19:02:50 +0000 |
commit | 95dcbc6781cd8e62f8436f0cfe944b21dfd60ec0 (patch) | |
tree | e0259b9f2993e397e662d6c71a74e473133850b1 /src/decision/justification_heuristic.h | |
parent | 0697e19c09a8ac5f1d9c30ee053845f06ea39c0e (diff) |
Simplify --help=decision with only currently supported options
Add notice/warning when using incremental-mode + decision (it was
already disabled)
Some other minor cleanup
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/decision/justification_heuristic.h')
-rw-r--r-- | src/decision/justification_heuristic.h | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 5669ae79d..a3b05b1bb 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -130,7 +130,7 @@ public: Trace("decision") << "jh: Nothing to split on " << std::endl; -#if defined CVC4_ASSERTIONS || defined CVC4_DEBUG +#if defined CVC4_DEBUG bool alljustified = true; for(unsigned i = 0 ; i < d_assertions.size() && alljustified ; ++i) { TNode curass = d_assertions[i]; @@ -176,10 +176,6 @@ public: } } - /* Compute justified */ - /*bool computeJustified() { - - }*/ private: SatLiteral findSplitter(TNode node, SatValue desiredVal) { @@ -188,7 +184,6 @@ private: ret = findSplitterRec(node, desiredVal, &litDecision); if(ret == true) { Debug("decision") << "Yippee!!" << std::endl; - //d_prvsIndex = i; ++d_helfulness; return litDecision; } else { @@ -198,7 +193,6 @@ private: /** * Do all the hard work. - * @param findFirst returns */ bool findSplitterRec(TNode node, SatValue value, SatLiteral* litDecision); |