diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-10-23 00:45:57 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-10-23 00:45:57 +0000 |
| commit | 18f710cbfb5ce1ea13c8e929445abc211c732a81 (patch) | |
| tree | 69e4517ad67d6afd82c4b48a886e828ed84070f1 /src/theory/theory_engine.h | |
| parent | 9039185001b789eadd8b20149455fe778a80fb69 (diff) | |
Implement changes from yesterday morning's meeting (10/21/2011):
* OutputChannel::lemma() now returns an unsigned int. This facility isn't functional yet, but the signature is there. For now, it always returns the current user level (which is "correct" from the interface point of view, but not what we want).
* Pseudobooleans disabled. This should fix some quantifier benchmarks Andy's been working with on the quantifiers2 branch.
* --limit / --time-limit options renamed --rlimit and --tlimit.
There may be slowdown from disabling pseudobooleans.
Diffstat (limited to 'src/theory/theory_engine.h')
| -rw-r--r-- | src/theory/theory_engine.h | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 80890303b..09bb6963e 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -200,10 +200,10 @@ class TheoryEngine { d_engine->propagate(literal, d_theory); } - void lemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) { + unsigned lemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) { Trace("theory") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; - d_engine->lemma(lemma, false, removable); + return d_engine->lemma(lemma, false, removable); } void setIncomplete() throw(AssertionException) { @@ -346,7 +346,7 @@ class TheoryEngine { /** * Adds a new lemma */ - void lemma(TNode node, bool negated, bool removable) { + unsigned lemma(TNode node, bool negated, bool removable) { if(Dump.isOn("t-lemmas")) { Dump("t-lemmas") << CommentCommand("theory lemma: expect valid") << std::endl @@ -363,6 +363,10 @@ class TheoryEngine { // Mark that we added some lemmas d_lemmasAdded = true; + + // Lemma analysis isn't online yet; this lemma may only live for this + // user level. + return d_userContext->getLevel(); } public: |