Cleaned up and documented ecdata and theory_uf.

Committing small changes to attribute, and theory to avoid future merge problems for Moragn. Also cleaned up theory uf and ecdata, and updated both to reflect attribute. Should be close now.

Minor optimizations to parser (use const string& for ids, keep only one binding in symtab)

cosmetic changes, comments, and renaming of Expr related stuff to Node (leftovers from before switching to Node)

finally works

Merging from branch branches/Liana r241

Switching to types-as-attributes in parser

* src/expr/attribute.h: fixed an issue with "const pointer"-valued
  attributes.

* src/expr/attribute.h, src/expr/node_manager.h, src/expr/node.h:
  hasAttribute() and getAttribute() are now const member functions.

* configure.ac: Remove doc/ from search path for Makefile.ams

* configure.ac, test/unit/Makefile.am: Resolved an issue where even
  when not testing, one unit test was built.

* Re-ran contrib/update-copyright.pl on all source files to ensure
  consistent and correct header comments.

* contrib/get-authors: Change definition of "minor contributor"
  to >= 10% of lines (rather than strictly greater than 10% of lines)

Re-committing revision 232 properly:

* Add virtual destructors to CnfStream, Theory, OutputChannel, and
  ExplainOutputChannel.  Safer and stops a compiler warning.

* node attributes: fix compiler warnings on 64-bit.

* Node: add asserts to make sure the current NodeManager is non-NULL
  when it's needed.  This can happen when public-facing functions
  don't properly set the node manager, and it can look like a bug in
  another part of the library.  Also some code format cleanup.

* configure.ac, config/cvc4.m4: added --enable-static-binary (see
  discussion on bug 33), fixed bad configure lines (bug 19), added
  documentation for some things.

* config.h.in: removed; it's auto-generated.

undoing improperly-committed revision 232; will re-commit to get "svn blame" correct, etc..

* Add virtual destructors to CnfStream, Theory, OutputChannel, and
  ExplainOutputChannel.  Safer and stops a compiler warning.

* node attributes: fix compiler warnings on 64-bit.

* Node: add asserts to make sure the current NodeManager is non-NULL
  when it's needed.  This can happen when public-facing functions
  don't properly set the node manager, and it can look like a bug in
  another part of the library.  Also some code format cleanup.

* configure.ac, config/cvc4.m4: added --enable-static-binary (see
  discussion on bug 32), fixed bad configure lines (bug 19), added
  documentation for some things.

* config.h.in: removed; it's auto-generated.

Small changes to the smt-engine, removed the assertions list.

resolve bug 32; public-facing interface functions in expr package must set current NodeManager

fix bug 33 (statically link the "cvc4" binary); also main driver cleanup

fix bug 22 (remove tracing from non-trace builds; remove all output
from muzzled builds)

add public-facing CVC4::Configuration class that gives CVC4's (static)
configuration (whether debugging is enabled, assertions, version
information, etc...)

add some whitebox tests for assertions, output classes, and new
CVC4::Configuration class

main driver now gets about() information from CVC4::Configuration.

configure.ac now more flexible at specifying major/minor/release
versions of CVC4

add --show-config option that dumps CVC4's static configuration

commented option processing strings in src/main/getopt.cpp

fixed some compilation problems for muzzled builds.

fixed some test code for non-assertion builds (where no assertions are expected)

specialized implementation for boolean node attributes ("flags"): they now share memory words properly; also, implementations of some output functionality

* Attribute infrastructure -- static design.  Documentation is coming.
  See test/unit/expr/node_white.h for use examples, including how to
  define new attribute kinds.

Also:

* fixes to test infrastructure
* minor changes to code formatting throughout
* attribute tests in test/unit/expr/node_white.h
* fixes to NodeManagerScope ordering
* use NodeValue::getKind() to properly deal with UNDEFINED_KIND
  (removing compiler warning)
* ExprManager: add proper NodeManagerScope to public-facing member
  functions
* store variable names and types in attributes
* SoftNode is a placeholder, not a real implementation

Changing minArity of AND/OR to 1 in SMT parser

Adding --no-checking option to disable semantic checks in parser

Rm'ing doc from SUBDIRS

Adding doxygen configuration parameters and doxygen-doc Makefile target

Initial draft of TheoryUF. Should compile without problems. A decent amount of functionality is stubbed out. Still needs a bit of cleanup.

fix bug 27: --with-cxxtest-dir=(relative-path) now works

Moving parser error checking into AntlrParser

Adding --parse-only option

removing assertion and warning that shouldn't be there. adding initialization of kind to undefined to a default constructor.

Removing spurious commit of configure

Converting semantic predicates in parser to AlwaysAssertions

simplification minisat

Improvements to CNF conversion when already in CNF

build fix

Fix to compile out Debug(...) << ... statements in optimized mode. Someone please look to see if it makes sense.

Changes to hashing that solve the xinetd boolean benchmark in 14s (from ~25min). Switched to standard hash_set, hash_map, new hash for the vector of node values (from boost), changed the hash for nodes to be over id's, all the hash values are now size_t. The parser is down from 11s to 10s on the benchmark, so most of the solve time is parsing and we need to figure this out.

svn ignore

Adding precedence regressions

note on setup(); for discussion at 2010.02.11 meeting

svn:ignore for build stuff; add Liana to AUTHORS

fixing annoying eclipse build settings, no more broken pipe errors with these settings

Added calls to destructor in CDList plus optional flag to disable.

Changes to the CNF conversion and the SAT solver. All regression pass now, and we're ready for nightly testing. We should not add regression tests that test future behaviour, as the builds will nag for all failing regressions. Thus, I've separated the multi-query regressions into multiple regressions until the cnf/context/sat is able to handle it. Also, fixed a typo in the CVC parser.

removing other pieces of autotools stuff to fix bug #24

moving built-in kinds out of the kind.h prologue/middle for uniformity; added TUPLE built-in

empty stubs for push and pop to fix the build fail

Disabling the failing test case for the context.

Fixing the test case, it had a unary or. The cnf converter should be adapted to handle cases like this.

Push/Pop parsing and commands

Moving the template stuff back into the header in order to use CDList.

Documenting type.h/cpp
Making Boolean and Kind types singletons

force sorting of AC_CONFIG_FILES, otherwise different computers generate the configure script differently and we get useless commits of it; fix NodeBuilder memory leak in response to Kaustubh's expr code review (bug#15)

Preliminary support for types in parser

final fixes to addsourcedir source-directory-Makefile-generation script

auto-generated list of AC_CONFIG_FILES so that you needn't add each recursive Makefile to configure.ac

automatic generator script for sourcedir Makefiles and Makefile.ams

remove the last vestiges of support for "make build-profile" without first configuring the build-profile, simplifying the build process and closing bug 21

minor interface changes to TheoryEngine/Theory after meeting and conversation with Tim

fix run_regression script

beautification of the prop engine

assign expected-status to regressions

build system for multi-level regressions

remove warnings from use of __gnu_cxx::hash_map<>; also spacing fixes in symbol table

remove -*- c++ -*- emacs tag from source files (it overrides cvc4-c++-editing-mode from contrib/editing-with-emacs

Changed mapping from atoms to literals in the prop engine to be atoms to vars.

Moved regressions into various levels based on running time.

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