cvc5.git
11 years agoadded option --model-u-dt-enum for outputting uninterpreted sorts as datatype enumera...
Andrew Reynolds [Sun, 24 Feb 2013 22:37:46 +0000 (16:37 -0600)]
added option --model-u-dt-enum for outputting uninterpreted sorts as datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts

11 years agoSingle -q quiets messages/warnings. Double -qq silences sat/unsat output too.
Morgan Deters [Sat, 16 Feb 2013 20:35:16 +0000 (15:35 -0500)]
Single -q quiets messages/warnings.  Double -qq silences sat/unsat output too.

11 years agoSome exception specification fixes in SmtEngine/Command infrastructure
Morgan Deters [Wed, 20 Feb 2013 23:09:59 +0000 (18:09 -0500)]
Some exception specification fixes in SmtEngine/Command infrastructure

11 years agoFix for gitinfo (resolves bug 399).
Morgan Deters [Mon, 18 Feb 2013 16:04:43 +0000 (11:04 -0500)]
Fix for gitinfo (resolves bug 399).

11 years agoMerge branch '1.0.x'
Kshitij Bansal [Sun, 17 Feb 2013 04:57:57 +0000 (23:57 -0500)]
Merge branch '1.0.x'

11 years agogitinfo modifications fix
Kshitij Bansal [Sun, 17 Feb 2013 04:56:22 +0000 (23:56 -0500)]
gitinfo modifications fix

11 years agoMerge pull request #6 from kbansal/decNewoptions
Kshitij Bansal [Sun, 17 Feb 2013 03:28:14 +0000 (19:28 -0800)]
Merge pull request #6 from kbansal/decNewoptions

decision/ code refactoring

11 years agodecision: jh: more refactoring (.h->.cpp, xor/iff)
Kshitij Bansal [Sun, 17 Feb 2013 01:52:03 +0000 (20:52 -0500)]
decision: jh: more refactoring (.h->.cpp, xor/iff)

11 years agodecision/ : jh: refactor embedded ITE, other minor
Kshitij Bansal [Sun, 17 Feb 2013 00:58:07 +0000 (19:58 -0500)]
decision/ : jh: refactor embedded ITE, other minor

other minor: cleanup some remaning fragments of GiveUpException(),
hopefully all is gone now.

11 years agodecision/: justification: refactor ITE out
Kshitij Bansal [Sun, 17 Feb 2013 00:22:31 +0000 (19:22 -0500)]
decision/: justification: refactor ITE out

11 years agorefactoring justification_heuristic code
Kshitij Bansal [Sat, 16 Feb 2013 23:19:02 +0000 (18:19 -0500)]
refactoring justification_heuristic code

11 years agorm decision jh GiveUp related code
Kshitij Bansal [Wed, 13 Feb 2013 21:39:51 +0000 (16:39 -0500)]
rm decision jh GiveUp related code

11 years agoSome cleanup and copyright updating
Morgan Deters [Fri, 15 Feb 2013 16:19:08 +0000 (11:19 -0500)]
Some cleanup and copyright updating

* update some copyrights for 2013
* cleaned up some comments/ifdefs, indentation
* some spelling corrections
* add some missing makefiles

11 years agoMerge branch '1.0.x'
Morgan Deters [Sat, 16 Feb 2013 20:22:14 +0000 (15:22 -0500)]
Merge branch '1.0.x'

11 years agoFix version identification for new git repository.
Morgan Deters [Fri, 25 Jan 2013 22:11:44 +0000 (17:11 -0500)]
Fix version identification for new git repository.

11 years agoFix typo in error message
Morgan Deters [Fri, 15 Feb 2013 20:16:23 +0000 (15:16 -0500)]
Fix typo in error message

11 years agoMerge branch '1.0.x'
Kshitij Bansal [Fri, 15 Feb 2013 22:21:00 +0000 (17:21 -0500)]
Merge branch '1.0.x'

