Age | Commit message (Collapse) | Author |
|
|
|
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
|
|
|
|
|
|
|
|
|
|
Fix for emptyset in smt2 parser, sets translator to quantified logic, misc
|
|
Also ensure // commented Debug() lines don't get included in Debug/Trace_tags.
|
|
catches some corner cases, more readable too
|
|
9978c259f30b1f4b2c70c04589a309033a6eb1f6
|
|
Fixed, at the cost of an antlr warning that's safe to ignore for now.
|
|
|
|
|
|
|
|
todo: set logic correctly, split the code for two translators
|
|
|
|
Sets translator, bug fixes
|
|
|
|
|
|
types get sent to the theory of the type.
Adding a new test case for bug 569.
Fixes to the normal form of arithmetic so that real terms are before integer terms.
|
|
|
|
|
|
|
|
- $ is a simple symbol is smt2.
- ever found yourself counting in kind.h? no longer.
- expose parser "logic is set" state for smt/smt2 (any better way?)
- a more helpful assertion message in smt_engine
|
|
|
|
|
|
|
|
|
|
(related to bug #569).
|
|
|
|
|
|
bvor, and bvxor.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|