| 2013-05-28 |
Morgan Deters | Standardize SMT-LIBv2 set of logics to use LogicInfo. |
commit | commitdiff | tree |
| 2013-05-21 |
Morgan Deters | Fix bug 512: an assertion failure only appearing with... |
commit | commitdiff | tree |
| 2013-05-21 |
Morgan Deters | Fix an error that valgrind found. |
commit | commitdiff | tree |
| 2013-05-21 |
Morgan Deters | Fix incremental bug in symmetry breaker. |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Fix error reporting on use of (nonlinear) div,mod,... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Update THANKS to mention David Cok's contributions. |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Detect multiply-defined :named annotations and issue... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Fix parsing of SMT-LIBv2 |quoted| symbols that span... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Compliance fixes for :named annotations: they must... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Don't allow get-model & co after a user push/pop |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | As per SMT-LIB standard: make - and xor take n>2 args... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Fix for equality-chaining of Booleans in SMT-LIBv2. |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Fix destruction issue in GetValueCommand leading to... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Better error on invalid logic strings. |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Better error on illegal (pop N); also more compliant... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | A couple of fixes to the get-option command for complia... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Disallow construction of (_ BitVec 0). |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Fixed "success" response to (push N) / (pop N) with... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Fix to empty response to (get-assignment). |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | configure fix for building with glpk on redhat, perhaps... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | minor changes to language bindings |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | disable Logic-checking with finite model finding for... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Fix erroneous results when the logic was incorrectly... |
commit | commitdiff | tree |
| 2013-05-08 |
Morgan Deters | Prerelease versioning for 1.2.x |
commit | commitdiff | tree |
| 2013-05-08 |
Morgan Deters | Merge tag 'smteval2013' |
commit | commitdiff | tree |
| 2013-05-08 |
Morgan Deters | Cutting release 1.2. |
commit | commitdiff | tree |
| 2013-05-08 |
Morgan Deters | Removing arithmetic compile warning for release |
commit | commitdiff | tree |
| 2013-05-08 |
Morgan Deters | update versioning |
commit | commitdiff | tree |
| 2013-05-08 |
Morgan Deters | final updates for smt-eval script |
commit | commitdiff | tree |
| 2013-05-08 |
Clark Barrett | Fixed assertion bug |
commit | commitdiff | tree |
| 2013-05-08 |
Morgan Deters | fix for smt-eval run script |
commit | commitdiff | tree |
| 2013-05-07 |
Morgan Deters | BV strategy for SMT-EVAL |
commit | commitdiff | tree |
| 2013-05-07 |
Morgan Deters | fix for nonterminating model-based array loop |
commit | commitdiff | tree |
| 2013-05-07 |
lianah | added type checking rule to check for bit-vector consta... |
commit | commitdiff | tree |
| 2013-05-07 |
lianah | one more fix for rewrites |
commit | commitdiff | tree |
| 2013-05-07 |
lianah | fixed bv rewrite blow-up |
commit | commitdiff | tree |
| 2013-05-07 |
Dejan Jovanović | fix for bug500 |
commit | commitdiff | tree |
| 2013-05-07 |
Tim King | Fixes a bug with arithmetic's new attempt solution... |
commit | commitdiff | tree |
| 2013-05-07 |
Tim King | Improving arithmetic debugging output. |
commit | commitdiff | tree |
| 2013-05-07 |
Tim King | Disabling an incorrect prototyping line from the simple... |
commit | commitdiff | tree |
| 2013-05-07 |
Morgan Deters | Change SMT-EVAL run-script to use Tim's best QF_LRA... |
commit | commitdiff | tree |
| 2013-05-07 |
Liana Hadarean | fixed bv rewrite rule bug |
commit | commitdiff | tree |
| 2013-05-06 |
Morgan Deters | Removing excess verbosity from ApproxSimplex (after... |
commit | commitdiff | tree |
| 2013-05-06 |
Tim King | Adding a heuristic for guessing an optimization functio... |
commit | commitdiff | tree |
| 2013-05-06 |
Tim King | Disables justification stop only for LRA if the problem... |
commit | commitdiff | tree |
| 2013-05-06 |
Clark Barrett | Some bug fixes for mb arrays |
commit | commitdiff | tree |
| 2013-05-05 |
Tim King | Adding cut offs for likely integer infeasible paths. |
commit | commitdiff | tree |
| 2013-05-04 |
Tim King | Adding a smarter technique for pivoting in solutions... |
commit | commitdiff | tree |
| 2013-05-03 |
Tim King | Fixing compilation of unit tests. These problems were... |
commit | commitdiff | tree |
| 2013-05-03 |
Tim King | More misc. arithmetic cleanup. Removing unused files... |
commit | commitdiff | tree |
| 2013-05-03 |
Tim King | Code cleanup. Reducing misc. warnings in arithmetic. |
commit | commitdiff | tree |
| 2013-05-03 |
Tim King | Removing arithmetic legacy code and unifying functions. |
commit | commitdiff | tree |
| 2013-05-03 |
Tim King | Fixing a debug typo. |
commit | commitdiff | tree |
| 2013-05-03 |
Tim King | Merging branch 'soiquickexplain'. |
commit | commitdiff | tree |
| 2013-05-03 |
Tim King | Merge branch 'fcexplanations' |
commit | commitdiff | tree |
| 2013-05-02 |
Tim King | Adding quick explain for soi simplex. |
commit | commitdiff | tree |
| 2013-05-02 |
Dejan Jovanović | * splitLemma to request atoms |
commit | commitdiff | tree |
| 2013-05-02 |
lianah | merged master |
commit | commitdiff | tree |
| 2013-05-02 |
lianah | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2013-05-01 |
Morgan Deters | Comment out some debug-related things in attribute... |
commit | commitdiff | tree |
| 2013-05-01 |
Morgan Deters | Fix to dumping re: boolean terms, datatypes |
commit | commitdiff | tree |
| 2013-05-01 |
Morgan Deters | Fix to boolean-terms; resolves bug #507 |
commit | commitdiff | tree |
| 2013-05-01 |
lianah | removed tracing code causing slowdown; cleaned up some... |
commit | commitdiff | tree |
| 2013-05-01 |
Tim King | Working on the new explanation system. |
commit | commitdiff | tree |
| 2013-05-01 |
lianah | added back BitwiseEq rule |
commit | commitdiff | tree |
| 2013-05-01 |
Morgan Deters | Adding a missing makefile to the dist (fixes distcheck) |
commit | commitdiff | tree |
| 2013-04-30 |
Tim King | Making propagation more conversative. |
commit | commitdiff | tree |
| 2013-04-30 |
Tim King | Draft of the new propagation code. |
commit | commitdiff | tree |
| 2013-04-30 |
lianah | fixed merge conflicts |
commit | commitdiff | tree |
| 2013-04-30 |
lianah | merged cvc4 master |
commit | commitdiff | tree |
| 2013-04-30 |
lianah | updated the author name |
commit | commitdiff | tree |
| 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 |
lianah | updated the author name |
commit | commitdiff | tree |
| 2013-04-30 |
Andrew Reynolds | Add option in quantifiers for clause splitting |
commit | commitdiff | tree |
| 2013-04-30 |
lianah | added several rewrite rules (BitwiseSlicing, Ule/SleEli... |
commit | commitdiff | tree |
| 2013-04-30 |
Kshitij Bansal | add decision_attributes.h for make dist |
commit | commitdiff | tree |
| 2013-04-30 |
Tim King | Adding has bound counts and tracking for rows. |
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 |
lianah | added bvule, bvsle operator elimination rulesl; added... |
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-21 |
lianah | added some bv rewrite rules |
commit | commitdiff | tree |
| 2013-04-18 |
lianah | Merge branch 'master' of https://github.com/CVC4/CVC4 |
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 |
| next |
projects / cvc5.git / shortlog