Minor fixes for bounded integers, rewrite engine.

More bug fixes for interval models.

Fix portfolio builds after yesterday's commits.

Better check-models output for some kinds of problems; add anassertion that the master equality engine is consistent when it needs to be.

This is intended to help root out some recent model-generation bugs.

Fix minor warnings found by recent clang/gcc.

Remove output.h from public space, to avoid clashes with symbols defined in users' space.

Specifically, output.h was moved to CVC4's "private-library" rules, which means that it's
not installed on users' machines, and public headers should not include it.

Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.

Small fix for IS_INTEGER.

Remove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_public.h so that they don't escape to user space

Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.

Better user documentation for mkVar() and mkBoundVar().

Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.

Minor printer cleanup for SMT-LIBv2 symbols "div" and "mod".

Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.

Add support for interval models in bounded integers MBQI (in progress).

Merge branch '1.2.x'

Proposed fix for bug #513

Refactoring of model engine to separate individual implementations of model builder.  Begin work on interval models for integers.  Other minor cleanup.

Add files missing from last commit

Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk allows linearization of div,mod,/ by a constant.

Add options for symmetry breaking in uf+ss totality axiom approach, option for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine

Fix failure in non-assertion builds on incorrect SmtEngine use.

Merge branch '1.2.x'

Workaround for suspected clang 3.0 codegen bug on Mac

Fix to the "include" extended feature of the SMT-LIB parser

Give a more useful parse error message for "undeclared variable -1".

Indeed, "-1" is a valid user symbol in SMT-LIB; this commit makes a small
change to the parser to detect when something like "-1" is used but
undeclared, and adds a note to the error message giving the syntax for
unary minus.

Java streams example I forgot to add a long time ago

Make --var-elim-quant true by default.  Add rewrite engine to quantifiers module.

Fix in SMT2 parser for parametric datatypes

another fix for array-store-all printing

Better array-store-all output for SMT-LIB.

Fix typos in alttheoryskel

Fixes for Boolean terms in arrays (including fix for bug 517).

One more case for arrays of Boolean.

Fix for bug 517.

Allow disabling include-file feature

small parese issue in IDL

typo

IDL example theory (to be used with --use-theory=idl).

Fix bug in --fmf-fmc for producing models of functions not appearing in quantified formulas.

File inclusion in Smt2 parser.

The extended command (include-file "filename") now includes file content.

Add --no-condense-function-values option for explicit function models (useful in some applications)

Merge branch '1.2.x'

Fix clang static initialization order issue; fixes bug 512.

Add partial support for MBQI with arrays when using --fmf-fmc.  Fix constant bounds for bounded integers.

Merge tag 'casc24'

Updated CASC scripts, as provided to Geoff Sutcliffe

Merge branch '1.2.x'

Per SMT-LIB spec, allow (set-info..) command to succeed implicitly with unknown key.

SMT-LIB printer updates (some missing cases).

Fix bug where strict mode didn't allow DIV or MOD, and Ints permitted real division

Standardize SMT-LIBv2 set of logics to use LogicInfo.

Previously, SMT-LIB logics were treated specially, as in SMT-LIB v1.2.
This led to inconsistencies---such as nonstandard logics like "QF_LIRA"
being accepted in set-logic but not providing the "Real" sort.  Now,
the LogicInfo is used and queried, so nonstandard logics should work
fine and declare the correct symbols.  SMT-LIB v1.2, unfortunately,
can't take advantage of this fully since symbols like "Array" have
substantially different meanings in different logics.

Refactoring to prepare for MBQI with integer quantification.  Minor bug fixes.

Merge branch 'master' of https://github.com/CVC4/CVC4

Conflicts:
src/theory/arith/theory_arith_private.cpp
src/theory/quantifiers_engine.cpp

Significant work on bounded integer quantification to handle non-trivial bounds.  Refactoring of InstConstantAttribute to be internal to TermDb.

Add regressions for finite model finding

Merge branch '1.2.x'

Fix bug 512: an assertion failure only appearing with clang on Mac OS, due to improper ITE removal in quantifier instantiations.

Fix an error that valgrind found.

