more push/pop infrastructure, some SAT stuff

fixes to incremental simplification, cnf routines, other stuff in preparation of user push/pop in SAT solver

compatibility work, documentation

build system fixes

Some base infrastructure for user push/pop; a few bugfixes to user push/pop and model gen also.
I also expect this commit to fix bug #273.

No performance change is expected on regressions with this commit, see
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863

some test fixes

another make dist fix for java compat bindings

variety of visibility fixes (should clean up some of the many warnings on MacOS-production-dynamic builds)

CVC4::Integer was not marked CVC4_PUBLIC, causing dynamic link errors on MacOS in production builds.  Fixed.

fixes for make dist ; make install

better fix for #281, also fix issue with command line options not existing on older g++en, like Apple's 4.2 on Snow Leopard.

Regular expressions in shell scripts on MacOS are inconsistent... again. :-(  Fixing a problem with Debug_tags and Trace_tags, closes bug #281

removed "typename" keyword (fix to bug 280)

more interface work; adding legacy C interface

first crack at compatibility java interface (not built by default)

Fix to building and linking for unit tests.  (This should fix the segfaulting units in optimized-dynamic.  The problem was that the code incorrectly determined the address of one of the thread-scoped global variables, and I think it's because the same library was linked twice into the unit test in two different ways, confusing the runtime support code.)

interface cleanup, java bindings work

Java binding now working.  Some interface types still need some work (e.g. iterators aren't functional).  Also, output isn't very flexible yet, as I told SWIG to ignore all the operator<<'s.

considerable bindings interface work, some improvements to build

fix build

Merge from "swig" branch: language binding for Java is compiling and linking.  Enable with --enable-language-bindings=java

cleaned up the mechanism for library versioning

--show-debug-tags and --show-trace-tags now supported by Configuration API; also, the information is only recompiled and relinked when it has changed, avoiding unnecessary relinking

dump define-funs correctly with "--dump declarations", whether the function is defined via API or through input language

include example theory (former "UF-Tim") that's included in the dist but not built for the library

final(?) documentation fixes

fix up more documentation

some minor fixes to the cvc3 compatibility library and test case

new, improved doxygen config file

fix serious issue with copyright-updating script

fix numerous documentation issues; doxygen complains much less, now

fix an oversight in the language printers

fix debian build without breaking anything (i hope)

tim's fixes for context-dependent pre-registration

adding --show-debug-tags to list all available debug tracing tags

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)