cvc5.git
10 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
lianah [Thu, 12 Jun 2014 19:18:47 +0000 (15:18 -0400)]
Merge branch 'master' of https://github.com/CVC4/CVC4

10 years agofixing bv inequality solver explanation bug
lianah [Thu, 12 Jun 2014 19:00:27 +0000 (15:00 -0400)]
fixing bv inequality solver explanation bug

10 years agoNew application track script, new heuristics and all --tear-down-incremental. Not...
Morgan Deters [Thu, 12 Jun 2014 17:43:06 +0000 (13:43 -0400)]
New application track script, new heuristics and all --tear-down-incremental.  Not yet tested.

10 years agoadded bvcomp case to bv to bool lifting
lianah [Thu, 12 Jun 2014 13:23:10 +0000 (09:23 -0400)]
added bvcomp case to bv to bool lifting

10 years agomore fix-ups
Morgan Deters [Thu, 12 Jun 2014 02:13:48 +0000 (22:13 -0400)]
more fix-ups

10 years agoadded optionException for trying to use abc in an non-abc build
lianah [Thu, 12 Jun 2014 01:43:33 +0000 (21:43 -0400)]
added optionException for trying to use abc in an non-abc build

10 years agomore smtcomp-submission script work
Morgan Deters [Thu, 12 Jun 2014 00:58:11 +0000 (20:58 -0400)]
more smtcomp-submission script work

10 years agoFlush output stream after result printed in portfolio.
Morgan Deters [Wed, 11 Jun 2014 23:11:56 +0000 (19:11 -0400)]
Flush output stream after result printed in portfolio.

10 years agoFix for competition mode + parallel.
Morgan Deters [Wed, 11 Jun 2014 22:33:52 +0000 (18:33 -0400)]
Fix for competition mode + parallel.

10 years agoFix parallel run script.
Morgan Deters [Wed, 11 Jun 2014 22:33:37 +0000 (18:33 -0400)]
Fix parallel run script.

10 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
lianah [Wed, 11 Jun 2014 22:40:39 +0000 (18:40 -0400)]
Merge branch 'master' of https://github.com/CVC4/CVC4

10 years agoswitched bv equality order
lianah [Wed, 11 Jun 2014 22:40:02 +0000 (18:40 -0400)]
switched bv equality order

10 years agoUpdate SMTCOMP script to handle all quantified logics.
ajreynol [Wed, 11 Jun 2014 22:31:29 +0000 (00:31 +0200)]
Update SMTCOMP script to handle all quantified logics.

10 years agoFix an omission in bv sources.
Morgan Deters [Wed, 11 Jun 2014 20:55:50 +0000 (16:55 -0400)]
Fix an omission in bv sources.

10 years ago--best now implies --with-glpk --with-abc
Morgan Deters [Wed, 11 Jun 2014 18:15:23 +0000 (14:15 -0400)]
--best now implies --with-glpk --with-abc

10 years agoSome clean-up, post bv-merge.
Morgan Deters [Tue, 10 Jun 2014 21:52:26 +0000 (17:52 -0400)]
Some clean-up, post bv-merge.

Add abc to build id and fix static building.

Add abc to --show-config output and Configuration class API.

Add ability to select abc source path.

Fix arch_flags for abc.

10 years agoMerge pull request #31 from kbansal/sets
Kshitij Bansal [Wed, 11 Jun 2014 20:05:16 +0000 (16:05 -0400)]
Merge pull request #31 from kbansal/sets

Sets

10 years agofixed unit tests failures
lianah [Wed, 11 Jun 2014 19:48:53 +0000 (15:48 -0400)]
fixed unit tests failures

10 years agodisable another test, after recent merges taking too long
Kshitij Bansal [Wed, 11 Jun 2014 18:47:13 +0000 (14:47 -0400)]
disable another test, after recent merges taking too long

10 years agodisable failing test
Kshitij Bansal [Wed, 11 Jun 2014 18:31:01 +0000 (14:31 -0400)]
disable failing test

10 years agosets: comment out an assertion too strong
Kshitij Bansal [Wed, 11 Jun 2014 16:35:46 +0000 (12:35 -0400)]
sets: comment out an assertion too strong

10 years agouser/sat context issue in sets
Kshitij Bansal [Wed, 11 Jun 2014 16:33:17 +0000 (12:33 -0400)]
user/sat context issue in sets

10 years agofix in sets rewriter
Kshitij Bansal [Wed, 11 Jun 2014 16:09:39 +0000 (12:09 -0400)]
fix in sets rewriter

