Skip to content

Commit

Permalink
reverted Quantorizer.cpp
Browse files Browse the repository at this point in the history
  • Loading branch information
Fredo Erxleben committed Mar 5, 2015
2 parents 1118b6e + 1360a87 commit c9f41a5
Show file tree
Hide file tree
Showing 2 changed files with 53 additions and 62 deletions.
104 changes: 47 additions & 57 deletions interfaces/quantor/Quantorizer.cpp
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
#line 68 "Quantorizer.ypp"

#include "Quantorizer.hpp"
#include "QtDebug"

using namespace q2d::quantor;

Expand Down Expand Up @@ -95,12 +94,12 @@ unsigned Quantorizer::nextToken(YYSVal &sval) {
break;
}
if(res == 0) {
unsigned const var = (*context)[std::string(formula, len)];
qDebug() << "resolve:" << QString(formula) << "->" << var;
assert(var > 0);
assert(var <= max_named);
sval = var;
res = IDENT;
std::string name(formula, len);
unsigned const var = (*context)[name];
assert(var <= max_named);
if(var == 0) error("Could not resolve variable \"" + name + '"');
sval = var;
res = IDENT;
}
formula = p;
return res;
Expand All @@ -113,15 +112,6 @@ unsigned Quantorizer::nextToken(YYSVal &sval) {

//- Public Usage Interface ---------------------------------------------------
inline Result Quantorizer::solve0(QICircuit const &c, std::vector<int> &sol) {

qDebug() << c.configVars().size() << " config vars";

// DEBUG
for(unsigned i : c.configVars()){
qDebug() << ":->" << QString::number(i);
}
// END DEBUG

// Quantifier Preamble
openScope(QUANTOR_EXISTENTIAL_VARIABLE_TYPE, c.configVars());
closeScope();
Expand Down Expand Up @@ -160,7 +150,7 @@ Result Quantorizer::solve(QICircuit const &c, std::vector<int> &sol) {
}


#line 152 "Quantorizer.cpp"
#line 153 "Quantorizer.cpp"
#include <vector>
class q2d::quantor::Quantorizer::YYStack {
class Ele {
Expand Down Expand Up @@ -197,7 +187,7 @@ class q2d::quantor::Quantorizer::YYStack {
unsigned short operator*() const { return stack.back().state; }
};

char const *const q2d::quantor::Quantorizer::yyterms[] = { "EOF",
char const *const q2d::quantor::Quantorizer::yyterms[] = { "EOF",
"NOT", "AND", "OR", "XOR", "NAND", "NOR", "XNOR", "IDENT",
"'='", "'('", "')'", };
unsigned short const q2d::quantor::Quantorizer::yyintern[] = {
Expand Down Expand Up @@ -354,135 +344,135 @@ void q2d::quantor::Quantorizer::parse() {
YYSVal yylval;
unsigned short const yyrno = (yyact < 0)? -yyact : 0;
unsigned short const yylen = yylength[yyrno];

#ifdef TRACE
std::cerr << "Reduce by " << yyrules[yyrno] << std::endl;
#endif
switch(yyrno) { // do semantic actions
case 0: // accept
return;
case 1: {
#line 226 "Quantorizer.ypp"
#line 227 "Quantorizer.ypp"

addClause(yystack[yylen - 1]);

#line 358 "Quantorizer.cpp"
addClause(yystack[yylen - 1]);
#line 359 "Quantorizer.cpp"
break;
}
case 2: {
#line 229 "Quantorizer.ypp"
#line 230 "Quantorizer.ypp"

addClause( yystack[yylen - 1], -yystack[yylen - 3]);
addClause(-yystack[yylen - 1], yystack[yylen - 3]);

#line 367 "Quantorizer.cpp"
#line 368 "Quantorizer.cpp"
break;
}
case 3: {
#line 233 "Quantorizer.ypp"
#line 234 "Quantorizer.ypp"

unsigned const res = makeAuxiliary();
addClause( res, -yystack[yylen - 1], -yystack[yylen - 3]);
addClause(-res, yystack[yylen - 1]);
addClause(-res, yystack[yylen - 3]);
yylval = res;

#line 379 "Quantorizer.cpp"
#line 380 "Quantorizer.cpp"
break;
}
case 4: {
#line 240 "Quantorizer.ypp"
#line 241 "Quantorizer.ypp"

unsigned const res = makeAuxiliary();
addClause(-res, yystack[yylen - 1], yystack[yylen - 3]);
addClause( res, -yystack[yylen - 1]);
addClause( res, -yystack[yylen - 3]);
yylval = res;

#line 391 "Quantorizer.cpp"
#line 392 "Quantorizer.cpp"
break;
}
case 5: {
#line 247 "Quantorizer.ypp"
#line 248 "Quantorizer.ypp"

unsigned const res = makeAuxiliary();
addClause(-res, -yystack[yylen - 1], -yystack[yylen - 3]);
addClause(-res, yystack[yylen - 1], yystack[yylen - 3]);
addClause( res, -yystack[yylen - 1], yystack[yylen - 3]);
addClause( res, yystack[yylen - 1], -yystack[yylen - 3]);
yylval = res;

#line 404 "Quantorizer.cpp"
#line 405 "Quantorizer.cpp"
break;
}
case 6: {
#line 255 "Quantorizer.ypp"
#line 256 "Quantorizer.ypp"

unsigned const res = makeAuxiliary();
addClause(-res, -yystack[yylen - 1], -yystack[yylen - 3]);
addClause( res, yystack[yylen - 1]);
addClause( res, yystack[yylen - 3]);
yylval = res;

#line 416 "Quantorizer.cpp"
#line 417 "Quantorizer.cpp"
break;
}
case 7: {
#line 262 "Quantorizer.ypp"
#line 263 "Quantorizer.ypp"

unsigned const res = makeAuxiliary();
addClause( res, yystack[yylen - 1], yystack[yylen - 3]);
addClause(-res, -yystack[yylen - 1]);
addClause(-res, -yystack[yylen - 3]);
yylval = res;

#line 428 "Quantorizer.cpp"
#line 429 "Quantorizer.cpp"
break;
}
case 8: {
#line 269 "Quantorizer.ypp"
#line 270 "Quantorizer.ypp"

unsigned const res = makeAuxiliary();
addClause( res, -yystack[yylen - 1], -yystack[yylen - 3]);
addClause( res, yystack[yylen - 1], yystack[yylen - 3]);
addClause(-res, -yystack[yylen - 1], yystack[yylen - 3]);
addClause(-res, yystack[yylen - 1], -yystack[yylen - 3]);
yylval = res;

#line 441 "Quantorizer.cpp"
#line 442 "Quantorizer.cpp"
break;
}
case 9: {
#line 277 "Quantorizer.ypp"
yylval = yystack[yylen - 1];
#line 447 "Quantorizer.cpp"
#line 278 "Quantorizer.ypp"
yylval = yystack[yylen - 1];
#line 448 "Quantorizer.cpp"
break;
}
case 10: {
#line 278 "Quantorizer.ypp"
yylval = yystack[yylen - 1];
#line 453 "Quantorizer.cpp"
#line 279 "Quantorizer.ypp"
yylval = yystack[yylen - 1];
#line 454 "Quantorizer.cpp"
break;
}
case 11: {
#line 279 "Quantorizer.ypp"
yylval = yystack[yylen - 2];
#line 459 "Quantorizer.cpp"
#line 280 "Quantorizer.ypp"
yylval = yystack[yylen - 2];
#line 460 "Quantorizer.cpp"
break;
}
case 12: {
#line 280 "Quantorizer.ypp"
#line 281 "Quantorizer.ypp"

unsigned const res = makeAuxiliary();
addClause( res, yystack[yylen - 2]);
addClause(-res, -yystack[yylen - 2]);
yylval = res;

#line 470 "Quantorizer.cpp"
#line 471 "Quantorizer.cpp"
break;
}
}

yystack.pop(yylen);
yystack.push(yygoto[*yystack][yylhs[yyrno]], yylval);
}
Expand Down
11 changes: 6 additions & 5 deletions interfaces/quantor/Quantorizer.ypp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -160,11 +160,12 @@ unsigned Quantorizer::nextToken(YYSVal &sval) {
break;
}
if(res == 0) {
unsigned const var = (*context)[std::string(formula, len)];
assert(var > 0);
assert(var <= max_named);
sval = var;
res = IDENT;
std::string name(formula, len);
unsigned const var = (*context)[name];
assert(var <= max_named);
if(var == 0) error("Could not resolve variable \"" + name + '"');
sval = var;
res = IDENT;
}
formula = p;
return res;
Expand Down

0 comments on commit c9f41a5

Please sign in to comment.