Improvements to trigger selection, min triggers by default. Optimizations for E-matching. Minor work to equality infer.

Updates to E-matching to avoid entailed instantiations earlier. Minor updates to datatypes lemmas, other minor changes.

Updating the mailmap for git.

Minor cleanup from last commit (quant util, equality infer). Do not set fmfBoundIntLazy for stringsExp.

Implement equality inference module for arithmetic terms.  Optimization for entailment checks.  Other minor infrastructure.

Merge branch 'master' of https://github.com/CVC4/CVC4

Refactored the equality engine in order to remove theory-specific logic from equality path reconstruction

Fixing a garbage collection issue in simplifyWithCare(). Bug 729.

Deleting allocated NodeVecs in ITESimplifier.

Freeing CegConjecture::d_ceg_si. Also making d_ceg_si a provate member of CegConjecture.

Fixing a memory leak in CDInstMatchTrie::d_data.

Fix for a memory leak in InstStrategyCegqi.

Fixing a memory leak in QuantInfo::d_var_mg.

Merge pull request #82 from CVC4/master_for_merge

Squash-merge from the proof branch

squash-merge from proof branch

Fixing memory leaks in Trigger and TriggerTrie.

Fixed help for tear-down-incremental option

Fixing two garbage collection issues in Region and SortModel.

Deleting the CDInstMatchTries in QuantifiersEngine::d_c_inst_match_trie.

Garbage collecting the EqcInfo s in TheoryDatatypes::d_eqc_info.

Garbage collecting the MinisatEmptyNotify for the EagerBitblaster.

Bug fix for define functions + incremental. Minor work on relational triggers.

Deleting the contents of d_modelGlobalsCommands before it is cleared.

New version of the recursive options parsing strategy.

Limit duplicate propagating instances to avoid exponential behavior in QuantConflictFind.

Change internal representative selection for finite domains that do not involve uninterpreted sorts, including bounded integer quantification.

Add options related to interleaving quantifiers and theory combination, changes default behavior.

Faster conditional rewriting for and/or beneath quantifiers. Improvements to sort inference, related to constants. Add several quantifiers options, minor refactoring.

Extend synthesis solver to handle single invocation with additional universal quantification. Refactor query/check-sat to call one internal function in SmtEngine. Make check-synth its own command. Minor work on quant ee.

Minor change to F-Length inference in strings. No internal tracking of cardinality assertions in uf. Change fullModel false array collectModelInfo to assign constants.

Add missing code to track dependencies recursively for string explanations as well.

Work towards complete instantiation for datatypes.

Shorter explanations for strings based on tracking which parts of normal forms are dependent upon which equalities. Add anti-skolemization module to quantifiers. Disable rewriting of non-clashing equalities between same constructors.

Minor options to datatypes.

Refactoring of inferences in strings. Add several options.

Minor improvement to partial qe. Add options for representative selection in FMF.

Add entailment checks between length terms to reduce splitting in strings solver.  Minor additions to datatypes and qcf.

Adding the missing clause_id.h file.

Unifying the definitions of ClauseId to a single source of truth.

Fix term database for non-equal, congruent terms in master equality engine. Disable ITE terms in quant conflict find.

Fixes and improvements for datatypes properties and splitting.

Implement dynamic splitting for quantified formulas.  Minor refactoring of reductions in quantifiers engine.

Correct subtyping for arrays, disable subtyping for predicate subtypes.  Bug fixes in quantifiers related to subtypes/parametric sorts.  Make macros trace dependencies for get-unsat-core. Add regressions.

fix for windows builds

Refactor quantifiers attributes. Make quantifier elimination robust to preprocessing, implement get-qe-disjunct.

Public interface for quantifier elimination.  Minor changes to datatypes rewriter.

More simplification to internal implementation of tuples and records.

Minor change to last commit

Eliminate most of the internal representation infrastructure for tuples and records, replace with datatypes throughout, update cvc printer for tuples/records.  Minor changes to API for records and tuples.

More aggressive conditional rewriting for quantified formulas. Bug fix set incomplete for fmc.

Fix model postprocessor for tuples, add regression.

Fix regression, minor change to output.

