add some stats to UF/CC

The "UF engineering issues" release, after much profiling.

* swap in backtracking data structures (that use and maintain their own
  undo stack) in some places instead of the usual Context-aware
  paradigm (MUCH faster).

* cosmetic changes to UF, CC modules.

Added Theory::presolve().

SmtEngine now fails with a ModalException if --incremental is not enabled
but a push/pop or multiple query is attempted (previously it could give
incorrect answers)

Also, fix some multi-query and push-pop tests that had wrong answers, and
support a new "% COMMAND-LINE: " gesture in regression tests so that a
test can pass additional, specific command line flags it wants to run
with (here, --incremental).

Also fix mkbuilddir script for when it's called from contrib/switch-config.

fix function signatures

cleanup from today's commits: delegate as-yet-unimplemented prettyprinters in a better way; fix arith Makefile

Changes to Solver and PropEngine to support lemmasOnDemand during solve but not yet in d_checkSat.

Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printer
implemented.  This new infrastructure removes support for pretty-printing
(even in the AST language) an Expr with reference count 0.  Previously,
this was supported in a few places internally to the expr package, for
example in NodeBuilder.  (Now, a NodeBuilder cannot be prettyprinted, you
must extract the Node before printing it.)

This commit merges the arith-prop-opt branch into the main trunk. This was done by way of the intermediate branch arith-prop-tmp. Both arith-prop-opt and arith-prop-tmp will now be phased out.

minor tweaks to last commit, testing infrastructure

fix some things with the build system (make dist, make install, make check)

Some bug fixes in the SAT for lemmas, and an experiment with a more complete (wr propagation) splitter in arithmetic.

make addsourcedir executable

Lemmas on demand work, push-pop, some cleanup.

command-line flag to disable theory registration, also SMT-LIBv2 compliance (per SMT-LIB mailing list this afternoon)

cleanup, documentation, SMT-LIBv2 compliance

fix out-of-date version/copyright for minisats

Moving Options fiddling to options.h

competition mode implies --no-checking

Moving the post_mortem.py script out of contrib and into the cvc4 scripts directory.

Updates post_mortem.py script to be able to handle certain kinds of crashes and new statistics.

This commit adds the ejected and un-ejected statistics.

Adds size() to RowVector.

Adds statistics for the number of Uservariables and Slack variables used by arithmetic.

Adds AverageStat to stats.h.

small fix to debug segfaults

enable dependence graphs in doxygen; fix lots of doxygen warnings, fix some documentation, and make it possible to "make doc" on a clean source tree (post-configure)

maximize stack limit, handle SEGV signals on an alternate signal stack, and try to diagnose stack overflow

Adds a hueristic from Alberto's thesis. For a fixed window the row count is used to select which non-basic variable is a row in made basic.

Fix for a problem caused by using a != instead of == in generateConflictBelow(). Resolves a bug introduced in -r1063.

portability updates to build system

Adds a very small test that triggers a bug. The bug is from the commit for -r1063.

minor fixes as a result of review of Chris's getType() rewrite; also fix some macros to make various GCC versions happy

Fixes RowVector::has().

Factors out the QF_LRA decision procedure from TheoryArith and puts this into its own class SimplexDecisionProcedure. Implements about 1/2 of the pivoting rule from Alberto's thesis (section2.5.3).

The Row implementation has no been replaced by RowVector and ReducedRowVector.  A RowVector is an array of ArithVar and Rational pairs. (This replaces a map based implementation in Row.) ReducedRowVector is a RowVector with a notion of having a basic variable.  The Tableau is now a collection of ReduceRowVector's.  A major difference between ReducedRowVectors and Rows is that the iterator now includes the basic variable and its coefficient (always -1). Before only nonbasic members were accessible by the iterator.

Changing NodeBuilder::debugCheckType() to maybeCheckType()
Changing NodeManager/ExprManager constructors to take Options

Disabling bottom-up algorithm in NodeManager::getType() when type checking
is not requested or eager type checking is enabled

fix confusing CXXTEST configure message, indicating success at finding cxxtest when it wasn't found.

Small change to documentation in NodeManager::getType

Slightly more efficient version of getType

make dist-building more pleasant (put .tar.gz in builds/ directory)

Changing dependency info in README

