diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-12 11:00:44 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-12 11:00:44 +0100 |
| commit | ada1fc44c9b5b8746a2e1e4046032282149768b5 (patch) | |
| tree | efb350f7729004fedb4d7d872d5ff7e8d5d1fdc4 /src/theory/quantifiers/relevant_domain.h | |
| parent | 97470da31e14104f807fb33b2b3423e583e10726 (diff) | |
Minor fixes and improvements to purify quant, relational triggers.
Diffstat (limited to 'src/theory/quantifiers/relevant_domain.h')
| -rw-r--r-- | src/theory/quantifiers/relevant_domain.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 7d1c60f80..25c821e10 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -37,7 +37,7 @@ private: void merge( RDomain * r ); void addTerm( Node t, bool nonGround = false ); RDomain * getParent(); - void removeRedundantTerms( FirstOrderModel * fm ); + void removeRedundantTerms( QuantifiersEngine * qe ); bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); } }; std::map< Node, std::map< int, RDomain * > > d_rel_doms; @@ -56,7 +56,7 @@ public: void compute(); RDomain * getRDomain( Node n, int i ); - Node getRelevantTerm( Node f, int i, Node r ); + //Node getRelevantTerm( Node f, int i, Node r ); };/* class RelevantDomain */ }/* CVC4::theory::quantifiers namespace */ |