10 years agofixing bv ackermanization cache bug
lianah [Wed, 11 Jun 2014 18:07:17 +0000 (14:07 -0400)]
fixing bv ackermanization cache bug

10 years agoAdd new --pb-rewrites options to QF_LIA run script for SMT-COMP.
Morgan Deters [Tue, 10 Jun 2014 21:40:32 +0000 (17:40 -0400)]
Add new --pb-rewrites options to QF_LIA run script for SMT-COMP.

10 years agoSome news about API changes.
Morgan Deters [Mon, 9 Jun 2014 20:37:59 +0000 (16:37 -0400)]
Some news about API changes.

10 years agoMerging Tim's pseudoboolean work from his fmcad14 branch.
Tim King [Tue, 10 Jun 2014 21:32:57 +0000 (17:32 -0400)]
Merging Tim's pseudoboolean work from his fmcad14 branch.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
10 years agoreverting portfolio hack
lianah [Tue, 10 Jun 2014 19:07:31 +0000 (15:07 -0400)]
reverting portfolio hack

10 years agoMerging CAV14 paper bit-vector work.
lianah [Tue, 10 Jun 2014 17:48:45 +0000 (13:48 -0400)]
Merging CAV14 paper bit-vector work.

10 years agoDisallow copy/assignment of SmtEngine.
Morgan Deters [Mon, 9 Jun 2014 14:40:17 +0000 (10:40 -0400)]
Disallow copy/assignment of SmtEngine.

10 years agoTim's options for QF_LIA and QF_LRA---SOI+approx.
Morgan Deters [Mon, 9 Jun 2014 18:56:42 +0000 (14:56 -0400)]
Tim's options for QF_LIA and QF_LRA---SOI+approx.

10 years agoMerge pull request #29 from kbansal/alternatefix
Kshitij Bansal [Mon, 9 Jun 2014 17:32:51 +0000 (13:32 -0400)]
Merge pull request #29 from kbansal/alternatefix

Fix for emptyset in smt2 parser, sets translator to quantified logic, misc

10 years agoAdd missing set of braces, fixes --trace.
Morgan Deters [Mon, 9 Jun 2014 15:05:35 +0000 (11:05 -0400)]
Add missing set of braces, fixes --trace.

Also ensure // commented Debug() lines don't get included in Debug/Trace_tags.

10 years agoparseErrorHelper : factor out whole word matching
Kshitij Bansal [Mon, 9 Jun 2014 01:40:29 +0000 (21:40 -0400)]
parseErrorHelper : factor out whole word matching

catches some corner cases, more readable too

10 years agotest for prvs commit (tokenize emptyset)
Kshitij Bansal [Mon, 9 Jun 2014 01:07:15 +0000 (21:07 -0400)]
test for prvs commit (tokenize emptyset)

9978c259f30b1f4b2c70c04589a309033a6eb1f6

10 years agoPrevious "repeat" fix required extra lookahead (leading to assert-fails). Fixed...
Morgan Deters [Mon, 9 Jun 2014 00:10:08 +0000 (20:10 -0400)]
Previous "repeat" fix required extra lookahead (leading to assert-fails).  Fixed, at the cost of an antlr warning that's safe to ignore for now.

10 years agosmt2 parser: tokenize emptyset only if theory enabled
Kshitij Bansal [Sun, 8 Jun 2014 23:35:39 +0000 (19:35 -0400)]
smt2 parser: tokenize emptyset only if theory enabled

10 years agoBetter error when there are \backslashes in |quoted symbols|.
Morgan Deters [Sun, 8 Jun 2014 21:55:23 +0000 (17:55 -0400)]
Better error when there are \backslashes in |quoted symbols|.

10 years agoAllow 'repeat' as an SMT-LIB user symbol name (UFNIA/vcc-havoc does this).
Morgan Deters [Sun, 8 Jun 2014 21:54:50 +0000 (17:54 -0400)]
Allow 'repeat' as an SMT-LIB user symbol name (UFNIA/vcc-havoc does this).

10 years agosets translate: a different translation using axioms
Kshitij Bansal [Sun, 8 Jun 2014 21:01:54 +0000 (17:01 -0400)]
sets translate: a different translation using axioms

todo: set logic correctly, split the code for two translators

10 years agosets translator: fix for dags
Kshitij Bansal [Fri, 6 Jun 2014 23:40:18 +0000 (19:40 -0400)]
sets translator: fix for dags

