cvc5.git
10 years agoMerge pull request #34 from mdeters/datatypes-kinds
Andrew Reynolds [Wed, 25 Jun 2014 21:49:24 +0000 (23:49 +0200)]
Merge pull request #34 from mdeters/datatypes-kinds

Datatypes kinds documentation

10 years agoMerge pull request #37 from mdeters/quants-kinds
Andrew Reynolds [Wed, 25 Jun 2014 21:48:18 +0000 (23:48 +0200)]
Merge pull request #37 from mdeters/quants-kinds

Quantifiers kinds documentation

10 years agoMerge pull request #38 from mdeters/uf-kinds
Andrew Reynolds [Wed, 25 Jun 2014 21:47:30 +0000 (23:47 +0200)]
Merge pull request #38 from mdeters/uf-kinds

UF kinds documentation

10 years agoMerge pull request #43 from mdeters/threadstack
Kshitij Bansal [Wed, 25 Jun 2014 16:39:49 +0000 (12:39 -0400)]
Merge pull request #43 from mdeters/threadstack

stack-size portfolio fix.  boost 1.50 now required

"The intended behavior is this. If Boost threading library is available and portfolio is requested, we do a try-link during configure that sees if we can set a thread attribute. If that compiles and links, we set a #define in cvc4autoconfig.h. There's a new option --thread-stack=N, with N given in megabytes. 0 is default for the platform (which can be based on ulimit I guess as I mentioned in an email). If --thread-stack=N is given to sequential CVC4, it's an error. If it's given to pcvc4 and N > 0 and there isn't support in that Boost version for it, it's an error."

10 years agoMerge branch 'master' of github.com:CVC3/CVC4
Tim King [Wed, 25 Jun 2014 14:46:43 +0000 (10:46 -0400)]
Merge branch 'master' of github.com:CVC3/CVC4

10 years agoFixing the previous bugfix.
Tim King [Wed, 25 Jun 2014 14:46:40 +0000 (10:46 -0400)]
Fixing the previous bugfix.

10 years agoStack-size portfolio fix. If using Boost 1.50, --thread-stack=MB is now supported.
Morgan Deters [Tue, 24 Jun 2014 22:44:15 +0000 (18:44 -0400)]
Stack-size portfolio fix.  If using Boost 1.50, --thread-stack=MB is now supported.

10 years agoFix some #line annotations.
Morgan Deters [Wed, 25 Jun 2014 04:15:05 +0000 (00:15 -0400)]
Fix some #line annotations.

10 years agoDon't allow libabc to load extensions at runtime.
Morgan Deters [Wed, 25 Jun 2014 14:07:44 +0000 (10:07 -0400)]
Don't allow libabc to load extensions at runtime.

10 years agoAlternative lazier heuristic for assertion rewriting.
Tim King [Tue, 24 Jun 2014 23:19:58 +0000 (19:19 -0400)]
Alternative lazier heuristic for assertion rewriting.

10 years agoFixing a soundness bug in arithmetic and a roubustness problem in rings.
Tim King [Tue, 24 Jun 2014 20:46:09 +0000 (16:46 -0400)]
Fixing a soundness bug in arithmetic and a roubustness problem in rings.

10 years agoMerge pull request #41 from mdeters/tianyi-merge
Tianyi Liang [Tue, 24 Jun 2014 06:35:45 +0000 (14:35 +0800)]
Merge pull request #41 from mdeters/tianyi-merge

Merge from Tianyi

10 years agoSquashed commit of the following:
Morgan Deters [Tue, 24 Jun 2014 05:40:17 +0000 (01:40 -0400)]
Squashed commit of the following:

 * Fix a bug in intersection
 * merging...
 * add delayed length lemmas
 * PreRegisterTerm is changed.
 * Bug fix for string-opt2
 * PreRegisterTerm is changed.
 * add delayed length lemmas
 * Bug fix for string-opt2
 * PreRegisterTerm is changed.
 * Bug fix for string-opt2
 * PreRegisterTerm is changed.
 * Bug fix for string-opt2
 * PreRegisterTerm is changed.

10 years agoFix header check for glpk.h.
Morgan Deters [Mon, 23 Jun 2014 21:38:20 +0000 (17:38 -0400)]
Fix header check for glpk.h.

