fixup! fix OR node choice variables

Guillaume Girol · Guillaume Girol · commit 8f8dbff2666c · 2021-03-23T17:59:37.000+01:00
diff --git a/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp b/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp
@@ -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;
diff --git a/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h b/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h
@@ -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:
 
@@ -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;
 	}
diff --git a/src/src_sharpSAT/MainSolver/MainSolver.h b/src/src_sharpSAT/MainSolver/MainSolver.h
@@ -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)
@@ -441,7 +441,7 @@ class CMainSolver: public CInstanceGraph
 		}
 	}
     
-	void translateLiterals(const vector<int> varTranslation) {
+	void translateLiterals(const vector<unsigned> varTranslation) {
 		set<int> nodesSeen;
 		queue<DTNode *> openList;
 		openList.push(decStack.top().getDTNode());

Original file line number	Diff line number	Diff line change
`@@ -944,8 +944,8 @@ bool CInstanceGraph::createfromFile(const char* lpstrFileName)`
`944`	`944`	`//--- and add the default values for all variables`
`945`	`945`	`for (unsigned int i = 0; i <= countAllVars(); i++)`
`946`	`946`	`{`
`947`		`- varTranslation[(int) i] = (int) i;`
`948`		`- varUntranslation[(int) i] = (int) i;`
	`947`	`+ varTranslation[(int) i] = i;`
	`948`	`+ varUntranslation[(int) i] = i;`
`949`	`949`	`}`
`950`	`950`
`951`	`951`	`return true;`
Original file line number	Diff line number	Diff line change
`@@ -47,9 +47,9 @@ class CInstanceGraph`
`47`	`47`	`unsigned int numBinClauses;`
`48`	`48`	`unsigned int numBinCCls;`
`49`	`49`
`50`		`- vector<int> varTranslation;`
`51`		`- vector<int> varUntranslation;`
`52`		`- vector<int> origTranslation;`
	`50`	`+ vector<unsigned> varTranslation;`
	`51`	`+ vector<unsigned> varUntranslation;`
	`52`	`+ vector<unsigned> origTranslation;`
`53`	`53`
`54`	`54`	`protected:`
`55`	`55`
`@@ -172,17 +172,17 @@ class CInstanceGraph`
`172`	`172`	`CInstanceGraph();`
`173`	`173`	`~CInstanceGraph();`
`174`	`174`
`175`		`- const vector<int> & getVarTranslation() const`
	`175`	`+ const vector<unsigned> & getVarTranslation() const`
`176`	`176`	`{`
`177`	`177`	`return varTranslation;`
`178`	`178`	`}`
`179`	`179`
`180`		`- const vector<int> & getVarUnTranslation() const`
	`180`	`+ const vector<unsigned> & getVarUnTranslation() const`
`181`	`181`	`{`
`182`	`182`	`return varUntranslation;`
`183`	`183`	`}`
`184`	`184`
`185`		`- const vector<int> & getOrigTranslation() const`
	`185`	`+ const vector<unsigned> & getOrigTranslation() const`
`186`	`186`	`{`
`187`	`187`	`return origTranslation;`
`188`	`188`	`}`
Original file line number	Diff line number	Diff line change
`@@ -432,7 +432,7 @@ class CMainSolver: public CInstanceGraph`
`432`	`432`	`}`
`433`	`433`	`}`
`434`	`434`
`435`		`- void print_translation(const vector<int> trans)`
	`435`	`+ void print_translation(const vector<unsigned> trans)`
`436`	`436`	`{`
`437`	`437`	`toSTDOUT("Translation:" << endl);`
`438`	`438`	`for (int i = 0; i < trans.size(); ++i)`
`@@ -441,7 +441,7 @@ class CMainSolver: public CInstanceGraph`
`441`	`441`	`}`
`442`	`442`	`}`
`443`	`443`
`444`		`- void translateLiterals(const vector<int> varTranslation) {`
	`444`	`+ void translateLiterals(const vector<unsigned> varTranslation) {`
`445`	`445`	`set<int> nodesSeen;`
`446`	`446`	`queue<DTNode *> openList;`
`447`	`447`	`openList.push(decStack.top().getDTNode());`