adding cache for preprocessing datatypes terms to fix bug 475, fix for handling user attributes in quantifiers (was broken)

(cherry-picked from commit 206edb6f11674e954f5762a1db9712131151a276)

Fix bug 476: when CxxTest is not found, make the error less fatal-looking

Fix to portfolio builds
(cherry picked from commit f46ba71e78054af63b529eb3271952c55beba37e)

Fix performance issue in a DFS search (bug 474)
(cherry picked from commit f056522a587d1b080224992355be070b73d97a3b)

* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issues
* build bugfix for win32
* also fix a bug re: tuples and records in the datatypes rewriter

These fixes are for both trunk and 1.0.x branches.

(cherry picked from commit 8c8985f024cec925f774ff32ebccc306be8e4b26)

distribute the find_public_interface.sh script
(cherry picked from commit af44cd27d5b079f1279c407e610e557e81285d8f)

version numbering
(cherry picked from commit 4cae70d893601a2070dc2b00c5640b48515b1a22)

Fix for fuzzer-found model bug

(cherry picked from commit 25c6e1331d338c6ba8d60224711343986e11cf79)

Cutting release 1.0.

fix cut-release sanity checks

fix to TNode assertion (which is too strict, given lax ordering requirements on static data initialization)---this should fix debug-staticbinary Mac builds, maybe others

Throw a logic exception if user makes an assertion using a STORE_ALL

remove instantiator framework

(this commit was certified error- and warning-free by the test-and-commit script.)

Fix the way abstract values are typed; fixes some compliance issues.

Also support array-store-all for Boolean terms (related to abstract values, since that's the only way for the user to include an array-store-all in an assertion).

(this commit was certified error- and warning-free by the test-and-commit script.)

fix memory corruption issue in debug builds that led to unhelpful output

remove an obsolete (and incorrect) assertion in boolean-terms; also add failing regression for bug 472

fix java system test dependences

drastic simplification of quantifiers code regarding equality queries, instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine

Fix for a CLN related bug on 32 bit systems. Integer((1<<29)+1) and Integer((long int)((1<<29)+1)) gave different values.  This was confirmed on vm-int1.cims.nyu.edu. See ginac.de/CLN/cln_3.html#SEC15 for more details. rational_white and integer_white have tests covering this.

Some fixes for boolean arrays

also a regression for bug 411

(this commit was certified error- and warning-free by the test-and-commit script.)

fix #line annotation warning

updated examples

added a new example for the combination of bit-vectors and arrays (includes model generation) and set the logic for the bitvector example

another part of last commit

definition-expansion fixed for get-model, resolves bug 411

Polishing API examples.

Adding SmtEngine::setLogic(const char* logic) so that smt.setLogic("QF_LRA"); works.

Fixes for stricter compilers Andy brought to my attention.

Changing the documentation of ARR_TABLE_FUN to say (internal symbol).

all API examples now have java versions too; bitvectors gets built; also updated old-style copyrights in the examples

incorporating some comments from Clark

Fix assertion in smt_engine's getValue
Minor changes to RELASE-NOTES

Updating the combination.cpp example.

Committing tests to potentially discover an obscure CLN library issue on 32 bit platforms. The issue is discussed here: ginac.de/CLN/cln_3.html#SEC15.

renaming --smtlib to --smtlib-strict; removing --smtlib2 option

internal variables (skolems) aren't printed as part of the model

(this commit was certified error- and warning-free by the test-and-commit script.)

change detection/handling of output language more reasonably; fixes a nagging bug Tim found in API examples

(this commit was certified error- and warning-free by the test-and-commit script.)

quantifiers now uses master equality engine, preparation work to cleanup code

parametric datatypes fix related to non-ascribed type constructors introduced by decision procedure

added a simple API example example showing how to use the bit-vector theory.

Changes to SExpr to accept autoconversion from bool and const char*. Adding an example for combination.

Adding smtname level options for tlimit, rlimit, etc. Fix to the internal documentation in base_options.

Partial fix for bug 435; still needs some effort.

(this commit was certified error- and warning-free by the test-and-commit script.)

Add some regressions for bug 438.

(this commit was certified error- and warning-free by the test-and-commit script.)

fix rewrite-rules syntax in regression

minor fix to release script

fix the syntax of assert-rewrite/-propagation/-reduction by putting the pattern first
just after the bindings

 Do it before the release in order to not break user files later

reliable benchmark corresponding to bug468

require type ascriptions for parametric datatype constructors (making them canonical), this fixes the followup issue of bug 438

Fix for hidden symbols in library on Mac.  It's a strange issue to do with
explicit template instantiation rules, -fvisibility=hidden, and the way that
Apple distributes libstdc++.

(this commit was certified error- and warning-free by the test-and-commit script.)

fixes bug 438, incorporate subtypes into type unification when typechecking parameterized datatypes

fix for andy: boolean terms stuff really shouldn't look at datatypes at all in this release

minor documentation fix

svn:ignore property

Fix for nasty corner case found by fuzzer...

Hack to support global variables for CVC language extended to export mechanism.
- Adds GlobalVarAttr node attribute

(this commit was certified error- and warning-free by the test-and-commit script.)

Fixing function models with Boolean terms.  Also, LAMBDA's should not be const.

Adding the helloworld.cpp example.

fix a potential race (have failed to reproduce)

Fix for getValue.  Now it can handle lambda applications

Attempted "quick-fix" for QF_UF performance regression since Boolean terms added.

Sharing is turned on only when Boolean terms are detected during preprocessing.  QF_UF problems (and others)
that don't use any Boolean terms won't have BV turned on.

(this commit was certified error- and warning-free by the test-and-commit script.)

treat all get commands like getValue (send only to lastWinner)

minor

update to release notes

Bug fix:
* Fix creation of bound variables in CVC native language parser
* This corrects a problem with misleading model output

(this commit was certified error- and warning-free by the test-and-commit script.)

fix: correct misleading comment in dump output

Functions and predicates over Boolean now work with --check-models and output correct
models for such functions (though they are somewhat ugly at present).

There's still a problem with model extraction, but it's not Boolean terms' fault.
Sometimes checkModel() can report that the model is just fine, but if a user extracts
values with getValue(), they find problems with the model (i.e., it doesn't satisfy some
assertions).  This appears to be due to an asymmetry between how checkModel() works and
how Model::getValue() works.  I'll open a bugzilla report to discuss this after thinking
some more on it.

(this commit was certified error- and warning-free by the test-and-commit script.)

fix in CommandSequence invoke : maintain success/failure. Fixes bug 465.

(this commit was certified error- and warning-free by the test-and-commit script.)

more mac fixes

fix for some Mac builds

Simplify --help=decision with only currently supported options

Add notice/warning when using incremental-mode + decision (it was
already disabled)

Some other minor cleanup

(this commit was certified error- and warning-free by the test-and-commit script.)

give warning at configure-time about unsupported language bindings, and don't advertise them in help listing for --enable-language-bindings

do not turn on BV for QF_SAT

(this commit was certified error- and warning-free by the test-and-commit script.)

First chunk of boolean-terms support.

Passes simple tests and doesn't break existing functionality.
Still need some work merged in for models.

This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV).  Tonight's nightly regression run should tell us if/how that hurts performance.