Modifying getType to use a non-recursive algorithm (Fixes: #228)

fix test Makefile

"make dist" fixes; a distribution tarball can now build and pass tests. "make distcheck" fails only because one of the "clean" targets needs work in test/unit

support focus on a particular subpackage (e.g. "expr")

inter-package dependence graph generation (in dot format)

GetValueCommand now gives a TUPLE as output, with the first operand the input expression and the second the value (resolves bug 227)

Cleaning up some header files

Adding dependency info to README

for static linking of driver binary, list libmain.a first (fixes link errors in last night's regressions)

missing case in expr output; resolves bug 226

Adding unit test for InteractiveShell

add a CVC4_UNDEFINED keyword, for intentionally undefined functions (like private copy constructors and assignment, for instance) that generates better, compile-time error messages if the function is used (before, you'd have to wait until link time); also some minor cleanup

Removed slack.h, and arith_activity.h. Replaced IsBasicManager with the more general ArithVarDenseSet.  Renamed NextArithRewriter to ArithRewriter.

Adding Parser::setInput and using it in InteractiveShell (Fixes: #225)
Removing ParserBuilder::withStateFrom

removing unused functionality from util; related to bug #222

fix valgrind-reported errors in parser builder; a non-SMT parser was always used (rather than an Smt or Smt2) regardless of input language

Saving state between lines in interactive mode (Fixes: #223)

Using Options in ParserBuilder and InteractiveShell

Merging main/getopt.cpp, main/usage.h, and smt/options.h in
util/options.h,cpp

Code cleanup for TheoryArith.

comment out the "interactive" check in SmtEngine::getValue() for now (resolves bug 224), and fix a comment in NodeManager header

Fixes to getValue for TheoryArith.

* Option --no-type-checking now disables type checks in SmtEngine
* Adding options --lazy-type-checking and --eager-type-checking
  to control type checking in NodeBuilder, which can now be enabled
  in production mode and disabled in debug mode
* Option --no-checking implies --no-type-checking
* Adding constructor SmtEngine(ExprManager* em) that uses default options

Changing --no-early-type-checking to --no-type-checking
Disabling type checking when --no-checking is given (Fixes: #221)

Enabling semantic checks in ParserBuilder

Adding detection of TTY vs. piped input for interactive mode

Fixing minor whitespace bug in the parser

Adding support for interactive mode

fix bug #220 (assertion fails if no query/check-sat); add bug220.smt2 and bug217.smt2 as regressions; fix to build system to only run regressions (not units) if you "make -C test regress", for example (this matches behavior elsewhere)

Fixed computation of infinitesimals for arithmetic model generation.

Removed vector<Monomial> monos from Polynomial.  Now using expr::NodeSelfIterator.

Added test/regress/regress1/arith and populated it with some fast SMT LIB problems.

with --stats, statistics are dumped for memouts and (normal) exceptions.

IDENTITY has been removed.

minor unit test fix-ups

fix debugPrintNode(), debugPrintTNode(), debugPrintNodeValue(), debugPrintTypeNode() -- thanks Tim for pointing this out

fix some leaks in parser, add debug code to node manager to find more

hooked up "we are incomplete" flag after conversation with Tim (a theory notifies the theory engine through its output channel); some cleanup; add a regression for bug #216

Merge from cc-memout branch.  Here are the main points

* Add ContextMemoryAllocator<T> allocator type, conforming to
  STL allocator requirements.

* Extend the CDList<> template to take an allocator (defaults
  to std::allocator<T>).

* Add a specialized version of the CDList<> template (in
  src/context/cdlist_context_memory.h) that allocates a list
  in segments, in context memory.

* Add "forward" headers -- cdlist_forward.h, cdmap_forward.h,
  and cdset_forward.h.  Use these in public headers, and other
  places where you don't need the full header (just the
  forward-declaration).  These types justify their own header
  (instead of just forward-declaring yourself), because they
  are complex templated types, with default template parameters,
  specializations, etc.

* theory_engine.h no longer depends on individual theory headers.
  (Instead it forward-declares Theory implementations.)  This is
  especially important now that theory .cpp files depend on
  TheoryEngine (to implement Theory::getValue()).  Previously,
  any modification to any theory header file required *all*
  theories, and the engine, to be completely rebuilt.

* Support memory cleanup for nontrivial CONSTANT kinds.  This
  resolves an issue with arithmetic where memory leaked for
  each distinct Rational or Integer that was wrapped in a Node.

check last result in (get-assignment); some context cleanup

use "forward" headers

additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supported; work on Result type (biggest noticeable change is that CVC4 now outputs lowercase "sat" and "unsat"), Options class moved to src/smt, to allow for future work on runtime configuration via (set-option) command

reverting some changes to parser from last commit

support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary define-fun; several set-info, set-option, get-option, get-info improvementss

fix to unit tests

bug fixes to model gen

Model generation for arith, boolean, and uf theories via
(get-value ...) SMT-LIBv2 command.  As per SMT-LIBv2 spec,
you must pass --interactive --produce-models on the command
line (although they don't currently make us do any extra
work).  Closes bug #213.

* (define-fun...) now has proper type checking in non-debug builds
  (resolves bug #212)

* also closed some other type checking loopholes in SmtEngine

* small fixes to define-sort (resolves bug #214)

* infrastructural support for printing expressions in languages
  other than the internal representation language using an IO
  manipulator, e.g.:

    cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << expr;

  main() sets the output language for all streams to correspond to
  the input language

* support delaying type checking in debug builds, so that one can debug
  the type checker itself (before it was difficult, because debug builds did
  all the type checking on Node creation!): new command-line flag
  --no-early-type-checking (only makes sense for debug builds)

* disallowed copy-construction of ExprManager and NodeManager, and made other
  constructors explicit; previously it was easy to unintentionally create
  duplicate managers, with really weird results (i.e., disappearing
  attributes!)

support (set-info) on status, source, category, difficulty, smt-lib-version, and notes; reduces extraneous "unsupported" output

oops, reverting a change to a regression test that had intentionally caused a typechecking violation

type checking for define-fun in production builds; related to (and might resolve) bug 212

NodeSelfIterator implementation and unit test (resolves bug #204); also fix ParserBlack unit test initialization

Small tableau optimization.

SMT-LIBv2 (define-fun...) command now functional; does eager expansion at preprocessing time

declare-sort, define-sort working but not thoroughly tested; define-fun half working (just need to decide where to expand)

parser and core support for SMT-LIBv2 commands get-info, set-option, get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...

fix gdb issues (at least for static builds); resolves bug 194