Compute term indices lazily in TermDb. Optimization for qcf to recognize irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges.  Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.

Removing a null pointer reference that was found by -fsanitize=null.

Update to COPYING

Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.

Reviewed Tim's Asan changes and improved SatProof comments.

Workaround for a problem in clang

More work on inst propagate.  Optimization for qcf to check instances eagerly. Improvements to equality query for disequalities.

Adding an example lsan supression file.

Fixing memory leaks for garbage collection of ResChains in the sat proof implementation. As a part of tracking this down, I've modified a number of accessor functions in TSatProof to be const. An expert in this code will need to do a pass over this.

Fixing a memory leak of the ProofManager.

Fixed typo

More fixes for python interface

Rolling back the rewrite code

Fix for bug 717

Fixes for python bindings

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.