diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-09-08 14:25:25 +0000 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-09-08 14:25:25 +0000 |
| commit | cfa9e2cbbdf77a325791b5548b41093a0781311c (patch) | |
| tree | e843d38afe4b197a2dd81316998477cedac26c52 /src/main/portfolio.h | |
| parent | 6935324f45bd7f2c735ca4120a9e800ef8903442 (diff) | |
Single driver for both sequential and portfolio
A "command executer" layer between parsing commands and invoking them.
New implementation of portfolio driver splits only when check-sat or query
command is encountered, and then switches back to sequential till the next
one. As side effect, restores functionality of interactive mode and
push/pops.
Diffstat (limited to 'src/main/portfolio.h')
| -rw-r--r-- | src/main/portfolio.h | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/main/portfolio.h b/src/main/portfolio.h index 1a82d651b..341f243d3 100644 --- a/src/main/portfolio.h +++ b/src/main/portfolio.h @@ -11,10 +11,8 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** \brief Provides (somewhat) generic functionality to simulate a + ** (potentially cooperative) race **/ #ifndef __CVC4__PORTFOLIO_H |