From a8244198efcb865b48c1049d15c1c935c6927435 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <uni@thorsten-wissmann.de>
Date: Sun, 26 Jan 2014 20:51:21 +0100
Subject: [PATCH] Some GMLMIP improvements
---
GMLMIP-0.1/formulas/formula.cpp | 7 ++++---
GMLMIP-0.1/onestep-example.cpp | 6 ++++--
2 files changed, 8 insertions(+), 5 deletions(-)
diff --git a/GMLMIP-0.1/formulas/formula.cpp b/GMLMIP-0.1/formulas/formula.cpp
index 2b24377..5493548 100644
--- a/GMLMIP-0.1/formulas/formula.cpp
+++ b/GMLMIP-0.1/formulas/formula.cpp
@@ -271,13 +271,14 @@ 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/onestep-example.cpp b/GMLMIP-0.1/onestep-example.cpp
index 25e07f2..b5da1f3 100644
--- a/GMLMIP-0.1/onestep-example.cpp
+++ b/GMLMIP-0.1/onestep-example.cpp
@@ -33,8 +33,9 @@ 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_or(f->modal(new bdd(f->variable(4)), 4, 0),
- bdd_not(f->modal(new bdd(bdd_not(f->variable(7))), 3, 0)));
+ bdd b = bdd_and(bdd_and(f->modal(new bdd(f->variable(8)), 4, 0),
+ bdd_not(f->modal(new bdd(bdd_not(f->variable(7))), 3, 0))),
+ bdd_not(f->modal(new bdd(bdd_not(f->variable(9))), 3, 0)));
f->set_bdd(b);
// bdd_varblockall();
// bdd_reorder(BDD_REORDER_WIN3ITE);
@@ -62,6 +63,7 @@ int main (int argc, char *argv[]){
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,";
--
GitLab