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/inst_strategy_cbqi.h | |
| parent | 2e7ec13174e165cccc74159b5c6590d12894a674 (diff) | |
Basic support for EPR+CBQI. Minor cleanup.
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.h')
| -rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 20d872c36..18931f8f6 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -52,7 +52,7 @@ protected: /** has added cbqi lemma */ bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); } /** helper functions */ - bool hasNonCbqiVariable( Node q ); + int hasNonCbqiVariable( Node q ); bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ); /** process functions */ virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; |