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

fixing a few broken build-related items, adding test cases

big check-in of various fixes and adjustments

antlr parser for the cvc4 language (boolean only)
yet to be finalized, it should work as expected

Big chunk of changes:

* Fixed bugs in option parsing
* Simplified the main.cpp significantly (more c++ like)
* Added the null kind, expr value, and expression, with the default constructor public
* Simplified commands, we need to discuss this in the meeting (what to do with command results?)
* Removed all the lex/yacc files
* Symbol table is now a templated class, as we will have tables for variables, predicates and functions
* The ANTLR parsing infrastructure/makefiles is all in. SMT lib Boolean benchmarks should parse + giving nice error such as
      Parse Error: /home/dejan/eclipse-cxx/smtlib-parser/test/test4.smt:3:16: Undeclared variable p
      Parse Error: /home/dejan/eclipse-cxx/smtlib-parser/test/test2.smt:2:11: unexpected token: sa

Didn't add any unit tests as the unit testing doesn't work with the updated build system -- it doesn't know how to create directories in the corresponding build directory.

TODO:
 * add the PL grammar and unit test when the testing becomes available
 * with this build setup my eclipse debugger doesn't work.  Might have something to do with the visibility of symbols?
 * i'm getting g++ depracated warnings regarding the hash_map from the symbol table, need to figure out how to use it in a standard manner. the new <unordered_map> header is for C++0x, and the <ext/hash_map> is getting deprecation warningns... weird.

more build system work

more build system work

More changes to configure.ac to include the smt grammar directory. The parser refuses to be built in the new separate directory structure though.

Forgot to commit changes to configure.ac

Adding support for ANTLR checking in autogen.sh (config/antlr.m4). Commiting antlr SMT grammar that should compile, but is not yet integrated. Tests of compilation and antlr crashes appreciated.

Eclipse CVC4 settings (with code style)

additional build system fixes

first attempt at new build system

parsing/expr/command/result/various other fixes

svignore for parser and util

Added an EmptyCommand and a CommandSequence commands and changed the parser a bit.

Commands and the eclipse C++ project settings.

Enough parsing for tonight. Added:
* Everything goes through the ParserState instead of coding in lex/yacc files
* Bare Boolean SMT lexer/parser
* Basic commands
To be completed: ParserState method implementations, parser.h/parser.cpp, make it compile and run...

additional work on parser hookup, configuration + build

Missed file: symbol_table.h

Parser should be complete for Booleans

oops, missed a file

various fixes and updates to use and support parser

Stubbing commands

Stubbing commandsmake

Parser for boolean exprs (no commands)

Partial parser for booleans

configure option adjustments as per 11/24 meeting; various fixes and improvements

fixups, file comments

fixes to build/test system

fix to expr #includes; better test-environment configuration

testing framework, configure fixes, incorporations from meeting, continued work

work on exprs, driver, util

ignored items

from meeting

from meeting

from meeting

fixes/redesign of source layout from meeting

another pass

fixes and additions

minor fixes

parser, minisat, other things..

minor fixes, added contrib directory

additional headers and modifications; now passes syntax check

additional headers

commit of project structure including autotools support

Initial setup of the cvc4 repository