Fix for quantifiers containing Boolean terms.

Merge branch '1.0.x' of https://github.com/CVC4/CVC4 into 1.0.x

fix for bv crash in incremental mode; this is a temporary fix for bug 493

gitinfo modifications fix

Fix typo in error message

prvs commit: lower warning to notice

Signed-off-by: Kshitij Bansal <kshitij@cs.nyu.edu>

Merge pull request #5 from kbansal/1.0.x

make incremental+portfolio experimental

make incremental+portfolio experimental

Fix builds/ links to survive configuring twice with different prefixes

Fix ECHO command in CVC language parser to not output quotation marks

repairs a bug in rewriterule engine: constructor cannot be used as a pattern
(cherry picked from commit c33a1abc78bcd51f3f95562b117498caf252cafc)

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

Removing BVDebug and replacing with Debug.

Only put quantifier assertions in model equality engine if fullModel==true

Significant work on bug #491 (not yet closed).

More complete fix for bug 484 (includes fixes for records and tuples).

Fix error in tuple type-checking.

Make --default-dag-thresh apply to stringstreams

Do not install the "private-library" header

make datatypes enumerator behavior clearer (no exceptions in normal operation)

Fix a compiler warning in NodeBuilder

Merge pull request #3 from kbansal/1.0.x

decision/ : save d_prvsIndex in JH

decision/ : save d_prvsIndex in JH

dos2unix conversion for a number of files; this avoids spurious conflicts when merging to master

Fix NodeBuilder bug which could attempt to allocate beyond hard limit

driver::totalTime statistic is now reported correctly on crashes, too

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>

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

correct output language bug with --dump-to

Fix the regression test for bug 486, and enable it

(cherry-picked from master 23b4fd82d1ed326cd57e9bc57ef9fab98b0b1c87)

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 Intel benchmarks regarding quantifiers and datatypes, datatypes theory still crashes for datatypes with boolean subfields

(cherry picked from master bcbf52ffbe0416ecf70bdb644017c338c0540793)

another fix for quantifier models (related to bug 486)

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

partially address bug 486: allow some model inspection of quantifiers

update NEWS file

fix for theory preprocessing cache on clang, perhaps others.

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

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

adding copy constructor for the datatype enumerator
fixes bug 484

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

Fix printing of EXISTS in CVC language printer

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 #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

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

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

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

(cherry-picked from commit 206edb6f11674e954f5762a1db9712131151a276)

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

Fix to portfolio builds
(cherry picked from commit f46ba71e78054af63b529eb3271952c55beba37e)

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

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

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

fix java system test dependences

drastic simplification of quantifiers code regarding equality queries, instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine

Fix for a CLN related bug on 32 bit systems. Integer((1<<29)+1) and Integer((long int)((1<<29)+1)) gave different values.  This was confirmed on vm-int1.cims.nyu.edu. See ginac.de/CLN/cln_3.html#SEC15 for more details. rational_white and integer_white have tests covering this.

Some fixes for boolean arrays

also a regression for bug 411

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

fix #line annotation warning

updated examples

added a new example for the combination of bit-vectors and arrays (includes model generation) and set the logic for the bitvector example

another part of last commit

definition-expansion fixed for get-model, resolves bug 411

Polishing API examples.

Adding SmtEngine::setLogic(const char* logic) so that smt.setLogic("QF_LRA"); works.

Fixes for stricter compilers Andy brought to my attention.

Changing the documentation of ARR_TABLE_FUN to say (internal symbol).

all API examples now have java versions too; bitvectors gets built; also updated old-style copyrights in the examples

incorporating some comments from Clark

Fix assertion in smt_engine's getValue
Minor changes to RELASE-NOTES

Updating the combination.cpp example.

Committing tests to potentially discover an obscure CLN library issue on 32 bit platforms. The issue is discussed here: ginac.de/CLN/cln_3.html#SEC15.

renaming --smtlib to --smtlib-strict; removing --smtlib2 option

internal variables (skolems) aren't printed as part of the model

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

change detection/handling of output language more reasonably; fixes a nagging bug Tim found in API examples

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

quantifiers now uses master equality engine, preparation work to cleanup code

parametric datatypes fix related to non-ascribed type constructors introduced by decision procedure

added a simple API example example showing how to use the bit-vector theory.

Changes to SExpr to accept autoconversion from bool and const char*. Adding an example for combination.

Adding smtname level options for tlimit, rlimit, etc. Fix to the internal documentation in base_options.

Partial fix for bug 435; still needs some effort.

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

Add some regressions for bug 438.

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

fix rewrite-rules syntax in regression

minor fix to release script

fix the syntax of assert-rewrite/-propagation/-reduction by putting the pattern first
just after the bindings

 Do it before the release in order to not break user files later

reliable benchmark corresponding to bug468

require type ascriptions for parametric datatype constructors (making them canonical), this fixes the followup issue of bug 438

Fix for hidden symbols in library on Mac.  It's a strange issue to do with
explicit template instantiation rules, -fvisibility=hidden, and the way that
Apple distributes libstdc++.

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

fixes bug 438, incorporate subtypes into type unification when typechecking parameterized datatypes

fix for andy: boolean terms stuff really shouldn't look at datatypes at all in this release