Age | Commit message (Expand) | Author |
2013-11-07 | Flatten libcvc4 build structure; remove some #include interdependences | Morgan Deters |
2013-11-05 | fixed proof regression script and added a new uf test case | lianah |
2013-11-04 | Merge branch 'master' of https://github.com/CVC4/CVC4 | lianah |
2013-10-28 | Turn off model-based arrays (causing crashes in portfolio) | Clark Barrett |
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-07 | Multiple fixes for datatypes theory solver: add support for parametric dataty... | Andrew Reynolds |
2013-10-03 | Added support for converting unsorted problems to multi-sorted problems via s... | Andrew Reynolds |
2013-09-30 | replace with a new method for disequality, move to QF_S | Tianyi Liang |
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-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 | Fixes to theoryof-mode; no longer static in Theory class. | Morgan Deters |
2013-09-16 | Fix (extraneous) command dumping. | Morgan Deters |
2013-09-13 | Documentation fixes, some code typo fixes, file perms, other minor things. | 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-05 | Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a se... | Morgan Deters |
2013-08-20 | Change recursive expandDefinitions() to an interative worklist-based one; we ... | Morgan Deters |
2013-08-08 | Fix a serious bug in the preprocessor; problem inputs reported by Pantazis De... | Morgan Deters |
2013-08-08 | Parameterized, uninterpreted sorts need no Boolean-term conversion | Morgan Deters |
2013-07-24 | Regressions now checking models on unknown too. But quantifiers don't have t... | Morgan Deters |
2013-07-24 | Don't allow --stats if not a statistics-enabled build | Morgan Deters |
2013-07-23 | (get-info :all-options) to get option values; also command-line option sugges... | Morgan Deters |
2013-07-17 | Fix bug 516; include some bug testcases. | Morgan Deters |
2013-07-11 | Support for TPTP's TFF0 (with arithmetic) | Morgan Deters |
2013-07-11 | Fix for Boolean-term rewriting and LAMBDAs | Morgan Deters |
2013-07-06 | Model output is now const; this related to bug 519 | Morgan Deters |
2013-06-25 | Merge branch '1.2.x' | Morgan Deters |
2013-06-24 | Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al... | Morgan Deters |
2013-06-21 | Fix failure in non-assertion builds on incorrect SmtEngine use. | Morgan Deters |
2013-06-08 | Fixes for Boolean terms in arrays (including fix for bug 517). | Morgan Deters |
2013-06-07 | One more case for arrays of Boolean. | Morgan Deters |
2013-06-07 | Fix for bug 517. | Morgan Deters |
2013-05-20 | Merge branch '1.2.x' | Morgan Deters |
2013-05-20 | Fix error reporting on use of (nonlinear) div,mod,/ symbols | Morgan Deters |
2013-05-20 | Don't allow get-model & co after a user push/pop | Morgan Deters |
2013-05-20 | Fix for equality-chaining of Booleans in SMT-LIBv2. | Morgan Deters |
2013-05-20 | Better error on invalid logic strings. | Morgan Deters |
2013-05-20 | Fix to empty response to (get-assignment). | Morgan Deters |
2013-05-17 | Add support for --dump-models option, in preparation for casc. | Andrew Reynolds |