| 2014-06-17 |
Morgan Deters | Fix rewriter typo. |
commit | commitdiff | tree |
| 2014-06-17 |
Morgan Deters | Clean up glpk detection a little, fix a detection bug. |
commit | commitdiff | tree |
| 2014-06-17 |
Morgan Deters | fix typo |
commit | commitdiff | tree |
| 2014-06-17 |
Morgan Deters | More application-track fixes for use with trace executor. |
commit | commitdiff | tree |
| 2014-06-17 |
Morgan Deters | Versioning preparation. |
commit | commitdiff | tree |
| 2014-06-17 |
Morgan Deters | Some fixes for tear-down-incremental and "success"... |
commit | commitdiff | tree |
| 2014-06-17 |
Morgan Deters | Disallow context-dependent copy/assignment. |
commit | commitdiff | tree |
| 2014-06-17 |
Morgan Deters | Fix compile errors with some versions of GCC. |
commit | commitdiff | tree |
| 2014-06-16 |
Morgan Deters | Clean up some compiler warnings on 32-bit. |
commit | commitdiff | tree |
| 2014-06-16 |
Morgan Deters | Minor fixes to get-abc script and configure stuff. |
commit | commitdiff | tree |
| 2014-06-16 |
Morgan Deters | get-glpk-cut-log script, and configure code. |
commit | commitdiff | tree |
| 2014-06-16 |
Morgan Deters | dos2unix-convert some sources. |
commit | commitdiff | tree |
| 2014-06-16 |
Morgan Deters | Minor fixes, spelling etc. |
commit | commitdiff | tree |
| 2014-06-16 |
ajreynol | More proof support for CASC : include skolemization |
commit | commitdiff | tree |
| 2014-06-16 |
Morgan Deters | minor update to application track config in QF_BV |
commit | commitdiff | tree |
| 2014-06-16 |
lianah | core solver fix |
commit | commitdiff | tree |
| 2014-06-16 |
Morgan Deters | Careful there aren't too many "success" messages with... |
commit | commitdiff | tree |
| 2014-06-16 |
lianah | fixed bv bug due to applying equisatisfiable transforma... |
commit | commitdiff | tree |
| 2014-06-15 |
Morgan Deters | Application trace executor (if they end up using that... |
commit | commitdiff | tree |
| 2014-06-15 |
Morgan Deters | One last(?) fix for build script for smtcomp uploads. |
commit | commitdiff | tree |
| 2014-06-15 |
lianah | fixed fuzzer assertion failures for bv |
commit | commitdiff | tree |
| 2014-06-15 |
Morgan Deters | fix travis config |
commit | commitdiff | tree |
| 2014-06-15 |
Morgan Deters | better bv args for smtcomp |
commit | commitdiff | tree |
| 2014-06-15 |
lianah | added rewriting to bv-pow2 pass |
commit | commitdiff | tree |
| 2014-06-15 |
lianah | Evil bitvector preprocessing pass for simplifying power... |
commit | commitdiff | tree |
| 2014-06-15 |
lianah | bv static learning and rewrites for power of 2 terms |
commit | commitdiff | tree |
| 2014-06-14 |
lianah | more bv rewrites |
commit | commitdiff | tree |
| 2014-06-14 |
lianah | fix to inequality rewrite |
commit | commitdiff | tree |
| 2014-06-14 |
lianah | fixed merge |
commit | commitdiff | tree |
| 2014-06-14 |
lianah | added bv inequality rewrite |
commit | commitdiff | tree |
| 2014-06-14 |
Liana Hadarean | added bv inequality lemmas |
commit | commitdiff | tree |
| 2014-06-14 |
Liana Hadarean | added bv inequality lemmas |
commit | commitdiff | tree |
| 2014-06-14 |
ajreynol | Fix for fmf with large finite cardinalities. |
commit | commitdiff | tree |
| 2014-06-13 |
lianah | fixed BVMinisat bug due to not clearing seen properly |
commit | commitdiff | tree |
| 2014-06-13 |
Morgan Deters | Doubly-ensure incremental is off in main track. Also... |
commit | commitdiff | tree |
| 2014-06-13 |
ajreynol | Fix handling of ALIA. |
commit | commitdiff | tree |
| 2014-06-13 |
Morgan Deters | update application track script too |
commit | commitdiff | tree |
| 2014-06-13 |
Clark Barrett | Update for QF_AUFLIA strategy |
commit | commitdiff | tree |
| 2014-06-13 |
Morgan Deters | Allow parallel failures when building competition versi... |
commit | commitdiff | tree |
| 2014-06-13 |
Morgan Deters | Adjust incremental run script for QF_AX too. |
commit | commitdiff | tree |
| 2014-06-12 |
Clark Barrett | Modified run script for QF_AX |
commit | commitdiff | tree |
| 2014-06-12 |
Clark Barrett | Modified run script for QF_LRA |
commit | commitdiff | tree |
| 2014-06-12 |
Morgan Deters | More make submission stuff |
commit | commitdiff | tree |
| 2014-06-12 |
lianah | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2014-06-12 |
lianah | fixing bv inequality solver explanation bug |
commit | commitdiff | tree |
| 2014-06-12 |
Morgan Deters | New application track script, new heuristics and all... |
commit | commitdiff | tree |
| 2014-06-12 |
lianah | added bvcomp case to bv to bool lifting |
commit | commitdiff | tree |
| 2014-06-12 |
Morgan Deters | more fix-ups |
commit | commitdiff | tree |
| 2014-06-12 |
lianah | added optionException for trying to use abc in an non... |
commit | commitdiff | tree |
| 2014-06-12 |
Morgan Deters | more smtcomp-submission script work |
commit | commitdiff | tree |
| 2014-06-11 |
Morgan Deters | Flush output stream after result printed in portfolio. |
commit | commitdiff | tree |
| 2014-06-11 |
Morgan Deters | Fix for competition mode + parallel. |
commit | commitdiff | tree |
| 2014-06-11 |
Morgan Deters | Fix parallel run script. |
commit | commitdiff | tree |
| 2014-06-11 |
lianah | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2014-06-11 |
lianah | switched bv equality order |
commit | commitdiff | tree |
| 2014-06-11 |
ajreynol | Update SMTCOMP script to handle all quantified logics. |
commit | commitdiff | tree |
| 2014-06-11 |
Morgan Deters | Fix an omission in bv sources. |
commit | commitdiff | tree |
| 2014-06-11 |
Morgan Deters | --best now implies --with-glpk --with-abc |
commit | commitdiff | tree |
| 2014-06-11 |
Morgan Deters | Some clean-up, post bv-merge. |
commit | commitdiff | tree |
| 2014-06-11 |
Kshitij Bansal | Merge pull request #31 from kbansal/sets |
commit | commitdiff | tree |
| 2014-06-11 |
lianah | fixed unit tests failures |
commit | commitdiff | tree |
| 2014-06-11 |
Kshitij Bansal | disable another test, after recent merges taking too... |
commit | commitdiff | tree |
| 2014-06-11 |
Kshitij Bansal | disable failing test |
commit | commitdiff | tree |
| 2014-06-11 |
Kshitij Bansal | sets: comment out an assertion too strong |
commit | commitdiff | tree |
| 2014-06-11 |
Kshitij Bansal | user/sat context issue in sets |
commit | commitdiff | tree |
| 2014-06-11 |
Kshitij Bansal | fix in sets rewriter |
commit | commitdiff | tree |
| 2014-06-11 |
lianah | fixing bv ackermanization cache bug |
commit | commitdiff | tree |
| 2014-06-10 |
Morgan Deters | Add new --pb-rewrites options to QF_LIA run script... |
commit | commitdiff | tree |
| 2014-06-10 |
Morgan Deters | Some news about API changes. |
commit | commitdiff | tree |
| 2014-06-10 |
Tim King | Merging Tim's pseudoboolean work from his fmcad14 branch. |
commit | commitdiff | tree |
| 2014-06-10 |
lianah | reverting portfolio hack |
commit | commitdiff | tree |
| 2014-06-10 |
lianah | Merging CAV14 paper bit-vector work. |
commit | commitdiff | tree |
| 2014-06-09 |
Morgan Deters | Disallow copy/assignment of SmtEngine. |
commit | commitdiff | tree |
| 2014-06-09 |
Morgan Deters | Tim's options for QF_LIA and QF_LRA---SOI+approx. |
commit | commitdiff | tree |
| 2014-06-09 |
Kshitij Bansal | Merge pull request #29 from kbansal/alternatefix |
commit | commitdiff | tree |
| 2014-06-09 |
Morgan Deters | Add missing set of braces, fixes --trace. |
commit | commitdiff | tree |
| 2014-06-09 |
Kshitij Bansal | parseErrorHelper : factor out whole word matching |
commit | commitdiff | tree |
| 2014-06-09 |
Kshitij Bansal | test for prvs commit (tokenize emptyset) |
commit | commitdiff | tree |
| 2014-06-09 |
Morgan Deters | Previous "repeat" fix required extra lookahead (leading... |
commit | commitdiff | tree |
| 2014-06-08 |
Kshitij Bansal | smt2 parser: tokenize emptyset only if theory enabled |
commit | commitdiff | tree |
| 2014-06-08 |
Morgan Deters | Better error when there are \backslashes in |quoted... |
commit | commitdiff | tree |
| 2014-06-08 |
Morgan Deters | Allow 'repeat' as an SMT-LIB user symbol name (UFNIA... |
commit | commitdiff | tree |
| 2014-06-08 |
Kshitij Bansal | sets translate: a different translation using axioms |
commit | commitdiff | tree |
| 2014-06-06 |
Kshitij Bansal | sets translator: fix for dags |
commit | commitdiff | tree |
| 2014-06-06 |
Kshitij Bansal | Merge pull request #28 from kbansal/sets |
commit | commitdiff | tree |
| 2014-06-06 |
Morgan Deters | Fix submission script (again). |
commit | commitdiff | tree |
| 2014-06-06 |
Kshitij Bansal | rm warning from helloworld example |
commit | commitdiff | tree |
| 2014-06-06 |
Tim King | Patch for the subtype theoryof mode to make the equalit... |
commit | commitdiff | tree |
| 2014-06-06 |
Kshitij Bansal | sets: fix equality propagation |
commit | commitdiff | tree |
| 2014-06-06 |
Kshitij Bansal | -{d,t} help => --show-{debug,trace}-tags |
commit | commitdiff | tree |
| 2014-06-06 |
Kshitij Bansal | option to hide stats which are zero (off by default... |
commit | commitdiff | tree |
| 2014-06-06 |
Kshitij Bansal | Sets translate, and other short fixes |
commit | commitdiff | tree |
| 2014-06-05 |
Morgan Deters | SMT-COMP version gets built --with-abc. |
commit | commitdiff | tree |
| 2014-06-05 |
Morgan Deters | Add --default-dag-thresh to translator, build translato... |
commit | commitdiff | tree |
| 2014-06-05 |
Morgan Deters | When printing in SMT, print N-ary bvadd/bvmul/concat... |
commit | commitdiff | tree |
| 2014-06-04 |
Morgan Deters | Add operator support (resolves bug #563). |
commit | commitdiff | tree |
| 2014-06-04 |
Morgan Deters | SmtEngine::checkModel() now checks that model values... |
commit | commitdiff | tree |
| 2014-06-04 |
Morgan Deters | Update commit # for get-abc script, anticipating Liana... |
commit | commitdiff | tree |
| 2014-06-04 |
Morgan Deters | Fix usability issue with tear-down incremental mode. |
commit | commitdiff | tree |
| 2014-06-04 |
Morgan Deters | SMT strict mode now disallows N-ary use of concat,... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog