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.

better parametric datatype arity checking; fixes bug 433

Fixed a failing datatype regression with check-models

today's build system fix: sometimes examples weren't built with "make examples"; fixed

fixed bug in datatypes decision procedure enforcing rewriting of incorrectly applied selector terms, this effects two regression test where TCC fails, using --disable-dt-rewrite-error-sel changes answer of both regression tests

More bug fixes and more checks for models

last build system fix for now: fix some typos affecting Mac

extra quoting for special character

more minor fixes to build system

One of my changes to the build system yesterday broke the nightly build because:

1. The source tree was configured.
2. The builds directory was removed.
3. The source tree was re-configured.

Which led to a nasty dangling symlink that caused (3) to abort.

Fixed.

fixed assertion failures in efficient e-matching

Includes many fixes to build system for Solaris (thanks Tim!), and also
just in general, and some documentation adjustments.

Updated the ArithStaticLearner to be user context dependent.

Fix for systems that do not have the MAP_FILE macro defined.

fix for bug 429
* not all asserted units were tracked in the user trail, moved the tracking into uncheckedEnqueue

two smaller random pure LRA push-pop cases that fail

dejan@church:~/workspace/fuzz/problems$ ./check.sh arith_lra_01.smt2
z3:   sat sat sat sat sat sat sat sat sat unsat sat sat sat sat sat unsat sat
cvc4: sat sat sat sat sat sat sat sat sat unsat sat sat sat sat sat unsat unsat
dejan@church:~/workspace/fuzz/problems$ ./check.sh arith_lra_02.smt2
z3:   sat sat sat sat sat sat sat sat sat sat sat sat sat sat sat unsat unsat sat
cvc4: sat sat sat sat sat sat sat sat sat sat sat sat sat sat sat unsat unsat unsat

efficient e-matching now specific to rewrite rules

more major cleanup of quantifiers code, separating rewrite-rules-specific code from quantifiers-specific code

fixed problem with datatypes giving incorrect explanations, now corrected and improved.  this update fixes bug 428, also changes the result for 2 benchmarks where tcc in cvc3 fails (cvc4 had previously had been answering correctly by accident).

More debugging info, small changes to model builder

some fixes for "make examples" and "make install-examples" when invoked from tarballs (non-subversion-checkouts); should fix "INSTALL" failure we saw in last night's build email

Added reads that were missing in collectModelInfo

fixed TheoryBV collectModel info to check for shared terms; this seems to fix bug424

The contrib/get-antlr-3.4 script:
- Has no outdated reference to /usr/share/java/stringtemplate.jar (as discussed on the mailing list).
- Attempts to determine if the computer is 64 or 32 bit and configure antlr appropriately.
- Warns the user about it's guess.
- Tells the user how to correct an incorrect guess.

more updates to inst gen: fixed partial instantiations, recognize duplicate defaults for uf

fix parser generation in distributed tarballs (should fix bug #427)

one more incorrect #line fixed

fix misleading comment in example

fix installation of certain header files

add bug 425 models regression; fix mac-build execute permission

Fix for model building with shared terms for arithmetic.

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

Fix problem with incremental with portfolio. Fixes bug 420.

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

BV theory model fix

--fallback-sequential / --no-fallback-sequential option
closes bug 419, fix typo, fix warning

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

first working version of new inst-gen-style quantifier instantiation technique for fmf (--fmf-new-inst-gen), minor cleanup

more cleanup of quantifiers code

first draft of new inst gen method (still with bugs), some cleanup of quantifiers code

fix #line number warnings (sorry!)

Added assertions and tracing code for collectModelInfo phase

Latest changes to model code

Fix bug 421, again, and add a second, independent test case for the same
with --check-models (which caused the same bug, for a different reason,
due to some unintended interaction between the checkModel() function and
the UserContext, which rolled back the Model object.  (Groan...)

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

minor changes in wording for "cvc4 --version", and point to the COPYING file for full info

Standardizing copyright notice.  Touches **ALL** sources, guys, sorry.. it's
just the header comments at the top, though.  Don't update to this rev if
you don't have time for a complete rebuild, and exclude this rev if you
want to see what's new across a range of commits.

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