summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-12-05Fix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now wor...Morgan Deters
2013-12-04Partial kind branch merge, including new --rewrite-apply-to-const feature.Morgan Deters
2013-12-04Don't put define-funs in model output; bug 411 testcase no longer relevant.Morgan Deters
2013-12-02Another fix to Java destruction order issues. Thanks to Zheng Manchun for th...Morgan Deters
2013-11-29Fix proofs build.Morgan Deters
2013-11-27General pre-release cleanup commitMorgan Deters
2013-11-27Incremental is now on by default when using from API, off for command-line dr...Morgan Deters
2013-11-26Fix Java destruction order issue; thanks to Zheng Manchun for reporting this ...Morgan Deters
2013-11-25Substantial Changes:Tim King
2013-11-20Changing the number of bits allocated per field in node values.Tim King
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-11-05fixed proof regression script and added a new uf test caselianah
2013-11-04Merge branch 'master' of https://github.com/CVC4/CVC4lianah
2013-10-28Turn off model-based arrays (causing crashes in portfolio)Clark Barrett
2013-10-09fixed options::proof() segfaultlianah
2013-10-09cleaned up proof codelianah
2013-10-09fixed uf proof bug: now storing deleted theory lemmaslianah
2013-10-09More improvements to datatypes, eager selector collapsing, improved collect m...Andrew Reynolds
2013-10-08added currying for uf proofs; still needs debugginglianah
2013-10-07Multiple fixes for datatypes theory solver: add support for parametric dataty...Andrew Reynolds
2013-10-03Added support for converting unsorted problems to multi-sorted problems via s...Andrew Reynolds
2013-09-30replace with a new method for disequality, move to QF_STianyi Liang
2013-09-27Some fixes to recent strings commits.Morgan Deters
2013-09-27Merge branch 'master' of github.com:tiliang/CVC4Morgan Deters
2013-09-27adds communication with arith engineTianyi Liang
2013-09-27Add new symmetry breaking technique for finite model finding. Improvements t...Andrew Reynolds
2013-09-27removes unsound cases, adds unrollingTianyi Liang
2013-09-24Better fix for bug 528Clark Barrett
2013-09-23Revert Clark's last commit, at his request; there are some bugs.Morgan Deters
2013-09-23Cleaner version of bug-fix for 528, also moved substitutions.h out of theory.hClark Barrett
2013-09-19Fix for bug 528Clark Barrett
2013-09-18Fixes to theoryof-mode; no longer static in Theory class.Morgan Deters
2013-09-16Fix (extraneous) command dumping.Morgan Deters
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-09-09Fix declare-datatypes dumping bug (bug 385).Morgan Deters
2013-09-09Support per-command verbosity settings.Morgan Deters
2013-09-05Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a se...Morgan Deters
2013-08-20Change recursive expandDefinitions() to an interative worklist-based one; we ...Morgan Deters
2013-08-08Fix a serious bug in the preprocessor; problem inputs reported by Pantazis De...Morgan Deters
2013-08-08Parameterized, uninterpreted sorts need no Boolean-term conversionMorgan Deters
2013-07-24Regressions now checking models on unknown too. But quantifiers don't have t...Morgan Deters
2013-07-24Don't allow --stats if not a statistics-enabled buildMorgan Deters
2013-07-23(get-info :all-options) to get option values; also command-line option sugges...Morgan Deters
2013-07-17Fix bug 516; include some bug testcases.Morgan Deters
2013-07-11Support for TPTP's TFF0 (with arithmetic)Morgan Deters
2013-07-11Fix for Boolean-term rewriting and LAMBDAsMorgan Deters
2013-07-06Model output is now const; this related to bug 519Morgan Deters
2013-06-25Merge branch '1.2.x'Morgan Deters
2013-06-24Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al...Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback