Kshitij Bansal [Sun, 22 Jun 2014 05:17:27 +0000 (01:17 -0400)]
Renaming of SMT2 operator names, kinds for set theory
* SET_SINGLETON kind renamed to just SINGLETON
* "setenum" smt2 opertor renamed to "singleton"[1]
* "in" smt2 operator renamed to "member"[2]
[1] It was anyhow accepting exactly one argument, so was bit misleading
to call set enumerator.
[2] The corresponding kind was called MEMBER, so this will also make them
consistent. Only inconsistency now is for subset: kind is called
SUBSET but operator is called "subseteq".
Morgan Deters [Fri, 20 Jun 2014 23:59:48 +0000 (19:59 -0400)]
Sets kinds documentation
lianah [Sat, 21 Jun 2014 21:45:31 +0000 (17:45 -0400)]
fixed build failure
Morgan Deters [Sat, 21 Jun 2014 02:25:21 +0000 (22:25 -0400)]
Implement RecordProperties::mkGroundTerm(). Resolves bug #546.
lianah [Thu, 19 Jun 2014 22:52:55 +0000 (18:52 -0400)]
fixed merge conflict
lianah [Thu, 19 Jun 2014 22:19:25 +0000 (18:19 -0400)]
added model generation to eager bit-blasting and turned abc off by default
lianah [Thu, 19 Jun 2014 21:11:19 +0000 (17:11 -0400)]
update to abc install instructions
Morgan Deters [Thu, 19 Jun 2014 07:31:00 +0000 (03:31 -0400)]
Better --segv-spin messages.
Morgan Deters [Thu, 19 Jun 2014 07:30:51 +0000 (03:30 -0400)]
Fix make install-examples.
Morgan Deters [Thu, 19 Jun 2014 02:02:15 +0000 (22:02 -0400)]
Proper escaping in option documentation.
Morgan Deters [Thu, 19 Jun 2014 00:44:09 +0000 (20:44 -0400)]
Version of the run script that works with trace executor; waiting on StarExec infrastructure for testing.
Kshitij Bansal [Wed, 18 Jun 2014 20:09:18 +0000 (16:09 -0400)]
forgot to add the test with fix
according to bug report, fix was in 6267f3
Kshitij Bansal [Wed, 18 Jun 2014 19:51:57 +0000 (15:51 -0400)]
basic fixes for sets translator, separate binaries
Morgan Deters [Wed, 18 Jun 2014 19:41:02 +0000 (15:41 -0400)]
Options script fix.
Morgan Deters [Wed, 18 Jun 2014 19:30:32 +0000 (15:30 -0400)]
Fix for mac readline.
Morgan Deters [Wed, 18 Jun 2014 16:02:37 +0000 (12:02 -0400)]
Better error for invalid concrete syntax of sorts with too many parens, like (Int). Thanks to Dan Liew for the report.
Morgan Deters [Wed, 18 Jun 2014 04:10:38 +0000 (00:10 -0400)]
Fix GLPK builds: correct access specifier on cut classes.
Morgan Deters [Wed, 18 Jun 2014 01:24:26 +0000 (21:24 -0400)]
Java bindings fixes.
Morgan Deters [Wed, 18 Jun 2014 01:39:05 +0000 (21:39 -0400)]
Minor Doxygen fixes.
Kshitij Bansal [Wed, 18 Jun 2014 03:03:22 +0000 (23:03 -0400)]
disable unate lemmas when using incremental mode
Morgan Deters [Wed, 18 Jun 2014 00:21:12 +0000 (20:21 -0400)]
Fix for pre-C++11 is_sorted().
Morgan Deters [Tue, 17 Jun 2014 22:33:28 +0000 (18:33 -0400)]
More minor code cleanup.
Morgan Deters [Tue, 17 Jun 2014 20:58:43 +0000 (16:58 -0400)]
No more dependence on libstdc++ or PBDS stuff: remove build stuff that supported it.
Morgan Deters [Tue, 17 Jun 2014 19:58:04 +0000 (15:58 -0400)]
New translator features: expand define-funs and combine assertions.
Morgan Deters [Tue, 17 Jun 2014 21:29:58 +0000 (17:29 -0400)]
Code cleanup.
Morgan Deters [Tue, 17 Jun 2014 21:29:49 +0000 (17:29 -0400)]
Documentation clean-ups.
Morgan Deters [Tue, 17 Jun 2014 21:35:37 +0000 (17:35 -0400)]
Another fix for the CASC stuff.
Morgan Deters [Tue, 17 Jun 2014 21:29:12 +0000 (17:29 -0400)]
Final preparations for arithmetic for building with libc++.
Morgan Deters [Tue, 17 Jun 2014 20:32:47 +0000 (16:32 -0400)]
Fix for new CASC features, fixes Java builds.
Morgan Deters [Tue, 17 Jun 2014 20:00:50 +0000 (16:00 -0400)]
Some reversions of recent commits re: portfolio failure.
* Partial reversion of
b8e28a7, do it a different way.
* Revert "Test portfolio with --no-wait-to-join."
This reverts commit
8b56004ee8bf6c34aaf045bec12bf0e4401a044c.
Tim King [Tue, 17 Jun 2014 15:55:51 +0000 (11:55 -0400)]
This commit adds a priority queue implementation. This is to avoid compilation troubles with libc++.
Morgan Deters [Tue, 17 Jun 2014 13:56:39 +0000 (09:56 -0400)]
Test portfolio with --no-wait-to-join.
ajreynol [Tue, 17 Jun 2014 13:25:58 +0000 (15:25 +0200)]
For casc : print models of functions rewritten by sort inference.
Morgan Deters [Tue, 17 Jun 2014 03:44:57 +0000 (23:44 -0400)]
Fix rewriter typo.
Morgan Deters [Tue, 17 Jun 2014 03:26:49 +0000 (23:26 -0400)]
Clean up glpk detection a little, fix a detection bug.
Morgan Deters [Tue, 17 Jun 2014 02:37:35 +0000 (22:37 -0400)]
fix typo
Morgan Deters [Tue, 17 Jun 2014 02:35:14 +0000 (22:35 -0400)]
More application-track fixes for use with trace executor.
Morgan Deters [Mon, 16 Jun 2014 02:08:56 +0000 (22:08 -0400)]
Versioning preparation.
Morgan Deters [Mon, 16 Jun 2014 23:59:24 +0000 (19:59 -0400)]
Some fixes for tear-down-incremental and "success" output.
Morgan Deters [Mon, 16 Jun 2014 20:43:56 +0000 (16:43 -0400)]
Disallow context-dependent copy/assignment.
Morgan Deters [Mon, 16 Jun 2014 02:30:48 +0000 (22:30 -0400)]
Fix compile errors with some versions of GCC.
Morgan Deters [Mon, 16 Jun 2014 02:30:39 +0000 (22:30 -0400)]
Clean up some compiler warnings on 32-bit.
Morgan Deters [Mon, 16 Jun 2014 20:40:56 +0000 (16:40 -0400)]
Minor fixes to get-abc script and configure stuff.
Morgan Deters [Mon, 16 Jun 2014 20:05:12 +0000 (16:05 -0400)]
get-glpk-cut-log script, and configure code.
Morgan Deters [Mon, 16 Jun 2014 19:19:39 +0000 (15:19 -0400)]
dos2unix-convert some sources.
Morgan Deters [Wed, 30 Apr 2014 16:51:02 +0000 (12:51 -0400)]
Minor fixes, spelling etc.
ajreynol [Mon, 16 Jun 2014 16:05:36 +0000 (18:05 +0200)]
More proof support for CASC : include skolemization
Morgan Deters [Mon, 16 Jun 2014 03:08:50 +0000 (23:08 -0400)]
minor update to application track config in QF_BV
Morgan Deters [Thu, 19 Jun 2014 07:37:33 +0000 (03:37 -0400)]
More doc fixes; fixes some lintian warnings.
Morgan Deters [Thu, 19 Jun 2014 07:31:00 +0000 (03:31 -0400)]
Better --segv-spin messages.
Morgan Deters [Thu, 19 Jun 2014 07:30:51 +0000 (03:30 -0400)]
Fix make install-examples.
Morgan Deters [Thu, 19 Jun 2014 02:02:15 +0000 (22:02 -0400)]
Proper escaping in option documentation.
Morgan Deters [Thu, 19 Jun 2014 00:44:09 +0000 (20:44 -0400)]
Version of the run script that works with trace executor; waiting on StarExec infrastructure for testing.
Kshitij Bansal [Wed, 18 Jun 2014 20:11:32 +0000 (16:11 -0400)]
Merge remote-tracking branch 'upstream/master' into sets
Kshitij Bansal [Wed, 18 Jun 2014 20:09:18 +0000 (16:09 -0400)]
forgot to add the test with fix
according to bug report, fix was in 6267f3
Kshitij Bansal [Wed, 18 Jun 2014 19:51:57 +0000 (15:51 -0400)]
basic fixes for sets translator, separate binaries
Morgan Deters [Wed, 18 Jun 2014 19:41:02 +0000 (15:41 -0400)]
Options script fix.
Morgan Deters [Wed, 18 Jun 2014 19:30:32 +0000 (15:30 -0400)]
Fix for mac readline.
Morgan Deters [Wed, 18 Jun 2014 16:02:37 +0000 (12:02 -0400)]
Better error for invalid concrete syntax of sorts with too many parens, like (Int). Thanks to Dan Liew for the report.
Morgan Deters [Wed, 18 Jun 2014 04:10:38 +0000 (00:10 -0400)]
Fix GLPK builds: correct access specifier on cut classes.
Morgan Deters [Wed, 18 Jun 2014 01:24:26 +0000 (21:24 -0400)]
Java bindings fixes.
Morgan Deters [Wed, 18 Jun 2014 01:39:05 +0000 (21:39 -0400)]
Minor Doxygen fixes.
Kshitij Bansal [Wed, 18 Jun 2014 03:03:22 +0000 (23:03 -0400)]
disable unate lemmas when using incremental mode
Morgan Deters [Wed, 18 Jun 2014 00:21:12 +0000 (20:21 -0400)]
Fix for pre-C++11 is_sorted().
Morgan Deters [Tue, 17 Jun 2014 22:33:28 +0000 (18:33 -0400)]
More minor code cleanup.
Morgan Deters [Tue, 17 Jun 2014 20:58:43 +0000 (16:58 -0400)]
No more dependence on libstdc++ or PBDS stuff: remove build stuff that supported it.
Morgan Deters [Tue, 17 Jun 2014 19:58:04 +0000 (15:58 -0400)]
New translator features: expand define-funs and combine assertions.
Tim King [Tue, 17 Jun 2014 22:39:45 +0000 (18:39 -0400)]
Merge pull request #33 from mdeters/arith-proposal
Final preparations for arithmetic for building with libc++.
Morgan Deters [Tue, 17 Jun 2014 21:29:58 +0000 (17:29 -0400)]
Code cleanup.
Morgan Deters [Tue, 17 Jun 2014 21:29:49 +0000 (17:29 -0400)]
Documentation clean-ups.
Morgan Deters [Tue, 17 Jun 2014 21:35:37 +0000 (17:35 -0400)]
Another fix for the CASC stuff.
Morgan Deters [Tue, 17 Jun 2014 21:29:12 +0000 (17:29 -0400)]
Final preparations for arithmetic for building with libc++.
Morgan Deters [Tue, 17 Jun 2014 20:32:47 +0000 (16:32 -0400)]
Fix for new CASC features, fixes Java builds.
Morgan Deters [Tue, 17 Jun 2014 20:00:50 +0000 (16:00 -0400)]
Some reversions of recent commits re: portfolio failure.
* Partial reversion of
b8e28a7, do it a different way.
* Revert "Test portfolio with --no-wait-to-join."
This reverts commit
8b56004ee8bf6c34aaf045bec12bf0e4401a044c.
Tim King [Tue, 17 Jun 2014 15:55:51 +0000 (11:55 -0400)]
This commit adds a priority queue implementation. This is to avoid compilation troubles with libc++.
Morgan Deters [Tue, 17 Jun 2014 13:56:39 +0000 (09:56 -0400)]
Test portfolio with --no-wait-to-join.
ajreynol [Tue, 17 Jun 2014 13:25:58 +0000 (15:25 +0200)]
For casc : print models of functions rewritten by sort inference.
Morgan Deters [Tue, 17 Jun 2014 03:44:57 +0000 (23:44 -0400)]
Fix rewriter typo.
Morgan Deters [Tue, 17 Jun 2014 03:26:49 +0000 (23:26 -0400)]
Clean up glpk detection a little, fix a detection bug.
Morgan Deters [Tue, 17 Jun 2014 02:37:35 +0000 (22:37 -0400)]
fix typo
Morgan Deters [Tue, 17 Jun 2014 02:35:14 +0000 (22:35 -0400)]
More application-track fixes for use with trace executor.
Morgan Deters [Mon, 16 Jun 2014 02:08:56 +0000 (22:08 -0400)]
Versioning preparation.
Morgan Deters [Mon, 16 Jun 2014 23:59:24 +0000 (19:59 -0400)]
Some fixes for tear-down-incremental and "success" output.
Morgan Deters [Mon, 16 Jun 2014 20:43:56 +0000 (16:43 -0400)]
Disallow context-dependent copy/assignment.
Morgan Deters [Mon, 16 Jun 2014 02:30:48 +0000 (22:30 -0400)]
Fix compile errors with some versions of GCC.
Morgan Deters [Mon, 16 Jun 2014 02:30:39 +0000 (22:30 -0400)]
Clean up some compiler warnings on 32-bit.
Morgan Deters [Mon, 16 Jun 2014 20:40:56 +0000 (16:40 -0400)]
Minor fixes to get-abc script and configure stuff.
Morgan Deters [Mon, 16 Jun 2014 20:05:12 +0000 (16:05 -0400)]
get-glpk-cut-log script, and configure code.
Morgan Deters [Mon, 16 Jun 2014 19:19:39 +0000 (15:19 -0400)]
dos2unix-convert some sources.
Morgan Deters [Wed, 30 Apr 2014 16:51:02 +0000 (12:51 -0400)]
Minor fixes, spelling etc.
ajreynol [Mon, 16 Jun 2014 16:05:36 +0000 (18:05 +0200)]
More proof support for CASC : include skolemization
Morgan Deters [Mon, 16 Jun 2014 03:08:50 +0000 (23:08 -0400)]
minor update to application track config in QF_BV
lianah [Mon, 16 Jun 2014 01:33:51 +0000 (21:33 -0400)]
core solver fix
Morgan Deters [Mon, 16 Jun 2014 00:16:35 +0000 (20:16 -0400)]
Careful there aren't too many "success" messages with --tear-down-incremental (can confuse trace runner).
lianah [Mon, 16 Jun 2014 00:36:12 +0000 (20:36 -0400)]
fixed bv bug due to applying equisatisfiable transformations in ppRewrite
Morgan Deters [Sun, 15 Jun 2014 23:54:19 +0000 (19:54 -0400)]
Application trace executor (if they end up using that) requires --print-success.
Morgan Deters [Sun, 15 Jun 2014 21:29:13 +0000 (17:29 -0400)]
One last(?) fix for build script for smtcomp uploads.
lianah [Sun, 15 Jun 2014 20:10:32 +0000 (16:10 -0400)]
fixed fuzzer assertion failures for bv
Morgan Deters [Sun, 15 Jun 2014 06:05:17 +0000 (02:05 -0400)]
fix travis config
Morgan Deters [Sun, 15 Jun 2014 05:29:53 +0000 (01:29 -0400)]
better bv args for smtcomp