bitvector rewriting for the core theory and testcases

Bug fix to CVC4::theory::arith::VarList as well as some superficial changes. test/regress/regress0/arith/arith.03.cvc now passes and is turned on by default.  Tiny documentation fix for the arithmetic normal form.

* added test/regress/regress0/arith for easy arithmetic regress tests.

ensure uf/congruence closure debugging stuff isn't called in production builds

make Node iterators more STL-friendly, resolves bug #196

build system consistency in target names for unit test targets

statistics are now printed on timeout (SIGXCPU) and SIGINT if --stats is given

link TAGS file into builds/ directory, when built.  Resolves bug #195

* New normal form for arithmetic is in place.
* src/theory/arith/normal_form.{h,cpp} contains the description for the new
  normal form as well as utilities for dealing with the normal form.
* src/theory/arith/next_arith_rewriter.{h,cpp} contains the new rewriter.
  The new rewriter implements preRewrite() and postRewrite() for arithmetic.
* src/theory/arith/arith_rewriter.{h,cpp} have been removed.
* TheoryArith::rewrite() has been removed.
* Arithmetic with the new normal form outperforms the trunk where the branch
  occurred (-r797) on 46% of the examples in QF_LRA. (33% have no noticeable
  difference.) Some important optimizations are stilling pending to the code
  for handling the new normal form. (Bug 196.)

"Leftist NodeBuilders" are now supported.

That is, "nb << a << b << c << OR << d << AND" turns into
  (AND (OR a b c) d)

The rule is:  pushing a kind onto a NodeBuilder with a nonzero
number of child Nodes in it, the action "collapses" it.  If a
kind is already associated to the NodeBuilder, it is an error.

Thus:
  NodeBuilder<> nb(AND); nb << AND;
and
  NodeBuilder<> nb; nb << AND << OR;
are both errors (if assertions are on).

In reality, though, the implementation is trickier, as the collapsing
is done lazily on the following push.  This complicates things a bit,
but by placing an Assert(false), I found that we aren't depending on
the old behavior (at least for any unit tests or regressions in the
source tree).  The Assert(false) is now removed and leftist
NodeBuilders are in business.

Fixes bug 101.

recategorize eq_diamond14 as a regress2 test (instead of regress0)

fix an error in TimerStat

neglected build system update from r848 (last commit)

* add TimerStat statistic type
* add Stats black-box unit test
* new make target: "make units" now runs unit tests only
* revised make target: "make regress" now runs regressions only
* configure.ac: pull in librt for clock_gettime()

"make check" now places binaries in the proper place before doing the checks; this closes bug 46 finally, though the major annoyances related to this bug already had been fixed long ago

reflect in build strings that -gmp is now the default and -cln is an option

added documentation, closes bug 97

Making GMP default, CLN opt-in with --with-cln

updating the minisat restart parameters after running some experiments

turn off extra-checking (which does extra theory-rewriter checking); it was enabled by mistake in the last commit

UF theory bug fixes, code cleanup, and extra debugging output.
Enabled new UF theory by default.

Added some UF regressions.

Some work on the whole equality-over-bool-removed-in-favor-of-IFF
thing.  (Congruence closure module and other things have to handle
IFF as a special case of equality, etc..)

Added pre-rewriting to TheoryBool which rewrites:

  * (IFF true x)          =>  x
  * (IFF false x)         =>  (NOT x)
  * (IFF x true)          =>  x
  * (IFF x false)         =>  (NOT x)
  * (IFF x x)             =>  true
  * (IFF x (NOT x))       =>  false
  * (IFF (NOT x) x)       =>  false

  * (ITE true x y)        =>  x
  * (ITE false x y)       =>  y
  * (ITE cond x x)        =>  x

Added post-rewriting that does all of the above, plus normalize IFF and ITE:

  * (IFF x y)             =>  (IFF y x), if y < x
  * (ITE (NOT cond) x y)  =>  (ITE cond y x)

(Note: ITEs survive the removal-of-ITEs pass only if they are Boolean-valued.)

A little more debugging output from CNF stream, context pushes/pops,
ITE removal.

Some more documentation.

Fixed some typos.

more tests, configuration for UF

Merge from "cc" branch:

CongruenceClosure implementation; CongruenceClosure white-box test.

New UF theory implementation based on new CC module.  This one
supports predicates.  The two UF implementations exist in parallel
(they can be selected at runtime via the new command line option
"--uf").

Added type infrastructure for TUPLE.

Fixes to unit tests that failed in 16-August-2010 regressions.
Needed to instantiate TheoryEngine with an Options structure, and
explicitly call ->shutdown() on it before destruction (like the
SMTEngine does).

Fixed test makefiles to (1) perform all tests even in the presence of
failures, (2) give proper summaries of subdirectory tests
(e.g. regress0/uf and regress0/precedence)

Other minor changes.

Add "no trash" CDMap elements, so that CDMap elements can themselves
be allocated in context memory.  CDMap black-box test extended.

Change TheoryEngine to use pointers to theories instead of
calling them directly.  In tests this doesn't appear to
lead to slowdown.

add zlib checks to configure (new minisat requires it?)

