diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-08-26 16:27:57 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-08-26 16:27:57 -0500 |
commit | 9ac5255577a07e3bef123908d55003f89dea7619 (patch) | |
tree | 81a74251576a2bdcb58a010a8d0eb83c57b71a9d /src/theory/quantifiers/quant_util.h | |
parent | 2e7ec13174e165cccc74159b5c6590d12894a674 (diff) |
Basic support for EPR+CBQI. Minor cleanup.
Diffstat (limited to 'src/theory/quantifiers/quant_util.h')
-rw-r--r-- | src/theory/quantifiers/quant_util.h | 26 |
1 files changed, 25 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 79cdae437..049644ffb 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -149,7 +149,7 @@ public: }; -class EqualityQuery : public QuantifiersUtil{ +class EqualityQuery : public QuantifiersUtil { public: EqualityQuery(){} virtual ~EqualityQuery(){}; @@ -171,6 +171,30 @@ public: virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0; };/* class EqualityQuery */ +class QuantEPR +{ +private: + void registerNode( Node n, std::map< int, std::map< Node, bool > >& visited, bool beneathQuant, bool hasPol, bool pol ); + /** non-epr */ + std::map< TypeNode, bool > d_non_epr; +public: + QuantEPR(){} + virtual ~QuantEPR(){} + /** constants per type */ + std::map< TypeNode, std::vector< Node > > d_consts; + /* reset */ + //bool reset( Theory::Effort e ) {} + /** identify */ + //std::string identify() const { return "QuantEPR"; } + /** register assertion */ + void registerAssertion( Node assertion ); + /** finish init */ + void finishInit(); + /** is EPR */ + bool isEPR( TypeNode tn ) { return d_non_epr.find( tn )!=d_non_epr.end() ? false : true; } + /** is EPR constant */ + bool isEPRConstant( TypeNode tn, Node k ); +}; } } |