Age | Commit message (Collapse) | Author | |
---|---|---|---|
2013-03-15 | Boolean terms rewriting for quantified variables of type Bool, when ↵ | Morgan Deters | |
quantifier body uses them in term context | |||
2012-11-27 | Functions and predicates over Boolean now work with --check-models and ↵ | Morgan Deters | |
output correct models for such functions (though they are somewhat ugly at present). There's still a problem with model extraction, but it's not Boolean terms' fault. Sometimes checkModel() can report that the model is just fine, but if a user extracts values with getValue(), they find problems with the model (i.e., it doesn't satisfy some assertions). This appears to be due to an asymmetry between how checkModel() works and how Model::getValue() works. I'll open a bugzilla report to discuss this after thinking some more on it. (this commit was certified error- and warning-free by the test-and-commit script.) | |||
2012-11-27 | First chunk of boolean-terms support. | Morgan Deters | |
Passes simple tests and doesn't break existing functionality. Still need some work merged in for models. This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV). Tonight's nightly regression run should tell us if/how that hurts performance. (this commit was certified error- and warning-free by the test-and-commit script.) |