Set Constant's normal form and other short fixes

Other short fixes:
* use debug tag "theory::assertions::fulleffort" to dump assertions only at FULL_EFFORT
* theoryof-mode fix in smt_engine.cpp
* hack in TheoryModel::getModelValue [TODO: notify Clark/Andy]
* Lemma generation when it rewrites to true/false fix
* TermInfoManager::addTerm(..) fix
* Move SUBSET rewrite to preRewrite
* On preRegister, queue up propagation to be done upfront
** Hospital4 fails when all other fixes have been applied but not this one. Good to have an actual benchmark which relies on this code.
* TheorySetsProperties::getCardinality(..) fix

Thanks to Alvise Rabitti and Stefano Calzavara for reporting some of these; and to Morgan and Clark for help in fixing!

All Minisat solve calls now return lbool (fixes bug 599)

Compute model basis only for fmf.  Add another co-datatype regression.

Add local theory extensions instantiation strategy (incomplete).  Refactor how default options are set for quantifiers.  Minor improvement to datatypes.  Add unsat co-datatype regression.  Clean up instantiation engine.  Set inst level 0 on introduced constants for types with no ground terms.  Return introduced constant for variable trigger when no ground terms exist.

added command line option for extractArith bv rewrite

Short-circuit in TheoryArithPrivate::check(), care of Tim.

New, uniform checkTime statistic for all theories (as discussed in meeting).

Resource-limiting work.

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

Add term db mode.  Minor changes to quantifiers rewriter: split ITE's where equality resolution is possible on condition, pull nested quantifiers from ITE branches.  Minor cleanup.

Be lazier to consider EQC in UF+cardinality solver.  Minor cleanup.

Minor changes to AUTHORS and COPYING

Minor adjustments to wording.

Copyright text fixes.

Merge pull request #69 from mdeters/bug594

Fix memory leak in CDHashMap<> with Node keys (resolves bug 594).

Remove two obsolete versions of MBQI.

More preparation for filtering relevant terms in TermDb.

Possible fix for bug594

Merge pull request #65 from mdeters/bv-ineq-cachefix

Fix BV inequality solver caching, and TNode fix.

BV inequality graph TNode fix.

Fix BV inequality solver caching.

Fix tokenization of "reset" in SMT-LIB v2.0.  It's a reserved word only in 2.5.

Minor cleanup.

Merge pull request #64 from mdeters/theorysets-hashset-iteration

Update TheorySets to use CDHashSet<>::key_begin() / key_end().

Work on synchronizing decision=justification and E-matching.

Merge pull request #63 from mdeters/theorystrings-hashset-iteration

Update TheoryStrings to use CDHashSet<>::key_begin() / key_end().

Bug 593 fix: if the type is finite, it is now considered for detecting theories of nested terms.

Do not eliminate variables only occurring in patterns.  Minor improvements to sort inference.  Remove unused code.

Merge branch '1.4.x'

Update TheorySets to use CDHashSet<>::key_begin() / key_end().

Update TheoryStrings to use CDHashSet<>::key_begin() / key_end().

Work around an apparent bug in libc++ that was causing crashes on Mac..

Fix a deterministic assignment-ordering for get-assignment (fixes a regression failure on Mac).

Increase stack size when running regressions (fixes some regression crashes on Mac).

Fix dt shared terms issue, reenable regression.

Fix bug with incremental+datatypes.  Minor cleanup.  Disable regression bug484, enable parsing_ringer.

Merge pull request #62 from mdeters/bv-cleanup

Remove some unused variables.

Remove some unused variables.

Fixed bug in model builder with subtypes

Remove some dead code.

Fix a memory leak in SatSolverRegistry (re: bug #594).

Fix memory issues in bitvector theory, which is now valgrind-clean (mostly resolves bug #594).

Merge branch '1.4.x'

Conflicts:
src/smt/model_postprocessor.cpp
test/regress/regress0/Makefile.am

Fix missing case in Boolean terms rewriting.  (Resolves bug #596.)

Merge branch '1.4.x'

Conflicts:
src/smt/model_postprocessor.cpp

Corrected fix for missing case in model postprocessor (resolves bug #595).

Enable --quant-cf by default.  Fix bug in qcf for mixed Int/Real.  Minor improvement to performance of E-matching.

Revert "Fix missing case in model postprocessor (resolves bug #595)."

This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a.

Revert "Fix missing case in model postprocessor (resolves bug #595)."

This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a.

Conflicts:
test/regress/regress0/Makefile.am

Update competition build rules.

Merge branch '1.4.x'

Conflicts:
test/regress/regress0/Makefile.am

Fix missing case in model postprocessor (resolves bug #595).

Properly distinguish which EQC to assign values in datatypes, use assertRepresentative.  Disable regression related to records.  Enable fmf-fun related regression (modified).  Apply modified version of Morgan's patch to fix tuples/records in model.  Fix bug with sort inference + patterns.  Minor infrastructure.

Minor fix for getInstCons

Reenable regression.  Add (for now, disabled) changes to datatypes theory combination.  Relax communication of dt facts.

Fix model bug in --mbqi=fmc.  Minor cleanup in datatypes.

Merge branch '1.4.x'

Fix get-bug-attachments script.

More work on datatypes theory combination: fix bug in care graph, do not assign values for EQC of datatype type that contain only terms belonging to other theories, do not treat APPLY_UF as congruence operator, communicate equalities involving terms of external kind.  Minor fixes for fun_def_process.  Other minor changes.

Added cache to getModelValue

Fix cegqi for synthesis without syntax.

Simplify which lemmas to communicate in dt.

Fix bug 592: introduce skolem for dt instantiate lemma (avoids terms in lemmas being rewritten).  Minor improvement to dt care graph.  Reenable regressions.

Fix some mistakes in datatypes theory combination, disable two regressions.  Minor fix for fun defs.

Do not allow duplication of function definitions.  Set incomplete flag in model builder.

Be more lazy about generating array lemmas

Added new, much faster, care graph computation for arrays
Force split on true first in combineTheories
Fix bugs in getModelValue in bit-vectors

Preprocessing step for finding finite runs of well-defined function definitions using FMF.

Initial infrastructure for function definition quantifiers, internal parsing format for Smt2.

Improve stats in conjecture generator, minor cleanup.

Minor fix for --user-pat=resort

Fix typo.

Minor parser performance fix.

Add --user-pat=resort.  Minor cleanup of options.

Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.

* support for new commands meta-info, declare-const, echo, get-model,
  reset, and reset-assertions
* support for set-option :global-declarations
* support for set-option :produce-assertions
* support for set-option :reproducible-resource-limit
* support for get-info :assertion-stack-levels
* support for set-info :smt-lib-version 2.5
* ascribe types for abstract values (the new 2.5 standard clarifies that
  this is required)
* SMT-LIB v2.5 string literals (we still support 2.0 string literals when
  in 2.0 mode)

What's still to do:
* check-sat-assumptions/get-unsat-assumptions (still being hotly debated).
  Also set-option :produce-unsat-assumptions.
* define-fun-rec doesn't allow mutual recursion
* All options should be restored to defaults with (reset) command.
  (Currently :incremental and maybe others get "stuck" due to late driver
  integration.)

Fixed inefficiency in bit-vector rewrite rule.

Fix bug590 regression distcheck failure from last night.

Fixed bug 589

Fixed bug 590, added regression test

Minor cleanup in datatypes.

Merge pull request #59 from kbansal/sets3

sets type enumerator

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.