Skip to content

Commit

Permalink
Initial commit
Browse files Browse the repository at this point in the history
  • Loading branch information
bastianeicher committed Feb 20, 2019
0 parents commit 567cea2
Show file tree
Hide file tree
Showing 35 changed files with 1,174 additions and 0 deletions.
127 changes: 127 additions & 0 deletions .editorconfig
Original file line number Diff line number Diff line change
@@ -0,0 +1,127 @@
root = true

[*]
charset = utf-8
end_of_line = lf
indent_style = space
indent_size = 4
trim_trailing_whitespace = true
insert_final_newline = true
keep_existing_linebreaks = true
max_line_length = off

[CNAME]
insert_final_newline = false

[*.{json,xml,yml,htm,html,js,ts,css,scss,less}]
indent_size = 2

[*.{*proj,resx,config,ruleset,cd,props,targets,nuspec}]
end_of_line = crlf
indent_size = 2

[*.{txt,cs,ps1,psd1,manifest}]
end_of_line = crlf

[*.{bat,cmd}]
charset = latin1
end_of_line = crlf

[*.sln]
end_of_line = crlf
indent_style = tab

[*.{md,resx,Designer.*}]
trim_trailing_whitespace = false

[*.cs]
# Indentation
csharp_indent_block_contents = true
csharp_indent_braces = false
csharp_indent_case_contents = true
csharp_indent_switch_labels = true
csharp_outdent_binary_ops = true
csharp_outdent_dots = true
csharp_align_linq_query = true
csharp_align_multiline_parameter = true
csharp_align_multiline_calls_chain = true
csharp_align_multiline_binary_expressions_chain = true
csharp_align_multiline_array_and_object_initializer = false

# Line breaks
csharp_new_line_before_catch = true
csharp_new_line_before_else = true
csharp_new_line_before_finally = true
csharp_new_line_before_members_in_object_initializers = false
csharp_new_line_before_open_brace = all
csharp_blank_lines_around_single_line_field = 0
csharp_blank_lines_inside_region = 0
csharp_blank_lines_around_region = 0
csharp_blank_lines_after_block_statements = 0
csharp_empty_block_style = together
csharp_place_simple_blocks_on_single_line = true
csharp_place_simple_initializer_on_single_line = true
csharp_place_attribute_on_same_line = if_owner_is_single_line
csharp_place_expr_method_on_single_line = true
csharp_place_constructor_initializer_on_same_line = false
csharp_wrap_object_and_collection_initializer_style = chop_if_long
csharp_wrap_array_initializer_style = chop_if_long
csharp_wrap_parameters_style = chop_if_long
csharp_preserve_single_line_blocks = true
csharp_keep_existing_arrangement = true

# Spacing
csharp_space_after_cast = false
csharp_space_after_colon_in_inheritance_clause = true
csharp_space_after_comma = true
csharp_space_after_dot = false
csharp_space_after_keywords_in_control_flow_statements = true
csharp_space_after_semicolon_in_for_statement = true
csharp_space_around_binary_operators = before_and_after
csharp_space_before_colon_in_inheritance_clause = true
csharp_space_before_comma = false
csharp_space_before_dot = false
csharp_space_before_semicolon_in_for_statement = false
csharp_space_before_open_square_brackets = false
csharp_space_between_empty_square_brackets = false
csharp_space_between_method_declaration_name_and_open_parenthesis = false
csharp_space_between_method_declaration_parameter_list_parentheses = false
csharp_space_between_method_declaration_empty_parameter_list_parentheses = false
csharp_space_between_method_call_name_and_opening_parenthesis = false
csharp_space_between_method_call_parameter_list_parentheses = false
csharp_space_between_method_call_empty_parameter_list_parentheses = false
csharp_space_between_square_brackets = false
csharp_space_within_empty_braces = false

