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

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

merging...

add delayed length lemmas

initialization in model_engine

run_regression using valgrind by setting VALGRIND=1

Minor fix for explanations for co-datatypes.  Bug fix for explanations in FMF for quantifiers over arrays.

Versioning for master.

New versioning for development version.

Cutting release 1.4.

Status for new bug testcase.

Fix a bug in Boolean terms and arrays.  Thanks to Jean-Christophe Filliatre for the report.

Spelling.

fix for windows build

Merge pull request #48 from kbansal/segfaultfix

Segfaultfix

Merge pull request #49 from kbansal/cvcparser

Cvcparser

rm warning

membership cvc token changed to `IS_IN' to avoid conflict with IN used for let

Merge remote-tracking branch 'origin/master' into segfaultfix

friendlyparser: go back upto 2 words looking for match

reorganize friendlyparser, behavior unchanged

sets cvc parser

sets cvc printer

initialize variables

change lemma generation behavior

don't store lemmas in a pending queue, instead generate them right away

doing with pending queue is tricky, needs rethinking to do it properly

Fix cut-release script for new configure rules.

Minor.

Update portfolio_util.cpp

Fix path in CASC J7 scripts, and distribute them with tarball.

Update copyrights.

reword NEWS

Merge pull request #44 from mdeters/prio-queue-updates

BinaryHeap unit test and some usability/build fixes for the data structu...

chat about thread creation

Merge pull request #45 from mdeters/turn-off-strings-exp

Turn strings-exp off by default (for the release)

Update NEWS

Merge pull request #47 from kbansal/sets

Sets theory operators in SMTLIB2 and kinds to use from API have changed. They now are:

SMTLIB: emptyset, singleton*, insert*, union, intersection, setminus, member*, subset*
API: EMPTYSET, SINGLETON*, INSERT*, UNION, INTERSECTION, SETMINUS, MEMBER, SUBSET

(those marked with [*] have changed or been added, others are as earlier)

In the set-logic string use FS to enable sets.

A not-so-well-tested perl command for translating old benchmarks:
  perl -pi -e 's/\(set-logic (.+)_SETS\)/\(set-logic \1FS\)/; s/\(in\b/\(member/g; s/\(setenum\b/\(singleton/g; s/\(subseteq\b/\(subset/g; '

Use FS as the set-logic string for theory of sets