| 2013-10-09 |
lianah | cleaned up proof code |
commit | commitdiff | tree |
| 2013-10-09 |
lianah | fixed uf proof bug: now storing deleted theory lemmas |
commit | commitdiff | tree |
| 2013-10-08 |
lianah | added currying for uf proofs; still needs debugging |
commit | commitdiff | tree |
| 2013-10-08 |
lianah | fixed uf proof with holes bugs |
commit | commitdiff | tree |
| 2013-10-08 |
Liana Hadarean | fixed some bugs |
commit | commitdiff | tree |
| 2013-10-08 |
Liana Hadarean | first draft implementation of uf proofs with holes |
commit | commitdiff | tree |
| 2013-10-07 |
Liana Hadarean | merged golden |
commit | commitdiff | tree |
| 2013-10-07 |
Andrew Reynolds | Multiple fixes for datatypes theory solver: add support... |
commit | commitdiff | tree |
| 2013-10-03 |
Tianyi Liang | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2013-10-03 |
Andrew Reynolds | Adding example proof signatures for LFSC. |
commit | commitdiff | tree |
| 2013-10-03 |
Andrew Reynolds | Added support for converting unsorted problems to multi... |
commit | commitdiff | tree |
| 2013-10-03 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2013-10-03 |
Tianyi Liang | adds some fixes. it solves kaluza problems |
commit | commitdiff | tree |
| 2013-10-03 |
Andrew Reynolds | Adding example proof signatures for LFSC. |
commit | commitdiff | tree |
| 2013-10-02 |
Andrew Reynolds | Added support for converting unsorted problems to multi... |
commit | commitdiff | tree |
| 2013-10-02 |
Tianyi Liang | adds partial function substr. the use of this function... |
commit | commitdiff | tree |
| 2013-10-02 |
Tianyi Liang | adds partial function substr. the use of this function... |
commit | commitdiff | tree |
| 2013-10-01 |
Andrew Reynolds | Fix a bug in smt2 parser for quantified formulas with... |
commit | commitdiff | tree |
| 2013-10-01 |
Tianyi Liang | replace with a new method for disequality, move to... |
commit | commitdiff | tree |
| 2013-09-30 |
Tianyi Liang | add x=y |
commit | commitdiff | tree |
| 2013-09-30 |
Tianyi Liang | fixed a loop bug |
commit | commitdiff | tree |
| 2013-09-30 |
Liana Hadarean | merged golden |
commit | commitdiff | tree |
| 2013-09-30 |
Andrew Reynolds | Bug fixes and improvements for symmetry breaking, it... |
commit | commitdiff | tree |
| 2013-09-27 |
Morgan Deters | Some fixes to recent strings commits. |
commit | commitdiff | tree |
| 2013-09-27 |
Morgan Deters | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2013-09-27 |
Tianyi Liang | adds communication with arith engine |
commit | commitdiff | tree |
| 2013-09-27 |
Andrew Reynolds | Add new symmetry breaking technique for finite model... |
commit | commitdiff | tree |
| 2013-09-27 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2013-09-27 |
Tianyi Liang | removes unsound cases, adds unrolling |
commit | commitdiff | tree |
| 2013-09-27 |
Tianyi Liang | fix the infinite issue |
commit | commitdiff | tree |
| 2013-09-27 |
Tianyi Liang | for morgan to see the regression problems |
commit | commitdiff | tree |
| 2013-09-27 |
Tianyi Liang | fix loop detection for multi-vars |
commit | commitdiff | tree |
| 2013-09-27 |
Tianyi Liang | optimizing model generation for strings |
commit | commitdiff | tree |
| 2013-09-27 |
Tianyi Liang | adds model generation for strings, and a hacked way... |
commit | commitdiff | tree |
| 2013-09-27 |
Tianyi Liang | removes unsound cases, adds unrolling |
commit | commitdiff | tree |
| 2013-09-25 |
Tianyi Liang | fix the infinite issue |
commit | commitdiff | tree |
| 2013-09-25 |
Tianyi Liang | for morgan to see the regression problems |
commit | commitdiff | tree |
| 2013-09-24 |
Clark Barrett | Reduce compiler dependencies on substitutions.h, |
commit | commitdiff | tree |
| 2013-09-24 |
Clark Barrett | Better fix for bug 528 |
commit | commitdiff | tree |
| 2013-09-24 |
Tianyi Liang | fix loop detection for multi-vars |
commit | commitdiff | tree |
| 2013-09-24 |
Tianyi Liang | optimizing model generation for strings |
commit | commitdiff | tree |
| 2013-09-24 |
Tianyi Liang | adds model generation for strings, and a hacked way... |
commit | commitdiff | tree |
| 2013-09-23 |
Morgan Deters | Revert Clark's last commit, at his request; there are... |
commit | commitdiff | tree |
| 2013-09-23 |
Clark Barrett | Cleaner version of bug-fix for 528, also moved substitu... |
commit | commitdiff | tree |
| 2013-09-19 |
Clark Barrett | Fix for bug 528 |
commit | commitdiff | tree |
| 2013-09-18 |
Morgan Deters | Support a personal build configuration and make rules. |
commit | commitdiff | tree |
| 2013-09-18 |
Morgan Deters | Support for bv2nat/int2bv in parser and BV rewriter. |
commit | commitdiff | tree |
| 2013-09-18 |
Morgan Deters | Fixes to theoryof-mode; no longer static in Theory... |
commit | commitdiff | tree |
| 2013-09-16 |
Morgan Deters | Fix (extraneous) command dumping. |
commit | commitdiff | tree |
| 2013-09-15 |
Andrew Reynolds | Change default option of simple ite lifting within... |
commit | commitdiff | tree |
| 2013-09-13 |
Morgan Deters | Fix sat_proof "parentheses into the void" after conferr... |
commit | commitdiff | tree |
| 2013-09-13 |
Morgan Deters | Move some regress benchmarks around that took too long... |
commit | commitdiff | tree |
| 2013-09-13 |
Morgan Deters | Documentation fixes, some code typo fixes, file perms... |
commit | commitdiff | tree |
| 2013-09-13 |
Kshitij Bansal | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2013-09-12 |
Kshitij Bansal | fix bug 534: portfolio define-fun duplicate model |
commit | commitdiff | tree |
| 2013-09-11 |
Tianyi Liang | Theory of strings. |
commit | commitdiff | tree |
| 2013-09-09 |
Andrew Reynolds | Another minor fix for datatypes to repair my previous... |
commit | commitdiff | tree |
| 2013-09-09 |
Morgan Deters | Add support for check-sat with argument. |
commit | commitdiff | tree |
| 2013-09-09 |
Morgan Deters | Fix declare-datatypes dumping bug (bug 385). |
commit | commitdiff | tree |
| 2013-09-09 |
Morgan Deters | Support per-command verbosity settings. |
commit | commitdiff | tree |
| 2013-09-09 |
Morgan Deters | Support empty (and 1-ary) tuples and records. |
commit | commitdiff | tree |
| 2013-09-09 |
Morgan Deters | Fix some line-numbering in auto-generated metakind... |
commit | commitdiff | tree |
| 2013-09-09 |
Morgan Deters | Fix portfolio on bug411.smt2. (get-model command shoul... |
commit | commitdiff | tree |
| 2013-09-09 |
Morgan Deters | Ensure no cost for datatypes debugging when not tracing it. |
commit | commitdiff | tree |
| 2013-09-07 |
Andrew Reynolds | Fix datatypes for bug 503 |
commit | commitdiff | tree |
| 2013-09-05 |
Morgan Deters | Fix FLOOR and DISTINCT in CVC language parser. |
commit | commitdiff | tree |
| 2013-09-05 |
Morgan Deters | Fix lambda handling in CVC parser |
commit | commitdiff | tree |
| 2013-09-05 |
Morgan Deters | Permit setOption(decision-mode) |
commit | commitdiff | tree |
| 2013-09-05 |
Morgan Deters | Fix bugs/issues with missed-t-prop dump output |
commit | commitdiff | tree |
| 2013-09-05 |
Morgan Deters | Fix declare-fun/define-fun in dumps; resolves bugs... |
commit | commitdiff | tree |
| 2013-08-31 |
Morgan Deters | Add ability to mkConst(TupleSelect) and friends in... |
commit | commitdiff | tree |
| 2013-08-26 |
Kshitij Bansal | Merge branch '1.2.x' |
commit | commitdiff | tree |
| 2013-08-26 |
Kshitij Bansal | bug 374 fix: assert litVal=desiredVal only for leaf... |
commit | commitdiff | tree |
| 2013-08-26 |
Kshitij Bansal | Bug 374 benchmarks |
commit | commitdiff | tree |
| 2013-08-20 |
Morgan Deters | Change recursive expandDefinitions() to an interative... |
commit | commitdiff | tree |
| 2013-08-13 |
Morgan Deters | --segv-nospin is now default. |
commit | commitdiff | tree |
| 2013-08-13 |
Morgan Deters | Minor cleanup. |
commit | commitdiff | tree |
| 2013-08-13 |
Andrew Reynolds | Minor fixes for --fmf-fmc for quantifiers containing... |
commit | commitdiff | tree |
| 2013-08-13 |
Andrew Reynolds | initial modifications for per-ic cbqi |
commit | commitdiff | tree |
| 2013-08-09 |
Morgan Deters | Clean up "make install"-produced intermediate files... |
commit | commitdiff | tree |
| 2013-08-08 |
Morgan Deters | Fix a serious bug in the preprocessor; problem inputs... |
commit | commitdiff | tree |
| 2013-08-08 |
Morgan Deters | Parameterized, uninterpreted sorts need no Boolean... |
commit | commitdiff | tree |
| 2013-07-30 |
Morgan Deters | Minor fixes to build system. |
commit | commitdiff | tree |
| 2013-07-29 |
Morgan Deters | Fix numerous compiler warnings on various platforms |
commit | commitdiff | tree |
| 2013-07-24 |
Morgan Deters | Regressions now checking models on unknown too. But... |
commit | commitdiff | tree |
| 2013-07-24 |
Morgan Deters | Fixes for building with mingw win64. |
commit | commitdiff | tree |
| 2013-07-24 |
Morgan Deters | Don't allow --stats if not a statistics-enabled build |
commit | commitdiff | tree |
| 2013-07-24 |
Morgan Deters | some portfolio driver cleanup |
commit | commitdiff | tree |
| 2013-07-24 |
Morgan Deters | Some fixes for (get-info :all-options) |
commit | commitdiff | tree |
| 2013-07-23 |
Morgan Deters | fix for win32 option parsing via mingw32 |
commit | commitdiff | tree |
| 2013-07-23 |
Morgan Deters | (get-info :all-options) to get option values; also... |
commit | commitdiff | tree |
| 2013-07-22 |
Morgan Deters | Allow BV and DT in either order in the logic string |
commit | commitdiff | tree |
| 2013-07-22 |
Andrew Reynolds | Add option --cbqi-recurse. |
commit | commitdiff | tree |
| 2013-07-22 |
Andrew Reynolds | Bug fix for --fmf-fmc for non-uninterpreted sort quanti... |
commit | commitdiff | tree |
| 2013-07-20 |
Morgan Deters | enable bug521 regression tests |
commit | commitdiff | tree |
| 2013-07-19 |
Dejan Jovanovic | possible fix for bug 521 |
commit | commitdiff | tree |
| 2013-07-19 |
Morgan Deters | Minor fix for --no-condense-function-values |
commit | commitdiff | tree |
| 2013-07-18 |
Andrew Reynolds | Fix quantifier instantiation bug in cbqi, add default... |
commit | commitdiff | tree |
| 2013-07-17 |
Morgan Deters | Fix bug 516; include some bug testcases. |
commit | commitdiff | tree |
| 2013-07-16 |
Liana Hadarean | fixed seg fault when bv equality is turned off |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog