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)

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)