[mathprog] version 2

  • From: Noam Petrank <buga@xxxxxxxxxxxxx>
  • To: mathprog@xxxxxxxxxxxxx
  • Date: Thu, 10 Oct 2002 14:27:37 +0200 (IST)

the algorithm is debuged.
It is possible that I missed some minor bugs. If you find any, let me 
know.



#include "SentenceTree.h"
#include "Sentence.h"
#include <queue>
#include <map>
#include <list>
#include <utility>
#include <sstream>
using namespace std;

const string SentenceTree::PRE_STRING = "buga";
const int SentenceTree::checkSequence = 1;


SentenceTree::SentenceTree(list<Sentence*>* li) {
  //assuming that the list doesn't contain two sentences in the form F, notF.
  root = new Node();
  for (list<Sentence*>::iterator it = li->begin(); it != li->end(); it++) {
    pair<Sentence*, bool>* myPair = new pair<Sentence*, bool>(*it, false);
    root->data->push_back(myPair);
  }

}

SentenceTree::~SentenceTree() {
  delete root;
}

string SentenceTree::toString() const {
  if (root)
    return root->toString();
  else
    return "";
}

string SentenceTree::getNewIndex() {
  static int varIndex =0;
  varIndex++;
  stringstream s;
  s << PRE_STRING << varIndex;
  return s.str();
}

bool SentenceTree::buildTree() {
  treeQueue forAllFirstTimeQueue;
  treeQueue expressQueue;
  treeQueue fastQueue;
  treeQueue slowQueue;
  queue<Node*> forAllQueue;

  for (list<pair<Sentence*, bool>* >::iterator it = root->data->begin(); it != 
root->data->end(); it++) {
    insertToQueue (forAllFirstTimeQueue ,expressQueue, fastQueue, slowQueue, 
*it, root);       
  }
  int check = 0;
  while (!forAllFirstTimeQueue.empty() || !expressQueue.empty() ||
          
         !fastQueue.empty() || !slowQueue.empty()  ||!forAllQueue.empty())  {
    if (!root->open) 
      return false;
    check ++;
    if (check == checkSequence) {
      check = 0;
      if (checkFull())
        return true;
    }

    cout<<"buga"<<endl;
    flush(cout);
    cout << "party1" << endl;
    flush(cout);
    if (forAllFirstTimeQueue.empty()==false)  {
      cout << "party2" << endl;
      flush(cout);
      pair<pair<Sentence*,bool>*, Node*> &current = 
forAllFirstTimeQueue.front();
      forAllFirstTimeQueue.pop();
      cout << "party3" << endl;
      flush(cout);
      if (current.second->open) {
        cout << "party4" << endl;
        flush(cout);
        dischargeFTAQueue (current.first->first, current.second,
                           forAllFirstTimeQueue, expressQueue,
                           fastQueue, slowQueue, forAllQueue);
        current.first->second = true;
      }
    }

    else if (expressQueue.empty() == false) {
      pair<pair<Sentence*,bool>*, Node*> &current = expressQueue.front();
      fastQueue.pop();
      if (current.second->open) {
        dischargeExpressQueue (current.first->first, current.second, 
forAllFirstTimeQueue,
                               expressQueue, fastQueue, slowQueue);
        current.first->second = true;
      }
    }

    else if (fastQueue.empty()==false) {
      cout << "ata toen" << endl;
      flush(cout);
      pair<pair<Sentence*,bool>*, Node*> &current = fastQueue.front();
      fastQueue.pop();
      cout << "ata toen2" << endl;
      flush(cout);
      if (current.second->open) {
        dischargeFastQueue (current.first->first, current.second, 
forAllFirstTimeQueue,
                            expressQueue, fastQueue, slowQueue);
        current.first->second = true;
      }
    }

    else if (slowQueue.empty() == false)  {
      pair<pair<Sentence*,bool>*, Node*> &current = slowQueue.front();
      slowQueue.pop();
      if (current.second->open) {
        dischargeSlowQueue (current.first->first, current.second, 
forAllFirstTimeQueue,
                            expressQueue, fastQueue, slowQueue);
        current.first->second = true;
      }
    }

    else if (forAllQueue.empty() == false) {
      Node* n = forAllQueue.front();
      forAllQueue.pop();
      dischargeForAllQueue (n, forAllFirstTimeQueue,
                            expressQueue, fastQueue, slowQueue);
    }
  }
  
  return root->open;
}

void SentenceTree::dischargeFTAQueue (Sentence* s, Node* n,
                                      treeQueue &allQueue,
                                      treeQueue &eQueue,
                                      treeQueue &fQueue,
                                      treeQueue &sQueue,
                                      queue<Node*> &forAllQueue) {
        
  QuantifierSentence* casts = dynamic_cast<QuantifierSentence*>(s);
  list<const ConstantSentence*>* conlist = getBranchConstants (n);
  cout << "preyoohoo" << endl;
  flush(cout);
  if (conlist != 0) {
    cout<<"yoooho"<<endl;
    flush(cout);
    while (conlist->empty() == false) {
      Sentence* newS = casts->getSentence()->clone( casts->getVariable(), 
conlist->front());
      if (!newS) {
        cout<<"ahhh"<<endl;
        flush(cout);
      }
      conlist->pop_front();
      pair<Sentence*, bool>* p = new pair<Sentence*, bool>(newS, false);
      n->data->push_back(p);
      checkBranch(newS, n);
      insertToQueue(allQueue, eQueue, fQueue, sQueue, p, n);
    }
    delete conlist;
  }
  else {
    string name = getNewIndex();
    ConstantSentence* newCon = new ConstantSentence (name);
    Sentence* newS = casts->getSentence()->clone( casts->getVariable(), newCon);
    pair<Sentence*, bool>* p = new pair<Sentence*,bool>(newS, false);
    n->data->push_back(p);
    checkBranch(p->first, n);
    insertToQueue(allQueue, eQueue, fQueue, sQueue, p, n);
  }
  n->forAllList->addSentence(casts);
  forAllQueue.push(n);
}


