Finish sets type enumerator implementation.

fix statistic in decision engine

Fix assertion.

Add dt lemma: zero size implies nullary constructor.

Fix for bounded integers when incremental, fixes bug 588.  Add option --dt-binary-split.

Merge branch '1.4.x'

Remove a bad (unstable, timing-dependent) test.

Minor change for performance according to Andy's suggestion.

Fix clang warnings

Make --user-pat=trust default.  Fix a few warnings found by Morgan.  Minor changes to options.

Merge branch '1.4.x'

Add Thomas Hunger to THANKS file (for having submitted patches).

Use n-ary splits instead of binary splits in theory datatypes.

Add dt.size to datatypes theory.  Add option for fairness strategy used by CEGQI.  Improve care graph/equality status for datatypes.  Only do FULL effort check in datatypes if no other theories used output channel.

fix for memory leak in BVQuickCheck

Merge pull request #58 from mdeters/smt-attributes

Context-dependent expr attributes are now attached to a specific SmtEngine, and the SAT context is owned by the SmtEngine.

Context-dependent expr attributes are now attached to a specific SmtEngine, and the SAT context is owned by the SmtEngine.

amend prvs commit

trace decision-node

CEGQI uses model.  Enforce fairness in CEGQI natively.

Model building into quantifiers engine.  Simplify axiom-inst mode.

Refactor model builder from model engine to quant engine.  Work on fairness strategy for CEGQI.  Add option for single/multi triggers.  Minor cleanup.

Merge branch '1.4.x'

Some defensive programming at destruction time, and fix a latent dangling pointer bug.

Merge remote-tracking branch 'origin/1.4.x'

Initial draft of CEGQI.

Fix issue with shared but non-preregistered term setup. Thanks Alvise Rabitti for the report.

Cleanup

Add owner map to better manage QuantifiersModules.  Initial infrastructure for cegqi.

Refactor quantifier prenex option.  By default, do not pull quantifiers with user patterns.

Merge branch '1.4.x'

Add unsat cores support to CVC native language.

Some minor cleanup.

Remove private header from public driver.

Fix portoflio issues (debugging code was being called even when tag was off)

Merge remote-tracking branch 'upstream/master' into sets-mergable

update default Sets options

whitespace fixes

Cache for getInstance, thanks to Johannes Kanig for the report.  Do not mkRep for multi triggers.

add couple of stats

sets stronger equality propagator

Refactor quantifiers attributes.

define-const is an extended command, not permitted in strict mode.

Fix unit test that was broken with last commit.

Fix a resource limiting issue where interruption didn't occur promptly.  Thanks Johannes Kanig for the report.

Merge branch '1.4.x'

Fix a bug in tuple-record handling.  Thanks to Saumya Debray for the report.

Some minor cleanup.

Merge branch '1.4.x'

Copyright-updating script now retains non-NYU/UIowa copyrights in files if present.

fix for bug586

Print array constants in SMT-LIB models with new syntax.

Clear out decls/defs with RESET command.

Extended parsing testcase, with constant arrays and RESET.

Merge branch '1.4.x'

Conflicts:
test/regress/regress0/arrays/Makefile.am

Fix native language parsing of chained-store expressions (resolves bug 585).  Thanks to Eric Seidel for the report.  Also fixed some operator precedence problems w.r.t. store expressions and arithmetic.

Support for RESET command in CVC native language (and infrastructure for support elsewhere).

Enable some old bug testcases that (maybe?) never got added.

Support exporting array-store-all expressions to other ExprManagers (fixes portfolio test failures).

Merge branch '1.4.x'

Conflicts:
NEWS

Fix output of integer-valued real constants in SMT-LIB models (thanks Christoph Sticksel for reporting).

Add some (so far trivial) regressions for constant arrays.

Improve error in CVC parser in presence of unrecognized command name.

More array constants and parsing: better error messages, extend to CVC presentation language.

Minor fixes to CVC printer.

SMT-LIB parser support for array constants (Z3 syntax).

Merge branch '1.4.x'

Note array const support in NEWS

Fix unit test for ArrayStoreAll.

Added internal support for constant arrays.

Merge branch '1.4.x'.

Added option for developer use only

More model-based combination for arrays

Better getEqualityStatus for arrays, smarter combination of theories

Update AUTHORS affiliations and add Martin.

Fix comment in SmtEngine.

Merge pull request #54 from kbansal/bugfix_setssegfault

fix getModelValue(<non-preregistered term>)

fix getModelValue(<non-preregistered term>)

Fix for an array-of-record model generation assert-fail (assert was too strong).

Option for more aggressive merging in UEE.

Merge branch '1.4.x'

Fix improper #inclusion of private header outside library.

Fix a command-replay bug in tear-down-incremental mode.  Thanks to Christoph Sticksel for the report.

Proofs- and cores-related segfault fixes (mainly a usability issue), thanks Christoph Sticksel for reporting these.

Add option for aggressive model filtering in conjecture generator (enumerate ground terms).

Merge branch '1.4.x'

Fix infinite loop in --bitblast-aig/--bv-aig-simp options.

Merge branch '1.4.x'

Fix bv options doc.

Fix some configuration-related oddness.

Clarify some licensing-related things.

Finer-grained resource-limiting in quantifiers.

Fix AIG bitblaster for unsat cores.

fix unit test for new fair datatype enumeration

Fair datatype enumeration.

Fix infinite loop in datatypes enumerator.  Minor work on conjecture generator.

Refactor option for uf+cardinality constraints solver.

Partial support for codatatype models.

Support :no-pattern.

Do not throw error when codatatype is not well-founded.  Add option for disabling codatatype reasoning.  Minor cleanup.