Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-01-17 | More optimizations for quantifiers conflict find. Add trust user patterns mode. | Andrew Reynolds | |
2014-01-17 | Merge branch '1.3.x' | Kshitij Bansal | |
2014-01-17 | enable search for html doc | Kshitij Bansal | |
2014-01-16 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
Conflicts: src/printer/smt2/smt2_printer.cpp | |||
2014-01-16 | adds partial functions | Tianyi Liang | |
2014-01-15 | adds smt2 print for strings | 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 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
2014-01-09 | add constant replace, indexof | Tianyi Liang | |
2014-01-09 | add constant replace, indexof | Tianyi Liang | |
2014-01-09 | Merge branch '1.3.x' | Morgan Deters | |
2014-01-09 | gmp is again default, not cln, for build ID (reverting due to license ↵ | Morgan Deters | |
discussion at Monday meeting) | |||
2014-01-09 | Another way to handle negative contain | Tianyi Liang | |
2014-01-08 | Merge branch '1.3.x' | Morgan Deters | |
Conflicts: COPYING NEWS config/cvc4.m4 | |||
2014-01-08 | Switch license default back to BSD, and add --best and --enable-gpl options. | Morgan Deters | |
2014-01-08 | Cache apt packages on Travis. | Morgan Deters | |
2014-01-08 | clean some code | Tianyi Liang | |
2014-01-08 | Fix LogicInfo parsing for string logics | Morgan Deters | |
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 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
2013-12-27 | minor fix | Tianyi Liang | |
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 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Tianyi Liang | |
2013-12-25 | fix for some nightly build failures | Morgan Deters | |
2013-12-24 | Cleanup related to output language fix. | 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 | Merge branch '1.3.x' | Morgan Deters | |
2013-12-24 | Java datatype API fixups, datatype API examples | Morgan Deters | |
2013-12-23 | cln now default w.r.t. build ID string | 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 | |