Clean up Theory base class as per code review bug #60; also fixes to CodeTimer statistic, and adding a CodeTimer to TheoryEngine::EngineOutputChannel::newFact() for investigation into (possible) slow or redundant theory registration.

- Merges queue-interrogation branch into the trunk. This branch adds extra phases of looking for additional conflicts during and after the heuristic pivoting stage. (For the expected performance gain, comparing jobs 1676 and 1643 gives a rough idea.)

Merges branches/arithmetic/tableau-reset into the trunk.  The tableau is now heuristically reset to its initial state during restarts.

- Adds PermissiveBackArithVarSet.  This is very similar to ArithVarSet. The difference is that set.isMember(x) for an ArithVar x s.t. x > set.allocated() returns false for PermissiveBackArithVarSet and is an assertion failure for ArithVarSet.  This cuts down on the memory usage of the ColumnMatrix slightly.

Enables the PreferenceFunction minBoundAndRowCount.

- Adds "PreferenceFunction" to SimplexDecisionProcedure.  A PreferenceFunction allows for specifying how to choose between two nonbasic variables for which should become basic during the selectSlack(...) function. This partially addresses a point brought up by Dejan during the Code Review.  (Unfortunately, function pointers are involved in the implementation. Because of this, I have had Morgan review this code before check-in.)

- Made Rational::sgn() function const.

adding three features to CVC parser that drastically improve its support for the language: LET now supported (but not "type-lets" yet), OPTION now supported, and ^ operator (exponentiation) supported for nonnegative integer exponents.  The latter simply expands to MULT, and of course fails assertions in arithmetic if a variable is raised to n >= 2.  Also other CVC parser clean-up.

fix for bug #244, "Segfault if file cannot be found and --stats is on"

- Creates a queue for lemmas discovered during the simplex procedure. Lemmas are sent to the sat solver during theory propagation. The lemmas currently come from additional conflicts that are discovered by findConflictOnTheQueue(...).

resurrecting triple.h from r1023 (after which it was removed)

Merged the tableau-copy branch into trunk. This adds a copy constructor and operator=(...) to Tableau.

fixing a type that caused the segfaults in the regressions

fixing the big with lemma reallocation in minisat garbage collection

CongruenceClosure module now should support nullary congruence operators (now that they are allowed for the datatypes theory, as in (APPLY_CONSTRUCTOR nil) or (APPLY_CONSTRUCTOR zero)).  It does this by treating such terms with zero children as non-candidates for congruence, even though they have the congruence kind APPLY_CONSTRUCTOR.

Review of mktheorytraits, mkrewriter, and recent changes to other mk* scripts.  Minor changes only, correcting some documentation and fixing some warnings that were being issued about functions not existing.

minor doxygen build target fixes

Review of statistics code.  Added lots of documentation, and fixed an issue (I think) that Tim found with TimerStat involving wild, sometimes negative, timer statistic values.  (It was due to improper initialization.)

- Adds a path for Theory to be passed a reference to Options.
- Adds 3 choices of heuristic variable orders to use in ArithPriorityQueue.
- Adds the pivot-rule command line option.

- Makes VarCoeffPair a class instead of a typedef of pair<ArithVar, Rational>.  This addresses a point Dejan brought up in the code review.

- Adds a buffer to the ReducedRowVector addRowTimesConstant operation to reduce the number of allocations made.  Compare cluster jobs 1585 and 1584 for the expected performance increase.

- Merged RowVector and ReducedRowVector.
- Renamed NonZeroIterator to const_iterator.
- Both of these changes are in response to the code review.

Commit to fix bug 241 (improper "using namespace std" in a header).  This caused a number of latent errors in sources and headers to come up.  Those are now fixed (by adding "using" or "std::" depending on the context).  Took the opportunity to bring many rewriter sources in line with coding conventions.

Merge from theory-break-dependences branch to break Theory and TheoryEngine dependences; now, if you touch theory_engine.h, only a few things in theory need be recompiled (TheoryEngine, SharedTermManager, .... but no theory implementations), along with the PropEngine and SmtEngine.  If you touch a specific theory's .h file, only that theory must be recompiled (along with the TheoryEngine, since it uses traits, and SmtEngine, since it tells the TheoryEngine which theory implementations to use).

fix serious regression breakage (segfaults) caused by an off-by-one error in initialization of the expression variable statistics in last commit

adding the variables count to the statistics in the expr manager

adding statistics about how many different kinds of expressions we have created in the expression manager.
this is useful, for example, with --parse-only, to figure out a bit of problem structure

- This commit adds some debugging information to ArithPriorityQueue.
- There was a missing break statement in ArithPriorityQueue. This addresses the bug discovered in the debug regression (http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=1566&reference_id=1548&category=1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,29&p=10).

slicing manager is not breaking the old regressions, time to sync

- Adds an additional round of checks for a conflict after the difference heuristic round has been completed.  This happens immediately before switching to the variable order round.

- Adds an additional mode to ArithPriorityQueue, Collection. Collection is a mode where the heap structure is not maintained.  There is just a list of variables that may be inconsistent. This is used up until the simplex procedure is invoked.
- Misc. cleanup and renaming in ArithPriorityQueue.

- Changes ArithPriorityQueue to use stl::vector<>'s plus stl's heap algorithms instead of stl's priority queue (which is really an stl vector plus the stl heap algorithms).  This offers more control of the underlying data structure.

- Adds column based iterators.

- Adds the ArithPriorityQueue class. The ArithPriorityQueue class provides an abstraction to the previous priority queues representing the 2 different pivoting rules.

- Adds the statistic d_avgNumRowsNotContainingOnPivot.
- Removed a bug in row counting in row counting.

Changes:
- The Tableau is now in charge of managing what variables are basic in a unified manner. Specifically, TheoryArith::d_basicManager was merged into Tableau::d_basicVariables.

Changes:
- ArithVar is no longer an attribute
- RowVector's destructor reduces the row count of its variables upon.
- Tableau's destructor now free its rows instead of leaking memory.
- Added ability to convert ReducedRowVectors into equivalent Nodes.
- getValue() should work again.

This commit merges the branch branches/arithmetic/quick-row-has into trunk. quick-row-has has an optimization to make checking if a variable is in a row faster.

This commit is the promised clean up after removing row ejection.

Removed ActivityMonitor from arithmetic. This was only used for row ejection, and is now superfluous.

Row ejection is now completely disabled. Another commit cleaning this one up will follow shortly.

Removed vestigial normal form notes file from src/theory/arith/Makefile.am. Should have been removed earlier.

some unit tests to work on slicing

I replaced the pattern "x = x + y;" with "x += y;" in a few places in DeltaRational. This addresses a point that came up in the code review.

Updates based on the group code review of arithmetic on 2011-02-15.  The only substantive change is that UnatePropagator no longer uses attributes. The rest is comments and other beatification.

Deleting depricated files.

getting ready for slicing bitvectors

Overview of the changes:
- Preparing to remove row ejection from the code base!
- Checks for conflicts immediately after a pivot to avoid potentially wasteful search.
- Added arithvar_set.h. This replaces ArithVarSet that was previously in the Tableau, and ArithVarDenseSet.
- Removes variables that have no preregistered bounds during presolve().
- Theory::isLeafOf() currently returns true for atoms. (I was unaware.) I modified Variable::isMember() to account for this exclude atoms.
- Added statistics all over the place.

This commit effects both boolean search and simplex search so expect running times to go all over the place. The time differences should be roughly as follows:
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=1486&reference_id=1447&p=10&category=1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,29

updates for the rewriter, added some statistics

Reverses the order of the d_possiblyInconsistent queue. (It is that old termination bug again. *le sigh*)

3 heuristics were added to arithmetic. A heuristic for detecting an encoding of min added to static learning in LRA. A heuristic added for when the true branch and false branch are both constants (also in static learning). A heuristic for checking whether any variables begin in conflict before pivoting.

fix for build errors

Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.

tls.h, rational.h, and integer.h are only re-generated if changed.  this obviates the need for a full rebuild just because you re-./configured.

minor fixes for correct doxygen output

make some CC module methods private that should not have been public

congruence closure module now supports things other than APPLY_UF; ported from "arrays" branch to trunk

permit PARAMETERIZED operators to be zero-ary

fix to static learning application in UF, resolves bug# 239

Changin the get() semantics to a CDQeue-sque semantics.

Merge from ufprop branch, including:

* Theory::staticLearning() for statically adding new T-stuff before
  normal preprocessing.  UF's staticLearning() does transitivity of
  equality/iff, solving the diamonds.

* more aggressive T-propagation for UF

