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

Merges the pqueue-set branch into trunk.  During VarOrder mode and Collection mode, the arithmetic priority queue is maintained as a set. Compare jobs 1781 and 1782 for the expected performance change.

- The learned clauses from the miplib trick were being added twice. This was slowing down the search. (The effect can be seen in the difference between jobs 1765 and 1755). This happened during commit -r1480 when adding the ArithStaticLearner.  This has been fixed.

Switched SimplexDecisionProcedure::d_delayedLemmas from a vector to a queue.

SimplexDecisionProcedure no longer takes an OutputChannel as a parameter.

- Removes arith_constants.h
- Adds ArithStaticLearner.  Consolidates and cleans up the code for static learning in arithmetic.  Static learning is now associated with a small amount of state between calls. This is used to track the data for the miplib trick.  The goal is to make this inference work without relying on the fact that all of the miplib problem is asserted under the same AND node.
- This commit contains miscellaneous other arithmetic cleanup.

Adds debugging output to EngineOutputChannel::lemma.

Fix for the bug introduced in 1477.  The stuff that was added to CVC4ostream::operator<< should only be executed when d_os != NULL. This was the cause of the NULL pointer dereference in debug builds.

push and pop manipulators for output stream so that one can indent the output
ueful for me, maybe someone else finds it useful also

- Turns on the excluded middle assertions during the miplibTrick. If it is known that x \in {c_i}, then x is not in the interval (c_{i}, c_{i+1}) (assuming the c_i's are sorted). (Compare jobs 1742 and 1739 for the expected performance change on trunk. Compare jobs 1740 and 1738 for the expected performance change with the rewrite-equality patch.)

- Turns on the miplibTrick.  This detects during the static learning phase a set of nodes that are asserted to the theory of the form (=> p_i (= x c_i)). If (or p_1 p_2 ...) is a tautology, then x \in {c_1, c_2, ...}. (This tautology check currently requires CUDD to be installed.)  Right now all this does is assert x \leq max{c_i} and x \geq min{c_i}. (Compare jobs 1728 to 1626 for how this affects the miplib examples.)

real fix for bug 245, previous one was faulty

small fixes for run_regression script to workaround bug in old mktemp, was causing a hang in bug220.smt2

fix for bug 254, lemmas were propagating at lower levels, and the conflict clauses asserting literal  would overwrite the propagated literal
let's see if i break the build again

Merge from cudd branch.  This mostly just adds support for linking
against cudd libraries, the propositional_query class (in util/),
which uses cudd if it's available (and otherwise answers UNKNOWN for
all queries), and the arith theory support for it (currently disabled
per Tim's request, so he can clean it up).

Other changes include:

* contrib/debug-keys - script to print all used keys under Debug(), Trace()
* test/regress/run_regression - minor fix (don't export a variable)
* configure.ac - replace a comment removed by dejan's google perf commit
* some minor copyright/documentation updates, and minor changes to source
  text to make 'clang --analyze' happy.

adding support for google performance tools to the build sytem, it can be enabled at configure with
--with-google-perftools

to use it on ubuntu, you need to install packages google-perftools and libgoogle-perftools0

to run the profiling of the heap, you can run it for example with

HEAPPROFILE=/tmp/profile ./builds/bin/cvc4 test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.smt

this will create some files  /tmp/profile* that you can then

to get the pdf of the profile you can then run

google-pprof --pdf ./builds/bin/cvc4 /tmp/profile.0001.heap > profile.pdf

or for other options check http://goog-perftools.sourceforge.net/doc/

change to the run_regression script to better manage temporary files; hopefully this will somewhat alleviate the problem with all the junk files in /tmp

Fix to bug 251 (non-spurious warnings in builds) by shifting metakind array by 1 to handle the UNDEFINED_KIND case.

Fix bug 246 (occasional buffer overflow related to varargs in assertion-failure string construction) and addition of an assert_white unit test check for the issue

ITE removal in TheoryEngine was not properly handling PARAMETERIZED kinds.  Fixed and added bug regression.  Thanks Andrew Reynolds for the bug report!

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.