Eager introduction of eqc, lemma cache for ground fmf. Apply preprocessing to quantifier instantiations.

Updates related to finite model finding and (co)datatypes. Bug fix enumerator and codatatype rewriter, further simplify fmc.

Changing the way the equality engine explains disequalities.

The explanation for a != b is now:
1. a == find(a)
2. ( find(a) == find(b) ) == false
3. find(b) == b

This simplifies the creation of transitivity proofs for disequalities.

Add two optimizations for datatypes, currently disabled. Bug fix rewriter for selectors applied to codatatype values.

Fixed two more memory leaks in array_info.cpp

Added --omit-dont-cares option which doesn't print model values for
variables known to be don't-cares.

Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. Breaking an edge between the sat solver and command.h.

Removing the CVC4_PUBLIC attribute from the forward declaration of Record in type.h.

Removing the CVC4_NEEDS_REPLACEMENT_FUNCTIONS guard to have a simpler build process.

Generalizing lib/strtok_r.c so that it can always be compiled.

Generalizing the implementation of lib/clock_gettime.c so that it can always be compiled.

Fixing a potentially malformed template expansion when Dump() is disabled.

Fixing a memory leak in bv_subtheory_algebraic.cpp. Also formatting the file.

Adding an virtual destructor to OstreamUpdate.

Making the ManagedOstream::defaultSource() a const function.

Adding a destructor to ProofOutputChannel.

Fixing white spaces in sat_proof.h.

Making the references to std more explicit in didyoumean.cpp.

Fixing a memory leak in array info.

Deleting the dead code in proof/sat_proof.cpp.

Simplify fmc model construction, add regression. Improve FMF debug assertions.

Adding listeners to Options.
- Options
-- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options.
-- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners.
-- Added functions to Options for registering listeners of the notify calls.
-- Changed a number of options to use the new listener infrastructure.
-- Fixed a number of warnings in options.
-- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure.
-- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}.

- Theories
-- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options.

- Ostream Handling:
-- Added new functionality that generalized how ostreams are opened, options/open_stream.h.
-- Simplified the memory management for different ostreams, smt/managed_ostreams.h.
-- Had the SmtEnginePrivate manage the memory for the ostreams set by options.
-- Simplified how the setting of ostreams are updated, smt/update_ostream.h.

- Configuration and Tags:
-- Configuration can now be used during predicates and handlers for options.
-- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/.
-- Moved {Debug,Trace}_tags.* from being generated in options/ into base/.

- cvc4_private.h
-- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's.
-- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations.
-- Made lib/lib/clock_gettime.h a cvc4_private_library.h header.

- Antlr
-- Fixed antlr and cvc4 macro definition conflicts that caused warnings.

- SmtGlobals
-- Refactored replayStream and replayLog out of SmtGlobals.
-- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.

Merged bit-vector and uf proof branch.

Fix bug in fmc mbqi where modelscomputed for mbqi could involve non-constant values. Add regression.

Bug fixes for model construction with codatatypes, add regressions.

Bug fix rewriter for fun defs.

Type enumerators take optional argument indicating fixed cardinalities of uninterpreted sorts. Modify TheoryModelBuilder.  Fix bug in fmf-empty-sorts.

Ensure model construction for parametric sorts involving uninterpreted sorts respect cardinality bounds on when finite model finding is enabled.

Lemma cache datatypes. Do not send true lemma in quantifiers. Minor fix for datatypes model generation for UFinite datatypes when FMF.

Adding a new Listener utility class. Changing the ResourceManager to use Listeners for reporting hard and soft resource out() events.

