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.

Best heuristics for handling decision requests from arrays

fixed two bugs for the new E-matching implementation, added aggressive miniscoping option --ag-miniscope-quant, minor cleanup

Merge branch '1.0.x'

Conflicts:
src/smt/smt_engine.cpp

Bugfix for SmtEngine: proper unsubscribing for NodeManager events

Merge branch '1.0.x'

Bug fix for rep-set.

(Cherry-picked from commit c71ec27 in master.)

Fix for quantifiers containing Boolean terms.

Merge branch '1.0.x'

Merge branch '1.0.x' of https://github.com/CVC4/CVC4 into 1.0.x

fix for bv crash in incremental mode; this is a temporary fix for bug 493

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

Single -q quiets messages/warnings.  Double -qq silences sat/unsat output too.

Some exception specification fixes in SmtEngine/Command infrastructure

Fix for gitinfo (resolves bug 399).

Merge branch '1.0.x'

gitinfo modifications fix

Merge pull request #6 from kbansal/decNewoptions

decision/ code refactoring

decision: jh: more refactoring (.h->.cpp, xor/iff)

decision/ : jh: refactor embedded ITE, other minor

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

decision/: justification: refactor ITE out

refactoring justification_heuristic code

rm decision jh GiveUp related code

Some cleanup and copyright updating

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

Merge branch '1.0.x'

Fix version identification for new git repository.

Fix typo in error message

Merge branch '1.0.x'

prvs commit: lower warning to notice

Signed-off-by: Kshitij Bansal <kshitij@cs.nyu.edu>

Merge branch '1.0.x'

make incremental+portfolio experimental

Merge pull request #5 from kbansal/1.0.x

make incremental+portfolio experimental

make incremental+portfolio experimental

Merge branch '1.0.x'

Fix builds/ links to survive configuring twice with different prefixes

Fix ECHO command in CVC language parser to not output quotation marks

Merge branch '1.0.x'

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>

Merge pull request #4 from tiliang/master

a bugfix in rewriting rules

Removing BVDebug and replacing with Debug.

repairs a bug in rewriterule engine: constructor cannot be used as a pattern

Fix a preprocessing performance issue.

Fix user-values in SMT-LIB v1.2

Merge branch '1.0.x'

Conflicts:
src/theory/quantifiers/theory_quantifiers.cpp

Only put quantifier assertions in model equality engine if fullModel==true

Significant work on bug #491 (not yet closed).

More complete fix for bug 484 (includes fixes for records and tuples).

Fix error in tuple type-checking.

Make --default-dag-thresh apply to stringstreams

Do not install the "private-library" header

make datatypes enumerator behavior clearer (no exceptions in normal operation)

make datatypes enumerator behavior clearer (no exceptions in normal operation)

Merge branch '1.0.x'

Fix a compiler warning in NodeBuilder

Merge remote-tracking branch 'origin/1.0.x'

Merge pull request #3 from kbansal/1.0.x

decision/ : save d_prvsIndex in JH

Merge branch '1.0.x'

remove now-unnecessary wrappers from Type interface

Fix to miplib trick to make it less "cautious" and apply in more cases

decision/ : save d_prvsIndex in JH

dos2unix conversion for a number of files; this avoids spurious conflicts when merging to master

More improvements for E-matching

Merge branch '1.0.x'

Fix NodeBuilder bug which could attempt to allocate beyond hard limit

driver::totalTime statistic is now reported correctly on crashes, too

fixed files with DOS newlines; fixed contrib/ scripts to use git

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

Printing commands as they're executed now requires verbosity 3+

Merge branch '1.0.x'

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>

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.

Some cleanup of miplib regressions and options

Merge from mdeters/miplib branch (commit 'ce7c485182902ae43871057185095f71f74a8a58')

new option for doing top-level miplib substitutions (or not)

extended miplib trick to 6 vars, should work on pp miplib examples now

new miplib pass, works for 1 or 2 vars

Remove old miplibtrick from arith static learner

correct output language bug with --dump-to

Merge branch '1.0.x'

Fix a tuple attribute bug that was causing model-generation problems for tuples

Merge branch '1.0.x'

Fix a small problem in clang builds due to namespaces and symbol lookup

Fix a small problem in clang builds due to namespaces and symbol lookup

Adding a heuristic to more eagerly split bounded integer variables.

correct output language bug with --dump-to

currently disabling bug486 regression.  we need to discuss getValue/collectModelInfo for quantifiers more.

fix for finite model finding caused by new collectModelInfo code

Updated NEWS for recent changes.

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)

Merge branch '1.0.x'

Fix the regression test for bug 486, and enable it

(cherry-picked from master 23b4fd82d1ed326cd57e9bc57ef9fab98b0b1c87)

Fix the regression test for bug 486, and enable it

made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced user-level context dependent.  this fixes bug 486

(cherry-picked from master c5d1a5d8f898bf22c6bbc98f1d484b07706c035b)

some fixes for win32, including ability to "make check" win32 builds via wine

made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced user-level context dependent.  this fixes bug 486

some fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory still crashes for datatypes with boolean subfields

(cherry picked from master bcbf52ffbe0416ecf70bdb644017c338c0540793)

some fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory still crashes for datatypes with boolean subfields

Merge branch '1.0.x'

another fix for quantifier models (related to bug 486)

fix --check-model --finite-model-find when used together (related to bug 486)