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)

Fixed last currently known bug in array models

* enable previously-failing (now succeeding) datatype example that uses records
* some bindings cleanup

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

fix for language bindings (fixes debian build fail last night)

* Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ALL_SUPPORTED logic
* Java bindings fixes: fixed access to ostreams, iterators
* Make SmtEngine::setUserAttribute() (and others) take a const string&
* Also a few compliance fixes

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

Fix for bug451

fixing and refactoring the equality iterator

Fix dumping of array-select expressions in CVC native language.
Thanks to Wei for the bug report.

fix a compiler warning in models

some fixes for --threads=1

fix for "make examples"

More fixes to model generation, with previously failing testcases
Also refactored some header file includes to reduce compile time

forgot to uncomment setLogicInternal for THEORY_BV

changed logic options so that justification is turned on for QF_ABV and QF_UFBV as well

d_incomplete is context-dependent; we shouldn't be saving its value and restoring after a flipDecision().

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

fuzz15 should have been fuzz14

Fix for bug 447.

Fixed another AUFBV model bug.  BV equality subtheory needed to do something
similar to arrays - limit the set of terms reported to those relevant in the
current context.  Also removed collectModelInfo from sharedTermsDatabase -
doesn't seem to be needed any more.

Fixing comments in print_lambda.cvc.

Fix for bug 407. mkAnonymousFunction() in the parser no longer uses ':'. CVC printer now properly prints LAMBDAs. Model builing now gives bound variables names that can be parsed bypresentation language.

replaced all static member data from rewrite rule triggers, added infrastructure for recognizing quantifier macros

Fixed a typo in r4576

Beautifying smt_engine.cpp.

Fix to bug449. Adds shared constants to the set of DeltaRationals that must be in the final total order.

bug fixes to models, array rewriter with previously failing testcases

Quantifiers enabled with portfolio, closing bug 423.

fix a race problem. due to interrupt mechanism minisat returned true instead of undef.

More bugfixes for models

SmtEngine::checkModel() should only be called if the result is sat or unknown because of incompleteness. Other unknown results are not safe to build models for, timeout, interrupted, etc.

refactoring of quantifiers rewriter based on code review from yesterday, refactoring code out of instantiators in preparation for quantifiers equality engine

fixed failed bv regressions by refactoring out some rewrite rules from smt_engine.cpp

added support for division by zero for bit-vector division operators

Relaxing too-strict assertion

Fixed an array rewriting bug found by fuzzer

Testcases for fixed bugs

Fixed bug in array constant normalization found by fuzzer.

Improved error reporting for improperly using non-linear division in linear arithmetic.

Delta is now generated in arithmetic to keep consistent the total order of DeltaRational values for lowerbounds, upperbounds, assignments and disequalities.  Throws LogicException when a non-linear term is asserted and the the LogicInfo isLinear() disagrees.

changed BitVector::unsignedRem to match the behavior of the bit-blasted circuit for division by 0; temporary fix for bug440

Fix for bug 444, dealing with the placing of set-logic in dumping modes.
CVC4 now produces equivalent output when dumping the SMT1 and SMT2 attachments to that bug report.

This also fixes a memory leak in the new-variable-notification mechanism.

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

* Fix language bindings: various issues
** remove a number of warnings in bindings generation
** give appropriate names for operator-overloading
** make sure Java language bindings are built with -fno-strict-aliasing, to ensure the optimizer doesn't produce bad code

* Also remove BitVector::equals(), which wasn't used and was inconsistently implemented (operator==() is still there).

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

minor bug fixes for quantifiers, added sort inference module (not ready to be used yet), added new totality lemma option for uf strong solver

Fixes for the arithmetic normal form and rewriter to handle arbitrary constants for total functions.

Beautifying integer_cln_imp.h

Fix to quantifier rewritting not being idempotent. See bug 441.

Removing rewriter call in SmtEngine::addFormula().

Fixed missing \ in uflra/Makefile.ma
Fixed another model bug and added previously failing fuzz testcase

Fix for bug 439. Delta computation now includes disequality information.

Change run-regression script to *additionally* run a second test with --check-models *if* the benchmark is sat/invalid (or is incremental, with at least one sat/invalid result).

This increases significantly the time to do a "make regress", as more tests are running.

We need to run both *with* and *without* --check-models, since that option disables certain preprocessing.

To turn off these extra tests during a make regress, you can set CVC4_REGRESSION_ARGS=--no-check-models.

To turn off the extra test for a *particular* regression benchmark, you can put this in the benchmark:

; COMMAND-LINE: --no-check-models

That might be necessary in e.g. nonlinear arithmetic benchmarks.

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

Updates to Clark's commit r4540:

* ALL_SUPPORTED/QF_ALL_SUPPORTED don't include nonlinear
* Change "Notice" to "Warning" when produce-models turned off due to non-linear

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

fix typo in language bindings

Finally tracked down problems in regressions and fuzz results (this also
explains why my build was giving different answers from Dejan's build).
Problem was that if you run:

cvc4 --check-models foo.smt

it would fail, but if you run

cvc4 --check-models --produce-models foo.smt

it would succeed.  Even though produce-models is supposed to be automatically
set when you set check-models, it seems this was happening too late.  Fixed by
removing any distinction between produce-models and check-models in the
heuristic setting code.  Kind of ugly though.

Also, disable models if nonlinear arithmetic is on.

TheoryEngineModelBuilder::buildModel() is only called once with fullModel=true, within a SAT context.  This fixes some outstanding model bugs.

Committing also a Clark-provided assertion the Model code to ensure the call is only done once per context.

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

export null nodes (fixes a bug in portfolio model stuff)

Test that breaks arithmetic model building due to disequality terms.

Arithmetic problem that fails --check-models due incompleteness with multiplication.

Bug-fix for a crash involving improperly-thrown exceptions; also, add LogicException for errors where the user uses a feature not permitted in the current logic (e.g., a quantifier in a QF logic)

In non-linear logics, rewrite DIVISION, INTS_DIVISION, and INTS_MODULUS into ITEs of the form:

  IF (denom = 0) THEN divByZero(num) ELSE (DIVISION_TOTAL num denom) ENDIF

where divByZero is an uninterpreted function symbol (there's one for each of the partial operators).

In linear logics, don't do any of this.

Bitvector partial functions to come, if this is successful for Tim.

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

another DISTCLEANFILES entry, for proper "make distclean" behavior (fixes "distclean" target error last night)

Fix for another model assertion failure

Turns on TheoryUF when non-linear arithmetic is turned on. Adds test cases for division by 0.

fix "make distcheck"

Review of trunk r4525 (TypeNode::getBaseType()):

* fixed TypeNode::getBaseType() for predicate subtypes
* added Type::getBaseType() for public interface
* added unit testing

To avoid confusion, also:

* renamed PredicateType::getBaseType() to "getParentType()"
* renamed TypeNode::getSubtypeBaseType() to "getSubtypeParentType()"

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

Improved support for division by zero.  This adds the *_TOTAL kinds and uninterpreted functions for division by 0.

exception fix

Fixed two small bugs in model generation

Added getBaseType - Morgan please check

added support for parametric datatypes in smt2 parser, includes support for 'as' qualifier

* Type ascription bug fixed (resolves bug 432), but there are others I discovered (still outstanding).  :-(
* Fix a documentation-building problem when building from tarballs (fixes distcheck build failure last night)
* Provide expected output for arith regression 'mod.01.smt2'
* Also, fix a compiler warning in inst_gen.cpp

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

Fix to a bug in integer mod lemmas.

fix issue in compatibility layer that could segfault

Fix to the context dependent static learning code.

fixes for replacement function library

fixes for mac os

fix for tarball building (fixes debian and distcheck problems in nightly builds)

more minor updates to inst gen and representative selection, clean up of equality query

cleaning up some of the equality query stuff, implemented a new representative selection strategy for quantifier instantiation

delta of a model-building failure case

more updates and minor bug fixes for fmf/inst-gen quantifier instantiation

Tweak to options configuration for turning off minisat elimination when models are on

Disable minisat elimination when models are on

Disable some array optimizations when models are on

auflia directory missing from regression summary - fixed

Fix to subrange type enumerator, and its unit test.  Resolves bug 436.

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

bug fix for parametric datatypes, previously datatypes theory/rewriter was not recognizing parametric datatype types as being datatype types

Fix for bug 430. d_delta in PartialModel was never being computed. (Delta remained at its initial non-sensical value of -1.)  There was a problem with guarding d_delta with d_deltaIsSafe in PartialModel.

build options sources into distribution tarballs (in the same way that antlr grammars are pre-generated for tarballs).  this speeds up user builds by not requiring them to run the mkoptions script (unless they change an options meta-file).  i've tested this, but let me know if there are any problems you encounter.

new boost.m4 makes boost-thread require boost-system.  relax this dependence (since it doesn't appear to affect us?!), and make it non-fatal anyway, since threads aren't strictly required for all cvc4 builds.  give a warning.