La aplicación de resolución de problemas SAT consiste en los siguientes archivos:
- master: crea los esclavos y envía los datos procesados a vision y mostrados results.txt.
- vision: imprime los datos por standard output.
- slave: realiza el procesamiento utilizando minisat.
- shm_lib y sem_lib: librerías para el manejo de semáforos y memoria compartida.
Ejecutar make o make all para el compilado de los archivos. Asegurarse de tener instalado minisat con apt-get install minisat en su contenedor de docker.
Luego de la ejecución se generarán los siguientes archivos:
- Master
- Vision
- Slave
Si desea remover los mismos, ejecute make clean en el mismo directorio donde fue realizada la compilación.
Para correr el programa ejecutar el archivo Master corriendo ./Master junto a una lista de archivos .cnf pasados como parámetros.
Por ejemplo:
./Master files/*Para ejecutar Vision hay dos formas:
- Pipe de lo enviado por Master
./Master files/* | ./Vision- Corriendo Master en una terminal y Vision en otra, pasando el valor retornado de Master.
# Terminal 1:
./Master
3# Terminal 2:
./Vision 3- Correr Master en background y Vision en foreground pasando el valor de retorno de Master.
./Master files/*& # background
./Vision 3 # foregroundAl finalizar la ejecución de Master se creará un archivo llamado results.txt, con la resolución de los SAT y por standard output será mostrado gracias a Vision.
Para el testeo con tanto PVS-Studio, Cppcheck como Valgrind se debe primero instalar PVS-Studio de no tenerlo, de la siguiente manera en su contenedor de docker.
apt-get update
apt-get install pvs-studio
pvs-studio-analyzer credentials "PVS-Studio Free" "FREE-FREE-FREE-FREE"Luego correr el siguiente comando:
make testLos resultados se encontrarán de la siguiente manera:
- PVS-Studio: report.tasks
- Valgrind: vision.valgrind, master.valgrind
- Cppcheck: cppoutput.txt
Para remover los mismos, correr el comando make cleanTest en el mismo directorio donde fue realizada la compilación.