Method updateFalse

contribs/qecode/WorkManager.cc:309–345

}

void WorkManager::updateFalse(Strategy s) { // called when s is false
  // cout<<"  UF on ";
  // vector<int> hihi = s.getPosition();
  // if (hihi.empty()) cout<<"empty";
  // for (int i=0;i< hihi.size();i++) cout<<hihi[i]<<" ";
  // cout<<endl;

  trashWorks(s.getPosition());
  if (s.isDummy()) {
    return;
  }
  Strategy father=s.getFather();

  if (s.quantifier()) { // if s is universal, its father is false
    // cout<<"  UF A";
    if (father.isDummy()) { // if father is dummy, it is the root of the strategy. We must cut all its children and ad a false node.
      // cout<<" father root "<<endl;
      while (father.degree() != 0) {
	father.detach(father.degree()-1);
      }
      father.attach(Strategy::SFalse());
    }
    // cout<<endl;
    updateFalse(s.getFather());
  }
  else { // if s is existential, it it detached from its father
    // cout<<"  UF E ";
    father.detach(s);
    if (father.degree() == 0) {
      // cout<<" father false"<<endl;
      updateFalse(father);
    }
    else {
      // cout<<" father still not false"<<endl;
    }
  }
}


void WorkManager::trashWorks(vector<int> prefix) {