diff --git a/CoAlgLogics.ml b/CoAlgLogics.ml
index 3a088a5c5bfcc862dd4a96da6e55451f648444ff..3ae37bbc178976d01a26f672e342e7add1e6ec14 100644
--- a/CoAlgLogics.ml
+++ b/CoAlgLogics.ml
@@ -270,6 +270,13 @@ let mkRule_GML sort bs sl =
let s1 = List.hd sl in (* [s1] = List.hd sl *)
let boxes = bsetFilter bs (fun f -> lfGetType sort f = MoreThanF) in
let diamonds = bsetFilter bs (fun f -> lfGetType sort f = MaxExceptF) in
+ (*
+ mkRule_GML sort bs [s1]
+ = { (λ[bs1]. bs, [(s1, { a_i | i∈I })])
+ | {[C_i]a_i | i∈I} ⊆ bs,
+ C_i pairwise disjoint and I maximal
+ }
+ *)
mkRule_MultiModalK sort bs sl
let mkRule_Choice sort bs sl =
diff --git a/GMLMIP-0.1/formulas/formula.cpp b/GMLMIP-0.1/formulas/formula.cpp
index d1e3428dbeeb07a59d1834d069e26446ad08bd76..a0fe3b663100c28ddda35aa2a9803b56c204037f 100644
--- a/GMLMIP-0.1/formulas/formula.cpp
+++ b/GMLMIP-0.1/formulas/formula.cpp
@@ -3,6 +3,7 @@
template<class ModalValueType>
Formula<ModalValueType>::Formula(){
recursive_satisfiability_check = true;
+ modality_depth = 0;
number_of_variables = 0;
variables.set_empty_key(-1); //
variables_back.set_empty_key(-1); //
@@ -62,76 +63,6 @@ bool Formula<ModalValueType>::check_satisfiability(bdd b){
return sat;
}
-template<class ModalValueType>
-vector<RuleChild> Formula<ModalValueType>::onestep_rules(bdd b){
- bool sat = false; // handle the case of no satisfying assignments.
- recursive_satisfiability_check = false;
- //bdd_printdot(b);
- bdd_allsat(b, sat_handler); // pushes satisfying assignment onto stack
- vector<SatisfyingAssignment> sat_ass = sat_ass_stack;
- sat_ass_stack.clear();
- vector<RuleChild> res;
- for(unsigned int i=0; i < sat_ass.size() && !sat; i++){ // we break if proved sat
- vector<RuleChild> hunk = apply_rule_non_rec(sat_ass[i]);
- res.insert(res.end(), hunk.begin(), hunk.end());
- }
- return res;
-}
-
-// apply rules without recursion, just remove created formulas
-template<class ModalValueType>
-vector<RuleChild> Formula<ModalValueType>::apply_rule_non_rec(SatisfyingAssignment& sat){
- vector<RuleChild> results;
-
- int no_of_positive = 0;
- int no_of_negative = 0;
- ModalValueType *positive_modal_indices, *negative_modal_indices;
-
- // We first find the size of the required arrays.
- for(int v=0; v < sat.get_size(); v++){
- if(sat.get_array_i(v)==1 && modal_variables_back.count(v)) // if true and represents a modal formula.
- no_of_positive++;
- else if(sat.get_array_i(v)==0 && modal_variables_back.count(v)) // if false and ...
- no_of_negative++;
- }
- // cout << no_of_positive + no_of_negative << endl;
- if(no_of_positive + no_of_negative > 0){
-
- positive_modal_indices = new ModalValueType[no_of_positive];
- negative_modal_indices = new ModalValueType[no_of_negative];
-
- // We then fill our underlying formulae and modal value arrays.
- int i=0, j=0;
- for(int v=0; v < sat.get_size(); v++){
- if(sat.get_array_i(v)==1 && modal_variables_back.count(v)){
- positive_modal_indices[i] = (modal_variables_back[v]).value;
- i++;
- }
- else if(sat.get_array_i(v)==0 && modal_variables_back.count(v)){ //if false and represents a modal formula.
- negative_modal_indices[j] = (modal_variables_back[v]).value;
- j++;
- }
- }
-
- // Construct a GML premise
- Premise<ModalValueType> premise(no_of_positive, no_of_negative, positive_modal_indices, negative_modal_indices);
- // Check the rule cache
- if(!rule_cache.count(premise)){ // if in cache
- enumerate_rules(premise, NULL);
- }
- SetOfConclusions concs = rule_cache[premise];
- for(int i = 0; i < concs.number_of_conclusions(); i++){
- RuleChild con = concs.get_jth_conclusion(i);
- results.push_back(con);
- }
-
- delete [] positive_modal_indices;
- delete [] negative_modal_indices;
- }
-
- return results;
-}
-
template<class ModalValueType>
bool Formula<ModalValueType>::apply_rules(SatisfyingAssignment& sat){
bool result = true;
@@ -179,9 +110,7 @@ bool Formula<ModalValueType>::apply_rules(SatisfyingAssignment& sat){
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);
- if (recursive_satisfiability_check) {
- result = check_satisfiability(b);
- }
+ result = check_satisfiability(b);
}
} else {
result = enumerate_rules(premise, underlying_formulae);
@@ -291,13 +220,11 @@ bool Formula<ModalValueType>::enum_rules_intern(glp_prob* problem, glp_iocp* par
//cout << "solution found " << valid_nodes.size() << endl;
//for (int l = 0; l < total_valuations; l++)
// cout << " " << new_node[l] << endl;
- if (recursive_satisfiability_check) {
- 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);
- }
+ 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);
} 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 dd0f64d58966805118a2f0d427e2952a99fa7618..e4ece7c5cafc2456d91a8516d62860fde0752474 100644
--- a/GMLMIP-0.1/formulas/formula.h
+++ b/GMLMIP-0.1/formulas/formula.h
@@ -136,6 +136,7 @@ class Formula : public IFormula{
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()
public:
Formula();
diff --git a/GMLMIP-0.1/onestep.cpp b/GMLMIP-0.1/onestep.cpp
index 0ae0dad7a8b02606bfbfab92a110bb0828ec4433..a059b249e6588bd9d92d8445d4f1b51e5241338a 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)), 3, 0),
- bdd_not(f->modal(new bdd(f->variable(0)), 2, 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)));
f->set_bdd(b);
// bdd_varblockall();
// bdd_reorder(BDD_REORDER_WIN3ITE);
@@ -42,26 +42,26 @@ int main (int argc, char *argv[]){
//bdd_printset(f->get_bdd());
//cout << endl;
//(driver.formula)->print_back_vars();
- vector<RuleChild> res = f->onestep_rules(b);
- cout << res.size() << " childs" << endl;
- for (unsigned int r = 0; r < res.size(); r++) {
- RuleChild& rc = res[r];
- for (unsigned int i = 0; i < rc.size(); i++) {
- cout << "\\/ (";
- for (unsigned int j = 0; j < rc[i].size(); j++) {
- pair<bool,int>& p = rc[i][j];
- if (j != 0) cout << ", ";
- if (!p.first) cout << "~";
- cout << p.second;
- }
- cout << ")";
- }
- cout << endl;
- }
- //if(f->satisfiability(verbose))
- // cout << "Satisfiable" << endl;
- //else
- // cout << "Unsatisfiable" << endl;
+ //vector<RuleChild> res = f->onestep_rules(b);
+ //cout << res.size() << " childs" << endl;
+ //for (unsigned int r = 0; r < res.size(); r++) {
+ // RuleChild& rc = res[r];
+ // for (unsigned int i = 0; i < rc.size(); i++) {
+ // cout << "\\/ (";
+ // for (unsigned int j = 0; j < rc[i].size(); j++) {
+ // pair<bool,int>& p = rc[i][j];
+ // if (j != 0) cout << ", ";
+ // if (!p.first) cout << "~";
+ // cout << p.second;
+ // }
+ // cout << ")";
+ // }
+ // cout << endl;
+ //}
+ if(f->satisfiability(0))
+ cout << "Satisfiable" << endl;
+ else
+ cout << "Unsatisfiable" << endl;
f->clear_maps();
delete f;
bdd_done();