void SentenceTree::dischargeExpressQueue (Sentence* s, Node* n,
                                          treeQueue &allQueue,
                                          treeQueue &eQueue,
                                          treeQueue &fQueue,
                                          treeQueue &sQueue) {
  cout<<"reached "<<endl;
  flush(cout);
  int form = whichSentence (s);
        
  if (form == 12) {
    cout<<"reched1"<<endl;
    flush(cout);
   
    QuantifierSentence* existsS = dynamic_cast<QuantifierSentence*>(s);
    const TruthValueSentence* wished = existsS->getSentence();
    const VariableSentence* var = existsS->getVariable();
    Node* cur = n;
    cout<<"reched1"<<endl;
    flush(cout);
    while (cur != 0) {
      for (list<pair<Sentence*, bool>*>::iterator it = cur->data->begin(); it 
!= cur->data->end(); it++) {
        cout<<"buga buga"<<endl;
        flush(cout);
        pair<bool, ConstantSentence*> p = 
wished->equalsUpToSubstitution((*it)->first, var);
        if (p.first) 
          break;
      }
      cur = cur->parent;
    }
    if (cur == 0) { //failed finding the right sentence.
      string name = getNewIndex();
      ConstantSentence* newCon = new ConstantSentence (name);
      Sentence* newS = wished->clone (var, newCon);
      pair<Sentence*, bool>* p = new pair<Sentence*,bool>(newS, false);
      n->data->push_back(p);
      checkBranch(newS, n);
      insertToQueue(allQueue, eQueue, fQueue, sQueue, p, n);
      insertConstantToContainers (n, newCon);
    }
  }

  else if (form == 16) {
    EqualitySentence* es = dynamic_cast<EqualitySentence*>(s);
    const ConstantSentence* c1 = dynamic_cast<const 
ConstantSentence*>(es->getFirst());
    const ConstantSentence* c2 = dynamic_cast<const 
ConstantSentence*>(es->getSecond());
    Node* cur = n;
    while (cur != 0) {
      for (list<pair<Sentence*, bool>*>::iterator it = cur->data->begin(); it 
!= cur->data->end(); it++) {
        if ((*it)->first->containsConstant(c1)  ) {
          list<Sentence*>* li =
            (*it)->first->getAllPossibleSubstitutions(c1, c2);

          while (li->empty() == false)  {
            pair<Sentence*, bool>* p = new pair <Sentence*, bool>(li->front(), 
false);
            li->pop_front();
            cur->data->push_back(p);
            insertToQueue(allQueue, eQueue, fQueue, sQueue, p, n);
          }
          checkBranch(li, n);
          delete li;
        }
                                
        if ((*it)->first->containsConstant(c2)  ) {
          list<Sentence*>* li = (*it)->first->getAllPossibleSubstitutions(c2, 
c1);
          while (li->empty() == false)  {
            pair<Sentence*, bool>* p = new pair <Sentence*, bool>(li->front(), 
false);
            li->pop_front();
            cur->data->push_back(p);
            insertToQueue(allQueue, eQueue, fQueue, sQueue, p, n);
          }
          checkBranch(li, n);
          delete li;
        }
      }
      cur = cur->parent;
    }
  }
}

