Adding static_fact_manager

Clark's work on array theory - can now solve all QF_AX problems

fix some confusing debug output (bogus counter)

mark the new minimized benchmark as unsat

if running in QF_AX, equalities over terms of uninterpreted sort go to arrays, as well as pre-registration of free constants of uninterpreted sort, etc..

minimized example

array benchmarks

adding disequality propagation

relevant comparison http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2602&reference_id=2590&p=5

merge from symmetry branch

Reverting mistaken check-in

changing the sat solver remove clauses constants
with these we get closer to yices on uf and it seems better on lra

vs yices uf http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2590&category=&p=5&reference_id=1471
vs trunk on lra http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2591&category=&p=5&reference_id=2576

Fixed bug in default solve - wasn't returning when it was supposed to

another typo

yet another uf bug fix, hopefully the last

another bugfix for uf

some immediate bug fixes

fix submission makefile

minor fixups

surprize surprize

removing duplicate clauses in ite cnf conversion

cudd-building prefs with --with-cudd / --without-cudd

Fixing two bugs:

1) arithmetic should check for subterms when solving equations, for instance x = if b then x + 1 else x -1 is not a valid substitution
2) a memory problem in minisat - explanations are constructed during conflict analysis, so the clause database might resize and relocate, which invalidates any references to clauses

missing test case

updated preprocessing and rewriting input equalities into inequalities for LRA

Allow (- x) for unary minus in SMT-LIBv1, in addition to the standard (~ x),
when --strict-parsing is off (which it is by default).  The danoint benchmarks
have such monsters.

Changed the defaults for arithPivotThreshold and arithPropagateMaxLength to 16. Enabled arithmetic propagation and variable removal by default. Changed the command line arguments for both propagation and variable removal allow for disabling these.

Merging the playground branch upto r1957 into trunk.

only use theory registration if (1) a theory requests it, or (2) if there's more than one "real" theory (not BUILTIN or BOOL) active

some things I had laying around in a directory but never got committed; minor fix-ups to documentation and some node stuff

Fixed spelling mistake and documentation for --enable-variable-removal.

Some fixes inspired by Fedora 15:
* compilation fixes for GCC 4.6.x
  + ptrdiff_t is now in std::
* fix some make rules that are ok in Make 3.81 but broke in Make 3.82
* look for cxxtestgen.py as well as cxxtestgen.pl, and look for cxxtest headers in /usr/include

compilation fix for x86 (from previous commit)

Fix for Mac OS breakage (x86 didn't crash, but probably would, eventually, on some problems---valgrind gave many complaints): the problem was that calloc() (in the Backtracker) wasn't allocating enough space for the type located at the resulting address.  Resolves bug #263.

Also, some debugging improvements.

fixed various bugs related to ambiguous parametric datatype constructors, parametric datatype versions of paper benchmarks are now working

datatypes work

minor fix to build system for system tests

added (temporary) support for ensuring that all ambiguously typed constructor nodes created internally are given a type ascription

minor fix, and better output for type errors

type ascriptions (casts) for parameterized datatypes, e.g. "nil :: list[INT]

This commit contains the code for allowing arbitrary equalities in the theory of arithmetic.
* This code has been partially tested. (My testing situation is currently not so great.)  The code for testing not preregistering equalities can be compile time enabled by setting the boolean turnOffEqualityPreRegister. Don't be shocked by slowdowns or failures.  This does pass make regress as well as a fresh checkout does. (The Mac version has issues.)
* I need to disable the permanent row removal heuristic by default.  We need to discuss why this needs to happen.  We should probably detect pure QF_LRA/QF_RDL problems and enable this when this can safely be done.
* I have disabled the arithmetic rewrite equality flag.  This code needs to be added to the parser.
* For all of the above changes, I have annotated the code with the key word BREADCRUMB.
* I have renamed ArithUnatePropagator to ArithAtomDatabase.

fix unit test linking issue

include subversion information used for each build in the --show-config output and as a banner in --interactive mode; intended to resolve confusion in cases where you don't know where a CVC4 binary came from

apply arithmetic static learner's miplibtrick in a consistent order (for easier replication of experiment)

fixes for "make dist" and "make doc", minor cleanups

Merge from arrays2 branch.

fix production-build compiler warning

re-add a removed Datatype constructor that was causing a unit test failure, so nightlies go through tonight

reverting node manager change from 1881; also part of parameterized datatypes review

add AscriptionType stuff to support nullary parameterized datatypes; also, review of Andy's earlier commit, with some minor code clean-up and documentation

added support for parametric datatypes, updated cvc parser to handle parametric datatypes, type ascriptions are not implemented yet

* fix for Mac OS (includes some ThreadLocal stuff copied in from portfolio
  branch)
* add Theory::isSharedTermFact() -- it currently always returns false,
  pending theory combination work
* Add "unknown" cardinalities to Cardinality class
* Fix run_regression script to handle CRLF line terminators on Macs
  (where sed is non-GNU)
* Convert CRLF line terminators in datatypes regressions to LF

Deleting dead code.

added 10 benchmarks to regress/regress0/datatypes from paper

significant revisions/improvements to code for theory datatypes solver

Merge from nonclausal-simplification-v2 branch:

* Preprocessing-time, non-clausal, Boolean simplification round to
  support "quasi-non-linear rewrites" as discussed at last few meetings.

* --simplification=none is the default for now, but we'll probably
  change that to --simplification=incremental.  --simplification=batch
  is also a possibility.  See --simplification=help for details.

* RecursionBreaker<T> now uses a hash set for the seen trail.
* Fixes to TLS stuff to support that.
* Fixes to theory and SmtEngine documentation.
* Fixes to stream indentation.
* Other miscellaneous stuff.

luby sequence generator; can use to plot MiniSat's restart sequence

Stronger support for zero-performance-penalty output, and fixes and
simplifications for the "muzzled" (i.e. competition) design, which had
been broken.  Addition of some new unit test bits to ensure that
nothing is ever called in muzzled builds, e.g. things like

  Warning() << expensiveFunction();

Also, fix some compiler warnings.

output fixes for performance

minor updates to exp manager, fixed 32bit vs 64bit issues in transitive closure module, theory datatypes now uses transitive closure for cycle detection, bug 261 fixed

fix for configure

adding some previously-failing "bug" test cases for bitvectors

updating bv regressions

parser fixes for bug 243

updates for bitvectors

more minor fixes related to last few commits

another small fix

fix broken build; sorry, all!

fix a performance issue from last commit

Minor fixes to various parts of CVC4, including the removal of the uintptr_t constructors for Type and Expr (which existed due to ANTLR limitations).  These issues are now handled (as a hack, due to said limitations) in the parser rather than the CVC4 core.

minor fixes, plus experimental readline support in InteractiveShell

refactoring to datatypes theory, added working prototype for proof/explanation manager

more fixes/improvements to datatypes theory and transitive closure

cleaned up some of the hacks in the datatypes theory solver, working on using Transitive Closure to detect cycles, added rewrite rule for disinguished ground terms

Monday tasks:

* new "well-foundedness" type property (like cardinality) specified in
  Theory kinds files; specifies well-foundedness and a ground term

* well-foundedness / finite checks in Datatypes now superseded by type
  system isFinite(), isWellFounded(), mkGroundTerm().

* new "RecursionBreaker" template class, a convenient class that keeps
  a "seen" trail without you having to pass it around (which is
  difficult in cases of mutual recursion) of the idea of passing
  around a "seen" trail

small unit test fix; was broken only in non-assertion, non-CLN builds

Weekend work.  The main points:

* Type::getCardinality() returns the cardinality for for all types.
  Theories give a cardinality in the their kinds file.  For
  cardinalities that depend on a type argument, a "cardinality
  computer" function is named in the kinds file, which takes a
  TypeNode and returns its cardinality.

* There's a bitmap for the set of "active theories" in the
  TheoryEngine.  Theories become "active" when a term that is owned by
  them, or whose type is owned by them, is pre-registered (run CVC4
  with --verbose to see theory activation).  Non-active theories don't
  get any calls for check() or propagate() or anything, and if we're
  running in single-theory mode, the shared term manager doesn't have
  to get involved.  This is really important for get() performance
  (which can only skimp on walking the entire sub-DAG only if the
  theory doesn't require it AND the shared term manager doesn't
  require it).

* TheoryEngine now does not call presolve(), registerTerm(),
  notifyRestart(), etc., on a Theory if that theory doesn't declare
  that property in its kinds file.  To avoid coding errors,
  mktheorytraits greps the theory header and gives warnings if:
  + the theory appears to declare one of the functions (check,
    propagate, etc.) that isn't listed among its kinds file properties
    (but probably should be)
  + the theory appears NOT to declare one of the functions listed in
    its kinds file properties

* some bounded token stream work

fix for parser/tests for ANTLR 3.2 (it was working fine on 3.3)

* reviewed BooleanSimplification, added documentation & unit test
* work around a lexer ambiguity in CVC grammar
* add support for tracing antlr parser/lexer
* add parsing support for more language features
* initial parameterized types parsing work to support Andy's work

make run_regression script robust to DOS newlines :(

added fixes for datatype theory solver to account for rewriting before finite/well-founded check.

fix to last commit

Fixing SmtEngine::getValue() by adding a NodeManagerScope (thanks Tim for finding this)

numerous bugfixes

incorrect usage of C++ std::string caused a test to fail

Minor mixed-bag commit.  Expected performance impact negligible.

* Fixed hole in arrays typechecking.
* Fixed "make dist".
* Better ouroborous test, and some printer fixes.
* Continued cleanup in CVC parser, removed some warnings.
* Better output.

Tuesday end-of-day commit.

Expected performance impact outside of datatypes/CVC parser is
negligible.

* CVC language LAMBDA, functional LET, type LET, precedence fixes,
  bitvectors, and arrays, with partial parsing support also for
  quantifiers, tuples, subranges, subtypes, and records
* support for complex recursive DATATYPE selectors, e.g.
    tree = node(children:ARRAY INT OF tree) | leaf(data:INT)
  these are complicated because they have to be left unresolved
  at parse time and dealt with in a second pass.
* bugfix for Exprs/Types that occurred when setting them to null
  (not Nodes/TypeNodes, just Exprs/Types).
* Cleanup/code review items

Removing dead code that came in on commit r1740.

more work on CVC language

mostly CVC presentation language parsing and printing

This commit merges the branch arithmetic/propagation-again into trunk.
- This adds code for bounds refinement, and conflict weakening.
- This adds util/boolean_simplification.h.
- This adds a propagation manager to theory of arithmetic.
- Propagation is disabled by default.
- Propagation can be enabled by the command line flag "--enable-arithmetic-propagation"
- Propagation interacts *heavily* with rewriting equalities, and will work best if the command line flag "--rewrite-arithmetic-equalities" is enabled.

Partial merge from datatypes-merge branch:

1. Defines a new type "DatatypeType", a type-constant that holds a Datatype, describing an inductive data type.
2. CVC language parser supports datatypes.
3. CVC language printer now functional.
4. Minor other cleanups.

No performance impact is expected outside of datatypes.  I'm verifying that that is the case with a cluster job this morning.

Fixing output for EOF token in parser errors

also a fix for a system test related to ParserBuilder

unit test fixes for new NodeManager constructor (related to previous two trunk commits)

parser/driver fixes for last commit

partial merge from portfolio branch, adding conversions (library-internal-only of course) between Exprs and Nodes, Types and TypeNodes, ExprManagers and NodeManagers.

reverting back the minisat code and adding a simpler one that shouldn't change the search

Three things:
1. Infrastructure for unit T-conflicts added to SAT proxy
   (and also the theory output channel documentation);
   previously theories could not communicate unit T-conflicts
   with the SAT layer because that layer had an implicit
   assumption (not asserted) that the conflict nodes were an AND.
2. UF now pre-rewrites trivial equalities to "true".  These could
   conceivably occur in artificial benchmarks in this form:
     (let (?x BIG-HUGE-TERM) ... (= ?x ?x) ... )
3. The SMT-LIBv2 printer now properly prints Bool constants.

fixing an uninitialized literal variable

adding support for unit conflicts in minisat...