| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2010-12-14 | congruence closure module now supports things other than APPLY_UF; ported ↵ | Morgan Deters | |
| from "arrays" branch to trunk | |||
| 2010-11-16 | fix function signatures | Morgan Deters | |
| 2010-11-15 | cleanup from today's commits: delegate as-yet-unimplemented prettyprinters ↵ | Morgan Deters | |
| in a better way; fix arith Makefile | |||
| 2010-11-15 | Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printer | Morgan Deters | |
| implemented. This new infrastructure removes support for pretty-printing (even in the AST language) an Expr with reference count 0. Previously, this was supported in a few places internally to the expr package, for example in NodeBuilder. (Now, a NodeBuilder cannot be prettyprinted, you must extract the Node before printing it.) | |||
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback