TIEMPO = 3
VERIFICADOR = verificador.cpp
include ../../../lab.mk

# solution.cpp incluye driver.h, que está en esta carpeta.
CXXFLAGS += -I.
$(BUILD)/solution: driver.h

# Para mirar cada mitad por separado, con un caso:
#   make formula CASO=01    escribe build/01.cnf
#   make respuesta CASO=01  corre minisat con esa fórmula y escribe build/01.res
#   make decode CASO=01     llama a decode con esa respuesta
CASO ?= 01
.PHONY: formula respuesta decode

formula: $(BUILD)/solution
	$(BUILD)/solution --encode < casos/$(CASO).in > $(BUILD)/$(CASO).cnf
	@head -n 1 $(BUILD)/$(CASO).cnf

# minisat termina con 10 o 20 aunque todo haya salido bien, y make lo tomaría como un error.
respuesta: formula
	@minisat -verb=0 $(BUILD)/$(CASO).cnf $(BUILD)/$(CASO).res > /dev/null 2>&1; echo "minisat terminó con el código $$?"
	@head -c 100 $(BUILD)/$(CASO).res; echo

decode: respuesta
	$(BUILD)/solution --decode casos/$(CASO).in $(BUILD)/$(CASO).res