* new KEEP_STATISTIC macro to hide Theories from having to
  register/deregister statistics (and also has the advantage of
  keeping the statistic type, field name, and the 'tag' used to output
  the statistic in the same place---instead of scattered in the theory
  definition and constructor initializer list.  See documentation for
  KEEP_STATISTIC in src/util/stats.h for more of an explanation).

* more statistics for UF

* restart notifications from SAT (through TheoryEngine) via
  Theory::notifyRestart()

* StackingMap and UnionFind unit tests

* build fixes/adjustments

* code cleanup; minor other improvements

add statistics support information to --show-config

small changes to documentation; also, '\''make doc'\'' doesn't build dot graphs (but nightly build system will produce them)

fix improper CongruenceClosureWhite test by merging from a uf branch; fixes the nightly test failure

add some stats to UF/CC

The "UF engineering issues" release, after much profiling.

* swap in backtracking data structures (that use and maintain their own
  undo stack) in some places instead of the usual Context-aware
  paradigm (MUCH faster).

* cosmetic changes to UF, CC modules.

Added Theory::presolve().

SmtEngine now fails with a ModalException if --incremental is not enabled
but a push/pop or multiple query is attempted (previously it could give
incorrect answers)

Also, fix some multi-query and push-pop tests that had wrong answers, and
support a new "% COMMAND-LINE: " gesture in regression tests so that a
test can pass additional, specific command line flags it wants to run
with (here, --incremental).

Also fix mkbuilddir script for when it's called from contrib/switch-config.

fix function signatures

cleanup from today's commits: delegate as-yet-unimplemented prettyprinters in a better way; fix arith Makefile

Changes to Solver and PropEngine to support lemmasOnDemand during solve but not yet in d_checkSat.

Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printer
implemented.  This new infrastructure removes support for pretty-printing
(even in the AST language) an Expr with reference count 0.  Previously,
this was supported in a few places internally to the expr package, for
example in NodeBuilder.  (Now, a NodeBuilder cannot be prettyprinted, you
must extract the Node before printing it.)

This commit merges the arith-prop-opt branch into the main trunk. This was done by way of the intermediate branch arith-prop-tmp. Both arith-prop-opt and arith-prop-tmp will now be phased out.

minor tweaks to last commit, testing infrastructure

fix some things with the build system (make dist, make install, make check)

Some bug fixes in the SAT for lemmas, and an experiment with a more complete (wr propagation) splitter in arithmetic.

make addsourcedir executable

Lemmas on demand work, push-pop, some cleanup.

command-line flag to disable theory registration, also SMT-LIBv2 compliance (per SMT-LIB mailing list this afternoon)

cleanup, documentation, SMT-LIBv2 compliance

fix out-of-date version/copyright for minisats

Moving Options fiddling to options.h

competition mode implies --no-checking

Moving the post_mortem.py script out of contrib and into the cvc4 scripts directory.

Updates post_mortem.py script to be able to handle certain kinds of crashes and new statistics.

This commit adds the ejected and un-ejected statistics.

Adds size() to RowVector.

Adds statistics for the number of Uservariables and Slack variables used by arithmetic.

Adds AverageStat to stats.h.

small fix to debug segfaults

enable dependence graphs in doxygen; fix lots of doxygen warnings, fix some documentation, and make it possible to "make doc" on a clean source tree (post-configure)

maximize stack limit, handle SEGV signals on an alternate signal stack, and try to diagnose stack overflow

Adds a hueristic from Alberto's thesis. For a fixed window the row count is used to select which non-basic variable is a row in made basic.

Fix for a problem caused by using a != instead of == in generateConflictBelow(). Resolves a bug introduced in -r1063.

portability updates to build system

Adds a very small test that triggers a bug. The bug is from the commit for -r1063.

minor fixes as a result of review of Chris's getType() rewrite; also fix some macros to make various GCC versions happy

Fixes RowVector::has().

Factors out the QF_LRA decision procedure from TheoryArith and puts this into its own class SimplexDecisionProcedure. Implements about 1/2 of the pivoting rule from Alberto's thesis (section2.5.3).

The Row implementation has no been replaced by RowVector and ReducedRowVector.  A RowVector is an array of ArithVar and Rational pairs. (This replaces a map based implementation in Row.) ReducedRowVector is a RowVector with a notion of having a basic variable.  The Tableau is now a collection of ReduceRowVector's.  A major difference between ReducedRowVectors and Rows is that the iterator now includes the basic variable and its coefficient (always -1). Before only nonbasic members were accessible by the iterator.