void SentenceTree::dischargeFastQueue (Sentence* s, Node* n,
                                       treeQueue &allQueue,
                                       treeQueue &eQueue,
                                       treeQueue &fQueue,
                                       treeQueue &sQueue)  {

  int form = whichSentence (s);
                                
  if (form == 1) {
    OperatorSentence* os = dynamic_cast<OperatorSentence*>(s);
    Sentence* s1 = os->getFirstOperand()->clone();
    Sentence* s2 = os->getSecondOperand()->clone();
    cout<<"ff"<<endl;
    flush(cout);
    insertToLeaves (allQueue, eQueue, fQueue, sQueue, s1, s2, n);
  }

  else if (form == 7) {
    OperatorSentence* os = dynamic_cast<OperatorSentence*>(s);
    const OperatorSentence* sMain =  dynamic_cast<const 
OperatorSentence*>(os->getFirstOperand());
    Sentence* s1 = new OperatorSentence(OperatorSentence::NOT, 
sMain->getFirstOperand()->clone());
    Sentence* s2 = new OperatorSentence(OperatorSentence::NOT, 
sMain->getSecondOperand()->clone());
    insertToLeaves (allQueue, eQueue, fQueue, sQueue, s1, s2, n);
  }

  else if (form == 8) {
    OperatorSentence* os = dynamic_cast<OperatorSentence*>(s);
    const OperatorSentence* sMain =  dynamic_cast<const 
OperatorSentence*>(os->getFirstOperand());
    TruthValueSentence* s1 = sMain->getFirstOperand()->clone();
    Sentence* s2 = new OperatorSentence(OperatorSentence::NOT, 
sMain->getSecondOperand()->clone());
                
    insertToLeaves (allQueue, eQueue, fQueue, sQueue, s1, s2, n);
  }

  else if (form == 9) {
    OperatorSentence* os = dynamic_cast<OperatorSentence*>(s);
    const OperatorSentence* sMain =  dynamic_cast<const 
OperatorSentence*>(os->getFirstOperand());
    TruthValueSentence* s2 = sMain->getFirstOperand()->clone();
    Sentence* s1 = new OperatorSentence(OperatorSentence::NOT, 
sMain->getSecondOperand()->clone());
                
    insertToLeaves (allQueue, eQueue, fQueue, sQueue, s1, s2, n);
  }

  else if (form == 10) {
    OperatorSentence* os = dynamic_cast<OperatorSentence*>(s);
    const OperatorSentence* scast =  dynamic_cast<const 
OperatorSentence*>(os->getFirstOperand());
    insertToLeaves (allQueue, eQueue, fQueue, sQueue, scast->clone(), n);
  }

  else if (form == 13) {
    cout << "I'm here!!" << endl;
    flush(cout);
    OperatorSentence* os = dynamic_cast<OperatorSentence*>(s);
    const QuantifierSentence* qs = dynamic_cast<const 
QuantifierSentence*>(os->getFirstOperand()->clone());
    OperatorSentence* no = new OperatorSentence (OperatorSentence::NOT, 
qs->getSentence()->clone());
    QuantifierSentence* newSentence = new 
QuantifierSentence(QuantifierSentence::EXISTS, 
dynamic_cast<VariableSentence*>(qs->getVariable()->clone()), no);
    cout << "I'm here2" << endl;
    flush(cout);
    insertToLeaves (allQueue, eQueue, fQueue, sQueue, newSentence, n);
    cout << "I'm here3" << endl;
    flush(cout);
  }

  else if (form == 14) {
    cout<<"chikamakomako"<< endl;
    flush(cout);
    OperatorSentence* os = dynamic_cast<OperatorSentence*>(s);
    const QuantifierSentence* qs = dynamic_cast<const 
QuantifierSentence*>(os->getFirstOperand());
    OperatorSentence* no = new OperatorSentence (OperatorSentence::NOT, 
qs->getSentence()->clone());
    QuantifierSentence* newSentence = new 
QuantifierSentence(QuantifierSentence::FORALL, 
dynamic_cast<VariableSentence*>(qs->getVariable()->clone()), no);

    insertToLeaves (allQueue, eQueue, fQueue, sQueue, newSentence, n);

  }
}

void SentenceTree::dischargeSlowQueue (Sentence* s, Node* n,
                                       treeQueue &allQueue,
                                       treeQueue &eQueue,
                                       treeQueue &fQueue,
                                       treeQueue &sQueue) {
  int form = whichSentence (s);

  if (form == 2)  {
    OperatorSentence* os = dynamic_cast<OperatorSentence*>(s);
    TruthValueSentence* s1 = os->getFirstOperand()->clone();
    TruthValueSentence* s2 = os->getSecondOperand()->clone();
                
    createLeaves (allQueue, eQueue, fQueue, sQueue, s1, s2, n);

  }

  else if (form == 3)  {
    OperatorSentence* os = dynamic_cast<OperatorSentence*>(s);
    OperatorSentence* s1 = new OperatorSentence (OperatorSentence::NOT, 
os->getFirstOperand()->clone());
    Sentence* s2 = os->getSecondOperand()->clone();
    cout<<"qq";
    flush(cout);
    createLeaves (allQueue, eQueue, fQueue, sQueue, s1, s2, n);
  }

  else if (form == 4)  {
    OperatorSentence* os = dynamic_cast<OperatorSentence*>(s);
    Sentence* s1 = os->getFirstOperand()->clone();
    OperatorSentence* s2 = new OperatorSentence (OperatorSentence::NOT, 
os->getSecondOperand()->clone());
                
    createLeaves (allQueue, eQueue, fQueue, sQueue, s1, s2, n);
  }

  else if (form == 5)  {
    OperatorSentence* os = dynamic_cast<OperatorSentence*>(s);
    Sentence* s1 = os->getFirstOperand()->clone();
    Sentence* s2 = os->getSecondOperand()->clone();
    OperatorSentence* s3 = new OperatorSentence (OperatorSentence::NOT, 
os->getFirstOperand()->clone());
    OperatorSentence* s4 = new OperatorSentence (OperatorSentence::NOT, 
os->getSecondOperand()->clone());

    createLeaves (allQueue, eQueue, fQueue, sQueue, s1, s2, s3, s4, n);

  }

  else if (form == 6)  {
    OperatorSentence* os = dynamic_cast<OperatorSentence*>(s);
    const OperatorSentence* sMain = dynamic_cast<const OperatorSentence*>( 
os->getFirstOperand());
    OperatorSentence* s1 = new OperatorSentence (OperatorSentence::NOT, 
sMain->getFirstOperand()->clone());
    OperatorSentence* s2 = new OperatorSentence (OperatorSentence::NOT, 
sMain->getSecondOperand()->clone());
                
    createLeaves (allQueue, eQueue, fQueue, sQueue, s1, s2, n);

  }

  else if (form == 18)  {
    OperatorSentence* os = dynamic_cast<OperatorSentence*>(s);
    const OperatorSentence* sMain = dynamic_cast<const 
OperatorSentence*>(os->getFirstOperand());
    TruthValueSentence* s1 = sMain->getFirstOperand()->clone();
    OperatorSentence* s2 = new OperatorSentence (OperatorSentence::NOT, 
sMain->getSecondOperand()->clone());
    OperatorSentence* s3 = new OperatorSentence (OperatorSentence::NOT, s1);
    TruthValueSentence* s4 = sMain->getSecondOperand()->clone();

    createLeaves (allQueue, eQueue, fQueue, sQueue, s1, s2, s3, s4, n);
  }
}

