Merge from arrays2 branch.

fix production-build compiler warning

re-add a removed Datatype constructor that was causing a unit test failure, so nightlies go through tonight

reverting node manager change from 1881; also part of parameterized datatypes review

add AscriptionType stuff to support nullary parameterized datatypes; also, review of Andy's earlier commit, with some minor code clean-up and documentation

added support for parametric datatypes, updated cvc parser to handle parametric datatypes, type ascriptions are not implemented yet

* fix for Mac OS (includes some ThreadLocal stuff copied in from portfolio
  branch)
* add Theory::isSharedTermFact() -- it currently always returns false,
  pending theory combination work
* Add "unknown" cardinalities to Cardinality class
* Fix run_regression script to handle CRLF line terminators on Macs
  (where sed is non-GNU)
* Convert CRLF line terminators in datatypes regressions to LF

Deleting dead code.

added 10 benchmarks to regress/regress0/datatypes from paper

significant revisions/improvements to code for theory datatypes solver

Merge from nonclausal-simplification-v2 branch:

* Preprocessing-time, non-clausal, Boolean simplification round to
  support "quasi-non-linear rewrites" as discussed at last few meetings.

* --simplification=none is the default for now, but we'll probably
  change that to --simplification=incremental.  --simplification=batch
  is also a possibility.  See --simplification=help for details.

* RecursionBreaker<T> now uses a hash set for the seen trail.
* Fixes to TLS stuff to support that.
* Fixes to theory and SmtEngine documentation.
* Fixes to stream indentation.
* Other miscellaneous stuff.

luby sequence generator; can use to plot MiniSat's restart sequence

Stronger support for zero-performance-penalty output, and fixes and
simplifications for the "muzzled" (i.e. competition) design, which had
been broken.  Addition of some new unit test bits to ensure that
nothing is ever called in muzzled builds, e.g. things like

  Warning() << expensiveFunction();

Also, fix some compiler warnings.

output fixes for performance

minor updates to exp manager, fixed 32bit vs 64bit issues in transitive closure module, theory datatypes now uses transitive closure for cycle detection, bug 261 fixed

fix for configure

adding some previously-failing "bug" test cases for bitvectors

updating bv regressions

parser fixes for bug 243

updates for bitvectors

more minor fixes related to last few commits

another small fix

fix broken build; sorry, all!

fix a performance issue from last commit

Minor fixes to various parts of CVC4, including the removal of the uintptr_t constructors for Type and Expr (which existed due to ANTLR limitations).  These issues are now handled (as a hack, due to said limitations) in the parser rather than the CVC4 core.

minor fixes, plus experimental readline support in InteractiveShell

refactoring to datatypes theory, added working prototype for proof/explanation manager

more fixes/improvements to datatypes theory and transitive closure

cleaned up some of the hacks in the datatypes theory solver, working on using Transitive Closure to detect cycles, added rewrite rule for disinguished ground terms

Monday tasks:

* new "well-foundedness" type property (like cardinality) specified in
  Theory kinds files; specifies well-foundedness and a ground term

* well-foundedness / finite checks in Datatypes now superseded by type
  system isFinite(), isWellFounded(), mkGroundTerm().

* new "RecursionBreaker" template class, a convenient class that keeps
  a "seen" trail without you having to pass it around (which is
  difficult in cases of mutual recursion) of the idea of passing
  around a "seen" trail

small unit test fix; was broken only in non-assertion, non-CLN builds

Weekend work.  The main points:

* Type::getCardinality() returns the cardinality for for all types.
  Theories give a cardinality in the their kinds file.  For
  cardinalities that depend on a type argument, a "cardinality
  computer" function is named in the kinds file, which takes a
  TypeNode and returns its cardinality.

* There's a bitmap for the set of "active theories" in the
  TheoryEngine.  Theories become "active" when a term that is owned by
  them, or whose type is owned by them, is pre-registered (run CVC4
  with --verbose to see theory activation).  Non-active theories don't
  get any calls for check() or propagate() or anything, and if we're
  running in single-theory mode, the shared term manager doesn't have
  to get involved.  This is really important for get() performance
  (which can only skimp on walking the entire sub-DAG only if the
  theory doesn't require it AND the shared term manager doesn't
  require it).

* TheoryEngine now does not call presolve(), registerTerm(),
  notifyRestart(), etc., on a Theory if that theory doesn't declare
  that property in its kinds file.  To avoid coding errors,
  mktheorytraits greps the theory header and gives warnings if:
  + the theory appears to declare one of the functions (check,
    propagate, etc.) that isn't listed among its kinds file properties
    (but probably should be)
  + the theory appears NOT to declare one of the functions listed in
    its kinds file properties

* some bounded token stream work

fix for parser/tests for ANTLR 3.2 (it was working fine on 3.3)

* reviewed BooleanSimplification, added documentation & unit test
* work around a lexer ambiguity in CVC grammar
* add support for tracing antlr parser/lexer
* add parsing support for more language features
* initial parameterized types parsing work to support Andy's work

