Age | Commit message (Expand) | Author |
2013-05-03 | More misc. arithmetic cleanup. Removing unused files and functions. Also remo... | Tim King |
2013-05-03 | Code cleanup. Reducing misc. warnings in arithmetic. | Tim King |
2013-05-03 | Removing arithmetic legacy code and unifying functions. | Tim King |
2013-05-03 | Fixing a debug typo. | Tim King |
2013-05-03 | Merging branch 'soiquickexplain'. | Tim King |
2013-05-03 | Merge branch 'fcexplanations' | Tim King |
2013-05-02 | Adding quick explain for soi simplex. | Tim King |
2013-05-02 | * splitLemma to request atoms | Dejan Jovanović |
2013-05-02 | merged master | lianah |
2013-05-02 | Merge branch 'master' of https://github.com/CVC4/CVC4 | lianah |
2013-05-01 | Comment out some debug-related things in attribute code, no longer needed | Morgan Deters |
2013-05-01 | Fix to dumping re: boolean terms, datatypes | Morgan Deters |
2013-05-01 | Fix to boolean-terms; resolves bug #507 | Morgan Deters |
2013-05-01 | removed tracing code causing slowdown; cleaned up some code | lianah |
2013-05-01 | Working on the new explanation system. | Tim King |
2013-05-01 | added back BitwiseEq rule | lianah |
2013-04-30 | Making propagation more conversative. | Tim King |
2013-04-30 | Draft of the new propagation code. | Tim King |
2013-04-30 | fixed merge conflicts | lianah |
2013-04-30 | merged cvc4 master | lianah |
2013-04-30 | updated the author name | lianah |
2013-04-30 | added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ExtractSignExt... | lianah |
2013-04-30 | added bvule, bvsle operator elimination rulesl; added bvurem lemma generation | lianah |
2013-04-30 | added some bv rewrite rules | lianah |
2013-04-30 | innd examples are solved fast, but destruction assertion fail | lianah |
2013-04-30 | fixed compile error | Liana Hadarean |
2013-04-30 | uncompiling new bv to bool lifting | lianah |
2013-04-30 | finished implementing bv to bool lifting and added --bv-to-bool option | lianah |
2013-04-30 | more work on boolean lifting | Liana Hadarean |
2013-04-30 | started work on bv1 to boolean lifting | lianah |
2013-04-30 | added support for dumping the SAT problem the sat solver is working on | lianah |
2013-04-30 | updated the author name | lianah |
2013-04-30 | Add option in quantifiers for clause splitting | Andrew Reynolds |
2013-04-30 | added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ExtractSignExt... | lianah |
2013-04-30 | add decision_attributes.h for make dist | Kshitij Bansal |
2013-04-30 | Adding has bound counts and tracking for rows. | Tim King |
2013-04-29 | Some fixes for GCC 4.2, and for Java on Mac | Morgan Deters |
2013-04-29 | Merge pull request #9 from kbansal/master | Kshitij Bansal |
2013-04-29 | Fixes to FCSimplex for some versions of compilers | Morgan Deters |
2013-04-28 | Fixing the failure for make distcheck. | Tim King |
2013-04-26 | Merge experimental decisionweight branch | Kshitij Bansal |
2013-04-26 | FCSimplex branch merge | Tim King |
2013-04-25 | added bvule, bvsle operator elimination rulesl; added bvurem lemma generation | lianah |
2013-04-23 | Theory "alternates" support | Morgan Deters |
2013-04-22 | add bit0 and bit1 constants to smt-lib v1 parser | Morgan Deters |
2013-04-21 | added some bv rewrite rules | lianah |
2013-04-18 | Merge branch 'master' of https://github.com/CVC4/CVC4 | lianah |
2013-04-18 | making sure sat context is zero when user context is popped to 0 in SmtEngine... | lianah |
2013-04-18 | fixing destruction order in SmtEngine | lianah |
2013-04-17 | bool flatten: node num_children workaround | Kshitij Bansal |