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.
Morgan Deters [Wed, 21 May 2014 17:55:13 +0000 (13:55 -0400)]
Safer swig-wrapping for unsigned long long in Java, which will throw an exception if the argument is out of bounds for unsigned long long. Thanks to Steve Siegel for the report.
Morgan Deters [Fri, 16 May 2014 03:33:55 +0000 (23:33 -0400)]
Fix compiler warning (missing virtual dtor)
Tim King [Mon, 19 May 2014 19:14:54 +0000 (15:14 -0400)]
More documentation fixes. Apologies for multiple commits.
Tim King [Mon, 19 May 2014 19:12:54 +0000 (15:12 -0400)]
Fixing documentation for glpk configuration.
Tianyi Liang [Mon, 19 May 2014 02:06:29 +0000 (21:06 -0500)]
minor fix for string equality engine assertion.
Kshitij Bansal [Sat, 17 May 2014 06:43:55 +0000 (02:43 -0400)]
Merge pull request #26 from kbansal/sets
Sets
Kshitij Bansal [Fri, 16 May 2014 22:38:22 +0000 (18:38 -0400)]
lfsc_checker: fix some warnings reported by _both_ gcc and clang
Kshitij Bansal [Fri, 16 May 2014 22:18:35 +0000 (18:18 -0400)]
sets: fix a bug in model building, another in handling set of sets
Kshitij Bansal [Fri, 16 May 2014 17:41:31 +0000 (13:41 -0400)]
minor improvements (fixes) to did-you-mean suggestions
Andrew Reynolds [Thu, 15 May 2014 17:51:35 +0000 (12:51 -0500)]
Minor fixes. Add SMTCOMP 2014 script.
Andrew Reynolds [Wed, 14 May 2014 19:46:53 +0000 (14:46 -0500)]
Finish --dump-instantiations option. Update scripts.
Tianyi Liang [Tue, 13 May 2014 20:22:38 +0000 (15:22 -0500)]
Reject native extended ASCII characters. It requires user to use escaped sequence for an extended ASCII character.
Tianyi Liang [Tue, 13 May 2014 16:16:06 +0000 (11:16 -0500)]
Reject un-escaped extended ASCII characters
ajreynol [Tue, 13 May 2014 15:18:18 +0000 (17:18 +0200)]
Add lazy strategy for bounded integers to avoid non-terminating unsat cases. Add regressions.
Tianyi Liang [Tue, 13 May 2014 02:03:25 +0000 (21:03 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Tue, 13 May 2014 02:02:24 +0000 (21:02 -0500)]
Fix a bug in the IndexOf function.
Tianyi Liang [Tue, 13 May 2014 02:02:24 +0000 (21:02 -0500)]
Fix a bug in the IndexOf function.
Andrew Reynolds [Mon, 12 May 2014 19:15:40 +0000 (14:15 -0500)]
Minor updates/fix to --cbqi-recurse
Tim King [Mon, 12 May 2014 17:10:16 +0000 (13:10 -0400)]
Merge remote-tracking branch 'timothy-king/master'
Tim King [Mon, 12 May 2014 17:08:53 +0000 (13:08 -0400)]
Merging in additional glpk options and statistics from CAV submission.
Tianyi Liang [Mon, 12 May 2014 16:10:06 +0000 (11:10 -0500)]
Add a benchmark that detects a bug in parsing. Thank Vijay for his bug report.
Tianyi Liang [Mon, 12 May 2014 03:14:46 +0000 (22:14 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Mon, 12 May 2014 03:13:17 +0000 (22:13 -0500)]
Replace lemma sending with EQ assertions. Fix a typo in hex_to_int function.
Tianyi Liang [Mon, 12 May 2014 03:13:17 +0000 (22:13 -0500)]
Replace lemma sending with EQ assertions. Fix a typo in hex_to_int function.
Andrew Reynolds [Sun, 11 May 2014 19:36:50 +0000 (14:36 -0500)]
More preparation for CASC proofs. Minor fix for sort inference (rewrite new assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.