# BSSolver

BSSolver (Bottler Sat Solver) es un sistema que resuelve múltiples fórmulas proposicionales en CNF
de forma distribuida. 

## Table de contenidos
* [Requisitos](#requisitos)
* [Compilación](#compilación)
* [Ejecución](#ejecución)
* [Testeos](#tests)

## Requisitos <a name="requisitos"></a>

Debe instalar minisat. Este se encuentra disponible en el repositorio de la vasta mayoría de distribuciones de Linux/macOS.

Debian/Ubuntu: `apt install minisat`\
macOS (con [homebrew](https://brew.sh/)): `brew install minisat`

Si tiene otra distribución consulte cómo hacerlo. De todos modos, puede construirlo desde la [fuente](https://github.com/niklasso/minisat).

## Compilación <a name="compilación"></a>

Para compilar todos los archivos se debe hacer:

```bash
make all
```

## Ejecución <a name="ejecución"></a>

Ahora, tendrá dos ejecutables: `view` y `solve`.

Para ejecutar el programa que se encarga de resolver usted debe pasarle los archivos CNF como parámetros.

```bash
./solve $(CNF_FILES)
```
Este enviará por salida estándar la cantidad de archivos a resolver y su PID, los cuales son necesarios para el programa `view`. Por lo tanto, usted tiene dos posibles modos de uso del sistema:

1) Enviar el output de `solve` directamente a `view` (con el uso de pipes):

```bash
./solve $(CNF_FILES) | ./view
```

2) Correr primero `solve` y luego en otra terminal (o en la misma si se corrió en background) ejecutar `view` pasándole como argumentos la cantidad de archivos y el PID.

```bash
./solve $(CNF_FILES)
```
```bash
./view $(TOTAL_FILES) $(PID)
```

3) No correr el proceso `view`.

Debe notar que en todos los casos se escribirá el output un archivo llamado `ouputFile.txt`. 

Además, dispondrá de 5 segundos para correr el programa `view`.

## Testeos <a name="tests"></a>

En orden de realizar un análisis estático del sistema usted debe tener instalado [cppcheck](http://cppcheck.net/) y [pvs-studio](https://pvs-studio.com/). Luego, puede correrlos con:

```bash
make test
```

Por último, si quiere hacer un análisis dinámico (usando [valgrind](https://valgrind.org/)) debe ejecutar el programa `valAnalysis.sh` pasandole como argumento la carpeta con los archivos `.cnf` o directamente los archivos:

```bash
./valAnalysis.sh $(CNF_FILES)
```

# Autores
- Barmasch, Juan Martín (61033)
- Bellver, Ezequiel (61268)
- Lo Coco, Santiago (61301)