diff --git a/GMLMIP-0.1/formulas/formula.cpp b/GMLMIP-0.1/formulas/formula.cpp
index 0a9ef1ed30324d9b7d2717442aa57719686eb1f7..09a9e6ab22fb25e1e894799104bdf0fa8266f7bf 100644
--- a/GMLMIP-0.1/formulas/formula.cpp
+++ b/GMLMIP-0.1/formulas/formula.cpp
@@ -1,5 +1,10 @@
#include "formula.h"
+#include <set>
+
+IFormula::~IFormula() {
+}
+
template<class ModalValueType>
Formula<ModalValueType>::Formula(){
number_of_variables = 0;
@@ -49,21 +54,18 @@ void sat_handler(char *varset, int size){
}
template<class ModalValueType>
-bool Formula<ModalValueType>::check_satisfiability(bdd b){
- bool sat = false; // handle the case of no satisfying assignments.
+RuleCollection Formula<ModalValueType>::check_satisfiability(bdd b){
//bdd_printdot(b);
bdd_allsat(b, sat_handler); // pushes satisfying assignment onto stack
vector<SatisfyingAssignment> sat_ass = sat_ass_stack;
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]);
- }
- return sat;
+ assert(sat_ass.size() == 1);
+ return apply_rules(sat_ass[0]);
}
template<class ModalValueType>
-bool Formula<ModalValueType>::apply_rules(SatisfyingAssignment& sat){
- bool result = true;
+RuleCollection Formula<ModalValueType>::apply_rules(SatisfyingAssignment& sat){
+ RuleCollection result;
int no_of_positive = 0;
int no_of_negative = 0;
@@ -106,9 +108,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++){
- bdd b = concs.get_jth_conclusion(underlying_formulae, i);
- result = check_satisfiability(b);
+ for(int i = 0; i < concs.number_of_conclusions(); i++){
+ result.insert(concs.get_jth_conclusion(underlying_formulae, i));
}
} else {
result = enumerate_rules(premise, underlying_formulae);
@@ -123,8 +124,8 @@ bool Formula<ModalValueType>::apply_rules(SatisfyingAssignment& sat){
}
template<class ModalValueType>
-bool Formula<ModalValueType>::enumerate_rules(Premise<ModalValueType>& prem, bdd** underlying_formulae){
- bool result = true;
+RuleCollection Formula<ModalValueType>::enumerate_rules(Premise<ModalValueType>& prem, bdd** underlying_formulae){
+ RuleCollection result;
vector<vector<bool> > valid_nodes;
vector<pair<vector<bool>, int> > anti_nodes;
vector<vector<bool> > node_queue;
@@ -145,16 +146,15 @@ 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))
- result = false;
- else {
+ if (run_solver(problem, parameters, true, zero, 0)) {
+ } else {
node_queue.push_back(zero);
//int i = 0;
- while(result && node_queue.size()) {
+ while(node_queue.size()) {
//cout << "outer space: " << i++ << " runs: " << test_counter << " queue: " << node_queue.size() << " sols: " << valid_nodes.size() << " antisols: " << anti_nodes.size() << endl;
result = enum_rules_intern(problem, parameters, prem, underlying_formulae, node_queue, valid_nodes, anti_nodes);
}
- if (result && !rule_cache.count(prem)) {
+ if (!rule_cache.count(prem)) {
rule_cache[prem] = SetOfConclusions(prem.get_n() + prem.get_m(), valid_nodes);
}
//cout << "runs: " << test_counter << " sols: " << valid_nodes.size() << " antisols: " << anti_nodes.size() << endl;
@@ -169,19 +169,19 @@ bool Formula<ModalValueType>::enumerate_rules(Premise<ModalValueType>& prem, bdd
}
template<class ModalValueType>
-bool Formula<ModalValueType>::enum_rules_intern(glp_prob* problem, glp_iocp* parameters, Premise<ModalValueType>& prem, bdd** underlying_formulae,
+RuleCollection Formula<ModalValueType>::enum_rules_intern(glp_prob* problem, glp_iocp* parameters, Premise<ModalValueType>& prem, bdd** underlying_formulae,
vector<vector<bool> >& node_queue, vector<vector<bool> >& valid_nodes, vector<pair<vector<bool>, int> >& anti_nodes){
- bool result = true;
+ RuleCollection result;
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(); 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; i++){
vector<bool> new_node(current_node);
new_node[i] = true;
@@ -221,8 +221,7 @@ bool Formula<ModalValueType>::enum_rules_intern(glp_prob* problem, glp_iocp* par
vector<vector<bool> > singleton;
singleton.push_back(new_node);
SetOfConclusions temp = SetOfConclusions(prem.get_n() + prem.get_m(), singleton);
- bdd b = temp.get_jth_conclusion(underlying_formulae, 0);
- result = check_satisfiability(b);
+ result.insert(temp.get_jth_conclusion(underlying_formulae, 0));
} else {
new_node_queue.push_back(new_node);
}
diff --git a/GMLMIP-0.1/formulas/formula.h b/GMLMIP-0.1/formulas/formula.h
index a5931d1497c1b2cfd0d3b7f08c9eeed1ef80933d..6226bbf1804d684a6f32f02626afbf37c48c8384 100644
--- a/GMLMIP-0.1/formulas/formula.h
+++ b/GMLMIP-0.1/formulas/formula.h
@@ -7,6 +7,7 @@
#include <iomanip>
#include <sstream>
#include <string>
+#include <set>
#include <time.h>
#include "bdd.h"
@@ -32,15 +33,19 @@ using std::vector;
using google::dense_hash_map;
using __gnu_cxx::hash;
+typedef set<set<set<int> > > RuleCollection;
+
// Formula interface so we can have abstract template class pointers.
class IFormula {
public:
+ virtual ~IFormula();
virtual bdd variable(int n)=0;
virtual void set_bdd(bdd &b)=0;
virtual bdd get_bdd()=0;
virtual bdd modal(bdd *b, int n, int m)=0;
virtual bool satisfiability(int option)=0;
virtual void clear_maps()=0;
+ virtual RuleCollection onestep() = 0;
};
template<class ModalValueType>
@@ -122,10 +127,10 @@ class Formula : public IFormula{
int test_counter;
- bool check_satisfiability(bdd b);
- bool apply_rules(SatisfyingAssignment& sat);
- bool enumerate_rules(Premise<ModalValueType>& prem, bdd** underlying_formulae);
- bool enum_rules_intern(glp_prob* problem, glp_iocp* parameters, Premise<ModalValueType>& prem, bdd** underlying_formulae, vector<vector<bool> >& node_queue, vector<vector<bool> >& valid_nodes, vector<pair<vector<bool>, int> >& anti_nodes);
+ RuleCollection check_satisfiability(bdd b);
+ RuleCollection apply_rules(SatisfyingAssignment& sat);
+ RuleCollection enumerate_rules(Premise<ModalValueType>& prem, bdd** underlying_formulae);
+ RuleCollection enum_rules_intern(glp_prob* problem, glp_iocp* parameters, Premise<ModalValueType>& prem, bdd** underlying_formulae, vector<vector<bool> >& node_queue, vector<vector<bool> >& valid_nodes, vector<pair<vector<bool>, int> >& anti_nodes);
bool run_solver(glp_prob *problem, glp_iocp* parameters, bool strict, vector<bool> current_node, int index);
virtual void load_linear_program(glp_prob* problem, Premise<ModalValueType>& prem)=0;
@@ -147,7 +152,8 @@ class Formula : public IFormula{
void print_back_vars();
//virtual void print_back_modal()=0;
- bool satisfiability(int option){ return check_satisfiability(bdd_rep); };
+ bool satisfiability(int option){ assert(0=="patched GMLMIP\n"); return true;};
+ RuleCollection onestep() { return check_satisfiability(bdd_rep); };
void clear_maps(){
variables.clear();
diff --git a/GMLMIP-0.1/main.cpp b/GMLMIP-0.1/main.cpp
index c4a5098ca02f274407898f43bd284751c0e771af..219c05539b0d7d21a9673edf774a5681242bdeb7 100644
--- a/GMLMIP-0.1/main.cpp
+++ b/GMLMIP-0.1/main.cpp
@@ -39,10 +39,11 @@ int main (int argc, char *argv[]){
//bdd_printset(f->get_bdd());
//cout << endl;
//(driver.formula)->print_back_vars();
- if(f->satisfiability(verbose))
- cout << "Satisfiable" << endl;
- else
- cout << "Unsatisfiable" << endl;
+ fprintf(stderr,"Cannot check satisfiability due to patched GMLMIP\n");
+ //if(f->satisfiability(verbose))
+ // cout << "Satisfiable" << endl;
+ //else
+ // cout << "Unsatisfiable" << endl;
f->clear_maps();
delete f;
}
diff --git a/GMLMIP-0.1/onestep-example.cpp b/GMLMIP-0.1/onestep-example.cpp
index d0503f1df41f595cc0d9e6c4f06f68944df03cde..a6ab821e0992537e081b4f433d35a52d9f77d038 100644
--- a/GMLMIP-0.1/onestep-example.cpp
+++ b/GMLMIP-0.1/onestep-example.cpp
@@ -69,19 +69,26 @@ int main (int argc, char *argv[]){
// cout << endl;
//}
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,";
+ RuleCollection vsa = f->onestep();
+ cout << vsa.size() << " rules\n";
+ for (RuleCollection::iterator it = vsa.begin(); it != vsa.end(); ++it) {
+ const set<set<int> > &r = *it;
+ cout << "\\/(";
+ for (set<set<int> >::iterator jt = r.begin(); jt != r.end(); ++jt) {
+ const set<int>& clause = *jt;
+ cout << " /\\(";
+ for (set<int>::iterator kt = clause.begin(); kt != clause.end(); ++kt) {
+ int v = *kt;
+ if (v > 0) {
+ cout << " p" << v;
+ } else {
+ cout << " ¬p" << v;
+ }
}
+ cout << " )";
}
- cout << endl;
+ cout << " )";
+ cout << endl << endl;
}
f->clear_maps();
delete f;
diff --git a/GMLMIP-0.1/onestep.cpp b/GMLMIP-0.1/onestep.cpp
index 0df8e83ef39648d694247300b99d572f2b4ee747..a61f8cb8f6106fc3283e1db9d3df937bd58844b9 100644
--- a/GMLMIP-0.1/onestep.cpp
+++ b/GMLMIP-0.1/onestep.cpp
@@ -53,9 +53,10 @@ static bdd tupleModality2Bdd(IFormula* f, const pair<pair<bool,int>,int>& t) {
GMLConclusion gmlmip_onestep_gml(GMLPremise modvec) {
IFormula* f = NULL;
- vector<vector<pair<int,bool> > > rulevec;
if (modvec.size() <= 0) {
// Nothing to do -> no rules
+ GMLConclusion rulevec;
+ return rulevec;
} else {
f = new GML_Formula;
bdd b = tupleModality2Bdd(f, modvec[0]);
@@ -63,20 +64,9 @@ GMLConclusion gmlmip_onestep_gml(GMLPremise modvec) {
b = bdd_and(b, tupleModality2Bdd(f, modvec[i]));
}
f->set_bdd(b);
- vector<SatisfyingAssignment> vsa = f->onestep();
- for (unsigned int i = 0; i < vsa.size(); i++) {
- SatisfyingAssignment& sat = vsa[i];
- vector<pair<int,bool> > rule;
- for (int v=0; v < sat.get_size(); v++) {
- if (f->has_variable_back(v)) {
- bool val = sat.get_array_i(v) == 1;
- rule.push_back(make_pair(v, val));
- }
- }
- rulevec.push_back(rule);
- }
+ RuleCollection vsa = f->onestep();
f->clear_maps();
delete f;
+ return vsa;
}
- return rulevec;
}
diff --git a/GMLMIP-0.1/onestep.h b/GMLMIP-0.1/onestep.h
index e6c43be34483dc0457c089ce900e6be81dcfb320..233f52c03c4c8af7ccf9b2c98fd71af266102d3c 100644
--- a/GMLMIP-0.1/onestep.h
+++ b/GMLMIP-0.1/onestep.h
@@ -2,6 +2,7 @@
#define __GMLMIP_ONESTEP_H_
#include <vector>
+#include <set>
#include <utility> // for pair
@@ -11,7 +12,8 @@
given conjunct of modalities true
*/
typedef std::vector<std::pair<std::pair<bool,int>,int> > GMLPremise;
-typedef std::vector<std::vector<std::pair<int,bool> > > GMLConclusion;
+typedef std::set<std::set<std::set<int> > > GMLConclusion;
+
GMLConclusion gmlmip_onestep_gml(GMLPremise modvec);
#endif
diff --git a/GMLMIP-0.1/rules/setofconclusions.cpp b/GMLMIP-0.1/rules/setofconclusions.cpp
index d85e192ae8a90c5b66360fa12510c1488046bbbd..5969e404b9e06db3d5b6ec8f169db4cef5ee1064 100644
--- a/GMLMIP-0.1/rules/setofconclusions.cpp
+++ b/GMLMIP-0.1/rules/setofconclusions.cpp
@@ -1,4 +1,5 @@
#include "setofconclusions.h"
+#include <set>
SetOfConclusions::SetOfConclusions(int n, const vector<vector<bool> >& set){
no_of_literals=n;
@@ -17,19 +18,18 @@ SetOfConclusions::SetOfConclusions(int n, const vector<vector<bool> >& set){
}
}
-bdd SetOfConclusions::get_jth_conclusion(bdd** underlying, int j){
- bdd b = bdd_false();
+set<set<int> > SetOfConclusions::get_jth_conclusion(bdd** underlying, int j){
+ set< set<int> > disj;
for(unsigned int i=0; i < rules[j].size(); i++){
- bdd clause = bdd_true();
+ set<int> conj;
for(int k=0; k < no_of_literals; k++){
if(rules[j][i].get_p_i(k)==1)
- clause = bdd_and(clause, *(underlying[k]));
+ conj.insert(bdd_var(*(underlying[k])));
if(rules[j][i].get_p_i(k)==0)
- clause = bdd_and(clause, bdd_not(*(underlying[k])));
+ conj.insert(-bdd_var(*(underlying[k])));
}
- b = bdd_or(clause, b);
-
+ disj.insert(conj);
}
- return b;
+ return disj;
}
-
+
diff --git a/GMLMIP-0.1/rules/setofconclusions.h b/GMLMIP-0.1/rules/setofconclusions.h
index 5a7d2af65ab905a103eb9fd73876f37bbc484820..c0e11425e54e6ecac7dd5cc5de390b2efca8e4cb 100644
--- a/GMLMIP-0.1/rules/setofconclusions.h
+++ b/GMLMIP-0.1/rules/setofconclusions.h
@@ -3,6 +3,7 @@
#include <vector>
+#include <set>
#include <stdio.h>
#include <cmath>
@@ -28,7 +29,7 @@ class SetOfConclusions{
SetOfConclusions(int n, const vector<vector<bool> >& set);
int number_of_conclusions(){return rules.size();};
- bdd get_jth_conclusion(bdd** underlying, int j);
+ set<set<int> > get_jth_conclusion(bdd** underlying, int j);