Removing StatisticsRegistry's static functions current() and registerStat().
- The functionality the get the StatisticsRegistry attached to the SmtEngine was previously through StatisticsRegistry::current(). This is the dominant StatisticsRegistry in the code. (There is another StatisticsRegistry attached to the NodeManager.) Having this be a static function on StatisticsRegistry requires the use of an SmtEngine in the wrong compilation unit.
- Usages of StatisticsRegistry::current() that were visible in prop/{bvminisat,minisat} has been removed. A pointer to the relevant StatisticsRegistry should be passed instead into the constructor.
- The function StatisticsRegistry::current() has been replaced by SmtScope::currentStatisticsRegistry(). SmtScope is in the libcvc4 package, where SmtEngine is available in the compilation unit.
- The function smtStatisticsRegistry() is a synonym for SmtScope::currentStatisticsRegistry() in smt/smt_statistics_registry.h. This header has fewer include dependencies than the one for SmtScope.
- Correspondingly, the static functions StatisticsRegistry::{registerStat, unregisterStat} have been removed. One should instead use smtStatisticsRegistry()->{registerStat,unregisterStat} instead.
- The KEEP_STATISTIC macro has been moved into smt/smt_statistics_registry.h.
- Documents the reason StatisticsRegistry is CVC4_PUBLIC. This lets me remove the warning I added.
- Removing most operators for timespec from statistics_registry.h file. These a bit error prone in clang.
- Most of the really confusing ifdef's in util/statistics_registry.h are gone.

Disabling the RESTART command.

fix windows builds

Fixing a SWIG ordering issue between bitvector and integer.

Improving the documentation of the CVC command CONTINUE.

Removing dead code. StackingMap only appeared in unit tests.

Moving sexpr.{cpp,h,i} from expr/ back into util/.

Add SmtGlobals Class
- The options replayStream, lemmaInputChannel, lemmaOutputChannel have been removed due to their datatypes. These datatypes were previously pointers to types that were not usable from the options/ library.
- The option replayLog has been removed due to inconsistent memory management.
- SmtGlobals is a class that wraps a pointer to each of these removed options. These can each be set independently.
- There is a single SmtGlobals per SmtEngine with the lifetime of the SmtEngine.
- A pointer to this is freely given to the user of an SmtEngine to parameterize the solver after construction.
- Selected classes have been given a copy of this pointer in their constructors.
- Removed the dependence on Node from Result. Moving Result back into util/.

Adding a new class LastExceptionBuffer for the purpose of owning the memory for the last exception C string. This replaces s_debugLastException.

Added propagation rule for array ext lemmas to aid proofs

Modified tear-down-incremental option to take an integer - the integer is the
number of times a check must be executed before the system is reset.

Shuffling around public vs. private headers
- Adding a script contrib/test_install_headers.h that tests whether one can include all cvc4_public headers. CVC4 can pass this test after this commit.
- Making lib/{clock_gettime.h,ffs.h,strtok_r.h} cvc4_private.
- Making prop/sat_solver_factory.h cvc4_private.
- Moving the expr iostream manipulators into their own files: expr_iomanip.{h,cpp}.
- Setting the generated *_options.h files back to being cvc4_private.
-- Removing the usage of options/expr_options.h from expr.h.
-- Removing the include of base_options.h from options.h.
- Cleaning up CPP macros in cvc4_public headers.
-- Changing the ROLL macro in floatingpoint.h into an inline function.
-- Removing the now unused flag -D__BUILDING_STATISTICS_FOR_EXPORT.

Adding a missing header include for cvc4_assert.h in smt_engine_check_proof.cpp for when proofs are disabled.

Merged my changes from experimental branch (new array decision procedure,
translation to bit-vectors for QF_NIA).

Changing the attribute on the forward declaration of SetType in emptyset.h. This seems to give many fewer warnings.

Adding a missing return on the new ArrayStoreAll::operator= .

Miscellaneous fixes
- Splitting the two instances of CheckArgument. The template version is now always defined in base/exception.h and is available in a cvc4_public header. This version has lost its variadic version (due to swig not supporting va_list's). The CPP macro version has been renamed PrettyCheckArgument. (Taking suggestions for a better name.) This is now only defined in base/cvc4_assert.h. Only use this in cvc4_private headers and in .cpp files that can use cvc4_private headers. To use a variadic version of CheckArguments, outside of this scope, you need to duplicate this macro locally. See cvc3_compat.cpp for an example.
- Making fitsSignedInt() and fitsUnsignedInt() work more robustly for CLN on 32 bit systems.
- Refactoring ArrayStoreAll to avoid potential problems with circular header inclusions.
- Changing some headers to use iosfwd when possible.

Enabled array propagation during lemma propagation - this should catch some
conflicts that now require extra splitting.