Morgan Deters [Fri, 13 Jun 2014 21:41:42 +0000 (17:41 -0400)]
Doubly-ensure incremental is off in main track. Also import bv-portfolio strategy.
ajreynol [Fri, 13 Jun 2014 15:18:05 +0000 (17:18 +0200)]
Fix handling of ALIA.
Morgan Deters [Fri, 13 Jun 2014 15:00:24 +0000 (11:00 -0400)]
update application track script too
Clark Barrett [Fri, 13 Jun 2014 07:38:33 +0000 (00:38 -0700)]
Update for QF_AUFLIA strategy
Morgan Deters [Fri, 13 Jun 2014 05:31:18 +0000 (01:31 -0400)]
Allow parallel failures when building competition version (they are spurious).
Morgan Deters [Fri, 13 Jun 2014 05:26:03 +0000 (01:26 -0400)]
Adjust incremental run script for QF_AX too.
Clark Barrett [Thu, 12 Jun 2014 22:39:56 +0000 (15:39 -0700)]
Modified run script for QF_AX
Clark Barrett [Thu, 12 Jun 2014 22:20:41 +0000 (15:20 -0700)]
Modified run script for QF_LRA
Morgan Deters [Thu, 12 Jun 2014 20:22:29 +0000 (16:22 -0400)]
More make submission stuff
lianah [Thu, 12 Jun 2014 19:18:47 +0000 (15:18 -0400)]
Merge branch 'master' of https://github.com/CVC4/CVC4
lianah [Thu, 12 Jun 2014 19:00:27 +0000 (15:00 -0400)]
fixing bv inequality solver explanation bug
Morgan Deters [Thu, 12 Jun 2014 17:43:06 +0000 (13:43 -0400)]
New application track script, new heuristics and all --tear-down-incremental. Not yet tested.
lianah [Thu, 12 Jun 2014 13:23:10 +0000 (09:23 -0400)]
added bvcomp case to bv to bool lifting
Morgan Deters [Thu, 12 Jun 2014 02:13:48 +0000 (22:13 -0400)]
more fix-ups
lianah [Thu, 12 Jun 2014 01:43:33 +0000 (21:43 -0400)]
added optionException for trying to use abc in an non-abc build
Morgan Deters [Thu, 12 Jun 2014 00:58:11 +0000 (20:58 -0400)]
more smtcomp-submission script work
Morgan Deters [Wed, 11 Jun 2014 23:11:56 +0000 (19:11 -0400)]
Flush output stream after result printed in portfolio.
Morgan Deters [Wed, 11 Jun 2014 22:33:52 +0000 (18:33 -0400)]
Fix for competition mode + parallel.
Morgan Deters [Wed, 11 Jun 2014 22:33:37 +0000 (18:33 -0400)]
Fix parallel run script.
lianah [Wed, 11 Jun 2014 22:40:39 +0000 (18:40 -0400)]
Merge branch 'master' of https://github.com/CVC4/CVC4
lianah [Wed, 11 Jun 2014 22:40:02 +0000 (18:40 -0400)]
switched bv equality order
ajreynol [Wed, 11 Jun 2014 22:31:29 +0000 (00:31 +0200)]
Update SMTCOMP script to handle all quantified logics.
Morgan Deters [Wed, 11 Jun 2014 20:55:50 +0000 (16:55 -0400)]
Fix an omission in bv sources.
Morgan Deters [Wed, 11 Jun 2014 18:15:23 +0000 (14:15 -0400)]
--best now implies --with-glpk --with-abc
Morgan Deters [Tue, 10 Jun 2014 21:52:26 +0000 (17:52 -0400)]
Some clean-up, post bv-merge.
Add abc to build id and fix static building.
Add abc to --show-config output and Configuration class API.
Add ability to select abc source path.
Fix arch_flags for abc.
Kshitij Bansal [Wed, 11 Jun 2014 20:05:16 +0000 (16:05 -0400)]
Merge pull request #31 from kbansal/sets
Sets
lianah [Wed, 11 Jun 2014 19:48:53 +0000 (15:48 -0400)]
fixed unit tests failures
Kshitij Bansal [Wed, 11 Jun 2014 18:47:13 +0000 (14:47 -0400)]
disable another test, after recent merges taking too long
Kshitij Bansal [Wed, 11 Jun 2014 18:31:01 +0000 (14:31 -0400)]
disable failing test
Kshitij Bansal [Wed, 11 Jun 2014 16:35:46 +0000 (12:35 -0400)]
sets: comment out an assertion too strong
Kshitij Bansal [Wed, 11 Jun 2014 16:33:17 +0000 (12:33 -0400)]
user/sat context issue in sets
Kshitij Bansal [Wed, 11 Jun 2014 16:09:39 +0000 (12:09 -0400)]
fix in sets rewriter
lianah [Wed, 11 Jun 2014 18:07:17 +0000 (14:07 -0400)]
fixing bv ackermanization cache bug
Morgan Deters [Tue, 10 Jun 2014 21:40:32 +0000 (17:40 -0400)]
Add new --pb-rewrites options to QF_LIA run script for SMT-COMP.
Morgan Deters [Mon, 9 Jun 2014 20:37:59 +0000 (16:37 -0400)]
Some news about API changes.
Tim King [Tue, 10 Jun 2014 21:32:57 +0000 (17:32 -0400)]
Merging Tim's pseudoboolean work from his fmcad14 branch.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
lianah [Tue, 10 Jun 2014 19:07:31 +0000 (15:07 -0400)]
reverting portfolio hack
lianah [Tue, 10 Jun 2014 17:48:45 +0000 (13:48 -0400)]
Merging CAV14 paper bit-vector work.
Morgan Deters [Mon, 9 Jun 2014 14:40:17 +0000 (10:40 -0400)]
Disallow copy/assignment of SmtEngine.
Morgan Deters [Mon, 9 Jun 2014 18:56:42 +0000 (14:56 -0400)]
Tim's options for QF_LIA and QF_LRA---SOI+approx.
Kshitij Bansal [Mon, 9 Jun 2014 17:32:51 +0000 (13:32 -0400)]
Merge pull request #29 from kbansal/alternatefix
Fix for emptyset in smt2 parser, sets translator to quantified logic, misc
Morgan Deters [Mon, 9 Jun 2014 15:05:35 +0000 (11:05 -0400)]
Add missing set of braces, fixes --trace.
Also ensure // commented Debug() lines don't get included in Debug/Trace_tags.
Kshitij Bansal [Mon, 9 Jun 2014 01:40:29 +0000 (21:40 -0400)]
parseErrorHelper : factor out whole word matching
catches some corner cases, more readable too
Kshitij Bansal [Mon, 9 Jun 2014 01:07:15 +0000 (21:07 -0400)]
test for prvs commit (tokenize emptyset)
9978c259f30b1f4b2c70c04589a309033a6eb1f6
Morgan Deters [Mon, 9 Jun 2014 00:10:08 +0000 (20:10 -0400)]
Previous "repeat" fix required extra lookahead (leading to assert-fails). Fixed, at the cost of an antlr warning that's safe to ignore for now.
Kshitij Bansal [Sun, 8 Jun 2014 23:35:39 +0000 (19:35 -0400)]
smt2 parser: tokenize emptyset only if theory enabled
Morgan Deters [Sun, 8 Jun 2014 21:55:23 +0000 (17:55 -0400)]
Better error when there are \backslashes in |quoted symbols|.
Morgan Deters [Sun, 8 Jun 2014 21:54:50 +0000 (17:54 -0400)]
Allow 'repeat' as an SMT-LIB user symbol name (UFNIA/vcc-havoc does this).
Kshitij Bansal [Sun, 8 Jun 2014 21:01:54 +0000 (17:01 -0400)]
sets translate: a different translation using axioms
todo: set logic correctly, split the code for two translators
Kshitij Bansal [Fri, 6 Jun 2014 23:40:18 +0000 (19:40 -0400)]
sets translator: fix for dags
Kshitij Bansal [Fri, 6 Jun 2014 21:43:57 +0000 (17:43 -0400)]
Merge pull request #28 from kbansal/sets
Sets translator, bug fixes
Morgan Deters [Fri, 6 Jun 2014 21:36:16 +0000 (17:36 -0400)]
Fix submission script (again).
Kshitij Bansal [Fri, 6 Jun 2014 20:29:28 +0000 (16:29 -0400)]
rm warning from helloworld example
Tim King [Fri, 6 Jun 2014 15:45:16 +0000 (11:45 -0400)]
Patch for the subtype theoryof mode to make the equalities over disequal types get sent to the theory of the type.
Adding a new test case for bug 569.
Fixes to the normal form of arithmetic so that real terms are before integer terms.
Kshitij Bansal [Fri, 6 Jun 2014 19:32:32 +0000 (15:32 -0400)]
sets: fix equality propagation
Kshitij Bansal [Fri, 6 Jun 2014 01:29:20 +0000 (21:29 -0400)]
-{d,t} help => --show-{debug,trace}-tags
Kshitij Bansal [Fri, 6 Jun 2014 00:35:15 +0000 (20:35 -0400)]
option to hide stats which are zero (off by default), also some aliases
Kshitij Bansal [Fri, 30 May 2014 00:13:52 +0000 (20:13 -0400)]
Sets translate, and other short fixes
- $ is a simple symbol is smt2.
- ever found yourself counting in kind.h? no longer.
- expose parser "logic is set" state for smt/smt2 (any better way?)
- a more helpful assertion message in smt_engine
Morgan Deters [Wed, 4 Jun 2014 22:08:34 +0000 (18:08 -0400)]
SMT-COMP version gets built --with-abc.
Morgan Deters [Thu, 5 Jun 2014 23:08:44 +0000 (19:08 -0400)]
Add --default-dag-thresh to translator, build translator with other examples.
Morgan Deters [Thu, 5 Jun 2014 23:09:30 +0000 (19:09 -0400)]
When printing in SMT, print N-ary bvadd/bvmul/concat/bvand/bvor/bvxor as binary.
Morgan Deters [Wed, 4 Jun 2014 22:34:24 +0000 (18:34 -0400)]
Add operator support (resolves bug #563).
Morgan Deters [Wed, 4 Jun 2014 22:10:08 +0000 (18:10 -0400)]
SmtEngine::checkModel() now checks that model values are of the correct type (related to bug #569).
Morgan Deters [Wed, 4 Jun 2014 21:16:15 +0000 (17:16 -0400)]
Update commit # for get-abc script, anticipating Liana's merge.
Morgan Deters [Wed, 4 Jun 2014 19:22:38 +0000 (15:22 -0400)]
Fix usability issue with tear-down incremental mode.
Morgan Deters [Wed, 4 Jun 2014 19:21:52 +0000 (15:21 -0400)]
SMT strict mode now disallows N-ary use of concat, bvadd, bvmul, bvand, bvor, and bvxor.
Morgan Deters [Wed, 4 Jun 2014 00:14:42 +0000 (20:14 -0400)]
Fixing run-script for smt-comp
Morgan Deters [Tue, 3 Jun 2014 23:59:32 +0000 (19:59 -0400)]
Another check when making SMT-COMP submission zipfiles.
Morgan Deters [Tue, 3 Jun 2014 23:01:01 +0000 (19:01 -0400)]
Fix StarExec description files for new requirements.
ajreynol [Tue, 3 Jun 2014 12:01:01 +0000 (14:01 +0200)]
Support E-matching/QCF for Set operators.
Morgan Deters [Sun, 1 Jun 2014 17:21:05 +0000 (13:21 -0400)]
Fix for Windows builds (rlimit doesn't exist on Windows).
Morgan Deters [Fri, 30 May 2014 23:31:12 +0000 (19:31 -0400)]
More make rules
Morgan Deters [Fri, 30 May 2014 22:01:47 +0000 (18:01 -0400)]
One final bit (I hope) of make magic
Morgan Deters [Fri, 30 May 2014 21:58:48 +0000 (17:58 -0400)]
More make rules
Morgan Deters [Fri, 30 May 2014 21:07:38 +0000 (17:07 -0400)]
Bug fix for string-opt2 (copied from Tianyi's branch).
Morgan Deters [Fri, 30 May 2014 19:41:20 +0000 (15:41 -0400)]
Update submission make rules.
ajreynol [Fri, 30 May 2014 19:30:23 +0000 (21:30 +0200)]
Change SMT COMP script to use external timeouts.
Morgan Deters [Fri, 30 May 2014 19:00:38 +0000 (15:00 -0400)]
Run script updates: no --stats, also application-track version.
Kshitij Bansal [Fri, 30 May 2014 18:38:05 +0000 (14:38 -0400)]
run script fix
ajreynol [Fri, 30 May 2014 13:48:53 +0000 (15:48 +0200)]
Improve --dt-stc-ind for multi-variable datatype properties.
ajreynol [Fri, 30 May 2014 10:17:05 +0000 (12:17 +0200)]
Fixes for --inst-max-level
Morgan Deters [Fri, 30 May 2014 04:11:44 +0000 (00:11 -0400)]
Fix personal.mk for some make targets.
ajreynol [Wed, 28 May 2014 21:32:59 +0000 (23:32 +0200)]
Minor changes to script. Disable cbqi sat.
Andrew Reynolds [Wed, 28 May 2014 07:28:39 +0000 (02:28 -0500)]
Add option to avoid dumping partial models/proofs.
Morgan Deters [Wed, 28 May 2014 03:35:40 +0000 (23:35 -0400)]
Some fixes to GC order in Java.
Kshitij Bansal [Tue, 27 May 2014 21:51:07 +0000 (17:51 -0400)]
Merge pull request #27 from kbansal/statistics
update stats_black
Kshitij Bansal [Tue, 27 May 2014 20:16:55 +0000 (16:16 -0400)]
update stats_black
Morgan Deters [Tue, 5 Mar 2013 00:58:15 +0000 (19:58 -0500)]
New --tear-down-incremental mode, useful for debugging and performance profiling.
Kshitij Bansal [Tue, 27 May 2014 18:46:11 +0000 (14:46 -0400)]
fix timespec printing
sorry prvs fix added some unrelated code
Kshitij Bansal [Tue, 27 May 2014 18:43:46 +0000 (14:43 -0400)]
Revert "timespec printing bug"
This reverts commit
9006b759cfa01c6006196e0716c2d67c760556a6.
Kshitij Bansal [Tue, 27 May 2014 18:41:47 +0000 (14:41 -0400)]
timespec printing bug
Morgan Deters [Tue, 27 May 2014 04:07:17 +0000 (00:07 -0400)]
Fix typo in Java destruction code; should fix some recent bug reports of crashes in Java.
Morgan Deters [Tue, 27 May 2014 04:06:42 +0000 (00:06 -0400)]
Improved type-checking for tuple and record selects.
Kshitij Bansal [Tue, 27 May 2014 00:22:55 +0000 (20:22 -0400)]
Fix bug 567
This bug got introduced in
96eccb0d6134ccf4ead0134299b2e3750a890083.
The backing Node didn't always exist because of the changes.
Clark Barrett [Mon, 26 May 2014 19:30:13 +0000 (12:30 -0700)]
Fixing Tim's subtype/solving bug for arrays
Tim King [Mon, 26 May 2014 15:44:38 +0000 (11:44 -0400)]
Separating an implicit inclusion of smt_engine.h from theory.h.
Tim King [Mon, 26 May 2014 14:12:19 +0000 (10:12 -0400)]
Fixing a soundness bug due to the default implmentation of Theory::ppAssert() not respecting subtyping.
Andrew Reynolds [Sun, 25 May 2014 14:18:42 +0000 (09:18 -0500)]
Improve quantifier instantiation: always use original terms when matching (was missing for simple triggers). Minor updates to scripts.
Morgan Deters [Sun, 25 May 2014 00:16:46 +0000 (20:16 -0400)]
Some cleanup, fix warnings raised by Debian packager.
Andrew Reynolds [Fri, 23 May 2014 21:59:48 +0000 (16:59 -0500)]
Fix bug in E-matching Real/Int terms.