diff --git a/interfaces/Quantor.h b/interfaces/Quantor.h
index 64ec313..44b7a3f 100644
--- a/interfaces/Quantor.h
+++ b/interfaces/Quantor.h
@@ -36,8 +36,6 @@ class QuantorInterface :
 
     QMap<QString, QIContext> m_contexts;
 
-    // the solver will return a zero-terminated array of int
-    Result (*m_solverMain)(QICircuit const &, std::vector<int> &) = nullptr;
     QList<int> m_solution;
 
     // helper functions
diff --git a/interfaces/quantor/ParseException.h b/interfaces/quantor/ParseException.h
index b20de8e..0b505cb 100644
--- a/interfaces/quantor/ParseException.h
+++ b/interfaces/quantor/ParseException.h
@@ -5,7 +5,6 @@
 
 namespace q2d {
 namespace quantor {
-class QIContext;
 /**
  * This class captures information about and the location of
  * a parsing problem encountered by the Quantorizer and may
@@ -15,19 +14,22 @@ class QIContext;
  */
 class ParseException {
     std::string const  m_msg;
-    QIContext   const &m_ctx;
+    unsigned           m_pos;
 
 public:
-    ParseException(std::string  msg, QIContext const &ctx)
-        : m_msg(msg), m_ctx(ctx) {}
+    ParseException(std::string  msg, unsigned  pos)
+        : m_msg(msg), m_pos(pos) {}
     ~ParseException() {}
 
 public:
     std::string const &message() const {
         return  m_msg;
     }
-    QIContext   const &context() const {
-        return  m_ctx;
+    unsigned position() const {
+        return  m_pos;
+    }
+    void position(unsigned  pos) {
+	m_pos = pos;
     }
 };
 }
diff --git a/interfaces/quantor/Quantorizer.cpp b/interfaces/quantor/Quantorizer.cpp
index c7438c2..282cd39 100644
--- a/interfaces/quantor/Quantorizer.cpp
+++ b/interfaces/quantor/Quantorizer.cpp
@@ -1,51 +1,24 @@
-#line 68 "Quantorizer.ypp"
+#line 70 "Quantorizer.ypp"
 
 #include "Quantorizer.hpp"
-#include <QtDebug>
 
-using namespace q2d::quantor;
+#include <cctype>
+#include <cassert>
+#include <string.h>
 
-//- Life Cycle ---------------------------------------------------------------
-inline Quantorizer::Quantorizer() : max_var(0), context(0), formula(0) {}
-inline Quantorizer::~Quantorizer() {}
-
-//- Problem Building ---------------------------------------------------------
-template<typename IT>
-void Quantorizer::openScope(QuantorQuantificationType const  type, IT  vars) {
-  quantor.scope(type);
-  for(unsigned const  var : vars) {
-    assert(var > 0);
-    if(var > max_var)  max_var = var;
-    quantor.add(var);
-  }
+extern "C" {
+#include "Quantor.h"
 }
-inline void Quantorizer::closeScope() { quantor.add(0); }
 
-//- Private Parser Helpers ---------------------------------------------------
-inline unsigned Quantorizer::makeAuxiliary() {
-  unsigned const  res = ++max_var;
-  quantor.add(res);
-  return  res;
-}
-inline void Quantorizer::addClause(int const  a) {
-  clauses.push_back(a);
-  clauses.push_back(0);
-}
-inline void Quantorizer::addClause(int const  a, int const  b) {
-  clauses.push_back(a);
-  clauses.push_back(b);
-  clauses.push_back(0);
-}
-inline void Quantorizer::addClause(int const  a, int const  b, int const  c) {
-  clauses.push_back(a);
-  clauses.push_back(b);
-  clauses.push_back(c);
-  clauses.push_back(0);
-}
+using namespace q2d::quantor;
+
+//- Life Cycle ---------------------------------------------------------------
+Quantorizer::Quantorizer() : max_var(0), context(0), formula(0) {}
+Quantorizer::~Quantorizer() {}
 
 //- Parser Interface Methods -------------------------------------------------
 inline void Quantorizer::error(std::string  msg) {
-  throw  ParseException(msg, *context);
+  throw  ParseException(msg, 0);
 }
 
 unsigned Quantorizer::nextToken(YYSVal &sval) {
@@ -76,32 +49,28 @@ unsigned Quantorizer::nextToken(YYSVal &sval) {
     if(isspace(c))  continue;
     if(isalpha(c) || (c == '_')) {
       char const *p = formula--;
-      while(isalnum(*p) || (*p == '_') || (*p == '/') || (*p == '-'))  p++;
+      while(isalnum(*p) || (c == '_') || (c == '-') || (c == '/'))  p++;
       unsigned const  len = p-formula;
       unsigned  res = 0;
       switch(len) {
       case 2:
-    if(strncmp(formula, "or", 2) == 0)  res = OR;
-    break;
+	if(strncmp(formula, "or", 2) == 0)  res = OR;
+	break;
       case 3:
-    if     (strncmp(formula, "and", 3) == 0)  res = AND;
-    else if(strncmp(formula, "xor", 3) == 0)  res = XOR;
-    else if(strncmp(formula, "nor", 3) == 0)  res = NOR;
-    else if(strncmp(formula, "not", 3) == 0)  res = NOT;
-    break;
+	if     (strncmp(formula, "and", 3) == 0)  res = AND;
+	else if(strncmp(formula, "xor", 3) == 0)  res = XOR;
+	else if(strncmp(formula, "nor", 3) == 0)  res = NOR;
+	else if(strncmp(formula, "not", 3) == 0)  res = NOT;
+	break;
       case 4:
-    if     (strncmp(formula, "nand", 4) == 0)  res = NAND;
-    else if(strncmp(formula, "xnor", 4) == 0)  res = XNOR;
-    break;
+	if     (strncmp(formula, "nand", 4) == 0)  res = NAND;
+	else if(strncmp(formula, "xnor", 4) == 0)  res = XNOR;
+	break;
       }
       if(res == 0) {
-    std::string  name(formula, len);
-    qDebug() << "Resolving" << name.c_str();
-    unsigned const  var = (*context)[name];
-    assert(var <= max_named);
-    if(var == 0)  error("Could not resolve variable \"" + name + '"');
-    sval = var;
-    res  = IDENT;
+	unsigned const  var = getVar(std::string(formula, len));
+	sval = var;
+	res  = VAR;
       }
       formula = p;
       return  res;
@@ -112,63 +81,101 @@ unsigned Quantorizer::nextToken(YYSVal &sval) {
   }
 }
 
+//- Private Parser Helpers ---------------------------------------------------
+unsigned Quantorizer::getVar(std::string const &name) {
+  Variable const  var = (*context)[name];
+  std::map<Variable, unsigned> *cat;
+  switch(context->typeOf(var)) {
+  case VariableType::CONFIG:  cat = &varConfigs; break;
+  case VariableType::INPUT:   cat = &varInputs;  break;
+  case VariableType::NODE:    cat = &varNodes;   break;
+  default: error("Unknown identifier: " + name);
+  }
+
+  // Check if variable is known already
+  auto const  v = cat->find(var);
+  if(v != cat->end())  return  v->second;
+
+  // Register new variable according to its type
+  return (*cat)[var] = ++max_var;
+}
+
+inline unsigned Quantorizer::makeAuxiliary() {
+  unsigned const  id = ++max_var;
+  varAux.push_back(id);
+  return  id;
+}
+
+inline void Quantorizer::addClause(int const  a) {
+  clauses.push_back(a);
+  clauses.push_back(0);
+}
+inline void Quantorizer::addClause(int const  a, int const  b) {
+  clauses.push_back(a);
+  clauses.push_back(b);
+  clauses.push_back(0);
+}
+inline void Quantorizer::addClause(int const  a, int const  b, int const  c) {
+  clauses.push_back(a);
+  clauses.push_back(b);
+  clauses.push_back(c);
+  clauses.push_back(0);
+}
+
 //- Public Usage Interface ---------------------------------------------------
-inline Result Quantorizer::solve0(QICircuit const &c, std::vector<int> &sol) {
-  // Quantifier Preamble
+void Quantorizer::parse(char const *fct) throw (ParseException) {
+  formula = fct;
+  try {
+    parse();
+  }
+  catch(ParseException &e) {
+    e.position(formula-fct);
+    throw;
+  }
+}
 
-    // DEBUG
-    for(unsigned i : c.configVars()){
-        qDebug() << "Config var" << i;
-    }
-    for(unsigned i : c.inputVars()){
-        qDebug() << "Input var" << i;
-    }
-    for(unsigned i : c.nodeVars()){
-        qDebug() << "Node var" << i;
-    }
-    // END DEBUG
-  openScope(QUANTOR_EXISTENTIAL_VARIABLE_TYPE, c.configVars());
-  closeScope();
-  openScope(QUANTOR_UNIVERSAL_VARIABLE_TYPE,   c.inputVars());
-  closeScope();
-  openScope(QUANTOR_EXISTENTIAL_VARIABLE_TYPE, c.nodeVars());
-  // leave it open!
-#ifndef NDEBUG
-  max_named = max_var;
-#endif
+Result Quantorizer::solve(std::vector<int> &sol) {
+  q2d::quantor::Quantor         q;      // solver
+  std::map<unsigned, Variable>  confs;  // reverse map for configs
 
-  // Parse in Component Specifications
-  for(QIContext const &ctx : c.contexts()) {
-    context = &ctx;
-    for(std::string const&  f : ctx.functions()) {
-      formula = f.c_str();
-      parse();
-    }
+  // Problem Building
+  q.scope(QUANTOR_EXISTENTIAL_VARIABLE_TYPE);
+  for(auto const &e : varConfigs) {
+    q.add(e.second);
+    confs.emplace(e.second, e.first);
   }
+  varConfigs.clear();
+  q.add(0);
+
+  q.scope(QUANTOR_UNIVERSAL_VARIABLE_TYPE);
+  for(auto const &e : varInputs)  q.add(e.second);
+  varInputs.clear();
+  q.add(0);
+
+  q.scope(QUANTOR_EXISTENTIAL_VARIABLE_TYPE);
+  for(auto const &e : varNodes)  q.add(e.second);
+  varNodes.clear();
+  for(unsigned  v : varAux)  q.add(v);
+  varAux.clear();
+  q.add(0);
 
-  // Finish Problem Specification
-  closeScope();
-  QString debugText = "clauses: ";
-  for(int  lit : clauses)  {
-      debugText.append(QString::number(lit)).append(", ");
-      quantor.add(lit);}
-  qDebug() << debugText << "";
+  for(int  lit : clauses)  q.add(lit);
+  clauses.clear();
 
   // Solve Problem
-  Result const  res = quantor.sat();
-  if(res == QUANTOR_RESULT_SATISFIABLE) {
-    int const *s = quantor.assignment();
-    while(*s)  sol.push_back(*s++);
+  Result const  res = q.sat();
+  if(res) {
+    auto const  end = confs.end();
+    for(int const *s = q.assignment(); *s; s++) {
+      auto const  it = confs.find(abs(*s));
+      if(it != end)  sol.push_back(*s < 0? -it->second : it->second);
+    }
   }
   return  res;
 }
 
-Result Quantorizer::solve(QICircuit const &c, std::vector<int> &sol) {
-  return  Quantorizer().solve0(c, sol);
-}
 
-
-#line 153 "Quantorizer.cpp"
+#line 178 "Quantorizer.cpp"
 #include <vector>
 class q2d::quantor::Quantorizer::YYStack {
   class Ele {
@@ -205,8 +212,8 @@ class q2d::quantor::Quantorizer::YYStack {
   unsigned short operator*() const { return  stack.back().state; }
 };
 
-char const *const  q2d::quantor::Quantorizer::yyterms[] = { "EOF",
-"NOT", "AND", "OR", "XOR", "NAND", "NOR", "XNOR", "IDENT",
+char const *const  q2d::quantor::Quantorizer::yyterms[] = { "EOF", 
+"NOT", "AND", "OR", "XOR", "NAND", "NOR", "XNOR", "VAR",
 "'='", "'('", "')'", };
 unsigned short const  q2d::quantor::Quantorizer::yyintern[] = {
      0,    264,    264,    264,    264,    264,    264,    264,
@@ -256,7 +263,7 @@ char const *const  q2d::quantor::Quantorizer::yyrules[] = {
 "   7: [ 2] expr     -> expr NOR expr",
 "   8: [ 2] expr     -> expr XNOR expr",
 "   9: [ 2] expr     -> prim",
-"  10: [ 3] prim     -> IDENT",
+"  10: [ 3] prim     -> VAR",
 "  11: [ 0] prim     -> '(' expr ')'",
 "  12: [ 1] prim     -> NOT prim",
 };
@@ -362,7 +369,7 @@ 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
@@ -370,48 +377,48 @@ void q2d::quantor::Quantorizer::parse() {
         case 0:         // accept
           return;
 case 1: {
-#line 227 "Quantorizer.ypp"
-
-       addClause(yystack[yylen - 1]);
+#line 254 "Quantorizer.ypp"
 
-#line 359 "Quantorizer.cpp"
+        addClause(yystack[yylen - 1]);
+       
+#line 384 "Quantorizer.cpp"
 break;
 }
 case 2: {
-#line 230 "Quantorizer.ypp"
+#line 257 "Quantorizer.ypp"
 
-           addClause( yystack[yylen - 1], -yystack[yylen - 3]);
-           addClause(-yystack[yylen - 1],  yystack[yylen - 3]);
-
-#line 368 "Quantorizer.cpp"
+        addClause( yystack[yylen - 1], -yystack[yylen - 3]);
+        addClause(-yystack[yylen - 1],  yystack[yylen - 3]);
+       
+#line 393 "Quantorizer.cpp"
 break;
 }
 case 3: {
-#line 234 "Quantorizer.ypp"
+#line 261 "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 380 "Quantorizer.cpp"
+       
+#line 405 "Quantorizer.cpp"
 break;
 }
 case 4: {
-#line 241 "Quantorizer.ypp"
+#line 268 "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 392 "Quantorizer.cpp"
+       
+#line 417 "Quantorizer.cpp"
 break;
 }
 case 5: {
-#line 248 "Quantorizer.ypp"
+#line 275 "Quantorizer.ypp"
 
         unsigned const  res = makeAuxiliary();
         addClause(-res, -yystack[yylen - 1], -yystack[yylen - 3]);
@@ -419,36 +426,36 @@ case 5: {
         addClause( res, -yystack[yylen - 1],  yystack[yylen - 3]);
         addClause( res,  yystack[yylen - 1], -yystack[yylen - 3]);
         yylval = res;
-
-#line 405 "Quantorizer.cpp"
+       
+#line 430 "Quantorizer.cpp"
 break;
 }
 case 6: {
-#line 256 "Quantorizer.ypp"
+#line 283 "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 417 "Quantorizer.cpp"
+       
+#line 442 "Quantorizer.cpp"
 break;
 }
 case 7: {
-#line 263 "Quantorizer.ypp"
+#line 290 "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 429 "Quantorizer.cpp"
+       
+#line 454 "Quantorizer.cpp"
 break;
 }
 case 8: {
-#line 270 "Quantorizer.ypp"
+#line 297 "Quantorizer.ypp"
 
         unsigned const  res = makeAuxiliary();
         addClause( res, -yystack[yylen - 1], -yystack[yylen - 3]);
@@ -456,41 +463,41 @@ case 8: {
         addClause(-res, -yystack[yylen - 1],  yystack[yylen - 3]);
         addClause(-res,  yystack[yylen - 1], -yystack[yylen - 3]);
         yylval = res;
-
-#line 442 "Quantorizer.cpp"
+       
+#line 467 "Quantorizer.cpp"
 break;
 }
 case 9: {
-#line 278 "Quantorizer.ypp"
- yylval = yystack[yylen - 1];
-#line 448 "Quantorizer.cpp"
+#line 305 "Quantorizer.ypp"
+ yylval = yystack[yylen - 1]; 
+#line 473 "Quantorizer.cpp"
 break;
 }
 case 10: {
-#line 279 "Quantorizer.ypp"
- yylval = yystack[yylen - 1];
-#line 454 "Quantorizer.cpp"
+#line 307 "Quantorizer.ypp"
+ yylval = yystack[yylen - 1]; 
+#line 479 "Quantorizer.cpp"
 break;
 }
 case 11: {
-#line 280 "Quantorizer.ypp"
- yylval = yystack[yylen - 2];
-#line 460 "Quantorizer.cpp"
+#line 308 "Quantorizer.ypp"
+ yylval = yystack[yylen - 2]; 
+#line 485 "Quantorizer.cpp"
 break;
 }
 case 12: {
-#line 281 "Quantorizer.ypp"
+#line 309 "Quantorizer.ypp"
 
         unsigned const  res = makeAuxiliary();
         addClause( res,  yystack[yylen - 2]);
         addClause(-res, -yystack[yylen - 2]);
         yylval = res;
-
-#line 471 "Quantorizer.cpp"
+       
+#line 496 "Quantorizer.cpp"
 break;
 }
         }
-
+        
         yystack.pop(yylen);
         yystack.push(yygoto[*yystack][yylhs[yyrno]], yylval);
       }
diff --git a/interfaces/quantor/Quantorizer.hpp b/interfaces/quantor/Quantorizer.hpp
index 86e680a..25e3007 100644
--- a/interfaces/quantor/Quantorizer.hpp
+++ b/interfaces/quantor/Quantorizer.hpp
@@ -3,67 +3,69 @@
 #line 1 "Quantorizer.ypp"
 
 #include <vector>
-#include <cctype>
-#include <cassert>
+#include <map>
 
-#include <string.h>
-
-#include "Quantor.h"
-#include "QICircuit.h"
 #include "QIContext.h"
 #include "ParseException.h"
+#include "Result.h"
 
 using namespace q2d::quantor;
 
-#line 18 "Quantorizer.hpp"
+#line 14 "Quantorizer.hpp"
 #include <string>
 namespace q2d {
 namespace quantor {
 class Quantorizer {
   typedef unsigned YYSVal;
   class YYStack;
-#line 26 "Quantorizer.ypp"
+#line 22 "Quantorizer.ypp"
+
 
-  Quantor   quantor;
+  // Variable Bookkeeping
   unsigned  max_var;
-#ifndef NDEBUG
-  unsigned  max_named;
-#endif
 
-  std::vector<int>  clauses;
-  QIContext const  *context;
-  char      const  *formula;
+  typedef unsigned Variable;
+  std::map<Variable, unsigned>  varConfigs;
+  std::map<Variable, unsigned>  varInputs;
+  std::map<Variable, unsigned>  varNodes;
+
+  std::vector<unsigned>  varAux;
+  std::vector<int>       clauses;
+
+  // Current Parsing State
+  QIContext const *context;
+  char      const *formula;
 
 //- Life Cycle ---------------------------------------------------------------
-private:
+public:
   Quantorizer();
   ~Quantorizer();
 
-//- Problem Building ---------------------------------------------------------
+//- Parser Interface Methods -------------------------------------------------
 private:
-  template<typename IT>
-  void openScope(QuantorQuantificationType const  type, IT  vars);
-  void closeScope();
+  void error(std::string  msg);
+  unsigned nextToken(YYSVal &sval);
 
 //- Private Parser Helpers ---------------------------------------------------
 private:
+  unsigned getVar(std::string const &name);
   unsigned makeAuxiliary();
   void addClause(int const  a);
   void addClause(int const  a, int const  b);
   void addClause(int const  a, int const  b, int const  c);
 
-//- Parser Interface Methods -------------------------------------------------
-private:
-  void error(std::string  msg);
-  unsigned nextToken(YYSVal &sval);
-
 //- Usage Interface ----------------------------------------------------------
-private:
-  Result solve0(QICircuit const &c, std::vector<int> &sol);
 public:
-  static Result solve(QICircuit const &c, std::vector<int> &sol);
+  // Builds a problem by adding contexts with formulae.
+  void set(QIContext const &ctx) {
+    context = &ctx;
+  }
+  void parse(char const *fct) throw (ParseException);
+
+  // Solves the current problem and clears this Quantorizers state.
+  Result solve(std::vector<int> &sol);
 
-#line 66 "Quantorizer.hpp"
+#line 68 "Quantorizer.hpp"
 private:
   void parse();
 public:
@@ -75,7 +77,7 @@ enum {
   NAND = 260,
   NOR = 261,
   XNOR = 262,
-  IDENT = 263,
+  VAR = 263,
 };
 private:
 enum { YYINTERN = 264 };
diff --git a/interfaces/quantor/Quantorizer.ypp b/interfaces/quantor/Quantorizer.ypp
index a5affb8..e3a239f 100644
--- a/interfaces/quantor/Quantorizer.ypp
+++ b/interfaces/quantor/Quantorizer.ypp
@@ -1,14 +1,10 @@
 %header{
 #include <vector>
-#include <cctype>
-#include <cassert>
-
-#include <string.h>
+#include <map>
 
-#include "Quantor.h"
-#include "QICircuit.h"
 #include "QIContext.h"
 #include "ParseException.h"
+#include "Result.h"
 
 using namespace q2d::quantor;
 }
@@ -24,93 +20,73 @@ using namespace q2d::quantor;
  * @author Thomas B. Preußer <thomas.preusser@utexas.edu>
  */
 %class q2d::quantor::Quantorizer {
-  Quantor   quantor;
+
+  // Variable Bookkeeping
   unsigned  max_var;
-#ifndef NDEBUG
-  unsigned  max_named;
-#endif
 
-  std::vector<int>  clauses;
-  QIContext const  *context;
-  char      const  *formula;
+  typedef unsigned Variable;
+  std::map<Variable, unsigned>  varConfigs;
+  std::map<Variable, unsigned>  varInputs;
+  std::map<Variable, unsigned>  varNodes;
+
+  std::vector<unsigned>  varAux;
+  std::vector<int>       clauses;
+
+  // Current Parsing State
+  QIContext const *context;
+  char      const *formula;
 
 //- Life Cycle ---------------------------------------------------------------
-private:
+public:
   Quantorizer();
   ~Quantorizer();
 
-//- Problem Building ---------------------------------------------------------
+//- Parser Interface Methods -------------------------------------------------
 private:
-  template<typename IT>
-  void openScope(QuantorQuantificationType const  type, IT  vars);
-  void closeScope();
+  void error(std::string  msg);
+  unsigned nextToken(YYSVal &sval);
 
 //- Private Parser Helpers ---------------------------------------------------
 private:
+  unsigned getVar(std::string const &name);
   unsigned makeAuxiliary();
   void addClause(int const  a);
   void addClause(int const  a, int const  b);
   void addClause(int const  a, int const  b, int const  c);
 
-//- Parser Interface Methods -------------------------------------------------
-private:
-  void error(std::string  msg);
-  unsigned nextToken(YYSVal &sval);
-
 //- Usage Interface ----------------------------------------------------------
-private:
-  Result solve0(QICircuit const &c, std::vector<int> &sol);
 public:
-  static Result solve(QICircuit const &c, std::vector<int> &sol);
+  // Builds a problem by adding contexts with formulae.
+  void set(QIContext const &ctx) {
+    context = &ctx;
+  }
+  void parse(char const *fct) throw (ParseException);
+
+  // Solves the current problem and clears this Quantorizers state.
+  Result solve(std::vector<int> &sol);
 }
 
 %sval unsigned
 %impl {
 #include "Quantorizer.hpp"
 
-using namespace q2d::quantor;
+#include <cctype>
+#include <cassert>
+#include <string.h>
 
-//- Life Cycle ---------------------------------------------------------------
-inline Quantorizer::Quantorizer() : max_var(0), context(0), formula(0) {}
-inline Quantorizer::~Quantorizer() {}
-
-//- Problem Building ---------------------------------------------------------
-template<typename IT>
-void Quantorizer::openScope(QuantorQuantificationType const  type, IT  vars) {
-  quantor.scope(type);
-  for(unsigned const  var : vars) {
-    assert(var > 0);
-    if(var > max_var)  max_var = var;
-    quantor.add(var);
-  }
+extern "C" {
+#include "Quantor.h"
 }
-inline void Quantorizer::closeScope() { quantor.add(0); }
 
-//- Private Parser Helpers ---------------------------------------------------
-inline unsigned Quantorizer::makeAuxiliary() {
-  unsigned const  res = ++max_var;
-  quantor.add(res);
-  return  res;
-}
-inline void Quantorizer::addClause(int const  a) {
-  clauses.push_back(a);
-  clauses.push_back(0);
-}
-inline void Quantorizer::addClause(int const  a, int const  b) {
-  clauses.push_back(a);
-  clauses.push_back(b);
-  clauses.push_back(0);
-}
-inline void Quantorizer::addClause(int const  a, int const  b, int const  c) {
-  clauses.push_back(a);
-  clauses.push_back(b);
-  clauses.push_back(c);
-  clauses.push_back(0);
-}
+using namespace q2d::quantor;
+
+//- Life Cycle ---------------------------------------------------------------
+Quantorizer::Quantorizer() : max_var(0), context(0), formula(0) {}
+Quantorizer::~Quantorizer() {}
 
 //- Parser Interface Methods -------------------------------------------------
 inline void Quantorizer::error(std::string  msg) {
-  throw  ParseException(msg, *context);
+  throw  ParseException(msg, 0);
 }
 
 unsigned Quantorizer::nextToken(YYSVal &sval) {
@@ -141,31 +117,28 @@ unsigned Quantorizer::nextToken(YYSVal &sval) {
     if(isspace(c))  continue;
     if(isalpha(c) || (c == '_')) {
       char const *p = formula--;
-      while(isalnum(*p) || (*p == '_') || (*p == '/') || (*p == '-'))  p++;
+      while(isalnum(*p) || (c == '_') || (c == '-') || (c == '/'))  p++;
       unsigned const  len = p-formula;
       unsigned  res = 0;
       switch(len) {
       case 2:
-    if(strncmp(formula, "or", 2) == 0)  res = OR;
-    break;
+	if(strncmp(formula, "or", 2) == 0)  res = OR;
+	break;
       case 3:
-    if     (strncmp(formula, "and", 3) == 0)  res = AND;
-    else if(strncmp(formula, "xor", 3) == 0)  res = XOR;
-    else if(strncmp(formula, "nor", 3) == 0)  res = NOR;
-    else if(strncmp(formula, "not", 3) == 0)  res = NOT;
-    break;
+	if     (strncmp(formula, "and", 3) == 0)  res = AND;
+	else if(strncmp(formula, "xor", 3) == 0)  res = XOR;
+	else if(strncmp(formula, "nor", 3) == 0)  res = NOR;
+	else if(strncmp(formula, "not", 3) == 0)  res = NOT;
+	break;
       case 4:
-    if     (strncmp(formula, "nand", 4) == 0)  res = NAND;
-    else if(strncmp(formula, "xnor", 4) == 0)  res = XNOR;
-    break;
+	if     (strncmp(formula, "nand", 4) == 0)  res = NAND;
+	else if(strncmp(formula, "xnor", 4) == 0)  res = XNOR;
+	break;
       }
       if(res == 0) {
-	std::string  name(formula, len);
-	unsigned const  var = (*context)[name];
-	assert(var <= max_named);
-	if(var == 0)  error("Could not resolve variable \"" + name + '"');
+	unsigned const  var = getVar(std::string(formula, len));
 	sval = var;
-	res  = IDENT;
+	res  = VAR;
       }
       formula = p;
       return  res;
@@ -176,110 +149,165 @@ unsigned Quantorizer::nextToken(YYSVal &sval) {
   }
 }
 
+//- Private Parser Helpers ---------------------------------------------------
+unsigned Quantorizer::getVar(std::string const &name) {
+  Variable const  var = (*context)[name];
+  std::map<Variable, unsigned> *cat;
+  switch(context->typeOf(var)) {
+  case VariableType::CONFIG:  cat = &varConfigs; break;
+  case VariableType::INPUT:   cat = &varInputs;  break;
+  case VariableType::NODE:    cat = &varNodes;   break;
+  default: error("Unknown identifier: " + name);
+  }
+
+  // Check if variable is known already
+  auto const  v = cat->find(var);
+  if(v != cat->end())  return  v->second;
+
+  // Register new variable according to its type
+  return (*cat)[var] = ++max_var;
+}
+
+inline unsigned Quantorizer::makeAuxiliary() {
+  unsigned const  id = ++max_var;
+  varAux.push_back(id);
+  return  id;
+}
+
+inline void Quantorizer::addClause(int const  a) {
+  clauses.push_back(a);
+  clauses.push_back(0);
+}
+inline void Quantorizer::addClause(int const  a, int const  b) {
+  clauses.push_back(a);
+  clauses.push_back(b);
+  clauses.push_back(0);
+}
+inline void Quantorizer::addClause(int const  a, int const  b, int const  c) {
+  clauses.push_back(a);
+  clauses.push_back(b);
+  clauses.push_back(c);
+  clauses.push_back(0);
+}
+
 //- Public Usage Interface ---------------------------------------------------
-inline Result Quantorizer::solve0(QICircuit const &c, std::vector<int> &sol) {
-  // Quantifier Preamble
-  openScope(QUANTOR_EXISTENTIAL_VARIABLE_TYPE, c.configVars());
-  closeScope();
-  openScope(QUANTOR_UNIVERSAL_VARIABLE_TYPE,   c.inputVars());
-  closeScope();
-  openScope(QUANTOR_EXISTENTIAL_VARIABLE_TYPE, c.nodeVars());
-  // leave it open!
-#ifndef NDEBUG
-  max_named = max_var;
-#endif
-
-  // Parse in Component Specifications
-  for(QIContext const &ctx : c.contexts()) {
-    context = &ctx;
-    for(std::string const&  f : ctx.functions()) {
-      formula = f.c_str();
-      parse();
-    }
+void Quantorizer::parse(char const *fct) throw (ParseException) {
+  formula = fct;
+  try {
+    parse();
+  }
+  catch(ParseException &e) {
+    e.position(formula-fct);
+    throw;
   }
+}
+
+Result Quantorizer::solve(std::vector<int> &sol) {
+  q2d::quantor::Quantor         q;      // solver
+  std::map<unsigned, Variable>  confs;  // reverse map for configs
+
+  // Problem Building
+  q.scope(QUANTOR_EXISTENTIAL_VARIABLE_TYPE);
+  for(auto const &e : varConfigs) {
+    q.add(e.second);
+    confs.emplace(e.second, e.first);
+  }
+  varConfigs.clear();
+  q.add(0);
+
+  q.scope(QUANTOR_UNIVERSAL_VARIABLE_TYPE);
+  for(auto const &e : varInputs)  q.add(e.second);
+  varInputs.clear();
+  q.add(0);
+
+  q.scope(QUANTOR_EXISTENTIAL_VARIABLE_TYPE);
+  for(auto const &e : varNodes)  q.add(e.second);
+  varNodes.clear();
+  for(unsigned  v : varAux)  q.add(v);
+  varAux.clear();
+  q.add(0);
 
-  // Finish Problem Specification
-  closeScope();
-  for(int  lit : clauses)  quantor.add(lit);
+  for(int  lit : clauses)  q.add(lit);
+  clauses.clear();
 
   // Solve Problem
-  Result const  res = quantor.sat();
-  if(res == QUANTOR_RESULT_SATISFIABLE) {
-    int const *s = quantor.assignment();
-    while(*s)  sol.push_back(*s++);
+  Result const  res = q.sat();
+  if(res) {
+    auto const  end = confs.end();
+    for(int const *s = q.assignment(); *s; s++) {
+      auto const  it = confs.find(abs(*s));
+      if(it != end)  sol.push_back(*s < 0? -it->second : it->second);
+    }
   }
   return  res;
 }
 
-Result Quantorizer::solve(QICircuit const &c, std::vector<int> &sol) {
-  return  Quantorizer().solve0(c, sol);
-}
-
 } // impl
 
 %%
 %right NOT
 %left AND OR XOR NAND NOR XNOR
-%token IDENT
+%token VAR
 %start spec
 %%
-spec    : expr {
-	   addClause($1);
-          }
-        | expr '=' expr {
-           addClause( $1, -$3);
-           addClause(-$1,  $3);
-          }
-expr    : expr AND  expr {
+spec : expr {
+        addClause($1);
+       }
+     | expr '=' expr {
+        addClause( $1, -$3);
+        addClause(-$1,  $3);
+       }
+expr : expr AND  expr {
         unsigned const  res = makeAuxiliary();
         addClause( res, -$1, -$3);
         addClause(-res,  $1);
         addClause(-res,  $3);
         $$ = res;
-          }
-        | expr OR   expr {
+       }
+     | expr OR   expr {
         unsigned const  res = makeAuxiliary();
         addClause(-res,  $1, $3);
         addClause( res, -$1);
         addClause( res, -$3);
         $$ = res;
-          }
-        | expr XOR  expr {
+       }
+     | expr XOR  expr {
         unsigned const  res = makeAuxiliary();
         addClause(-res, -$1, -$3);
         addClause(-res,  $1,  $3);
         addClause( res, -$1,  $3);
         addClause( res,  $1, -$3);
         $$ = res;
-          }
-        | expr NAND expr {
+       }
+     | expr NAND expr {
         unsigned const  res = makeAuxiliary();
         addClause(-res, -$1, -$3);
         addClause( res,  $1);
         addClause( res,  $3);
         $$ = res;
-          }
-        | expr NOR  expr {
+       }
+     | expr NOR  expr {
         unsigned const  res = makeAuxiliary();
         addClause( res,  $1, $3);
         addClause(-res, -$1);
         addClause(-res, -$3);
         $$ = res;
-          }
-        | expr XNOR expr {
+       }
+     | expr XNOR expr {
         unsigned const  res = makeAuxiliary();
         addClause( res, -$1, -$3);
         addClause( res,  $1,  $3);
         addClause(-res, -$1,  $3);
         addClause(-res,  $1, -$3);
         $$ = res;
-          }
-        | prim           { $$ = $1; }
-prim    : IDENT          { $$ = $1; }
-    | '(' expr ')'   { $$ = $2; }
-    | NOT prim {
+       }
+     | prim         { $$ = $1; }
+
+prim : VAR          { $$ = $1; }
+     | '(' expr ')' { $$ = $2; }
+     | NOT prim {
         unsigned const  res = makeAuxiliary();
         addClause( res,  $2);
         addClause(-res, -$2);
         $$ = res;
-      }
+       }