Age | Commit message (Collapse) | Author | |
---|---|---|---|
2012-08-03 | fix uses of getMetaKind() from outside the expr package. (they now use ↵ | Morgan Deters | |
isConst() and isVar() as appropriate) also some base infrastructure for the new ::isConst(). | |||
2012-07-14 | Type enumerator infrastructure and uninterpreted constant support. No ↵ | Morgan Deters | |
support yet for enumerating arrays, or for enumerating non-trivial datatypes. | |||
2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters | |
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure. Adds theory instantiators to many theories. Adds the UF strong solver. |