MathSAT 5

Version 5.6.10 (May 31, 2023)

• Fixed bugs in using the LIA solver incrementally.
• Fixed crash in the combination of FP and Array theories.

Version 5.6.9 (Nov 8, 2022)

• Fixed bugs in the combination of FP and BV theories.

Version 5.6.8 (Jun 30, 2022)

• Fixed bug in incremental model with the FP solver.
• API: added msat_type_id function.
• Made the Linux builds compatible with older versions of glibc and glibcxx.

Version 5.6.7 (Apr 11, 2022)

• Fixed correctness issue with handling const arrays.
• Added option to use partial semantics for fp.to_(s|u)bv operators.
• Fixed encoding of FP to BV operators.
• API: added msat_get_version_id.
• Do not force important symbols to be Boolean constants in allsat.

Version 5.6.6 (Apr 23, 2021)

• Fixed Python3 incompatibilities in the Python API.

Version 5.6.5 (Nov 9, 2020)

• Fixed regression in computing models for LIA.

Version 5.6.4 (Oct 13, 2020)

• Added new AIG API mathsataig.h.
• SMT-LIB: added (nonstandard) function fp.as_ieee_bv.
• Fixed various bugs.

Version 5.6.3 (May 12, 2020)

• SMT-LIB: fixed bug in printing terms with quantified variables.
• Fixed bug in producing interpolants over a combination of theories.

Version 5.6.2 (Apr 21, 2020)

• SMT-LIB: respect the standard :global-declarations option.
• Use a standards-compliant output in the DIMACS interface.
• API: added new function msat_simplify, to perform toplevel propagation programmatically.
• Automatically disable toplevel propagation if bool_model_generation is turned on.

Version 5.6.1 (Mar 18, 2020)

This is a minor release that fixes a couple of glitches.

Version 5.6.0 (Jan 22, 2020)

• Added support for quantifiers in the front-end only. This means that it is now possible to use the MathSAT API to parse/create/manipulate/print formulas involving quantified variables. The solver still works only on quantifier-free input though. For more details, see the new API functions msat_make_exists, msat_make_forall, msat_make_variable, msat_existentially_quantify, msat_term_is_exists, msat_term_is_forall, msat_term_is_variable.
• Fixed various bugs related to theory combination.

Version 5.5.4 (Feb 21, 2019)

This is a minor release that fixes bugs in the nonlinear and array solvers.

Version 5.5.3 (Nov 20, 2018)

This is a minor release that fixes a number of (small) bugs, mostly affecting model generation. We have also added statistics about the main CNF conversion algorithm (number of clauses and auxiliary vars generated).

Version 5.5.2 (May 23, 2018)

This is a minor release that fixes a number of (small) bugs, mostly in the API and SMT-LIB frontend.

Version 5.5.1 (Dec 11, 2017)

This is a "hotfix" release for a misconfiguration of the Windows version. For Linux and OS X users, this version is identical to 5.5.0.

Version 5.5.0 (Dec 5, 2017)

• Added a new solver for the theory of arrays, incorporating ideas from the "weakly equivalent arrays" approach of Christ and Hoenicke. The new solver should generally perform significantly better than the old one, but of course YMMV.
• Added support for non-linear polynomial arithmetic (NRA and NIA), using an incomplete solver based on incremental linearization.
• Fixed some performance regressions in the ACDCL-based solver for FP (introduced in version 5.3.14).
• We no longer provide builds for 32-bit systems by default. If you need one, please contact us.
• The Linux and OSX tarballs now include also shared versions of the MathSAT library.
• Various bugs fixed.

Version 5.4.1 (May 12, 2017)

• Added support for assumptions-based unsat core computation (using -unsat_core_generation=3).
• Added support for parsing (fp b0 b1 b2) terms where the bi's are not numbers.
• Fixed bugs in the LIA and array solvers when used in incremental mode.

Version 5.4.0 (Mar 14, 2017)

• Added reentrant version of the library for Linux x86_64 (for other OSes and architectures, please ask).
• Fix differences in execution across different compilers (due to undefined argument evaluation order).
• Fixed various bugs in model computation.

Version 5.3.14 (Nov 17, 2016)

• FP: fixed bugs in the ACDCL-based solver (-theory.fp.mode=2).
• Fixed a few crashes on incremental usage.
• Fixed broken theory combination when -theory.eq_propagation=false.
• API: added msat_make_eq convenience function.
• Added config param interface_eq_batch_size to limit the number of interface equalities generated in one shot.
• updated default MathSAT configuration by setting (hopefully) more sensible values.

Version 5.3.13 (Aug 22, 2016)

