Age | Commit message (Collapse) | Author | |
---|---|---|---|
2013-10-07 | Multiple 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-03 | Added support for converting unsorted problems to multi-sorted problems via ↵ | Andrew Reynolds | |
sort inference and monotonicity. Minor cleanup. | |||
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 ↵ | Andrew Reynolds | |
to bounded integer quantifier instantiation. | |||
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 | |
This reverts commit 9775bced75843c6f01e9524c2d0e7021535e3ec0. | |||
2013-09-23 | Cleaner version of bug-fix for 528, also moved substitutions.h out of theory.h | Clark Barrett | |
for faster compilation | |||
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 ↵ | Morgan Deters | |
segfault in smt2 printer | |||
2013-08-20 | Change recursive expandDefinitions() to an interative worklist-based one; we ↵ | Morgan Deters | |
were blowing the stack. Fixes a segfault reported by Pantazis Deligiannis. | |||
2013-08-08 | Fix a serious bug in the preprocessor; problem inputs reported by Pantazis ↵ | Morgan Deters | |
Deligiannis. | |||
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 ↵ | Morgan Deters | |
to be simplified by check-model in that case. | |||
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 ↵ | Morgan Deters | |
suggestions | |||
2013-07-17 | Fix bug 516; include some bug testcases. | Morgan Deters | |
2013-07-11 | Support 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-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 ↵ | Morgan Deters | |
allows linearization of div,mod,/ by a constant. | |||
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 | |
Conflicts: library_versions src/parser/parser.h | |||
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 | |
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-20 | Fix for equality-chaining of Booleans in SMT-LIBv2. | Morgan Deters | |
Thanks to David Cok for reporting this. | |||
2013-05-20 | Better error on invalid logic strings. | Morgan Deters | |
Thanks to David Cok for reporting this issue. Conflicts: library_versions | |||
2013-05-20 | Fix to empty response to (get-assignment). | Morgan Deters | |
Thanks to David Cok for reporting this issue. | |||
2013-05-17 | Add support for --dump-models option, in preparation for casc. | Andrew Reynolds | |
2013-05-17 | Fix for equality-chaining of Booleans in SMT-LIBv2. | Morgan Deters | |
Thanks to David Cok for reporting this. | |||
2013-05-17 | Better error on invalid logic strings. | Morgan Deters | |
Thanks to David Cok for reporting this issue. | |||
2013-05-17 | Fix to empty response to (get-assignment). | Morgan Deters | |
Thanks to David Cok for reporting this issue. | |||
2013-05-09 | Add simplification option --fo-prop-quant. Add model support for new ↵ | Andrew Reynolds | |
model-checking procedure. Add run script for casc24-fnt. | |||
2013-05-08 | Add 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-08 | final updates for smt-eval script | Morgan Deters | |
2013-05-06 | Disables 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-02 | Merge branch 'master' of https://github.com/CVC4/CVC4 | lianah | |
2013-05-01 | Fix to dumping re: boolean terms, datatypes | Morgan Deters | |