Moving the ITE removal from CnfStream to TheoryEngine, which is a bit closer to its final destination. Added a basic rewriter to TheoryUF. (x=x rewrites to true.) Added DIVISION to src/expr/node_manager.cpp's getType. Fixed the theory returned for variables in theoryOf() for bool and arith. Fixed TheoryEngine rewrite children to properly handle APPLY_UFs. Removed the special case for equality in TheoryEngine rewrite. A few tests are currently broken due to deallocation errors. Morgan and I will try to commit a fix to this in a little bit.

fix bug #134: infinite deallocation loop

small cosmetic change to tests summary output

Remove isAtomic() as per 4/27/2010 meeting.  Add comments about its potential design for later.  Resolves bug 113, invalidates bugs 93 and 94.

fix compiler comparison-signedness warnings

Reverting this file to not include any comments. (Morgan's revision and my revision were in conflict.)

added the ability to add custom expected stdout, stderr, and exit codes to smt and smt2 regressions; resolves bug 132

Preregistration has been turned on. Highly experimental eager splitting support has been added.  Also a few bug fixes to Tableau.

Use the newer automake test driver "parallel-tests".  This driver:

* keeps test logs around
* provides parallel testing functionality (with make -jN).

I've also added new functionality in test/Makefile.am which deletes old test logs, ensures that ALL tests are tried (even if units fail), and provides a color-coded summary at the end of the test run, which shows how many units, regressions (per level), and system tests failed (or passed), and provides a link to the log file for further information.

Resolves bug 117.

Adding debug assertions on most TNode operations

Adding NodeManager::prepareToBeDestroyed() (Fixes: #128)

Adding .cvc4_config to .gitignore

fix bug #111: errors in building lcov-all

fix bug 120; competition mode regression failures for intentionally-buggy input

 . '+Outstanding case split in theory arith'

Adding CnfStreamBlack tests for all Boolean connectives

Fixing test failures in CnfStreamBlack (it was the test's fault)

Adding documentation to my-configure

Fixing my-configure

Adding contrib/my-configure

Adding CnfStream unit tests

CDMap<> and CDOmap<> fixes to resolve bug 123

Fix for bug 131. Added some additional debugging assertions for the arith rewriter.

CDMap: fix bug 130

Prevent lexer errors being raised if a parser error is pending.
This fixes a bug Dejan has often whined about but never filed.

Added Rational constructors that only take a numerator. The const char* Rational and Integer constructors are now explicit. This means that 'Integer = 3;' and so on are no longer permitted.  This closes bug 121.

Some initial changes to allow for lemmas on demand.

To be done:
* Add erasable map Clause* to bool to minisat (backtracks with the solver)
* Add map from Clause* to Node (clauses that came from a node)
* Add reference counting Literal -> Node to CNFManager
* If Literal -> Node refcount goes to zero, the clauses of Node can be erased (if eresable)
* If clause is erased for each L in clause L -> Node refcount goes down

Small fixes to TheoryArith.  Added a hack to make Integers a subtype of Real. See Bug 127 for a discussion of the hack.  I am also adding a regression test that does not work (bug 128). It is not enabled so make check should still be fine.

Added the division symbol to the parser, and minimal support for it in TheoryArith.  Also directly hacked in support for theoryOf() to work for equalities where the left hand is a variable of type real.

Significant revision to theory/arith.  The new draft has a lot of small bug fixes and organizational changes.  The theory is now enabled to perform checking in the TheoryEngine. This draft can now solve 2 new regression tests test/regress/regress0/ineq_slack.smt and test/regress/regress0/ineq_basic.smt. There is also a small bug fix inside src/expr/attribute.h.

Adding debugging code in PropEngine/CnfStream

Adding ITE tests

Adding rudimentary ITE handling in CnfStream

Virtualizing interface between CnfStream and SatSolver

Minor refactorings to PropEngine, SatSolver

Minor refactorings and corrections to comments

Adding ParserBuilder, reducing visibility of Parser and Input constructors
Adding Smt2 subclass of Parser
Checking for multiple calls to set-logic in SMT v2

true and false are only defined if the core theory is loaded in SMT v2 strict mode

Refactoring parser tests

Adding class Smt2 to handle declaration of logic and theory symbols

Tightening lexer rules for numerals in SMT v2

make CVC4::Rational public (fixes broken build)

Adding --strict-parsing option

Adding AntlrInput::tokenTextSubstr

Adding tests for Rational::fromDecimal

Adding tests for Integer::pow

Adding bit-vector constants in SMT2

Implementing Rational::fromDecimal and adding support for real constants in SMT parsers

fixing the nightly failure. TypeCheckingException is now marked with CVC4_PUBLIC

changing the interface to bit-vector constant constructor

bit-vector constant constructor from string

bug fixes for types, old unit tests for types work now

Adding simple SMT2 parser tests

Disabling semantic checks in competition mode.
Adding function debugTagIsOn to safely test for tracing in any
compilation mode.
Removing irrelevant command-line options from usage message
in muzzled mode.

Minor change to SMT v2 grammar

Adding general support for SMT2 set-info command

Handling SMT 2.0 symbols and info flags

Type-checking classes and hooks (not tested yet).

more reasonable smt 2.0 benchmark test

main driver supports .smt2 input, added an smt2 regression (currently broken, so it doesn't run with "make check")

theory detection fixes; fixes build breakage when you delete build directories

Small mistake in previous commit

Importing ANTLR3 lexer nextToken function to avoid escaped exceptions.

smt parser for bit-vectors

Fix for the last night's build errors (type that broke proper expression generation).

Adding missed antlr_input files

Fixing private/public header warnings in parser library

Adding comments to bounded token files

Fix for bug 115, mapping was going in the wrong direction.

Added the capability to construct expressions by passing the operator instead of the kind, i.e.

Expr op = ..."f"...
em.mkExpr(op, children);

Operator kinds are automatically associated with the enclosing expression kind in the DSL and generated.

(Not) Handling parameterized sorts in SMT v2

Minor fix to SMT v2 parser tests

First draft implementation of SMT v2 parser

SMT parser has to map 'Real' to RealType

Merging the arithmetic theory draft (lra-init) back into the main trunk.  This should not affect other parts of the system. This code is untested, and is volatile.  It is going to be improved in the future so don't pick on it too much.  I am merging this code in its current state back into the main trunk because it was getting unruly to keep merging the updated trunk back into the branch.

adding integer and real types to the public interface

Build fix for parser

Refactoring Input/Parser code to support external manipulation of the parser state.

Added theory/arith/kind and enabled the smt parser to read in these symbols. Also a bug fix to a couple of unit tests.

Adding Integer and Rational constants to SMT

Adding a bit of documentation to the SMT parser

Some cleanup. Also added the integer and real types.

Adding the intermediary TypeNode to represent (and separate) the Types at the Node level.

Fixing compiler error for optimized builds

Adding info in the minisat README

Implementing missing NodeBuilder::constructNode

Enhancements to NodeManager tests, taking advantage of new Type implementation

Removing horrible, system-locking option from Eclipse Make preferences.

Moving debug output in ~ContextObj under a conditional. Should fix most of the slowdown from r413.

Marging from types 404:415, changes: Massive

* Types are now represented as nodes in the attribute table and are managed, i.e. you can say
    Type booleanType = d_nodeManager->booleanType();
    Type t = d_nodeManager->mkFunctionType(booleanType, booleanType);
    FunctionType ft = (FunctionType)t;
    Assert(ft.getArgTypes()[0], booleanType);
* The attributes now have a table for Nodes and a table for TNodes (both should be used with caution)
* Changes the way nodes are extracted from NodeBuilder, added several methods to
  extract a Node, NodeValue, or Node*, with corresponding methods for extraction
* Used the above in the construction of Expr and Type objects
* The NodeManager now destroys the attributes in the destructor by pausing the
  garbage collection
* To achive destruction a flag d_inDesctruction has been added to loosen the assertion
  in NodeValue::dec() (there might be -refcount TNodes leftover)
* Beginnings of the Bitvector constants using GMP

Not yet in tiptop phase, needs more documentation, and Types should be pulled out to TypeNodes eventually. Also, the types are currently defined in the builting_kinds, and I need to add these to the theory specific definitions with special 'type' constructs.

I hate branching and merging.

* Better dependency tracking for unit test building and linking, and
  auto-generated headers (metakind.h etc.), so they don't have to be
  recompiled every time.  This drastically improves build time when
  only small updates are made.

* Added "memory.h" unit test header for checking out-of-memory
  conditions.  cdlist_black uses it.

* Added helpful output when you "make lcov" in a non-coverage-enabled
  build.

* Removed strict aliasing warning when compiling metakind.h header
  with optimization on.

* Removed const version of NodeBuilder::operator Node()---it was
  poorly performing, better to not permit it---and fixed the
  convenience builders to use the non-const version
  (re: code review #63)

* Color-coded test output on capable terminals.

* Fixed some warnings in unit tests.

Merging from branches/decl-scopes (r401:411)

Doxygen fixes

minor fixes to lcov build target, better contextobj testing

added experimental "make lcov" target (it runs only unit tests); better coverage for util and context classes; implemented some output functionality that was missing; reclassified some tests white -> black or black -> public; other minor fixes

A handful of build system fixes:

* (test/unit/Makefile.am) libtool was being passed relative paths of
  sources in .cpp, confusing lcov if -b wasn't given.  Fixed.
  Closes bug #102.

* (configure.ac) --enable-coverage now implies --enable-static
  --enable-static-binary --disable-shared.

* (configure.ac) Create top-level config.status for informational and
  re-configuration purposes.

* (configure.ac) Remove -fvisibility=hidden for debug builds.
  Closes bug #104.

* (test/unit/Makefile.am) Build unit tests with -Wall.

* (various unit tests) Fixed trivially-fixable warnings in building
  unit tests.  (Signedness in comparison, unused variables, etc.)

* (Makefile.builds.in) Copy the binary correctly if it is static.
  (It was failing, but only with --enable-static --enable-shared
  --enable-static-binary.)  Closes bug #103.

* (src/parser/Makefile.am) libcvc4parser.so now links with libcvc4.so.

* Other minor cleanups to the build system.

This update contains more black-box tests as part of the attributes code review. I have confirmed by eyeball that every executable line of attributes.h is now getting hit in coverage testing. This can only be eyeballed at the moment because of templates. (There is 1 function that is not being touched, something included from NodeTemplate: _ZNK4CVC44expr4attr16AttributeManager12getAttributeINS0_9AttributeINS_6theory15RewriteCacheTagENS_12NodeTemplateILb0EEENS1_19NullCleanupStrategyELb0EEEEENT_10value_typeEPNS0_9NodeValueERKSB_)

* Add some protected ContextObj accessors for ContextObj-derived classes:
  + Context* getContext() -- gets the context
  + ContextMemoryManager* getCMM() -- gets the CMM
  + int getLevel() -- the scope level of the ContextObj's most recent update
  + bool isCurrent() -- true iff the most recent update is the current top level

  In particular, the ContextObj::getCMM() call cleans up by TheoryUF's
  ECData::addPredecessor() function substantially (re: code review bug #64).

* Fix serious bugs in context operations that corrupted the ContextObj
  linked lists.  Closes bug #85.

* Identified a bug in the way objects of the "Link" class are
  allocated; see bug #96.

* Re-enable context white-box tests that ensure proper links in linked
  lists.  Closes bug #86.

* Re-enable CDMap<>::emptyTrash().  Closes bug #87.

* Add a tracing option (-t foo or --trace foo) to the driver to enable
  Trace("foo") output stream.  -d foo implies -t foo.

* Minor clean-up of some TheoryUF code; addition of some documentation
  (re: code review bug #64).

* Address some things that caused Doxygen discomfort.

* Address an issue raised in NodeManager's code review (bug #65).

* Remove an inaccurate comment in Attribute code (re: code review bug #61).

Adding black-box tests for NodeManager (Closes bug #65)

Removing unused functions that were causing compiler warnings