cvc5.git
10 years agoOne small thing forgotten in core commit.
Morgan Deters [Fri, 22 Aug 2014 22:04:48 +0000 (18:04 -0400)]
One small thing forgotten in core commit.

10 years agoJava-side interface improvements for unsat cores.
Morgan Deters [Wed, 20 Aug 2014 22:16:01 +0000 (18:16 -0400)]
Java-side interface improvements for unsat cores.

10 years agoUnsat core infrastruture and API (SMT-LIB compliance to come).
Morgan Deters [Fri, 22 Aug 2014 20:59:28 +0000 (16:59 -0400)]
Unsat core infrastruture and API (SMT-LIB compliance to come).

10 years agoMerge branch '1.4.x'
Morgan Deters [Fri, 22 Aug 2014 21:02:31 +0000 (17:02 -0400)]
Merge branch '1.4.x'

10 years agoFix incorrectly-labeled test.
Morgan Deters [Fri, 22 Aug 2014 20:34:48 +0000 (16:34 -0400)]
Fix incorrectly-labeled test.

10 years agoMerge branch '1.4.x'
Morgan Deters [Fri, 22 Aug 2014 19:40:47 +0000 (15:40 -0400)]
Merge branch '1.4.x'

10 years agoFix operator-printing issue in SMT2.
Morgan Deters [Fri, 22 Aug 2014 19:40:14 +0000 (15:40 -0400)]
Fix operator-printing issue in SMT2.

10 years agoFix SMT1 parser :extrasorts/:extrapreds.
Morgan Deters [Fri, 22 Aug 2014 19:02:43 +0000 (15:02 -0400)]
Fix SMT1 parser :extrasorts/:extrapreds.

10 years agoAvoid doing work in quantifiers engine when no quantifiers are asserted.
ajreynol [Thu, 21 Aug 2014 16:28:36 +0000 (18:28 +0200)]
Avoid doing work in quantifiers engine when no quantifiers are asserted.

10 years agoFix --inst-max-level for strategies that use arbitrary representative terms.
ajreynol [Wed, 20 Aug 2014 22:26:55 +0000 (00:26 +0200)]
Fix --inst-max-level for strategies that use arbitrary representative terms.

10 years agoUpdate bv proof signature and example, after discussions with Liana.
ajreynol [Wed, 20 Aug 2014 20:43:22 +0000 (22:43 +0200)]
Update bv proof signature and example, after discussions with Liana.

10 years agoAdd option for inductive strengthening based on well-founded induction for integers...
ajreynol [Wed, 20 Aug 2014 16:38:04 +0000 (18:38 +0200)]
Add option for inductive strengthening based on well-founded induction for integers (default schema).

10 years agoMerge branch '1.4.x'
Morgan Deters [Tue, 19 Aug 2014 20:39:14 +0000 (16:39 -0400)]
Merge branch '1.4.x'

10 years agoProduce error for bad indexed function names in SMT-LIB, remove antlr warning.
Morgan Deters [Tue, 19 Aug 2014 20:39:06 +0000 (16:39 -0400)]
Produce error for bad indexed function names in SMT-LIB, remove antlr warning.

10 years agoMaking getEqualityStatus more powerful for bit-vector theory.
lianah [Fri, 15 Aug 2014 23:46:06 +0000 (19:46 -0400)]
Making getEqualityStatus more powerful for bit-vector theory.

10 years agoMerge branch '1.4.x'
Morgan Deters [Mon, 18 Aug 2014 19:53:53 +0000 (15:53 -0400)]
Merge branch '1.4.x'

Conflicts:
test/regress/regress0/Makefile.am

