cvc5.git
11 years agoSome model and printing fixes for defined functions in input.
Morgan Deters [Thu, 21 Mar 2013 18:04:35 +0000 (14:04 -0400)]
Some model and printing fixes for defined functions in input.

11 years agoFix for SmtEngine::expandDefinitions()---improper TypeCheckingException
Morgan Deters [Wed, 20 Feb 2013 23:11:54 +0000 (18:11 -0500)]
Fix for SmtEngine::expandDefinitions()---improper TypeCheckingException

11 years agofixing constant evaluation bugs
Dejan Jovanović [Thu, 21 Mar 2013 04:21:24 +0000 (00:21 -0400)]
fixing constant evaluation bugs

11 years agoBetter reporting of detached git state in --version and --show-config
Morgan Deters [Wed, 20 Mar 2013 22:46:45 +0000 (18:46 -0400)]
Better reporting of detached git state in --version and --show-config

11 years agoFix to bug 497: make justification heuristic's ITE cache context-dependent.
Morgan Deters [Tue, 12 Mar 2013 23:41:28 +0000 (19:41 -0400)]
Fix to bug 497: make justification heuristic's ITE cache context-dependent.

11 years agoRemove unintentionally-committed-to-master README from interactive branch
Morgan Deters [Thu, 21 Mar 2013 00:00:40 +0000 (20:00 -0400)]
Remove unintentionally-committed-to-master README from interactive branch

11 years agoInteractive mode support for multiline input
Morgan Deters [Wed, 12 Dec 2012 22:28:14 +0000 (17:28 -0500)]
Interactive mode support for multiline input

11 years agoProperly |quote| symbols in SMT-LIBv2 output.
Morgan Deters [Wed, 20 Mar 2013 17:09:18 +0000 (13:09 -0400)]
Properly |quote| symbols in SMT-LIBv2 output.

11 years agoSome statistics for narrowing down incrementality issues (push/pop vs solve timing)
Morgan Deters [Tue, 5 Mar 2013 23:52:20 +0000 (18:52 -0500)]
Some statistics for narrowing down incrementality issues (push/pop vs solve timing)

11 years agoAdding evaluation of constant terms to the equality engine. Evaluation on a particula...
Dejan Jovanović [Wed, 20 Mar 2013 01:10:27 +0000 (21:10 -0400)]
Adding evaluation of constant terms to the equality engine. Evaluation on a particular kind can be set by setting interpreted = true when calling addFunctionKind.

11 years agoMinor cleanup of sources
Morgan Deters [Tue, 12 Feb 2013 04:56:10 +0000 (23:56 -0500)]
Minor cleanup of sources

11 years agoFixes for miplib-trick application (and a new testcase)
Morgan Deters [Fri, 8 Feb 2013 15:57:38 +0000 (10:57 -0500)]
Fixes for miplib-trick application (and a new testcase)

11 years agoRemove PropositionalQuery class and all CUDD-related build stuff (and references)
Morgan Deters [Thu, 31 Jan 2013 19:29:58 +0000 (14:29 -0500)]
Remove PropositionalQuery class and all CUDD-related build stuff (and references)

11 years agoMinor fixes to build system
Morgan Deters [Tue, 19 Mar 2013 19:07:46 +0000 (15:07 -0400)]
Minor fixes to build system

11 years agoBoolean terms rewriting for quantified variables of type Bool, when quantifier body...
Morgan Deters [Fri, 15 Mar 2013 17:30:05 +0000 (13:30 -0400)]
Boolean terms rewriting for quantified variables of type Bool, when quantifier body uses them in term context

11 years agoMerge branch '1.0.x'
Morgan Deters [Fri, 15 Mar 2013 16:34:58 +0000 (12:34 -0400)]
Merge branch '1.0.x'

11 years agofix up build system for swig (d242c30 introduced a subtle error)
Morgan Deters [Fri, 15 Mar 2013 16:34:52 +0000 (12:34 -0400)]
fix up build system for swig (d242c30 introduced a subtle error)

11 years agochanged default option for quantifier instantiation
Andrew Reynolds [Fri, 15 Mar 2013 14:15:23 +0000 (09:15 -0500)]
changed default option for quantifier instantiation

11 years agoMerge branch '1.0.x'
Morgan Deters [Thu, 14 Mar 2013 21:27:19 +0000 (17:27 -0400)]
Merge branch '1.0.x'

11 years agoFix warning (line annotation)
Morgan Deters [Thu, 14 Mar 2013 21:23:43 +0000 (17:23 -0400)]
Fix warning (line annotation)

11 years agofix to build system: #include the proper file when they are in both builds and src
Morgan Deters [Thu, 14 Mar 2013 21:16:02 +0000 (17:16 -0400)]
fix to build system: #include the proper file when they are in both builds and src

11 years agoAdded a rewrite for iff:
Clark Barrett [Thu, 14 Mar 2013 00:37:57 +0000 (20:37 -0400)]
Added a rewrite for iff:
x = c iff x = d ---> false
This fixes Andy's problem if unconstrained simplification is turned on.

11 years agoite removal option for quantifiers --ite-remove-quant, e-matching for boolean terms...
Andrew Reynolds [Mon, 11 Mar 2013 21:29:22 +0000 (16:29 -0500)]
ite removal option for quantifiers --ite-remove-quant, e-matching for boolean terms, improvement for pre skolemization

11 years agoDisallow overflow in bitvector literals (parser only)
Morgan Deters [Fri, 22 Feb 2013 21:48:13 +0000 (16:48 -0500)]
Disallow overflow in bitvector literals (parser only)

* For example, (_ bv5 1) is now an error instead of being silently truncated.
* Probably inappropriate for 1.0.x because it changes exception specifications.

11 years agoBest heuristics for handling decision requests from arrays
Clark Barrett [Wed, 6 Mar 2013 19:17:43 +0000 (14:17 -0500)]
Best heuristics for handling decision requests from arrays

11 years agofixed two bugs for the new E-matching implementation, added aggressive miniscoping...
Andrew Reynolds [Wed, 6 Mar 2013 16:46:07 +0000 (10:46 -0600)]
fixed two bugs for the new E-matching implementation, added aggressive miniscoping option --ag-miniscope-quant, minor cleanup

11 years agoMerge branch '1.0.x'
Morgan Deters [Tue, 5 Mar 2013 22:49:25 +0000 (17:49 -0500)]
Merge branch '1.0.x'

Conflicts:
src/smt/smt_engine.cpp

11 years agoBugfix for SmtEngine: proper unsubscribing for NodeManager events
Morgan Deters [Tue, 5 Mar 2013 00:58:09 +0000 (19:58 -0500)]
Bugfix for SmtEngine: proper unsubscribing for NodeManager events

11 years agoMerge branch '1.0.x'
Morgan Deters [Fri, 1 Mar 2013 23:28:22 +0000 (18:28 -0500)]
Merge branch '1.0.x'

11 years agoBug fix for rep-set.
Morgan Deters [Tue, 26 Feb 2013 21:41:56 +0000 (16:41 -0500)]
Bug fix for rep-set.

(Cherry-picked from commit c71ec27 in master.)

11 years agoFix for quantifiers containing Boolean terms.
Morgan Deters [Fri, 22 Feb 2013 15:52:46 +0000 (10:52 -0500)]
Fix for quantifiers containing Boolean terms.

11 years agoMerge branch '1.0.x'
lianah [Tue, 26 Feb 2013 21:02:52 +0000 (16:02 -0500)]
Merge branch '1.0.x'

11 years agoMerge branch '1.0.x' of https://github.com/CVC4/CVC4 into 1.0.x
lianah [Tue, 26 Feb 2013 20:50:48 +0000 (15:50 -0500)]
Merge branch '1.0.x' of https://github.com/CVC4/CVC4 into 1.0.x

11 years agofix for bv crash in incremental mode; this is a temporary fix for bug 493
lianah [Tue, 26 Feb 2013 20:50:37 +0000 (15:50 -0500)]
fix for bv crash in incremental mode; this is a temporary fix for bug 493

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