diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-13 10:13:16 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-13 10:13:30 +0200 |
| commit | e7439fc0daf1049f59540b9aeb890a52d86a77bd (patch) | |
| tree | 823cfdcb1ddedcfc2e787893ffc688c090c10a07 /src/theory/quantifiers/model_engine.h | |
| parent | dcb85a122a2dc9c80c2626ba6ab83f97d7e983ad (diff) | |
Refactor interface for incompleteness in quantifiers engine, cbqi. Minor fix for sygus.
Diffstat (limited to 'src/theory/quantifiers/model_engine.h')
| -rw-r--r-- | src/theory/quantifiers/model_engine.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 6cdb47be2..c357c2876 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -49,7 +49,9 @@ public: public: bool needsCheck( Theory::Effort e ); unsigned needsModel( Theory::Effort e ); + void reset_round( Theory::Effort e ); void check( Theory::Effort e, unsigned quant_e ); + bool checkComplete(); void registerQuantifier( Node f ); void assertNode( Node f ); Node explain(TNode n){ return Node::null(); } |