diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-08 08:13:05 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-08 08:13:05 -0500 |
commit | ce831651caf58c1005fd3ebfdd2b75923d594328 (patch) | |
tree | 8787737dde71b80722bbf39718c38e739596d9fd /src/theory/quantifiers_engine.h | |
parent | 2ca4e063ca007851ebf73ccb2ac6b7c85e73133d (diff) |
Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. Minor fixes to ambqi. Preparation for CASC proof output. Add NNF option.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index eb9803592..7a899db0c 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -235,6 +235,8 @@ public: /** get the master equality engine */ eq::EqualityEngine* getMasterEqualityEngine() ; public: + /** print instantiations */ + void printInstantiations( const char * c ); /** statistics class */ class Statistics { public: |