diff options
Diffstat (limited to 'src/decision/relevancy.h')
| -rw-r--r-- | src/decision/relevancy.h | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h index 3a33a5cb8..f45ce2e8f 100644 --- a/src/decision/relevancy.h +++ b/src/decision/relevancy.h @@ -46,8 +46,6 @@ namespace CVC4 { namespace decision { -typedef std::vector<TNode> IteList; - class RelGiveUpException : public Exception { public: RelGiveUpException() : @@ -56,6 +54,7 @@ public: };/* class GiveUpException */ class Relevancy : public RelevancyStrategy { + typedef std::vector<TNode> IteList; typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache; typedef hash_map<TNode,TNode,TNodeHashFunction> SkolemMap; typedef hash_map<TNode,SatValue,TNodeHashFunction> PolarityCache; @@ -139,6 +138,10 @@ public: d_maxTimeAsPercentageOfTotalTime(decOpt.maxRelTimeAsPermille*1.0/10.0), d_curDecision(NULL) { + Warning() << "There are known bugs in this Relevancy code which we know" + << "how to fix (but haven't yet)." << std::endl + << "Please bug kshitij if you wish to use." << std::endl; + StatisticsRegistry::registerStat(&d_helfulness); StatisticsRegistry::registerStat(&d_polqueries); StatisticsRegistry::registerStat(&d_polhelp); @@ -350,7 +353,7 @@ private: SatValue tryGetSatValue(Node n); /* Get list of all term-ITEs for the atomic formula v */ - const IteList& getITEs(TNode n); + const Relevancy::IteList& getITEs(TNode n); /* Compute all term-ITEs in a node recursively */ void computeITEs(TNode n, IteList &l); |