diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-10-13 04:14:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-10-13 04:14:38 +0000 |
commit | 3cbb76ef86a769cfe3dac5976a14e1bc43c42ca6 (patch) | |
tree | e08efdc63abd663de4f5750db9326b69c79829e5 /src/theory/output_channel.h | |
parent | 3a7aafccadbfa1543c435b7dfe4f53116224a11f (diff) |
Interruption, time-out, and deterministic time-out ("resource-out") features.
Details here: http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_October_14,_2011#Resource.2Ftime_limiting_API
This will need more work, but it's a start.
Also implemented TheoryEngine::properPropagation().
Other minor things.
Diffstat (limited to 'src/theory/output_channel.h')
-rw-r--r-- | src/theory/output_channel.h | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index f5bf620bf..625abc580 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -105,6 +105,20 @@ public: */ virtual void setIncomplete() throw(AssertionException) = 0; + /** + * "Spend" a "resource." The meaning is specific to the context in + * which the theory is operating, and may even be ignored. The + * intended meaning is that if the user has set a limit on the "units + * of resource" that can be expended in a search, and that limit is + * exceeded, then the search is terminated. Note that the check for + * termination occurs in the main search loop, so while theories + * should call OutputChannel::spendResource() during particularly + * long-running operations, they cannot rely on resource() to break + * out of infinite or intractable computations. + */ + virtual void spendResource() throw() { + } + };/* class OutputChannel */ }/* CVC4::theory namespace */ |