diff --git a/GMLMIP-0.1/formulas/formula.cpp b/GMLMIP-0.1/formulas/formula.cpp
index a0fe3b663100c28ddda35aa2a9803b56c204037f..26c3f0f5ee7535705a1f76e22366183f6a06b12b 100644
--- a/GMLMIP-0.1/formulas/formula.cpp
+++ b/GMLMIP-0.1/formulas/formula.cpp
@@ -50,17 +50,42 @@ void sat_handler(char *varset, int size){
sat_ass_stack.push_back(s);
}
+template<class ModalValueType>
+vector<SatisfyingAssignment> Formula<ModalValueType>::onestep() {
+ rulechildren.clear();
+ bool backup_rek = recursive_satisfiability_check;
+ recursive_satisfiability_check = false;
+ check_satisfiability(bdd_rep);
+ recursive_satisfiability_check = backup_rek;
+ vector<SatisfyingAssignment> ret = rulechildren;
+ rulechildren.clear();
+ return ret;
+}
+
template<class ModalValueType>
bool Formula<ModalValueType>::check_satisfiability(bdd b){
- bool sat = false; // handle the case of no satisfying assignments.
- //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]);
+ 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());
+ sat_ass_stack.clear();
+ return false; // simulate unsatisfiability to get all assignments
+ } else {
+ modality_depth++;
+ bool sat = false; // handle the case of no satisfying assignments.
+ //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]);
+ }
+ modality_depth--;
+ return sat;
}
- return sat;
}
template<class ModalValueType>
diff --git a/GMLMIP-0.1/formulas/formula.h b/GMLMIP-0.1/formulas/formula.h
index e4ece7c5cafc2456d91a8516d62860fde0752474..bdea56da4a800687ce4897da20aef5f0689a9aca 100644
--- a/GMLMIP-0.1/formulas/formula.h
+++ b/GMLMIP-0.1/formulas/formula.h
@@ -32,8 +32,6 @@ using std::vector;
using google::dense_hash_map;
using __gnu_cxx::hash;
-typedef vector<vector<pair<bool,int> > > RuleChild;
-
// Formula interface so we can have abstract template class pointers.
class IFormula {
public:
@@ -42,9 +40,11 @@ class IFormula {
virtual bdd get_bdd()=0;
virtual bdd modal(bdd *b, int n, int m)=0;
virtual bool satisfiability(int option)=0;
+ virtual vector<SatisfyingAssignment> onestep() = 0;
virtual void clear_maps()=0;
virtual ~IFormula() { };
- virtual vector<RuleChild> onestep_rules(bdd b) = 0;
+ virtual int variable_back(int v) = 0;
+ virtual bool has_variable_back(int v) = 0;
};
template<class ModalValueType>
@@ -131,12 +131,11 @@ class Formula : public IFormula{
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);
bool run_solver(glp_prob *problem, glp_iocp* parameters, bool strict, vector<bool> current_node, int index);
- vector<RuleChild> onestep_rules(bdd b);
- vector<RuleChild> apply_rule_non_rec(SatisfyingAssignment& sat);
virtual void load_linear_program(glp_prob* problem, Premise<ModalValueType>& prem)=0;
bool recursive_satisfiability_check; // whether rule enumerationis should call check_satisfiability()
int modality_depth; // nesting depth of satisfiability()
+ vector<SatisfyingAssignment> rulechildren;
public:
Formula();
@@ -151,11 +150,14 @@ class Formula : public IFormula{
// Also constructs appropriate data structures.
bdd variable(int n);
bdd modal_var(bdd *b, ModalValueType &n);
+ int variable_back(int v) { return variables_back[v]; }
+ bool has_variable_back(int v) { return variables_back.count(v); }
void print_back_vars();
//virtual void print_back_modal()=0;
bool satisfiability(int option){ return check_satisfiability(bdd_rep); };
+ vector<SatisfyingAssignment> onestep();
void clear_maps(){
variables.clear();
diff --git a/GMLMIP-0.1/onestep.cpp b/GMLMIP-0.1/onestep.cpp
index a059b249e6588bd9d92d8445d4f1b51e5241338a..b01b1f741750f88229c8324cab1957ce1edc2145 100644
--- a/GMLMIP-0.1/onestep.cpp
+++ b/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_and(f->modal(new bdd(f->variable(0)), 4, 0),
- bdd_not(f->modal(new bdd(f->variable(0)), 3, 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)));
f->set_bdd(b);
// bdd_varblockall();
// bdd_reorder(BDD_REORDER_WIN3ITE);
@@ -58,10 +58,20 @@ int main (int argc, char *argv[]){
// }
// cout << endl;
//}
- if(f->satisfiability(0))
- cout << "Satisfiable" << endl;
- else
- cout << "Unsatisfiable" << 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->clear_maps();
delete f;
bdd_done();