c-cube/mc2

[research] A modular SMT solver in OCaml, based on mcSAT

MC2

MC² ("Model Constructing Modular Contraption") is a modular SMT solver in OCaml, based on the MCSat calculus.

It implements most of the techniques described in de Moura and Jovanović (VMCAI 13), in around 7 thousands lines of code (not including dependencies). EUF is supported via congruence lemmas; LRA is based on a conflict-driven Fourier-Motzkin solver. Boolean formulas are turned into clauses during preprocessing, using the Tseitin encoding; the core solver handles clauses like a regular SAT solver, as the code was originally derived from msat (github.com/Gbury/mSAT), itself derived from Alt-Ergo Zero. However most of the code was modified or rewritten by Simon Cruanes while working at Veridis at Loria, Nancy, France; and later in his own free time.

Documentation

https://c-cube.github.io/mc2/

Short Summary

MC² is a SMT solver. SMT solvers are automatic tools that try to assess whether a given logic formula is satisfiable (admits a model, an interpretation that makes it true) or unsatisfiable (no interpretation can make it true; it is absurd, and its negation is a theorem). Prominent solvers include Z3, cvc5, Yices 2, and others; all of them follow the CDCL(T) paradigm. Most of these solvers are implemented in C or C++.

In contract, MC² is based on the mcSAT calculus (see [fmcad'13] and [vmcai'13]). mcSAT is fundamentally different from CDCL(T); it is a so-called natural SMT calculus where the boolean reasoning of CDCL is extended so as to be able to assign values to non-boolean variables (such as linear arithmetic variables, for example). As a calculus it can be considered stronger, in some sense, because it can have shorter proofs by virtue of being allowed to introduce new terms during the proof search. On the other hand, mcSAT is not as well known or battle tested as CDCL(T). MC² started as an experiment to try and reproduce some results from vmcai'13.

COPYRIGHT

This program is distributed under the Apache Software License version 2.0. See the enclosed file LICENSE.

mc2's Issues

missing support for boolean subterms

answers sat on this unsat problem:

(declare-sort U 0)
(declare-fun f (Bool) U)
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(assert
  (distinct (f a) (f b) (f c)))
(check-sat)

bug in `p-0-bucket_s7.smt2`

reports spurious "unsat". need proof checking?

missing conversion

remove push/pop and add assumptions instead

might make it easier to fix #2 (no more base level)