11 years agoprvs commit: lower warning to notice
Kshitij Bansal [Fri, 15 Feb 2013 22:10:50 +0000 (17:10 -0500)]
prvs commit: lower warning to notice

Signed-off-by: Kshitij Bansal <kshitij@cs.nyu.edu>
11 years agoMerge branch '1.0.x'
Kshitij Bansal [Fri, 15 Feb 2013 21:43:30 +0000 (16:43 -0500)]
Merge branch '1.0.x'

11 years agomake incremental+portfolio experimental
Kshitij Bansal [Fri, 15 Feb 2013 20:54:04 +0000 (15:54 -0500)]
make incremental+portfolio experimental

11 years agoMerge pull request #5 from kbansal/1.0.x
Kshitij Bansal [Fri, 15 Feb 2013 21:40:29 +0000 (13:40 -0800)]
Merge pull request #5 from kbansal/1.0.x

make incremental+portfolio experimental

11 years agomake incremental+portfolio experimental
Kshitij Bansal [Fri, 15 Feb 2013 20:54:04 +0000 (15:54 -0500)]
make incremental+portfolio experimental

11 years agoMerge branch '1.0.x'
Morgan Deters [Fri, 15 Feb 2013 17:37:50 +0000 (12:37 -0500)]
Merge branch '1.0.x'

11 years agoFix builds/ links to survive configuring twice with different prefixes
Morgan Deters [Fri, 15 Feb 2013 17:00:29 +0000 (12:00 -0500)]
Fix builds/ links to survive configuring twice with different prefixes

11 years agoFix ECHO command in CVC language parser to not output quotation marks
Morgan Deters [Fri, 15 Feb 2013 16:48:24 +0000 (11:48 -0500)]
Fix ECHO command in CVC language parser to not output quotation marks

11 years agoMerge branch '1.0.x'
Tim King [Fri, 15 Feb 2013 16:35:34 +0000 (11:35 -0500)]
Merge branch '1.0.x'

11 years agorepairs a bug in rewriterule engine: constructor cannot be used as a pattern
Tianyi Liang [Thu, 14 Feb 2013 05:12:04 +0000 (23:12 -0600)]
repairs a bug in rewriterule engine: constructor cannot be used as a pattern
(cherry picked from commit c33a1abc78bcd51f3f95562b117498caf252cafc)

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
11 years agoMerge pull request #4 from tiliang/master
Dejan Jovanović [Thu, 14 Feb 2013 22:10:20 +0000 (14:10 -0800)]
Merge pull request #4 from tiliang/master

a bugfix in rewriting rules

11 years agoRemoving BVDebug and replacing with Debug.
Tim King [Thu, 14 Feb 2013 21:11:42 +0000 (16:11 -0500)]
Removing BVDebug and replacing with Debug.

11 years agorepairs a bug in rewriterule engine: constructor cannot be used as a pattern
Tianyi Liang [Thu, 14 Feb 2013 05:12:04 +0000 (23:12 -0600)]
repairs a bug in rewriterule engine: constructor cannot be used as a pattern

11 years agoFix a preprocessing performance issue.
Morgan Deters [Wed, 13 Feb 2013 04:04:53 +0000 (23:04 -0500)]
Fix a preprocessing performance issue.

11 years agoFix user-values in SMT-LIB v1.2
Morgan Deters [Fri, 8 Feb 2013 22:23:32 +0000 (17:23 -0500)]
Fix user-values in SMT-LIB v1.2

11 years agoMerge branch '1.0.x'
Morgan Deters [Fri, 8 Feb 2013 00:03:09 +0000 (19:03 -0500)]
Merge branch '1.0.x'

Conflicts:
src/theory/quantifiers/theory_quantifiers.cpp

11 years agoOnly put quantifier assertions in model equality engine if fullModel==true
Morgan Deters [Thu, 7 Feb 2013 21:18:08 +0000 (16:18 -0500)]
Only put quantifier assertions in model equality engine if fullModel==true

