diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-09-02 18:28:52 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-09-03 15:19:10 -0400 |
| commit | 8dc1280a5161633fddfb8334811a86c911bb25c1 (patch) | |
| tree | f4b100a3f70acc10e6ca05a1d4c28c659df0eafe /src/theory/quantifiers/theory_quantifiers.cpp | |
| parent | e9fb730333b2719cddaa0a9209aa7953d7f30b0b (diff) | |
check() optimization
Details of testing here:
http://church.cims.nyu.edu/wiki/User:Kshitij/theorycheckoptimization
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
| -rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 4e8a0a411..18546b09c 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -109,6 +109,10 @@ void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) { } void TheoryQuantifiers::check(Effort e) { + if (done() && !fullEffort(e)) { + return; + } + CodeTimer codeTimer(d_theoryTime); Trace("quantifiers-check") << "quantifiers::check(" << e << ")" << std::endl; |