Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-01-16 | adds partial functions | Tianyi Liang | |
2014-01-15 | adds smt2 print for strings | Tianyi Liang | |
2014-01-15 | Optimizations for quantifiers conflict find: better caching, process ↵ | Andrew Reynolds | |
matching constraints eagerly. | |||
2014-01-10 | normal form breaking | Tianyi Liang | |
2014-01-10 | add repalce | Tianyi Liang | |
2014-01-10 | Add stats to quantifiers conflict find. Added option for qcf. Working on ↵ | Andrew Reynolds | |
handling non-APPLY_UF terms. | |||
2014-01-10 | Add new method --quant-cf for finding conflicts eagerly for quantified ↵ | Andrew Reynolds | |
formulas. This module can efficiently determine when there exists a conflict wrt quantified formulas that is implied by the current set of equalities, and reports the single lemma corresponding to the conflict. It does so before resorting to heuristic instantiation. Clean up the rewriter, other minor cleanup. | |||
2014-01-09 | move new functions under exp options | Tianyi Liang | |
2014-01-09 | add constant replace, indexof | Tianyi Liang | |
2014-01-09 | Another way to handle negative contain | Tianyi Liang | |
2014-01-08 | clean some code | Tianyi Liang | |
2014-01-08 | Fix LogicInfo parsing for string logics | Morgan Deters | |
2014-01-07 | remove a warning in strings | Tianyi Liang | |
2014-01-07 | minor fix, bring back the assertion. | Tianyi Liang | |
2014-01-07 | string contain changes | Tianyi Liang | |
2014-01-03 | Removing and consolidating options for uf-ss and quantifiers. Bug fix for ↵ | Andrew Reynolds | |
inst gen-style MBQI. | |||
2014-01-03 | Added support for proof production in Equality Engine. Cleaned up existing ↵ | Andrew Reynolds | |
proof signatures and added proof signature for theory of arrays. Added new MBQI technique based on interval abstraction. Cleaned up option names. Improved symmetry breaking for uf strong solver. Other minor cleanup. | |||
2014-01-02 | Merge branch '1.3.x' | Morgan Deters | |
2014-01-02 | Update copyright year. | Morgan Deters | |
2013-12-27 | minor fix | Tianyi Liang | |
2013-12-27 | Merge branch '1.3.x' | Morgan Deters | |
2013-12-27 | Fix for ANTLR warning. | Morgan Deters | |
2013-12-26 | new functions in strings | Tianyi Liang | |
2013-12-25 | fix for some nightly build failures | Morgan Deters | |
2013-12-24 | Merge branch '1.3.x' | Morgan Deters | |
Conflicts: NEWS | |||
2013-12-24 | Better automatic handling of output language setting. | Morgan Deters | |
2013-12-24 | Better get-value parse error message for common user error. | Morgan Deters | |
2013-12-24 | Minor code cleanup. | Morgan Deters | |
2013-12-24 | Java datatype API fixups, datatype API examples | Morgan Deters | |
2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof ↵ | Morgan Deters | |
generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals) * proofs are *not* yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line | |||
2013-12-22 | Merge branch '1.3.x' | Morgan Deters | |
2013-12-22 | Fix to interactive mode determination. | Morgan Deters | |
2013-12-22 | Fix option specification. | Morgan Deters | |
2013-12-17 | Merge branch '1.3.x' | Morgan Deters | |
Conflicts: COPYING NEWS | |||
2013-12-17 | some config changes: new --bsd option, readline gives warning, default build ↵ | Morgan Deters | |
is now production. | |||
2013-12-16 | First attempt at incorporating LFSC proof checker into CVC4. | Morgan Deters | |
2013-12-16 | Fix for bug 544. | Morgan Deters | |
2013-12-13 | Fix link error when using clang. | Morgan Deters | |
2013-12-10 | Fix timer statistics to report correct time even on process abort. | Morgan Deters | |
2013-12-10 | Whitespace. | Morgan Deters | |
2013-12-10 | Fix warning. | Morgan Deters | |
2013-12-10 | Remove "NodeValue width" output | Morgan Deters | |
2013-12-07 | fix bug 542 | Kshitij Bansal | |
2013-12-05 | disable substring in default mode | Tianyi Liang | |
2013-12-05 | Fix NodeValue bitfields for 32-bit; fix comment. | Morgan Deters | |
2013-12-05 | Minor cleanup. | Morgan Deters | |
2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters | |
2013-12-05 | Fixes related to parametric datatype printing. | Morgan Deters | |
2013-12-05 | Fix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now ↵ | Morgan Deters | |
works). | |||
2013-12-04 | Minor cleanup. | Morgan Deters | |