summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
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
2013-06-21Fix failure in non-assertion builds on incorrect SmtEngine use.Morgan Deters
2013-06-08Fixes for Boolean terms in arrays (including fix for bug 517).Morgan Deters
2013-06-07One more case for arrays of Boolean.Morgan Deters
2013-06-07Fix for bug 517.Morgan Deters
2013-05-20Merge branch '1.2.x'Morgan Deters
2013-05-20Fix error reporting on use of (nonlinear) div,mod,/ symbolsMorgan Deters
2013-05-20Don't allow get-model & co after a user push/popMorgan Deters
2013-05-20Fix for equality-chaining of Booleans in SMT-LIBv2.Morgan Deters
2013-05-20Better error on invalid logic strings.Morgan Deters
2013-05-20Fix to empty response to (get-assignment).Morgan Deters
2013-05-17Add support for --dump-models option, in preparation for casc.Andrew Reynolds
2013-05-17Fix for equality-chaining of Booleans in SMT-LIBv2.Morgan Deters
2013-05-17Better error on invalid logic strings.Morgan Deters
2013-05-17Fix to empty response to (get-assignment).Morgan Deters
2013-05-09Add simplification option --fo-prop-quant. Add model support for new model-c...Andrew Reynolds
2013-05-08Add new method for checking candidate models, --fmf-fmc. Add infrastructure ...Andrew Reynolds
2013-05-08final updates for smt-eval scriptMorgan Deters
2013-05-06Disables justification stop only for LRA if the problem contains no ites. Thi...Tim King
2013-05-02Merge branch 'master' of https://github.com/CVC4/CVC4lianah
2013-05-01Fix to dumping re: boolean terms, datatypesMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback