diff options
Diffstat (limited to 'src/theory/quantifiers/quant_util.h')
| -rw-r--r-- | src/theory/quantifiers/quant_util.h | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index c1c39fa0f..116211bfb 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -28,7 +28,7 @@ namespace CVC4 { namespace theory { class QuantifiersEngine; - + class QuantArith { public: @@ -112,6 +112,9 @@ public: class QuantLtePartialInst { private: + // was this module invoked + bool d_wasInvoked; + //representatives per type std::map< TypeNode, std::vector< Node > > d_reps; // should we instantiate quantifier std::map< Node, bool > d_do_inst; @@ -125,7 +128,7 @@ private: /** reset */ void reset(); /** get instantiations */ - void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, + void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, std::vector< Node >& vars, std::vector< Node >& inst, std::vector< TypeNode >& types, unsigned index ); /** get eligible inst variables */ void getEligibleInstVars( Node n, std::map< Node, bool >& vars ); @@ -135,6 +138,8 @@ public: bool addQuantifier( Node q ); /** get instantiations */ void getInstantiations( std::vector< Node >& lemmas ); + /** was invoked */ + bool wasInvoked() { return d_wasInvoked; } }; |