diff options
author | Tim King <taking@cs.nyu.edu> | 2017-11-18 16:27:46 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-18 18:27:46 -0600 |
commit | 6f95e3c711d39b531eb0a8ac0e098c89a5737ce2 (patch) | |
tree | f30496e445b710b5a1fa1dae5a5cad0911648857 /src/theory/quantifiers/quant_conflict_find.h | |
parent | a7524f1f72c324dae36bd4a461d31e5e26fdca15 (diff) |
Names the Effort enum of QuantConflictFind class. (#1354)
* Changes the Effort level of QuantConflictFind to an enum class. Adding a third value to the enum to indicate not being set. Minor refactoring related to this change. Resolves CID 1172043.
* Fixing a missed assertion. Fixing a few compiler warnings.
* Switching back to an enum from an enum class.
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.h')
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.h | 29 |
1 files changed, 21 insertions, 8 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 0e5fe3c18..8a1043ded 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -17,6 +17,9 @@ #ifndef QUANT_CONFLICT_FIND #define QUANT_CONFLICT_FIND +#include <ostream> +#include <vector> + #include "context/cdhashmap.h" #include "context/cdchunk_list.h" #include "theory/quantifiers_engine.h" @@ -202,7 +205,6 @@ private: void setIrrelevantFunction( TNode f ); private: std::map< Node, Node > d_op_node; - int d_fid_count; std::map< Node, int > d_fid; Node mkEqNode( Node a, Node b ); public: //for ground terms @@ -214,14 +216,23 @@ private: private: //for equivalence classes // type -> list(eqc) std::map< TypeNode, std::vector< TNode > > d_eqcs; -public: - enum { - effort_conflict, - effort_prop_eq, + + public: + enum Effort : unsigned { + EFFORT_CONFLICT, + EFFORT_PROP_EQ, + EFFORT_INVALID, }; - short d_effort; - void setEffort( int e ) { d_effort = e; } - static short getMaxQcfEffort(); + void setEffort(Effort e) { d_effort = e; } + + inline bool atConflictEffort() const { + return d_effort == QuantConflictFind::EFFORT_CONFLICT; + } + + private: + Effort d_effort; + + public: bool areMatchEqual( TNode n1, TNode n2 ); bool areMatchDisequal( TNode n1, TNode n2 ); public: @@ -270,6 +281,8 @@ public: std::string identify() const { return "QcfEngine"; } }; +std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e); + } /* namespace CVC4::theory::quantifiers */ } /* namespace CVC4::theory */ } /* namespace CVC4 */ |