microsoft
/
mcBV
зеркало из https://github.com/microsoft/mcBV.git
1
0
Форкнуть 0
Код Задачи Пакеты Проекты Релизы Вики Активность
A satisfiability solver for (existential) bit-vector formulas based on the mcSAT framework.
12 коммитов 3 Ветки 1 Тег 153 KiB
F# 96.8%
SMT 3.1%
Перейти к файлу
Christoph M. Wintersteiger 784e6a3265
Merge pull request #5 from microsoft/users/GitHubPolicyService/7beadec5-8f3e-476d-bac7-4c648bffbb9d 
Adding Microsoft SECURITY.MD
 		2023-06-13 11:06:34 +01:00
issues/gh1 Added simplified test cases for #1 2016-09-13 18:53:00 +01:00
tests First public release 2016-06-08 15:14:02 +01:00
z3 First public release 2016-06-08 15:14:02 +01:00
z3-mono First public release 2016-06-08 15:14:02 +01:00
.gitattributes First public release 2016-06-08 15:14:02 +01:00
.gitignore First public release 2016-06-08 15:14:02 +01:00
App.config First public release 2016-06-08 15:14:02 +01:00
Bit.fs First public release 2016-06-08 15:14:02 +01:00
BitVector.fs First public release 2016-06-08 15:14:02 +01:00
BitVectorValuation.fs First public release 2016-06-08 15:14:02 +01:00
BooleanValuation.fs First public release 2016-06-08 15:14:02 +01:00
BoundInference.fs First public release 2016-06-08 15:14:02 +01:00
BoundsOperations.fs First public release 2016-06-08 15:14:02 +01:00
BoundsTheory.fs Potential partial fixes for issue #1 2016-07-25 19:17:45 +01:00
BoundsValuation.fs First public release 2016-06-08 15:14:02 +01:00
Clause.fs Bugfixes for conflict generalization. 2016-09-16 20:11:55 +01:00
ClauseDB.fs First public release 2016-06-08 15:14:02 +01:00
ConflictRules.fs First public release 2016-06-08 15:14:02 +01:00
DataBase.fs formatting/style/whitespace 2016-09-13 16:06:43 +01:00
DecisionRules.fs First public release 2016-06-08 15:14:02 +01:00
Explain.fs Bugfixes for conflict generalization. 2016-09-16 20:11:55 +01:00
GlobalOptions.fs First public release 2016-06-08 15:14:02 +01:00
InitializationRules.fs First public release 2016-06-08 15:14:02 +01:00
Interval.fs First public release 2016-06-08 15:14:02 +01:00
LICENSE.txt First public release 2016-06-08 15:14:02 +01:00
Learning.fs First public release 2016-06-08 15:14:02 +01:00
Literal.fs First public release 2016-06-08 15:14:02 +01:00
Main.fs Added version/copyright string 2016-06-08 15:17:36 +01:00
Makefile First public release 2016-06-08 15:14:02 +01:00
Model.fs First public release 2016-06-08 15:14:02 +01:00
ModelVerification.fs First public release 2016-06-08 15:14:02 +01:00
Numeral.fs First public release 2016-06-08 15:14:02 +01:00
NumeralDB.fs Numeral DB bug fix for temp-mode snapshots 2016-09-13 16:21:52 +01:00
Preprocessing.fs First public release 2016-06-08 15:14:02 +01:00
PriorityQueue.fs First public release 2016-06-08 15:14:02 +01:00
Problem.fs First public release 2016-06-08 15:14:02 +01:00
PropagationRules.fs Bugfixes for conflict generalization. 2016-09-16 20:11:55 +01:00
README.md First public release 2016-06-08 15:14:02 +01:00
RLEBVOperations.fs First public release 2016-06-08 15:14:02 +01:00
RLEBVTheory.fs formatting/style/whitespace 2016-09-13 16:06:43 +01:00
Rules.fs Bugfixes for conflict generalization. 2016-09-16 20:11:55 +01:00
SECURITY.md Microsoft mandatory file 2023-06-12 19:11:57 +00:00
SandboxState.fs First public release 2016-06-08 15:14:02 +01:00
Solver.fs First public release 2016-06-08 15:14:02 +01:00
State.fs First public release 2016-06-08 15:14:02 +01:00
Stats.fs First public release 2016-06-08 15:14:02 +01:00
TheoryDB.fs First public release 2016-06-08 15:14:02 +01:00
TheoryRelation.fs First public release 2016-06-08 15:14:02 +01:00
Trail.fs Merge branch 'master' of https://github.com/Microsoft/mcBV into issue1 2016-09-16 20:14:21 +01:00
Util.fs First public release 2016-06-08 15:14:02 +01:00
VariableDB.fs First public release 2016-06-08 15:14:02 +01:00
VariableOrder.fs First public release 2016-06-08 15:14:02 +01:00
WatchManager.fs formatting/style/whitespace 2016-09-13 16:06:43 +01:00
Z3Check.fs Bugfixes for conflict generalization. 2016-09-16 20:11:55 +01:00
mcBV-mono.fsproj First public release 2016-06-08 15:14:02 +01:00
mcBV.fsproj First public release 2016-06-08 15:14:02 +01:00
mcBV.sln First public release 2016-06-08 15:14:02 +01:00
packages.config First public release 2016-06-08 15:14:02 +01:00

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.