Fixing failures in minisat

renaming minisat .C to .cc

Adding the changes to the original copy

Importing MiniSat2 070721 into trunk

Removing newer version of MiniSat for Dejan's preferred import

Importing MiniSat2 2.2.0 into trunk

Removing old version of MiniSat for proper vendor import

Adding configuration_private.h to allow inlining of configuration checks

fix TheoryEngineWhite, add documentation; related to bug #188

Adding TypeCheckingException to throws clause in SMT parsers

Forcing a type check on Node construction in debug mode (Fixes: #188)
NOTE: mkNode/mkExpr/parsing functions can now throw type checking exceptions

fixed theory engine white test for new (old) theoryOf() behavior (re: bug 188)

Moving EQ->IFF handling from TheoryEngine to parser/type checker

Adding optional 'check' parameter to getType() methods

incorporate a fix from smtcomp2010 version for handling CNF of (= bool bool); also make theoryOf(= t1 t2) return theoryOf(t1.getType()), rather than theoryOf(t1), as the latter gives different results for (= (geq x1 x2) (leq x2 x1)) and (= a (leq x2 x1)), which is strange and causes problems.  should discuss at tuesday meeting.  resolves bug 187.

Added test file for fuzzsmt bug, bug187.smt2.

add >, <=, and >= comparisons for Exprs and Nodes

Fix for the type in sat propagation.

the tableaux optimization

Moving cluster-qf_lra-full to scripts project

Moving cluster-qf_lra-benchmark to scripts project

Adding missing operators in SMT2 parser: UMINUS, DIVISION, GEQ, LEQ

Fixing Array type in SMT v1.2

I am adding my smt-crunch scripts to source control.  Others may find them useful. To use them, log into goedel, sudo su acsys-user, and run ./cluster-script PATH_TO_EXECUTABLE. Be sure to change the email address in the script before using it. Improvements are of course welcome.

context work to support cdmaps with elements allocated in context memory

Updates to the post_mortem.py script.

Shared term manager tested and working
It is currently tracking all asserted equalities for simplicity.
Might want to check if this is a performance hit

Making plus-mult.cvc test a bit more torturous (as enabled by r744)

Fixes arith rewriter to allow for division by a constant. It previously only allowed for a constant divided by a constant.

Fixing test plus-mult.cvc by making it linear (Fixes: #184)

minor changes to cdmap/cdset interface for detection of duplicate inserts

chris and i committed the same fix; reverting the (now duplicated) fix

Updated headers

Added shared term manager.  Basic mechanism for identifying shared terms is
working.  Still need to implement theory-specific shared term propagation.

Disabling failing tests

add exit status to regression that was failing

some build system changes reverted after the CLN build system work a few days ago, these are now fixed:  competition configurations build with -O9 (as they used to); they are static-binary by default and shared libs are not built; also the default autoconf compiler flags "-g -O2" is removed from builds

competition submission should be fully static

fixed submission target

things for competition upload: new "make submission" target

Adding tests for precedence of arithmetic in CVC inputs

Adding config.reconfig to .gitignore

Fixed exit status for competition mode.

Don't eagerly collect zombies.  This should speed up things for competition but might flush out some memory issues.  Passes all regressions so far..

add Configuration::isCompetitionBuild() and some main driver fixes

fix crash on command line parsing

Moved registration to theory engine

Adding Array types to SMT2 parser

Adding arithmetic symbols to CVC parser (Fixes: #176)

merge from CC work: pieces of the parser need to be declared to throw AssertionException, and language enum should have stream insertion op

Fixes for doubled-statistics (bug 171), a fix to muzzled builds and some minor code
cleanup found while searching for additional cases.  Closes bug 171.

add regressions from bug reports

better exception wording, assertion-handling in multiple-exception case; resolves bug 175.  also newer URL for config/pkg.m4

better exception wording, assertion-handling in multiple-exception case; resolves bug 175.  also newer URL for config/pkg.m4

workaround for strange CIMS installation of automake; resolves bug 172: autogen fails on CIMS machines

Added Cesare to list of authors

Changed AUTHORS - removed references to earlier CVC tool authors

Considerably simplified the way output streams are used.  This commit
should have no impact on production performance and speed up debug
performance considerably, while making the code much cleaner.  On some
benchmarks, debug builds now run _much_ faster.

We no longer have to sprinkle our code with things like:

  if(debugTagIsOn("context")) {
    Debug("context") << theContext << std::endl;
  }

which we had to do to get around performance problems previously.
Now just writing:

  Debug("context") << theContext << std::endl;

does the same in production and debug builds.  That is, if "context"
debugging is off, theContext isn't converted to a string, nor is it
output to a "/dev/null" ostream.  I've confirmed this.  In production
builds, the whole statement inlines to nothing.  I've confirmed this
too.

Also, "Debug" is no longer a #definition, so you can use it directly
in production builds where you couldn't previously, e.g.

  if(Debug.isOn("paranoid:check_tableau")) {
    checkTableau();
  }

I'm leaving debugTagIsOn() for now, but marking it as deprecated.

assigning benchmark statuses

better detection for static binary building

fix to production build

enable arrays

don't do extra-checking for all regressions; that's probably a bad default

With "-d extra-checking", rewrites are now checked (after
post-rewrite, another full rewrite is performed and the results
compared).

Also added another response code to rewriters.  Theories return a
CVC4::theory::RewriteResponse from preRewrite() and postRewrite().
This class has nice subclasses to make the theory rewriters somewhat
self-documenting in termination behavior.  They look like
tail-recursive rewriting calls, but they're not; they are
instantiations of the RewriteResponse result code, which carries the
Node being returned:

  // Flags the node as DONE pre- or post-rewriting, though this is
  // ignored if n belongs to another theory.
  //
  // NOTE this just changed name from RewritingComplete(), which
  // didn't match RewriteAgain().
  //
  return RewriteComplete(n);

  // Flags the node as needing another pre-rewrite (if returned from a
  // preRewrite()) or post-rewrite (if returned from a postRewrite()).
  //
  return RewriteAgain(n);

  // Flags the node as needing another FULL rewrite.  This is the same
  // as RewriteAgain() if returned from preRewrite().  If it's returned
  // from postRewrite(), however, this causes a full preRewrite() and
  // postRewrite() of the Node and all its children (though the cache is
  // still in effect, which might elide some rewriting calls).
  //
  // This would have been another fix for bug #168.  Its use should be
  // discouraged in practice, but there are places where it will
  // probably be necessary, where a theory rewrites a Node into
  // something in another theory about which it knows nothing.
  // A common case is where the returned Node is expressed as a
  // conjuction or disjunction of EQUALs, or a negation of EQUAL,
  // where the EQUAL is across terms in another theory, and that EQUAL
  // subterm should be seen by the owning theory.
  //
  return FullRewriteNeeded(n);

bug 168 fixed (TheoryEngine::rewrite is not fully rewriting to a fix point); problem had to do with the builtin theory post-rewriting DISTINCT into an arithmetic term not in normal form.  fix was to do DISTINCT rewriting in pre-rewrite.  note that this doesn't add to the amount of theory rewriting work that needs to be done, because everything is cached

make dist && make distcheck functional, other fixes

fix warnings

better config.reconfig script auto-generated

With this commit come a number of changes to build system to support
building with CLN or with GMP, the contrib/switch-config script
(enabling "fast switching" of different configurations in the same
builds/ directory), and also some minor changes.

./configure --with-gmp     (or --without-cln) forces building with GMP
and doesn't even look for CLN.  Configure fails if GMP isn't installed.

./configure --with-cln     (or --without-gmp) forces building with CLN
and doesn't even look for GMP.  Configure fails if CLN isn't installed.

./configure [no arguments] will detect what's installed.  CLN is
default, if it isn't installed, or is too old, GMP is looked for (and
configure fails if neither is available).

It is an error to specify --with-gmp --with-cln (or --without-* for
both) at the same time.

Building with CLN (whether forced or detected) adds a note to the
configure output mentioning the fact that the build of CVC4 will be
linked against a GPLed library and notifying the user of the
--without-cln option.

Building with GMP (whether forced or detected) affects the build
directory, so CLN and GMP builds are kept separate.

./configure --with-cln debug     builds in builds/$arch/debug
./configure --with-gmp debug     builds in builds/$arch/debug-gmp

The final binaries are linked explicitly against either gmp or cln,
but not both.  If linked against cln, cln pulls in gmp as a
dependency, so the result will be linked against both.

=== Details that you probably don't care about ===

The headers src/util/{integer,rational}.h are generated from the
corresponding .in versions.  A user installing a CVC4-devel package
will get the headers for rational and integer that match the library
that s/he installs.

The preprocessor #defines CVC4_GMP_IMP and CVC4_CLN_IMP are added to
cvc4autoconfig.h.  Only one is ever #defined.  cvc4autoconfig.h
doesn't need to be #included directly; you get it through #including
cvc4_private.h (or the parser version).

AM_CONDITIONALs are also defined so that Makefiles get the cln/gmp
configuration.  AC_SUBSTs are defined so that public headers (see
src/util/{integer,rational}.h.in) can use the setting.

*Public* headers that need to depend on the cln/gmp configuration
can't use cvc4autoconfig.h, because we're keeping that in the private,
internal-only space, never to be installed on users' machines.  Here,
something special is required, like the configure-level generation of
headers that I used for src/util/{integer,rational}.h.in.

Tim's Integer and Rational wrappers are the only bits of code that
should care which library is used (and also src/util/configuration.h,
which gives the user of the library information about how CVC4 is
built), and possibly some unit tests (?).

Merges the cln-test branch into the main branch.

The current commit allows for switching in between GMP and CLN by changing a flag manually in configure.ac.  A configure time flag has not yet been added for deciding between the two.

To get this to work you will need to install cln in some form (for Ubuntu users the packages are libcln6(lucid)/libcln5 on karmic and libcln-dev).  You will also need to install pkg-config. You will need to rerun ./autogen.sh, and reconfigure.

re-generated comment headers of source files

roll back a small change that made arith fail some asserts