A satisfiability solver for (existential) bit-vector formulas based on the mcSAT framework.
F# SMT Makefile
Switch branches/tags
Nothing to show
Clone or download
Permalink
Failed to load latest commit information.
issues/gh1
tests
z3-mono
z3
.gitattributes
.gitignore
App.config
Bit.fs First public release Jun 8, 2016
BitVector.fs First public release Jun 8, 2016
BitVectorValuation.fs
BooleanValuation.fs First public release Jun 8, 2016
BoundInference.fs
BoundsOperations.fs
BoundsTheory.fs
BoundsValuation.fs
Clause.fs
ClauseDB.fs
ConflictRules.fs
DataBase.fs
DecisionRules.fs
Explain.fs
GlobalOptions.fs
InitializationRules.fs
Interval.fs
LICENSE.txt
Learning.fs
Literal.fs
Main.fs
Makefile
Model.fs
ModelVerification.fs
Numeral.fs
NumeralDB.fs
Preprocessing.fs
PriorityQueue.fs
Problem.fs
PropagationRules.fs
README.md First public release Jun 8, 2016
RLEBVOperations.fs
RLEBVTheory.fs
Rules.fs
SandboxState.fs
Solver.fs
State.fs
Stats.fs
TheoryDB.fs
TheoryRelation.fs
Trail.fs
Util.fs
VariableDB.fs
VariableOrder.fs
WatchManager.fs
Z3Check.fs
mcBV-mono.fsproj
mcBV.fsproj
mcBV.sln
packages.config

README.md

About

mcBV is a solver for (existential) bit-vector formulas (SMT QF_BV) based on the mcSAT framework.

The technical aspects and experimental results are described in: Zeljic, Wintersteiger, Ruemmer: [Deciding Bit-Vector Formulas with mcSAT] (http://research.microsoft.com/apps/pubs/default.aspx?id=264535). Proceedings of SAT, Springer, 2016.

Licence

mcBV is licensed under the MIT licence (see LICENSE.txt).

Requirements

Contributing

To contribute, you will need to complete a Contributor License Agreement (CLA). Briefly, this agreement testifies that you are granting us permission to use the submitted change according to the terms of the project's license, and that the work being submitted is under appropriate copyright.