| 2018-05-18 |
Andrew Reynolds | Cache isInterpretedFinite (#1943) |
blob | commitdiff | raw |
| 2018-04-11 |
Andrew Reynolds | Properly implement function extensionality based on... |
blob | commitdiff | raw | diff to current |
| 2018-01-27 |
Tim King | Removing structurally dead code. (#1540) |
blob | commitdiff | raw | diff to current |
| 2017-10-11 |
Andrew Reynolds | Ho node manager types (#1203) |
blob | commitdiff | raw | diff to current |
| 2017-09-14 |
Andrew Reynolds | Remove unhandled subtypes (#1098) |
blob | commitdiff | raw | diff to current |
| 2017-07-21 |
Tim King | Merge branch 'master' into cleanup-regexp |
blob | commitdiff | raw | diff to current |
| 2017-07-21 |
Tim King | Moving from the gnu extensions for hash maps to the... |
blob | commitdiff | raw | diff to current |
| 2017-07-13 |
Aina Niemetz | Merge pull request #188 from aniemetz/cx11 |
blob | commitdiff | raw | diff to current |
| 2017-07-12 |
ajreynol | Make type rules more strict for operators whose type... |
blob | commitdiff | raw | diff to current |
| 2017-07-07 |
Mathias Preiner | Update copyright headers. |
blob | commitdiff | raw | diff to current |
| 2017-04-21 |
Clark Barrett | Merge pull request #150 from 4tXJ7f/check_exceptions2 |
blob | commitdiff | raw | diff to current |
| 2017-04-21 |
ajreynol | Handle subtypes in sets. Bug fixes for tuples with... |
blob | commitdiff | raw | diff to current |
| 2016-12-02 |
Tim King | Merge pull request #95 from 4tXJ7f/fix_sierra_build |
blob | commitdiff | raw | diff to current |
| 2016-12-02 |
Clark Barrett | Merge pull request #113 from 4tXJ7f/remove_extract_rule |
blob | commitdiff | raw | diff to current |
| 2016-12-02 |
ajreynol | Bug fixes and refactoring of parametric datatypes,... |
blob | commitdiff | raw | diff to current |
| 2016-10-31 |
ajreynol | Minor refactoring in preparation for datatypes node... |
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-23 |
ajreynol | Fix related to parametric sorts whose interpretation... |
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-02-18 |
ajreynol | Correct subtyping for arrays, disable subtyping for... |
blob | commitdiff | raw | diff to current |
| 2016-02-16 |
ajreynol | More simplification to internal implementation of tuple... |
blob | commitdiff | raw | diff to current |
| 2016-02-15 |
PaulMeng | Merge remote-tracking branch 'origin/master' |
blob | commitdiff | raw | diff to current |
| 2016-02-15 |
ajreynol | Eliminate most of the internal representation infrastru... |
blob | commitdiff | raw | diff to current |
| 2015-12-30 |
Tim King | Shuffling around public vs. private headers |
blob | commitdiff | raw | diff to current |
| 2015-12-15 |
Tim King | Breaking the include cycle between Record and Expr. |
blob | commitdiff | raw | diff to current |
| 2015-12-15 |
Tim King | Removing the build cycle for predicate. |
blob | commitdiff | raw | diff to current |
| 2015-08-19 |
Kshitij Bansal | fix bug 605 |
blob | commitdiff | raw | diff to current |
| 2015-05-12 |
barrettcw | Merge pull request #74 from finnhaedicke/namespace_minisat |
blob | commitdiff | raw | diff to current |
| 2015-04-23 |
Clark Barrett | Merge branch 'master' into google |
blob | commitdiff | raw | diff to current |
| 2015-04-21 |
Clark Barrett | Changes needed to compile at Google, plus some bug... |
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-06 |
Tim King | Merge pull request #21 from pcc/ite-fix |
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-21 |
Kshitij Bansal | Merge pull request #22 from kbansal/sets-model |
blob | commitdiff | raw | diff to current |
| 2014-03-20 |
Kshitij Bansal | push subtyping for sets to the element type |
blob | commitdiff | raw | diff to current |
| 2013-12-03 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2013-12-03 |
Morgan Deters | Minor cleanup. |
blob | commitdiff | raw | diff to current |
| 2013-12-03 |
Morgan Deters | Support for parametric datatype subtyping, so that... |
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-09-30 |
Liana Hadarean | merged golden |
blob | commitdiff | raw | diff to current |
| 2013-08-26 |
Kshitij Bansal | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
| 2013-06-27 |
Morgan Deters | Remove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_publ... |
blob | commitdiff | raw | diff to current |
| 2013-06-08 |
Morgan Deters | Fixes for Boolean terms in arrays (including fix for... |
blob | commitdiff | raw | diff to current |
| 2013-06-07 |
Morgan Deters | Fix for bug 517. |
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-27 |
lianah | added model generation for bv subtheories and bv-inequa... |
blob | commitdiff | raw | diff to current |
| 2013-03-23 |
Dejan Jovanović | Merge remote-tracking branch 'dddejan/c++11' |
blob | commitdiff | raw | diff to current |
| 2013-03-22 |
Morgan Deters | Support for Boolean term conversion in datatypes. |
blob | commitdiff | raw | diff to current |
| 2012-11-27 |
Morgan Deters | Tuples and records merge. Resolves bug 270. |
blob | commitdiff | raw | diff to current |
| 2012-11-08 |
Morgan Deters | Review of trunk r4525 (TypeNode::getBaseType()): |
blob | commitdiff | raw | diff to current |
| 2012-11-08 |
Clark Barrett | Added getBaseType - Morgan please check |
blob | commitdiff | raw | diff to current |
| 2012-10-11 |
Morgan Deters | Standardizing copyright notice. Touches **ALL** source... |
blob | commitdiff | raw | diff to current |
| 2012-09-26 |
Morgan Deters | Finish off SEXPR kind work. |
blob | commitdiff | raw | diff to current |
| 2012-09-26 |
Morgan Deters | The Tuesday Afternoon Catch-All Commit (TACAC): |
blob | commitdiff | raw | diff to current |
| 2012-08-28 |
Morgan Deters | Improved compatibility layer, now supports quantifiers... |
blob | commitdiff | raw | diff to current |
| 2012-05-18 |
Tim King | This commit adds TypeNode::leastCommonTypeNode(). ... |
blob | commitdiff | raw | diff to current |
| 2012-05-18 |
Tim King | This commit removes the dead psuedoboolean code. |
blob | commitdiff | raw | diff to current |
| 2012-05-15 |
Morgan Deters | Implement TypeNode::isComparableTo() and add a unit... |
blob | commitdiff | raw | diff to current |
| 2012-03-01 |
Morgan Deters | Partial merge from kind-backend branch, including Minis... |
blob | commitdiff | raw | diff to current |
| 2011-11-04 |
Morgan Deters | STRING_TYPE and CONST_STRING and associate type infrast... |
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-09-02 |
Morgan Deters | Partial merge of integers work; this is simple B&B... |
blob | commitdiff | raw | diff to current |
| 2011-06-01 |
Morgan Deters | minor fix, and better output for type errors |
blob | commitdiff | raw | diff to current |
| 2011-06-01 |
Morgan Deters | type ascriptions (casts) for parameterized datatypes... |
blob | commitdiff | raw | diff to current |
| 2011-05-14 |
Morgan Deters | add AscriptionType stuff to support nullary parameteriz... |
blob | commitdiff | raw | diff to current |
| 2011-05-13 |
Andrew Reynolds | added support for parametric datatypes, updated cvc... |
blob | commitdiff | raw | diff to current |
| 2011-05-05 |
Morgan Deters | Merge from nonclausal-simplification-v2 branch: |
blob | commitdiff | raw | diff to current |
| 2011-04-25 |
Morgan Deters | Monday tasks: |
blob | commitdiff | raw | diff to current |
| 2011-04-25 |
Morgan Deters | Weekend work. The main points: |
blob | commitdiff | raw | diff to current |
| 2011-04-20 |
Morgan Deters | Tuesday end-of-day commit. |
blob | commitdiff | raw | diff to current |
| 2011-04-18 |
Morgan Deters | Partial merge from datatypes-merge branch: |
blob | commitdiff | raw | diff to current |
| 2010-10-07 |
Morgan Deters | SMT-LIBv2 (define-fun...) command now functional; does... |
blob | commitdiff | raw | diff to current |
| 2010-10-06 |
Morgan Deters | declare-sort, define-sort working but not thoroughly... |
blob | commitdiff | raw | diff to current |
| 2010-10-04 |
Morgan Deters | remove/shuffle some #include dependencies; fix some... |
blob | commitdiff | raw | diff to current |
| 2010-08-17 |
Morgan Deters | Merge from "cc" branch: |
blob | commitdiff | raw | diff to current |
| 2010-07-02 |
Morgan Deters | re-generated comment headers of source files |
blob | commitdiff | raw | diff to current |
| 2010-07-02 |
Morgan Deters | * Added white-box TheoryEngine test that tests the... |
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-21 |
Tim King | Small fixes to TheoryArith. Added a hack to make Integ... |
blob | commitdiff | raw | diff to current |
| 2010-05-02 |
Dejan Jovanović | smt parser for bit-vectors |
blob | commitdiff | raw | diff to current |
| 2010-04-29 |
Dejan Jovanović | Added the capability to construct expressions by passin... |
blob | commitdiff | raw | diff to current |
| 2010-04-26 |
Dejan Jovanović | Some cleanup. Also added the integer and real types. |
blob | commitdiff | raw | diff to current |
| 2010-04-26 |
Dejan Jovanović | Adding the intermediary TypeNode to represent (and... |
blob | commitdiff | raw | diff to current |
|
projects / cvc5.git / history