void SentenceTree::dischargeForAllQueue (Node* n, 
                                         treeQueue &allQueue,
                                         treeQueue &eQueue,
                                         treeQueue &fQueue,
                                         treeQueue &sQueue) {

  ForAllContainer* all = n->forAllList;
  list<QuantifierSentence*>* li = all->getSentences();

  for (map<Node* ,std::list<ConstantSentence*>*>::iterator it = all->begin(); 
it!=all->end(); it++) {
    list<Sentence*>* newS = new list<Sentence*>;
    list<ConstantSentence*>* conList = (*it).second;
    for (list<QuantifierSentence*>::iterator i = li->begin(); i != li->end(); 
i++ ) {
      const TruthValueSentence* s = (*i)->getSentence();
      const VariableSentence* var = (*i)->getVariable();
                        
      for (list<ConstantSentence*>::iterator j = conList->begin(); j != 
conList->end(); j++ )  {
        Sentence* cloned = s->clone(var, (*j));
        newS->push_back(cloned);
      }
    }

    insertToLeaves (allQueue, eQueue, fQueue, sQueue, newS, (*it).first);
    delete newS;
    delete conList;
  }
  all->initialaize();
}

/*
  this method checks what is the kind of a given sentence: 
  1 - A and B
  2 - A or B
  3 - A -> B
  4 - A <-B
  5 - A <-> B
  6 - not (A and B)
  7 - not (A or B)
  8 - not (A -> B)
  9 - not (A <- B)
  10 - not (not (A))
  11 - For All x f(x)
  12 - Exsists y f(y)
  13 - not For All x f(x)
  14 - not exsists y f(y)
  15 - worldvalue
  16 - A = B
  17 - not (worldvalue)
  18 - not (A <-> B)
  19 - not (A = B)
  20 - predicate or not predictae
  21 - ERROR!
  p.s - this method is baaaaaa, and I'm not responsible for its uglyness,
  there was no other way.
*/
int SentenceTree::whichSentence(Sentence* check) {
  
  const OperatorSentence* os;
  const WorldValueSentence* ws;
  const QuantifierSentence* qs;
  const PredicateSentence* ps;
  const EqualitySentence* es;
  if (!check)
    return 21;
  if ((os = dynamic_cast<const OperatorSentence*>(check))) {
    int op = os->getOp();
    switch (op) {
      case 1: return 1;
      case 2: return 2;
      case 4: return 3;
      case 5: return 4;
      case 6: return 5;
      case 3: {
        const Sentence* first = os->getFirstOperand();
        const OperatorSentence* tos;
        const WorldValueSentence* tws;
        const QuantifierSentence* tqs;
        const PredicateSentence* tps;
        if ((tos = dynamic_cast<const OperatorSentence*>(first))) {
          if(tos->getOp() == 1)
            return 6;
          if(tos->getOp() == 2)
            return 7;
          if(tos->getOp() == 3)
            return 10;
          if(tos->getOp() == 4)
            return 8;
          if(tos->getOp() == 5)
            return 9;
          if(tos->getOp() == 6)
            return 18;
        }
        if ((tqs = dynamic_cast<const QuantifierSentence*>(first))) {
          if(tqs->getQuantifier() == 1)
            return 13;
          if(tqs->getQuantifier() == 2)
            return 14;
        }
        if ((tws = dynamic_cast<const WorldValueSentence*>(first))) {
          return 17;
        }
        if ((tps = dynamic_cast<const PredicateSentence*>(first)))
          return 20;
        else
          return 19;
      }
    }
  }
  if ((ws = dynamic_cast<const WorldValueSentence*>(check))) 
    return 15;
  if ((ps = dynamic_cast<const PredicateSentence*>(check)))
    return 20;
  if ((qs = dynamic_cast<const QuantifierSentence*>(check))) {
    if (qs->getQuantifier() == 1)
      return 11;
    if (qs->getQuantifier() == 2)
      return 12;
  }
  if ((es = dynamic_cast<const EqualitySentence*>(check))) {
    return 16;
  }
  return 21;
}

void SentenceTree::insertToQueue (treeQueue &allFTQueue,
                                  treeQueue &eQueue,
                                  treeQueue &fQueue,
                                  treeQueue &sQueue,
                                  pair<Sentence*, bool>* p , Node* n) {
        
  int ch = whichSentence (p->first);
  if (p->first == 0) {
    cout << "p->first is null for goose's sake!" << endl;
    flush(cout);
  }
  cout << "ch is : " << ch << endl;
  flush(cout);
  if (ch == 16 || ch == 12)
    eQueue.push(pair<pair<Sentence*, bool>*, Node*>(p,n));
  else if (ch == 1 || ch == 7 || ch == 8 || ch == 9 || ch == 10 ||  ch == 13 || 
ch == 14 )
    fQueue.push(pair<pair<Sentence*, bool>*, Node*>(p,n));
  else if (ch == 2 || ch == 3 || ch == 4 || ch == 5 || ch == 6 || ch ==18)
    sQueue.push(pair<pair<Sentence*, bool>*, Node*>(p,n));
  else if (ch == 11) {
    cout<<"godel"<<endl;
    flush(cout);
    allFTQueue.push(pair<pair<Sentence*, bool>*, Node*>(p,n));
    cout << "godel, eat this!" << endl;
    flush(cout);
  }
 else
    p->second = true;


}

