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

Remove some no-longer-required rewrites of array lemmas

Add option --snorm-infer-eq to infer equalities based on normalization in ArithCongruenceManager at standard effort (disabled by default).

Add missing function for regexp to expr manager.

Update native language support for strings.

Minor improvements for alpha equivalence and partial quantifier elimination in incremental mode. Change defaults to addInstantiation method.

Handle parametric datatypes with --quant-ind. Minor updates.

Bug fixes related to parametric datatypes + theory combination + quantifiers. Add regression.

Optimizations for QCF to check relevant domain of variable argument positions eagerly, global ordering mechanism for quantified formulas within check. Refactoring of term database.

Minor fixes for inst match generators. Updates to qip.

More work on instantiation propagation. Enable external filtering of instantiations. All quantifiers strategies terminate when a conflict can be established.

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

Made ProofArray's printing functions non-static, and consequently the data members non-static as well

cardinality operation for finite sets (based on my thesis / ijcar16 paper)

Some further cleanup/fixes pending

This is squash of 39 commits (kbansal/card branch + cleanup):
* add card operator
* local reasoning
* towards graph building
* first implementation
* close cardinality terms
* model building
* more
* more
* more
* Add aggressive sets rewriting.
* Recursively aggressive rewrite sets.
* Fix
* incomplete card2 implementation
* ...
* Avoid using auto in sets.
* fix merge
* more
* ...
* more
* ...
* Fixed for loops
* Slight modification to computeRelevantTerms
* more
* ..
* more
* ...
* mv empty set lemma generation to later point
* more options/reordering
* debug related
* more trace
* ...
* fix merge_nodes, models
* rm warnigns
* fix compile errors
* warning
* bug fixes/cleanup
* mroe fixes
* cleanup
* ...

Minor refactoring of entailment tests and quantifiers util. Initial draft of instantiation propagator.

Refactor trigger selection, revisions to --relational-trigger. Properly process non-standard user-provided triggers. Avoid entailed instantiations based on equality earlier. Refactor core addInstantiation method, add notification mechanism. Add optional argument to entailment checks. Fix bug for duplicate triggers.

New options for trigger selection, add option --strict-triggers. Do not infer alpha equivalence for quantifiers with annotations, limit rewrite operations when triggers are trusted.

Updating the copyright headers and scripts.

s_ prefix for static members

Removed the theory-specific merge reason types. Instead, added a mechanism for dynamically allocating these tags upon request.

Improvements to equality inference module: add missing cases for solvable variables, do not infer equalities that are derivable by transitivity of other inferred equalities, refactor solved vars/eqc into one, option to track explanations.  Handle case when equality inference in quantifiers can derive purely arithmetic ground conflicts at full effort.

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.