New release: Boolector version 2.0.0

[Mathias Preiner]

There is a new version (2.0.0) of Boolector available at:

http://fmv.jku.at/boolector/

Here is a list of the most important changes since version 1.6.0:

• General:

• Boolector Python API

• Cloning support

• Support for uninterpreted functions

• New improved model generation, supports two modes now:

• --model-gen=1 or -m: generate model for all asserted expressions (same as model generation in previous versions)

• --model-gen=2 or -m -m: generate model for all created expressions

• Fixed several rewriting bugs

• Refactored a lot of code

• New output format for models

• Optimizations:

• Re-enabled and fixed unconstrained optimization

• Don't care reasoning on bit vector skeleton

• Dual propagation optimization

• Justification optimization

• API changes:

• API functions return node of type BoolectorNode instead of BtorNode

• Options

• Can be set via environment variables or boolector_set_opt

• New options (for a complete list of options please refer to the documentation of boolector_set_opt)

• Deprecated functions:

• boolector_get_symbol_of_var (use boolector_get_symbol)

• boolector_enable_model_gen (use boolector_set_opt ("model_gen", 1))

• boolector_generate_model_for_all_reads (use boolector_set_opt ("model_gen", 2))

• boolector_enable_inc_usage (use boolector_set_opt ("incremental", 1))

• boolector_set_rewrite_level (use boolector_set_opt ("rewrite_level", ...))

• boolector_set_verbosity (use boolector_set_opt ("verbosity", ...))

• boolector_set_loglevel (use boolector_set_opt ("loglevel", ...))

• New API functions to create uninterpreted functions

• boolector_uf

• boolector_bool_sort

• boolector_bitvec_sort

• boolector_fun_sort

• Limited boolector_sat calls

• set lemmas on demand limit

• set conflict limit for SAT solver

• Notes:

• If uninterpreted functions occur in the formula it is not possible to dump the formula to BTOR 1.2 format (this will be fixed with BTOR 2.0).

The documentation of Boolector and it's public APIs can be found at: http://fmv.jku.at/boolector/doc/

This version of Boolector is available under a restricted license for non-commercial use.

This source release is packed with the SAT competition 2014 version of Lingeling (azd).


Mathias

[yoshihid...@pacificdesign-japan.com]

Dear Mathias-san:

Great!!!!
This is so great, Mathias-san!
I would like to confirm the lingeling performance and many other items.
I believe many people are waiting for your release.

Thanks again for you and Boolector's team research & development activities.

Best Regards,
Yoshihide Sugiura

2014年10月22日水曜日 0時00分58秒 UTC+9 Mathias Preiner: