Add option to enforce entire exploration

With this option, the entire level of modality depth 1 is explored and
all satisfying assignments are listed.

GMLMIP-0.1/formulas/formula.cpp

@@ -55,7 +55,7 @@ vector<SatisfyingAssignment> Formula<ModalValueType>::onestep() {
 	rulechildren.clear();
 	bool backup_rek = recursive_satisfiability_check;
 	recursive_satisfiability_check = false;
-	check_satisfiability(bdd_rep);
+	assert(false == check_satisfiability(bdd_rep));
 	recursive_satisfiability_check = backup_rek;
 	vector<SatisfyingAssignment> ret = rulechildren;
 	rulechildren.clear();
@@ -64,10 +64,8 @@ vector<SatisfyingAssignment> Formula<ModalValueType>::onestep() {
 
 template<class ModalValueType>
 bool Formula<ModalValueType>::check_satisfiability(bdd b){
-	cerr << "checksat\n";
 	if (!recursive_satisfiability_check && modality_depth >= 1) {
 		bdd_allsat(b, sat_handler); // pushes satisfying assignment onto stack
-		cerr << "another " << sat_ass_stack.size() << " elems\n";
 		rulechildren.insert(rulechildren.end(),
 		                    sat_ass_stack.begin(),
 		                    sat_ass_stack.end());
@@ -82,6 +80,7 @@ bool Formula<ModalValueType>::check_satisfiability(bdd b){
 		sat_ass_stack.clear();
 		for(unsigned int i=0; i < sat_ass.size() && !sat; i++){ // we break if proved sat
 			sat = apply_rules(sat_ass[i]);
+			if (!recursive_satisfiability_check) sat = false;
 		}
 		modality_depth--;
 		return sat;
@@ -133,7 +132,8 @@ bool Formula<ModalValueType>::apply_rules(SatisfyingAssignment& sat){
 		// Check the rule cache
 		if(rule_cache.count(premise)){ // if in cache
 			SetOfConclusions concs = rule_cache[premise];
-			for(int i = 0; i < concs.number_of_conclusions() && result; i++){
+			for(int i = 0; i < concs.number_of_conclusions() &&
+			               (!recursive_satisfiability_check || result); i++){
 				bdd b = concs.get_jth_conclusion(underlying_formulae, i);
 				result = check_satisfiability(b);
 			}
@@ -171,10 +171,10 @@ bool Formula<ModalValueType>::enumerate_rules(Premise<ModalValueType>& prem, bdd
 	
 	vector<bool> zero(total_valuations, false);
 	
-	if (run_solver(problem, parameters, false, zero, -1)) {
-		if (run_solver(problem, parameters, true, zero, 0))
+	if (run_solver(problem, parameters, false, zero, -1) || !recursive_satisfiability_check) {
+		if (run_solver(problem, parameters, true, zero, 0)) {
 			result = false;
-		else {
+		} else {
 			node_queue.push_back(zero);
 			//int i = 0;
 			while(result && node_queue.size()) {
@@ -202,13 +202,13 @@ bool Formula<ModalValueType>::enum_rules_intern(glp_prob* problem, glp_iocp* par
 	vector<vector<bool> > new_node_queue;
 	int total_valuations = prem.get_total_valuations();
 
-	for (unsigned int k = 0; k < node_queue.size() && result; k++) {
+	for (unsigned int k = 0; k < node_queue.size() && (result || !recursive_satisfiability_check); k++) {
 		vector<bool> current_node = node_queue[k];
 
 		int power = total_valuations-1;
 		while(power >= 0 && !current_node[power])
 			power--;
-		for(int i = power+1; i < total_valuations && result; i++){
+		for(int i = power+1; i < total_valuations && (result || !recursive_satisfiability_check); i++){
 			vector<bool> new_node(current_node);
 			new_node[i] = true;
 

GMLMIP-0.1/onestep.cpp

@@ -33,8 +33,8 @@ int main (int argc, char *argv[]){
     // 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_or(f->modal(new bdd(f->variable(0)), 4, 0),
-	                bdd_not(f->modal(new bdd(f->variable(1)), 3, 0)));
+	bdd b = bdd_or(f->modal(new bdd(f->variable(4)), 4, 0),
+	               bdd_not(f->modal(new bdd(f->variable(7)), 3, 0)));
 	f->set_bdd(b);
 	// bdd_varblockall();
 	// bdd_reorder(BDD_REORDER_WIN3ITE);
@@ -58,20 +58,20 @@ int main (int argc, char *argv[]){
 	//	}
 	//	cout << endl;
 	//}
-	f->satisfiability(0);
-	//vector<SatisfyingAssignment> vsa = f->onestep();
-	//cout << vsa.size() << " possible assignments\n";
-	//for (unsigned int i = 0; i < vsa.size(); i++) {
-	//	SatisfyingAssignment& sat = vsa[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;
-	//}
+	f->onestep();
+	vector<SatisfyingAssignment> vsa = f->onestep();
+	cout << vsa.size() << " possible assignments\n";
+	for (unsigned int i = 0; i < vsa.size(); i++) {
+		SatisfyingAssignment& sat = vsa[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;
+	}
 	f->clear_maps();
 	delete f;
 	bdd_done();