summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-01-17More optimizations for quantifiers conflict find. Add trust user patterns mode.Andrew Reynolds
2014-01-17Merge branch '1.3.x'Kshitij Bansal
2014-01-17enable search for html docKshitij Bansal
2014-01-16Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
Conflicts: src/printer/smt2/smt2_printer.cpp
2014-01-16adds partial functionsTianyi Liang
2014-01-15adds smt2 print for stringsTianyi Liang
2014-01-15adds smt2 print for stringsTianyi Liang
2014-01-15Optimizations for quantifiers conflict find: better caching, process ↵Andrew Reynolds
matching constraints eagerly.
2014-01-10normal form breakingTianyi Liang
2014-01-10add repalceTianyi Liang
2014-01-10Add stats to quantifiers conflict find. Added option for qcf. Working on ↵Andrew Reynolds
handling non-APPLY_UF terms.
2014-01-10Add 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-09move new functions under exp optionsTianyi Liang
2014-01-09Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-01-09add constant replace, indexofTianyi Liang
2014-01-09add constant replace, indexofTianyi Liang
2014-01-09Merge branch '1.3.x'Morgan Deters
2014-01-09gmp is again default, not cln, for build ID (reverting due to license ↵Morgan Deters
discussion at Monday meeting)
2014-01-09Another way to handle negative containTianyi Liang
2014-01-08Merge branch '1.3.x'Morgan Deters
Conflicts: COPYING NEWS config/cvc4.m4
2014-01-08Switch license default back to BSD, and add --best and --enable-gpl options.Morgan Deters
2014-01-08Cache apt packages on Travis.Morgan Deters
2014-01-08clean some codeTianyi Liang
2014-01-08Fix LogicInfo parsing for string logicsMorgan Deters
2014-01-08Fix LogicInfo parsing for string logicsMorgan Deters
2014-01-07remove a warning in stringsTianyi Liang
2014-01-07minor fix, bring back the assertion.Tianyi Liang
2014-01-07string contain changesTianyi Liang
2014-01-03Removing and consolidating options for uf-ss and quantifiers. Bug fix for ↵Andrew Reynolds
inst gen-style MBQI.
2014-01-03Added 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-02Merge branch '1.3.x'Morgan Deters
2014-01-02Update copyright year.Morgan Deters
2013-12-27Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2013-12-27minor fixTianyi Liang
2013-12-27minor fixTianyi Liang
2013-12-27Merge branch '1.3.x'Morgan Deters
2013-12-27Fix for ANTLR warning.Morgan Deters
2013-12-26new functions in stringsTianyi Liang
2013-12-25Merge branch 'master' of https://github.com/CVC4/CVC4Tianyi Liang
2013-12-25fix for some nightly build failuresMorgan Deters
2013-12-24Cleanup related to output language fix.Morgan Deters
2013-12-24Merge branch '1.3.x'Morgan Deters
Conflicts: NEWS
2013-12-24Better automatic handling of output language setting.Morgan Deters
2013-12-24Better get-value parse error message for common user error.Morgan Deters
2013-12-24Minor code cleanup.Morgan Deters
2013-12-24Merge branch '1.3.x'Morgan Deters
2013-12-24Java datatype API fixups, datatype API examplesMorgan Deters
2013-12-23cln now default w.r.t. build ID stringMorgan Deters
2013-12-23Proof-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-22Merge branch '1.3.x'Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback