cvc5.git
10 years agoAPI documentation improvements.
Morgan Deters [Sun, 22 Jun 2014 01:10:12 +0000 (21:10 -0400)]
API documentation improvements.

10 years agoFix to the compatibility library (this does fix the build).
Morgan Deters [Sun, 22 Jun 2014 00:12:42 +0000 (20:12 -0400)]
Fix to the compatibility library (this does fix the build).

10 years agoFix compat-Java layer, should fix build.
Morgan Deters [Sat, 21 Jun 2014 23:30:32 +0000 (19:30 -0400)]
Fix compat-Java layer, should fix build.

10 years agoLower the Java JRE version requirement.
Morgan Deters [Sat, 21 Jun 2014 22:15:57 +0000 (18:15 -0400)]
Lower the Java JRE version requirement.

10 years agoAdjust library dependencies to be more correct (fixes lintian warnings).
Morgan Deters [Sat, 21 Jun 2014 21:28:01 +0000 (17:28 -0400)]
Adjust library dependencies to be more correct (fixes lintian warnings).

10 years agoAdd some missing functions in configuration and compat library.
Morgan Deters [Sat, 21 Jun 2014 21:15:24 +0000 (17:15 -0400)]
Add some missing functions in configuration and compat library.

10 years agoSlightly-improved kinds documentation for builtin, Boolean, arrays, strings, and...
Morgan Deters [Sat, 21 Jun 2014 00:00:22 +0000 (20:00 -0400)]
Slightly-improved kinds documentation for builtin, Boolean, arrays, strings, and arith.

10 years agoMinor fixes for man pages.
Morgan Deters [Sat, 21 Jun 2014 22:11:39 +0000 (18:11 -0400)]
Minor fixes for man pages.

10 years agoSome minor cleanup and documentation.
Morgan Deters [Fri, 20 Jun 2014 18:17:01 +0000 (14:17 -0400)]
Some minor cleanup and documentation.

10 years agofixed build failure
lianah [Sat, 21 Jun 2014 21:45:31 +0000 (17:45 -0400)]
fixed build failure

10 years agoImplement RecordProperties::mkGroundTerm(). Resolves bug #546.
Morgan Deters [Sat, 21 Jun 2014 02:25:21 +0000 (22:25 -0400)]
Implement RecordProperties::mkGroundTerm().  Resolves bug #546.

10 years agofixed merge conflict
lianah [Thu, 19 Jun 2014 22:52:55 +0000 (18:52 -0400)]
fixed merge conflict

10 years agoadded model generation to eager bit-blasting and turned abc off by default
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

10 years agoupdate to abc install instructions
lianah [Thu, 19 Jun 2014 21:11:19 +0000 (17:11 -0400)]
update to abc install instructions

10 years agoBetter --segv-spin messages.
Morgan Deters [Thu, 19 Jun 2014 07:31:00 +0000 (03:31 -0400)]
Better --segv-spin messages.

10 years agoFix make install-examples.
Morgan Deters [Thu, 19 Jun 2014 07:30:51 +0000 (03:30 -0400)]
Fix make install-examples.

10 years agoProper escaping in option documentation.
Morgan Deters [Thu, 19 Jun 2014 02:02:15 +0000 (22:02 -0400)]
Proper escaping in option documentation.

10 years agoVersion of the run script that works with trace executor; waiting on StarExec infrast...
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.

10 years agoforgot to add the test with fix
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

10 years agobasic fixes for sets translator, separate binaries
Kshitij Bansal [Wed, 18 Jun 2014 19:51:57 +0000 (15:51 -0400)]
basic fixes for sets translator, separate binaries

10 years agoOptions script fix.
Morgan Deters [Wed, 18 Jun 2014 19:41:02 +0000 (15:41 -0400)]
Options script fix.

10 years agoFix for mac readline.
Morgan Deters [Wed, 18 Jun 2014 19:30:32 +0000 (15:30 -0400)]
Fix for mac readline.

10 years agoBetter error for invalid concrete syntax of sorts with too many parens, like (Int...
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.

10 years agoFix GLPK builds: correct access specifier on cut classes.
Morgan Deters [Wed, 18 Jun 2014 04:10:38 +0000 (00:10 -0400)]
Fix GLPK builds: correct access specifier on cut classes.

10 years agoJava bindings fixes.
Morgan Deters [Wed, 18 Jun 2014 01:24:26 +0000 (21:24 -0400)]
Java bindings fixes.

10 years agoMinor Doxygen fixes.
Morgan Deters [Wed, 18 Jun 2014 01:39:05 +0000 (21:39 -0400)]
Minor Doxygen fixes.

10 years agodisable unate lemmas when using incremental mode
Kshitij Bansal [Wed, 18 Jun 2014 03:03:22 +0000 (23:03 -0400)]
disable unate lemmas when using incremental mode

10 years agoFix for pre-C++11 is_sorted().
Morgan Deters [Wed, 18 Jun 2014 00:21:12 +0000 (20:21 -0400)]
Fix for pre-C++11 is_sorted().

10 years agoMore minor code cleanup.
Morgan Deters [Tue, 17 Jun 2014 22:33:28 +0000 (18:33 -0400)]
More minor code cleanup.

10 years agoNo more dependence on libstdc++ or PBDS stuff: remove build stuff that supported it.
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.

10 years agoNew translator features: expand define-funs and combine assertions.
Morgan Deters [Tue, 17 Jun 2014 19:58:04 +0000 (15:58 -0400)]
New translator features: expand define-funs and combine assertions.

10 years agoCode cleanup.
Morgan Deters [Tue, 17 Jun 2014 21:29:58 +0000 (17:29 -0400)]
Code cleanup.

10 years agoDocumentation clean-ups.
Morgan Deters [Tue, 17 Jun 2014 21:29:49 +0000 (17:29 -0400)]
Documentation clean-ups.

10 years agoAnother fix for the CASC stuff.
Morgan Deters [Tue, 17 Jun 2014 21:35:37 +0000 (17:35 -0400)]
Another fix for the CASC stuff.

10 years agoFinal preparations for arithmetic for building with libc++.
Morgan Deters [Tue, 17 Jun 2014 21:29:12 +0000 (17:29 -0400)]
Final preparations for arithmetic for building with libc++.

10 years agoFix for new CASC features, fixes Java builds.
Morgan Deters [Tue, 17 Jun 2014 20:32:47 +0000 (16:32 -0400)]
Fix for new CASC features, fixes Java builds.

10 years agoSome reversions of recent commits re: portfolio failure.
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.

10 years agoThis commit adds a priority queue implementation. This is to avoid compilation troub...
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++.

10 years agoTest portfolio with --no-wait-to-join.
Morgan Deters [Tue, 17 Jun 2014 13:56:39 +0000 (09:56 -0400)]
Test portfolio with --no-wait-to-join.

10 years agoFor casc : print models of functions rewritten by sort inference.
ajreynol [Tue, 17 Jun 2014 13:25:58 +0000 (15:25 +0200)]
For casc : print models of functions rewritten by sort inference.

10 years agoFix rewriter typo.
Morgan Deters [Tue, 17 Jun 2014 03:44:57 +0000 (23:44 -0400)]
Fix rewriter typo.

10 years agoClean up glpk detection a little, fix a detection bug.
Morgan Deters [Tue, 17 Jun 2014 03:26:49 +0000 (23:26 -0400)]
Clean up glpk detection a little, fix a detection bug.

10 years agofix typo
Morgan Deters [Tue, 17 Jun 2014 02:37:35 +0000 (22:37 -0400)]
fix typo

10 years agoMore application-track fixes for use with trace executor.
Morgan Deters [Tue, 17 Jun 2014 02:35:14 +0000 (22:35 -0400)]
More application-track fixes for use with trace executor.

10 years agoVersioning preparation.
Morgan Deters [Mon, 16 Jun 2014 02:08:56 +0000 (22:08 -0400)]
Versioning preparation.

10 years agoSome fixes for tear-down-incremental and "success" output.
Morgan Deters [Mon, 16 Jun 2014 23:59:24 +0000 (19:59 -0400)]
Some fixes for tear-down-incremental and "success" output.

10 years agoDisallow context-dependent copy/assignment.
Morgan Deters [Mon, 16 Jun 2014 20:43:56 +0000 (16:43 -0400)]
Disallow context-dependent copy/assignment.

10 years agoFix compile errors with some versions of GCC.
Morgan Deters [Mon, 16 Jun 2014 02:30:48 +0000 (22:30 -0400)]
Fix compile errors with some versions of GCC.

10 years agoClean up some compiler warnings on 32-bit.
Morgan Deters [Mon, 16 Jun 2014 02:30:39 +0000 (22:30 -0400)]
Clean up some compiler warnings on 32-bit.

10 years agoMinor fixes to get-abc script and configure stuff.
Morgan Deters [Mon, 16 Jun 2014 20:40:56 +0000 (16:40 -0400)]
Minor fixes to get-abc script and configure stuff.

10 years agoget-glpk-cut-log script, and configure code.
Morgan Deters [Mon, 16 Jun 2014 20:05:12 +0000 (16:05 -0400)]
get-glpk-cut-log script, and configure code.

10 years agodos2unix-convert some sources.
Morgan Deters [Mon, 16 Jun 2014 19:19:39 +0000 (15:19 -0400)]
dos2unix-convert some sources.

10 years agoMinor fixes, spelling etc.
Morgan Deters [Wed, 30 Apr 2014 16:51:02 +0000 (12:51 -0400)]
Minor fixes, spelling etc.

10 years agoMore proof support for CASC : include skolemization
ajreynol [Mon, 16 Jun 2014 16:05:36 +0000 (18:05 +0200)]
More proof support for CASC : include skolemization

10 years agominor update to application track config in QF_BV
Morgan Deters [Mon, 16 Jun 2014 03:08:50 +0000 (23:08 -0400)]
minor update to application track config in QF_BV

10 years agoMore doc fixes; fixes some lintian warnings.
Morgan Deters [Thu, 19 Jun 2014 07:37:33 +0000 (03:37 -0400)]
More doc fixes; fixes some lintian warnings.

10 years agoBetter --segv-spin messages.
Morgan Deters [Thu, 19 Jun 2014 07:31:00 +0000 (03:31 -0400)]
Better --segv-spin messages.

10 years agoFix make install-examples.
Morgan Deters [Thu, 19 Jun 2014 07:30:51 +0000 (03:30 -0400)]
Fix make install-examples.

10 years agoProper escaping in option documentation.
Morgan Deters [Thu, 19 Jun 2014 02:02:15 +0000 (22:02 -0400)]
Proper escaping in option documentation.

10 years agoVersion of the run script that works with trace executor; waiting on StarExec infrast...
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.

10 years agoMerge remote-tracking branch 'upstream/master' into sets
Kshitij Bansal [Wed, 18 Jun 2014 20:11:32 +0000 (16:11 -0400)]
Merge remote-tracking branch 'upstream/master' into sets

10 years agoforgot to add the test with fix
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

10 years agobasic fixes for sets translator, separate binaries
Kshitij Bansal [Wed, 18 Jun 2014 19:51:57 +0000 (15:51 -0400)]
basic fixes for sets translator, separate binaries

10 years agoOptions script fix.
Morgan Deters [Wed, 18 Jun 2014 19:41:02 +0000 (15:41 -0400)]
Options script fix.

10 years agoFix for mac readline.
Morgan Deters [Wed, 18 Jun 2014 19:30:32 +0000 (15:30 -0400)]
Fix for mac readline.

10 years agoBetter error for invalid concrete syntax of sorts with too many parens, like (Int...
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.

10 years agoFix GLPK builds: correct access specifier on cut classes.
Morgan Deters [Wed, 18 Jun 2014 04:10:38 +0000 (00:10 -0400)]
Fix GLPK builds: correct access specifier on cut classes.

10 years agoJava bindings fixes.
Morgan Deters [Wed, 18 Jun 2014 01:24:26 +0000 (21:24 -0400)]
Java bindings fixes.

10 years agoMinor Doxygen fixes.
Morgan Deters [Wed, 18 Jun 2014 01:39:05 +0000 (21:39 -0400)]
Minor Doxygen fixes.

10 years agodisable unate lemmas when using incremental mode
Kshitij Bansal [Wed, 18 Jun 2014 03:03:22 +0000 (23:03 -0400)]
disable unate lemmas when using incremental mode

10 years agoFix for pre-C++11 is_sorted().
Morgan Deters [Wed, 18 Jun 2014 00:21:12 +0000 (20:21 -0400)]
Fix for pre-C++11 is_sorted().

10 years agoMore minor code cleanup.
Morgan Deters [Tue, 17 Jun 2014 22:33:28 +0000 (18:33 -0400)]
More minor code cleanup.

10 years agoNo more dependence on libstdc++ or PBDS stuff: remove build stuff that supported it.
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.

10 years agoNew translator features: expand define-funs and combine assertions.
Morgan Deters [Tue, 17 Jun 2014 19:58:04 +0000 (15:58 -0400)]
New translator features: expand define-funs and combine assertions.

10 years agoMerge pull request #33 from mdeters/arith-proposal
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++.

10 years agoCode cleanup.
Morgan Deters [Tue, 17 Jun 2014 21:29:58 +0000 (17:29 -0400)]
Code cleanup.

10 years agoDocumentation clean-ups.
Morgan Deters [Tue, 17 Jun 2014 21:29:49 +0000 (17:29 -0400)]
Documentation clean-ups.

10 years agoAnother fix for the CASC stuff.
Morgan Deters [Tue, 17 Jun 2014 21:35:37 +0000 (17:35 -0400)]
Another fix for the CASC stuff.

10 years agoFinal preparations for arithmetic for building with libc++.
Morgan Deters [Tue, 17 Jun 2014 21:29:12 +0000 (17:29 -0400)]
Final preparations for arithmetic for building with libc++.

10 years agoFix for new CASC features, fixes Java builds.
Morgan Deters [Tue, 17 Jun 2014 20:32:47 +0000 (16:32 -0400)]
Fix for new CASC features, fixes Java builds.

10 years agoSome reversions of recent commits re: portfolio failure.
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.

10 years agoThis commit adds a priority queue implementation. This is to avoid compilation troub...
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++.

10 years agoTest portfolio with --no-wait-to-join.
Morgan Deters [Tue, 17 Jun 2014 13:56:39 +0000 (09:56 -0400)]
Test portfolio with --no-wait-to-join.

10 years agoFor casc : print models of functions rewritten by sort inference.
ajreynol [Tue, 17 Jun 2014 13:25:58 +0000 (15:25 +0200)]
For casc : print models of functions rewritten by sort inference.

10 years agoFix rewriter typo.
Morgan Deters [Tue, 17 Jun 2014 03:44:57 +0000 (23:44 -0400)]
Fix rewriter typo.

10 years agoClean up glpk detection a little, fix a detection bug.
Morgan Deters [Tue, 17 Jun 2014 03:26:49 +0000 (23:26 -0400)]
Clean up glpk detection a little, fix a detection bug.

10 years agofix typo
Morgan Deters [Tue, 17 Jun 2014 02:37:35 +0000 (22:37 -0400)]
fix typo

10 years agoMore application-track fixes for use with trace executor.
Morgan Deters [Tue, 17 Jun 2014 02:35:14 +0000 (22:35 -0400)]
More application-track fixes for use with trace executor.

10 years agoVersioning preparation.
Morgan Deters [Mon, 16 Jun 2014 02:08:56 +0000 (22:08 -0400)]
Versioning preparation.

10 years agoSome fixes for tear-down-incremental and "success" output.
Morgan Deters [Mon, 16 Jun 2014 23:59:24 +0000 (19:59 -0400)]
Some fixes for tear-down-incremental and "success" output.

10 years agoDisallow context-dependent copy/assignment.
Morgan Deters [Mon, 16 Jun 2014 20:43:56 +0000 (16:43 -0400)]
Disallow context-dependent copy/assignment.

10 years agoFix compile errors with some versions of GCC.
Morgan Deters [Mon, 16 Jun 2014 02:30:48 +0000 (22:30 -0400)]
Fix compile errors with some versions of GCC.

10 years agoClean up some compiler warnings on 32-bit.
Morgan Deters [Mon, 16 Jun 2014 02:30:39 +0000 (22:30 -0400)]
Clean up some compiler warnings on 32-bit.

10 years agoMinor fixes to get-abc script and configure stuff.
Morgan Deters [Mon, 16 Jun 2014 20:40:56 +0000 (16:40 -0400)]
Minor fixes to get-abc script and configure stuff.

10 years agoget-glpk-cut-log script, and configure code.
Morgan Deters [Mon, 16 Jun 2014 20:05:12 +0000 (16:05 -0400)]
get-glpk-cut-log script, and configure code.

10 years agodos2unix-convert some sources.
Morgan Deters [Mon, 16 Jun 2014 19:19:39 +0000 (15:19 -0400)]
dos2unix-convert some sources.

10 years agoMinor fixes, spelling etc.
Morgan Deters [Wed, 30 Apr 2014 16:51:02 +0000 (12:51 -0400)]
Minor fixes, spelling etc.

10 years agoMore proof support for CASC : include skolemization
ajreynol [Mon, 16 Jun 2014 16:05:36 +0000 (18:05 +0200)]
More proof support for CASC : include skolemization

10 years agominor update to application track config in QF_BV
Morgan Deters [Mon, 16 Jun 2014 03:08:50 +0000 (23:08 -0400)]
minor update to application track config in QF_BV

10 years agocore solver fix
lianah [Mon, 16 Jun 2014 01:33:51 +0000 (21:33 -0400)]
core solver fix