Merge branch '1.0.x'

Model no longer adds subterms of quantifiers to equality engine, this fixed bug 492 and resolves previous issue for bug 486.
(cherry picked from *part* of commit e54c0f73712b25f1d6d49a3817c923eea077da81)

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

Model no longer adds subterms of quantifiers to equality engine, this fixed bug 492 and resolves previous issue for bug 486.\n Multiple improvements for E-matching: do not choose multi-triggers if single triggers exist, only create multi-triggers that contain all variables, consider multiple terms per equivalence class but only add one instantiation per round per (trigger,term) pair.\nImprovements for strong solver: make use of sort inference information when choosing splits, check for cliques eagerly when disequalities are asserted.

Some cleanup of miplib regressions and options

Merge from mdeters/miplib branch (commit 'ce7c485182902ae43871057185095f71f74a8a58')

new option for doing top-level miplib substitutions (or not)

extended miplib trick to 6 vars, should work on pp miplib examples now

new miplib pass, works for 1 or 2 vars

Remove old miplibtrick from arith static learner

correct output language bug with --dump-to

Merge branch '1.0.x'

Fix a tuple attribute bug that was causing model-generation problems for tuples

Merge branch '1.0.x'

Fix a small problem in clang builds due to namespaces and symbol lookup

Fix a small problem in clang builds due to namespaces and symbol lookup

Adding a heuristic to more eagerly split bounded integer variables.

correct output language bug with --dump-to

currently disabling bug486 regression.  we need to discuss getValue/collectModelInfo for quantifiers more.

fix for finite model finding caused by new collectModelInfo code

Updated NEWS for recent changes.

Fixes for Win32 (closes bugs 488 and 489)

* timer statistics now supported (closes bug 488)
* use of --mmap doesn't crash anymore (closes bug 489)

Merge branch '1.0.x'

Fix the regression test for bug 486, and enable it

(cherry-picked from master 23b4fd82d1ed326cd57e9bc57ef9fab98b0b1c87)

Fix the regression test for bug 486, and enable it

made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced user-level context dependent.  this fixes bug 486

(cherry-picked from master c5d1a5d8f898bf22c6bbc98f1d484b07706c035b)

some fixes for win32, including ability to "make check" win32 builds via wine

made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced user-level context dependent.  this fixes bug 486

some fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory still crashes for datatypes with boolean subfields

(cherry picked from master bcbf52ffbe0416ecf70bdb644017c338c0540793)

some fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory still crashes for datatypes with boolean subfields

Merge branch '1.0.x'

another fix for quantifier models (related to bug 486)

fix --check-model --finite-model-find when used together (related to bug 486)

Fix errors and reduce warnings on clang (merge from mdeters/clang)

fix --check-model --finite-model-find when used together (related to bug 486)

Add win32 support (merge from mdeters/win32, with some cleanup).

Adding miplibtrick option.

Adding substitution size cap.

Merge branch '1.0.x'

Conflicts:
NEWS

fix to workaround ANTLR 3.2 issue with initialization

partially address bug 486: allow some model inspection of quantifiers

partially address bug 486: allow some model inspection of quantifiers

update NEWS file

add user patterns to the Smt1 parser; update NEWS file

Merge branch '1.0.x'

fix for theory preprocessing cache on clang, perhaps others.

Merge branch '1.0.x'

update ANTLR URLs (antlr.org -> antlr3.org)

Merge branch '1.0.x'

Fix an options-processing bug on some platforms (e.g., MacOS).

SMT-LIB get-model output now is easier to machine-parse: contains (model...) bracketing

Merge branch '1.0.x'

adding copy constructor for the datatype enumerator
fixes bug 484

Merge branch '1.0.x'

Fix bug 483: readline checks must come after Boost checks in configure

Fix printing of EXISTS in CVC language printer

Fix bug 483: readline checks must come after Boost checks in configure

Fix printing of EXISTS in CVC language printer

