Age | Commit message (Collapse) | Author | |
---|---|---|---|
2020-08-19 | Remove example theory (#4922) | Andrew Reynolds | |
This code is unused and obsolete. | |||
2020-06-16 | Update copyright headers. | Aina Niemetz | |
2019-10-30 | Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366) | Mathias Preiner | |
2019-04-24 | Do not use __ prefix for header guards. (#2974) | Mathias Preiner | |
Fixes 2887. | |||
2019-03-26 | Update copyright headers. | Aina Niemetz | |
2018-09-22 | cmake: Remove unused CMakeLists.txt | Mathias Preiner | |
2018-09-22 | cmake: Added initial build infrastructure. | Aina Niemetz | |
2018-06-25 | Updated copyright headers. | Aina Niemetz | |
2018-01-17 | Removes yet more throw specifiers. Updating the documentation as needed. (#1518) | Tim King | |
2017-07-07 | Update copyright headers. | Mathias Preiner | |
2016-04-20 | update from the master | PaulMeng | |
2014-11-17 | New, uniform checkTime statistic for all theories (as discussed in meeting). | Morgan Deters | |
2014-07-01 | Update copyrights. | Morgan Deters | |
2014-01-22 | Delay QuantifiersEngine and UF strong solver initialization until after ↵ | Morgan Deters | |
final options/logic are set. | |||
2013-11-10 | Flatten libcvc4 build structure; remove some #include interdependences | Morgan Deters | |
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters | |
2013-04-01 | update copyrights | Morgan Deters | |
2013-03-14 | fix to build system: #include the proper file when they are in both builds ↵ | Morgan Deters | |
and src | |||
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-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 | |||
2012-07-12 | merged fmf-devel branch, includes support for SMT2 command get-value and ↵ | Andrew Reynolds | |
(extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this. | |||
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. | |||
2011-09-29 | Some base infrastructure for user push/pop; a few bugfixes to user push/pop ↵ | Morgan Deters | |
and model gen also. I also expect this commit to fix bug #273. No performance change is expected on regressions with this commit, see http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863 | |||
2011-09-16 | include example theory (former "UF-Tim") that's included in the dist but not ↵ | Morgan Deters | |
built for the library |