test infrastructure updated for multiple-level regressions

minor cleanup; give the main driver a different exit code for SAT-INVALID/UNSAT-VALID

src/expr/kind.h is now automatically generated.

Build src/expr before src/util.

Moved CVC4::Command to the expr package.

Re-quieted the "result is sat/invalid" etc. from PropEngine (this is
now done at the main driver level).

Added file-level documentation to Antlr sources

When built for debug, spin on SEGV instead of aborting.  Really useful
for debugging problems that crop up only on long runs.  Added
'--segv-nospin' to override this spinning so that "make check,"
nightly regressions, etc. don't hang when built with debug.

Updated src/main/about.h for 2010.

minor fix for update-copyright.pl; ran update-copyright.pl on all sources; regenerated configure script

added bool and arith theory makefiles to AC_CONFIG_FILES in configure.ac

Added theory output channel interfaces and "Interrupted" exception.

Updated contrib/update-copyright to handle Antlr (.g) parser/lexer inputs.
Updated copyright year.

Added a new "bool" theory (right now just to hold a kind.h contribution).

Added "kinds" files to UF and the new "bool" theory.

Fixes to the cnf converter. Also a barebones utility for printing out a satisifying model.

Adding extra test to parser

adding an option to minisat to not do any debug checks/output

Fixing bad commit

Adding functions/predicates to SMT grammar

Addressed many of the concerns of bug 10 (build system code review).
Some parts split into other bugs: 19, 20, 21.

Addressed concerns of bug 11 (util package code review).

Slight parser source file modifications: file comments, #included
headers in generated parsers/lexers

Added CVC4::Result propagation back through
MiniSat->PropEngine->SmtEngine->main().  Silenced MiniSat when
verbosity is not requested.

ELSEIF support and parser debugging with '-d parser'

simple ITE parsing

By popular demand, I also added a printAst to Expr.

I hacked in a temporary way to restart minisat for multiple queries.

Within node I added printAst(..) for general purpose debugging use throughout the code. I also added debugPrint() to Node for use within gdb.

Enabled more regress tests. Takes 26s on my machine to run a make -k check in debug mode.  All regress tests currently pass.

context_mm testing

some more tests for the context.

Fixed bug in context code

for tim

beginings of test for CDO. one fail

Rethrow rewrite in antlr_parser. Taking LT(0) to locate the error causes the build to break on 64-bit machines. Changed to LT(1), it works now, but i'll ask around how this actually works.

Switched cnf conversion to go through CnfStream.

Minor changes to parser

Adding support for escapes in string literals (strings like "\n\t\"")

Fixed compile errors

Updates to context:
  Use vector instead of linked list for Scopes
  Added CDO and CDList templates

Fixing the CVC grammar for parsing Boolean expressions. All the associativity stufff is now in the grammar. All the parser tests pass now.

