Age | Commit message (Expand) | Author |
2016-05-26 | Use term indexing in TheoryUF::computeCareGraph. Do not reject model value in... | ajreynol |
2016-05-20 | Improvements to theory combination + strings: do not return trivial care grap... | ajreynol |
2016-04-03 | Updating the copyright headers and scripts. | Tim King |
2016-03-23 | squash-merge from proof branch | Guy |
2016-01-28 | Adding listeners to Options. | Tim King |
2016-01-26 | Merged bit-vector and uf proof branch. | Liana Hadarean |
2016-01-05 | Add SmtGlobals Class | Tim King |
2015-10-26 | Promote InstStrategyCbqi to quantifier module. Cleanup unused code. | ajreynol |
2014-07-01 | Update copyrights. | Morgan Deters |
2014-04-29 | Fix compiler warning re: TheoryUF destructor. | Morgan Deters |
2014-04-29 | Mostly resolves bug #561 memory leaks, and more. | Morgan Deters |
2014-01-22 | Delay QuantifiersEngine and UF strong solver initialization until after final... | Morgan Deters |
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-02-24 | added option --model-u-dt-enum for outputting uninterpreted sorts as datatype... | Andrew Reynolds |
2012-12-01 | remove instantiator framework | Morgan Deters |
2012-11-26 | Adding support for a master equality engine. Each theory gets the master equa... | Dejan Jovanović |
2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
2012-07-12 | merged fmf-devel branch, includes support for SMT2 command get-value and (ext... | Andrew Reynolds |
2012-07-06 | Added virtual destructor to PpRewrite. | Tim King |
2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |
2012-06-10 | fixes for bug347 | Dejan Jovanović |
2012-06-06 | Changes to the combination mechanism, lots of details. Not done yet, there ar... | Dejan Jovanović |
2012-05-21 | Updating equality manager to handle tagged trigger terms. Notifications are p... | Dejan Jovanović |
2012-05-09 | * simplifying equality engine interface | Dejan Jovanović |
2012-05-03 | Some cleanup starting off from trying to understand the sharing code. Changes... | Dejan Jovanović |
2012-03-22 | some improvements to the sharing mechanism/interface | Dejan Jovanović |
2012-03-02 | CDMap -> CDHashMap | Dejan Jovanović |
2012-02-24 | Theory interface changes: | Dejan Jovanović |
2011-11-30 | fix linking errors on oneiric | Morgan Deters |
2011-10-17 | Sharing work | Dejan Jovanović |
2011-09-29 | Some base infrastructure for user push/pop; a few bugfixes to user push/pop a... | Morgan Deters |
2011-09-15 | additional stuff for sharing, | Dejan Jovanović |
2011-09-07 | fixes for uf/equality engine from the quantifiers branch. mainly backtracking... | Dejan Jovanović |
2011-09-02 | Merge from my post-smtcomp branch. Includes: | Morgan Deters |
2011-07-11 | adding disequality propagation | Dejan Jovanović |
2011-07-11 | merge from symmetry branch | Morgan Deters |
2011-07-09 | some immediate bug fixes | Dejan Jovanović |
2011-07-09 | minor fixups | Morgan Deters |
2011-07-09 | surprize surprize | Dejan Jovanović |
2011-04-25 | Weekend work. The main points: | Morgan Deters |
2011-03-25 | This is a merge from the "theoryfixes+cdattrhash" branch. The changes | Morgan Deters |
2011-01-05 | Commit for the theory engine and rewriter changes. Changes are substantial an... | Dejan Jovanović |
2010-08-17 | Merge from "cc" branch: | Morgan Deters |
2010-07-07 | Added shared term manager. Basic mechanism for identifying shared terms is | Clark Barrett |
2010-07-04 | With "-d extra-checking", rewrites are now checked (after | Morgan Deters |
2010-06-30 | * theory "tree" rewriting implemented and works | Morgan Deters |
2010-06-04 | ** Don't fear the files-changed list, almost all changes are in the ** | Morgan Deters |