diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-14 10:42:39 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-14 10:42:39 -0500 |
| commit | beb73911f71daa6711390264221e7b4de7dc8c6c (patch) | |
| tree | dc102dfca7f3ac87944af7760de759fe56a2b648 /src/theory/quantifiers/quant_util.h | |
| parent | 5887766342258361d3635a5b29a015dadb9ebe83 (diff) | |
Lemma cache in theory sep. Minor optimization for sets. Minor improvements to EPR
Diffstat (limited to 'src/theory/quantifiers/quant_util.h')
| -rw-r--r-- | src/theory/quantifiers/quant_util.h | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 049644ffb..d8e57b1ca 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -177,6 +177,8 @@ 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; + /** axioms for epr */ + std::map< TypeNode, Node > d_epr_axiom; public: QuantEPR(){} virtual ~QuantEPR(){} @@ -191,9 +193,15 @@ public: /** finish init */ void finishInit(); /** is EPR */ - bool isEPR( TypeNode tn ) { return d_non_epr.find( tn )!=d_non_epr.end() ? false : true; } + bool isEPR( TypeNode tn ) const { return d_non_epr.find( tn )==d_non_epr.end(); } /** is EPR constant */ bool isEPRConstant( TypeNode tn, Node k ); + /** add EPR constant */ + void addEPRConstant( TypeNode tn, Node k ); + /** get EPR axiom */ + Node mkEPRAxiom( TypeNode tn ); + /** has EPR axiom */ + bool hasEPRAxiom( TypeNode tn ) const { return d_epr_axiom.find( tn )!=d_epr_axiom.end(); } }; } |