Code cleanup.

Documentation clean-ups.

Another fix for the CASC stuff.

Final preparations for arithmetic for building with libc++.

Fix for new CASC features, fixes Java builds.

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.

This commit adds a priority queue implementation.  This is to avoid compilation troubles with libc++.

Test portfolio with --no-wait-to-join.

For casc : print models of functions rewritten by sort inference.

Fix rewriter typo.

Clean up glpk detection a little, fix a detection bug.

fix typo

More application-track fixes for use with trace executor.

Versioning preparation.

Some fixes for tear-down-incremental and "success" output.

Disallow context-dependent copy/assignment.

Fix compile errors with some versions of GCC.

Clean up some compiler warnings on 32-bit.

Minor fixes to get-abc script and configure stuff.

get-glpk-cut-log script, and configure code.

dos2unix-convert some sources.

Minor fixes, spelling etc.

More proof support for CASC : include skolemization

minor update to application track config in QF_BV

core solver fix

Careful there aren't too many "success" messages with --tear-down-incremental (can confuse trace runner).

fixed bv bug due to applying equisatisfiable transformations in ppRewrite

Application trace executor (if they end up using that) requires --print-success.

One last(?) fix for build script for smtcomp uploads.

fixed fuzzer assertion failures for bv

fix travis config

better bv args for smtcomp

added rewriting to bv-pow2 pass

Evil bitvector preprocessing pass for simplifying powers of two.

bv static learning and rewrites for power of 2 terms

more bv rewrites

fix to inequality rewrite

fixed merge

added bv inequality rewrite

added bv inequality lemmas

added bv inequality lemmas

Fix for fmf with large finite cardinalities.

fixed BVMinisat bug due to not clearing seen properly

Doubly-ensure incremental is off in main track.  Also import bv-portfolio strategy.

Fix handling of ALIA.

update application track script too

Update for QF_AUFLIA strategy

Allow parallel failures when building competition version (they are spurious).

Adjust incremental run script for QF_AX too.

Modified run script for QF_AX

Modified run script for QF_LRA

More make submission stuff

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

fixing bv inequality solver explanation bug

New application track script, new heuristics and all --tear-down-incremental.  Not yet tested.

added bvcomp case to bv to bool lifting

more fix-ups

added optionException for trying to use abc in an non-abc build

more smtcomp-submission script work

Flush output stream after result printed in portfolio.

Fix for competition mode + parallel.

Fix parallel run script.

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

switched bv equality order

Update SMTCOMP script to handle all quantified logics.

Fix an omission in bv sources.

--best now implies --with-glpk --with-abc

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.

Merge pull request #31 from kbansal/sets

Sets

fixed unit tests failures

disable another test, after recent merges taking too long

disable failing test

sets: comment out an assertion too strong

user/sat context issue in sets

fix in sets rewriter

fixing bv ackermanization cache bug

Add new --pb-rewrites options to QF_LIA run script for SMT-COMP.

Some news about API changes.

Merging Tim's pseudoboolean work from his fmcad14 branch.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

reverting portfolio hack

Merging CAV14 paper bit-vector work.

Disallow copy/assignment of SmtEngine.

Tim's options for QF_LIA and QF_LRA---SOI+approx.

Merge pull request #29 from kbansal/alternatefix

Fix for emptyset in smt2 parser, sets translator to quantified logic, misc

Add missing set of braces, fixes --trace.

Also ensure // commented Debug() lines don't get included in Debug/Trace_tags.

parseErrorHelper : factor out whole word matching

catches some corner cases, more readable too

test for prvs commit (tokenize emptyset)

9978c259f30b1f4b2c70c04589a309033a6eb1f6

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.

smt2 parser: tokenize emptyset only if theory enabled

Better error when there are \backslashes in |quoted symbols|.

Allow 'repeat' as an SMT-LIB user symbol name (UFNIA/vcc-havoc does this).

sets translate: a different translation using axioms

todo: set logic correctly, split the code for two translators

sets translator: fix for dags

Merge pull request #28 from kbansal/sets

Sets translator, bug fixes

Fix submission script (again).

rm warning from helloworld example

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.

sets: fix equality propagation

-{d,t} help => --show-{debug,trace}-tags

option to hide stats which are zero (off by default), also some aliases