cvc5.git
10 years agorm warning
Kshitij Bansal [Thu, 10 Jul 2014 20:05:25 +0000 (16:05 -0400)]
rm warning

10 years agomembership cvc token changed to `IS_IN' to avoid conflict with IN used for let
Kshitij Bansal [Thu, 10 Jul 2014 17:11:36 +0000 (13:11 -0400)]
membership cvc token changed to `IS_IN' to avoid conflict with IN used for let

10 years agofriendlyparser: go back upto 2 words looking for match
Kshitij Bansal [Thu, 10 Jul 2014 17:06:30 +0000 (13:06 -0400)]
friendlyparser: go back upto 2 words looking for match

10 years agoreorganize friendlyparser, behavior unchanged
Kshitij Bansal [Thu, 10 Jul 2014 17:05:45 +0000 (13:05 -0400)]
reorganize friendlyparser, behavior unchanged

10 years agosets cvc parser
Kshitij Bansal [Wed, 9 Jul 2014 19:58:40 +0000 (15:58 -0400)]
sets cvc parser

10 years agosets cvc printer
Kshitij Bansal [Wed, 9 Jul 2014 18:33:31 +0000 (14:33 -0400)]
sets cvc printer

10 years agochange lemma generation behavior
Kshitij Bansal [Thu, 3 Jul 2014 22:37:51 +0000 (18:37 -0400)]
change lemma generation behavior

don't store lemmas in a pending queue, instead generate them right away

doing with pending queue is tricky, needs rethinking to do it properly

10 years agoFix cut-release script for new configure rules.
Morgan Deters [Wed, 2 Jul 2014 19:22:22 +0000 (15:22 -0400)]
Fix cut-release script for new configure rules.

10 years agoMinor.
Morgan Deters [Wed, 2 Jul 2014 18:45:28 +0000 (14:45 -0400)]
Minor.

10 years agoUpdate portfolio_util.cpp
Kshitij Bansal [Tue, 1 Jul 2014 23:09:07 +0000 (19:09 -0400)]
Update portfolio_util.cpp

10 years agoFix path in CASC J7 scripts, and distribute them with tarball.
Morgan Deters [Tue, 1 Jul 2014 19:10:37 +0000 (15:10 -0400)]
Fix path in CASC J7 scripts, and distribute them with tarball.

10 years agoUpdate copyrights.
Morgan Deters [Tue, 1 Jul 2014 18:47:24 +0000 (14:47 -0400)]
Update copyrights.

10 years agoreword NEWS
Morgan Deters [Mon, 30 Jun 2014 20:25:27 +0000 (16:25 -0400)]
reword NEWS

10 years agoMerge pull request #44 from mdeters/prio-queue-updates
Morgan Deters [Tue, 1 Jul 2014 18:36:38 +0000 (14:36 -0400)]
Merge pull request #44 from mdeters/prio-queue-updates

BinaryHeap unit test and some usability/build fixes for the data structu...

10 years agoMerge pull request #45 from mdeters/turn-off-strings-exp
Morgan Deters [Tue, 1 Jul 2014 03:14:45 +0000 (23:14 -0400)]
Merge pull request #45 from mdeters/turn-off-strings-exp

Turn strings-exp off by default (for the release)

10 years agoUpdate NEWS
Kshitij Bansal [Mon, 30 Jun 2014 19:47:59 +0000 (15:47 -0400)]
Update NEWS

10 years agoMerge pull request #47 from kbansal/sets
Kshitij Bansal [Mon, 30 Jun 2014 17:28:09 +0000 (13:28 -0400)]
Merge pull request #47 from kbansal/sets

Sets theory operators in SMTLIB2 and kinds to use from API have changed. They now are:

SMTLIB: emptyset, singleton*, insert*, union, intersection, setminus, member*, subset*
API: EMPTYSET, SINGLETON*, INSERT*, UNION, INTERSECTION, SETMINUS, MEMBER, SUBSET

(those marked with [*] have changed or been added, others are as earlier)

In the set-logic string use FS to enable sets.

A not-so-well-tested perl command for translating old benchmarks:
  perl -pi -e 's/\(set-logic (.+)_SETS\)/\(set-logic \1FS\)/; s/\(in\b/\(member/g; s/\(setenum\b/\(singleton/g; s/\(subseteq\b/\(subset/g; '

10 years agoUse FS as the set-logic string for theory of sets
Kshitij Bansal [Mon, 30 Jun 2014 14:53:52 +0000 (10:53 -0400)]
Use FS as the set-logic string for theory of sets

10 years agosets: "insert" operator
Kshitij Bansal [Sun, 29 Jun 2014 22:44:40 +0000 (18:44 -0400)]
sets: "insert" operator

new™! support for (insert (X (Set X)) (Set X) :right-associative)
from the finte sets theory prosoal.