# Style
csharp_parentheses_redundancy_style = remove_if_not_clarifies_precedence
csharp_allow_comment_after_lbrace = true
csharp_braces_for_ifelse = required_for_multiline
csharp_braces_for_for = required_for_multiline
csharp_braces_for_foreach = required_for_multiline
csharp_braces_for_while = required_for_multiline
csharp_braces_for_using = required_for_multiline
csharp_braces_for_lock = required_for_multiline
csharp_braces_for_fixed = required_for_multiline
csharp_style_var_for_built_in_types = false
csharp_style_var_when_type_is_apparent = true
csharp_style_expression_bodied_constructors = false
csharp_style_expression_bodied_accessors = true
csharp_style_expression_bodied_methods = true
csharp_style_expression_bodied_properties = true
csharp_local_function_body = expression_body
csharp_style_qualification_for_event = false
csharp_style_qualification_for_field = false
csharp_style_qualification_for_method = false
csharp_style_qualification_for_property = false
csharp_style_pattern_matching_over_as_with_null_check = true
csharp_style_pattern_matching_over_is_with_cast_check = true
csharp_style_object_initializer = true
csharp_style_collection_initializer = true
csharp_style_explicit_tuple_names = true
csharp_style_null_propagation = true
csharp_style_coalesce_expression = true
csharp_style_conditional_delegate_call = true
csharp_style_throw_expression = true
csharp_style_predefined_type_for_locals_parameters_members = true
csharp_style_predefined_type_for_member_access = true
6 changes: 6 additions & 0 deletions .gitattributes
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
# Disable linebreak normalization
* -text

# Visual Studio file types
*.cs diff=csharp
*.sln merge=union
13 changes: 13 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
*.user
*.bak

# Caches
/src/.vs/
/src/.idea/
/src/_ReSharper.*/
/src/*/obj/
/src/*/bin/
/doc/*.tag

# Output
/artifacts/
14 changes: 14 additions & 0 deletions .travis.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
dist: xenial
language: minimal
sudo: required
before_install:
- sudo apt-get install -y --no-install-recommends 0install-core
script:
- doc/build.sh
deploy:
provider: pages
skip-cleanup: true
local-dir: artifacts/Documentation
github-token: $GITHUB_TOKEN
on:
tags: true
21 changes: 21 additions & 0 deletions COPYING.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
The MIT License (MIT)

Copyright (c) Bastian Eicher

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
15 changes: 15 additions & 0 deletions GitVersion.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
mode: ContinuousDeployment

branches:
# Mainline branches
develop:
tag: alpha
increment: patch
master:
tag: beta

# Stabilization branches
release:
tag: rc
hotfix:
tag: rc
55 changes: 55 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,55 @@
# NanoByte SAT Solver

[![NuGet](https://img.shields.io/nuget/v/NanoByte.SatSolver.svg)](https://www.nuget.org/packages/NanoByte.SatSolver/)
[![API documentation](https://img.shields.io/badge/api-docs-orange.svg)](https://sat-solver.nano-byte.net/)
[![Build status](https://img.shields.io/appveyor/ci/nano-byte/sat-solver.svg)](https://ci.appveyor.com/project/nano-byte/sat-solver)
NanoByte SAT Solver is a DPLL Boolean Satisfiability Solver for .NET.

This library is available for .NET Framework 2.0+ and .NET Standard 1.0+.

## Usage

First you need to choose the underlying type to use for Literals in Boolean Formulas. This will often be `int` or `string` but you can also use any other type that implements the `IEquatable<T>` interface. You can then create an instance of `Solver<T>`:

```csharp
var solver = new Solver<string>();
```

The library enables you to express Boolean Formulas using implicit casting and operators for human-friendly sample and test code:
```csharp
Literal<string> a = "a", b = "b", c = "c", d = "d";
var formula = (a | b) & (!a | c) & (!c | d) & a;
```

For constructing Formulas at run-time you can use a collection-like interface instead:
```csharp
var formula = new Formula<string>
{
new Clause<string> {Literal.Of("a"), Literal.Of("b")},
new Clause<string> {Literal.Of("a").Negate(), Literal.Of("c")},
new Clause<string> {Literal.Of("c").Negate(), Literal.Of("d")},
new Clause<string> {Literal.Of("a")}
};
```

Finally, you can use the solver to determine whether a Formula is satisfiable:
```csharp
bool result = solver.IsSatisfiable(formula);
```

When the Solver needs to choose a Literal to assign a truth value to during backtracking, it simply picks the first unset Literal from the list. You can replace this with your own domain-specific logic for better performance by deriving from `Solver<T>` and overriding the `ChooseLiteral()` method.

## Building

The source code is in [`src/`](src/), a project for API documentation is in [`doc/`](doc/) and generated build artifacts are placed in `artifacts/`.

You need [Visual Studio 2017](https://www.visualstudio.com/downloads/) to perform a full build of this project.
You can build for .NET Standard on Linux using just the [.NET Core SDK 2.1+](https://www.microsoft.com/net/download). Additionally installing [Mono 5.10+](https://www.mono-project.com/download/stable/) allows you to also build for .NET Framework. The build scripts will automatically adjust accordingly.

Run `.\build.ps1` on Windows or `./build.sh` on Linux. These scripts take a version number as an input argument. The source code itself contains no version numbers. Instead the version is picked by continuous integration using [GitVersion](http://gitversion.readthedocs.io/).

## Contributing

We welcome contributions to this project such as bug reports, recommendations and pull requests.

This repository contains an [EditorConfig](http://editorconfig.org/) file. Please make sure to use an editor that supports it to ensure consistent code style, file encoding, etc.. For full tooling support for all style and naming conventions consider using JetBrain's [ReSharper](https://www.jetbrains.com/resharper/) or [Rider](https://www.jetbrains.com/rider/) products.
42 changes: 42 additions & 0 deletions appveyor.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
image:
- Visual Studio 2017
- Ubuntu

for:
- matrix:
only:
- image: Visual Studio 2017

cache:
- '%USERPROFILE%\.nuget\packages -> **\*.csproj'

before_build:
- gitversion /l console /output buildserver

build_script:
- ps: src\build.ps1 $env:GitVersion_NuGetVersion

test_script:
- ps: src\test.ps1

artifacts:
- path: artifacts\Release\*.nupkg

deploy:
provider: Environment
name: NuGet
on:
appveyor_repo_tag: true

- matrix:
only:
- image: Ubuntu

cache:
- '$HOME/.nuget/packages -> **/*.csproj'

