Age | Commit message (Collapse) | Author | |
---|---|---|---|
2013-06-26 | Add support for interval models in bounded integers MBQI (in progress). | Andrew Reynolds | |
2013-06-25 | Refactoring of model engine to separate individual implementations of model ↵ | Andrew Reynolds | |
builder. Begin work on interval models for integers. Other minor cleanup. | |||
2013-06-04 | Add partial support for MBQI with arrays when using --fmf-fmc. Fix constant ↵ | Andrew Reynolds | |
bounds for bounded integers. | |||
2013-05-22 | Significant work on bounded integer quantification to handle non-trivial ↵ | Andrew Reynolds | |
bounds. Refactoring of InstConstantAttribute to be internal to TermDb. | |||
2013-05-11 | Preliminary version of finite model finding over bounded integer ↵ | Andrew Reynolds | |
quantification. Minor update to casc script. | |||
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters | |
2013-02-16 | Some cleanup and copyright updating | Morgan Deters | |
* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles | |||
2013-02-04 | fixed files with DOS newlines; fixed contrib/ scripts to use git | Morgan Deters | |
2012-11-12 | minor bug fixes for quantifiers, added sort inference module (not ready to ↵ | Andrew Reynolds | |
be used yet), added new totality lemma option for uf strong solver | |||
2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters | |
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.) | |||
2012-10-09 | fixed datatypes rewriter to detect clashes between non-datatype subfields. ↵ | Andrew Reynolds | |
cleaned up model code, TheoryModel::getValue is now const. | |||
2012-08-31 | merge from fmf-devel branch. more updates to models: now with ↵ | Andrew Reynolds | |
collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models |