void SentenceTree::insertToLeaves (treeQueue &allFTQueue,
                                   treeQueue &eQueue,
                                   treeQueue &fQueue,
                                   treeQueue &sQueue,
                                   Sentence* first, Sentence* second, Node* n) 
{ 

  if (n->left) {
    if (n->left->open)
      insertToLeaves(allFTQueue, eQueue, fQueue, sQueue, first, second, 
n->left);                       
  }
        
  if (n->right) {
    if (n->right->open)
      insertToLeaves(allFTQueue, eQueue, fQueue, sQueue, first, second,  
n->right);
  }
        
  else {

    pair<Sentence*, bool>* p1 = new pair<Sentence*, bool>(first, false);
    pair<Sentence*, bool>* p2 = new pair<Sentence*, bool>(second, false);
    n->data->push_back(p1);
    n->data->push_back(p2);
    insertToQueue (allFTQueue, eQueue, fQueue, sQueue, p1, n);
    insertToQueue (allFTQueue, eQueue, fQueue, sQueue, p2, n);
    checkBranch(first, second, n);
  }

}

void SentenceTree::createLeaves (treeQueue &allFTQueue,
                                 treeQueue &eQueue,
                                 treeQueue &fQueue,
                                 treeQueue &sQueue,
                                 Sentence* first, Sentence* second, Node* n) { 
  if (n->left) {
    if (n->left->open)
      createLeaves(allFTQueue, eQueue, fQueue, sQueue, first, second, n->left); 
                
  }
        
  if (n->right) {
    if (n->right->open)
      createLeaves (allFTQueue, eQueue, fQueue, sQueue, first, second,  
n->right);
  }
        
  else {
    Node* leftChild = new Node();
    leftChild->parent = n;
    n->left = leftChild;
    pair<Sentence*, bool>* p1 = new pair<Sentence*, bool>(first, false);
    leftChild->data->push_back(p1);

    Node* rightChild = new Node();
    rightChild->parent = n;
    n->right = rightChild;
    pair<Sentence*, bool>* p2 = new pair<Sentence*, bool>(second, false);
    rightChild->data->push_back(p2);

    checkBranch(first, leftChild);
    checkBranch(second, rightChild);
    insertToQueue(allFTQueue, eQueue, fQueue, sQueue, p1, leftChild);
    insertToQueue(allFTQueue, eQueue, fQueue, sQueue, p2, rightChild);
  }
}

void SentenceTree::createLeaves (treeQueue &allFTQueue,
                                 treeQueue &eQueue,
                                 treeQueue &fQueue,
                                 treeQueue &sQueue,
                                 Sentence* first, Sentence* second, Sentence* 
third,
                                 Sentence* forth, Node* n) { 

  if (n->left) {
    if (n->left->open)
      createLeaves(allFTQueue, eQueue, fQueue, sQueue, first, second, third, 
forth, n->left);
  }
        
  if (n->right) {
    if (n->right->open)
      createLeaves (allFTQueue, eQueue, fQueue, sQueue, first, second, third,
                    forth,  n->right);
  }
        
  else {
    Node* leftChild = new Node();
    leftChild->parent = n;
    n->left = leftChild;
    pair<Sentence*, bool>* p1 = new pair<Sentence*, bool>(first, false);
    pair<Sentence*, bool>* p2 = new pair<Sentence*, bool>(second, false);
    leftChild->data->push_back(p1);
    leftChild->data->push_back(p2);

    Node* rightChild = new Node();
    rightChild->parent = n;
    n->right = rightChild;
    pair<Sentence*, bool>* p3 = new pair<Sentence*, bool>(third, false);
    pair<Sentence*, bool>* p4 = new pair<Sentence*, bool>(forth, false);
    rightChild->data->push_back(p3);
    rightChild->data->push_back(p4);

    checkBranch(first, second, leftChild);
    checkBranch(third, forth, rightChild);

    insertToQueue(allFTQueue, eQueue, fQueue, sQueue, p1, leftChild);
    insertToQueue(allFTQueue, eQueue, fQueue, sQueue, p2, leftChild);
    insertToQueue(allFTQueue, eQueue, fQueue, sQueue, p3, rightChild);
    insertToQueue(allFTQueue, eQueue, fQueue, sQueue, p4, rightChild);
  }
}

void SentenceTree::insertToLeaves (treeQueue &allFTQueue,
                                   treeQueue &eQueue,
                                   treeQueue &fQueue,
                                   treeQueue &sQueue,
                                   Sentence* first, Node* n) { 
  if (n->left) {
    if (n->left->open)
      insertToLeaves(allFTQueue, eQueue, fQueue, sQueue, first, n->left);       
                
  }
        
  if (n->right) {
    if (n->right->open)
      insertToLeaves (allFTQueue, eQueue, fQueue, sQueue, first,  n->right);
  }
        
  else {
    pair<Sentence*, bool>* p1 = new pair<Sentence*, bool>(first, false);
    n->data->push_back(p1);
    cout<<"u"<<endl;
    checkBranch(first, n);
    insertToQueue(allFTQueue, eQueue, fQueue, sQueue, p1, n);
  }
}

