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.)

Fix wording on GPL in legal notices; also remove an unnecessary source dependence.

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

compliance note

Abstract values for SMT-LIB.
Also fix bug 421 relating to incrementality and models.

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

cleanup up some static data members in the quantifiers code

fixing the cvc bv parser and typechecker

typo

bugfix: isQuantified, bugfix: flush

fixed datatypes rewriter to detect clashes between non-datatype subfields.  cleaned up model code, TheoryModel::getValue is now const.

* make Model class private (as discussed at meeting today)
* fix minor issue with s-expr parsing in CVC and SMT grammars
* other minor things

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

fixed bv rewriter to evaluate bvurem over constants

More fixes to model code

made datatypes rewrite incorrect selectors to ground term.  this feature can be turned off by --disable-dt-rewrite-error-sel.  changed regression answer to reflect new default behavior.

usability: remove --no-interactive from --smtlib option

fix for bug 415

* Add assertion in TheoryModel code to ensure we don't get inconsistent
  substitutions for solved variables.  Related to bug 418 (and might
  resolve it).

* Respect phase-locking in Minisat (one phase-saving site was unguarded).

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

fix beta reduction in both preRewrite() *and* postRewrite(), related to bug 417.  oops.  also fix spelling on "rewritting" test

some documentation fixes

adding mergePredicates method to the equality engine to be able to
assert equalities betweeen predicates

* Models' SubstitutionMaps are now attached to the user context
  (rather than SAT context)
* Enable part of CVC3 system test (resolves bug 375)
* Fix infinite recursion in beta reduction code (resolves bug 417)
* Some model-building assertions have been added
* Other minor changes

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

added reduced bv model failing test case

Fixed problem in assertEqualityEngine: predicates that are not false are no
longer assumed to be true

small fix for compat JNI library installation

fix SMT-LIBv2 compliance mode for bitvectors (was completely broken; didn't allow use of any BV ops

turn off cudd by default in configure script

* more complete support for --dump assertions:{pre,post}-PREPROCESSING-PASS
* more minor cleanup/doc

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

* Clean up some options documentation
* Remove defunct --no-theory-registration option
* Point people to Wiki tutorial
* Modernize the cut-release script
* Misc cleanup, documentation

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

* Some documentation about building compatibility and language bindings
* Better errors/warnings when SWIG isn't installed (resolves bug 373)
* Allow compatibility bindings to be built when SWIG isn't available

* Include a few bug testcases for resolved bugs.

* Fix error message if you POP beyond the bottom user stack frame.

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

* Fix some regressions' expected outputs.

* Ensure Rewriter::init() is called before ::rewrite().
  The array type enumerator recently gave us an end-run around
  ::init().  TheoryEngine no longer calls these, they're done
  via static initialization.

* Respect scope for declare-sort/declare-fun/define-sort/define-fun... (resolves bug 412).

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

fix \file

Bug-related:

* ITE removal fixed to be context-dependent (on UserContext).
  Resolves incrementality bugs 376 and 396 (which had given wrong answers).
* some bugfixes for incrementality that Dejan found (fixes bug 394)
* fix for bug in SmtEngine::getValue() where definitions weren't respected
  (partially resolves bug 411, but get-model is still broken).
* change status of microwave21.ec.minimized.smt2 (it's actually unsat, but
  was labeled sat); re-enable it for "make regress"

Also:

* --check-model doesn't fail if quantified assertions don't simplify away.

* fix some examples, and the Java system test, for the disappearance of the
  BoolExpr class

* add copy constructor to array type enumerator (the type enumerator
  framework requires copy ctors, and the automatically-generated copy ctor
  was copying pointers that were then deleted, leaving dangling pointers in
  the copy and causing segfaults)

* --dump=assertions now implies --dump=skolems
* --dump=assertions:pre-<PASS> and --dump=assertions:post-<PASS> now allow
  you to dump before/after a particular preprocessing pass.  E.g.,
  --dump=assertions:pre-ite-removal or --dump=assertions:post-static-learning.
  "--dump=assertions" by itself is after all preprocessing, just before CNF
  conversion.
* minor fixes to dumping output
* include Model in language bindings

Minor refactoring/misc:

* fix compiler warning in src/theory/model.cpp
* remove unnecessary SmtEngine::printModel().
* mkoptions script doesn't give progress output if stdout isn't a terminal
  (e.g., if it's written to a log, or piped through less(1), or whatever).
* add some type enumerator unit tests
* de-emphasize --parse-only and --preprocess-only (they aren't really "common"
  options)
* fix some exception throw() specifications in SmtEngine
* minor documentation clarifications

BoolExpr removed and replaced with Expr

disable model-generation by default in cvc3 compatibility layer.  should fix system test failure (bug 414).

Implemented array type enumerator, more fixes for models

IllegalArgumentException in java needs to be named "CVC4IllegalArgumentException" to avoid a name clash with java.lang.IllegalArgumentException, which isn't easily avoided, due to swig-autogenerated code that uses it unqualified.  X-(

minor fix for mbqi in finite model finding

implemented collectModelInfo for TheoryBV

updates to contrib scripts to match docs

better documentation, allow examples to be installed, etc

New model code, mostly workin

new README and INSTALL files

added support for interrupting TheoryBV

--wait-to-join / --no-wait-to-join option

workaround option till we fix bug 409. for now, I have kept --wait-to-join to
be default (old behavior). We could technically make --no-wait-to-join the
default when using non-incremental mode, but still possible for problems at
exit I think

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

adding ::getBooleanVariables to the PropEngine
you can get the Boolean variables in the TheoryEngine now by using d_propEngine->getBooleanVariables

* re-enable some Z3 extended commands:
  declare-const
  declare-funs
  declare-preds
  define
  simplify

* don't output --help on bad options, just invite user to try --help

* Datatypes from SMT2 parser now name the tester is-cons (e.g.)

* unknown results produce models, --check-model doesn't fail hard for
  incorrect unknown models.  removed the assert that kept arithmetic
  from producing models if it saw nonlinear

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

workaround for a nasty CLN bug

"Fix" (disable) portfolio when using quantifiers

Other changes:
* fix compile error in smt_engine in debug builds
* add getLogicInfo in smt_engine
* remove "empty-channel" and "disable-lemma-sharing" debug tags

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