fix for de+lemmas

for the first time make regress passes even if JH is enabled

This commit merges in the branch branches/arithmetic/congruence into trunk. Here are a summary of the changes:
- Adds CDMaybe and CDRaised in cdmaybe.h
- Add test for congruence over arithmetic terms and constants
- Renames DifferenceManager to CongruenceManager
- Changes a number of internal details for CongruenceManager

Merge from decision branch -- partially working justification heuristic

Overview of changes
* command line option --decision={internal,justification}
* justification heuristic handles all operators except ITEs
  revelant stats: decision::jh::*
* if decisionEngine has solved the problem PropEngine returns
  unknown and smtEngine queries DE to get the answer
  relevant stat: smt::resultSource
* there are known bugs

Full list of commits being merged
r3330 use CD data structures in JH
r3329 add command-line option --decision=MODE
r3328 timer stat, other fixes
r3326 more trace
r3325 enable implies, iff, xor (no further regression losses)
r3324 feed decision engine lemmas, changes to quitting mechanism
r3322 In progress
r3321 more fixes...
r3318 bugfix1 (69 more to go)
r3317 Handle other boolean operators in JH (except ITE)
r3316 mechanism for DE to stopSearch
r3315 merge from trunk + JH translation continuation
r3275 change option to enable JH by default[A

Updates to array theory - much more lazy about introduction of reads
Also disabled eager lemmas - slows down QF_AX but gets new examples in QF_AUFBV

In the constructor of DecisionEngine, there were 2 pointers that were assumed to be initialized to NULL. This is not true on all platforms. This is now done explicitly.  Macs builds should now work again.

add the missing BINARY variable in some test/regress makefiles

cout -> warning. Happening in portfolio
rest of the search go through, but still should be investigated

disabling the problematic pragma in node_manager.h on gcc < 4.6 until we figure out what to do with it

Fix for thos annoying "array index" warnings in production builds

A dummy decision engine. Expected performance impact: none.

Adds DecisionEngine and an abstract class DecisionStrategy
which other strategies will derive from eventually.

Full revision summary of merged commits:
r3241 merge from trunk
r3240 fix
r3239 WIP
r3238 JH, CVC3 code: 5% done -- 5% translated
r3237 JH groundwork
r3236 make make regrss pass
r3234 hueristic->heuristic
r3229 JustificationHeuristic: EOD-WIP
r3228 DecisionEngine: hookup assetions
r3227 move ITE outside simplifyAssertions
r3226 DecisionStrategy abstract class
r3222 DecisionEngine: begin

Merges branches/arithmetic/atom-database r2979 through 3247 into trunk.  Below is a highlight of the changes:
- This introduces a new normal form to arithmetic.
-- Equalities and disequalities are in solved form.
   Roughly speaking this means: (= x (+ y z)) is in normal form.
   (See the comments in normal_form.h for what this formally requires.)
-- The normal form for inequality atoms always uses GEQ and GT instead of GEQ and LEQ.
   Integer atoms always use GEQ.
- Constraint was added to TheoryArith.
-- A constraint is a triple of (k x v) where:
--- k is the type of the constraint (either LowerBound, UpperBound, Equality or Disequality),
--- x is an ArithVar, and
--- v is a DeltaRational value.
-- Constraints are always attached to a ConstraintDatabase.
-- A Constraint has its negation in the ConstraintDatabase [at least for now].
-- Every constraint belongs to a set of constraints for each ArithVar sorted by the delta rational values.
-- This set can be iterated over and provides efficient access to other constraints for this variable.
-- A literal may be attached to a constraint.
-- Constraints with attached literals may be marked as being asserted to the theory (sat context dependent).
-- Constraints can be propagated.
-- Every constraint has a proof (sat context dependent).
-- Proofs can be explained for either conflicts or propagations (if the node was propagated). (These proofs may be different.)
-- Equalities and disequalities can be marked as being split (user context dependent)
- This removes and replaces:
-- src/theory/arith/arith_prop_manager.*
-- src/theory/arith/atom_database.*
-- src/theory/arith/ordered_set.h
- Added isZero(), isOne() and isNegativeOne() to Rational and Integer.
- Added operator+ to CDList::const_iterator.
- Added const_iterator to CDQueue.
- Changes to regression tests.

Fixed bug in sharing with arrays of different types

Fix SExpr name qualification for swig, and #include integer and rational headers.

svn ignore Makefile.in for aufbv regression directory

Adds an operator<< to SExpr::SexprTypes. This fixes bug 317. In debug builds, an Unhandled(SExpr::SexprTypes) could not compile on debian.

merge from arrays-clark branch

* Smt2 printer for datatypes
* Fix DefineFunctionCommand when a constant is defined

* Fix ITEs and functions in CVC language printer.
* Permit "BOOL = BOOL" in CVC language parser (auto-replaced with IFF
  internally, except in strict mode).
* SExpr atoms now can be string-, integer-, or rational-valued.
* SmtEngine::setInfo(":status", ...) now properly dumps a
  SetBenchmarkStatusCommand rather than a SetInfoCommand.
* Some dumping fixes (resolves bug 313)

fix distributed builds (and therefore the Debian nightly build) by ignoring Makefile.am files under src/prop/cryptominisat.

processing assertions in bit-vectors even when in fullcheck (needed for sharing)

Support to test the "dumper" mechanism in regressions (feeding dump output back in) by doing "make regress RUN_REGRESSION_ARGS=--dump"

some settings in bvminisat

changed BVMinisat options to use cc_min=0 in propagate only calls and cc_min=2 in solve

changed ccmin_mode in BvMinisat

   * added propagation as lemmas to TheoryBV:
   * modified BVMinisat to work incrementally
   * added more bv regressions

Fix for make dist.

Fix for broken unit tests from the previous commit.

- Merged in the branch cdlist-cleanup.
- This adds a CleanUp template argument to CDList.
- CDChunkList<T> replaces the CDList specialization for ContextMemoryAllocator.
- CDVector<T> has been simplified and improved.
- The expected performance impact is negligible.

fix for cvc4_logic dump

Removing large and unused regress2 benchmarks to decrease the size of checkouts.

some more build system fixes

fixing some build systme warnings

Fix for bug 316. If the flag @CVC4_TLS_SUPPORTED@ is false, function pointers cannot be directly used with the CVC4_THREADLOCAL macro. This is why there were problems on macs.

Fixes a linking problem with the new SatSolverConstructor on Mac.

bringing cryptominisat into the main branch

enabling the --disable-arithmetic-propagation option in the arithmetic code (it wasn't used)

fix swig-ignored interface name; hopefully fixes Debian package nightly builds

Update to the ArithRewriter to remove REWRITE_AGAIN_FULL and limit REWRITE_AGAIN calls.

Some renaming and refactoring in SAT

getting rid of a rewrite in uf sharing, speeds things up a bit

fixed faulty bv rewrite rule

adding an extra cache check in the rewriter, speeds things a bit
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3828&category=&p=5&reference_id=3820

Global registry of SAT solvers, where they are registered at compile time. The available SAT solvers can be seen with the --show-sat-solvers option.

More cleaning up.

more datail from the build failure

with a small fix

forgot to commit this one, fixing build errors

moving minisat implementation into their respective directories (regular and bv)

sat_module.h,cpp -> sat_solver.h,cpp (as intended)

sat.h,cpp -> theory_proxy.h,cpp (this is what it defines)

a cute script to make a video of development from the svn logs

Removed the variableRemovalEnabled option and d_removedRows from TheoryArith.  This had been disabled for several months.

* improving arithmetic getEqualityStatus
* some sharing improvements based on model

Merged updated version of the bitvector theory:
  * added simplification rewrites

some improvements to the sharing mechanism/interface

Disable nonclausal simplification for QF_SAT benchmarks by default.
(Can be overridden with --simplification=batch, for example.)

Some work on the dump infrastructure to support portfolio work.

  Dump("foo") << FooCommand(...);

now "dumps" the textual representation of the command (in the current
output language) to a file, IF dumping is on at configure-time, AND the
"muzzle" feature is off, AND the "foo" flag is turned on for the dump
stream during this run.

If it's a portfolio build, the above will also store the command in a
CommandSequence, IF the "foo" flag is turned on for the dump stream
during this run.  This is done even if the muzzle is on.

This commit also cleans up some code that used the dump feature (in arrays,
particularly).

fix a "lost command" bug and associated memory leak in SMT-LIBv1 parser due to an out-of-place parenthesis

Strengthen minisat assertion regarding t-propagations that was unintentionally allowing a theory to propagate p and ~p at the same time (and the conflict was undetected, leading to an incorrect answer).  Credit to Clark for finding this.

minor fixes: to "make dist" in build directories with language bindings enabled; and to makefile standards conformance

fix "make dist"

Fixin the bug Clark found. In final check, enqueued propagations were not discharged.

Removing QUICK_CHECK, and other unused ones, from the Theory::Effort.

Seems to be working better <http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3749&category=&p=5&reference_id=3739>, and should fix the failing cases in the regressions.

Removing one test case from the integer regress0.

cdqueue : fix size(). Thank you Clark for spotting this silly mistake.

fix some Java compatibility-layer interface problems; also fix some Mac OS X build issues

updating the equality engine to be able to give explanations for terms that were not in the databas (queried by areEqual and areDisequal)
and it's a bit better
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3738&category=&p=-1&reference_id=3731

Changing the dependency checking; GMP is required (and sometimes must be explicitly linked in with -l) when using CLN.  Fixes a bug on recent Debian that Francois reported.  Hopefully this doesn't break anything..

Remove some commented out code from sat.h

This commit merges in the changes from branches/arithmetic/refactor0
- Improved the checks in AssertLower and AssertUpper so that redundant bounds cause less work.
- Because of the above change, d_constantIntegerVariables now cannot have duplicate elements enqueued. This allows removing d_varsInDioSolver.
- Fix to an assertion in CDQueue.
- Implements a CDArithVarSet using a vector of booleans and CDList.
- Refactored ArithVar out of arith_utilities.h. Miscellaneous cleanup of arithmetic.

CDMap -> CDHashMap
CDSet -> CDHashSet

committing the TNode/Node fix that was in the kind-backend branch; there's still something fishy here, I think I need to merge in a few more things to support incrementality properly.  But this fixes "make check" for now

Renamed CDQueue to CDTrailQueue and CDQueue2 to CDQueue. Small changes to function names and documentation.

Partial merge from kind-backend branch, including Minisat and CNF work to
support incrementality.

Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.

Expected performance change negligible; slightly better on memory:
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!

cdqueue2 : cdlist that can be used like queue and can delete element that will never be restored

Fixed a copy paste error where a lower bound was looked up instead of an upper bound.

This should fix the debian build fails:
   * removed bvpicosat directory as it is currently not used

Cleared some of the flurry of warnings my previous merge caused in src/prop/

fixing bug310

* theories that are parametric and therefore need the combination framwork should be tagged as "parametric" in the kinds file
* default care graph computation was not sufficient, fixed

consistency in how the Dump output stream is used

This commit merges in branches/arithmetic/internalbb up to revision 2831.  This is a significant refactoring of code.

- r2820
-- Refactors Simplex so that it does significantly fewer functions.
--  Adds the LinearEqualityModule for handling update and pivotAndUpdate and other utility functions that require access to both the tableau and partial model.
-- Some of the code for propagation has moved to TheoryArith.
-r2826
-- Small changes to documentation and removes the no longer implemented deduceLowerBound() and deduceUpperBound().
- r2827
-- Adds isZero() to Rational. Adds cmp to DeltaRational.
- r2831
-- Refactored comparison to upper and lower in the partial model to use DeltaRational::cmp.
-- Refactored AssertUpper and AssertLower in TheoryArith to include functionality that has weaseled into TheoryArith::assertionCases.

Improves the arithmetic difference manager to delay any work until a shared term is added.

fix theory "kinds" file documentation for allowed arity of operators

Adds the CDQueue class.  This is a wrapper for combining a CDList<T> and a CDO<size_t> into a FIFO queue.

Replace the sequence of hardcoded addTheory() calls with a use of the theory traits---with the effect that everything with a kinds file is registered as a theory.  Eventually we may want a more dynamic way of selecting theory implementations, but for now we don't have a need for this.  Expected performance impact: none.  (This commit addresses and re-closes the reopened bug #307.)

fixes to new-theory script; resolves bug #307

ppAsert -> ppAssert

Refactored CnfStream to work with the bv theory Bitblaster:
    * separated SatSolverInput interface class into two classes:
           - TheoryProxy for the sat solver to communicate with the theories
           - SatSolverInterface abstract class to communicate with the sat solver
    * instead of using #ifdef typedef for SatClauses and SatLiterals, now there are CVC4 SatLiteral/SatClause types and mappings between them and the internal sat solver clause/literal representation
    * added abstract classes for DPLLSatSolver and BVSatSolver different interfaces

Replaced TheoryBV with bitblasting implementation:
    * all operators bitblasted
    * only operator elimination rewrite rules so far

Theory interface changes:

solve -> ppAsert
staticLearning -> ppStaticLearn
preprocess -> ppRewrite
SolveStatus -> PPAssertStatus (SOLVE_* -> PP_ASSERT_*)

via Eclipse refactoring magic.

Added ability to set a "cvc4-specific logic" in standards-compliant
SMT-LIBv1 and SMT-LIBv2 input:

    In SMT-LIBv1, you specify the "cvc4_logic" benchmark attribute; for instance:

    (benchmark actually_a_sat_benchmark_but_looks_like_uf
      :logic QF_UF
      :cvc4_logic { QF_SAT }
      [...]

    In SMT-LIBv2, you use a set-info; for instance:

    (set-logic QF_UF)
    (set-info :cvc4-logic "QF_SAT")
    [...]

    Right now, the only thing this does is disable the symmetry breaker for
    benchmarks like the above ones.

As part of this work, TheoryEngine::setLogic() was removed (the logic field there
wasn't actually used anywhere, its need disappeared when
Theory::setUninterpretedSortOwner() was provided).

Also, Theory::d_uninterpretedSortOwner got a name change to
Theory::s_uninterpretedSortOwner, to highlight that it is static to the Theory
class.  This represents a breakage of our separation goals for CVC4, since it
means that two SmtEngines cannot be created separately to solve a QF_AX and
QF_UF problem.  A bug report is pending.

pcvc4 only built if --with-portfolio given to the configure script (Clark-requested change)

Fix for bug 305.

fixes to configure and boost.m4 to make certain boost installations nonfatal errors; threading support should only be required to build pcvc4, not cvc4

another static library unavailability issue

make sure to clear out READLINE_LIBS if readline causes problems at configure time; fixes a bug reported by Clark for static-binary builds on machines where no static libreadline is available (like CIMS machines)

Added OutputChannel::propagateAsDecision() functionality, allowing a theory
to request a decision on a literal.  All these theory requests are kept in a
context-dependent queue and serviced in order when the SAT solver goes to make a
decision.  Requests that don't have a SAT literal give an assert-fail.  Requests
for literals that already have an assignment are silently ignored.

Since the queue is CD, requests can actually be serviced more than once (e.g., if
a request is made at DL 5, but not serviced until DL 10, and later, a conflict
backtracks to level 7, the request may be serviced again).

Performance impact: none to negligible for theories that don't use it
  See http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3620&reference_id=3614&mode=&category=&p=0

Fixes to documentation / fixes for MacOS

minor change to order fn in sat solver's ElimLt
(better, (marginally) faster -- regressions 3605, 3606)

add a "--with-portfolio" configure option that makes a missing boost-thread library an error; useful for builds requiring a "pcvc4" binary at the end

fix src/util/hash.h to specialize GNU's hash template for <uint64_t> on platforms that need it; fixes Mac builds.

language bindings fixes for yesterday's portfolio merge

Fix for bug303. The problem was with function applications that get normalized when added to the term database. For example, if x=y exists, and the term f(x) is added, f(y) was stored. So, when getExplanation(f(x), f(y)) was called, trouble ensued. I now keep the original version so that explanations can be properly produced.

Also added theory::assertions debug flag that will printout assertions of each theory for ease and uniformity of debugging in the future.