void SentenceTree::insertToLeaves(treeQueue &allFTQueue,
                                  treeQueue &eQueue,
                                  treeQueue &fQueue,
                                  treeQueue &sQueue,
                                  list<Sentence*>* li, Node* n) {
  if (n->left) {
    if (n->left->open)
      insertToLeaves(allFTQueue, eQueue, fQueue, sQueue, li, n->left);          
        
  }
        
  if (n->right) {
    if (n->right->open)
      insertToLeaves (allFTQueue, eQueue, fQueue, sQueue, li,  n->right);
  }
        
  else {
    for (list<Sentence*>::iterator it = li->begin(); it != li->end(); it++) {
      pair<Sentence*, bool>* myPair = new pair<Sentence*, bool>(*it, false);
      n->data->push_back(myPair);
      insertToQueue (allFTQueue, eQueue, fQueue, sQueue, myPair, n);
    }
    checkBranch(li, n);
  }
}

/*
 This method gets a leaf node, and two sentences. preform two tests:
 first, if the sentences are in the form of "not A=A",
 second, if there is sentence which is a contradiction to it.
 If there is a contradiction, closes the branch.
*/

void SentenceTree::checkBranch (Sentence* s1, Sentence* s2, Node* n) {
  if (isNotEqual(s2) || isNotEqual(s1))
    closeBranch(n);
 
  else {
    Node* par = n;
    while (par!=0) {
      for (list<pair<Sentence*, bool>*>::iterator it = par->data->begin(); it 
!= par->data->end(); it++) {
        if (isContra((*it)->first ,s1)) {
          closeBranch (n);
          break;
        }
      }
      par = par->parent;
    }
  }
}



void SentenceTree::checkBranch (Sentence* s, Node* n) {
  if (isNotEqual(s))
    closeBranch(n);

  else {
    Node* par = n;
    while (par!=0) {
      for (list<pair<Sentence*, bool>*>::iterator it = par->data->begin(); it 
!= par->data->end(); it++) {
        if (isContra((*it)->first ,s)) {
          cout<<"q"<<endl;
          closeBranch (n);
          break;
        }
      }
      par = par->parent;
    }
  }
}

void SentenceTree::checkBranch (list<Sentence*>* li, Node* n) {
  for (list<Sentence*>::iterator it = li->begin(); it !=li->end(); it++)  {
    if (isNotEqual(*it)) {
      closeBranch(n);
      break;
    }
  }
        
  for (list<Sentence*>::iterator i = li->begin(); i !=li->end(); i++)  {
    for (list<Sentence*>::iterator j = i; j !=li->end(); j++)  {
      if (isContra((*i), (*j))) {
        closeBranch(n);
        break;
      }
    }
  }
  Sentence* s = li->front();
  Node* par = n;
  while (par!=0) {
    for (list<pair<Sentence*, bool>*>::iterator it = par->data->begin(); it != 
par->data->end(); it++) {
      if (isContra((*it)->first ,s)) {
        closeBranch (n);
        break;
      }
    }
    par = par->parent;
  }
}


/*
This method check if two sentences are a contradiction, meaning, in the 
form: F, not F
If so, returns true.
*/

bool SentenceTree::isContra (Sentence* first, Sentence* second) {
  OperatorSentence* os;
  if ((os = dynamic_cast<OperatorSentence*>(first))) {
    if ((os->getOp() == 3)) {
      cout<<"yonatan"<< first->toString()<<endl;
      flush(cout);
      if (*(os->getFirstOperand()) == *second) {
        cout<<"noam"<<endl;
        return true;
      }
    }
  }
        
  const OperatorSentence* os2;
  if ((os2 = dynamic_cast<const OperatorSentence*>(second))) {
    if ((os2->getOp() == 3)) {
      cout<<"maybe not"<<endl;
      if ((*first) == (*(os2->getFirstOperand())))
        return true;
    }
  }

  return false;
}

/*
This method gets a pointer to a leaf node, marks it as close, and
iterates on its branch (closes it, if necessery).
*/

void SentenceTree::closeBranch (Node* n) {
  n->open = false;
  Node* par = n->parent;
  while (par !=0) {
    if (par->left->open == false && par->right->open == false) {
      par->open = false;
      par = par->parent;
    }
    else
      break;                    
  }
}

/*
checks if a given sentence is in the form not (A = A)
*/


bool SentenceTree::isNotEqual(Sentence* s) {
  if (whichSentence(s) == 19) {
    OperatorSentence* os = dynamic_cast<OperatorSentence*>(s);
    const EqualitySentence* es = dynamic_cast<const 
EqualitySentence*>(os->getFirstOperand());
    if (*(es->getFirst()) == *(es->getSecond()))
      return true;
  }
  return false;
}

list<const ConstantSentence*>* SentenceTree::getBranchConstants (Node* n) {
  Node* cur = n;
  list<const ConstantSentence*>* returnVal = new list<const ConstantSentence*>;
  while (cur!=0)  {
    for (list<pair<Sentence*, bool>*>::iterator it = cur->data->begin(); it != 
cur->data->end(); it++ )  {
      list<const ConstantSentence*>* tmp = getConstants((*it)->first);
      if (tmp!=0)       {
        returnVal->splice(returnVal->end() , *tmp);
        delete tmp;
      }
    }
    cur = cur->parent;
  }
  return returnVal;
}