Merge branch '1.2.x'

Fix incremental bug in symmetry breaker.

Thanks to Christoph Sticksel for reporting this.

Merge branch '1.2.x'

Conflicts:
library_versions
src/parser/parser.h

Fix error reporting on use of (nonlinear) div,mod,/ symbols

Update THANKS to mention David Cok's contributions.

Detect multiply-defined :named annotations and issue an error.

Thanks to David Cok for pointing out this issue.

Conflicts:
library_versions

Fix parsing of SMT-LIBv2 |quoted| symbols that span newlines in interactive mode.

Thanks to David Cok for raising this issue.

Compliance fixes for :named annotations: they must name closed subterms, the names must be user-permitted names, etc.

Thanks to David Cok for raising this issue.

Don't allow get-model & co after a user push/pop

This makes us more strictly adhere to the spec, but it's useful anyway:
previously we would support a get-model until the problem was explicitly
changed with e.g. a new assertion.  That meant you could check-sat, then
pop, then get-model, but you'd only get the part of the model still in
scope.  This is strange, and would likely lead to problems, so it's now
disabled.

Thanks to David Cok for inquiring about this.

As per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => takes n>2 args and is right-assoc.

Thanks to David Cok for pointing out this issue.

Fix for equality-chaining of Booleans in SMT-LIBv2.

Thanks to David Cok for reporting this.

Fix destruction issue in GetValueCommand leading to crash.

Thanks to David Cok for reporting this.

Better error on invalid logic strings.

Thanks to David Cok for reporting this issue.

Conflicts:
library_versions

Better error on illegal (pop N); also more compliant SMT-LIB error messages in some places

Thanks to David Cok for reporting these issues.

A couple of fixes to the get-option command for compliance with SMT-LIB.

Thanks to David Cok for reporting this issue.

Disallow construction of (_ BitVec 0).

Thanks to David Cok for reporting this issue.

Fixed "success" response to (push N) / (pop N) with N > 1.

Thanks to David Cok for reporting this issue.

Fix to empty response to (get-assignment).

Thanks to David Cok for reporting this issue.

configure fix for building with glpk on redhat, perhaps others

minor changes to language bindings

disable Logic-checking with finite model finding for now, since FMF uses Rationals, making the check think arithmetic should be enabled (but it's not)

Fix erroneous results when the logic was incorrectly specified (by throwing LogicException).  Also correct a case where sharing was doing some work during pure theory solving.

Possible final version of run scripts for casc.

Add model-producing run script for casc.

Add support for --dump-models option, in preparation for casc.

As per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => takes n>2 args and is right-assoc.

Thanks to David Cok for pointing out this issue.

Fix for equality-chaining of Booleans in SMT-LIBv2.

Thanks to David Cok for reporting this.

Fix destruction issue in GetValueCommand leading to crash.

Thanks to David Cok for reporting this.

Better error on invalid logic strings.

Thanks to David Cok for reporting this issue.

Better error on illegal (pop N); also more compliant SMT-LIB error messages in some places

Thanks to David Cok for reporting these issues.

A couple of fixes to the get-option command for compliance with SMT-LIB.

Thanks to David Cok for reporting this issue.

Disallow construction of (_ BitVec 0).

Thanks to David Cok for reporting this issue.

Fixed "success" response to (push N) / (pop N) with N > 1.

Thanks to David Cok for reporting this issue.

Fix to empty response to (get-assignment).

Thanks to David Cok for reporting this issue.

configure fix for building with glpk on redhat, perhaps others

Fix minor bug in full_model_check.cpp

minor changes to language bindings

Update casc24-fnt run script.  Add casc24-fof run script.

added some extra options to the bit-vector theory

Add support for quantifier patterns in smt2 printer.

Refactoring to separate old and new model building/checking code.

Preliminary version of finite model finding over bounded integer quantification. Minor update to casc script.

disable Logic-checking with finite model finding for now, since FMF uses Rationals, making the check think arithmetic should be enabled (but it's not)

now proofs print mapping between atom and propositional variable as a comment in LFSC

Update casc run script.  Work on compliance for SZS output.