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

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