list<const ConstantSentence*>* SentenceTree::getConstants(const Sentence* a) {
  const OperatorSentence* os;
  const PredicateSentence* ps;
  const QuantifierSentence* qs;
  const ConstantSentence* cs;
  const FunctionSentence* fs;
  const VariableSentence* vs;
  const EqualitySentence* es;

  if ((os = dynamic_cast<const OperatorSentence*>(a))) {
    if ((os->getOp() !=3))  {
      list<const ConstantSentence*>* s1 = getConstants(os->getFirstOperand());
      list<const ConstantSentence*>* s2 = getConstants(os->getSecondOperand());
      if (s1 != 0)  {
        if (s2!=0)  {
          s1->splice(s1->end(), *s2);
          delete s2;
          return s1;
        }
        else 
          return s1;
      }
      return 0;
    }
    else 
      return getConstants(os->getFirstOperand());
        
  }
        
  if ((ps = dynamic_cast<const PredicateSentence*>(a))) {
    const list<WorldValueSentence*>* li = ps->getParameters();
    list<const ConstantSentence*>* returnVal = new list<const 
ConstantSentence*> ;
    for (list<WorldValueSentence*>::const_iterator it = li->begin(); it != 
li->end() ; it++ )   {
      list<const ConstantSentence*>* tmp = getConstants((*it));
      if (tmp!=0)
        returnVal->splice(returnVal->end(), *tmp);
      delete tmp;
    }
    return returnVal;
    delete li;
  }
  if ((qs = dynamic_cast<const QuantifierSentence*>(a))) {
    return getConstants(qs->getSentence());
  }
  if ((cs = dynamic_cast<const ConstantSentence*>(a))) {
    list<const ConstantSentence*>* li = new list<const ConstantSentence*>;
    li->push_back(cs);
    return li;
  }
  if ((fs = dynamic_cast<const FunctionSentence*>(a))) {
    const list<WorldValueSentence*>* li = fs->getParameters();
    list<const ConstantSentence*>* returnVal = new list<const 
ConstantSentence*> ;
    for (list<WorldValueSentence*>::const_iterator it = li->begin(); it != 
li->end() ; it++ )   {
      list<const ConstantSentence*>* tmp = getConstants((*it));
      if (tmp!=0)
        returnVal->splice(returnVal->end(), *tmp);
      delete tmp;
    }
    return returnVal;
  }
  if ((vs = dynamic_cast<const VariableSentence*>(a))) {
    return 0;
  }
  if ((es = dynamic_cast<const EqualitySentence*>(a))) {
    list<const ConstantSentence*>* s1 = getConstants(es->getFirst());
    list<const ConstantSentence*>* s2 = getConstants(es->getSecond());
    if (s1 != 0)  {
      if (s2!=0)  {
        s1->splice(s1->end(), *s2);
        delete s2;
        return s1;
      }
      else 
        return s1;
    }
  }
  return 0;
}

bool SentenceTree::checkFull () {
  return checkFull(root);
}

bool SentenceTree::checkFull (Node* n) {
  if (n->open) {
    for (list<pair<Sentence*, bool>*>::iterator it = n->data->begin(); it!= 
n->data->end(); it++ ) {
      if ((*it)->second == false)
        return false;
    }
    if (n->forAllList->isRight && n->forAllList->isLeft)
      return false;
    if (n->left == 0 && n->right== 0)
      return true;
    if (checkFull(n->left))
      return true;
    if (checkFull(n->right))
      return true;
  }
  return false;
}

void SentenceTree::insertConstantToContainers(Node* n, ConstantSentence* a) {
  Node* cur = n;
  Node* pre = 0;
  n->forAllList->isLeft = true;
  n->forAllList->isRight = true;

  while (cur != 0)  {
    cur->forAllList->addConstant(n, a);
    if (cur->left == pre) {
      cur->forAllList->isRight = true;
    }
    if (cur->right == pre) {
      cur->forAllList->isRight = true;
    }
    pre = cur;
    cur = cur->parent;
  }
}





/***************************FORALLCONTAINER***********/

SentenceTree::ForAllContainer::ForAllContainer(): isRight(false), isLeft(false) 
{ 
  sentences = new list <QuantifierSentence*>;
}

SentenceTree::ForAllContainer::~ForAllContainer()  { 
  delete sentences;
}

list <QuantifierSentence*>* SentenceTree::ForAllContainer::getSentences() {
  return sentences;
}

void SentenceTree::ForAllContainer::addConstant(Node* n, ConstantSentence* con) 
{
  if (constantsMap.find(n) == constantsMap.end()) 
    constantsMap[n] = new list<ConstantSentence*>;
  constantsMap[n]->push_back(con);
}

void SentenceTree::ForAllContainer::initialaize () {
  for (map<Node* ,std::list<ConstantSentence*>*>::iterator cur = 
         constantsMap.begin(); cur != constantsMap.end(); cur++) {
    delete (*cur).second;
  }
  constantsMap.clear();
  isRight = false;
  isLeft = false;
}

map<SentenceTree::Node*, std::list<ConstantSentence*>*>::iterator 
SentenceTree::ForAllContainer::begin() {
  return begin();
}

map<SentenceTree::Node*, std::list<ConstantSentence*>*>::iterator 
SentenceTree::ForAllContainer::end() {
  return end();
}

void SentenceTree::ForAllContainer::addSentence(QuantifierSentence* a) {
  sentences->push_back(a);
}


/***********************NODE*****************/

SentenceTree::Node::Node() {
  open = true;
  right = left = parent = 0;
  data = new list<pair<Sentence*, bool>*>;
  forAllList = new ForAllContainer();
}

