Skip to content

Commit 9ca6435

Browse files
mocenigomocenigo
committed
Improved upper/lower support and detection of bad chars
1 parent 79fda21 commit 9ca6435

20 files changed

+98
-21
lines changed

‎src/anf.cpp‎

Lines changed: 15 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ SOFTWARE.
2424
#include "anf.hpp"
2525

2626
#include <cctype>
27+
#include <cstdio>
2728
#include <fstream>
2829
#include <string>
2930
#include <boost/lexical_cast.hpp>
@@ -66,7 +67,7 @@ bool isCharInStr(const char c, const std::string& s) {
6667
return false;
6768
}
6869

69-
size_t ANF::readFileForMaxVar(const std::string& filename)
70+
size_t ANF::readFileForNumVars(const std::string& filename)
7071
{
7172
// Read in the file line by line
7273
size_t maxes[26] = {0};
@@ -100,9 +101,7 @@ size_t ANF::readFileForMaxVar(const std::string& filename)
100101
//At this point, only numbers are valid
101102
if (!std::isdigit(temp[i])) {
102103
var = 0;
103-
char temp_char = temp[i];
104-
if (temp_char >= 'A' && temp_char <= 'Z')
105-
temp_char += 'a' - 'A';
104+
106105
if (temp[i] == '_')
107106
continue;
108107

@@ -122,10 +121,17 @@ size_t ANF::readFileForMaxVar(const std::string& filename)
122121
start_bracket = true;
123122
continue;
124123
}
125-
if (isCharInStr(temp_char,var_letters)) {
126-
varLetter = temp_char;
124+
tmp_char = tolower(temp[i]);
125+
if (isCharInStr(tmp_char,var_letters)) {
126+
varLetter = tmp_char;
127127
isMonomial = true;
128128
} else {
129+
if (!isascii(temp[i])) {
130+
cout << "ERROR: Unknown character 0x" << (int)temp[i] << " (" << temp[i] << ")"
131+
<< " at position " << i
132+
<< " in equation: \"" << temp << "\"" << endl;
133+
exit(-1);
134+
}
129135
isMonomial = false;
130136
}
131137
} else if (isMonomial) {
@@ -148,7 +154,7 @@ size_t ANF::readFileForMaxVar(const std::string& filename)
148154
return maxVar+2;
149155
}
150156

151-
size_t ANF::readFile(const std::string& filename)
157+
size_t ANF::readANFFromFile(const std::string& filename)
152158
{
153159
// Read in the file line by line
154160
vector<std::string> text_file;
@@ -381,9 +387,9 @@ size_t ANF::readFile(const std::string& filename)
381387

382388
//At this point, only numbers are valid
383389
if (temp[i] < '0' || temp[i] > '9') {
384-
cout << "ERROR: Unknown character 0x" << (int)temp[i]
390+
cout << "ERROR: Unknown character 0x" << (int)temp[i] << " (" << temp[i] << ")"
385391
<< " at position " << i
386-
<< " in equation: " << temp << "\"" << endl;
392+
<< " in equation: \"" << temp << "\"" << endl;
387393
exit(-1);
388394
}
389395

‎src/anf.hpp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -86,7 +86,7 @@ class ANF
8686
ANF(const ANF&) = delete;
8787
~ANF();
8888

89-
size_t readFile(const string& filename);
89+
size_t readANFFromFile(const string& filename);
9090
bool propagate();
9191
inline vector<lbool> extendSolution(const vector<lbool>& solution) const;
9292
void printStats() const;
@@ -122,7 +122,7 @@ class ANF
122122
inline lbool value(const uint32_t var) const;
123123
inline Lit getReplaced(const uint32_t var) const;
124124
inline ANF& operator=(const ANF& other);
125-
static size_t readFileForMaxVar(const std::string& filename);
125+
static size_t readFileForNumVars(const std::string& filename);
126126
set<size_t> get_proj_set() const;
127127

128128
private:

‎src/bosphorus.cpp‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -140,14 +140,14 @@ Bosph::ANF* Bosphorus::read_anf(const char* fname)
140140
assert(fname != NULL);
141141
check_library_in_use();
142142

143-
// Find out maxVar in input ANF file
144-
size_t maxVar = BLib::ANF::readFileForMaxVar(fname);
143+
// Find out number of variables in input ANF file
144+
size_t numVars = BLib::ANF::readFileForNumVars(fname);
145145

146146
// Construct ANF
147-
// ring size = maxVar + 1, because ANF variables start from x0
148-
dat->pring = new BoolePolyRing(maxVar + 1);
147+
// ring size = numVars,
148+
dat->pring = new BoolePolyRing(numVars);
149149
auto anf = new BLib::ANF(dat->pring, dat->config);
150-
anf->readFile(fname);
150+
anf->readANFFromFile(fname);
151151
return (Bosph::ANF*)anf;
152152
}
153153

‎tests/anf-files/anf_prop.anf.resolve‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
0 signifies 0
2+
1 signifies 1
3+
2 signifies x_1
4+
3 signifies x_2

‎tests/anf-files/anf_prop.cnf‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
p cnf 6 2
2+
-3 4 0
3+
3 -4 0
4+
c p show 1 2 3 0
5+
c Learnt 0 fact(s), not all of which have been dumped

‎tests/anf-files/bad_char.anf‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
x(1) + x2 + ü1
2+
X1*x2 + x2*ü1 + 1

‎tests/anf-files/bad_char.anf.resolve‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
0 signifies 0
2+
1 signifies 1
3+
2 signifies x_1
4+
3 signifies x_2

‎tests/anf-files/gj,cnf‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
p cnf 7 3
2+
-3 0
3+
-4 0
4+
-5 0
5+
c p show 1 2 0
6+
c Learnt 4 fact(s), not all of which have been dumped

‎tests/anf-files/gj.anf.resolve‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
0 signifies 0
2+
1 signifies 1
3+
2 signifies x_1
4+
3 signifies x_2
5+
4 signifies x_3

‎tests/anf-files/not_eaten.cnf‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
p cnf 5 1
2+
-3 0
3+
c p show 1 2 0
4+
c Learnt 1 fact(s), not all of which have been dumped

0 commit comments

Comments
 (0)