Better getEqualityStatus for arrays, smarter combination of theories

Merge pull request #54 from kbansal/bugfix_setssegfault

fix getModelValue(<non-preregistered term>)

fix getModelValue(<non-preregistered term>)

Option for more aggressive merging in UEE.

Merge branch '1.4.x'

Fix improper #inclusion of private header outside library.

Fix a command-replay bug in tear-down-incremental mode.  Thanks to Christoph Sticksel for the report.

Proofs- and cores-related segfault fixes (mainly a usability issue), thanks Christoph Sticksel for reporting these.

Add option for aggressive model filtering in conjecture generator (enumerate ground terms).

Merge branch '1.4.x'

Fix infinite loop in --bitblast-aig/--bv-aig-simp options.

Merge branch '1.4.x'

Fix bv options doc.

Fix some configuration-related oddness.

Clarify some licensing-related things.

Finer-grained resource-limiting in quantifiers.

Fix AIG bitblaster for unsat cores.

fix unit test for new fair datatype enumeration

Fair datatype enumeration.

Fix infinite loop in datatypes enumerator.  Minor work on conjecture generator.

Refactor option for uf+cardinality constraints solver.

Partial support for codatatype models.

Support :no-pattern.

Do not throw error when codatatype is not well-founded.  Add option for disabling codatatype reasoning.  Minor cleanup.

Resource spending support in theories (and especially in quantifiers).

cvc4terminate infinite loop fix

cvc4terminate infinite loop fix

Merge branch '1.4.x' while ignoring commit 8d5eb49.

Fix fix. There are no unsat cores in 1.4

Merge branch '1.4.x'

Fix (push) and (pop). Thanks to Christoph Sticksel for the bug report.

Fix soundness bug for quantifier macros involving Int/Real.

Refactor entailment filtering for conjecture generator.  Other minor cleanup.

More refactoring of conjecture generation.  Term generation into own class.

Bug fix variable triggers with --inst-max-level : use term in EQC with minimal instantiation level.

Refactoring of conjecture generator.  Determine subgoals are non-canonical based on ground equalities.  Add filtering options to options file.

Fix bug for variable term triggers within multi-triggers.

Accept user-provided triggers with variable terms.  Flush lemmas before quantifiers check.  Minor fix for conjecture generation.

Update command_executor_portfolio.cpp

Merge remote-tracking branch 'origin/master'

check() optimization

Details of testing here:
http://church.cims.nyu.edu/wiki/User:Kshitij/theorycheckoptimization

Implement and enable --dt-var-exp-quant, cleanup trace messages, minor changes for relevant term filtering.

Work on conjecture generator : do not generalize subterms with concrete values, filter conjectures with ground substitutions whose equality is unknown, simplify generalization depth calculation.  Print --dump-instantiations on sat/unknown.

Set instantiation level on skolemized bodies of quantifiers.  Rename inst-level attribute to quant-inst-max-level

Do not use pure theory terms as single triggers.  Minor cleanup.

fixing bug580 caused by bad bv inequality explanation

fixing bug580 caused by bad bv inequality explanation

Fix assertion in rep_set.cpp, avoid full check in datatypes when in conflict.

Improved SMT-LIBv2 language support for unsat cores.

Bug fixes for --purify-triggers, --dt-force-assignment.

Fix build rule.

Fix Win32 builds.

New option --purify-triggers.  Refactoring of InstMatchGenerator.

remove some debugging code

(it can be brought back from version control, if needed)

improvements to sets sharing

* Add TheorySets::getEqualityStatus(TNode, TNode)
* Add TheorySets::getModelValue(TNode)

fix option alias (minor)

fix type in sets_translate

Unsat core printing.

Some fixes for dump- and get-unsat-core.

Quieter finish to build.

Unit test fix.

One small thing forgotten in core commit.

Java-side interface improvements for unsat cores.

Unsat core infrastruture and API (SMT-LIB compliance to come).

Merge branch '1.4.x'

Fix incorrectly-labeled test.

Merge branch '1.4.x'

Fix operator-printing issue in SMT2.

Fix SMT1 parser :extrasorts/:extrapreds.

Avoid doing work in quantifiers engine when no quantifiers are asserted.

Fix --inst-max-level for strategies that use arbitrary representative terms.

Update bv proof signature and example, after discussions with Liana.

Add option for inductive strengthening based on well-founded induction for integers (default schema).

Merge branch '1.4.x'

Produce error for bad indexed function names in SMT-LIB, remove antlr warning.

Making getEqualityStatus more powerful for bit-vector theory.

Merge branch '1.4.x'

Conflicts:
test/regress/regress0/Makefile.am

Revert a8e0ce67 and add test case (resolves bug #578).

This reverts commit a8e0ce673ba00533a663804cf74500e4d9a3a5cb.

Add support for quantifier-specific instantiation levels.  Add option for setting inst-level 0 only for input terms.

Update smt_engine.cpp

Code changed but comment didn't, might as well get rid of it.

To avoid confusion, permit --enable-staticbinary as an alias for --enable-static-binary.

Fix a build issue for some configurations, thanks Tianyi.

Add draft of BV proof signature (incomplete) and example proof.

Another build fix.

Fix win32 build.

Fix double-linking issue (I think) by simplifying builds/ structure.

First crack at fixing double-linking issues in build system.

Fix for manpages.

fixed bug575 for bv models

fixed bug575 for bv models

Minor fix : do not drop instantiation patterns when merging quantifiers.

Some fixes to symmetry breaker (resolves bug 576).

Some fixes to symmetry breaker (resolves bug 576).

Better support for resource-limiting when there aren't any actual conflicts.

Minor cleanup from previous commit.  Better organization for how quantifiers modules check (introduce QuantifiersEngine::QEffort).

New module for generating candidate equality conjectures used in inductive proofs.  Filtering currently includes: LHS generalizes a term from an active conjecture, terms must be canonical, conjecture must be confirmed by a ground witness, and cannot be falsified by a ground witness.  Refactoring of term database.  QcfEngine now uses central data structure for term indexing.  Add two options for quantifier instantiation : trigger selection mode --trigger-sel=mode, and --inst-no-entail which blocks all quantifier instantiations that are currently entailed (using an incomplete check).

Minor bug fix for exhaustive instantiation in model_engine.

bug fix for pierre 0717

fix for regexp union rewriting

patch for regular expression intersection caching