portfolio merge

readline links in -ltermcap -ltinfo too (fixes breakage in static-binary builds)

Added Theory::postsolve() infrastructure as Clark requested.
(Though currently unused.)

For theories that request presolve and postsolve (in their kinds file),
they will get a presolve() notification before the first check().  After
the final check during the current search, they get a postsolve().
presolve() and postsolve() notifications always come in pairs, bracketing
all check()/propagate()/getValue() calls related to a single query.  In
the case of incremental benchmarks, theories may get additional
presolve()/postsolve() pairs, but again, they always come in pairs.

Expected performance impact: none (for theories that don't use it)
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3598&reference_id=3581&p=5

By default, ONLY enable symmetry breaker ONLY for QF_UF (both SMT-LIBv1
and SMT-LIBv2).

There are --enable-symmetry-breaker and --disable-symmetry-breaker
options that are always respected regardless of this default.

Expected performance impact: positive

New default (UF only) compared to old default (always on):
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3594&reference_id=3595&p=5

Symmetry breaker remains a big win on UF:
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3594&reference_id=3596&p=5

The last link to results looks at first that the symmetry breaker should
always be turned off, since its use loses more regressions than it gains.
*However*, the lost ones are only our "QF_SAT" benchmarks.  For these, we
should indeed turn off the symmetry breaker, but that's impossible for
now because we tag them internally with the logic "QF_UF."

clarify wording in README, thanks for finding this Francois!

Last commit accidentally lacked r2778 and r2779 from integer2.  I have manually brought these changes over.  Changed the tests used by test/regress/regress0/arith/integers/Makefile.am to be 15 of the more interesting tests.  Did a bit of cleanup on TheoryArith to eliminate a warning and remove dead code.

This commit merges into trunk the branch branches/arithmetic/integers2 from r2650 to r2779.
- This excludes revision 2777.  This revision had some strange performance implications and was delaying the merge.
- This includes the new DioSolver. The DioSolver can discover conflicts, produce substitutions, and produce cuts.
- The DioSolver can be disabled at command line using --disable-dio-solver.
- This includes a number of changes to the arithmetic normal form.
- The Integer class features a number of new number theoretic function.
- This commit includes a few rather loud warning. I will do my best to take care of them today.

precision in theoryskel

proper handling of improper get-value

copyright year updated to 2012

separate new-theory components into a "theoryskel" directory so that new files can be added to it without modifying the script.

ensure using bash for new-theory script

attempt at a fix for the local regression failure (CLN linking issues on oneiric

script to ease creating a new theory from scratch (will go along with new reference documentation)

correct comment typo found during today's architectural meeting

fixing antoher small bug in backtracking

fixing a bug in uf_engine application lookup backtracking
this should also fix bug299

Number of changes to cvc_printer.cpp. Specialized the printing for BVPLUS, BVSUB, and BVMULT.  Fixed a bug in printing on PREFIX operators. Added parenthsis for POSTFIX operators. Passing the ouroborous test now.

re-adding comment about available languages

removing the 100 integer benchmarks from regress0, too many

fixing some missing stuff

Fixing a bug in the integer unit tests when configured for GMP with assertions off.

changes to the cvc4 language printer, so that it actually prints the cvc4 language
all theory writers should take a look a what's being printed, to ensure all cases are covered

support for isWellFounded/mkGroundTerm on uninterpretted sorts.  cvc4 now assumes uninterpretted sorts are well-founded, allowing datatypes to work with uninterpretted sort subdata

updating configure to use python-config for building python bindings

effecting the same change in the compat Java binding as was done to CVC3 yesterday (ValidityChecker::value() and ValidityChecker::getValue())

Adding regress1 test ooo.rf6.smt2.

Partial fix to TheoryEngine::getExplanation so that SharedAssertions request explanations from the theory that can explain them. This partially fixes bug 295.

fix for bug295

updates to smt2 parser to support datatypes, minor updates to datatypes theory/rewriter to support datatypes with non-datatype subdata

Partial fix to bug 295.

Fix to the previous commit.

Partial fix in arithmetic for propagating shared terms. This partially resolves bug 289.  Adds failing tests to regress1.

added minor documentation for parametric datatypes, for bug 283

minor fixes to printing and parsing of CVC-language defined functions and lambdas; resolves bug 294

some more bug fixes (TNode -> Node, normalize literals in explanations)

* merging some uf stuff from incremental_work branch that somehow nobody merged-in
* since two theories can propagate the same literal minisat now explicitly checks that a propagated literal has not been asserted yet

adding additional checks for theories propagating literals that already have a value

a bit more changes, when propagting equalities/dis-equalities don't assert them to theories that rewrite them to true. for example, 1 != 0 rewrites to true, so it shouldn't get propagated to arithmetic.

attempt to fix bug 293: if a split on a trivial shared pair is requested from a theory, such as 1 = 0, it is reasserted to the theory.

Disable a BV rewriter statistic (after checking with Liana) that was static,
and thus caused big problems with programs that create two SmtEngines in
one process.

If we need state like this in the rewriters, we'll need to make them
nonstatic.

LemmaStatus changes, as agreed to during 12/2 meeting.

oops, removing some integer operations that leaked in (they aren't part of trunk yet)

fix errors in smt-lib2 output; needed for debugging

change short-circuiting behavior of Command execution in the main driver; allows a (limited) form of error recovery, matching what we had previously

Error detection is different now---with new Command infrastructure, exceptions are not thrown outside the library.  Reflect this in the exit code of the driver.  Fixes a bug found by Tim among the nightly regressions.

Also improved error reporting if antlr is unavailable and the parsers need to be generated.

disable bug288.smt so that "make check" goes through---pending integers merge, see bug #288

fix linking errors on oneiric

Simplified bug288.smt to reflect the problem in integers better.

Added a failing regression test corresponding to bug 289.

Adding a failing UFLIA benchmark corresponding to bug #288.

Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic now supports propagating equalities when a slack variable corresponding to a difference of shared terms must be 0. Similarly disequalities are propagated when these variables cannot be zero.

Fix Java JNI installation path

fix module name for CVC4 jar file; part of the fix for the Debian package build failure last night

More language bindings work:

* with a patched SWIG, the ocaml bindings build correctly.
** I will provide my patch to the SWIG dev team.
* fixed some class interfaces to play more nicely with SWIG.
* php, perl, tcl now work; examples added.
* improved binding module building and installation.

Also:

Stop #defining NULL ((void*) 0).  This has been in cvc4_public.h for
a long, long time, I forget why I added it in the first place, and
it's a very, very bad idea.  In C++, certain things are permitted
for NULL that aren't permitted for ((void*) 0), like for instance
implicit conversion to any pointer type.  We didn't see an issue
here (until now, when interfacing with SWIG), because GCC is usually
pretty smart at working around such a broken #definition of NULL.
But that's fragile.

New exception-free Command architecture.  Previously, some command
invocations were wrapped in a try {} catch() {} and printed out an
error.  This is much more consistent now.  Each Command invocation
results in a CommandStatus.  The status can be "unsupported",
"error", or "success" (these are each derived classes, though, not
strings, so that they can be easily printed in a language-specific
way... e.g., in SMT-LIBv2, they are printed in a manner consistent
with the spec, and "success" is not printed if the print-success
option is off.)  All Command functionality are now no-throw
functions, which @cconway reports is a Good Thing for Google
(where all C++ exceptions are suspect), and also I think is much
cleaner than the old way in this instance.

Added an --smtlib2 option that enables an "SMT-LIBv2 compliance
mode"---really it just sets a few other options like strictParsing,
inputLanguage, and printSuccess.  In the future we might put other
options into a compliance mode, or we might choose to make it the
default.

Fix "make dist".  Fixes to python and ruby bindings; ruby example written.  They should both work out of the box, now, with swig 2.0.4 at least.  "make install" likely still needs to be adjusted to install them sensibly.

Addressed many of the concerns raised in the public interface review of CVC4 Datatypes (bug #283) by Chris Conway.  Thanks, Chris!

fix to build system for java bindings

* Applying Andy's fix for datatypes bug #286; thanks for the quick work, Andy!
* Also some better configure script wording

Bindings work (ocaml bindings are now sort of working); also minor cleanup

additional minor changes to get python binding on better footing

fixes for python language binding, added python example

public tests need to be linked against gmp/cln explicitly---looks like a subtle linker change in Ubuntu 11.10 oneiric :-(

datatype stuff in compatibility interface implemented

Context::ScopedPush implemented (in support of theory speculation, like upcoming internal branch-&-bound for integers)

STRING_TYPE and CONST_STRING and associate type infrastructure implemented.

Only print a shortlist of most-commonly-used options on option processing errors; reduces clutter, increases usability

give an option error if the user specifies --proof in a non-proof-enabled build

fully implement the always-check-again-after-the-output-channel-is-used fix for bug #275.  will finally close #275.

Sometimes antlr decides to generate lexers and parsers in a different directory than specified by "-o dir" ?!   Fix that by specifying "-fo dir".

better Integer asserts when there's overflow on conversion to unsigned long / long

Improvements to header installation on user machines.  Internally, we can
still write, for example:

#include "expr/node.h"

but public CVC4 headers, upon installation to /usr/include/cvc4 (or wherever),
have such #includes rewritten automatically to:

#include <cvc4/expr/node.h>

fixes to assertions in GMP to match CLN behavior

Added assertions to the CLN implementation of Integer for getLong() and getUnsignedLong().

another make distclean fix

fixes to "make distclean" and "make maintainerclean"

fix to "make install"

fix some doxygen warnings

support for proof regressions in other parts of the test tree

fix unit tests

Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, SmtEngine::getProof(), a few other things..

proof regressions

* ability to output NodeBuilders without first converting them to Nodes---useful for debugging.
* language-dependent Node::toString()
* some minor proof-related cleanup

merged the proofgen3 branch into trunk:
    - can now output LFSC checkable resolution proofs
    - added configuration option  --enable-proof
    - added command line argument --proof
To turn proofs on build with proofs enabled and run with --proof.

Adding a check in Polynomial::parsePolynomial to better enforce the arithmetic normal form when assertions are enabled.

Initialize resource limit and millisecond limit options

Implement changes from yesterday morning's meeting (10/21/2011):

* OutputChannel::lemma() now returns an unsigned int.  This facility isn't functional yet, but the signature is there.  For now, it always returns the current user level (which is "correct" from the interface point of view, but not what we want).
* Pseudobooleans disabled.  This should fix some quantifier benchmarks Andy's been working with on the quantifiers2 branch.
* --limit / --time-limit options renamed --rlimit and --tlimit.

There may be slowdown from disabling pseudobooleans.

some printing and parser fixes for problems recently uncovered

add gcc version information to Configuration, and warn when building with v4.5.1 which has a buggy optimizer (resolves bug #266)

add support for QF_AUFLIA and QF_AUFLIRA logic strings in SMT inputs, for testing

fix configure step on Ubuntu oneiric (11.10)-- related to bug #284

fix bug #264: competition / other static library builds when readline isn't available

Adding support for QF_UFLIA to the smt2 parser.

Merging the branch branches/arithmetic/push-pop-support from r2247 to r2256 into trunk.  Arithmetic should now be closer to being able to support push and pop.

Sharing work

fix make dist

Interruption, time-out, and deterministic time-out ("resource-out") features.
Details here: http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_October_14,_2011#Resource.2Ftime_limiting_API
This will need more work, but it's a start.

Also implemented TheoryEngine::properPropagation().

Other minor things.

Some new Datatype public functionality, as per Chris Conway's suggestions on the dev mailing list.

don't build language bindings unless expressly requested with --enable-language-bindings

Reverting a fix from earlier today that fixed a Mac OS warning but completely broke Linux. :-(