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.
Andrew Reynolds [Sat, 10 May 2014 20:14:34 +0000 (15:14 -0500)]
Bug fixes to CBQI. Add first draft of CASC j7 TFF script. Add regression, minor changes.
Morgan Deters [Fri, 9 May 2014 15:11:31 +0000 (11:11 -0400)]
Fix for example installation.
Andrew Reynolds [Fri, 9 May 2014 21:53:57 +0000 (16:53 -0500)]
Initial draft of run scripts for CASC j7
Andrew Reynolds [Fri, 9 May 2014 11:51:43 +0000 (06:51 -0500)]
Add variable ordering to ambqi. Bug fix to macros. More preparation for CASC proofs.
ajreynol [Thu, 8 May 2014 16:18:53 +0000 (18:18 +0200)]
Major simplifications to macros module.
Andrew Reynolds [Thu, 8 May 2014 13:13:05 +0000 (08:13 -0500)]
Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. Minor fixes to ambqi. Preparation for CASC proof output. Add NNF option.
Andrew Reynolds [Thu, 8 May 2014 07:18:54 +0000 (02:18 -0500)]
Basic optimizations for ambqi : only normalize UF applied to variables, direct handling of NOT
Dejan Jovanovic [Thu, 8 May 2014 06:26:42 +0000 (23:26 -0700)]
Adding encoding of sha1 collision for the hashing example
Tianyi Liang [Thu, 8 May 2014 00:32:03 +0000 (19:32 -0500)]
patch to the last commit: add a single character case
Tianyi Liang [Wed, 7 May 2014 20:49:09 +0000 (15:49 -0500)]
fix a bug in contain
Tianyi Liang [Wed, 7 May 2014 19:45:57 +0000 (14:45 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Wed, 7 May 2014 19:43:42 +0000 (14:43 -0500)]
add splits
Tianyi Liang [Wed, 7 May 2014 19:43:42 +0000 (14:43 -0500)]
add splits
Andrew Reynolds [Wed, 7 May 2014 18:36:58 +0000 (13:36 -0500)]
Fixes to ambqi, now solution-sound.
Andrew Reynolds [Tue, 6 May 2014 13:19:04 +0000 (08:19 -0500)]
First draft of ambqi_builder (new implementation of MBQI based on disjoint sets).
Tianyi Liang [Tue, 6 May 2014 01:17:31 +0000 (20:17 -0500)]
fix a bug in replace and contains
Tianyi Liang [Mon, 5 May 2014 23:01:14 +0000 (18:01 -0500)]
add constant regular expression check for intersection.
Tim King [Mon, 5 May 2014 21:20:38 +0000 (17:20 -0400)]
Improving documentation for glpk-cut-log switch.
Morgan Deters [Mon, 5 May 2014 18:10:10 +0000 (14:10 -0400)]
Valuation::entailmentCheck() proxy for TheoryEngine version. Signature and contract is the same as for TheoryEngine version.
Morgan Deters [Fri, 2 May 2014 23:22:26 +0000 (19:22 -0400)]
Fix typo in bitvectors example; thanks to Adam Gashlin for reporting the issue.
Andrew Reynolds [Fri, 2 May 2014 21:25:56 +0000 (16:25 -0500)]
Simplification of EqualityEngine::areDisequal. Comparison for production : church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6444&reference_id=6445&p=5. Comparison for debug : http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6449&reference_id=6446&p=5.
ajreynol [Fri, 2 May 2014 12:45:09 +0000 (14:45 +0200)]
Fix assertion from previous commit.
Andrew Reynolds [Fri, 2 May 2014 12:11:08 +0000 (07:11 -0500)]
Add option --dt-stc-ind for strengthening skolemization. Refactor skolemization.
ajreynol [Fri, 2 May 2014 08:57:51 +0000 (10:57 +0200)]
More minor optimizations for datatypes.
ajreynol [Thu, 1 May 2014 11:28:56 +0000 (13:28 +0200)]
Minor optimizations to datatypes, revert to checkClash not mod eq. Minor clean up.
Kshitij Bansal [Thu, 1 May 2014 04:04:21 +0000 (00:04 -0400)]
Merge remote-tracking branch 'upstream/master' into sets
Kshitij Bansal [Wed, 30 Apr 2014 20:09:32 +0000 (16:09 -0400)]
decision engine: cache start index for and/or nodes
This is done only in "hard" case. Limited testing has not shown
improvement in the "easy" case.
This was triggerred by a benchmark sent by andy/viktor.
performance comparison notes for the change on wiki
http://church.cims.nyu.edu/wiki/User:Kshitij/decisioncacheindex
Tim King [Wed, 30 Apr 2014 21:28:00 +0000 (17:28 -0400)]
T-entailment work, and QCF (quant conflict find) work that uses it.
This commit includes work from the past month on the T-entailment check
infrastructure (due to Tim), an entailment check for arithmetic
(also Tim), and QCF work that uses T-entailment (due to Andrew Reynolds).
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Morgan Deters [Wed, 30 Apr 2014 01:57:16 +0000 (21:57 -0400)]
Fix warnings, cleanup in strings typechecker.
Morgan Deters [Wed, 30 Apr 2014 01:48:49 +0000 (21:48 -0400)]
Fix compiler warning re: TheoryUF destructor.
Morgan Deters [Wed, 30 Apr 2014 01:28:25 +0000 (21:28 -0400)]
Fix simplify output for SMT2 printer.
Morgan Deters [Tue, 29 Apr 2014 22:04:38 +0000 (18:04 -0400)]
Fix for (user) context-dependence of arith TO_INT/IS_INT rewriting and rewrite-divk.
Morgan Deters [Tue, 29 Apr 2014 23:51:29 +0000 (19:51 -0400)]
Mostly resolves bug #561 memory leaks, and more.
Morgan Deters [Tue, 29 Apr 2014 21:57:17 +0000 (17:57 -0400)]
Fix for --force-logic to extend its reach to the parser.
Kshitij Bansal [Tue, 29 Apr 2014 23:38:29 +0000 (19:38 -0400)]
fixed couple of more warnings
Kshitij Bansal [Tue, 29 Apr 2014 23:07:20 +0000 (19:07 -0400)]
fix was compiler warning in antlr_input, crashing test case with the old fix
Morgan Deters [Tue, 29 Apr 2014 22:14:34 +0000 (18:14 -0400)]
Revert a compiler warning fix from
ea6a5a6.
Tianyi Liang [Tue, 29 Apr 2014 21:54:26 +0000 (16:54 -0500)]
fix a typo: --string-exp => --strings-exp; fix a signed int warning in antlr
Tianyi Liang [Tue, 29 Apr 2014 20:32:38 +0000 (15:32 -0500)]
add leading zeros support for str.to.int
ajreynol [Tue, 29 Apr 2014 13:39:11 +0000 (15:39 +0200)]
Significantly improve performance for producing datatypes models.