diff options
Diffstat (limited to 'src/theory/quantifiers/model_engine.h')
| -rw-r--r-- | src/theory/quantifiers/model_engine.h | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 377fe9aa9..2560cf50e 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -44,8 +44,12 @@ private: bool optOneQuantPerRound(); bool optExhInstEvalSkipMultiple(); private: + enum{ + check_model_full, + check_model_no_inst_gen, + }; //check model - void checkModel( int& addedLemmas ); + int checkModel( int checkOption ); //exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced int exhaustiveInstantiate( Node f, bool useRelInstDomain = false ); private: |