10 years agoMerge pull request #28 from kbansal/sets
Kshitij Bansal [Fri, 6 Jun 2014 21:43:57 +0000 (17:43 -0400)]
Merge pull request #28 from kbansal/sets

Sets translator, bug fixes

10 years agoFix submission script (again).
Morgan Deters [Fri, 6 Jun 2014 21:36:16 +0000 (17:36 -0400)]
Fix submission script (again).

10 years agorm warning from helloworld example
Kshitij Bansal [Fri, 6 Jun 2014 20:29:28 +0000 (16:29 -0400)]
rm warning from helloworld example

10 years agoPatch for the subtype theoryof mode to make the equalities over disequal types get...
Tim King [Fri, 6 Jun 2014 15:45:16 +0000 (11:45 -0400)]
Patch for the subtype theoryof mode to make the equalities over disequal types get sent to the theory of the type.
Adding a new test case for bug 569.
Fixes to the normal form of arithmetic so that real terms are before integer terms.

10 years agosets: fix equality propagation
Kshitij Bansal [Fri, 6 Jun 2014 19:32:32 +0000 (15:32 -0400)]
sets: fix equality propagation

10 years ago-{d,t} help => --show-{debug,trace}-tags
Kshitij Bansal [Fri, 6 Jun 2014 01:29:20 +0000 (21:29 -0400)]
-{d,t} help => --show-{debug,trace}-tags

10 years agooption to hide stats which are zero (off by default), also some aliases
Kshitij Bansal [Fri, 6 Jun 2014 00:35:15 +0000 (20:35 -0400)]
option to hide stats which are zero (off by default), also some aliases

10 years agoSets translate, and other short fixes
Kshitij Bansal [Fri, 30 May 2014 00:13:52 +0000 (20:13 -0400)]
Sets translate, and other short fixes

- $ is a simple symbol is smt2.
- ever found yourself counting in kind.h? no longer.
- expose parser "logic is set" state for smt/smt2 (any better way?)
- a more helpful assertion message in smt_engine

10 years agoSMT-COMP version gets built --with-abc.
Morgan Deters [Wed, 4 Jun 2014 22:08:34 +0000 (18:08 -0400)]
SMT-COMP version gets built --with-abc.

10 years agoAdd --default-dag-thresh to translator, build translator with other examples.
Morgan Deters [Thu, 5 Jun 2014 23:08:44 +0000 (19:08 -0400)]
Add --default-dag-thresh to translator, build translator with other examples.

10 years agoWhen printing in SMT, print N-ary bvadd/bvmul/concat/bvand/bvor/bvxor as binary.
Morgan Deters [Thu, 5 Jun 2014 23:09:30 +0000 (19:09 -0400)]
When printing in SMT, print N-ary bvadd/bvmul/concat/bvand/bvor/bvxor as binary.