• FP: fixed regression in handling cast operations.
• Fixed performance bottleneck in the generation of interface equalities for theory combination.
• SMTLIB2: fixed bugs in printing terms with uninterpreted sorts.
• API: changed msat_all_sat to avoid enumerating duplicate models. The old behaviour can be restored by setting the option dpll.allsat_allow_duplicates to true.
• Fixed other small bugs.

Version 5.3.12 (Aug 8, 2016)

• FP: fixed bugs in handling casts and parsing numbers with scientific notation.
• BV: fixed bug in computing interpolants via LIA encoding.
• SMTLIB2: improved error messages for syntax errors.
• API: clarified semantics of msat_all_sat.
• Fixed various other small bugs.

Version 5.3.11 (May 3, 2016)

• API: improve robustness wrt. exceptions and misconfiguration.
• Added support for existential quantifier elimination for Linear Integer Arithmetic formulas.
• BV: fixed bug in interpreting division by zero with theory.bv.div_by_zero_mode=1.
• Fixed various other small bugs.

Version 5.3.10 (Jan 7, 2016)

• Fixed a linking problem due to an undefined reference in libmathsat.a.

Version 5.3.9 (Dec 11, 2015)

• Fixed bug in incremental solving with proof generation enabled.
• Fixed bug in combination between FP and BV.
• Fixed compilation errors in the Java API bindings.
• API: added new function msat_apply_substitution.
• API: added new msat_model object and related functions.

Version 5.3.8 (Oct 2, 2015)

• Fixed several bugs in the floating-point solver.
• Fixed bugs in model generation.
• Added option to disable global rewriting rules during preprocessing (see the help for preprocessor.simplification).NOTE: now global rewriting rules are not enabled by default anymore. To restore the behaviour of MathSAT 5.3.7, use -preprocessor.simplification=8.
• Added new option preprocessor.interpolation_ite_minimization to control whether to allow Term-ITEs in interpolants.
• Made quantifier elimination work also in the presence of Term-ITEs.
• API: changed signature of the function msat_add_preferred_for_branching.

Version 5.3.7 (Jul 7, 2015)

• Improved performance of "light-weight" Boolean model generation (i.e. when model_generation=false and bool_model_generation=true).
• Added options for controlling the semantics of bit-vector division by zero (theory.bv.div_by_zero_mode) and floating-point min and max functions when both arguments are zeros (theory.fp.minmax_zero_mode)
• Fixed several minor bugs.

Version 5.3.6 (Jun 12, 2015)

• Now the MathSAT library is distributed as DLL on Windows, making it possible to use the same library with different versions of the compiler.
• Really fixed buffering problem in parsing SMT-LIBv2 files in interactive mode for non-linux platforms.
• Added new Floating-Point functions: fp.sqrt, fp.roundToIntegral, fp.abs, fp.min, fp.max, fp.isPositive, fp.isNegative, fp.isNormal.
• Improved performance of the DPLL preprocessor.
• Improved cut generation strategy of the LA(Z) solver.
• Fixed several bugs.

Version 5.3.5 (Mar 30, 2015)

• Fixed buffering problem in parsing SMT-LIBv2 files in interactive mode.
• Fixed bugs in handling constant arrays.
• Added support for the upcoming version 2.5 of the SMT-LIB standard.

Version 5.3.4 (Mar 13, 2015)

• Added Python and Java bindings for msat_exist_elim.
• Added support for interpolation under assumptions.
• Fixed bug in deleting satisfied clauses in incremental mode.
• Fixed bug in parsing define-fun with parameters and let bindings.
• Added support for more SMT-LIBv2 Floating-Point functions and types.

Version 5.3.3 (Feb 27, 2015)

This version fixes serious regression in the SMT-LIBv2 parser introduced in version 5.3.2.

Version 5.3.2 (Feb 26, 2015)

• Fixed bugs in reading and writing floating-points in decimal notation.
• Added support for fp.to_ubv.
• Fixed bug in the bit-blasting based FP solver in incremental mode.
• Added basic existential quantifier elimination API (see header msatexistelim.h).
• Improved performance of the SMT-LIBv2 parser.
• Improved performance of term creation.
• Made interpolation groups reusable across different backtracking points: now it is not necessary anymore to create a new interpolation group after each msat_push_backtrack_point() call.

Version 5.3.1 (Dec 19, 2014)

• Fixed bug in printing interpolants in SMT2 format.
• Added function msat_ll_set_var_decision to the low-level API.

Version 5.3.0 (Dec 5, 2014)

• Added new low-level API.
• Added support for constant arrays (see msat_make_array_const).
• Improved model generation for Arrays.
• Fixed bug in floating-point format conversion circuit.
• Included Java bindings in the official distribution.

