support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary define-fun; several set-info, set-option, get-option, get-info improvementss

fix to unit tests

bug fixes to model gen

Model generation for arith, boolean, and uf theories via
(get-value ...) SMT-LIBv2 command.  As per SMT-LIBv2 spec,
you must pass --interactive --produce-models on the command
line (although they don't currently make us do any extra
work).  Closes bug #213.

* (define-fun...) now has proper type checking in non-debug builds
  (resolves bug #212)

* also closed some other type checking loopholes in SmtEngine

* small fixes to define-sort (resolves bug #214)

* infrastructural support for printing expressions in languages
  other than the internal representation language using an IO
  manipulator, e.g.:

    cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << expr;

  main() sets the output language for all streams to correspond to
  the input language

* support delaying type checking in debug builds, so that one can debug
  the type checker itself (before it was difficult, because debug builds did
  all the type checking on Node creation!): new command-line flag
  --no-early-type-checking (only makes sense for debug builds)

* disallowed copy-construction of ExprManager and NodeManager, and made other
  constructors explicit; previously it was easy to unintentionally create
  duplicate managers, with really weird results (i.e., disappearing
  attributes!)

support (set-info) on status, source, category, difficulty, smt-lib-version, and notes; reduces extraneous "unsupported" output

oops, reverting a change to a regression test that had intentionally caused a typechecking violation

type checking for define-fun in production builds; related to (and might resolve) bug 212

NodeSelfIterator implementation and unit test (resolves bug #204); also fix ParserBlack unit test initialization

Small tableau optimization.

SMT-LIBv2 (define-fun...) command now functional; does eager expansion at preprocessing time

declare-sort, define-sort working but not thoroughly tested; define-fun half working (just need to decide where to expand)

parser and core support for SMT-LIBv2 commands get-info, set-option, get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...

fix gdb issues (at least for static builds); resolves bug 194

fix regular expressions in build system

fixing CLN builds, which had broken the build tonight; will re-run regression script

re-add a dependency to fix compile warnings

remove/shuffle some #include dependencies; fix some documentation; apply coding standards

Fix to bug 211. ArithVar is now typedefed to uint32_t.

file header documentation regenerated with contributors names; no code modified in this commit

revert a workaround fix to CDMap that was committed as part of the arith-indexed-vars merge, and fix the root cause (maybe?) in attribute.cpp: previously, items from the cdnodes attribute table weren't properly being "obliterated" from the table due to a typo

dump statistics on abnormal output: unexpected exceptions, SEGV, ILL, memout...

branches/arith-indexed-variables merged into the main trunk.

re-add no-deprecated to C sources; update some file-level documentation; first look at cdvector for code review

last update broke the parser inadvertently, fixing...

replacement implementation for clock_gettime() on mac os x, build portability (resolving mac os x issues), code cleanup, fix compiler warnings

fixed a number of problems with mac os x builds.  build now works on mac os x if you disable the clock_gettime check in configure.ac (resolves bug #202), but the parser is broken (new bug #208)

fix predicate bug in UF; code cleanup in theory.cpp

node iterator work

fix pre-registration of operator, previously committed; clean up theory engine code and unit test

fix unit test for kinded iterators in Node/TNode

fix TLS support for platforms (e.g. Mac OS X) where __thread storage class doesn't exist, and clean up a few things in NodeManager

comment fix as per this morning's meeting; also, don't theory-rewrite operators (resolves bug #198)

add workaround for systems (i.e., Mac OS X) that don't support __thread; also configure script auto-detection of __thread support and syntax

- This update adds DynamicArray<T>.  This is a bare bones heap allocated array that dynamically can increase in size.  This has functionality similar to vector<T>. The main difference is that it can be constructed in an ill-formed manner. This means that it can generalize CDList<T>.
- CDVector<T> has been added. This is intended to allow for context-dependent destructive updates, while the vector size increases are permanent. Behaviorally, this is most similar to vector< CDO<T> >. The differences between the two are: only one ContextObj is registered to the Context, backtracks are done in a lazy fashion, CDVector::push_back(val) sets the value of back() at context level 0 to val where vector<CDO<T>>::push_back(val) sets back() at the current context level to val and back() at context level 0 to the default constructor T().

equality triggers for the equality engine
fixed order of destruction in smt_engine

roll back an unintended change with r900

Fix build system for Mac OS X builds (resolves bug #203)

basic union find for bitvectors

Fixing NodeBuilderBlack

Rm'ing automatic type check in NodeBuilder for vars/constants

remove assertion in TNode destructor and ensure all TNode methods check rc > 0 (resolves bug #200); on NodeManager/ExprManager side, no more prepareToBeDestroyed() / inDestruction

fix statistics-registry-related memory leaks

part of review (bug #197): coding conventions, file-level documentation, re-ran update-copyright.pl, etc.

svn:ignore properties for new bv stuff

some code cleanup, documentation, review of "kinded-iterator" code, and addition of a unit test

iterators for tim, begin<PLUS>() and end<PLUS>() should give him what he wants

Rm'ing Makefile.in's

Moving automatic type check to NodeBuilder (Fixes: #199)

hooking up the bitvector tests

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