diff --git a/GMLMIP-0.1/formulas/formula.cpp b/GMLMIP-0.1/formulas/formula.cpp
index 2491e553decb42ff0b6f28e7405941079873e687..d1e3428dbeeb07a59d1834d069e26446ad08bd76 100644
--- a/GMLMIP-0.1/formulas/formula.cpp
+++ b/GMLMIP-0.1/formulas/formula.cpp
@@ -2,6 +2,7 @@
template<class ModalValueType>
Formula<ModalValueType>::Formula(){
+ recursive_satisfiability_check = true;
number_of_variables = 0;
variables.set_empty_key(-1); //
variables_back.set_empty_key(-1); //
@@ -61,6 +62,76 @@ 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;
@@ -108,7 +179,9 @@ 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);
- result = check_satisfiability(b);
+ if (recursive_satisfiability_check) {
+ result = check_satisfiability(b);
+ }
}
} else {
result = enumerate_rules(premise, underlying_formulae);
@@ -218,11 +291,13 @@ 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;
- 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);
+ 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);
+ }
} 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 3cc0372321d3a7b555b46049c55f124704dfb4bf..dd0f64d58966805118a2f0d427e2952a99fa7618 100644
--- a/GMLMIP-0.1/formulas/formula.h
+++ b/GMLMIP-0.1/formulas/formula.h
@@ -32,6 +32,8 @@ 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,6 +44,7 @@ class IFormula {
virtual bool satisfiability(int option)=0;
virtual void clear_maps()=0;
virtual ~IFormula() { };
+ virtual vector<RuleChild> onestep_rules(bdd b) = 0;
};
template<class ModalValueType>
@@ -128,8 +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()
public:
Formula();
diff --git a/GMLMIP-0.1/onestep.cpp b/GMLMIP-0.1/onestep.cpp
index 005f25203f9763633e535d747ddf99c8e0ae7281..0ae0dad7a8b02606bfbfab92a110bb0828ec4433 100644
--- a/GMLMIP-0.1/onestep.cpp
+++ b/GMLMIP-0.1/onestep.cpp
@@ -2,13 +2,14 @@
#include <vector>
#include <time.h>
-#include "./parser/mlf-driver.h"
+#include "bdd.h"
#include "./formulas/formula.h"
+#include "./formulas/GML_formula.h"
+#include "./formulas/PML_formula.h"
+#include "./formulas/rational.h"
#include "./formulas/satisfyingassignment.h"
#include "satisfyingstack.h"
-#include "bdd.h"
-
using namespace std;
vector<SatisfyingAssignment> sat_ass_stack;
@@ -21,49 +22,51 @@ void error_handler(int errorcode){
cout << "BDD package error number " << errorcode << endl;
}
-void parse(IFormula* &formula, int argc, char *argv[], int& verbose);
-
int main (int argc, char *argv[]){
clock_t total_time = clock();
IFormula* f = NULL;
- int verbose = 0;
//initalize buddy
bdd_init(100000, 10000);
bdd_setvarnum(100); // Minimum is two.
bdd_error_hook(error_handler);
- parse(f, argc, argv, verbose);
- if(f){
- // bdd_varblockall();
- // bdd_reorder(BDD_REORDER_WIN3ITE);
- // bdd_printdot((driver.formula)->bdd_rep);
- //bdd_printset(f->get_bdd());
- //cout << endl;
- //(driver.formula)->print_back_vars();
- if(f->satisfiability(verbose))
- cout << "Satisfiable" << endl;
- else
- cout << "Unsatisfiable" << endl;
- f->clear_maps();
- delete f;
+ 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(f->modal(new bdd(f->variable(0)), 3, 0),
+ bdd_not(f->modal(new bdd(f->variable(0)), 2, 0)));
+ f->set_bdd(b);
+ // bdd_varblockall();
+ // bdd_reorder(BDD_REORDER_WIN3ITE);
+ // bdd_printdot((driver.formula)->bdd_rep);
+ //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;
+ 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;
}
-void parse(IFormula* &formula, int argc, char *argv[], int& option){
- mlf_driver driver;
- for (++argv; argv[0]; ++argv)
- if (*argv == std::string ("-p"))
- driver.trace_parsing = true;
- else if (*argv == std::string ("-v"))
- option = 1;
- else if (*argv == std::string ("-t"))
- option = 2;
- else if (*argv == std::string ("-s"))
- driver.trace_scanning = true;
- else if (!driver.parse (*argv))
- driver.extract_formula(formula);
-}
-
diff --git a/GMLMIP-0.1/rules/setofconclusions.cpp b/GMLMIP-0.1/rules/setofconclusions.cpp
index d85e192ae8a90c5b66360fa12510c1488046bbbd..c4a54729b90f7b3b7068ef7c626ade3c9fb3be1b 100644
--- a/GMLMIP-0.1/rules/setofconclusions.cpp
+++ b/GMLMIP-0.1/rules/setofconclusions.cpp
@@ -28,8 +28,20 @@ bdd SetOfConclusions::get_jth_conclusion(bdd** underlying, int j){
clause = bdd_and(clause, bdd_not(*(underlying[k])));
}
b = bdd_or(clause, b);
-
}
return b;
}
-
+vector<vector<pair<bool,int> > > SetOfConclusions::get_jth_conclusion(int j) {
+ vector<vector<pair<bool,int> > > b;
+ for(unsigned int i=0; i < rules[j].size(); i++){
+ vector<pair<bool,int> > clause;
+ for(int k=0; k < no_of_literals; k++){
+ if(rules[j][i].get_p_i(k)==1)
+ clause.push_back(make_pair(true, k));
+ if(rules[j][i].get_p_i(k)==0)
+ clause.push_back(make_pair(false, k));
+ }
+ b.push_back(clause);
+ }
+ return b;
+}
diff --git a/GMLMIP-0.1/rules/setofconclusions.h b/GMLMIP-0.1/rules/setofconclusions.h
index 5a7d2af65ab905a103eb9fd73876f37bbc484820..5429fe678f0845a16d44ac013f4a65121e5a4029 100644
--- a/GMLMIP-0.1/rules/setofconclusions.h
+++ b/GMLMIP-0.1/rules/setofconclusions.h
@@ -27,8 +27,9 @@ class SetOfConclusions{
SetOfConclusions(){no_of_literals = 0;};
SetOfConclusions(int n, const vector<vector<bool> >& set);
- int number_of_conclusions(){return rules.size();};
+ int number_of_conclusions(){return rules.size();};
bdd get_jth_conclusion(bdd** underlying, int j);
+ vector<vector<pair<bool,int> > > get_jth_conclusion(int j);