Version 5.2.12 (Jun 5, 2014)

• Fixed bug in solving under assumptions.
• Fixed bad typing of Term-ITEs over integer numbers.
• Fixed bug in floating-point rounding circuit.
• Fixed bugs in interpolation for EUF and BV.
• Fixed nondeterminism in writing API call traces (see the debug.api_call_trace option).
• Fixed bug in the array solver on incremental queries.
• Added support for some non-standard SMT-LIB functions and commands.
• Updated example configuration files in the release tarball.

Version 5.2.11 (Feb 21, 2014)

• Fixed correctness bug in the ACDCL-based Floating-Point solver.
• Fixed crash in BV interpolation.
• Added new API functions msat_annotated_list_from_smtlib2* and msat_annotated_list_to_smtlib2* to read/write a list of terms with attached annotations.
• Included Python bindings in the official distribution.

Version 5.2.10 (Oct 31, 2013)

• Fixed more corner-case bugs in interpolation for combined theories.
• Fixed bug in handling casts from BitVector to FloatingPoint.
• Fixed segfault due to exhaustion of stack space in the internal vector sorting routine.
• Added new API function msat_to_smtlib2_term to generate an SMT-LIBv2 compliant representation of a single msat_term (i.e., without symbol/type declarations or other SMT-LIBv2 commands).

Version 5.2.9 (Oct 17, 2013)

• Fixed several corner-case bugs in interpolation for the combined theory UF+LRA.
• Fixed bug in parsing FloatingPoint numbers.
• Fixed bugs in bit-blasting FloatingPoint terms.
• Fixed bug in model generation in the LA solver, leading to an infinite loop.
• Added support for proof compression/simplification (activated with the config setting dpll.proof_simplification=true).
• Added debugging API functions msat_type_repr and msat_decl_repr.

Version 5.2.8 (Jul 10, 2013)

This version fixes a few glitches in handling the FP theory introduced in version 5.2.7.

Version 5.2.7 (Jul 5, 2013)

• Several minor bugs fixed.
• Fixed memory leak in the SMT-LIB parser.
• Improved support for the FP theory:
  • Made the parser and printer for FP terms compliant with the upcoming official SMT-LIBv2 syntax for the theory;
  • Added rounding mode argument to the API function msat_make_fp_to_bv;
  • Added new API function msat_make_fp_from_ieeebv, and renamed msat_make_fp_as_bv to msat_make_fp_as_ieeebv for consistency (and clarity).

Version 5.2.6 (Mar 29, 2013)

• Fixed various bugs in the combination between FP and BV theories.

Version 5.2.5 (Feb 28, 2013)

• Fixed a bug in theory combination with the eager BV solver;
• Fixed various (mostly corner-case) bugs in interpolation for combined theories;
• Fixed a bug in parsing SMT-LIBv2 scripts using define-fun with parameters.

Version 5.2.4 (Feb 14, 2013)

• Fixed typo in the ACDCL-based floating-point solver that caused MathSAT to return unknown for formulas involving a combination of theories when theory.fp.mode was set to 2 (even when the formula did not involve floats);
• Fixed bug in the EUF solver which caused wrong results when solving under assumptions in some circumstances;
• Added preliminary support for interpolation in the floating-point solver (works only with theory.fp.mode set to 0 or 2. See also the new option theory.fp.interpolation_mode).

Version 5.2.3 (Jan 25, 2013)

• More bug fixes in the floating-point solvers;
• Added new algorithms (symmetric and "McMillan prime") for propositional interpolation (controlled with the -dpll.interpolation_mode option);
• Fixed bug in solving under assumptions;
• Fixed bad return values of some API functions in some (rare) corner cases.

Version 5.2.2 (Nov 20, 2012)

• Fixed various bugs in the solvers for floating points;
• Fixed incrementality bugs in the linear arithmetic solver;
• Re-implemented the array solver based on lemmas-on-demand (activated with -theory.arr.mode=1), which is now significantly more efficient.

Version 5.2.1 (Oct 17, 2012)

This is a bugfix release that fixes some small glitches in version 5.2.0:

• Fixed bug in msat_from_string;
• Fixed undefined reference in the libmathsat.a library;
• Restored Mac OSX build;
• Reorganized options for SAT-level preprocessing;
• Fixed regression in memory consumption when SAT-level preprocessing is turned off.

Version 5.2.0 (Oct 15, 2012)

This is a major release, with several new features:

• Added initial support for the theory of floating point numbers, either via bit-blasting or via a CDCL-like search over intervals;
• Added support for SMT-compatible SAT-level preprocessing (variable elimination and various forms of subsumption);
• Added support for plugging in custom 3rd-party SAT solvers in MathSAT (see the documentation for more details).

