Permit setOption(decision-mode)

Fix bugs/issues with missed-t-prop dump output

Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a segfault in smt2 printer

Add ability to mkConst(TupleSelect) and friends in language bindings

Merge branch '1.2.x'

bug 374 fix: assert litVal=desiredVal only for leaf nodes

Bug 374 benchmarks

Change recursive expandDefinitions() to an interative worklist-based one; we were blowing the stack.  Fixes a segfault reported by Pantazis Deligiannis.

--segv-nospin is now default.

Minor cleanup.

Minor fixes for --fmf-fmc for quantifiers containing datatypes

initial modifications for per-ic cbqi

Clean up "make install"-produced intermediate files (resolves bug 526)

Fix a serious bug in the preprocessor; problem inputs reported by Pantazis Deligiannis.

Parameterized, uninterpreted sorts need no Boolean-term conversion

Minor fixes to build system.

Fix numerous compiler warnings on various platforms

Regressions now checking models on unknown too.  But quantifiers don't have to be simplified by check-model in that case.

Fixes for building with mingw win64.

Don't allow --stats if not a statistics-enabled build

some portfolio driver cleanup

Some fixes for (get-info :all-options)

fix for win32 option parsing via mingw32

(get-info :all-options) to get option values; also command-line option suggestions

Allow BV and DT in either order in the logic string

Add option --cbqi-recurse.

Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added infrastructure to BV collectModelInfo in preparation for bug fix.

enable bug521 regression tests

possible fix for bug 521

Minor fix for --no-condense-function-values

Fix quantifier instantiation bug in cbqi, add default priorities in rewrite engine.

Fix bug 516; include some bug testcases.

fixed seg fault when bv equality is turned off

fixed bug520

Fix for get-antlr script and PIC/non-PIC objects, on some platforms

"Tabular"-style function definitions in models with --no-condense-function-values

Minor bugfixes to model-building

Remove now-unused language bindings interface file.

Fix language bindings and portfolio builds.

Fix for curious GCC 4.8 translation with -O.

Remove auto-aritization from TPTP parser

Support for TPTP's TFF0 (with arithmetic)

This commit reverses an "SZS ontology compliance hack" that was
done for CASC-24 this year, and adds a TPTP pretty-printer which
is capable of outputting results in the TPTP way (rather than the
SMT way).

This commit includes minor changes to the Expr package to add
obvious missing functionality, and to fix the way expressions
with builtin operators are made.  These changes are truly a
_fix_, the implementation had not been properly aligned with
the design vision for some corner cases.

Fix for Boolean-term rewriting and LAMBDAs

Fix for bug 519; don't involve ITESimplifier in model generation.

add relevant domain computation

Model output is now const; this related to bug 519

Fix for a datatype parsing bug that Tim found.

Make uf strong solver user-context dependent, fixes bug 522.

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