e.g., (insert 1 2 3 4 (singleton 5))

10 years agoAutomatically make SMT options from command-line option names, warn when not possible.
Morgan Deters [Fri, 4 Apr 2014 18:50:02 +0000 (14:50 -0400)]
Automatically make SMT options from command-line option names, warn when not possible.

10 years agoFix bug in datatypes options specification
Morgan Deters [Sat, 28 Jun 2014 20:04:27 +0000 (16:04 -0400)]
Fix bug in datatypes options specification

10 years agoAnother fix for 32-bit (amends commit b825605).
Morgan Deters [Fri, 27 Jun 2014 17:02:31 +0000 (13:02 -0400)]
Another fix for 32-bit (amends commit b825605).

10 years agoFix for bug543
Clark Barrett [Fri, 27 Jun 2014 17:29:28 +0000 (10:29 -0700)]
Fix for bug543

10 years agoUpdated run script for QF_ABV
Clark Barrett [Sun, 15 Jun 2014 00:25:03 +0000 (17:25 -0700)]
Updated run script for QF_ABV

10 years agoMerge pull request #46 from mdeters/bug573
Kshitij Bansal [Thu, 26 Jun 2014 19:46:26 +0000 (15:46 -0400)]
Merge pull request #46 from mdeters/bug573

Potential fix for bug 573.

10 years agoFix for 32-bit (esp. win32 failing build).
Morgan Deters [Thu, 26 Jun 2014 16:14:06 +0000 (12:14 -0400)]
Fix for 32-bit (esp. win32 failing build).

10 years agoMerge tag 'smtcomp2014-resubmission'
Morgan Deters [Thu, 26 Jun 2014 05:55:38 +0000 (01:55 -0400)]
Merge tag 'smtcomp2014-resubmission'

Conflicts:
src/main/portfolio.cpp

10 years agoPotential fix for bug 573.
Morgan Deters [Thu, 26 Jun 2014 04:47:55 +0000 (00:47 -0400)]
Potential fix for bug 573.

10 years agoIgnore error result when an error is squelched via command verbosity.
Morgan Deters [Thu, 26 Jun 2014 04:41:48 +0000 (00:41 -0400)]
Ignore error result when an error is squelched via command verbosity.

10 years agoRemove leftover debugging output.
Morgan Deters [Thu, 26 Jun 2014 04:28:18 +0000 (00:28 -0400)]
Remove leftover debugging output.

10 years agoMinor language bindings fixes.
Morgan Deters [Thu, 26 Jun 2014 04:27:42 +0000 (00:27 -0400)]
Minor language bindings fixes.

10 years agoAdd missing function definition.
Morgan Deters [Thu, 26 Jun 2014 04:27:30 +0000 (00:27 -0400)]
Add missing function definition.

10 years agosets api example
Kshitij Bansal [Wed, 25 Jun 2014 23:10:55 +0000 (19:10 -0400)]
sets api example

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 agoTurn strings-exp off by default (for the release)
Morgan Deters [Wed, 25 Jun 2014 20:35:27 +0000 (16:35 -0400)]
Turn strings-exp off by default (for the release)

10 years agofix sets eager lemmas
Kshitij Bansal [Tue, 24 Jun 2014 16:15:42 +0000 (12:15 -0400)]
fix sets eager lemmas

10 years agocosmetic
Kshitij Bansal [Mon, 23 Jun 2014 15:49:22 +0000 (11:49 -0400)]
cosmetic

10 years agomv default care graph function inside the theory implementation
Kshitij Bansal [Mon, 23 Jun 2014 15:41:23 +0000 (11:41 -0400)]
mv default care graph function inside the theory implementation

10 years agomake emptyset construction with no arguments private
Kshitij Bansal [Sun, 22 Jun 2014 22:22:16 +0000 (18:22 -0400)]
make emptyset construction with no arguments private

10 years agorename subseteq to subset in smtlib, all kinds and smt operator names are now consistent
Kshitij Bansal [Tue, 24 Jun 2014 18:29:12 +0000 (14:29 -0400)]
rename subseteq to subset in smtlib, all kinds and smt operator names are now consistent

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 agoBinaryHeap unit test and some usability/build fixes for the data structure itself.
Morgan Deters [Tue, 24 Jun 2014 05:30:23 +0000 (01:30 -0400)]
BinaryHeap unit test and some usability/build fixes for the data structure itself.

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 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 agostack-size portfolio fix. boost 1.50 now required
Morgan Deters [Tue, 24 Jun 2014 22:44:15 +0000 (18:44 -0400)]
stack-size portfolio fix.  boost 1.50 now required

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 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 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 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 agoRenaming of SMT2 operator names, kinds for set theory
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".

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 agoSets kinds documentation
Morgan Deters [Fri, 20 Jun 2014 23:59:48 +0000 (19:59 -0400)]
Sets kinds documentation

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.