(this commit was certified error- and warning-free by the test-and-commit script.)

Tuples and records merge.  Resolves bug 270.

Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together.

(this commit was certified error- and warning-free by the test-and-commit script.)

Adding an example to show how to use arithmetic.

Improved implementation of Integer::length() with CLN enabled.  Additional tests to sanity check both versions CLN and GMP versions of length.

include new regression directories in summary test output

rolling back r4625 for now (closes bug 464), Andy we should talk about this a bit more..

fixup for incremental solving

Removing DioSolver::acceptableOriginalNodes(). This assertion was too strong, and was broken by r4620. This commit resolves bug463. Adding a previously triggering test case.

Adding support for a master equality engine. Each theory gets the master equality engine through the setMasterEqualityEngine method. This is a read-only equality engine, so nothing should be added to it directly. Instead each equality engine that is of interest should have the master equality engine attached to it. To set when to use the master equality engine see TheoryEngine::finishInit().

Improving arithmetic debugging output.

Disabling test/regress/regress0/push-pop/bug396.smt2. This takes 2m to run in debug mode. This is too long for a regress0 test.

don't include internal variables in model output

some fixes to language bindings and function visibility

Makefile fix for new versions of Make (thanks Clark for noticing this); see e.g. osdir.com/ml/bug-make-gnu/2011-04/msg00011.html

Adding a regression test from bug 462.

This commit fixes two incompleteness bugs (461, 459) introduced in r4611 dues to a problem of not correctly handling disequalities.  Performance implications are uncertain.

Adds ensureConstraint(...) to ConstraintDatabase. This is a slightly optimized way of doing getConstraint() if the user already has a ValueCollection&.

Example of rewrite rules use that comes from an harness test

- Removes getDeltaValueWithNonlinear() entirely
- Changes the signature of getDeltaValue to throw DeltaRationalException and ModelException
-- DeltaRationalExceptions can occur with non-linear arithmetic computations that cannot be done. (0 + delta) * (1 + delta) is not a DeltaRational.
-- ModelExceptions occur if getDeltaValue() is going to return a value that disagrees with its value in the model (due to non-linear arithmetic)
-- ModelExceptions also occur if getDeltaValue(n) is called on a variable arithmetic has never seen before.
- getEqualityStatus() now wraps and catches both of these exceptions. If either occurs, the equality status is EQUALITY_UNKNOWN. This allows arithmetic to handle terms it has never seen before in getEqualityStatus. This resolves bug 453.
- Removes the dead code rowImplication() entirely.

Adds a number of new capabilities to DeltaRational. This adds DeltaRationalException which can be called when an operation on a DeltaRational does not have well formed semantics. This allows for things like multiplying two DeltaRationals, which may or may not result in a DeltaRational.

Added debugging output to --check-models. I've found this output quite useful while debugging.

Run lastWinner thread for all commands. Earlier behavior was to run
lastWinner only for (get-model) command, using thread0 otherwise.

Adding hand minimized test for bug 450.

Changed the splitting-on-demand lemmas of arithmetic to no longer contain the equality being split on. Instead of issuing 'x != y implies (x < y or x > y)', the lemma is now '(x <= y or x >= y)'. This resolves bug 450.

Fix for bug452.

Disable predicate subtyping:
* remove from public interface (ExprManager, Type)
* CVC parser reports an unimplemented feature error if used

I didn't want to tear it out completely (from NodeManager, TypeNode,
type-checking, pre-processing, etc.) because that's a lot of hassle
and we'll add it back in after the release anyway.  It *does* mean
that CVC4::Predicate is in the public interface, but that it can't be
used for anything (by users).

(this commit was certified error- and warning-free by the test-and-commit script.)

support for quantifiers macros, bug fix for bug 454 involving E-matching Array select terms (thanks for the bug report Francois)