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

make sure to mark LogicInfo as CVC4_PUBLIC

fix for dejan: term ITEs now dumped correctly

initial draft of skolemization during pre-processing, made simple cliques the default option for uf strong solver

minor changes to arithmetic assertions involving nonlinearity and models (related to bug 405)

minor fixes to pickler (hopefully fixes Debian build from last night)

release notes

Calling the setIncompleteness() flag on all full checks once a non-linear term has been seen.

Fix a few segfaults in driver.

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

draft RELEASE-NOTES file, and minor release stuff

fixes to "make distclean" and C compatibility bindings; should fix the broken builds last night

fixes to "make distclean" and C compatibility bindings; should fix the broken builds last night

This commit add interpretation by lemma for INTS_DIVISION, INTS_MODULUS, and DIVISION. Improves support for non-linear monomials in getEqualityStatus(). Fixes bug 405.

Some fixes to portfolio

* respect output lang
* fix export variable for BOUND_VARIABLE
* support export of SUBRANGE_TYPE
* statistic for lastWinner, other minor stat changes
* fix running of multiple threads on checsat/query
* changes of Assert -> assert which became private
* fix some destruction time order issues
* fix Pickler with AssertionException going private

Fixed by not fixing:
* portfolio+datatypes does not work
  - added ExportUnsupportedException to more places, switches
    to sequential
   (still TODO / decide : not switch silently, but print error)
   > note: this exception now needs to be (and is) defined in expr.h

Known issues:
* problems in portfolio+quantifiers
   - at least some problems appear to be because of static variables
   (will be later "fixed" like the datatypes)

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

fix distribution of cvc4_assert.i

fixes for compatibility (i.e., CVC3) Java bindings

rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to make it unambiguous for case-insensitive filesystems like on Mac.  Fixes Mac builds

some fixes to build system

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

fix production-build linking error

Public interface review items:

* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument()
* Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only
* CheckArgument() throws non-AssertionException
* things outside the core library (parsers, driver) use regular C-style assert,
  or a public exception type.
* auto-generated documentation for Smt options and internal options

Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.

* fix compatibility library naming for SMT-LIBv1
* change name of JNI library to "libcvc4jni", which works better with Java's
  System.loadLibrary().

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

* Rename SMT parts (printer, parser) to SMT1
* Change --lang smt to mean SMT-LIBv2
* --lang smt1 now means SMT-LIBv1

* SMT-LIBv2 parser now gives helpful error if input looks like v1
* SMT-LIBv1 parser now gives helpful error if input looks like v2
* CVC presentation language parser now gives helpful error if input
  looks like either SMT-LIB v1 or v2

* Other associated changes

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

finally, a portable solution

fix for non-Mac

speed up mkoptions script (esp. on Macs)

better progress indicator for mkoptions

