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/output_channel.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/output_channel.h')
| -rw-r--r-- | src/theory/output_channel.h | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 625abc580..aaad25bd5 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -85,8 +85,10 @@ public: * * @param n - a theory lemma valid at decision level 0 * @param removable - whether the lemma can be removed at any point + * @return the user level at which the lemma resides; it will be + * removed when this user level pops */ - virtual void lemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) = 0; + virtual unsigned lemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) = 0; /** * Request a split on a new theory atom. This is equivalent to |