Additionally, we fixed bugs in model and interpolant computation, improved the handling of config files, and improved the performance of various preprocessing steps (normalization and toplevel propagation in particular).

Version 5.1.12 (Aug 21, 2012)

Bug fixes:

• Fixed bug in model generation for arrays;
• Fixed correctness bug in handling mixed-integer linear arithmetic constraints;
• Fixed bug in msat_named_list_to_smtlib2 occurring when the input list contained duplicated 0-arity terms;
• Fixed bug in parsing get-value commands in SMT-LIBv2 scripts.

New features:

• Added new config setting printer.bv_number_format for selecting the format in which to print bit-vector numbers (decimal, binary or hexadecimal).

Version 5.1.11 (Aug 14, 2012)

Bug fixes:

• Fixed bug in computing model values for terms containing constants not occurring in the asserted constraints;
• Fixed bug in parsing and printing constants containing a '|' character in SMT-LIBv2.

New features:

• Added option theory.la.laz_enabled to disable the LA(Z) solver;
• Added new API function msat_get_search_stats to retrieve search statistics.

Version 5.1.10 (Jul 25, 2012)

Bug fixes:

• Fixed some 64-bit portability issues causing occasional segmentation faults;
• Fixed bug in model computation when the EUF solver is enabled but no theory combination is needed;
• Fixed bug in printing a model when using the DIMACS front-end;
• Fixed bug in handling distinct when arguments are of type Bool in the SMT-LIBv2 front-end.

New features:

• Added support for garbage collection to MathSAT environments. This is available via the C API through the function msat_gc_env, via the SMT-LIBv2 front-end through the command (gc), and via the command-line through the option -gc_period. (This feature should still be considered somewhat experimental.)

Version 5.1.9 (Jun 26, 2012)

This version fixes a bug in the API function msat_get_theory_lemmas.

Version 5.1.8 (Jun 4, 2012)

This version fixes a bug in the array solver that was causing segmentation faults on some incremental problems.

Version 5.1.7 (May 31, 2012)

Bug fixes:

• Fixed bug in msat_named_list_from_smtlib2 for terms simplifying to true or false;
• Fixed various bugs in model computation;
• Fixed bug in incrementality support for EUF.

New features:

• Added support for extracting unsatisfiable cores with an external "group-oriented" Boolean unsat core extrator to the SMT-LIBv2 front-end;
• Improved performance on combinations of BV+EUF when the "eager" BV solver is used.

Version 5.1.6 (Apr 19, 2012)

This version adds new API functions msat_named_list_from_smtlib2 and msat_named_list_to_smtlib2 which can be used to read/write a list of terms from/to SMT-LIBv2 data.

Version 5.1.5 (Apr 4, 2012)

This version fixes a bug in computing interpolants in the combined theory QF_UFLRA, and a bug in preprocessing bit-vector formulas.

Version 5.1.4 (Mar 23, 2012)

This version fixes several bugs and adds a couple of new features.

Main bug fixes:

• Fixed bug in printing of interpolants in the SMT-LIBv2 front-end;
• Fixed bugs in inlining toplevel equalities in incremental mode;
• Fixed bug in the generation of interpolants for LA;
• Fixed several bugs in model generation, especially in conjunction with free input propagation;
• Fixed crash in the EUF solver in incremental mode;
• Fixed bugs related to theory combination in the Lazy BV solver.

New features:

• Added API functions for retrieving and examining proofs of unsatisfiability generated by MathSAT;
• Added support for interfacing MathSAT with an external Boolean unsat-core extraction tool for computing unsatisfiable cores of SMT formulas;
• Added (optional) new AIG to CNF conversion algorithm based on technology mapping;
• Added support for specifying config settings of MathSAT in SMT-LIBv2 files;
• Improved accuracy of generated debug traces;
• Significantly improved performance of model generation for large problems.

Version 5.1.3 (Dec 29, 2011)

This version fixes a couple of bugs in the SMT-LIBv2 front-end:

• Fixed bug in the get-value command with quoted symbols;
• Fixed bug in the get-interpolant command when the list of groups is empty or the produced interpolant is a single Boolean constant.

Version 5.1.2 (Dec 19, 2011)

This is identical to version 5.1.1, except that the MathSAT library has been extended to include the object code for the main function msat_main, in order to make it possible to relink the solver against a different version of the GMP and/or glibc library. (See the documentation page for more details).

Version 5.1.1 (Dec 16, 2011)

This is the first official release of MathSAT 5. It is a cleaned-up version of the solver entering SMT-COMP 2011, with some bug fixes.