Morgan Deters [Sat, 18 Jan 2014 04:00:32 +0000 (23:00 -0500)]
Merge branch '1.3.x'
Morgan Deters [Sat, 18 Jan 2014 03:59:39 +0000 (22:59 -0500)]
Fix for quote-escaping in smt2 printer
Andrew Reynolds [Fri, 17 Jan 2014 15:57:12 +0000 (09:57 -0600)]
More optimizations for quantifiers conflict find. Add trust user patterns mode.
Kshitij Bansal [Fri, 17 Jan 2014 14:12:25 +0000 (09:12 -0500)]
Merge branch '1.3.x'
Kshitij Bansal [Fri, 17 Jan 2014 14:11:58 +0000 (09:11 -0500)]
enable search for html doc
Tianyi Liang [Thu, 16 Jan 2014 21:40:01 +0000 (15:40 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Conflicts:
src/printer/smt2/smt2_printer.cpp
Tianyi Liang [Thu, 16 Jan 2014 21:37:58 +0000 (15:37 -0600)]
adds partial functions
Tianyi Liang [Wed, 15 Jan 2014 23:20:27 +0000 (17:20 -0600)]
adds smt2 print for strings
Tianyi Liang [Wed, 15 Jan 2014 23:20:27 +0000 (17:20 -0600)]
adds smt2 print for strings
Andrew Reynolds [Wed, 15 Jan 2014 16:22:10 +0000 (10:22 -0600)]
Optimizations for quantifiers conflict find: better caching, process matching constraints eagerly.
Tianyi Liang [Fri, 10 Jan 2014 23:42:01 +0000 (17:42 -0600)]
normal form breaking
Tianyi Liang [Fri, 10 Jan 2014 19:26:56 +0000 (13:26 -0600)]
add repalce
Andrew Reynolds [Fri, 10 Jan 2014 16:50:56 +0000 (10:50 -0600)]
Add stats to quantifiers conflict find. Added option for qcf. Working on handling non-APPLY_UF terms.
Andrew Reynolds [Fri, 10 Jan 2014 08:04:51 +0000 (02:04 -0600)]
Add new method --quant-cf for finding conflicts eagerly for quantified 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.
Tianyi Liang [Fri, 10 Jan 2014 00:23:15 +0000 (18:23 -0600)]
move new functions under exp options
Tianyi Liang [Thu, 9 Jan 2014 22:25:34 +0000 (16:25 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Thu, 9 Jan 2014 22:23:59 +0000 (16:23 -0600)]
add constant replace, indexof
Tianyi Liang [Thu, 9 Jan 2014 22:23:59 +0000 (16:23 -0600)]
add constant replace, indexof
Morgan Deters [Thu, 9 Jan 2014 21:48:32 +0000 (16:48 -0500)]
Merge branch '1.3.x'
Morgan Deters [Thu, 9 Jan 2014 21:48:21 +0000 (16:48 -0500)]
gmp is again default, not cln, for build ID (reverting due to license discussion at Monday meeting)
Tianyi Liang [Thu, 9 Jan 2014 19:24:27 +0000 (13:24 -0600)]
Another way to handle negative contain
Morgan Deters [Wed, 8 Jan 2014 20:32:59 +0000 (15:32 -0500)]
Merge branch '1.3.x'
Conflicts:
COPYING
NEWS
config/cvc4.m4
Morgan Deters [Wed, 8 Jan 2014 20:27:26 +0000 (15:27 -0500)]
Switch license default back to BSD, and add --best and --enable-gpl options.
Morgan Deters [Wed, 18 Dec 2013 02:13:12 +0000 (21:13 -0500)]
Cache apt packages on Travis.
Tianyi Liang [Wed, 8 Jan 2014 18:07:56 +0000 (12:07 -0600)]
clean some code
Morgan Deters [Wed, 8 Jan 2014 16:18:02 +0000 (11:18 -0500)]
Fix LogicInfo parsing for string logics
Morgan Deters [Wed, 8 Jan 2014 16:17:32 +0000 (11:17 -0500)]
Fix LogicInfo parsing for string logics
Tianyi Liang [Wed, 8 Jan 2014 02:04:27 +0000 (20:04 -0600)]
remove a warning in strings
Tianyi Liang [Wed, 8 Jan 2014 01:18:55 +0000 (19:18 -0600)]
minor fix, bring back the assertion.
Tianyi Liang [Wed, 8 Jan 2014 00:12:08 +0000 (18:12 -0600)]
string contain changes
Andrew Reynolds [Sat, 4 Jan 2014 04:36:55 +0000 (22:36 -0600)]
Removing and consolidating options for uf-ss and quantifiers. Bug fix for inst gen-style MBQI.
Andrew Reynolds [Fri, 3 Jan 2014 18:13:13 +0000 (12:13 -0600)]
Added support for proof production in Equality Engine. Cleaned up existing 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.
Morgan Deters [Thu, 2 Jan 2014 19:13:17 +0000 (14:13 -0500)]
Merge branch '1.3.x'
Morgan Deters [Thu, 2 Jan 2014 19:13:08 +0000 (14:13 -0500)]
Update copyright year.
Tianyi Liang [Fri, 27 Dec 2013 17:27:16 +0000 (11:27 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Fri, 27 Dec 2013 17:24:14 +0000 (11:24 -0600)]
minor fix
Tianyi Liang [Fri, 27 Dec 2013 17:24:14 +0000 (11:24 -0600)]
minor fix
Morgan Deters [Fri, 27 Dec 2013 17:21:25 +0000 (12:21 -0500)]
Merge branch '1.3.x'
Morgan Deters [Fri, 27 Dec 2013 17:21:20 +0000 (12:21 -0500)]
Fix for ANTLR warning.
Tianyi Liang [Thu, 26 Dec 2013 23:18:26 +0000 (17:18 -0600)]
new functions in strings
Tianyi Liang [Thu, 26 Dec 2013 00:44:59 +0000 (18:44 -0600)]
Merge branch 'master' of https://github.com/CVC4/CVC4
Morgan Deters [Wed, 25 Dec 2013 22:18:40 +0000 (17:18 -0500)]
fix for some nightly build failures
Morgan Deters [Tue, 24 Dec 2013 18:26:31 +0000 (13:26 -0500)]
Cleanup related to output language fix.
Morgan Deters [Tue, 24 Dec 2013 18:25:30 +0000 (13:25 -0500)]
Merge branch '1.3.x'
Conflicts:
NEWS
Morgan Deters [Tue, 24 Dec 2013 18:24:56 +0000 (13:24 -0500)]
Better automatic handling of output language setting.
Morgan Deters [Mon, 16 Dec 2013 14:49:05 +0000 (09:49 -0500)]
Better get-value parse error message for common user error.
Morgan Deters [Tue, 24 Dec 2013 17:45:13 +0000 (12:45 -0500)]
Minor code cleanup.
Morgan Deters [Tue, 24 Dec 2013 15:57:28 +0000 (10:57 -0500)]
Merge branch '1.3.x'
Morgan Deters [Mon, 3 Jun 2013 22:18:24 +0000 (18:18 -0400)]
Java datatype API fixups, datatype API examples
Morgan Deters [Mon, 23 Dec 2013 18:45:33 +0000 (13:45 -0500)]
cln now default w.r.t. build ID string
Morgan Deters [Mon, 5 Aug 2013 22:29:34 +0000 (18:29 -0400)]
Proof-checking code; fixups of segfaults and missing functionality in proof 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
Morgan Deters [Sun, 22 Dec 2013 17:06:34 +0000 (12:06 -0500)]
Merge branch '1.3.x'
Morgan Deters [Thu, 19 Dec 2013 16:52:00 +0000 (11:52 -0500)]
Fix to interactive mode determination.
Morgan Deters [Thu, 19 Dec 2013 16:32:56 +0000 (11:32 -0500)]
Fix option specification.
Tianyi Liang [Thu, 19 Dec 2013 18:01:28 +0000 (12:01 -0600)]
Merge branch 'master' of https://github.com/CVC4/CVC4
Morgan Deters [Wed, 18 Dec 2013 19:27:55 +0000 (14:27 -0500)]
Merge branch '1.3.x'
[skip ci]
Morgan Deters [Wed, 18 Dec 2013 17:23:24 +0000 (12:23 -0500)]
Fix an autoconf issue with CLN in some configurations; also clarification re: license issues
[skip ci]
Morgan Deters [Wed, 18 Dec 2013 16:47:59 +0000 (11:47 -0500)]
Merge branch '1.3.x'
Morgan Deters [Wed, 18 Dec 2013 16:47:50 +0000 (11:47 -0500)]
Fix configure handling for CLN (should fix win32 nightly builds)
Morgan Deters [Wed, 18 Dec 2013 16:11:36 +0000 (11:11 -0500)]
Merge branch '1.3.x'
Morgan Deters [Wed, 18 Dec 2013 16:11:34 +0000 (11:11 -0500)]
Reduce autoconf version for dependence (should fix 32-bit builds).
Morgan Deters [Wed, 18 Dec 2013 16:09:41 +0000 (11:09 -0500)]
Add missing regression-results directory.
Tianyi Liang [Wed, 18 Dec 2013 02:17:12 +0000 (20:17 -0600)]
Merge branch 'master' of https://github.com/CVC4/CVC4
Morgan Deters [Tue, 17 Dec 2013 23:56:24 +0000 (18:56 -0500)]
Merge branch '1.3.x'
Morgan Deters [Tue, 17 Dec 2013 23:56:19 +0000 (18:56 -0500)]
configure --with-portfolio disables CLN.
Tianyi Liang [Tue, 17 Dec 2013 23:52:40 +0000 (17:52 -0600)]
Merge branch 'master' of https://github.com/CVC4/CVC4
Morgan Deters [Tue, 17 Dec 2013 22:14:45 +0000 (17:14 -0500)]
Merge branch '1.3.x'
Conflicts:
COPYING
NEWS
Morgan Deters [Tue, 17 Dec 2013 17:40:50 +0000 (12:40 -0500)]
some config changes: new --bsd option, readline gives warning, default build is now production.
Morgan Deters [Thu, 12 Dec 2013 23:24:54 +0000 (18:24 -0500)]
First attempt at incorporating LFSC proof checker into CVC4.
Morgan Deters [Mon, 16 Dec 2013 19:34:44 +0000 (14:34 -0500)]
Merge branch '1.3.x'
Morgan Deters [Mon, 16 Dec 2013 19:34:38 +0000 (14:34 -0500)]
Send Travis-CI emails to everyone
Morgan Deters [Mon, 16 Dec 2013 14:52:52 +0000 (09:52 -0500)]
Merge branch '1.3.x'
Morgan Deters [Mon, 16 Dec 2013 12:30:06 +0000 (07:30 -0500)]
Fix for bug 544.
Tianyi Liang [Sun, 15 Dec 2013 17:51:44 +0000 (11:51 -0600)]
resolve merge issue.
Tianyi Liang [Sun, 15 Dec 2013 17:49:17 +0000 (11:49 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Conflicts:
NEWS
Morgan Deters [Sat, 14 Dec 2013 00:46:06 +0000 (19:46 -0500)]
Merge branch '1.3.x'
Morgan Deters [Sat, 14 Dec 2013 00:46:01 +0000 (19:46 -0500)]
Another fix for clang.
Morgan Deters [Sat, 14 Dec 2013 00:12:54 +0000 (19:12 -0500)]
Merge branch '1.3.x'
Morgan Deters [Sat, 14 Dec 2013 00:12:31 +0000 (19:12 -0500)]
Fix stack size on in-tree regressions.
Morgan Deters [Fri, 13 Dec 2013 23:53:13 +0000 (18:53 -0500)]
cleanup
Morgan Deters [Fri, 13 Dec 2013 23:25:48 +0000 (18:25 -0500)]
Merge branch '1.3.x'
Morgan Deters [Fri, 13 Dec 2013 23:25:36 +0000 (18:25 -0500)]
Fix link error when using clang.
Morgan Deters [Fri, 13 Dec 2013 23:21:01 +0000 (18:21 -0500)]
Fix to Travis-CI config.
Morgan Deters [Fri, 13 Dec 2013 23:21:01 +0000 (18:21 -0500)]
Fix to Travis-CI config.
Morgan Deters [Fri, 13 Dec 2013 22:12:37 +0000 (17:12 -0500)]
Merge branch '1.3.x'
Morgan Deters [Fri, 13 Dec 2013 22:11:54 +0000 (17:11 -0500)]
Travis-CI configuration.
Morgan Deters [Fri, 13 Dec 2013 15:41:37 +0000 (10:41 -0500)]
Some minor cleanup.
Morgan Deters [Wed, 11 Dec 2013 04:43:02 +0000 (23:43 -0500)]
Update NEWS.
Morgan Deters [Wed, 11 Dec 2013 04:39:58 +0000 (23:39 -0500)]
Merge branch '1.3.x'
Morgan Deters [Wed, 11 Dec 2013 04:17:13 +0000 (23:17 -0500)]
Fix timer statistics to report correct time even on process abort.
Morgan Deters [Wed, 11 Dec 2013 04:16:27 +0000 (23:16 -0500)]
Whitespace.
Morgan Deters [Wed, 11 Dec 2013 00:04:00 +0000 (19:04 -0500)]
Fix warning.
Morgan Deters [Tue, 10 Dec 2013 05:54:31 +0000 (00:54 -0500)]
Remove "NodeValue width" output
Morgan Deters [Mon, 9 Dec 2013 23:31:17 +0000 (18:31 -0500)]
GLPK build identifier, license warnings.
Morgan Deters [Wed, 11 Dec 2013 04:17:13 +0000 (23:17 -0500)]
Fix timer statistics to report correct time even on process abort.
Morgan Deters [Wed, 11 Dec 2013 04:16:27 +0000 (23:16 -0500)]
Whitespace.
Morgan Deters [Wed, 11 Dec 2013 00:04:00 +0000 (19:04 -0500)]
Fix warning.
Morgan Deters [Tue, 10 Dec 2013 05:54:31 +0000 (00:54 -0500)]
Remove "NodeValue width" output
Morgan Deters [Mon, 9 Dec 2013 23:31:17 +0000 (18:31 -0500)]
GLPK build identifier, license warnings.
Kshitij Bansal [Mon, 9 Dec 2013 19:14:46 +0000 (14:14 -0500)]
mv prp to regress1
projects / cvc5.git / log