diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-29 21:49:41 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-29 21:49:41 +0000 |
| commit | 9a8a3449b130b0154ae55ad223f362c6d662d6ce (patch) | |
| tree | 933bb099f84fdbfdbc15d790a9088d24bcb8ef15 /src/theory/quantifiers/model_engine.h | |
| parent | 45d96ce6cdd0eb5a899611b4b0be243c6887da39 (diff) | |
more updates and minor bug fixes for fmf/inst-gen quantifier instantiation
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: |