Age | Commit message (Expand) | Author |
2013-10-11 | adds native regexp. | Tianyi Liang |
2013-10-11 | add constant membership | Tianyi Liang |
2013-10-10 | Minor bug fix to datatypes. | Andrew Reynolds |
2013-10-10 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang |
2013-10-10 | adds native regexp. | Tianyi Liang |
2013-10-10 | adds native regexp. | Tianyi Liang |
2013-10-09 | fixed options::proof() segfault | lianah |
2013-10-09 | cleaned up proof code | lianah |
2013-10-09 | fixed uf proof bug: now storing deleted theory lemmas | lianah |
2013-10-09 | More improvements to datatypes, eager selector collapsing, improved collect m... | Andrew Reynolds |
2013-10-08 | added currying for uf proofs; still needs debugging | lianah |
2013-10-08 | fixed uf proof with holes bugs | lianah |
2013-10-08 | Optimizations for datatypes theory. There seems to be a bug in trans_closure... | Andrew Reynolds |
2013-10-07 | fixed some bugs | Liana Hadarean |
2013-10-07 | first draft implementation of uf proofs with holes | Liana Hadarean |
2013-10-07 | merged golden | Liana Hadarean |
2013-10-07 | Multiple fixes for datatypes theory solver: add support for parametric dataty... | Andrew Reynolds |
2013-10-03 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Tianyi Liang |
2013-10-03 | Adding example proof signatures for LFSC. | Andrew Reynolds |
2013-10-03 | Added support for converting unsorted problems to multi-sorted problems via s... | Andrew Reynolds |
2013-10-03 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang |
2013-10-03 | adds some fixes. it solves kaluza problems | Tianyi Liang |
2013-10-03 | Adding example proof signatures for LFSC. | Andrew Reynolds |
2013-10-02 | Added support for converting unsorted problems to multi-sorted problems via s... | Andrew Reynolds |
2013-10-01 | adds partial function substr. the use of this function should be guarded, esp... | Tianyi Liang |
2013-10-01 | adds partial function substr. the use of this function should be guarded, esp... | Tianyi Liang |
2013-10-01 | Fix a bug in smt2 parser for quantified formulas with attributes, fixes bug 535 | Andrew Reynolds |
2013-09-30 | replace with a new method for disequality, move to QF_S | Tianyi Liang |
2013-09-30 | add x=y | Tianyi Liang |
2013-09-30 | fixed a loop bug | Tianyi Liang |
2013-09-30 | merged golden | Liana Hadarean |
2013-09-30 | Bug fixes and improvements for symmetry breaking, it now supports multiple so... | Andrew Reynolds |
2013-09-27 | Some fixes to recent strings commits. | Morgan Deters |
2013-09-27 | Merge branch 'master' of github.com:tiliang/CVC4 | Morgan Deters |
2013-09-27 | adds communication with arith engine | Tianyi Liang |
2013-09-27 | Add new symmetry breaking technique for finite model finding. Improvements t... | Andrew Reynolds |
2013-09-27 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang |
2013-09-27 | removes unsound cases, adds unrolling | Tianyi Liang |
2013-09-27 | fix the infinite issue | Tianyi Liang |
2013-09-27 | for morgan to see the regression problems | Tianyi Liang |
2013-09-27 | fix loop detection for multi-vars | Tianyi Liang |
2013-09-27 | optimizing model generation for strings | Tianyi Liang |
2013-09-27 | adds model generation for strings, and a hacked way in arith engine for models | Tianyi Liang |
2013-09-27 | removes unsound cases, adds unrolling | Tianyi Liang |
2013-09-25 | fix the infinite issue | Tianyi Liang |
2013-09-25 | for morgan to see the regression problems | Tianyi Liang |
2013-09-24 | Reduce compiler dependencies on substitutions.h, | Clark Barrett |
2013-09-24 | Better fix for bug 528 | Clark Barrett |
2013-09-24 | fix loop detection for multi-vars | Tianyi Liang |
2013-09-24 | optimizing model generation for strings | Tianyi Liang |