Merging in patch from branch '1.0.x'.

Adding unit test for different versions of division.

Merge remote-tracking branch 'main-repo/1.0.x' into 1.0.x

Changing the rewriter to use Boute's Euclidean definition of division.

Merge pull request #2 from CVC4/1.0.x

1.0.x

Merge pull request #1 from lianah/1.0.x

* fixed bug 481 by adding check for division by 0 in bit-vector division...

* fixed bug 481 by adding check for division by 0 in bit-vector division circuit
* added printing for total bit-vector division kinds for debugging purposes

Merge branch '1.0.x', getting fix for bug 480

SMT-LIB compliance fix to get-assignment; resolves bug 480

Merge branch '1.0.x' (getting fix for bug 479)

Ignore unknown term annotations (giving a warning).  Resolves bug 479.

Merge branch '1.0.x'

adding cache for preprocessing datatypes terms to fix bug 475, fix for handling user attributes in quantifiers (was broken)

(cherry-picked from commit 206edb6f11674e954f5762a1db9712131151a276)

adding cache for preprocessing datatypes terms to fix bug 475, fix for handling user attributes in quantifiers (was broken)

Merge from 1.0.x (bugfix for 476).

Fix bug 476: when CxxTest is not found, make the error less fatal-looking

Merge release branch '1.0.x'

For clarity 1.0.x is always a subset of master even after cherry-picking

Fix to portfolio builds
(cherry picked from commit f46ba71e78054af63b529eb3271952c55beba37e)

Fix performance issue in a DFS search (bug 474)
(cherry picked from commit f056522a587d1b080224992355be070b73d97a3b)

Fix to portfolio builds

Fix performance issue in a DFS search (bug 474)

Merge branch 'release-1.0.x'

The commits have already been cherry-picked but this commit makes it clear.

* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issues
* build bugfix for win32
* also fix a bug re: tuples and records in the datatypes rewriter

These fixes are for both trunk and 1.0.x branches.

(cherry picked from commit 8c8985f024cec925f774ff32ebccc306be8e4b26)

distribute the find_public_interface.sh script
(cherry picked from commit af44cd27d5b079f1279c407e610e557e81285d8f)

version numbering
(cherry picked from commit 4cae70d893601a2070dc2b00c5640b48515b1a22)

Fix for fuzzer-found model bug

(cherry picked from commit 25c6e1331d338c6ba8d60224711343986e11cf79)

* tuple and record support in compatibility library

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

* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issues
* build bugfix for win32
* also fix a bug re: tuples and records in the datatypes rewriter

These fixes are for both trunk and 1.0.x branches.

Improved garbage collection for TheoryArith.  The merges all of the code over from branches/arithmetic/converge except for the new code for simplex.

Cleanup of arithmetic, and some new utility functions for the coming fcsimplex code.

This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses CDInsertHashMap. CDHashSet<TNode> have been changed to CDHashSet<Node>.  Switching CnfStream to use CDInsertSet. Switches a few CDHashMaps in arithmetic to use CDTrailHashMap. Documentation changes to CDHashMap.

* Add support for --decision=justification + incremental (bug 437)
 - Fix a destruction order issue this triggered in DE

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

distribute the find_public_interface.sh script

version numbering

Fix for fuzzer-found model bug

Cutting release 1.0.

fix cut-release sanity checks

fix to TNode assertion (which is too strict, given lax ordering requirements on static data initialization)---this should fix debug-staticbinary Mac builds, maybe others

Throw a logic exception if user makes an assertion using a STORE_ALL

remove instantiator framework

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

Fix the way abstract values are typed; fixes some compliance issues.

Also support array-store-all for Boolean terms (related to abstract values, since that's the only way for the user to include an array-store-all in an assertion).

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

fix memory corruption issue in debug builds that led to unhelpful output

remove an obsolete (and incorrect) assertion in boolean-terms; also add failing regression for bug 472