Age | Commit message (Expand) | Author |
2013-10-03 | adds some fixes. it solves kaluza problems | 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 | 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 | 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-24 | Reduce compiler dependencies on substitutions.h, | Clark Barrett |
2013-09-24 | Better fix for bug 528 | Clark Barrett |
2013-09-23 | Revert Clark's last commit, at his request; there are some bugs. | Morgan Deters |
2013-09-23 | Cleaner version of bug-fix for 528, also moved substitutions.h out of theory.h | Clark Barrett |
2013-09-19 | Fix for bug 528 | Clark Barrett |
2013-09-18 | Support for bv2nat/int2bv in parser and BV rewriter. | Morgan Deters |
2013-09-18 | Fixes to theoryof-mode; no longer static in Theory class. | Morgan Deters |
2013-09-16 | Fix (extraneous) command dumping. | Morgan Deters |
2013-09-15 | Change default option of simple ite lifting within quantifier bodies. add so... | Andrew Reynolds |
2013-09-13 | Fix sat_proof "parentheses into the void" after conferring with Liana. | Morgan Deters |
2013-09-13 | Documentation fixes, some code typo fixes, file perms, other minor things. | Morgan Deters |
2013-09-13 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Kshitij Bansal |
2013-09-12 | fix bug 534: portfolio define-fun duplicate model | Kshitij Bansal |
2013-09-11 | Theory of strings. | Tianyi Liang |
2013-09-09 | Another minor fix for datatypes to repair my previous commit. | Andrew Reynolds |
2013-09-09 | Add support for check-sat with argument. | Morgan Deters |
2013-09-09 | Fix declare-datatypes dumping bug (bug 385). | Morgan Deters |
2013-09-09 | Support per-command verbosity settings. | Morgan Deters |
2013-09-09 | Support empty (and 1-ary) tuples and records. | Morgan Deters |
2013-09-09 | Fix some line-numbering in auto-generated metakind.h. Thanks to Martin Brain... | Morgan Deters |
2013-09-09 | Fix portfolio on bug411.smt2. (get-model command should only go to last winner) | Morgan Deters |
2013-09-09 | Ensure no cost for datatypes debugging when not tracing it. | Morgan Deters |
2013-09-06 | Fix datatypes for bug 503 | Andrew Reynolds |
2013-09-05 | Fix FLOOR and DISTINCT in CVC language parser. | Morgan Deters |
2013-09-05 | Fix lambda handling in CVC parser | Morgan Deters |
2013-09-05 | Permit setOption(decision-mode) | Morgan Deters |
2013-09-05 | Fix bugs/issues with missed-t-prop dump output | Morgan Deters |
2013-09-05 | Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a se... | Morgan Deters |
2013-08-30 | Add ability to mkConst(TupleSelect) and friends in language bindings | Morgan Deters |
2013-08-26 | Merge branch '1.2.x' | Kshitij Bansal |
2013-08-26 | bug 374 fix: assert litVal=desiredVal only for leaf nodes1.2.x | Kshitij Bansal |
2013-08-20 | Change recursive expandDefinitions() to an interative worklist-based one; we ... | Morgan Deters |
2013-08-13 | --segv-nospin is now default. | Morgan Deters |