Add onestep test utility

GMLMIP-0.1/makefile

@@ -8,7 +8,7 @@ SUBDIRS = parser formulas rules
 
 .PHONY: all clean parser formulas rules
 
-all: main
+all: main onestep
 
 parser:
 	make -C parser
@@ -22,9 +22,16 @@ rules:
 main: main.o $(POBJS) $(FOBJS) $(ROBJS)
 	$(GCC) $(GCCFLAGS) $(POBJS) $(FOBJS) $(ROBJS) -lbdd -lm -lglpk $< -o $@
 
+onestep: onestep.o $(POBJS) $(FOBJS) $(ROBJS)
+	$(GCC) $(GCCFLAGS) $(POBJS) $(FOBJS) $(ROBJS) -lbdd -lm -lglpk $< -o $@
+
+
 main.o: main.cpp ./parser/mlf-driver.h ./formulas/formula.h ./formulas/satisfyingassignment.h $(SUBDIRS)
 	$(GCC) $(GCCFLAGS) -c $< -o $@
 
+onestep.o: onestep.cpp ./parser/mlf-driver.h ./formulas/formula.h ./formulas/satisfyingassignment.h $(SUBDIRS)
+	$(GCC) $(GCCFLAGS) -c $<
+
 clean:
 	rm -rf *.o main
 	make -C parser clean

GMLMIP-0.1/onestep.cpp

+#include <iostream>
+#include <vector>
+#include <time.h>
+
+#include "./parser/mlf-driver.h"
+#include "./formulas/formula.h"
+#include "./formulas/satisfyingassignment.h"
+#include "satisfyingstack.h"
+
+#include "bdd.h"
+
+using namespace std;
+
+vector<SatisfyingAssignment> sat_ass_stack;
+
+/* Error handler for running out of BDD nodes */
+void error_handler(int errorcode){
+	if(errorcode==BDD_VAR)
+		bdd_extvarnum(1000);
+	else
+		cout << "BDD package error number " << errorcode << endl;
+}
+
+void parse(IFormula* &formula, int argc, char *argv[], int& verbose);
+
+int main (int argc, char *argv[]){
+	clock_t total_time = clock();
+	IFormula* f = NULL;
+	int verbose = 0;
+	//initalize buddy
+	bdd_init(100000, 10000);
+	bdd_setvarnum(100); // Minimum is two.
+	bdd_error_hook(error_handler);
+	parse(f, argc, argv, verbose);
+	if(f){
+		// bdd_varblockall();
+		// bdd_reorder(BDD_REORDER_WIN3ITE);
+		// bdd_printdot((driver.formula)->bdd_rep);
+		//bdd_printset(f->get_bdd());
+		//cout << endl;
+		//(driver.formula)->print_back_vars();
+		if(f->satisfiability(verbose))
+			cout << "Satisfiable" << endl;
+		else
+			cout << "Unsatisfiable" << endl;
+		f->clear_maps();
+		delete f;
+	}
+	bdd_done();
+	total_time = clock() - total_time;
+	cout << "Total Time: " << static_cast<float>(total_time) / CLOCKS_PER_SEC << endl;
+	return 0;
+}
+
+void parse(IFormula* &formula, int argc, char *argv[], int& option){
+	mlf_driver driver;
+	for (++argv; argv[0]; ++argv)
+		if (*argv == std::string ("-p"))
+			driver.trace_parsing = true;
+		else if (*argv == std::string ("-v"))
+			option = 1;
+		else if (*argv == std::string ("-t"))
+			option = 2;
+		else if (*argv == std::string ("-s"))
+			driver.trace_scanning = true;
+		else if (!driver.parse (*argv))
+			driver.extract_formula(formula);
+}
+