11 years agoSignificant work on bug #491 (not yet closed).
Morgan Deters [Fri, 1 Feb 2013 23:00:12 +0000 (18:00 -0500)]
Significant work on bug #491 (not yet closed).

11 years agoMore complete fix for bug 484 (includes fixes for records and tuples).
Morgan Deters [Fri, 21 Dec 2012 23:44:34 +0000 (18:44 -0500)]
More complete fix for bug 484 (includes fixes for records and tuples).

11 years agoFix error in tuple type-checking.
Morgan Deters [Thu, 7 Feb 2013 20:34:23 +0000 (15:34 -0500)]
Fix error in tuple type-checking.

11 years agoMake --default-dag-thresh apply to stringstreams
Morgan Deters [Thu, 7 Feb 2013 20:28:20 +0000 (15:28 -0500)]
Make --default-dag-thresh apply to stringstreams

11 years agoDo not install the "private-library" header
Morgan Deters [Thu, 7 Feb 2013 18:58:22 +0000 (13:58 -0500)]
Do not install the "private-library" header

11 years agomake datatypes enumerator behavior clearer (no exceptions in normal operation)
Morgan Deters [Thu, 7 Feb 2013 02:30:35 +0000 (21:30 -0500)]
make datatypes enumerator behavior clearer (no exceptions in normal operation)

11 years agomake datatypes enumerator behavior clearer (no exceptions in normal operation)
Morgan Deters [Thu, 7 Feb 2013 02:30:35 +0000 (21:30 -0500)]
make datatypes enumerator behavior clearer (no exceptions in normal operation)

11 years agoMerge branch '1.0.x'
Morgan Deters [Tue, 5 Feb 2013 21:39:30 +0000 (16:39 -0500)]
Merge branch '1.0.x'

11 years agoFix a compiler warning in NodeBuilder
Morgan Deters [Tue, 5 Feb 2013 21:30:17 +0000 (16:30 -0500)]
Fix a compiler warning in NodeBuilder

11 years agoMerge remote-tracking branch 'origin/1.0.x'
Kshitij Bansal [Tue, 5 Feb 2013 21:24:02 +0000 (16:24 -0500)]
Merge remote-tracking branch 'origin/1.0.x'

11 years agoMerge pull request #3 from kbansal/1.0.x
Kshitij Bansal [Tue, 5 Feb 2013 21:08:13 +0000 (13:08 -0800)]
Merge pull request #3 from kbansal/1.0.x

decision/ : save d_prvsIndex in JH

11 years agoMerge branch '1.0.x'
Morgan Deters [Tue, 5 Feb 2013 21:03:43 +0000 (16:03 -0500)]
Merge branch '1.0.x'

11 years agoremove now-unnecessary wrappers from Type interface
Morgan Deters [Tue, 5 Feb 2013 20:25:38 +0000 (15:25 -0500)]
remove now-unnecessary wrappers from Type interface

11 years agoFix to miplib trick to make it less "cautious" and apply in more cases
Morgan Deters [Tue, 5 Feb 2013 21:00:02 +0000 (16:00 -0500)]
Fix to miplib trick to make it less "cautious" and apply in more cases

11 years agodecision/ : save d_prvsIndex in JH
Kshitij Bansal [Wed, 30 Jan 2013 16:59:59 +0000 (11:59 -0500)]
decision/ : save d_prvsIndex in JH

11 years agodos2unix conversion for a number of files; this avoids spurious conflicts when mergin...
Morgan Deters [Tue, 5 Feb 2013 19:28:52 +0000 (14:28 -0500)]
dos2unix conversion for a number of files; this avoids spurious conflicts when merging to master

11 years agoMore improvements for E-matching
Andrew Reynolds [Tue, 5 Feb 2013 07:35:21 +0000 (01:35 -0600)]
More improvements for E-matching

11 years agoMerge branch '1.0.x'
Morgan Deters [Mon, 4 Feb 2013 23:11:40 +0000 (18:11 -0500)]
Merge branch '1.0.x'