disable building of cvc3_george system-test object (which isn't used yet anyway, and required ~10 minutes to build with -O3).

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

Finish off SEXPR kind work.

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

updates to model generation : do not modify equality engine during getValue, other minor changes, still problems with constants not being specified for some eq classes

Fix a handful of things for Mac, and Java bindings.

Also add a "mac-build" script that sets up prerequisites for Mac.

bug #398 test (bug was resolved last night), and a script to download all bug attachments from bugzilla and put them in the tree

Fix type checking for define-funs (resolves bug 398).

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

The Tuesday Afternoon Catch-All Commit (TACAC):

* --early-exit and --no-early-exit command line options (the former is default for all builds except debug builds)

* New SEXPR kind for doing lists of things (we previously used TUPLEs for this purpose, but TUPLEs will be used in future by the datatypes theory, and so cannot have function symbols in them, etc.).

* SMT-LIB compliant output for (set-option :produce-unsat-cores true) and (get-unsat-core)

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

fix

fix some Mac issues

some buggy examples for incrementality, and make bug326 run as part of make regress, because the bug was fixed.

Also make QuantifiersModule's destructor virtual (it has virtual members).

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

some api changes

Fix the memout issue seen in recent nightly regressions (was due to a
Statistics-printing problem, limited to certain benchmarks).

Mark some unlabeled header files "cvc4_private.h".

Other minor cleanup.

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

Separate public-facing and internal-facing interfaces to Statistics.

The external interface (e.g., what's answered by ExprManager::getStatistics() and SmtEngine::getStatistics()) is a snapshot of the current statistics (rather than a reference to the actual StatisticsRegistry).

The StatisticsRegistry is now internal-only.  However, it's built as a convenience library so that the parser and driver can use it too (by re-linking against it).

This is part of the ongoing effort to clean up the public interface.

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

another fix for the equality class iterator

Fixes for datatype dumping and printing.  Add a new test case for dumping.

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

SMT-LIBv2 compliance updates:

* chainability of =, <, <=, >, >= via the new CHAINABLE kind and
  TheoryBuiltin rewriter support (resolves bug #383)
* with --smtlib2, force interactive mode off by default

Also:

* fix a few bugs causing crashes
* better "alias" processing for options
* configure-time fixes to readline detection

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

better verbosity support (so it's sensible when the library is used via the API)

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

map C++ exceptions to Java exceptions correctly when they are thrown, and give a build error for Java component if it is misconfigured

some bugfixes that come as a result of debugging some CASCADE/C stuff..

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

General subscriber infrastructure for NodeManager, as discussed in the
meeting last week.  The SmtEngine now subscribes to NodeManager events,
does appropriate dumping of variable declarations, and notifies the Model
class.

The way to create a skolem is now:

  nodeManager->mkSkolem("myvar_$$", TypeNode, "is a variable created by the theory of Foo")

The first argument is the name of the skolem, and the (optional) "$$" is a
placeholder for the node id (to get a unique name).  Without a "$$", a "_$$"
is automatically appended to the given name.

The second argument is the type.

The (optional, but recommended) third argument is a comment, used by the
dump infrastructure to indicate what the variable is for / who owns it.

An optional fourth argument (not shown) allows you to specify flags that
control the behavior (e.g., don't do notification, and/or don't make a
unique name).  Look at the documentation for details on these.

In particular, the above means you can't just do a mkSkolem(boolType) for
example---you have to specify a name and (hopefully also,
but it's optional) a comment.  This leads to easier debugging than the
anonymous skolems before, since we'll be able to track where the skolems
came from.

Much of the Model and Dump stuff, as well as some Command stuff, is cleaned up
by this commit.  Some remains to be cleaned up.

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

fix subtle bug in NodeValue::toStream()

fix for bug 370.
some internal nodes in eq engine were treated as constants incorrectly

Changing the equality engines's euivalence class iterator. Andy please check if this does what you want it to do.

SMT-LIBv2 compliance regarding outputting "unknown".

Thanks to Peter Collingbourne for the report, and the patch!

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

speed up option-file generation on Mac OS by an order of magnitude

more bindings fixes

minor fix for models, added simple cliques option for uf strong solver

enable bug regression for bug 382

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

store values returned by get-value in TheoryModel::d_reps if necessary, fixes bug 382.

minor interface improvements, compliance fixes

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

another bindings fix (should fix debian build)

bug testcase for model generation

a fix for the java bindings for wei

Fix a soundness bug reported by Matthias Weiler (had to do with expired TNodes).

Also fix an issue where --check-model didn't take user define-funs into account.

Also make preprocessing a bit more chatty (with -v -v).

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

Fix a few minor issues in options processing, improving usability, consistency, error-reporting, and documentation.

ensure that get-value and get-model are consistent, rewrite function value bodies, do not dag-ify model output

Adding model assertions after SAT responses.

To enable, use --check-models.  Turning on the option can be done in debug or optimized builds, regardless of whether normal assertions are on or not.  This is to allow us to check the generated models in long-running queries, and might be useful to end users as a double-check too.

By default, --check-models is quiet (no output unless it detects a problem).  That allows regression runs to pass unless there are problems:

  make regress CVC4_REGRESSION_ARGS=--check-models

To see it work, use -v in addition to --check-models.

There may still be bugs in the feature itself, but already I've found some apparent model-generation bugs (and discussed with Andy) from this feature, so it seems useful in its current state.

--check-models turns on what SMT-LIBv2 calls "interactive mode" (which keeps the list of user assertions around), and also implies --produce-models.  This version does NOT require incremental-mode, which one design did (the one mentioned in yesterday's meeting).

Also:

* TheoryUF::collectModelInfo() now generates UninterpretedConstants (rather than non-constants)
* The UF rewriter now reduces (APPLY_UF (LAMBDA...) args...), and treats uninterpreted constants correctly (e.g. uc_U_1 != uc_U_2)
* The SubstitutionMap now supports substitutions of operators for paramaterized kinds (e.g., function symbols)

added getCardinality to model

Partially reverting the changes made in 4308. There is now both an Expr and Node version of getValue() in TheoryModel.

modified getValue to return Expr instead of Node