Skip to content

fix OR node choice variables #10

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
haz merged 4 commits into from
Mar 25, 2021
Merged

fix OR node choice variables #10

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
970a7ec
fix OR node choice variables
Mar 17, 2021
8f8dbff
fixup! fix OR node choice variables
Mar 23, 2021
9eac83b
Adding .gitignore file.
haz Mar 24, 2021
e76dbc1
Setting the choiceVar everywhere that needs it.
haz Mar 24, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
.venv
Makefile
dsharp

*.dot
*.nnf
*.png
7 changes: 2 additions & 5 deletions src/src_sharpSAT/MainSolver/DecisionTree.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -723,11 +723,7 @@ void DTNode::genNNF(ostream & out)
}
else if (DT_OR == type)
{
//Dimitar Sht. Shterionov: ignoring negative values on OR nodes
if (choiceVar > 0)
out << "O " << choiceVar << " " << children.size();
else
out << "O 0 " << children.size();
out << "O " << choiceVar << " " << children.size();

if (2 != children.size())
toSTDOUT("Error: Or node with " << children.size() << " children.");
Expand Down Expand Up @@ -824,6 +820,7 @@ void DTNode::smooth(int &num_nodes, CMainSolver &solver, set<int> &literals)
newAnd->addChild(newOr, true);
newOr->addChild(solver.get_lit_node_full(var), true);
newOr->addChild(solver.get_lit_node_full(-1 * var), true);
newOr->choiceVar = (unsigned) var;
}
}
// Record the new values
Expand Down
2 changes: 1 addition & 1 deletion src/src_sharpSAT/MainSolver/DecisionTree.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ class DTNode

public:

int choiceVar;
unsigned choiceVar;
int nnfID;

bool checked;
Expand Down
4 changes: 2 additions & 2 deletions src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -944,8 +944,8 @@ bool CInstanceGraph::createfromFile(const char* lpstrFileName)
//--- and add the default values for all variables
for (unsigned int i = 0; i <= countAllVars(); i++)
{
varTranslation[(int) i] = (int) i;
varUntranslation[(int) i] = (int) i;
varTranslation[(int) i] = i;
varUntranslation[(int) i] = i;
}

return true;
Expand Down
12 changes: 6 additions & 6 deletions src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,9 +47,9 @@ class CInstanceGraph
unsigned int numBinClauses;
unsigned int numBinCCls;

vector<int> varTranslation;
vector<int> varUntranslation;
vector<int> origTranslation;
vector<unsigned> varTranslation;
vector<unsigned> varUntranslation;
vector<unsigned> origTranslation;

protected:

Expand Down Expand Up @@ -172,17 +172,17 @@ class CInstanceGraph
CInstanceGraph();
~CInstanceGraph();

const vector<int> & getVarTranslation() const
const vector<unsigned> & getVarTranslation() const
{
return varTranslation;
}

const vector<int> & getVarUnTranslation() const
const vector<unsigned> & getVarUnTranslation() const
{
return varUntranslation;
}

const vector<int> & getOrigTranslation() const
const vector<unsigned> & getOrigTranslation() const
{
return origTranslation;
}
Expand Down
5 changes: 4 additions & 1 deletion src/src_sharpSAT/MainSolver/MainSolver.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -179,6 +179,7 @@ void CMainSolver::solve(const char *lpstrFileName)

// Add an arbitrary choice between the two
DTNode* newOr = new DTNode(DT_OR, num_Nodes++);
newOr->choiceVar = (unsigned) i;
decStack.top().getDTNode()->addChild(newOr, true);
newOr->addChild(new DTNode(i, true, num_Nodes++), true);
newOr->addChild(new DTNode((-1 * i), true, num_Nodes++), true);
Expand All @@ -192,6 +193,7 @@ void CMainSolver::solve(const char *lpstrFileName)

newOr->addChild(get_lit_node_full(-1 * i), true);
newOr->addChild(newAnd, true);
newOr->choiceVar = (unsigned) i;

newAnd->addChild(new DTNode(i, true, num_Nodes++), true);
newAnd->addChild(botNode, true);
Expand All @@ -205,6 +207,7 @@ void CMainSolver::solve(const char *lpstrFileName)

newOr->addChild(get_lit_node_full(i), true);
newOr->addChild(newAnd, true);
newOr->choiceVar = (unsigned) i;

newAnd->addChild(new DTNode((-1 * i), true, num_Nodes++), true);
newAnd->addChild(botNode, true);
Expand Down Expand Up @@ -356,7 +359,7 @@ bool CMainSolver::decide()
DTNode * leftLit = get_lit_node(theLit.toSignedInt());
DTNode * rightLit = get_lit_node(-1 * theLit.toSignedInt());

newNode->choiceVar = theLit.toSignedInt();
newNode->choiceVar = theLit.toVarIdx();

// Set the parents
left->addParent(newNode, true);
Expand Down
60 changes: 50 additions & 10 deletions src/src_sharpSAT/MainSolver/MainSolver.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -333,7 +333,7 @@ class CMainSolver: public CInstanceGraph
out << "AND";
break;
case DT_OR:
out << "OR";
out << "OR " << node->choiceVar;
break;
case DT_BOTTOM:
out << "F";
Expand Down Expand Up @@ -432,7 +432,7 @@ class CMainSolver: public CInstanceGraph
}
}

void print_translation(const vector<int> trans)
void print_translation(const vector<unsigned> trans)
{
toSTDOUT("Translation:" << endl);
for (int i = 0; i < trans.size(); ++i)
Expand All @@ -441,15 +441,55 @@ class CMainSolver: public CInstanceGraph
}
}

void translateLiterals(const vector<int> varTranslation) {
for (int i = 0; i < litNodes.size(); i++) {
if (litNodes[i]->getVal() < 0)
{
litNodes[i]->setVal(-1 * varTranslation[-1 * litNodes[i]->getVal()]);
}
else
void translateLiterals(const vector<unsigned> varTranslation) {
set<int> nodesSeen;
queue<DTNode *> openList;
openList.push(decStack.top().getDTNode());

int rootID = openList.front()->getID();

DTNode *node;
while (!openList.empty())
{
node = openList.front();
openList.pop();

int node_id = node->getID();

if (nodesSeen.find(node_id) == nodesSeen.end())
{
litNodes[i]->setVal(varTranslation[litNodes[i]->getVal()]);
// Make sure we don't add this twice
nodesSeen.insert(node_id);

// Add the children to the open list
set<DTNode *>::iterator it;
for (it = node->getChildrenBegin(); it
!= node->getChildrenEnd(); it++)
{
openList.push(*it);
}

// process the node
if (DT_LIT == node->getType())
{
if (node->getVal() < 0)
{
node->setVal(-1 * varTranslation[-1 * node->getVal()]);
}
else
{
node->setVal(varTranslation[node->getVal()]);
}
}

if (DT_OR == node->getType())
{
if (node->choiceVar) {
node->choiceVar = varTranslation[node->choiceVar];
Copy link
Contributor

@haz haz Mar 23, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's this line I'm concerned with. varTranslation comes in as vector<int>, and while the other instances are int, this one comes in as unsigned.

Copy link
Author

@symphorien symphorien Mar 23, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh indeed ! I had missed this one !
I went all the way and fixed the translation vector to contain unsigned values. i'm fairly confident that it's correct because I can compile sucessfully with -Wsign-promo -Wsign-conversion -Wsign-compare -Werror

}
}


}
}
}
Expand Down