10 years agoFatal error if --unconstrained-simp and --produce-models used together (before it...
Morgan Deters [Fri, 20 Jun 2014 19:13:23 +0000 (15:13 -0400)]
Fatal error if --unconstrained-simp and --produce-models used together (before it would just override the user and turn off models).

10 years agoMake language explicit in casc scripts
ajreynol [Mon, 23 Jun 2014 19:53:14 +0000 (21:53 +0200)]
Make language explicit in casc scripts

10 years agoOutput language "cvc3" (as opposed to "cvc" or "cvc4") produces output for CVC3:
Morgan Deters [Sun, 22 Jun 2014 04:30:47 +0000 (00:30 -0400)]
Output language "cvc3" (as opposed to "cvc" or "cvc4") produces output for CVC3:

1. no decimals used for rational literals
2. queries/check-sats wrapped with PUSH/POP

10 years agoMinor cleanup stuff.
Morgan Deters [Sun, 22 Jun 2014 04:32:33 +0000 (00:32 -0400)]
Minor cleanup stuff.

10 years agoBetter documentation pages.
Morgan Deters [Sun, 22 Jun 2014 08:37:26 +0000 (04:37 -0400)]
Better documentation pages.

10 years agoRe-enable UNTERMINATED_QUOTED_SYMBOL rules.
Morgan Deters [Sun, 22 Jun 2014 06:56:37 +0000 (02:56 -0400)]
Re-enable UNTERMINATED_QUOTED_SYMBOL rules.

10 years agoMerge tag 'smtcomp2014-application'
Morgan Deters [Sun, 22 Jun 2014 07:15:36 +0000 (03:15 -0400)]
Merge tag 'smtcomp2014-application'

Conflicts:
contrib/run-script-smtcomp2014-application
src/main/driver_unified.cpp

10 years agoQuitCommand needs "success" output for trace executor. :-(
Morgan Deters [Sun, 22 Jun 2014 07:01:23 +0000 (03:01 -0400)]
QuitCommand needs "success" output for trace executor. :-(

10 years agoFinal fixes for smtcomp2014-application.
Morgan Deters [Sun, 22 Jun 2014 06:51:31 +0000 (02:51 -0400)]
Final fixes for smtcomp2014-application.

10 years agoMerge pull request #39 from mdeters/bv-warnings
lianah [Sun, 22 Jun 2014 05:34:26 +0000 (01:34 -0400)]
Merge pull request #39 from mdeters/bv-warnings

Fix compiler warnings in BV-related code (unused vars mostly).

10 years agoMerge pull request #35 from mdeters/bv-kinds
lianah [Sun, 22 Jun 2014 05:33:40 +0000 (01:33 -0400)]
Merge pull request #35 from mdeters/bv-kinds

Bit-vector kinds documentation

10 years agoAnother updated submission strategy.
Morgan Deters [Sun, 22 Jun 2014 05:23:19 +0000 (01:23 -0400)]
Another updated submission strategy.

10 years agoAnother updated submission strategy.
Morgan Deters [Sun, 22 Jun 2014 05:23:19 +0000 (01:23 -0400)]
Another updated submission strategy.

10 years agoRun in application track with --check-models.
Morgan Deters [Sun, 22 Jun 2014 02:09:17 +0000 (22:09 -0400)]
Run in application track with --check-models.

10 years agoFix compiler warnings (mostly unused variables).
Morgan Deters [Sun, 22 Jun 2014 01:12:36 +0000 (21:12 -0400)]
Fix compiler warnings (mostly unused variables).

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

10 years agoRun in application track with --check-models.
Morgan Deters [Sun, 22 Jun 2014 02:09:17 +0000 (22:09 -0400)]
Run in application track with --check-models.

10 years agoFix compiler warnings in BV-related code (unused vars mostly).
Morgan Deters [Sun, 22 Jun 2014 01:13:12 +0000 (21:13 -0400)]
Fix compiler warnings in BV-related code (unused vars mostly).

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 agoBit-vector kinds documentation
Morgan Deters [Sat, 21 Jun 2014 00:00:27 +0000 (20:00 -0400)]
Bit-vector kinds documentation

10 years agoDatatypes kinds documentation
Morgan Deters [Sat, 21 Jun 2014 00:00:36 +0000 (20:00 -0400)]
Datatypes kinds documentation

10 years agoQuantifiers kinds documentation
Morgan Deters [Fri, 20 Jun 2014 23:59:54 +0000 (19:59 -0400)]
Quantifiers kinds documentation

10 years agoUF kinds documentation
Morgan Deters [Fri, 20 Jun 2014 23:59:42 +0000 (19:59 -0400)]
UF kinds documentation

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 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.