Merge remote-tracking branch 'origin/master'

Fixed two bugs

Added fitsSignedLong and fitsUnsignedLong

Initial infrastructure for ExtTheory, generalize extended term handling in TheoryStrings to use this.

Expression sharing on demand in LFSC (replace definitionally equivalent child arguments after successful comparison).

Enable bounded set membership with --fmf-bound. Map to term models for bounded set membership.

Add a few more regressions.

Minor fixes to model construction to take singleton equivalence classes into account (fixes sets+dt model bug). Minor fix for mixed int/real quantifier instantiation.

Merge pull request #90 from 4tXJ7f/fewer_preproc_holes

Add support for fewer preprocessing holes

Add support for fewer preprocessing holes

This commit adds support for the --fewer-preprocessing-holes flag. This
flag changes the preprocessing part in proofs in two ways: it (1)
removes assertions that are just restating inputs and uses the inputs
directly instead and it (2) changes the form of the preprocessed
assertions to contain the input that they originate from.

The code in this commit is mostly taken from the proofs branch in Guy's
fork.

Minor change to strings, introduce proxy vars only when necessary.

Improvements to strings: work on propagations for reverse normal form processing. Better handling of disequalities, constant splitting and neg contain approximation. Introduce proxy vars for replace. Refactoring.

Merge pull request #89 from 4tXJ7f/fix_proof_spaces

Fix missing/redundant spaces in proofs

Fixes for sep star rewrite.

Fix missing/redundant spaces in proofs

Before, in some cases, e.g. when printing sorts and in resolution
proofs, the proofs contained redundant and/or missing spaces. With this
commit, CVC4 now prints out `(trust_f (= (Array Index Element) let10
let12)` instead of `(trust_f (= (Array Index  Element )let10 let12))`.

Merge pull request #88 from 4tXJ7f/fix_comments

Minor: add/fix comments, remove redundant includes

Minor: add/fix comments, remove redundant includes

Fixed an issue where arrays proofs would sometimes have an extra ")" at the end.

Merge pull request #87 from 4tXJ7f/fix_oob_access

Fix out-of-bounds access in ExprManager

Prioritize inferences when processing normal forms in strings.

fixed construction of TC graph

The "aggressive" optimizer for lemma L now returns the conjunction of all lemmas L' that originated from L and were used in the unsat core

fixed construction of TC graph

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

Bug fix involving negated lemmas

Fix bug 749.

Add the negative conjunction case

Fix out-of-bounds access in ExprManager

The size of `d_exprStatisticsVars` was `LAST_TYPE` which was not enough
because the INC_STAT macro tries to access
`d_exprStatisticsVars[LAST_TYPE]` in some cases, resulting in an
out-of-bounds access. Found bug with UBSan.

Proper instrumentation of the preprocessing phase

proper handling of ITEs

Proper handling of IFF lemmas in the unsat core.
Don't return duplicates in the unsat core

Added an option for a more aggressive weakest implicant optimization

If we can't find a weaker implicant, fail gracefully and return the original lemma

Merge pull request #86 from 4tXJ7f/fix_warnings

Fix warnings in src/proof

Fix warnings in src/proof

Fix warning due to `ProofLetCount` being defined as `struct` in
`proof_utils.h` and `class` in `proof.h`. Fix warnings due to different
number of arguments of `printConstantDisequalityProof()` and
`printTheoryLemmaProof()` in subclasses.

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

Bug fix:
If a lemma (a disjunction) has a "false" literal in it, it can be ignored, but a "true" literal really should stay

Add option to minimize sygus solutions based on using weakest implicants of instantiations in unsat cores.

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

Letification of BV constants

Minor improvements to strings related to constant splitting, including a few options (disabled by default).

Added functionality to retrieve a lemma's "weakest implicant" in the unsat core. Currently, lemmas that are not conjunctions and their own weakest implicants; but for lemmas that *are* conjunctions, we may return only a subset of the conjuncts.

Bug fix

Propagate the usage of proof let maps into constant disequality proofs

Bug fix

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

cleanup

Use letification for the aliasing declarations as well (consequently, print the global let map before the aliasing part)

Proper handling for lemmas that are conjuncts:
Record a separate recipe for each conjunct, but have as the "original lemma" in this recipe the complete conjunction, so that we can report this to the theory solver later, if asked.

Refactoring: instead of propagating the proof recipes from the theory engine to the prop engine and cnf stream to be registered there, just register them at the theory engine - as the prop engine and cnf stream don't change them.

more code refactor

more code refactor

refactored code

Minor, error handling for polymorphism + sep logic.

Fixes for strings, explanations for constant split propagations, substr under concat rewrite. Avoid duplicate re.range length lemmas.

bug fixes for reachablity check

Infrastructure for storing and printing heap models for separation logic. Ensure value of sep.nil is correct in models. Print instantiations as sexprs.

Print only instantiations that are in the unsat core when --proof is enabled.  Add option to minimize sygus solutions based on unsat core (disabled by default).

Infer conflicts in strings based on abstracting equality as contains. Minor cleanup.

Bug fix

Allow a caller to query whether an unsat core is available or not

Add infrastructure for tracking instantiation lemmas (for proofs, and minimization of --dump-instantiations, qe and synthesis solutions). Eliminate quantified arithmetic variables that only have lower/upper bounds. Cleanup strings preprocess, minor fix for str.replace semantics. Reorder cegqi before fmf. Minor cleanup.

