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

Support for printing a global let map in LFSC proofs.
Added a flag to enable/disbale this feature (enabled by default).

Also, added some infrastructure for proving rewrite rules.

Merge pull request #85 from CVC4/master_for_proof_merge

Merge from proof branch

Remove NodeListMap from datatypes and equality inference. Add option --dt-blast-splits.

Better infrastructure for proving constant disequality.
Added support for the BV case

A better mechanism for handling BV terms with aliases: inject the alias at the decl_bblast step, instead of having an individual "with alias" rule for each BV operation

Remove NodeListMap from strings, fixes memory leaks. Fix for regexp intersection.

Simple memory fixes, minor cleanup in quantifiers.

Reduce number of passes in quantifiers rewriter.

Fixed a magical bug that only appears when compiling with clang:
The assignment
      d_exprToVariableName[*it] = assignAlias(*it)

Creates an empty value for *it in d_exprToVariableName, causing the assertion in assignAlias to fail

Fix

Merge from proof branch

Revert "Merging proof branch"

This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.

Merging proof branch

Fix to ignore a case of triggers with no free variables.

Initial infrastructure for bounded set quantification (disabled). Refactoring and fixes for --fmf-bound-int. Fix simple memory leaks in strings and bounded integers.

Added Guy to authors list.

Fix build

Updated incremental run script

Disabling failing unit test for now

Removing check that is no longer valid.

Merged QF_UFBV support from experimental branch

Enabled bit-blasting option for QF_UFBV

Updated incremental script

Fixed bug in run script

Added cryptominisat flag to QF_NIA

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

Small change in run script

Changed aig_bitblaster to work with cryptominisat

Disabled m4ri in cryptominisat cmake command

Fix for aig_bitblaster.cpp

Use term indexing in TheoryUF::computeCareGraph. Do not reject model value instantiations in cbqi+BV. Use dag in alpha equivalence check. Fix simple memory leak in fmf.

Updated script, fixed bug in QF_NIA conversion.

Fixed unit test

Fixed build issue due to dummy Cryptominisat constructor.

Forgot to add second patch file.

Merged cryptominisat from experimental branch.

Improvements to symmetry breaking in sygus search. Minor fix for getting instantiations of non-registered quantifiers in sygus.

Fix related to parametric sorts whose interpretation is finite due to uninterpreted sorts + FMF.  Generalizes previous fix in term registration visitor.

Minor fix for strings.

Minor fix to strings, cleanup in datatypes.

Improvements to theory combination + strings: do not return trivial care graph, split on length terms for disequal strings. Term indexing for TheoryDatatypes::computeCareGraph. Minor fix in quantifiers rewriter for entailed conditions, strings cardinality.

Updated AUTHORS file

Refactor modes for sygus+single invocation.  Add option --inst-rlv-cond. Minor fixes for inst max level.

Minor fix cbqi for constant monomials.

Fix memory leak in interactive_shell.cpp

Enable --sygus-direct-eval by default, limit to terms that do not induce Boolean structure.  Minor fixes for bitvectors: rewrite SDIV to total operators when options::bitvectorDivByZeroConst is true, fix collectModelInfo when fullModel=false. Lift ITEs in sygus search. Fix sygus initialization related to cbqi.

Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. Enable e-matching when --strings-exp is enabled.

Add casc scripts. Improvements to qcf related to nested quantifiers and variable ordering.

Fix for --inst-max-level

Add smt comp 2016 scripts. Fix for --relevant-triggers. Add minor optimizations to sygus and qcf.

Re-enabling ite simplification in incremental mode - no reason why
it should be a problem.

Minor clean up, fixes related to sygus.

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.

change to use tuple element representatives to build TC graph for full
effort

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

Update to COPYING

implemented TC for standard effort

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.

update from the master

add utils class for relational theory

Refactored code

Fixed typo

More fixes for python interface

Rolling back the rewrite code

Fix for bug 717

Fixes for python bindings

change transitive closure operator name to TCLOUSRE

- Implement constant rewriter for relational operators for model generation
- fixed a few bugs

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

Remove some no-longer-required rewrites of array lemmas