diff --git a/GMLMIP-0.1/formulas/formula.cpp b/GMLMIP-0.1/formulas/formula.cpp
index dc58133a109d054a6a8142a949c385b4bc7f6f44..0a9ef1ed30324d9b7d2717442aa57719686eb1f7 100644
--- a/GMLMIP-0.1/formulas/formula.cpp
+++ b/GMLMIP-0.1/formulas/formula.cpp
@@ -2,8 +2,6 @@
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); //
@@ -50,42 +48,17 @@ 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;
- bool isSat = check_satisfiability(bdd_rep);
- assert(isSat == false);
- recursive_satisfiability_check = backup_rek;
- vector<SatisfyingAssignment> ret = rulechildren;
- rulechildren.clear();
- return ret;
-}
-
template<class ModalValueType>
bool Formula<ModalValueType>::check_satisfiability(bdd b){
- if (!recursive_satisfiability_check && modality_depth >= 1) {
- bdd_allsat(b, sat_handler); // pushes satisfying assignment onto stack
- 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]);
- if (!recursive_satisfiability_check) sat = false;
- }
- modality_depth--;
- return sat;
+ 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]);
}
+ return sat;
}
template<class ModalValueType>
@@ -133,8 +106,7 @@ 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() &&
- (!recursive_satisfiability_check || result); i++){
+ for(int i = 0; i < concs.number_of_conclusions() && result; i++){
bdd b = concs.get_jth_conclusion(underlying_formulae, i);
result = check_satisfiability(b);
}
@@ -172,10 +144,10 @@ bool Formula<ModalValueType>::enumerate_rules(Premise<ModalValueType>& prem, bdd
vector<bool> zero(total_valuations, false);
- if (run_solver(problem, parameters, false, zero, -1) || !recursive_satisfiability_check) {
- if (run_solver(problem, parameters, true, zero, 0)) {
+ if (run_solver(problem, parameters, false, zero, -1)) {
+ 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()) {
@@ -203,13 +175,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 || !recursive_satisfiability_check); k++) {
+ for (unsigned int k = 0; k < node_queue.size() && result; 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 || !recursive_satisfiability_check); i++){
+ for(int i = power+1; i < total_valuations && result; i++){
vector<bool> new_node(current_node);
new_node[i] = true;
@@ -272,14 +244,13 @@ bool Formula<ModalValueType>::run_solver(glp_prob *problem, glp_iocp* parameters
// Modify glp problem to match node
for(unsigned int i = 0; i < current_node.size(); i++){
- if(current_node[i]) {
+ if(current_node[i])
glp_set_row_bnds(problem, i+1, GLP_LO, 1.0, 0.0); // > 0
//+1 since valuations go zero to 2^(n+m)-1, glpk rows go 1 to 2^(n+m).
- } else if (strict || static_cast<int>(i) <= index) {
+ else if (strict || static_cast<int>(i) <= index)
glp_set_row_bnds(problem, i+1, GLP_UP, 0.0, 0.0); // leq 0
- } else {
+ else
glp_set_row_bnds(problem, i+1, GLP_FR, 0.0, 0.0); // don't care
- }
}
if (!strict) {
diff --git a/GMLMIP-0.1/formulas/formula.h b/GMLMIP-0.1/formulas/formula.h
index bdea56da4a800687ce4897da20aef5f0689a9aca..a5931d1497c1b2cfd0d3b7f08c9eeed1ef80933d 100644
--- a/GMLMIP-0.1/formulas/formula.h
+++ b/GMLMIP-0.1/formulas/formula.h
@@ -40,11 +40,7 @@ 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 int variable_back(int v) = 0;
- virtual bool has_variable_back(int v) = 0;
};
template<class ModalValueType>
@@ -133,9 +129,6 @@ class Formula : public IFormula{
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;
- bool recursive_satisfiability_check; // whether rule enumerationis should call check_satisfiability()
- int modality_depth; // nesting depth of satisfiability()
- vector<SatisfyingAssignment> rulechildren;
public:
Formula();
@@ -150,14 +143,11 @@ 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/rules/radixtree.h b/GMLMIP-0.1/rules/radixtree.h
index 5952c83fb09399872dc31388691eb2b0a3c1a31e..08df3d109f32811971b3474746aa428488aa6e63 100644
--- a/GMLMIP-0.1/rules/radixtree.h
+++ b/GMLMIP-0.1/rules/radixtree.h
@@ -1,8 +1,8 @@
#ifndef RADIXTREE_HH
#define RADIXTREE_HH
-#include <vector>
#include <cstdlib>
+#include <vector>
using namespace std;
diff --git a/GMLMIP-0.1/rules/setofconclusions.cpp b/GMLMIP-0.1/rules/setofconclusions.cpp
index c4a54729b90f7b3b7068ef7c626ade3c9fb3be1b..d85e192ae8a90c5b66360fa12510c1488046bbbd 100644
--- a/GMLMIP-0.1/rules/setofconclusions.cpp
+++ b/GMLMIP-0.1/rules/setofconclusions.cpp
@@ -28,20 +28,8 @@ 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 5429fe678f0845a16d44ac013f4a65121e5a4029..5a7d2af65ab905a103eb9fd73876f37bbc484820 100644
--- a/GMLMIP-0.1/rules/setofconclusions.h
+++ b/GMLMIP-0.1/rules/setofconclusions.h
@@ -27,9 +27,8 @@ 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);