| 2017-03-21 |
ajreynol | Improve computeCareGraph functions to check shared... |
blob | commitdiff | raw |
| 2017-03-02 |
ajreynol | Eliminate Boolean term conversion. Generalizes removeIT... |
blob | commitdiff | raw | diff to current |
| 2016-11-03 |
ajreynol | Add priorities to getNextDecision. Properly handle... |
blob | commitdiff | raw | diff to current |
| 2016-07-05 |
PaulMeng | Merge branch 'master' of https://github.com/CVC4/CVC4.git |
blob | commitdiff | raw | diff to current |
| 2016-05-26 |
Clark Barrett | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2016-05-26 |
ajreynol | Use term indexing in TheoryUF::computeCareGraph. Do... |
blob | commitdiff | raw | diff to current |
| 2016-05-20 |
ajreynol | Improvements to theory combination + strings: do not... |
blob | commitdiff | raw | diff to current |
| 2016-04-20 |
PaulMeng | update from the master |
blob | commitdiff | raw | diff to current |
| 2016-04-09 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2016-04-04 |
Tim King | Updating the copyright headers and scripts. |
blob | commitdiff | raw | diff to current |
| 2016-03-23 |
guykatzz | Merge pull request #82 from CVC4/master_for_merge |
blob | commitdiff | raw | diff to current |
| 2016-03-23 |
Guy | squash-merge from proof branch |
blob | commitdiff | raw | diff to current |
| 2016-01-28 |
Tim King | Adding listeners to Options. |
blob | commitdiff | raw | diff to current |
| 2016-01-27 |
Liana Hadarean | Merged bit-vector and uf proof branch. |
blob | commitdiff | raw | diff to current |
| 2016-01-06 |
Tim King | Add SmtGlobals Class |
blob | commitdiff | raw | diff to current |
| 2015-10-26 |
ajreynol | Promote InstStrategyCbqi to quantifier module. Cleanup... |
blob | commitdiff | raw | diff to current |
| 2014-07-10 |
Kshitij Bansal | Merge remote-tracking branch 'origin/master' into segfa... |
blob | commitdiff | raw | diff to current |
| 2014-07-01 |
Morgan Deters | Update copyrights. |
blob | commitdiff | raw | diff to current |
| 2014-04-30 |
Morgan Deters | Fix compiler warning re: TheoryUF destructor. |
blob | commitdiff | raw | diff to current |
| 2014-04-30 |
Morgan Deters | Mostly resolves bug #561 memory leaks, and more. |
blob | commitdiff | raw | diff to current |
| 2014-04-01 |
Tim King | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-03-26 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-03-11 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-03-11 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-02-21 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-02-21 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-02-19 |
Tim King | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-01-27 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-01-22 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2014-01-22 |
Morgan Deters | Delay QuantifiersEngine and UF strong solver initializa... |
blob | commitdiff | raw | diff to current |
| 2013-11-11 |
Morgan Deters | Flatten libcvc4 build structure; remove some #include... |
blob | commitdiff | raw | diff to current |
| 2013-11-07 |
Morgan Deters | Flatten libcvc4 build structure; remove some #include... |
blob | commitdiff | raw | diff to current |
| 2013-04-02 |
Morgan Deters | Regenerated copyrights: canonicalized names, no emails |
blob | commitdiff | raw | diff to current |
| 2013-04-02 |
Morgan Deters | update copyrights |
blob | commitdiff | raw | diff to current |
| 2013-03-15 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-03-14 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-03-13 |
lianah | post failed attempts at getting the incremental solver... |
blob | commitdiff | raw | diff to current |
| 2013-03-05 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-03-01 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-02-26 |
lianah | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
| 2013-02-24 |
Andrew Reynolds | added option --model-u-dt-enum for outputting uninterpr... |
blob | commitdiff | raw | diff to current |
| 2012-12-01 |
Morgan Deters | remove instantiator framework |
blob | commitdiff | raw | diff to current |
| 2012-11-26 |
Dejan Jovanović | Adding support for a master equality engine. Each theor... |
blob | commitdiff | raw | diff to current |
| 2012-10-11 |
Morgan Deters | Standardizing copyright notice. Touches **ALL** source... |
blob | commitdiff | raw | diff to current |
| 2012-08-31 |
Andrew Reynolds | merge from fmf-devel branch. more updates to models... |
blob | commitdiff | raw | diff to current |
| 2012-07-12 |
Andrew Reynolds | merged fmf-devel branch, includes support for SMT2... |
blob | commitdiff | raw | diff to current |
| 2012-07-06 |
Tim King | Added virtual destructor to PpRewrite. |
blob | commitdiff | raw | diff to current |
| 2012-06-11 |
Morgan Deters | Merge from quantifiers2-trunkmerge branch. |
blob | commitdiff | raw | diff to current |
| 2012-06-10 |
Dejan Jovanović | fixes for bug347 |
blob | commitdiff | raw | diff to current |
| 2012-06-06 |
Dejan Jovanović | Changes to the combination mechanism, lots of details... |
blob | commitdiff | raw | diff to current |
| 2012-05-21 |
Dejan Jovanović | Updating equality manager to handle tagged trigger... |
blob | commitdiff | raw | diff to current |
| 2012-05-09 |
Dejan Jovanović | * simplifying equality engine interface |
blob | commitdiff | raw | diff to current |
| 2012-05-03 |
Dejan Jovanović | Some cleanup starting off from trying to understand... |
blob | commitdiff | raw | diff to current |
| 2012-03-22 |
Dejan Jovanović | some improvements to the sharing mechanism/interface |
blob | commitdiff | raw | diff to current |
| 2012-03-02 |
Dejan Jovanović | CDMap -> CDHashMap |
blob | commitdiff | raw | diff to current |
| 2012-02-24 |
Dejan Jovanović | Theory interface changes: |
blob | commitdiff | raw | diff to current |
| 2011-11-30 |
Morgan Deters | fix linking errors on oneiric |
blob | commitdiff | raw | diff to current |
| 2011-10-17 |
Dejan Jovanović | Sharing work |
blob | commitdiff | raw | diff to current |
| 2011-09-29 |
Morgan Deters | Some base infrastructure for user push/pop; a few bugfi... |
blob | commitdiff | raw | diff to current |
| 2011-09-15 |
Dejan Jovanović | additional stuff for sharing, |
blob | commitdiff | raw | diff to current |
| 2011-09-07 |
Dejan Jovanović | fixes for uf/equality engine from the quantifiers branc... |
blob | commitdiff | raw | diff to current |
| 2011-09-02 |
Morgan Deters | Merge from my post-smtcomp branch. Includes: |
blob | commitdiff | raw | diff to current |
| 2011-07-11 |
Dejan Jovanović | adding disequality propagation |
blob | commitdiff | raw | diff to current |
| 2011-07-11 |
Morgan Deters | merge from symmetry branch |
blob | commitdiff | raw | diff to current |
| 2011-07-09 |
Dejan Jovanović | some immediate bug fixes |
blob | commitdiff | raw | diff to current |
| 2011-07-09 |
Morgan Deters | minor fixups |
blob | commitdiff | raw | diff to current |
| 2011-07-09 |
Dejan Jovanović | surprize surprize |
blob | commitdiff | raw | diff to current |
| 2011-04-25 |
Morgan Deters | Weekend work. The main points: |
blob | commitdiff | raw | diff to current |
| 2011-03-25 |
Morgan Deters | This is a merge from the "theoryfixes+cdattrhash" branc... |
blob | commitdiff | raw | diff to current |
| 2011-01-05 |
Dejan Jovanović | Commit for the theory engine and rewriter changes.... |
blob | commitdiff | raw | diff to current |
| 2010-08-17 |
Morgan Deters | Merge from "cc" branch: |
blob | commitdiff | raw | diff to current |
| 2010-07-07 |
Clark Barrett | Added shared term manager. Basic mechanism for identif... |
blob | commitdiff | raw | diff to current |
| 2010-07-04 |
Morgan Deters | With "-d extra-checking", rewrites are now checked... |
blob | commitdiff | raw | diff to current |
| 2010-06-30 |
Morgan Deters | * theory "tree" rewriting implemented and works |
blob | commitdiff | raw | diff to current |
| 2010-06-04 |
Morgan Deters | ** Don't fear the files-changed list, almost all change... |
blob | commitdiff | raw | diff to current |
| 2010-05-28 |
Tim King | Moving the ITE removal from CnfStream to TheoryEngine... |
blob | commitdiff | raw | diff to current |
| 2010-04-04 |
Morgan Deters | * Node::isAtomic() now looks at an "atomic" attribute... |
blob | commitdiff | raw | diff to current |
| 2010-04-01 |
Morgan Deters | reran update-copyright.pl to get new contributors and... |
blob | commitdiff | raw | diff to current |
| 2010-03-30 |
Morgan Deters | Highlights of this commit are: |
blob | commitdiff | raw | diff to current |
| 2010-03-25 |
Christopher L. Conway | Adding comments to NodeManager |
blob | commitdiff | raw | diff to current |
| 2010-03-16 |
Morgan Deters | * test/unit/Makefile.am, test/unit/expr/attribute_white.h, |
blob | commitdiff | raw | diff to current |
| 2010-03-11 |
Tim King | Added some hand generated UF tests. Unfortunartely... |
blob | commitdiff | raw | diff to current |
| 2010-03-05 |
Morgan Deters | * public/private code untangled (smt/smt_engine.h no... |
blob | commitdiff | raw | diff to current |
| 2010-03-04 |
Tim King | Committing a bug fix from Dejan. This resolves an issue... |
blob | commitdiff | raw | diff to current |
| 2010-03-01 |
Tim King | Added some documentation to theory_uf. |
blob | commitdiff | raw | diff to current |
| 2010-02-26 |
Morgan Deters | * test/unit/context/context_black.h: Test CDList<>... |
blob | commitdiff | raw | diff to current |
| 2010-02-26 |
Tim King | TheoryUFWhite tests are added. There are also accompany... |
blob | commitdiff | raw | diff to current |
| 2010-02-25 |
Tim King | Updated uf to reflect APPLY structure after conversatio... |
blob | commitdiff | raw | diff to current |
| 2010-02-25 |
Morgan Deters | * src/expr/node.h: add a copy constructor. Apparently... |
blob | commitdiff | raw | diff to current |
| 2010-02-24 |
Tim King | Cleaned up and documented ecdata and theory_uf. |
blob | commitdiff | raw | diff to current |
| 2010-02-24 |
Tim King | Committing small changes to attribute, and theory to... |
blob | commitdiff | raw | diff to current |
| 2010-02-22 |
Morgan Deters | * configure.ac: Remove doc/ from search path for Makefi... |
blob | commitdiff | raw | diff to current |
| 2010-02-17 |
Tim King | Initial draft of TheoryUF. Should compile without probl... |
blob | commitdiff | raw | diff to current |
|
projects / cvc5.git / history