cvc5.git
10 years agoadded rewriting to bv-pow2 pass
lianah [Sun, 15 Jun 2014 03:18:40 +0000 (23:18 -0400)]
added rewriting to bv-pow2 pass

10 years agoEvil bitvector preprocessing pass for simplifying powers of two.
lianah [Sun, 15 Jun 2014 03:06:50 +0000 (23:06 -0400)]
Evil bitvector preprocessing pass for simplifying powers of two.

10 years agobv static learning and rewrites for power of 2 terms
lianah [Sun, 15 Jun 2014 00:44:00 +0000 (20:44 -0400)]
bv static learning and rewrites for power of 2 terms

10 years agomore bv rewrites
lianah [Sat, 14 Jun 2014 20:13:46 +0000 (16:13 -0400)]
more bv rewrites

10 years agofix to inequality rewrite
lianah [Sat, 14 Jun 2014 18:18:45 +0000 (14:18 -0400)]
fix to inequality rewrite

10 years agofixed merge
lianah [Sat, 14 Jun 2014 17:53:33 +0000 (13:53 -0400)]
fixed merge

10 years agoadded bv inequality rewrite
lianah [Sat, 14 Jun 2014 17:48:55 +0000 (13:48 -0400)]
added bv inequality rewrite

10 years agoadded bv inequality lemmas
Liana Hadarean [Sat, 14 Jun 2014 15:01:59 +0000 (11:01 -0400)]
added bv inequality lemmas

10 years agoadded bv inequality lemmas
Liana Hadarean [Sat, 14 Jun 2014 15:01:59 +0000 (11:01 -0400)]
added bv inequality lemmas

10 years agoFix for fmf with large finite cardinalities.
ajreynol [Sat, 14 Jun 2014 07:40:49 +0000 (09:40 +0200)]
Fix for fmf with large finite cardinalities.

10 years agofixed BVMinisat bug due to not clearing seen properly
lianah [Fri, 13 Jun 2014 23:53:03 +0000 (19:53 -0400)]
fixed BVMinisat bug due to not clearing seen properly

10 years agoDoubly-ensure incremental is off in main track. Also import bv-portfolio strategy.
Morgan Deters [Fri, 13 Jun 2014 21:41:42 +0000 (17:41 -0400)]
Doubly-ensure incremental is off in main track.  Also import bv-portfolio strategy.

10 years agoFix handling of ALIA.
ajreynol [Fri, 13 Jun 2014 15:18:05 +0000 (17:18 +0200)]
Fix handling of ALIA.

10 years agoupdate application track script too
Morgan Deters [Fri, 13 Jun 2014 15:00:24 +0000 (11:00 -0400)]
update application track script too

10 years agoUpdate for QF_AUFLIA strategy
Clark Barrett [Fri, 13 Jun 2014 07:38:33 +0000 (00:38 -0700)]
Update for QF_AUFLIA strategy

10 years agoAllow parallel failures when building competition version (they are spurious).
Morgan Deters [Fri, 13 Jun 2014 05:31:18 +0000 (01:31 -0400)]
Allow parallel failures when building competition version (they are spurious).

10 years agoAdjust incremental run script for QF_AX too.
Morgan Deters [Fri, 13 Jun 2014 05:26:03 +0000 (01:26 -0400)]
Adjust incremental run script for QF_AX too.

10 years agoModified run script for QF_AX
Clark Barrett [Thu, 12 Jun 2014 22:39:56 +0000 (15:39 -0700)]
Modified run script for QF_AX

10 years agoModified run script for QF_LRA
Clark Barrett [Thu, 12 Jun 2014 22:20:41 +0000 (15:20 -0700)]
Modified run script for QF_LRA

10 years agoMore make submission stuff
Morgan Deters [Thu, 12 Jun 2014 20:22:29 +0000 (16:22 -0400)]
More make submission stuff

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