make run_regression script robust to DOS newlines :(

added fixes for datatype theory solver to account for rewriting before finite/well-founded check.

fix to last commit

Fixing SmtEngine::getValue() by adding a NodeManagerScope (thanks Tim for finding this)

numerous bugfixes

incorrect usage of C++ std::string caused a test to fail

Minor mixed-bag commit.  Expected performance impact negligible.

* Fixed hole in arrays typechecking.
* Fixed "make dist".
* Better ouroborous test, and some printer fixes.
* Continued cleanup in CVC parser, removed some warnings.
* Better output.

Tuesday end-of-day commit.

Expected performance impact outside of datatypes/CVC parser is
negligible.

* CVC language LAMBDA, functional LET, type LET, precedence fixes,
  bitvectors, and arrays, with partial parsing support also for
  quantifiers, tuples, subranges, subtypes, and records
* support for complex recursive DATATYPE selectors, e.g.
    tree = node(children:ARRAY INT OF tree) | leaf(data:INT)
  these are complicated because they have to be left unresolved
  at parse time and dealt with in a second pass.
* bugfix for Exprs/Types that occurred when setting them to null
  (not Nodes/TypeNodes, just Exprs/Types).
* Cleanup/code review items

Removing dead code that came in on commit r1740.

more work on CVC language

mostly CVC presentation language parsing and printing

This commit merges the branch arithmetic/propagation-again into trunk.
- This adds code for bounds refinement, and conflict weakening.
- This adds util/boolean_simplification.h.
- This adds a propagation manager to theory of arithmetic.
- Propagation is disabled by default.
- Propagation can be enabled by the command line flag "--enable-arithmetic-propagation"
- Propagation interacts *heavily* with rewriting equalities, and will work best if the command line flag "--rewrite-arithmetic-equalities" is enabled.

Partial merge from datatypes-merge branch:

1. Defines a new type "DatatypeType", a type-constant that holds a Datatype, describing an inductive data type.
2. CVC language parser supports datatypes.
3. CVC language printer now functional.
4. Minor other cleanups.

No performance impact is expected outside of datatypes.  I'm verifying that that is the case with a cluster job this morning.

Fixing output for EOF token in parser errors

also a fix for a system test related to ParserBuilder

unit test fixes for new NodeManager constructor (related to previous two trunk commits)

parser/driver fixes for last commit

partial merge from portfolio branch, adding conversions (library-internal-only of course) between Exprs and Nodes, Types and TypeNodes, ExprManagers and NodeManagers.

reverting back the minisat code and adding a simpler one that shouldn't change the search

Three things:
1. Infrastructure for unit T-conflicts added to SAT proxy
   (and also the theory output channel documentation);
   previously theories could not communicate unit T-conflicts
   with the SAT layer because that layer had an implicit
   assumption (not asserted) that the conflict nodes were an AND.
2. UF now pre-rewrites trivial equalities to "true".  These could
   conceivably occur in artificial benchmarks in this form:
     (let (?x BIG-HUGE-TERM) ... (= ?x ?x) ... )
3. The SMT-LIBv2 printer now properly prints Bool constants.

fixing an uninitialized literal variable

adding support for unit conflicts in minisat...

fix compiler warning in non-replay builds

cache the LET rewriting (and defined-function expansion too)---it wasn't before, leading to terrible slowdown on heavily-nested LETs (and defined functions)

add disequality token ("/=") and rules to CVC parser

another small fix to "make dist" that can lead to a misconfigured tarball

Transitive closure module is working

fix "make dist" issues in makefiles

merge from replay branch

Add -lprofiler when --with-google-perftools is offered; also fix some newswire-raised documentation issues.

changing the sat solver to assert propagated literals back to the theories

Added util class

Made Valuation::getValue() and Valuation::getSatValue() const.

Memory fix for congruence closure; affects many UF benchmarks, probably AX too.

Added options for setting the random decision frequency and random seed for the sat solver.  Also added command line options for setting both.

Minor adjustments to the Registrar commit in 1644, documentation.

Merging the satliteral-before-prereg branch into trunk. Theory preregistration is now called during the conversion to cnf. This fixes bug 257.

Reverts previous commit r1636.

Add documentation to Node and TNode (closes bug #201).
Also, only build doxygen documentation on stuff in src/,
not test/ or contrib/ or anywhere else.  Hopefully this
turns our 3000+ page user manual into something a little
more useful!

Delayed the addition of unate propagation lemmas until propagation is called.  The OutputChannel is now untouched by TheoryArith during preregistration.

with --with-google-perftools, don't just take it on blind faith, require a successful link at configure time

minor fixes

minor bugfixes (fixes broken dynamic-library build from last night)

documentation fix

This commit is a merge from the "betterstats" branch, which:

* Makes Options an "omnipresent thread-local global" (like the notion
  of the "current NodeManager" was already).  Options::current() accesses
  this structure.
* Removes Options from constructors and data structures everywhere
  (this cleans up a lot of things).
* No longer uses StatisticsRegistry statically.  An instance of the
  registry is created and linked to a NodeManager.
* StatisticsRegistry::current() is similar to Options::current(), but
  the pointer is stowed in the NodeManager (rather than stored)
* The static functions of StatisticsRegistry have been left, for backward
  compatibility; they now use the "current" statistics registry.
* SmtEngine::getStatisticsRegistry() is a public accessor for the
  registry; this is needed by main() to reach in and get the registry,
  for flushing statistics at the end.

Fixes to Valuation.

improve recent low-coverage complaints

adding CVC4:: qualifier to the #define for debugging so that it can be used outside of CVC4 namespace (like minisat)

Moved the constructor for Options out of the header and into the cpp. For people who fiddle with default values set by the Options constructor, this will require significantly less recompiling.

Added the command line flag --rewrite-arithmetic-equalities.  This sets a static flag in Options that the ArithRewriter uses to determine the equality rewriting policy.

Add Valuation::getSatValue() so that theories can access the current
(propositional) assignment for theory atoms.

Fixed Debug/Trace as discussed in bug ticket #252 and on the mailing list.
This implementation leads to some compiler warnings in production builds,
but these will be corrected in coming days.  There appears to be a small
speedup in the parser as a result of this fix:

  http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=1902&reference_id=1886&p=5

Cleaned up a few CD Boolean attribute things.

Various small fixes to coding guidelines / test coverage.

This commit:
* Resolves bug 252 (tracing not disabled in production builds)
* Resolves bug 254 (implement CDAttrHash<>::BitIterator::find())

Merged the branch sparse-tableau into trunk.

fixes to attribute-internals warnings on 64-bit; also some GCC function attribute cleanup; nothing major

fix for bug 253, was propagating an asserted literal
also fixing some compile warnings in attributes

fix typo

This is a merge from the "theoryfixes+cdattrhash" branch.  The changes
are somewhat disparate but belonged on the same branch because they were
held back from trunk all for the same reason (to keep the trunk stable
for furious bitvector development).  Dejan has now given me the go-ahead
for a merge.

=========================================
THIS COMMIT CHANGES THE THEORY INTERFACE!
=========================================

Theory constructors are expected to take an additional "Valuation*"
parameter that each Theory should send along to the base class
constructor.  The base class Theory keeps the Valuation* in a
d_valuation field for use by it and by its derived classes.
Theory::getValue() no longer takes a Valuation* (it is expected
to use d_valuation instead).  This allows other theory functions
to take advantage of getValue() for debugging or heuristic
purposes.

TODO BEFORE MERGE TO TRUNK:
****implement BitIterator find() in CDAttrHash<bool>.

Specifically:

* Added QF_BV support for SMT-LIB v2.
* Two adjustments to the theory interface as requested by Tim King:
  1. As described above.
  2. Theories now have const access to the fact queue through base
     class functions facts_begin() and facts_end(); useful for
     debugging.
* Added an "Asserted" attribute so that theories can check if something
  has been asserted or not (and therefore not propagate it).  However, this
  has been disabled for now, pending more data on the overhead of it, and
  pending discussion at the 3/25/2011 meeting.
* Do not define NDEBUG in MiniSat in assertion-enabled builds (so
  that MiniSat asserts are evaluated).
* As a result of the new MiniSat assertions, some --incremental
  regressions had to be disabled; also, some bitvectors ?!!
* Bug 71 is resolved by adding a specialization for CDAttrHash<> in the
  attribute package.
* Fixes for some warnings flagged by clang.
* System tests have arrived!  So far mainly infrastructure for having
  system tests, but there is a system test aimed at improving code
  coverage of the printer package.
* Minor other adjustments to documentation and coding to be more
  conformant to CVC4 policy.

Tests have been performed to demonstrate that these changes have no or
negligible effect on performance.  In particular, changing the
CDAttrHash<> doesn't have any real effect on performance or memory right
now, since there is only one context-dependent boolean flag (as soon
as another is added, the effect is noticeable but probably still slight).

Fix for a bug Andrew Reynolds found for iterators that affects empty CDList<> objects that allocate from ContextMemoryAllocator<>.  Iterators were broken in that begin() != end() for empty lists (again---only those that allocated space from ContextMemoryAllocator<>).  Added a unit test for this, too.  Thanks Andy!

Merges the small changes on the queue-period branch into trunk.  This branch importantly removes an unintentional line of code that had it pivoting more times than intended before rechecking the queue. Importantly, it does this without losing any examples with rewrite-equality enabled. This adds a parameter NUM_CHECKS which determines how many times the queue chould be checked during difference mode.  A value of 10 for NUM_CHECKS has been empirically determined to be good in practice. See jobs 1815, 1824, 1825, 1821, 1814.

updating debug output usage to eliviate impact of bug 252

more bugfixes, some basic propagation, and testcases to cover them

fixing a bug in the BV rewrite, off by one error when merging constants

again a typo

more bugfixes for bitvectors

fixing the failure from last nigth, due to using a reference to an element in a growing vector

missed one case

commit for the version of bitvectors that passes all the unit tests