Skip to content

0.7 Release
Compare
Choose a tag to compare
@Gbury Gbury released this 15 Jan 17:36
v0.7
d2f79b1

Release of mSAT version 0.7. Changes include:

Bugfixes

  • Some propagations were forgotten, which caused problems because it could make some conflicts disappear.
  • Similarly, new subterms could be forgotten to be added for semantic decision during temporary propagations
  • Duplicate elimination in clauses was buggy
  • Subterms are now added before simplification, in order to not forget terms
  • Late conflicts (with level lower than the current level) are now allowed
  • User level pushed while the solver is in the UNSAT state now raise an exception, as the solver is not in a coherent state that allows backtracking and storing

Features

  • New backend for Coq Proofs
  • Better interface for the Dot backend (breaking)
  • Propagations are now done at the lowest possible level (instead of the current level), following the possibility for late conflicts

Internal Changes

  • Better travis scripts (using opam 2.0)
  • Some warnings are now fixed
  • Some additional internal assertions particularly concerning theory inputs (conflicts clauses, etc...)
Assets 2
Loading