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

sets: "insert" operator

new™! support for (insert (X (Set X)) (Set X) :right-associative)
from the finte sets theory prosoal.

e.g., (insert 1 2 3 4 (singleton 5))

Automatically make SMT options from command-line option names, warn when not possible.

Fix bug in datatypes options specification

Another fix for 32-bit (amends commit b825605).

Fix for bug543

Updated run script for QF_ABV

Merge pull request #46 from mdeters/bug573

Potential fix for bug 573.

Fix for 32-bit (esp. win32 failing build).

Merge tag 'smtcomp2014-resubmission'

Conflicts:
src/main/portfolio.cpp

Potential fix for bug 573.

Ignore error result when an error is squelched via command verbosity.

Remove leftover debugging output.

Minor language bindings fixes.

Add missing function definition.

sets api example

Merge pull request #34 from mdeters/datatypes-kinds

Datatypes kinds documentation

Merge pull request #37 from mdeters/quants-kinds

Quantifiers kinds documentation

Merge pull request #38 from mdeters/uf-kinds

UF kinds documentation

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

fix sets eager lemmas

cosmetic

mv default care graph function inside the theory implementation

make emptyset construction with no arguments private

rename subseteq to subset in smtlib, all kinds and smt operator names are now consistent

Merge pull request #43 from mdeters/threadstack

stack-size portfolio fix.  boost 1.50 now required

"The intended behavior is this. If Boost threading library is available and portfolio is requested, we do a try-link during configure that sees if we can set a thread attribute. If that compiles and links, we set a #define in cvc4autoconfig.h. There's a new option --thread-stack=N, with N given in megabytes. 0 is default for the platform (which can be based on ulimit I guess as I mentioned in an email). If --thread-stack=N is given to sequential CVC4, it's an error. If it's given to pcvc4 and N > 0 and there isn't support in that Boost version for it, it's an error."

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

Fixing the previous bugfix.

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

Fixing the previous bugfix.

Stack-size portfolio fix.  If using Boost 1.50, --thread-stack=MB is now supported.

Fix some #line annotations.

Don't allow libabc to load extensions at runtime.

stack-size portfolio fix.  boost 1.50 now required

Alternative lazier heuristic for assertion rewriting.

Alternative lazier heuristic for assertion rewriting.