SentenceTree::Node::~Node() {
  if (left)
    delete left;
  if (right)
    delete right;
  for (list<pair<Sentence*, bool>*>::iterator it = data->begin(); it != 
data->end(); it++) {
    delete (*it)->first;
    delete *it;
  }
  delete data;
  delete forAllList;
}

string SentenceTree::Node::toString(string pre = "") const {
  string s;
  cout << "a" << endl;
  flush(cout);
  for (list<pair<Sentence*, bool>*>::const_iterator it = data->begin(); it != 
data->end(); it++) {
    s += pre;
    s += " ";
    s += (*it)->first->toString();
    s += "\n";
  }
  if (left) {
    s += left->toString(pre+"L");
  }
  if (right) {
    s += right->toString(pre+"R");
  }
  return s;
}
#ifndef __SENTENCE_TREE_H__
#define __SENTENCE_TREE_H__

#include "Sentence.h"
#include <set>
#include <queue>
#include <map>

class SentenceTree {
 private:
  struct Node;
  typedef std::queue<std::pair<std::pair<Sentence*, bool>*, Node*> > treeQueue;

  static const string PRE_STRING;
  
  class ForAllContainer;
  struct Node {
    Node* left;
    Node* right;
    Node* parent;
    bool open;
    std::list<pair<Sentence*, bool>* >* data;
    ForAllContainer* forAllList;
    Node();
    ~Node();
    std::string toString(string pre = "") const;
  };
      
  class ForAllContainer {
  private:
    map<Node* ,std::list<ConstantSentence*>*> constantsMap;
    std::list <QuantifierSentence*>* sentences;
            
  public:
    ForAllContainer();
    ~ForAllContainer();
            
    bool isRight;
    bool isLeft;
            
    bool searchNode (Node* n);
    map<Node* ,std::list<ConstantSentence*>*>::iterator begin();
    map<Node* ,std::list<ConstantSentence*>*>::iterator end();
    std::list <QuantifierSentence*>* getSentences();
    void addSentence(QuantifierSentence* sen);
    void addConstant(Node* n, ConstantSentence* con);
    void initialaize ();
  };
      
  Node* root;
  static const int checkSequence;
  std::string getNewIndex();
  void insertToQueue(treeQueue &allQueue,
                     treeQueue &eQueue,
                     treeQueue &fQueue,
                     treeQueue &sQueue,
                     pair<Sentence*, bool>* p, Node* n);
      
  void dischargeFTAQueue (Sentence* s, Node* n,
                          treeQueue &allQueue,
                          treeQueue &eQueue,
                          treeQueue &fQueue,
                          treeQueue &sQueue,
                          std::queue<Node*> &forAllQueue);
      
  void dischargeExpressQueue (Sentence* s, Node* n,
                              treeQueue &allQueue,
                              treeQueue &eQueue,
                              treeQueue &fQueue,
                              treeQueue &sQueue);
  void dischargeFastQueue (Sentence* s, Node* n,
                           treeQueue &allQueue,
                           treeQueue &eQueue,
                           treeQueue &fQueue,
                           treeQueue &sQueue);
  void dischargeSlowQueue (Sentence* s, Node* n,
                           treeQueue &allQueue,
                           treeQueue &eQueue,
                           treeQueue &fQueue,
                           treeQueue &sQueue);
  void dischargeForAllQueue (Node* n,
                             treeQueue &allQueue,
                             treeQueue &eQueue,
                             treeQueue &fQueue,
                             treeQueue &sQueue);
      
  void createLeaves (treeQueue &allFTQueue,
                     treeQueue &eQueue,
                     treeQueue &fQueue,
                     treeQueue &sQueue,
                     Sentence* first, Sentence* second, Node* n);
  void createLeaves (treeQueue &allFTQueue,
                     treeQueue &eQueue,
                     treeQueue &fQueue,
                     treeQueue &sQueue,
                     Sentence* first,
                     Sentence* second, Sentence* third, Sentence* forth, Node* 
n);
  void insertToLeaves(treeQueue &allFTQueue,
                      treeQueue &eQueue,
                      treeQueue &fQueue,
                      treeQueue &sQueue,
                      Sentence* first, Sentence* second, Node* n);
  void insertToLeaves (treeQueue &allFTQueue,
                       treeQueue &eQueue,
                       treeQueue &fQueue,
                       treeQueue &sQueue,
                       Sentence* first, Node* n);
  void insertToLeaves(treeQueue &allFTQueue,
                      treeQueue &eQueue,
                      treeQueue &fQueue,
                      treeQueue &sQueue,
                      std::list<Sentence*>* li, Node* n);
      
  void checkBranch (Sentence* s1, Sentence* s2, Node* n);
  void checkBranch (Sentence* s, Node* n);
  void checkBranch (list<Sentence*>* li, Node* n);
  list<const ConstantSentence*>* getBranchConstants(Node* n);
  list<const ConstantSentence*>* getConstants(const Sentence* a);
  void insertConstantToContainers(Node* n, ConstantSentence* s);
      
  bool isContra (Sentence* first, Sentence* second);
  void closeBranch (Node* n);
  bool checkFull(Node* n);
  bool checkFull();
 public:
  SentenceTree(std::list<Sentence*>* list);
  
  bool buildTree();
  int whichSentence(Sentence*);
  bool isNotEqual(Sentence* s);
  ~SentenceTree();
  std::string toString() const;
};


#endif

Other related posts:

  • » [mathprog] version 2