summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Collapse)Author
2013-10-07Multiple fixes for datatypes theory solver: add support for parametric ↵Andrew Reynolds
datatypes in type enumerator, fix infinite loop in type enumerator, fix fairness issue for splitting (moves constructor selection into model generation procedure), fixes bug 532, find conflict for constructor with conflicting label eagerly. Add representive flattening for quantifiers (currently disabled). Other minor cleanup.
2013-10-03Added support for converting unsorted problems to multi-sorted problems via ↵Andrew Reynolds
sort inference and monotonicity. Minor cleanup.
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 ↵Andrew Reynolds
to bounded integer quantifier instantiation.
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
This reverts commit 9775bced75843c6f01e9524c2d0e7021535e3ec0.
2013-09-23Cleaner version of bug-fix for 528, also moved substitutions.h out of theory.hClark Barrett
for faster compilation
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 ↵Morgan Deters
segfault in smt2 printer
2013-08-20Change recursive expandDefinitions() to an interative worklist-based one; we ↵Morgan Deters
were blowing the stack. Fixes a segfault reported by Pantazis Deligiannis.
2013-08-08Fix a serious bug in the preprocessor; problem inputs reported by Pantazis ↵Morgan Deters
Deligiannis.
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 ↵Morgan Deters
to be simplified by check-model in that case.
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 ↵Morgan Deters
suggestions
2013-07-17Fix bug 516; include some bug testcases.Morgan Deters
2013-07-11Support for TPTP's TFF0 (with arithmetic)Morgan Deters
This commit reverses an "SZS ontology compliance hack" that was done for CASC-24 this year, and adds a TPTP pretty-printer which is capable of outputting results in the TPTP way (rather than the SMT way). This commit includes minor changes to the Expr package to add obvious missing functionality, and to fix the way expressions with builtin operators are made. These changes are truly a _fix_, the implementation had not been properly aligned with the design vision for some corner cases.
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 ↵Morgan Deters
allows linearization of div,mod,/ by a constant.
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
Conflicts: library_versions src/parser/parser.h
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
This makes us more strictly adhere to the spec, but it's useful anyway: previously we would support a get-model until the problem was explicitly changed with e.g. a new assertion. That meant you could check-sat, then pop, then get-model, but you'd only get the part of the model still in scope. This is strange, and would likely lead to problems, so it's now disabled. Thanks to David Cok for inquiring about this.
2013-05-20Fix for equality-chaining of Booleans in SMT-LIBv2.Morgan Deters
Thanks to David Cok for reporting this.
2013-05-20Better error on invalid logic strings.Morgan Deters
Thanks to David Cok for reporting this issue. Conflicts: library_versions
2013-05-20Fix to empty response to (get-assignment).Morgan Deters
Thanks to David Cok for reporting this issue.
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
Thanks to David Cok for reporting this.
2013-05-17Better error on invalid logic strings.Morgan Deters
Thanks to David Cok for reporting this issue.
2013-05-17Fix to empty response to (get-assignment).Morgan Deters
Thanks to David Cok for reporting this issue.
2013-05-09Add simplification option --fo-prop-quant. Add model support for new ↵Andrew Reynolds
model-checking procedure. Add run script for casc24-fnt.
2013-05-08Add new method for checking candidate models, --fmf-fmc. Add infrastructure ↵Andrew Reynolds
for handling bounded integer quantification (quantifiers/bounded_integers.h and .cpp). Add option for disabling model minimality restriction for finite model finding, --disable-uf-ss-min-model. Add option for relational triggers such as x = f(y), --relational-trigger.
2013-05-08final updates for smt-eval scriptMorgan Deters
2013-05-06Disables justification stop only for LRA if the problem contains no ites. ↵Tim King
This is a bandaid for constraints-tempo-width family of benchmarks.
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