Make onestep-example more flexible

GMLMIP-0.1/onestep-example.cpp

@@ -9,6 +9,7 @@
 #include "./formulas/rational.h"
 #include "./formulas/satisfyingassignment.h"
 #include "satisfyingstack.h"
+#include "./parser/mlf-driver.h"
 
 using namespace std;
 
@@ -29,14 +30,22 @@ int main (int argc, char *argv[]){
 	bdd_init(100000, 10000);
 	bdd_setvarnum(100); // Minimum is two.
 	bdd_error_hook(error_handler);
-	f = new GML_Formula;
     // this turns into an endless loop
 	//bdd b = bdd_and(f->modal(new bdd(f->variable(0)), 4, 0),
 	//                bdd_not(f->modal(new bdd(f->variable(0)), 6, 0)));
-	bdd b = bdd_and(bdd_and(f->modal(new bdd(f->variable(8)), 4, 0),
-	               bdd_not(f->modal(new bdd(bdd_not(f->variable(7))), 3, 0))),
-                   bdd_not(f->modal(new bdd(bdd_not(f->variable(9))), 3, 0)));
-	f->set_bdd(b);
+	if (true) {
+		mlf_driver driver;
+		driver.set_formula_gml();
+		if (!driver.parse ("-")) {
+			driver.extract_formula(f);
+		}
+	} else {
+		f = new GML_Formula;
+		bdd b = bdd_and(bdd_and(f->modal(new bdd(f->variable(8)), 4, 0),
+					   bdd_not(f->modal(new bdd(bdd_not(f->variable(7))), 3, 0))),
+					   bdd_not(f->modal(new bdd(bdd_not(f->variable(9))), 3, 0)));
+		f->set_bdd(b);
+	}
 	// bdd_varblockall();
 	// bdd_reorder(BDD_REORDER_WIN3ITE);
 	// bdd_printdot((driver.formula)->bdd_rep);
@@ -59,23 +68,25 @@ int main (int argc, char *argv[]){
 	//	}
 	//	cout << endl;
 	//}
-	vector<SatisfyingAssignment> vsa = f->onestep();
-	cout << vsa.size() << " possible assignments\n";
-	for (unsigned int i = 0; i < vsa.size(); i++) {
-		SatisfyingAssignment& sat = vsa[i];
-		cout << i << ")";
-		for (int v=0; v < sat.get_size(); v++) {
-			if (sat.get_array_i(v)==1 && f->has_variable_back(v)) {
-				cout << " p" << f->variable_back(v) << "=1,";
-			} else if (sat.get_array_i(v)==0 && f->has_variable_back(v)) {
-				cout << " p" << f->variable_back(v) << "=0,";
+	if (f) {
+		vector<SatisfyingAssignment> vsa = f->onestep();
+		cout << vsa.size() << " possible assignments\n";
+		for (unsigned int i = 0; i < vsa.size(); i++) {
+			SatisfyingAssignment& sat = vsa[i];
+			cout << i << ")";
+			for (int v=0; v < sat.get_size(); v++) {
+				if (sat.get_array_i(v)==1 && f->has_variable_back(v)) {
+					cout << " p" << f->variable_back(v) << "=1,";
+				} else if (sat.get_array_i(v)==0 && f->has_variable_back(v)) {
+					cout << " p" << f->variable_back(v) << "=0,";
+				}
 			}
+			cout << endl;
 		}
-		cout << endl;
+		f->clear_maps();
+		delete f;
+		bdd_done();
 	}
-	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;