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.

Resource spending support in theories (and especially in quantifiers).

cvc4terminate infinite loop fix

cvc4terminate infinite loop fix

Merge branch '1.4.x' while ignoring commit 8d5eb49.

Fix fix. There are no unsat cores in 1.4

Merge branch '1.4.x'

Fix (push) and (pop). Thanks to Christoph Sticksel for the bug report.

Fix soundness bug for quantifier macros involving Int/Real.

Refactor entailment filtering for conjecture generator.  Other minor cleanup.

More refactoring of conjecture generation.  Term generation into own class.

Bug fix variable triggers with --inst-max-level : use term in EQC with minimal instantiation level.

Refactoring of conjecture generator.  Determine subgoals are non-canonical based on ground equalities.  Add filtering options to options file.

Fix bug for variable term triggers within multi-triggers.

Accept user-provided triggers with variable terms.  Flush lemmas before quantifiers check.  Minor fix for conjecture generation.

Update command_executor_portfolio.cpp

Merge remote-tracking branch 'origin/master'

check() optimization

Details of testing here:
http://church.cims.nyu.edu/wiki/User:Kshitij/theorycheckoptimization

Implement and enable --dt-var-exp-quant, cleanup trace messages, minor changes for relevant term filtering.

Work on conjecture generator : do not generalize subterms with concrete values, filter conjectures with ground substitutions whose equality is unknown, simplify generalization depth calculation.  Print --dump-instantiations on sat/unknown.

Set instantiation level on skolemized bodies of quantifiers.  Rename inst-level attribute to quant-inst-max-level

Do not use pure theory terms as single triggers.  Minor cleanup.