fix node manager code (bugzilla #15, comment #2) in case where there's a hash collision for distinct objects

Added this test back to avoid make check problems.

cnf conversion (variable-introducing), cleanups, fixes to minisat calling for multiple-query cases

Checking in small test fixes for node_black

fixing the last context build problem, it compiles now

one more bug

Fixed compile errors

Adding Makefile.in to svn:ignore

Adding Makefile.in to svn:ignore

Fixing boolean operator precedences

Update of context module

fixed CNF conversion, and more modular; CNF conversion command line option; various cleanups; renamed numChildren() to getNumChildren() and added it to NodeBuilder interface; fancier, non-exponential CNF conversion with variable introduction is still buggy (?)

Removing Makefile.in's

Replacing hand-coded autogen.sh with buildconf version

support "make check" in src/ subdirs for unit-testing of just that module; also support synonyms for "make check" globally

test framework fixes; bug 13 closed

Added additional tests to node_black.h. CVC4 currently passes all but 1 test.

Undoing stupid commit mistake.  Rolling back to -r 102 for test/unit/expr/node_black.h

Added test/regress/boolean.cvc

cnf conversion

fixes to build structure, util classes, lots of fixes to Node and NodeBuilder.  outstanding SEGVs fixed

minor fixes to scoped-context node manager

scoped node managers

Added pure PL regression tests. Mostly CNF

Added regression test

minor changes to Theory

Changes to configure.ac from code review

More fixes fot the parser tests.

Changing some deatils on the parser. Now we know we are done if command is null, or expression is null.

More fixes

numerous fixes to nodes; more coming

Updated parser tests, which are all kinds of FAIL

Changes to the parser tests to make them compile.

more build system fix-ups

Lots of parser changes to make Chris happy. Yet more to come later.

more build system fix-ups

update-copyright.pl now retrieves and incorporates author information from repository history; re-ran update-copyright.pl; cleaned up some things with make

Adding more parser tests

Adding more parser tests

coding standard fix on SmtEngine; fix recursive make

CvcParserBlack and supporting Makefile changes

+ test infrastructure fixes
+ regenerate configure script
+ add CVC4::Message output class
+ add some IllegalArgument() assertion things
+ rename NodeManager::mkExpr() to mkNode()

add system regression testing infrastructure

fix typos in Makefile.am for unit testing

addressed some concerns raised by Clark in bug #6 (code review of driver code)

making config/mkbuilddir executable

Minor changes from code review

build system cleanup; test system separation into white-box, black-box, and public tests

testing infrastructure fixes

support nonstandard, unconfigured builds (e.g., "./configure debug" followed by "make production ASSERTIONS=1")

+ refactoring fixes for expr package based on code review (see bug #4)
+ minor autogen/configure fixes for old versions of autotools

Small refactoring changes for the expr package.

Spelling correction in comments

Standardizing configure arguments for ANTLR/CxxTest

Fixes to the build system:

Makefile.am files - remove obsolete INCLUDES, incorporate into AM_CPPFLAGS
Makefile files in src/ - support "make" under src/ (current build profile)
configure.ac - updates to fix warnings
config/antlr.m4 - updates to fix warnings
autogen.sh - updates to generate warnings from autotools; also support Macs
src/include/cvc4_config.h - guard with #ifdef
total reimplementation of NodeBuilder
ExprValue => NodeValue
context_mm.{h,cpp} - fixed numerous compile errors

Minor changes to parser files from code review.

Added context_mm (haven't tested compilation yet...)

minor: fixing typos

Extracted the public Expr and ExprManager interface to encapsulate the optimized expressions and the internal expression manager.

build fixes, configuration simplifications

killing expr into node...

cleanups, assert work, add a stubbed uf theory, fix driver

some fixes and organizational adjustments to assert code, parsers/lexers, and build process

A mess of changes in the expression manager, simple example still failing due to some problems in the prop_engine
* default null expr and expr value and reorganisation/rewrite of some methods
* fixed some bugs
* expressions should always be passed as const Expr& to methods, otherwise copy constructors are called

Problematic code:
* Expr class has a bunch of methods that return Exprs, such as a.andExpr(b). None of these know what is their expression manager. We should
 (a) Not allow this, all expression construction should go through the ExprBuilder or directly thorugh the expression manager
 (b) Allow this, as it is now, but the have the default expression manager be setup in every entry into the smt solver + these construction methods shouldn't be available to the user (oterwise a mess ensues)
* We have to decide how to construct ExprBuilders:
 (a) constructing ExprBuilders with em = ExprBuilder(e).andExpr(b) is problematic as at construction we can't know the expression manager, and the kind of em will be UNDEFINED, so when adding b we can't assume its not UNDEFINED
 (b) constructing it with ExprBuilder(em) << AND << a << b or ExprBuilder(em, AND) << a << b seems like a nicer approach

 I am still confused about these expression builders so we should talk about this.

final (?) fixes to parser/generated build directory modifications

parser build fixes

check in automake/libtool/autoconf-generated files; add better file not found handling

broken formula

work on propositional layer, expression builder support for large expressions, output classes, and minisat