Refactor strings extf evaluation info. Ensure strings eager preprocess eliminates all extf symbols during ppRewrite. Add options stringGuessModel and stringUfReduct. Minor optimizations.

Moved the assertion to a better spot

The ProofManager now allows theory solvers to get their lemmas that participate in the unsat cores.
Currently this is only limited to lemmas generated via the d_out->lemma() interface, i.e. no propagations
and conflict lemmas.

Minor simplification to normal form explanations.

added support for expansion of transitive closure

Minor fix to last commit.

Simplifications for strings normal forms, fix case for concat reps in normal forms.

Ensure heap disjointness in sep refinements.

Refactoring of strings preprocess module. When enabled, apply eager preprocess during ppRewrite instead of during processAssertions. Simplify reduction for contains.  Fix bug in explanations for F_EndpointEq. Minor cleanup for sep.

A few proof bugs fixed

Minor cleanup in strings, mostly related to negated str.contains.

Add comment field for model, resolves hack for printing sep logic models.

Refactor last call for theories, only create one model when quantifiers are enabled. Fix sep.nil preregistration in TheorySep.

Add option --trigger-active-sel. Recognize simple triggers with polarity. Do not drop patterns from merged prenex (fixes bug 743).

resolved merge conflicts

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

Conflicts:
proofs/signatures/Makefile.am
src/Makefile.am
src/expr/datatype.cpp
src/options/datatypes_options
src/options/options_template.cpp
src/options/quantifiers_options
src/proof/arith_proof.cpp
src/proof/arith_proof.h
src/proof/array_proof.cpp
src/proof/array_proof.h
src/proof/bitvector_proof.cpp
src/proof/bitvector_proof.h
src/proof/cnf_proof.cpp
src/proof/cnf_proof.h
src/proof/proof_manager.cpp
src/proof/proof_manager.h
src/proof/sat_proof.h
src/proof/sat_proof_implementation.h
src/proof/skolemization_manager.h
src/proof/theory_proof.cpp
src/proof/theory_proof.h
src/proof/uf_proof.cpp
src/proof/uf_proof.h
src/prop/cnf_stream.cpp
src/prop/cnf_stream.h
src/prop/minisat/core/Solver.cc
src/prop/prop_engine.cpp
src/prop/prop_engine.h
src/prop/theory_proxy.cpp
src/smt/smt_engine.cpp
src/smt/smt_engine_check_proof.cpp
src/theory/arrays/array_proof_reconstruction.cpp
src/theory/arrays/theory_arrays.cpp
src/theory/bv/eager_bitblaster.cpp
src/theory/bv/lazy_bitblaster.cpp
src/theory/datatypes/theory_datatypes.cpp
src/theory/quantifiers/alpha_equivalence.cpp
src/theory/quantifiers/candidate_generator.cpp
src/theory/quantifiers/candidate_generator.h
src/theory/quantifiers/ce_guided_single_inv.cpp
src/theory/quantifiers/ceg_instantiator.cpp
src/theory/quantifiers/conjecture_generator.cpp
src/theory/quantifiers/equality_infer.cpp
src/theory/quantifiers/equality_infer.h
src/theory/quantifiers/inst_match_generator.cpp
src/theory/quantifiers/inst_propagator.cpp
src/theory/quantifiers/inst_propagator.h
src/theory/quantifiers/inst_strategy_e_matching.cpp
src/theory/quantifiers/inst_strategy_e_matching.h
src/theory/quantifiers/instantiation_engine.cpp
src/theory/quantifiers/model_builder.cpp
src/theory/quantifiers/model_engine.cpp
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/quantifiers/quant_conflict_find.h
src/theory/quantifiers/quant_split.cpp
src/theory/quantifiers/quant_util.cpp
src/theory/quantifiers/quantifiers_rewriter.cpp
src/theory/quantifiers/quantifiers_rewriter.h
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers/term_database.h
src/theory/quantifiers/trigger.cpp
src/theory/quantifiers/trigger.h
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
src/theory/sets/kinds
src/theory/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_private.h
src/theory/sets/theory_sets_rewriter.cpp
src/theory/sets/theory_sets_type_rules.h
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/equality_engine.cpp
test/regress/regress0/fmf/Makefile.am
test/regress/regress0/quantifiers/Makefile.am
test/regress/regress0/strings/Makefile.am
test/regress/regress0/sygus/Makefile.am
test/regress/regress0/sygus/max2-univ.sy

fixes bugs in std effort for TC

When proving a lemma, ignore literals that don't belong to the theory in question, except for equalties

Handle bitvector lemmas where a literal gets rewritten into false, and consequently the lemma doesn't match a recorded conflict

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

Support for the letification of chained AND and OR operations in LFSC proofs

debug statement

Merge remote-tracking branch 'origin/master'

test

reimplemented std effort for TC

Add theory/sep/kinds to EXTRA_DIST to fix distcheck failures.

Fixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black,
re-enabled cdmap_black.

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

Addressed a bug that occurs when proof production is triggered via text flags in the input.
Separated some initialization into two phases:
1. Those that can be done when the proof compiliation flag is set
2. Those that can be done only when the --proof option is set.
For #2, deferred their execution until the text flags in the input have been processed

Minor change to sep/kinds

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

Fixed a bug where the proofManager's init() call was not getting called, resutling a null point deference

Fix unit test.

Cleanup from last commit, treat sep.nil as variable kind.

Support for separation logic. Enable cbqi by default for pure BV.

Add syguscomp2016 scripts.

Dummy commit.

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

LFSC letification is true by default