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

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."

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.

Fixing a soundness bug in arithmetic and a roubustness problem in rings.

Fix header check for glpk.h.

Fixing a soundness bug in arithmetic and a roubustness problem in rings.

Merge pull request #41 from mdeters/tianyi-merge

Merge from Tianyi

Squashed commit of the following:

 * Fix a bug in intersection
 * merging...
 * add delayed length lemmas
 * PreRegisterTerm is changed.
 * Bug fix for string-opt2
 * PreRegisterTerm is changed.
 * add delayed length lemmas
 * Bug fix for string-opt2
 * PreRegisterTerm is changed.
 * Bug fix for string-opt2
 * PreRegisterTerm is changed.
 * Bug fix for string-opt2
 * PreRegisterTerm is changed.

Fix header check for glpk.h.

Fatal error if --unconstrained-simp and --produce-models used together (before it would just override the user and turn off models).

Make language explicit in casc scripts

Renaming of SMT2 operator names, kinds for set theory

* SET_SINGLETON kind renamed to just SINGLETON
* "setenum" smt2 opertor renamed to "singleton"[1]
* "in" smt2 operator renamed to "member"[2]

[1] It was anyhow accepting exactly one argument, so was bit misleading
    to call set enumerator.

[2] The corresponding kind was called MEMBER, so this will also make them
    consistent. Only inconsistency now is for subset: kind is called
    SUBSET but operator is called "subseteq".

Output language "cvc3" (as opposed to "cvc" or "cvc4") produces output for CVC3:

1. no decimals used for rational literals
2. queries/check-sats wrapped with PUSH/POP

Minor cleanup stuff.

Better documentation pages.

Re-enable UNTERMINATED_QUOTED_SYMBOL rules.

Merge tag 'smtcomp2014-application'

Conflicts:
contrib/run-script-smtcomp2014-application
src/main/driver_unified.cpp

QuitCommand needs "success" output for trace executor. :-(

Final fixes for smtcomp2014-application.

Merge pull request #39 from mdeters/bv-warnings

Fix compiler warnings in BV-related code (unused vars mostly).

Merge pull request #35 from mdeters/bv-kinds

Bit-vector kinds documentation

Another updated submission strategy.

Another updated submission strategy.

Run in application track with --check-models.

Fix compiler warnings (mostly unused variables).

API documentation improvements.

Run in application track with --check-models.

Fix compiler warnings in BV-related code (unused vars mostly).

Fix to the compatibility library (this does fix the build).

Fix compat-Java layer, should fix build.

Sets kinds documentation

Lower the Java JRE version requirement.

Adjust library dependencies to be more correct (fixes lintian warnings).

Add some missing functions in configuration and compat library.

Slightly-improved kinds documentation for builtin, Boolean, arrays, strings, and arith.

Minor fixes for man pages.

Some minor cleanup and documentation.

fixed build failure

Implement RecordProperties::mkGroundTerm().  Resolves bug #546.

Bit-vector kinds documentation

Datatypes kinds documentation

Quantifiers kinds documentation

UF kinds documentation

fixed merge conflict

added model generation to eager bit-blasting and turned abc off by default

update to abc install instructions

Better --segv-spin messages.

Fix make install-examples.

Proper escaping in option documentation.

Version of the run script that works with trace executor; waiting on StarExec infrastructure for testing.

forgot to add the test with fix

according to bug report, fix was in 6267f3

basic fixes for sets translator, separate binaries

Options script fix.

Fix for mac readline.

Better error for invalid concrete syntax of sorts with too many parens, like (Int).  Thanks to Dan Liew for the report.

Fix GLPK builds: correct access specifier on cut classes.

Java bindings fixes.

Minor Doxygen fixes.

disable unate lemmas when using incremental mode

Fix for pre-C++11 is_sorted().

More minor code cleanup.

No more dependence on libstdc++ or PBDS stuff: remove build stuff that supported it.

New translator features: expand define-funs and combine assertions.

Code cleanup.

Documentation clean-ups.

Another fix for the CASC stuff.

Final preparations for arithmetic for building with libc++.