| 2013-04-30 |
lianah | added several rewrite rules (BitwiseSlicing, Ule/SleEli... |
commit | commitdiff | tree |
| 2013-04-30 |
lianah | added bvule, bvsle operator elimination rulesl; added... |
commit | commitdiff | tree |
| 2013-04-30 |
lianah | added some bv rewrite rules |
commit | commitdiff | tree |
| 2013-04-30 |
lianah | innd examples are solved fast, but destruction assertio... |
commit | commitdiff | tree |
| 2013-04-30 |
Liana Hadarean | fixed compile error |
commit | commitdiff | tree |
| 2013-04-30 |
lianah | uncompiling new bv to bool lifting |
commit | commitdiff | tree |
| 2013-04-30 |
lianah | finished implementing bv to bool lifting and added... |
commit | commitdiff | tree |
| 2013-04-30 |
Liana Hadarean | more work on boolean lifting |
commit | commitdiff | tree |
| 2013-04-30 |
lianah | started work on bv1 to boolean lifting |
commit | commitdiff | tree |
| 2013-04-30 |
lianah | added support for dumping the SAT problem the sat solve... |
commit | commitdiff | tree |
| 2013-04-30 |
Andrew Reynolds | Add option in quantifiers for clause splitting |
commit | commitdiff | tree |
| 2013-04-30 |
Kshitij Bansal | add decision_attributes.h for make dist |
commit | commitdiff | tree |
| 2013-04-29 |
Morgan Deters | Some fixes for GCC 4.2, and for Java on Mac |
commit | commitdiff | tree |
| 2013-04-29 |
Kshitij Bansal | Merge pull request #9 from kbansal/master |
commit | commitdiff | tree |
| 2013-04-29 |
Morgan Deters | Fixes to FCSimplex for some versions of compilers |
commit | commitdiff | tree |
| 2013-04-28 |
Tim King | Fixing the failure for make distcheck. |
commit | commitdiff | tree |
| 2013-04-26 |
Kshitij Bansal | Merge experimental decisionweight branch |
commit | commitdiff | tree |
| 2013-04-26 |
Tim King | FCSimplex branch merge |
commit | commitdiff | tree |
| 2013-04-25 |
Morgan Deters | Add ability to run different regression levels with... |
commit | commitdiff | tree |
| 2013-04-24 |
Morgan Deters | Theory "alternates" support |
commit | commitdiff | tree |
| 2013-04-22 |
Morgan Deters | add bit0 and bit1 constants to smt-lib v1 parser |
commit | commitdiff | tree |
| 2013-04-18 |
lianah | making sure sat context is zero when user context is... |
commit | commitdiff | tree |
| 2013-04-18 |
lianah | fixing destruction order in SmtEngine |
commit | commitdiff | tree |
| 2013-04-17 |
Kshitij Bansal | bool flatten: node num_children workaround |
commit | commitdiff | tree |
| 2013-04-17 |
Kshitij Bansal | boolean flatten: bug fix in dfs search |
commit | commitdiff | tree |
| 2013-04-17 |
Kshitij Bansal | boolean flatten rewrite: dont re-rewrite |
commit | commitdiff | tree |
| 2013-04-17 |
Kshitij Bansal | generalize to handle and |
commit | commitdiff | tree |
| 2013-04-16 |
Kshitij Bansal | flatten or nodes |
commit | commitdiff | tree |
| 2013-04-11 |
Clark Barrett | Improved speed of no redundant lemma assertion by using... |
commit | commitdiff | tree |
| 2013-04-11 |
Clark Barrett | Fixes for getModelVal in bv theory |
commit | commitdiff | tree |
| 2013-04-11 |
Clark Barrett | Added check for infinite lemma loop |
commit | commitdiff | tree |
| 2013-04-11 |
lianah | fixed getModelValue to only query the value of leaves... |
commit | commitdiff | tree |
| 2013-04-09 |
Morgan Deters | Change TPTP parser to not use the STRING type; this... |
commit | commitdiff | tree |
| 2013-04-05 |
Morgan Deters | Fix unit test (compile error) for new SatSolver interface |
commit | commitdiff | tree |
| 2013-04-03 |
Dejan Jovanović | * changing the bitblast-eager to bitblast on pre-register |
commit | commitdiff | tree |
| 2013-04-03 |
Morgan Deters | Prerelease versioning for master. |
commit | commitdiff | tree |
| 2013-04-03 |
Morgan Deters | Pre-release versioning |
commit | commitdiff | tree |
| 2013-04-03 |
Morgan Deters | Cutting release 1.1. |
commit | commitdiff | tree |
| 2013-04-03 |
Morgan Deters | Some final minor changes before cutting 1.1. |
commit | commitdiff | tree |
| 2013-04-03 |
Liana Hadarean | updated NEWS to include inequality solver |
commit | commitdiff | tree |
| 2013-04-03 |
Andrew Reynolds | abort quantifiers check if master equality engine is... |
commit | commitdiff | tree |
| 2013-04-02 |
Tim King | Making arithmetic model reversion on unsat checks an... |
commit | commitdiff | tree |
| 2013-04-02 |
Morgan Deters | Regenerated copyrights: canonicalized names, no emails |
commit | commitdiff | tree |
| 2013-04-02 |
Morgan Deters | Remove old README file from rewrite-rules left over... |
commit | commitdiff | tree |
| 2013-04-02 |
Morgan Deters | Fix get-authors script to not extract email addresses... |
commit | commitdiff | tree |
| 2013-04-02 |
Morgan Deters | One final fix to "make submission" rule |
commit | commitdiff | tree |
| 2013-04-02 |
Morgan Deters | update copyrights |
commit | commitdiff | tree |
| 2013-04-02 |
Morgan Deters | Adjust release Makefile rules, new run script |
commit | commitdiff | tree |
| 2013-04-02 |
Clark Barrett | Fix regression error by turning off model-based solver... |
commit | commitdiff | tree |
| 2013-04-02 |
Clark Barrett | Turning on model based array solver for QF_AX |
commit | commitdiff | tree |
| 2013-04-02 |
Clark Barrett | Made eager lemmas an option, enabled for QF_AX |
commit | commitdiff | tree |
| 2013-04-02 |
Clark Barrett | Disabling eager array index splitting for QF_AX |
commit | commitdiff | tree |
| 2013-04-02 |
Morgan Deters | Fixes for two bugs: |
commit | commitdiff | tree |
| 2013-04-01 |
Tim King | Cleaning up the demand restart code. |
commit | commitdiff | tree |
| 2013-04-01 |
Tim King | Adding a restart test strategy to integers. |
commit | commitdiff | tree |
| 2013-04-01 |
Tim King | Adding demand restart. |
commit | commitdiff | tree |
| 2013-04-01 |
Tim King | Adding tests for the previous commit. |
commit | commitdiff | tree |
| 2013-04-01 |
Morgan Deters | Merging some cleanup work: |
commit | commitdiff | tree |
| 2013-04-01 |
Tim King | Fix for iff terms over equalities between the same... |
commit | commitdiff | tree |
| 2013-04-01 |
Morgan Deters | Fix bug 491 and related issues with checkModel() and... |
commit | commitdiff | tree |
| 2013-04-01 |
lianah | fixed TheoryBool rewriter bug |
commit | commitdiff | tree |
| 2013-04-01 |
lianah | fixed bug 502; now the core bv solver only gives the... |
commit | commitdiff | tree |
| 2013-03-31 |
Liana Hadarean | changed option to run inequality solver by default |
commit | commitdiff | tree |
| 2013-03-31 |
Clark Barrett | Disabling eager array index splitting for QF_AUFLIA |
commit | commitdiff | tree |
| 2013-03-30 |
Andrew Reynolds | do simple ite rewriting within quantifiers |
commit | commitdiff | tree |
| 2013-03-29 |
Morgan Deters | make Boolean term conversion partially non-recursive... |
commit | commitdiff | tree |
| 2013-03-29 |
Dejan Jovanović | Merge branch 'master' of github.com:CVC4/CVC4 |
commit | commitdiff | tree |
| 2013-03-29 |
Dejan Jovanović | removing cryptominisat since we're not using it |
commit | commitdiff | tree |
| 2013-03-28 |
Morgan Deters | fix memory corruption in arrays destructor |
commit | commitdiff | tree |
| 2013-03-28 |
Morgan Deters | some Java bindings fixes (fixes Debian build problems) |
commit | commitdiff | tree |
| 2013-03-28 |
Clark Barrett | Fixed a warning, made eager-index default to true ... |
commit | commitdiff | tree |
| 2013-03-28 |
Clark Barrett | Fixed bug in arrays |
commit | commitdiff | tree |
| 2013-03-28 |
Clark Barrett | Added assertion |
commit | commitdiff | tree |
| 2013-03-28 |
Clark Barrett | Updates to model-based array solver |
commit | commitdiff | tree |
| 2013-03-28 |
Clark Barrett | New model-based array procedure |
commit | commitdiff | tree |
| 2013-03-27 |
lianah | reverted the core solver to do static slicing, added... |
commit | commitdiff | tree |
| 2013-03-27 |
lianah | fixed inequality checkDisequalities inefficiency |
commit | commitdiff | tree |
| 2013-03-27 |
lianah | Merge branch 'master' into bv-core |
commit | commitdiff | tree |
| 2013-03-27 |
lianah | fixed some model stuff |
commit | commitdiff | tree |
| 2013-03-27 |
lianah | fixed model generation bug; commented out attempt... |
commit | commitdiff | tree |
| 2013-03-27 |
lianah | inequality solver now only splits on disequalities... |
commit | commitdiff | tree |
| 2013-03-27 |
lianah | added model generation for bv subtheories and bv-inequa... |
commit | commitdiff | tree |
| 2013-03-26 |
Morgan Deters | Fixes for warnings from clang++, from -std=gnu++0x... |
commit | commitdiff | tree |
| 2013-03-26 |
Morgan Deters | Make --incremental the default when running interactively |
commit | commitdiff | tree |
| 2013-03-26 |
lianah | core theory currently disabled |
commit | commitdiff | tree |
| 2013-03-26 |
Dejan Jovanović | getModelValue implementation in bitvectors |
commit | commitdiff | tree |
| 2013-03-26 |
Dejan Jovanović | adding |
commit | commitdiff | tree |
| 2013-03-26 |
Dejan Jovanović | Merge branch 'master' of git@github.com:CVC4/CVC4.git |
commit | commitdiff | tree |
| 2013-03-26 |
Dejan Jovanović | moving bv before arrays |
commit | commitdiff | tree |
| 2013-03-26 |
lianah | fixed inequality bugs due to improper explanation |
commit | commitdiff | tree |
| 2013-03-26 |
lianah | cleaned up the bv subtheory interface; added check... |
commit | commitdiff | tree |
| 2013-03-26 |
Morgan Deters | java input stream adapters working |
commit | commitdiff | tree |
| 2013-03-25 |
lianah | getEqualityStatus now also queries the inequality solver |
commit | commitdiff | tree |
| 2013-03-25 |
Morgan Deters | Fix for SCM detection |
commit | commitdiff | tree |
| 2013-03-25 |
Kshitij Bansal | Merge pull request #7 from kbansal/portfolio |
commit | commitdiff | tree |
| 2013-03-25 |
Kshitij Bansal | finish removal of separateOutput |
commit | commitdiff | tree |
| 2013-03-25 |
Liana Hadarean | added support for disequalities in the inequality solver |
commit | commitdiff | tree |
| 2013-03-24 |
lianah | incremental inequality solver implemented |
commit | commitdiff | tree |
| 2013-03-24 |
Morgan Deters | Fix bug in portfolio executor output; fixes nightly... |
commit | commitdiff | tree |
| 2013-03-23 |
lianah | non-incremental inequality solver seems to be bug-free... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog