Make --incremental the default when running interactively

getModelValue implementation in bitvectors

adding
* getModelValue to valuation
* getModelValue to theory engine
* getModelValue to theory
implemented getModelValue in bitvector

the purpose of getModelValue is to ask for a concrete value of a shared term

Merge branch 'master' of git@github.com:CVC4/CVC4.git

moving bv before arrays

java input stream adapters working

Fix for SCM detection

Merge pull request #7 from kbansal/portfolio

finish removal of separateOutput

finish removal of separateOutput

Fix bug in portfolio executor output; fixes nightly portfolio-checking runs.

Merge remote-tracking branch 'dddejan/c++11'

Conflicts:
src/smt/boolean_terms.cpp

changing string hash function to use the gnu namespace
due to namesapce resolution std namespace was used instead, which hashes the string pointers leading to mayhem

Support for Boolean term conversion in datatypes.

compiles with
export CXXFLAGS='-std=gnu++0x' before configure
fails all regressions in the parser

another typo/bugfix for equality constant evaluation

Better error in case of nonlinear assertions while in linear logic

Add the ability to "mute" commands, needed for SMT-LIB compliance.

fixing markings of internal nodes in equality engine

Merge branch 'master' of github.com:CVC4/CVC4

Some model and printing fixes for defined functions in input.

more equality constant evaluation

Fix for SmtEngine::expandDefinitions()---improper TypeCheckingException

fixing constant evaluation bugs

Better reporting of detached git state in --version and --show-config

Fix to bug 497: make justification heuristic's ITE cache context-dependent.

Remove unintentionally-committed-to-master README from interactive branch

Interactive mode support for multiline input

Properly |quote| symbols in SMT-LIBv2 output.

Some statistics for narrowing down incrementality issues (push/pop vs solve timing)

Adding evaluation of constant terms to the equality engine. Evaluation on a particular kind can be set by setting interpreted = true when calling addFunctionKind.

Minor cleanup of sources

Fixes for miplib-trick application (and a new testcase)

Remove PropositionalQuery class and all CUDD-related build stuff (and references)

Minor fixes to build system

Boolean terms rewriting for quantified variables of type Bool, when quantifier body uses them in term context

Merge branch '1.0.x'

fix up build system for swig (d242c30 introduced a subtle error)

changed default option for quantifier instantiation

Merge branch '1.0.x'

Fix warning (line annotation)

fix to build system: #include the proper file when they are in both builds and src

Added a rewrite for iff:
x = c iff x = d ---> false
This fixes Andy's problem if unconstrained simplification is turned on.

ite removal option for quantifiers --ite-remove-quant, e-matching for boolean terms, improvement for pre skolemization

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'