First release created!

CMakeLists.txt

@@ -41,5 +41,5 @@ endif()
 add_executable(SATIVA release/SATIVA.cc)
 target_link_libraries(SATIVA SOLVER)
 
-file (COPY "inputs" DESTINATION ".")
+#file (COPY "inputs" DESTINATION ".")
 

lib/CommandLineInterface.hh

@@ -1,5 +1,6 @@
-#ifndef COMMANDLINEINTERFACE_HH
+#ifndef COMMANDLINEINTERFACE_HH 
 #define COMMANDLINEINTERFACE_HH
+#include "Reader.hh"
 #include <iostream>
 #include "Config.h"
 #include "System.hh"
@@ -15,6 +16,7 @@ namespace tabular{
 	static clock_t clk;
 	static size_t mem;
 	static struct rusage rus;
+	static float parse_time;
 	void printInit(Solver* solver){
 		cout<<"\n\n";
 		int i=0;
@@ -50,6 +52,15 @@ namespace tabular{
 		cout<<"|-----------------------------------------------|\n";
 	};
 
+	void fillFromFile(char* filename, Solver* solver){
+		std::cout<<"\n";
+		clk=clock();
+		Dimacs::fillFromFile(filename, *solver);
+		clk=clock()-clk;
+		parse_time=clk;
+		std::cout<<"Parsing time: "<<(float)parse_time/CLOCKS_PER_SEC<<" s\n";
+	};
+
 	void printLaunch(Solver* solver){
 		cout<<"|--------- Launching CDCL procedure ------------|\n";
 		clk=clock();
@@ -155,7 +166,7 @@ namespace tabular{
 		clk=clock()-clk;
 		ofstream fout;
 		fout.open ("test.csv", std::ofstream::out | std::ofstream::app);
-		fout<<solver->pName()<<","<<solver->nL()<<","<<solver->nC()<<",=("<<clk<<")/"<<CLOCKS_PER_SEC<<","<<solver->nConflict()<<","<<solver->nLearnts()<<","<<solver->nDecision()<<","<<solver->nPropagation()<<","<<solver->getDeletedClause()<<","<<((sat)?"SAT":"UNSAT");
+		fout<<solver->pName()<<","<<solver->nL()<<","<<solver->nC()<<",=("<<parse_time<<")/"<<CLOCKS_PER_SEC<<",=("<<clk<<")/"<<CLOCKS_PER_SEC<<","<<solver->nConflict()<<","<<solver->nLearnts()<<","<<solver->nDecision()<<","<<solver->nPropagation()<<","<<solver->getDeletedClause()<<","<<((sat)?"SAT":"UNSAT");
 		fout<<",";
 		fout<<system_util::memUsedPeak()<<"\n";
 		fout.close();

release/SATIVA.cc

@@ -40,7 +40,8 @@ int main(int argc, char** argv){
 }
 
 void launchOnFile(Solver* solver){
-	Dimacs::fillFromFile(options.filename, *solver);
+	tabular::fillFromFile(options.filename, solver);
+//	Dimacs::fillFromFile(options.filename, *solver);
 	tabular::printInit(solver);
 	tabular::printLaunch(solver);
 	bool res=solver->CDCL();

test/CSV.cc

@@ -20,8 +20,8 @@ int main(int argc, char** argv){
 	name+=argv[1];
 	solver.setName(name);	
 	int holes=atoi(argv[1]);
-	pigeonhole::fillWithPigeonhole(solver, holes);
-//	if(argc>1) Dimacs::fillFromFile(argv[1], solver);
+//	pigeonhole::fillWithPigeonhole(solver, holes);
+	if(argc>1) tabular::fillFromFile(argv[1], &solver);
 
 	tabular::printInit(&solver);
 	tabular::printLaunch(&solver);