Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
just the header comments at the top, though. Don't update to this rev if
you don't have time for a complete rebuild, and exclude this rev if you
want to see what's new across a range of commits.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
Other changes:
* fix compile error in smt_engine in debug builds
* add getLogicInfo in smt_engine
* remove "empty-channel" and "disable-lemma-sharing" debug tags
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
* respect output lang
* fix export variable for BOUND_VARIABLE
* support export of SUBRANGE_TYPE
* statistic for lastWinner, other minor stat changes
* fix running of multiple threads on checsat/query
* changes of Assert -> assert which became private
* fix some destruction time order issues
* fix Pickler with AssertionException going private
Fixed by not fixing:
* portfolio+datatypes does not work
- added ExportUnsupportedException to more places, switches
to sequential
(still TODO / decide : not switch silently, but print error)
> note: this exception now needs to be (and is) defined in expr.h
Known issues:
* problems in portfolio+quantifiers
- at least some problems appear to be because of static variables
(will be later "fixed" like the datatypes)
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
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.
|