11 years agoFix NodeBuilder bug which could attempt to allocate beyond hard limit
Morgan Deters [Mon, 4 Feb 2013 23:11:09 +0000 (18:11 -0500)]
Fix NodeBuilder bug which could attempt to allocate beyond hard limit

11 years agodriver::totalTime statistic is now reported correctly on crashes, too
Morgan Deters [Wed, 30 Jan 2013 23:55:44 +0000 (18:55 -0500)]
driver::totalTime statistic is now reported correctly on crashes, too

11 years agofixed files with DOS newlines; fixed contrib/ scripts to use git
Morgan Deters [Mon, 4 Feb 2013 22:30:18 +0000 (17:30 -0500)]
fixed files with DOS newlines; fixed contrib/ scripts to use git

11 years agoSome fixes for the miplib preprocessing pass.
Morgan Deters [Mon, 4 Feb 2013 21:01:17 +0000 (16:01 -0500)]
Some fixes for the miplib preprocessing pass.

* TNode violation bug fix (thanks to Tim King for discovery & fix)
* change Boolean miplib-trick substitution option into a threshold
* ppAssert() the generated miplib constraints to arithmetic

11 years agoPrinting commands as they're executed now requires verbosity 3+
Morgan Deters [Mon, 4 Feb 2013 21:24:33 +0000 (16:24 -0500)]
Printing commands as they're executed now requires verbosity 3+

11 years agoMerge branch '1.0.x'
Morgan Deters [Mon, 4 Feb 2013 18:53:16 +0000 (13:53 -0500)]
Merge branch '1.0.x'

11 years agoModel no longer adds subterms of quantifiers to equality engine, this fixed bug 492...
Morgan Deters [Mon, 4 Feb 2013 18:52:45 +0000 (13:52 -0500)]
Model no longer adds subterms of quantifiers to equality engine, this fixed bug 492 and resolves previous issue for bug 486.
(cherry picked from *part* of commit e54c0f73712b25f1d6d49a3817c923eea077da81)

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
11 years agoModel no longer adds subterms of quantifiers to equality engine, this fixed bug 492...
Andrew Reynolds [Mon, 4 Feb 2013 06:08:32 +0000 (00:08 -0600)]
Model no longer adds subterms of quantifiers to equality engine, this fixed bug 492 and resolves previous issue for bug 486.\n Multiple improvements for E-matching: do not choose multi-triggers if single triggers exist, only create multi-triggers that contain all variables, consider multiple terms per equivalence class but only add one instantiation per round per (trigger,term) pair.\nImprovements for strong solver: make use of sort inference information when choosing splits, check for cliques eagerly when disequalities are asserted.

11 years agoSome cleanup of miplib regressions and options
Morgan Deters [Sun, 3 Feb 2013 21:05:37 +0000 (16:05 -0500)]
Some cleanup of miplib regressions and options

11 years agoMerge from mdeters/miplib branch (commit 'ce7c485182902ae43871057185095f71f74a8a58')
Morgan Deters [Sun, 3 Feb 2013 20:57:01 +0000 (15:57 -0500)]
Merge from mdeters/miplib branch (commit 'ce7c485182902ae43871057185095f71f74a8a58')

11 years agonew option for doing top-level miplib substitutions (or not)
Morgan Deters [Sun, 3 Feb 2013 20:37:04 +0000 (15:37 -0500)]
new option for doing top-level miplib substitutions (or not)

11 years agoextended miplib trick to 6 vars, should work on pp miplib examples now
Morgan Deters [Fri, 1 Feb 2013 23:05:39 +0000 (18:05 -0500)]
extended miplib trick to 6 vars, should work on pp miplib examples now

11 years agonew miplib pass, works for 1 or 2 vars
Morgan Deters [Tue, 29 Jan 2013 22:39:12 +0000 (17:39 -0500)]
new miplib pass, works for 1 or 2 vars

