Parsing support for SMT divisions: LRA, QF_UFLIA, QF_UFLRA, QF_UFNRA, UFNIA

Adding documentation for --strict-parsing (Closes: #166)

fix to switch fall-through; stats now off by default regardless of -d debugging options; thanks Chris for spoting this

checking in CC module interface for reference.

Support for failing .smt and .smt2 regressions (and other examples with
additional output).  If the benchmark file has '% EXPECT: ' gestures,
like for cvc regressions, that is used (after being stripped out so that
the cvc4 smt parser never sees these special lines).  However, this can
be a pain, since then you can't run the regression manually on the
command line (since it fails to parse).  So if there is another file
in the same directory as $benchmark called $benchmark.expect, that is
scanned for '% EXPECT: ' etc., and the benchmark file is used verbatim.

* theory "tree" rewriting implemented and works

* added TheoryArith::preRewrite() to test and demonstrate
  the use of pre-rewriting.

* array types and type checking now supported

* array type checking now supported

* theoryOf() dispatching properly to arrays now

* theories now required to implement a (simple) identify()
  function that returns a string identifying them for
  debugging/user output purposes

* added "builtin" theory to hold all built-in kinds and their
  type rules and rewriting (currently only exploding distinct)

* fixed production build failure (regarding NodeSetDepth)

* removed an errant "using namespace std" in util/bitvector.h
  (and made associated trivial fixes elsewhere)

* fixes to make unexpected exceptions more verbose in debug builds

* fixes to make multiple, cascading assertion fails simpler

* minor other fixes to comments etc.

add --default-expr-depth=N command line parameter, expose setdepth() to public interface

This commit merges the decaying-rows branch into the main trunk.

Update to stats.h is now back into the trunk.  The code should compile once again.

Merging the unate-propagator branch into the trunk.  This is a big update so expect a little turbulence. This commit will not compile. There will be a second commit that fixes this in a moment. I am delaying a change to avoid svn whining about a conflict.

* Add CDMap<>::insertAtContextLevelZero(k, d) for inserting "initializing"
  data into a CDMap.  Such a key doesn't disappear from the map on pop,
  but rather returns to its "initializing" state, set by
  insertAtContextLevelZero().  This can be used for lazy assignment,
  among other things, and has been added to support some exploratory
  coding by Tim in arithmetic.

* Made internal CDOmap<> copy constructor private (it should always have
  been).  This is necessary to avoid CxxTest (or others) doing nasty
  generic programming things that cause context invariants to be broken.

* Added unit testing for this feature, and in general beef up the unit
  testing for CDMap<>.

* src/expr/node_manager.cpp: Better output for unhandled cases in getType().

Added post_mortem.py a statistics collector for user with the smt_curnch cluster. Also a spelling correction for the statistic theory::conflict.

Made ~Stat() virtual. Added some additional statistics. And added some documentation.

"statistics" and "staticbinary" are now tags on the build (so you get build directories like builds/x86_64-unknown-linux-gnu/debug-staticbinary-nostatistics .. etc.  This is useful to distinguish static binary builds and statistics builds from each other when you configure multiple times in the same source directory

Merging the statistics branch into the main trunk. I'll go over how to use this Tuesday during the meeting. You'll need to run autogen and receonfigure after updating.

bug fix (unreported on bugzilla): skolem variables failing removal from pool

fix some minor annoyances in the regression test Makefiles; add some documentation

Added the experimental. +bool TheoryArith::AssertEquality(TNode n, TNode original){

More assorted changes to arithmetic in preparation for the code review.

This commit just contains miscellaneous arithmetic cleanup.

fix last commit gcc options (-wunknown-pragmas ==> -Wno-unknown-pragmas)

remove warnings about unknown #pragma GCC diagnostic on older compilers

I made a documentation change to get() to make explicit the contract requirements for 'slurping the queue'. Closes bug 154

(minor) fix for file documentation

Adding array select/store to SMT v1 and v2 parsers

Fix to arith to make sure it only attempts to report 1 conflict per check() call.

Started work on array theory

Some assorted fixes and local optimizations for theory arith.

Adding += and *= to Rational.

Changed how assignments are saved during check.  These are now backed by an attribute.  There is now a priority queue for selecting the smallest inconsistent basic variable. normal.h has been removed.  A large chunk of the registerTerm() stuff has been moved into preregister. The lazy splitting code is now been commented out so that it stops showing up in profiling.

Changed several arguments to const references.

Adding QF_SAT to SMT parsers

Reimplementing AntlrInputStream::newStreamInputStream

** Don't fear the files-changed list, almost all changes are in the **
** file-level documentation at the top of the sources.              **

This is the "make bugzilla stop bugging me" bugfix commit.

* Remove BackedNodeBuilder<> and collapse NodeBuilder<> hierarchy.
  Updated documentation in the file.  Resolves bug #99.

* Convenience NodeBuilders (PlusNodeBuilder, OrNodeBuilder, etc.)
  moved into a separate file.  Partially resolves bug #100.

* Moved isAssociative(Kind) into kind.h (and into the CVC4::kind
  namespace) instead of metakind.h (where it was in CVC4::metakind).
  This clears up a warning (private #inclusion) from the SMT and SMT2
  parsers, and maybe makes more sense anyways, since this is based on
  the kind (and not the metakind) of an operator.

* Documentation improvement; doxygen top-level \file gestures, \brief
  gestures for files, etc.  Changed contrib/update-copyright.pl for
  this change, and post-processed to add \brief.  Resolves bug #98.

* Removed ExprManager::mkExpr(Kind) and NodeManager::mkNode(Kind).
  They no longer made sense.  Resolves bug #91.

Missing files in last commit

Enabling RDL/IDL in SMT v1 and adding some simple tests

Implementing input from stdin (Fixes: #144)

Fixes 2 issues with assignments. The first is constructing an initial assignment for slack variables once solving has begun. (They cannot just be 0.) The second has to do with how assignments are backttacked.  Assignments are now tracked all of the time, and are frozen once they are known to be consistent, i.e. after a successful updateInconsistentVars().  Also added a fuzz test that shows both of these problems to the regressions.

Adds toString to DeltaRational

Fixes a bug where registration occurs before preregistration.

Changing ANTLR3 detection in configure (Fixes #147)

* Added NodeBuilder<>::getChild() to make interface more consistent
  with that of Node.

* If NodeBuilder<> hasn't yet been assigned a Kind, several member functions
  related to children now throw an IllegalArgumentException:

    * getNumChildren()
    * begin()
    * end()
    * operator[]
    * getChild()

  This is because if you later assign the NodeBuilder<> a PARAMETERIZED kind,
  the children are "reinterpreted" -- the first being an operator.  Interface-wise,
  it doesn't make sense to return one thing for nb[0], then later, after setting
  the kind, to return another thing for nb[0].

* Fixed unit tests depending on this behavior.

* Added a warning to the testing summary if unit tests didn't run (because this
  is likely due to compilation problems, and without a warning it looks kind of
  like a test success)

* VERBOSE wasn't exported to the environment for unit test "make check."  Fixed.

resolving bug 139: metaKindOf() warnings still exist, but it's probably a g++ 4.3 and 4.4 issue

added a handful of debugTagIsOn("context") checks to resolve bug 143

more VERBOSE test failures

Fixing test failures in production build

This commit adds a debugTagIsOn() guard around some extremely verbose debugging statements.  There is some evidence that these debugging statements were 20% of the running time for QF_LRA/miplib/fixnet-1000.smt in debug mode.

This commit is a fix for a bug in removeITEs().  The check that the then branch is a boolean should now be working. This fixes bug 138.

Adding SMT v2 parsing support for: QF_IDL, QF_NIA, QF_RDL, QF_UFIDL

Checking for executable permission on antlr3 script

Fixed a bug in partial_model.cpp where the data was immediately deallocated before being used.  Fixed a bug in node_builder.h's crop where a pointer is dereferenced after a realloc call.

Fixing failing test in r521
Adding general support for associative operators in SMT v1 and v2

In order for splitting on demand to be able to retract clauses every translation must indeed be a clause (if possible). I've changed the top level CNF conversion to generate clauses, instead of introducing unit clauses for each assertion.

First draft implementation of mkAssociative

Adding a couple of example from fuzzsmt to regress1.

Couple of fixes to theory arith. pivotAndUpdate now multiplies by a_kj. And the tableau now simulates older pivots while adding a new row.

After blasting the disjuncts, TheoryEngine rewrite needs to reinvoke itself. QF_LRA is now no longer complaining about seeing nodes that can be rewritten to CONST_BOOLEAN.

This update enables TheoryArith to accept assertions that rewrite to true or false. This is temporary and will be removed once TheoryEngine rewriting is more fully debugged.

Bug fixes for combining coefficients of rewritten nodes.

Added printModel() to src/theory/arith/partial_model.cpp.  This is a debugging utility that prints out the lower bound, upper bound, assignment, and the constraints that were asserted that caused the lower bound and upperbound to be asserted.

A few changes to the organization of TheoryEngine rewriting. A few bug fixes for it as well. make check should now work again.

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