10 years agoRevert a8e0ce67 and add test case (resolves bug #578).
Morgan Deters [Mon, 18 Aug 2014 19:41:46 +0000 (15:41 -0400)]
Revert a8e0ce67 and add test case (resolves bug #578).

This reverts commit a8e0ce673ba00533a663804cf74500e4d9a3a5cb.

10 years agoAdd support for quantifier-specific instantiation levels. Add option for setting...
ajreynol [Mon, 18 Aug 2014 10:47:07 +0000 (12:47 +0200)]
Add support for quantifier-specific instantiation levels.  Add option for setting inst-level 0 only for input terms.

10 years agoUpdate smt_engine.cpp
Kshitij Bansal [Fri, 15 Aug 2014 23:00:45 +0000 (19:00 -0400)]
Update smt_engine.cpp

Code changed but comment didn't, might as well get rid of it.

10 years agoTo avoid confusion, permit --enable-staticbinary as an alias for --enable-static...
Morgan Deters [Wed, 13 Aug 2014 01:29:56 +0000 (21:29 -0400)]
To avoid confusion, permit --enable-staticbinary as an alias for --enable-static-binary.

10 years agoFix a build issue for some configurations, thanks Tianyi.
Morgan Deters [Fri, 8 Aug 2014 16:13:57 +0000 (12:13 -0400)]
Fix a build issue for some configurations, thanks Tianyi.

10 years agoAdd draft of BV proof signature (incomplete) and example proof.
ajreynol [Fri, 8 Aug 2014 12:13:49 +0000 (14:13 +0200)]
Add draft of BV proof signature (incomplete) and example proof.

10 years agoAnother build fix.
Morgan Deters [Thu, 7 Aug 2014 16:53:14 +0000 (12:53 -0400)]
Another build fix.

10 years agoFix win32 build.
Morgan Deters [Thu, 7 Aug 2014 15:47:20 +0000 (11:47 -0400)]
Fix win32 build.

10 years agoFix double-linking issue (I think) by simplifying builds/ structure.
Morgan Deters [Wed, 6 Aug 2014 21:52:30 +0000 (17:52 -0400)]
Fix double-linking issue (I think) by simplifying builds/ structure.

10 years agoFirst crack at fixing double-linking issues in build system.
Morgan Deters [Wed, 6 Aug 2014 00:47:36 +0000 (20:47 -0400)]
First crack at fixing double-linking issues in build system.

10 years agoFix for manpages.
Morgan Deters [Tue, 5 Aug 2014 19:59:51 +0000 (15:59 -0400)]
Fix for manpages.

10 years agofixed bug575 for bv models
lianah [Tue, 5 Aug 2014 18:36:00 +0000 (14:36 -0400)]
fixed bug575 for bv models

10 years agofixed bug575 for bv models
lianah [Tue, 5 Aug 2014 18:36:00 +0000 (14:36 -0400)]
fixed bug575 for bv models

10 years agoMinor fix : do not drop instantiation patterns when merging quantifiers.
ajreynol [Tue, 5 Aug 2014 15:23:41 +0000 (17:23 +0200)]
Minor fix : do not drop instantiation patterns when merging quantifiers.

10 years agoSome fixes to symmetry breaker (resolves bug 576).
Morgan Deters [Fri, 1 Aug 2014 19:08:06 +0000 (15:08 -0400)]
Some fixes to symmetry breaker (resolves bug 576).

10 years agoSome fixes to symmetry breaker (resolves bug 576).
Morgan Deters [Fri, 1 Aug 2014 19:08:06 +0000 (15:08 -0400)]
Some fixes to symmetry breaker (resolves bug 576).

10 years agoBetter support for resource-limiting when there aren't any actual conflicts.
Morgan Deters [Fri, 1 Aug 2014 18:31:16 +0000 (14:31 -0400)]
Better support for resource-limiting when there aren't any actual conflicts.

10 years agoMinor cleanup from previous commit. Better organization for how quantifiers modules...
ajreynol [Fri, 1 Aug 2014 13:16:17 +0000 (15:16 +0200)]
Minor cleanup from previous commit.  Better organization for how quantifiers modules check (introduce QuantifiersEngine::QEffort).

10 years agoNew module for generating candidate equality conjectures used in inductive proofs...
ajreynol [Thu, 31 Jul 2014 10:49:28 +0000 (12:49 +0200)]
New module for generating candidate equality conjectures used in inductive proofs.  Filtering currently includes: LHS generalizes a term from an active conjecture, terms must be canonical, conjecture must be confirmed by a ground witness, and cannot be falsified by a ground witness.  Refactoring of term database.  QcfEngine now uses central data structure for term indexing.  Add two options for quantifier instantiation : trigger selection mode --trigger-sel=mode, and --inst-no-entail which blocks all quantifier instantiations that are currently entailed (using an incomplete check).

10 years agoMinor bug fix for exhaustive instantiation in model_engine.
ajreynol [Fri, 25 Jul 2014 22:50:21 +0000 (00:50 +0200)]
Minor bug fix for exhaustive instantiation in model_engine.

10 years agobug fix for pierre 0717
Tianyi Liang [Fri, 25 Jul 2014 20:43:16 +0000 (15:43 -0500)]
bug fix for pierre 0717

10 years agofix for regexp union rewriting
Tianyi Liang [Fri, 25 Jul 2014 19:50:10 +0000 (14:50 -0500)]
fix for regexp union rewriting

10 years agopatch for regular expression intersection caching
Tianyi Liang [Fri, 25 Jul 2014 18:43:44 +0000 (13:43 -0500)]
patch for regular expression intersection caching

10 years agomerging...
Tianyi Liang [Mon, 9 Jun 2014 20:36:36 +0000 (15:36 -0500)]
merging...

10 years agoadd delayed length lemmas
Tianyi Liang [Mon, 9 Jun 2014 12:52:23 +0000 (07:52 -0500)]
add delayed length lemmas

10 years agoinitialization in model_engine
Kshitij Bansal [Mon, 21 Jul 2014 22:50:36 +0000 (18:50 -0400)]
initialization in model_engine

10 years agorun_regression using valgrind by setting VALGRIND=1
Kshitij Bansal [Mon, 21 Jul 2014 22:49:53 +0000 (18:49 -0400)]
run_regression using valgrind by setting VALGRIND=1

10 years agoMinor fix for explanations for co-datatypes. Bug fix for explanations in FMF for...
ajreynol [Sat, 19 Jul 2014 09:58:35 +0000 (11:58 +0200)]
Minor fix for explanations for co-datatypes.  Bug fix for explanations in FMF for quantifiers over arrays.

10 years agoVersioning for master.
Morgan Deters [Sun, 13 Jul 2014 17:31:57 +0000 (13:31 -0400)]
Versioning for master.

10 years agoNew versioning for development version.
Morgan Deters [Sun, 13 Jul 2014 17:30:25 +0000 (13:30 -0400)]
New versioning for development version.

10 years agoCutting release 1.4.
Morgan Deters [Sun, 13 Jul 2014 17:24:08 +0000 (13:24 -0400)]
Cutting release 1.4.

10 years agoStatus for new bug testcase.
Morgan Deters [Sun, 13 Jul 2014 01:09:35 +0000 (21:09 -0400)]
Status for new bug testcase.

10 years agoFix a bug in Boolean terms and arrays. Thanks to Jean-Christophe Filliatre for the...
Morgan Deters [Wed, 2 Jul 2014 20:22:13 +0000 (16:22 -0400)]
Fix a bug in Boolean terms and arrays.  Thanks to Jean-Christophe Filliatre for the report.

10 years agoSpelling.
Morgan Deters [Wed, 9 Jul 2014 16:22:58 +0000 (12:22 -0400)]
Spelling.

10 years agofix for windows build
Kshitij Bansal [Fri, 11 Jul 2014 15:54:48 +0000 (11:54 -0400)]
fix for windows build

10 years agoMerge pull request #48 from kbansal/segfaultfix
Kshitij Bansal [Fri, 11 Jul 2014 00:11:04 +0000 (20:11 -0400)]
Merge pull request #48 from kbansal/segfaultfix

Segfaultfix

10 years agoMerge pull request #49 from kbansal/cvcparser
Kshitij Bansal [Fri, 11 Jul 2014 00:10:42 +0000 (20:10 -0400)]
Merge pull request #49 from kbansal/cvcparser

Cvcparser

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 agoMerge remote-tracking branch 'origin/master' into segfaultfix
Kshitij Bansal [Thu, 10 Jul 2014 20:20:42 +0000 (16:20 -0400)]
Merge remote-tracking branch 'origin/master' into segfaultfix

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 agoinitialize variables
Kshitij Bansal [Fri, 4 Jul 2014 19:34:40 +0000 (15:34 -0400)]
initialize variables

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 agochat about thread creation
Kshitij Bansal [Tue, 1 Jul 2014 18:27:50 +0000 (14:27 -0400)]
chat about thread creation

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.