additional stuff for sharing,

fixes for uf/equality engine from the quantifiers branch. mainly backtracking issues.

this should fix the build; doxygen documentation now gets built in srcdir/doc/doxygen

Disable a warning to address bug 277.  (This doesn't really resolve the issue, but the warning isn't dangerous here.  See the bugzilla comments.)

removing an assert i forgot to remove that andy found

Merge from my post-smtcomp branch.  Includes:

Dumping infrastructure.  Can dump preprocessed queries and clauses.  Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc.  For a
full list of options see --dump=help.

CUDD building much cleaner.

Documentation and assertion fixes.

Printer improvements, printing of commands in language-defined way, etc.

Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.

CVC3 compatibility layer (builds as libcompat).

SWIG detection and language binding support (infrastructure).

Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).

Copyright and file headers regenerated.

Ensure that assignment gestures through CDMap iterators like:

  (*myCDMap.find(foo)).second = bar;

fail with a compile-time error (rather than being silently ignored, like
they had been).

Resolves bug #276.

Partial merge of integers work; this is simple B&B and some pseudoboolean
infrastructure, and takes care not to affect CVC4's performance on LRA
benchmarks.

* Changing pre-registration to be context dependent -- it is called from the SAT solver on every backtrack
* Updated UF to handle the context dependent pre-registration
* Additionally some small changes in order to satisfy warnings of the eclipse code analysis tool

Fixin the SAT solver for Andy. Even if a SAT lemma is added, a FULL-CHECK will be reissued. Some unexpected slowdowns, but not too much.

Removing Theory::registerTerm() as discussed in the meeting. Now pre-register is called on all the theory terms and the foreign-terms also. This means, if x: REAL and f:REAL, that in f(x) >= 0, arithmetic gets pre-register call with x, f(x) and f(x) >= 0, while UF gets pre-register call with x, f(x).

Fixing the broken unit tests

Simplification of the preregister and register throught a NodeVisitor class. The theoryOf is not all in one place, theory::theoryOf. The uninterpreted sorts belong to the builtin theory and are dispatched to the apropriate theory (QF_UF, QF_AX) through theoryOf based on the setting in the Theory class.

some uf cleanup

new implementation of lemmas on demand
comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637>

forgot to reflect naming change in makefile.  fixed

fix bug 272, array unsoundness, and some array cleanup

remove some array regressions from "make check" so nightly regressions run

status of examples

new array bugs ?

fixing out of place typename (error on g++ 4.4.3-4ubuntu5)

submission script

Adding static_fact_manager

Clark's work on array theory - can now solve all QF_AX problems

fix some confusing debug output (bogus counter)

mark the new minimized benchmark as unsat

if running in QF_AX, equalities over terms of uninterpreted sort go to arrays, as well as pre-registration of free constants of uninterpreted sort, etc..

minimized example

array benchmarks

adding disequality propagation

relevant comparison http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2602&reference_id=2590&p=5

merge from symmetry branch

Reverting mistaken check-in

changing the sat solver remove clauses constants
with these we get closer to yices on uf and it seems better on lra

vs yices uf http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2590&category=&p=5&reference_id=1471
vs trunk on lra http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2591&category=&p=5&reference_id=2576

Fixed bug in default solve - wasn't returning when it was supposed to

another typo

yet another uf bug fix, hopefully the last

another bugfix for uf

some immediate bug fixes

fix submission makefile

minor fixups

surprize surprize

removing duplicate clauses in ite cnf conversion

cudd-building prefs with --with-cudd / --without-cudd

Fixing two bugs:

1) arithmetic should check for subterms when solving equations, for instance x = if b then x + 1 else x -1 is not a valid substitution
2) a memory problem in minisat - explanations are constructed during conflict analysis, so the clause database might resize and relocate, which invalidates any references to clauses

missing test case

updated preprocessing and rewriting input equalities into inequalities for LRA

Allow (- x) for unary minus in SMT-LIBv1, in addition to the standard (~ x),
when --strict-parsing is off (which it is by default).  The danoint benchmarks
have such monsters.

Changed the defaults for arithPivotThreshold and arithPropagateMaxLength to 16. Enabled arithmetic propagation and variable removal by default. Changed the command line arguments for both propagation and variable removal allow for disabling these.

Merging the playground branch upto r1957 into trunk.

only use theory registration if (1) a theory requests it, or (2) if there's more than one "real" theory (not BUILTIN or BOOL) active

some things I had laying around in a directory but never got committed; minor fix-ups to documentation and some node stuff

Fixed spelling mistake and documentation for --enable-variable-removal.

Some fixes inspired by Fedora 15:
* compilation fixes for GCC 4.6.x
  + ptrdiff_t is now in std::
* fix some make rules that are ok in Make 3.81 but broke in Make 3.82
* look for cxxtestgen.py as well as cxxtestgen.pl, and look for cxxtest headers in /usr/include

compilation fix for x86 (from previous commit)

Fix for Mac OS breakage (x86 didn't crash, but probably would, eventually, on some problems---valgrind gave many complaints): the problem was that calloc() (in the Backtracker) wasn't allocating enough space for the type located at the resulting address.  Resolves bug #263.

Also, some debugging improvements.

fixed various bugs related to ambiguous parametric datatype constructors, parametric datatype versions of paper benchmarks are now working

datatypes work

minor fix to build system for system tests

added (temporary) support for ensuring that all ambiguously typed constructor nodes created internally are given a type ascription

minor fix, and better output for type errors

type ascriptions (casts) for parameterized datatypes, e.g. "nil :: list[INT]

This commit contains the code for allowing arbitrary equalities in the theory of arithmetic.
* This code has been partially tested. (My testing situation is currently not so great.)  The code for testing not preregistering equalities can be compile time enabled by setting the boolean turnOffEqualityPreRegister. Don't be shocked by slowdowns or failures.  This does pass make regress as well as a fresh checkout does. (The Mac version has issues.)
* I need to disable the permanent row removal heuristic by default.  We need to discuss why this needs to happen.  We should probably detect pure QF_LRA/QF_RDL problems and enable this when this can safely be done.
* I have disabled the arithmetic rewrite equality flag.  This code needs to be added to the parser.
* For all of the above changes, I have annotated the code with the key word BREADCRUMB.
* I have renamed ArithUnatePropagator to ArithAtomDatabase.

fix unit test linking issue

include subversion information used for each build in the --show-config output and as a banner in --interactive mode; intended to resolve confusion in cases where you don't know where a CVC4 binary came from

apply arithmetic static learner's miplibtrick in a consistent order (for easier replication of experiment)

fixes for "make dist" and "make doc", minor cleanups

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