10 years agoAdd operator support (resolves bug #563).
Morgan Deters [Wed, 4 Jun 2014 22:34:24 +0000 (18:34 -0400)]
Add operator support (resolves bug #563).

10 years agoSmtEngine::checkModel() now checks that model values are of the correct type (related...
Morgan Deters [Wed, 4 Jun 2014 22:10:08 +0000 (18:10 -0400)]
SmtEngine::checkModel() now checks that model values are of the correct type (related to bug #569).

10 years agoUpdate commit # for get-abc script, anticipating Liana's merge.
Morgan Deters [Wed, 4 Jun 2014 21:16:15 +0000 (17:16 -0400)]
Update commit # for get-abc script, anticipating Liana's merge.

10 years agoFix usability issue with tear-down incremental mode.
Morgan Deters [Wed, 4 Jun 2014 19:22:38 +0000 (15:22 -0400)]
Fix usability issue with tear-down incremental mode.

10 years agoSMT strict mode now disallows N-ary use of concat, bvadd, bvmul, bvand, bvor, and...
Morgan Deters [Wed, 4 Jun 2014 19:21:52 +0000 (15:21 -0400)]
SMT strict mode now disallows N-ary use of concat, bvadd, bvmul, bvand, bvor, and bvxor.

10 years agoFixing run-script for smt-comp
Morgan Deters [Wed, 4 Jun 2014 00:14:42 +0000 (20:14 -0400)]
Fixing run-script for smt-comp

10 years agoAnother check when making SMT-COMP submission zipfiles.
Morgan Deters [Tue, 3 Jun 2014 23:59:32 +0000 (19:59 -0400)]
Another check when making SMT-COMP submission zipfiles.

10 years agoFix StarExec description files for new requirements.
Morgan Deters [Tue, 3 Jun 2014 23:01:01 +0000 (19:01 -0400)]
Fix StarExec description files for new requirements.

10 years agoSupport E-matching/QCF for Set operators.
ajreynol [Tue, 3 Jun 2014 12:01:01 +0000 (14:01 +0200)]
Support E-matching/QCF for Set operators.

10 years agoFix for Windows builds (rlimit doesn't exist on Windows).
Morgan Deters [Sun, 1 Jun 2014 17:21:05 +0000 (13:21 -0400)]
Fix for Windows builds (rlimit doesn't exist on Windows).

10 years agoMore make rules
Morgan Deters [Fri, 30 May 2014 23:31:12 +0000 (19:31 -0400)]
More make rules

10 years agoOne final bit (I hope) of make magic
Morgan Deters [Fri, 30 May 2014 22:01:47 +0000 (18:01 -0400)]
One final bit (I hope) of make magic

10 years agoMore make rules
Morgan Deters [Fri, 30 May 2014 21:58:48 +0000 (17:58 -0400)]
More make rules

10 years agoBug fix for string-opt2 (copied from Tianyi's branch).
Morgan Deters [Fri, 30 May 2014 21:07:38 +0000 (17:07 -0400)]
Bug fix for string-opt2 (copied from Tianyi's branch).

10 years agoUpdate submission make rules.
Morgan Deters [Fri, 30 May 2014 19:41:20 +0000 (15:41 -0400)]
Update submission make rules.

10 years agoChange SMT COMP script to use external timeouts.
ajreynol [Fri, 30 May 2014 19:30:23 +0000 (21:30 +0200)]
Change SMT COMP script to use external timeouts.

10 years agoRun script updates: no --stats, also application-track version.
Morgan Deters [Fri, 30 May 2014 19:00:38 +0000 (15:00 -0400)]
Run script updates: no --stats, also application-track version.

10 years agorun script fix
Kshitij Bansal [Fri, 30 May 2014 18:38:05 +0000 (14:38 -0400)]
run script fix

10 years agoImprove --dt-stc-ind for multi-variable datatype properties.
ajreynol [Fri, 30 May 2014 13:48:53 +0000 (15:48 +0200)]
Improve --dt-stc-ind for multi-variable datatype properties.

10 years agoFixes for --inst-max-level
ajreynol [Fri, 30 May 2014 10:17:05 +0000 (12:17 +0200)]
Fixes for --inst-max-level

10 years agoFix personal.mk for some make targets.
Morgan Deters [Fri, 30 May 2014 04:11:44 +0000 (00:11 -0400)]
Fix personal.mk for some make targets.

10 years agoMinor changes to script. Disable cbqi sat.
ajreynol [Wed, 28 May 2014 21:32:59 +0000 (23:32 +0200)]
Minor changes to script.  Disable cbqi sat.

10 years agoAdd option to avoid dumping partial models/proofs.
Andrew Reynolds [Wed, 28 May 2014 07:28:39 +0000 (02:28 -0500)]
Add option to avoid dumping partial models/proofs.

10 years agoSome fixes to GC order in Java.
Morgan Deters [Wed, 28 May 2014 03:35:40 +0000 (23:35 -0400)]
Some fixes to GC order in Java.

10 years agoMerge pull request #27 from kbansal/statistics
Kshitij Bansal [Tue, 27 May 2014 21:51:07 +0000 (17:51 -0400)]
Merge pull request #27 from kbansal/statistics

update stats_black

10 years agoupdate stats_black
Kshitij Bansal [Tue, 27 May 2014 20:16:55 +0000 (16:16 -0400)]
update stats_black

10 years agoNew --tear-down-incremental mode, useful for debugging and performance profiling.
Morgan Deters [Tue, 5 Mar 2013 00:58:15 +0000 (19:58 -0500)]
New --tear-down-incremental mode, useful for debugging and performance profiling.

10 years agofix timespec printing
Kshitij Bansal [Tue, 27 May 2014 18:46:11 +0000 (14:46 -0400)]
fix timespec printing

sorry prvs fix added some unrelated code

10 years agoRevert "timespec printing bug"
Kshitij Bansal [Tue, 27 May 2014 18:43:46 +0000 (14:43 -0400)]
Revert "timespec printing bug"

This reverts commit 9006b759cfa01c6006196e0716c2d67c760556a6.

10 years agotimespec printing bug
Kshitij Bansal [Tue, 27 May 2014 18:41:47 +0000 (14:41 -0400)]
timespec printing bug

10 years agoFix typo in Java destruction code; should fix some recent bug reports of crashes...
Morgan Deters [Tue, 27 May 2014 04:07:17 +0000 (00:07 -0400)]
Fix typo in Java destruction code; should fix some recent bug reports of crashes in Java.

10 years agoImproved type-checking for tuple and record selects.
Morgan Deters [Tue, 27 May 2014 04:06:42 +0000 (00:06 -0400)]
Improved type-checking for tuple and record selects.

10 years agoFix bug 567
Kshitij Bansal [Tue, 27 May 2014 00:22:55 +0000 (20:22 -0400)]
Fix bug 567

This bug got introduced in 96eccb0d6134ccf4ead0134299b2e3750a890083.
The backing Node didn't always exist because of the changes.

10 years agoFixing Tim's subtype/solving bug for arrays
Clark Barrett [Mon, 26 May 2014 19:30:13 +0000 (12:30 -0700)]
Fixing Tim's subtype/solving bug for arrays

10 years agoSeparating an implicit inclusion of smt_engine.h from theory.h.
Tim King [Mon, 26 May 2014 15:44:38 +0000 (11:44 -0400)]
Separating an implicit inclusion of smt_engine.h from theory.h.

10 years agoFixing a soundness bug due to the default implmentation of Theory::ppAssert() not...
Tim King [Mon, 26 May 2014 14:12:19 +0000 (10:12 -0400)]
Fixing a soundness bug due to the default implmentation of Theory::ppAssert() not respecting subtyping.

10 years agoImprove quantifier instantiation: always use original terms when matching (was missin...
Andrew Reynolds [Sun, 25 May 2014 14:18:42 +0000 (09:18 -0500)]
Improve quantifier instantiation: always use original terms when matching (was missing for simple triggers).   Minor updates to scripts.

10 years agoSome cleanup, fix warnings raised by Debian packager.
Morgan Deters [Sun, 25 May 2014 00:16:46 +0000 (20:16 -0400)]
Some cleanup, fix warnings raised by Debian packager.

10 years agoFix bug in E-matching Real/Int terms.
Andrew Reynolds [Fri, 23 May 2014 21:59:48 +0000 (16:59 -0500)]
Fix bug in E-matching Real/Int terms.

10 years agoSafer swig-wrapping for unsigned long long in Java, which will throw an exception...
Morgan Deters [Wed, 21 May 2014 17:55:13 +0000 (13:55 -0400)]
Safer swig-wrapping for unsigned long long in Java, which will throw an exception if the argument is out of bounds for unsigned long long.  Thanks to Steve Siegel for the report.

10 years agoFix compiler warning (missing virtual dtor)
Morgan Deters [Fri, 16 May 2014 03:33:55 +0000 (23:33 -0400)]
Fix compiler warning (missing virtual dtor)

10 years agoMore documentation fixes. Apologies for multiple commits.
Tim King [Mon, 19 May 2014 19:14:54 +0000 (15:14 -0400)]
More documentation fixes. Apologies for multiple commits.

10 years agoFixing documentation for glpk configuration.
Tim King [Mon, 19 May 2014 19:12:54 +0000 (15:12 -0400)]
Fixing documentation for glpk configuration.

10 years agominor fix for string equality engine assertion.
Tianyi Liang [Mon, 19 May 2014 02:06:29 +0000 (21:06 -0500)]
minor fix for string equality engine assertion.

10 years agoMerge pull request #26 from kbansal/sets
Kshitij Bansal [Sat, 17 May 2014 06:43:55 +0000 (02:43 -0400)]
Merge pull request #26 from kbansal/sets

Sets

10 years agolfsc_checker: fix some warnings reported by _both_ gcc and clang
Kshitij Bansal [Fri, 16 May 2014 22:38:22 +0000 (18:38 -0400)]
lfsc_checker: fix some warnings reported by _both_ gcc and clang

10 years agosets: fix a bug in model building, another in handling set of sets
Kshitij Bansal [Fri, 16 May 2014 22:18:35 +0000 (18:18 -0400)]
sets: fix a bug in model building, another in handling set of sets

10 years agominor improvements (fixes) to did-you-mean suggestions
Kshitij Bansal [Fri, 16 May 2014 17:41:31 +0000 (13:41 -0400)]
minor improvements (fixes) to did-you-mean suggestions