11 years agoRemove old miplibtrick from arith static learner
Morgan Deters [Thu, 31 Jan 2013 19:29:12 +0000 (14:29 -0500)]
Remove old miplibtrick from arith static learner

11 years agocorrect output language bug with --dump-to
Morgan Deters [Wed, 30 Jan 2013 20:43:33 +0000 (15:43 -0500)]
correct output language bug with --dump-to

11 years agoMerge branch '1.0.x'
Morgan Deters [Fri, 1 Feb 2013 14:17:46 +0000 (09:17 -0500)]
Merge branch '1.0.x'

11 years agoFix a tuple attribute bug that was causing model-generation problems for tuples
Morgan Deters [Fri, 1 Feb 2013 13:31:34 +0000 (08:31 -0500)]
Fix a tuple attribute bug that was causing model-generation problems for tuples

11 years agoMerge branch '1.0.x'
Morgan Deters [Thu, 31 Jan 2013 23:30:48 +0000 (18:30 -0500)]
Merge branch '1.0.x'

11 years agoFix a small problem in clang builds due to namespaces and symbol lookup
Morgan Deters [Thu, 31 Jan 2013 21:54:22 +0000 (16:54 -0500)]
Fix a small problem in clang builds due to namespaces and symbol lookup

11 years agoFix a small problem in clang builds due to namespaces and symbol lookup
Morgan Deters [Thu, 31 Jan 2013 21:54:22 +0000 (16:54 -0500)]
Fix a small problem in clang builds due to namespaces and symbol lookup

11 years agoAdding a heuristic to more eagerly split bounded integer variables.
Tim King [Thu, 31 Jan 2013 21:34:12 +0000 (16:34 -0500)]
Adding a heuristic to more eagerly split bounded integer variables.

11 years agocorrect output language bug with --dump-to
Morgan Deters [Wed, 30 Jan 2013 20:43:33 +0000 (15:43 -0500)]
correct output language bug with --dump-to

11 years agocurrently disabling bug486 regression. we need to discuss getValue/collectModelInfo...
Andrew Reynolds [Tue, 29 Jan 2013 06:07:52 +0000 (00:07 -0600)]
currently disabling bug486 regression.  we need to discuss getValue/collectModelInfo for quantifiers more.

11 years agofix for finite model finding caused by new collectModelInfo code
Andrew Reynolds [Tue, 29 Jan 2013 05:19:12 +0000 (23:19 -0600)]
fix for finite model finding caused by new collectModelInfo code

11 years agoUpdated NEWS for recent changes.
Morgan Deters [Mon, 28 Jan 2013 20:26:41 +0000 (15:26 -0500)]
Updated NEWS for recent changes.

11 years agoFixes for Win32 (closes bugs 488 and 489)
Morgan Deters [Mon, 28 Jan 2013 20:21:52 +0000 (15:21 -0500)]
Fixes for Win32 (closes bugs 488 and 489)

* timer statistics now supported (closes bug 488)
* use of --mmap doesn't crash anymore (closes bug 489)

11 years agoMerge branch '1.0.x'
Morgan Deters [Mon, 28 Jan 2013 16:53:01 +0000 (11:53 -0500)]
Merge branch '1.0.x'

11 years agoFix the regression test for bug 486, and enable it
Morgan Deters [Fri, 25 Jan 2013 20:57:54 +0000 (15:57 -0500)]
Fix the regression test for bug 486, and enable it

(cherry-picked from master 23b4fd82d1ed326cd57e9bc57ef9fab98b0b1c87)

11 years agoFix the regression test for bug 486, and enable it
Morgan Deters [Fri, 25 Jan 2013 20:57:54 +0000 (15:57 -0500)]
Fix the regression test for bug 486, and enable it

11 years agomade QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced...
Andrew Reynolds [Mon, 28 Jan 2013 07:57:20 +0000 (01:57 -0600)]
made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced user-level context dependent.  this fixes bug 486

(cherry-picked from master c5d1a5d8f898bf22c6bbc98f1d484b07706c035b)