build_script:
- sh: src/build.sh

test_script:
- sh: src/test.sh
9 changes: 9 additions & 0 deletions build.ps1
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
Param ($Version = "1.0-dev")
$ErrorActionPreference = "Stop"
pushd $(Split-Path -Path $MyInvocation.MyCommand.Definition -Parent)

src\build.ps1 $Version
src\test.ps1
doc\build.ps1

popd
7 changes: 7 additions & 0 deletions build.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
#!/bin/sh
set -e
cd `dirname $0`

src/build.sh ${1:-1.0-dev}
src/test.sh
doc/build.sh
1 change: 1 addition & 0 deletions doc/CNAME
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
sat-solver.nano-byte.net
20 changes: 20 additions & 0 deletions doc/Doxyfile
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
PROJECT_NAME = "NanoByte SAT Solver"

INPUT = . ../src
USE_MDFILE_AS_MAINPAGE = main.md
STRIP_FROM_PATH = ../src
RECURSIVE = YES
EXCLUDE_PATTERNS = */UnitTests/* */Properties/* */obj/* */bin/*

OUTPUT_DIRECTORY = ../artifacts/Documentation
GENERATE_TAGFILE = ../artifacts/Documentation/nanobyte-sat-solver.tag
HTML_OUTPUT = .

GENERATE_LATEX = NO
CASE_SENSE_NAMES = NO

EXTRACT_PACKAGE = YES
EXTRACT_STATIC = YES
AUTOLINK_SUPPORT = NO
WARN_IF_UNDOCUMENTED = NO
QUIET = YES
18 changes: 18 additions & 0 deletions doc/build.ps1
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
$ErrorActionPreference = "Stop"
pushd $(Split-Path -Path $MyInvocation.MyCommand.Definition -Parent)

# Ensure 0install is in the PATH
if (!(Get-Command 0install -ErrorAction SilentlyContinue)) {
mkdir -Force "$env:TEMP\zero-install" | Out-Null
Invoke-WebRequest "https://0install.de/files/0install.exe" -OutFile "$env:TEMP\zero-install\0install.exe"
$env:PATH = "$env:TEMP\zero-install;$env:PATH"
}

if (Test-Path ..\artifacts\Documentation) {rm -Recurse -Force ..\artifacts\Documentation}
mkdir ..\artifacts\Documentation | Out-Null

0install run --batch http://repo.roscidus.com/devel/doxygen

cp CNAME ..\artifacts\Documentation\

popd
10 changes: 10 additions & 0 deletions doc/build.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
#!/bin/bash
set -e
cd `dirname $0`

rm -rf ../artifacts/Documentation
mkdir -p ../artifacts/Documentation

0install run http://repo.roscidus.com/devel/doxygen

cp CNAME ../artifacts/Documentation/
Loading

0 comments on commit 567cea2

Please sign in to comment.