cvc5.git
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 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 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 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 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 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 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 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 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 agocore solver fix
lianah [Mon, 16 Jun 2014 01:33:51 +0000 (21:33 -0400)]
core solver fix

10 years agoCareful there aren't too many "success" messages with --tear-down-incremental (can...
Morgan Deters [Mon, 16 Jun 2014 00:16:35 +0000 (20:16 -0400)]
Careful there aren't too many "success" messages with --tear-down-incremental (can confuse trace runner).

10 years agofixed bv bug due to applying equisatisfiable transformations in ppRewrite
lianah [Mon, 16 Jun 2014 00:36:12 +0000 (20:36 -0400)]
fixed bv bug due to applying equisatisfiable transformations in ppRewrite

10 years agoApplication trace executor (if they end up using that) requires --print-success.
Morgan Deters [Sun, 15 Jun 2014 23:54:19 +0000 (19:54 -0400)]
Application trace executor (if they end up using that) requires --print-success.

10 years agoOne last(?) fix for build script for smtcomp uploads.
Morgan Deters [Sun, 15 Jun 2014 21:29:13 +0000 (17:29 -0400)]
One last(?) fix for build script for smtcomp uploads.

10 years agofixed fuzzer assertion failures for bv
lianah [Sun, 15 Jun 2014 20:10:32 +0000 (16:10 -0400)]
fixed fuzzer assertion failures for bv

10 years agofix travis config
Morgan Deters [Sun, 15 Jun 2014 06:05:17 +0000 (02:05 -0400)]
fix travis config

10 years agobetter bv args for smtcomp
Morgan Deters [Sun, 15 Jun 2014 05:29:53 +0000 (01:29 -0400)]
better bv args for smtcomp

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.