11 years agosome fixes for win32, including ability to "make check" win32 builds via wine
Morgan Deters [Mon, 28 Jan 2013 14:30:12 +0000 (09:30 -0500)]
some fixes for win32, including ability to "make check" win32 builds via wine

11 years agomade QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced...
Andrew Reynolds [Mon, 28 Jan 2013 07:57:20 +0000 (01:57 -0600)]
made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced user-level context dependent.  this fixes bug 486

11 years agosome fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory...
Andrew Reynolds [Sun, 27 Jan 2013 17:35:22 +0000 (11:35 -0600)]
some fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory still crashes for datatypes with boolean subfields

(cherry picked from master bcbf52ffbe0416ecf70bdb644017c338c0540793)

11 years agosome fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory...
Andrew Reynolds [Sun, 27 Jan 2013 17:35:22 +0000 (11:35 -0600)]
some fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory still crashes for datatypes with boolean subfields

11 years agoMerge branch '1.0.x'
Morgan Deters [Sun, 27 Jan 2013 02:11:36 +0000 (21:11 -0500)]
Merge branch '1.0.x'

11 years agoanother fix for quantifier models (related to bug 486)
Morgan Deters [Sun, 27 Jan 2013 02:09:55 +0000 (21:09 -0500)]
another fix for quantifier models (related to bug 486)

11 years agofix --check-model --finite-model-find when used together (related to bug 486)
Morgan Deters [Fri, 25 Jan 2013 22:06:02 +0000 (17:06 -0500)]
fix --check-model --finite-model-find when used together (related to bug 486)

11 years agoFix errors and reduce warnings on clang (merge from mdeters/clang)
Morgan Deters [Fri, 25 Jan 2013 20:16:43 +0000 (15:16 -0500)]
Fix errors and reduce warnings on clang (merge from mdeters/clang)

11 years agofix --check-model --finite-model-find when used together (related to bug 486)
Morgan Deters [Fri, 25 Jan 2013 22:06:02 +0000 (17:06 -0500)]
fix --check-model --finite-model-find when used together (related to bug 486)

11 years agoAdd win32 support (merge from mdeters/win32, with some cleanup).
Morgan Deters [Tue, 18 Dec 2012 20:33:43 +0000 (15:33 -0500)]
Add win32 support (merge from mdeters/win32, with some cleanup).

11 years agoAdding miplibtrick option.
Tim King [Wed, 23 Jan 2013 21:35:16 +0000 (16:35 -0500)]
Adding miplibtrick option.

11 years agoAdding substitution size cap.
Tim King [Wed, 23 Jan 2013 21:34:07 +0000 (16:34 -0500)]
Adding substitution size cap.

11 years agoMerge branch '1.0.x'
Morgan Deters [Wed, 23 Jan 2013 22:07:11 +0000 (17:07 -0500)]
Merge branch '1.0.x'

Conflicts:
NEWS

11 years agofix to workaround ANTLR 3.2 issue with initialization
Morgan Deters [Wed, 23 Jan 2013 22:04:43 +0000 (17:04 -0500)]
fix to workaround ANTLR 3.2 issue with initialization

11 years agopartially address bug 486: allow some model inspection of quantifiers
Morgan Deters [Wed, 23 Jan 2013 22:00:56 +0000 (17:00 -0500)]
partially address bug 486: allow some model inspection of quantifiers

11 years agopartially address bug 486: allow some model inspection of quantifiers
Morgan Deters [Wed, 23 Jan 2013 22:00:56 +0000 (17:00 -0500)]
partially address bug 486: allow some model inspection of quantifiers

11 years agoupdate NEWS file
Morgan Deters [Wed, 23 Jan 2013 21:11:55 +0000 (16:11 -0500)]
update NEWS file

11 years agoadd user patterns to the Smt1 parser; update NEWS file
Morgan Deters [Wed, 23 Jan 2013 20:53:31 +0000 (15:53 -0500)]
add user patterns to the Smt1 parser; update NEWS file