//---------------------------------------------------------------------------

#include <vcl.h>
#pragma hdrstop

#include "MyLogicSoftware.h"
#include "ResolutionExperiment1.h"

//---------------------------------------------------------------------------

#pragma package(smart_init)

FILE *Fi;
char line[1025];

//---------------------------------------------------------------------------
void __fastcall MyPrintList(char Title[], TList *List)
{
wsprintf(line, "\x0D\x0A %s |", Title);
fwrite(line, 1, strlen(line), Fi);
if (!List) return;
for (int i=0; i<List->Count; i++)
 {
  int Atom = (int)List->Items[i];
  wsprintf(line, " %d", Atom);
  fwrite(line, 1, strlen(line), Fi);
 }; // i
wsprintf(line, "|");
fwrite(line, 1, strlen(line), Fi);
}

//---------------------------------------------------------------------------
int __fastcall MyListSortCompare(void *Item1, void *Item2)
{
return (int)Item1 - (int)Item2;
}

//---------------------------------------------------------------------------
// class MyClause
//---------------------------------------------------------------------------
__fastcall MyClause::MyClause()
{
NegativeAtoms = new TList;
PositiveAtoms = new TList;
}

//---------------------------------------------------------------------------
__fastcall MyClause::MyClause(TList *NegativeAtoms, TList *PositiveAtoms)
{
NegativeAtoms->Sort(MyListSortCompare);
PositiveAtoms->Sort(MyListSortCompare);
this->NegativeAtoms = NegativeAtoms;
this->PositiveAtoms = PositiveAtoms;
}

//---------------------------------------------------------------------------
__fastcall MyClause::MyClause(int A1, int A2, int A3, int A4)
// A1, A2, A3, A4 = -1, 0, or +1
{
NegativeAtoms = new TList;
PositiveAtoms = new TList;
if (A1<0) NegativeAtoms->Add((void*)1);
else
if (A1>0) PositiveAtoms->Add((void*)1);
if (A2<0) NegativeAtoms->Add((void*)2);
else
if (A2>0) PositiveAtoms->Add((void*)2);
if (A3<0) NegativeAtoms->Add((void*)3);
else
if (A3>0) PositiveAtoms->Add((void*)3);
if (A4<0) NegativeAtoms->Add((void*)4);
else
if (A4>0) PositiveAtoms->Add((void*)4);
}

//---------------------------------------------------------------------------
__fastcall MyClause::~MyClause()
{
delete NegativeAtoms;
delete PositiveAtoms;
}

//---------------------------------------------------------------------------
bool __fastcall MyClause::EqualTo(MyClause *Clause2)
{
if (this->NegativeAtoms->Count != Clause2 ->NegativeAtoms->Count) return false;
if (this->PositiveAtoms->Count != Clause2 ->PositiveAtoms->Count) return false;

for (int i=0; i<this->NegativeAtoms->Count; i++)
  if ((int)this->NegativeAtoms->Items[i] != (int)Clause2->NegativeAtoms->Items[i]) return false;
for (int i=0; i<this->PositiveAtoms->Count; i++)
  if ((int)this->PositiveAtoms->Items[i] != (int)Clause2->PositiveAtoms->Items[i]) return false;
return true;
}

//---------------------------------------------------------------------------
void __fastcall MyClause::Print(char Title[])
{
bool first = true;
wsprintf(line, "\x0D\x0A %s ", Title);
fwrite(line, 1, strlen(line), Fi);

for (int i=0; i<NegativeAtoms->Count; i++)
 {
  int Atom = (int)NegativeAtoms->Items[i];
  if (first) first = false;
  else
   {
    wsprintf(line, "v");
    fwrite(line, 1, strlen(line), Fi);
   };
  wsprintf(line, "~%d", Atom);
  fwrite(line, 1, strlen(line), Fi);
 };
for (int i=0; i<PositiveAtoms->Count; i++)
 {
  int Atom = (int)PositiveAtoms->Items[i];
  if (first) first = false;
  else
   {
    wsprintf(line, "v");
    fwrite(line, 1, strlen(line), Fi);
   };
  wsprintf(line, "%d", Atom);
  fwrite(line, 1, strlen(line), Fi);
 };
if ((NegativeAtoms->Count == 0)&&(PositiveAtoms->Count == 0))
 {
  wsprintf(line, "empty");
  fwrite(line, 1, strlen(line), Fi);
 };
}

//---------------------------------------------------------------------------
// class MyClauseList
//---------------------------------------------------------------------------
__fastcall MyClauseList::MyClauseList()
{
Clauses = new TList;
NegativeSingleAtoms = new TList;
PositiveSingleAtoms = new TList;
}

//---------------------------------------------------------------------------
__fastcall MyClauseList::~MyClauseList()
{
for (int i=0; i<Clauses->Count; i++)
 {
  MyClause *Clause = (MyClause*)Clauses->Items[i];
  delete Clause;
 }; // i
delete Clauses;
delete NegativeSingleAtoms;
delete PositiveSingleAtoms;
}

//---------------------------------------------------------------------------
int __fastcall MyClauseList::Add(MyClause *newClause)
// returns 0 - duplicate found, 1 - OK, 2 - contradiction
{
for (int m=0; m<Clauses->Count; m++)
 {
  MyClause *Clause1 = (MyClause*)Clauses->Items[m];
  if (Clause1->EqualTo(newClause)) { delete newClause; return 0; }; // duplicate found
 };
Clauses->Add(newClause);

if ((newClause->NegativeAtoms->Count == 0)&&(newClause->PositiveAtoms->Count == 0))
 {
  //wsprintf(line, "\x0D\x0A Contradiction: empty clause.");
  //fwrite(line, 1, strlen(line), Fi);
  return 2; // empty clause - contradiction
 };
if ((newClause->NegativeAtoms->Count == 1)&&(newClause->PositiveAtoms->Count == 0))
 { // clause ~B
  int Atom = (int)newClause->NegativeAtoms->Items[0];
  NegativeSingleAtoms->Add((void*)Atom);
  if (PositiveSingleAtoms->IndexOf((void*)Atom) >= 0)
   {
    //wsprintf(line, "\x0D\x0A Contradiction derived: %d, ~%d", Atom, Atom);
    //fwrite(line, 1, strlen(line), Fi);
    return 2; // B and ~B found
   };
 };
if ((newClause->NegativeAtoms->Count == 0)&&(newClause->PositiveAtoms->Count == 1))
 { // clause B
  int Atom = (int)newClause->PositiveAtoms->Items[0];
  PositiveSingleAtoms->Add((void*)Atom);
  if (NegativeSingleAtoms->IndexOf((void*)Atom) >= 0)
   {
    //wsprintf(line, "\x0D\x0A Contradiction derived: ~%d, %d", Atom, Atom);
    //fwrite(line, 1, strlen(line), Fi);
    return 2; // ~B and B found
   };
 };
return 1;
}

//---------------------------------------------------------------------------
void __fastcall MyClauseList::Print(char Title[])
{
wsprintf(line, "\x0D\x0A %s ", Title);
fwrite(line, 1, strlen(line), Fi);

for (int i=0; i<Clauses->Count; i++)
 {
  MyClause *Clause = (MyClause*)Clauses->Items[i];
  Clause->Print("Clause:");
 };
if (Clauses->Count > 0)
wsprintf(line, "\x0D\x0A End of list.");
else
wsprintf(line, "\x0D\x0A Empty list.");
fwrite(line, 1, strlen(line), Fi);
}

//---------------------------------------------------------------------------
//---------------------------------------------------------------------------
//---------------------------------------------------------------------------
TList* __fastcall MyIntersection(TList *List1, TList *List2)
// intersect sorted lists
{
//MyPrintList("MyIntersection L1=", List1);
//MyPrintList("MyIntersection L2=", List2);
TList *Result = new TList;

int i2 = 0;
for (int i1=0; i1<List1->Count; i1++)
{
 int Item1 = (int)List1->Items[i1];
 int Item2;
 next_i2:
 if (i2 >= List2->Count) goto fin;
 Item2 = (int)List2->Items[i2];
 if (Item1 == Item2) { Result->Add((void*)Item1); i2++ ; }
 else
 if (Item1 > Item2) { i2++; goto next_i2; };
 // else Item1 < Item2 - do nothing
}; // i
fin:
//MyPrintList("MyIntersection Result=", Result);
return Result;
}

//---------------------------------------------------------------------------
TList* __fastcall MyUnionExclude(bool Exclude, TList *List1, TList *List2, int Member)
// merge sorted lists, exclude Member and duplicates
{
/*
MyPrintList("MyUnion L1=", List1);
MyPrintList("MyUnion L2=", List2);
if (Exclude)
 {
  wsprintf(line, "\x0D\x0A MyUnion Exclude=%d", Member);
  fwrite(line, 1, strlen(line), Fi);
 };
*/
TList *Result = new TList;
int Item1, Item2;
int i1 = 0;
int i2 = 0;

next_step:
if (i1 >= List1->Count) goto append_List2;
if (i2 >= List2->Count) goto append_List1;
// now i1 < List1->Count
// now i2 < List1->Count
Item1 = (int)List1->Items[i1];
Item2 = (int)List2->Items[i2];

if (Item1 < Item2) { if ((!Exclude)||(Item1 != Member)) Result->Add((void*)Item1); i1++; }
else
if (Item2 < Item1) { if ((!Exclude)||(Item2 != Member)) Result->Add((void*)Item2); i2++; }
else // Item1 == Item2
 { if ((!Exclude)||(Item1 != Member)) Result->Add((void*)Item1); i1++; i2++; };
goto next_step;

append_List1:
if (i1 >= List1->Count)
 {
  //MyPrintList("MyUnion Result1=", Result);
  return Result;
 };
Item1 = (int)List1->Items[i1++];
if ((!Exclude)||(Item1 != Member)) Result->Add((void*)Item1);
goto append_List1;

append_List2:
if (i2 >= List2->Count)
 {
  //MyPrintList("MyUnion Result2=", Result);
  return Result;
 };
Item2 = (int)List2->Items[i2++];
if ((!Exclude)||(Item2 != Member)) Result->Add((void*)Item2);
goto append_List2;
}

//---------------------------------------------------------------------------
bool __fastcall PropositionalResolution(MyClauseList *InitialList, FILE *Fi) // of clauses
{
//InitialList->Print("\x0D\x0A Initial List:");
if (InitialList->Clauses->Count < 2) return false;

MyClauseList *MainList = InitialList;
for (int j=1; ; j++)
{
 if (MainList->Clauses->Count < j+1)
  {
   //wsprintf(line, "\x0D\x0A No contradiction derived.");
   //fwrite(line, 1, strlen(line), Fi);
   return false; // no contradiction derived
  }
 else
  for (int i=0; i<j; i++)
   {
    //wsprintf(line, "\x0D\x0A Processing (%d, %d)", i, j);
    //fwrite(line, 1, strlen(line), Fi);
  //  if (j>100) return false;
  // consider i-th and j-th clauses in the main list: (Ni, Pi), (Nj, Pj)
    MyClause *Ci = (MyClause*)MainList->Clauses->Items[i];
    MyClause *Cj = (MyClause*)MainList->Clauses->Items[j];
    //Ci->Print("Ci");
    //Cj->Print("Cj");
    // if (Ni^Pj)U(Pi^Nj) contains exactly one atom C ^ means set intersection


    TList *CommonAtoms = MyUnionExclude(false, MyIntersection(Ci->NegativeAtoms, Cj->PositiveAtoms),
                                 MyIntersection(Cj->NegativeAtoms, Ci->PositiveAtoms), 0);
    if (CommonAtoms->Count == 1)
     {
      int C = (int)CommonAtoms->Items[0];
      //wsprintf(line, "\x0D\x0A Common atom %d", C);
      //fwrite(line, 1, strlen(line), Fi);

      // apply resolution - resolvent is (NiUNj-{C}, PiUPj-{C})
      MyClause *Resolvent = new MyClause(MyUnionExclude(true, Ci->NegativeAtoms, Cj->NegativeAtoms, C),
                                         MyUnionExclude(true, Ci->PositiveAtoms, Cj->PositiveAtoms, C));
      //Resolvent->Print("Resolvent:");
      int rc = MainList->Add(Resolvent);
      //Ci->Print("Ci");
      //Cj->Print("Cj");
      //Resolvent->Print("Resolvent:");
      if (rc == 2) // contradiction
       {
        //MainList->Print("\x0D\x0A Clause List:");
        //wsprintf(line, "\x0D\x0A XX Contradiction derived.");
        //fwrite(line, 1, strlen(line), Fi);
        delete CommonAtoms;
        return true;
       }; // contradiction
     };
    delete CommonAtoms;
   }; // j
}; // i
}

//---------------------------------------------------------------------------
void __fastcall MyResolutionExperiment1()
{
MyClauseList *InitialList;

int experiment = 1;
wsprintf(line, "%s\\kp_resol_%d.txt", MyGetModulePath().c_str(), experiment);
Fi = fopen(line, "w");

wsprintf(line, "\x0D\x0A\x0D\x0A-------------- Resolution Experiment 1 --------------");
fwrite(line, 1, strlen(line), Fi);
InitialList = new MyClauseList();
PropositionalResolution(InitialList, Fi);
delete InitialList;

wsprintf(line, "\x0D\x0A\x0D\x0A-------------- Resolution Experiment 2 --------------");
fwrite(line, 1, strlen(line), Fi);
InitialList = new MyClauseList();
InitialList->Add(new MyClause(0,0,0,0));
PropositionalResolution(InitialList, Fi);
delete InitialList;

wsprintf(line, "\x0D\x0A\x0D\x0A-------------- Resolution Experiment 3 --------------");
fwrite(line, 1, strlen(line), Fi);
InitialList = new MyClauseList();
InitialList->Add(new MyClause(1,2,3,4));
InitialList->Add(new MyClause(-1,2,3,0));
PropositionalResolution(InitialList, Fi);
delete InitialList;

wsprintf(line, "\x0D\x0A\x0D\x0A-------------- Resolution Experiment 4 --------------");
fwrite(line, 1, strlen(line), Fi);
InitialList = new MyClauseList();
InitialList->Add(new MyClause(-1,2,0,0));
InitialList->Add(new MyClause(1,2,0,0));
InitialList->Add(new MyClause(0,-2,0,0));
PropositionalResolution(InitialList, Fi);
delete InitialList;

wsprintf(line, "\x0D\x0A\x0D\x0A-------------- Resolution Experiment 5 --------------");
fwrite(line, 1, strlen(line), Fi);
InitialList = new MyClauseList();
InitialList->Add(new MyClause(1,-2,3,-4));
InitialList->Add(new MyClause(1,2,3,-4));
InitialList->Add(new MyClause(0,-2,-3,0));
InitialList->Add(new MyClause(0,0,-3,4));
PropositionalResolution(InitialList, Fi);
delete InitialList;

wsprintf(line, "\x0D\x0A\x0D\x0A--- Resolution Experiment 6 --- A->B, ~A->B |- B ----");
fwrite(line, 1, strlen(line), Fi);
// A->B, ~A->B |- B.
InitialList = new MyClauseList();
if (1==InitialList->Add(new MyClause(-1,2,0,0)))
if (1==InitialList->Add(new MyClause(1,2,0,0)))
if (1==InitialList->Add(new MyClause(0,-2,0,0)))
PropositionalResolution(InitialList, Fi);
delete InitialList;

wsprintf(line, "\x0D\x0A\x0D\x0A--- Resolution Experiment 7 --- (A->B)->A |- A ----");
fwrite(line, 1, strlen(line), Fi);
//(A->B)->A |- A
InitialList = new MyClauseList();
if (1==InitialList->Add(new MyClause(1,0,0,0)))
if (1==InitialList->Add(new MyClause(1,-2,0,0)))
if (1==InitialList->Add(new MyClause(-1,0,0,0)))
PropositionalResolution(InitialList, Fi);
delete InitialList;

wsprintf(line, "\x0D\x0A\x0D\x0A--- Resolution Experiment 8 --- B->(C->D), B->C |- B->D (Axiom L2) ----");
fwrite(line, 1, strlen(line), Fi);
//(B->(C->D), B->C |- B->D (Axiom L2)
InitialList = new MyClauseList();
if (1==InitialList->Add(new MyClause(0,-2,-3,4)))
if (1==InitialList->Add(new MyClause(0,-2,3,0)))
if (1==InitialList->Add(new MyClause(0,2,0,0)))
if (1==InitialList->Add(new MyClause(0,0,0,-4)))
PropositionalResolution(InitialList, Fi);
delete InitialList;

wsprintf(line, "\x0D\x0A\x0D\x0A--- Resolution Experiment 9 --- B->D, C->D |- BvC->D (Axiom L8) ----");
fwrite(line, 1, strlen(line), Fi);
// B->D, C->D |- BvC->D (Axiom L8)  -   ~BvD, ~CvD, BvC, ~D
InitialList = new MyClauseList();
if (1==InitialList->Add(new MyClause(0,-2,0,4)))
if (1==InitialList->Add(new MyClause(0,0,-3,4)))
if (1==InitialList->Add(new MyClause(0,2,3,0)))
if (1==InitialList->Add(new MyClause(0,0,0,-4)))
if (1==PropositionalResolution(InitialList, Fi))
delete InitialList;

wsprintf(line, "\x0D\x0A\x0D\x0A--- Resolution Experiment 10 --- ~A->BvC, B->AvC, A->C |- C ----");
fwrite(line, 1, strlen(line), Fi);
// ~A->BvC, B->AvC, A->C |- C  -  AvBvC, Av~BvC, ~AvC, ~C
InitialList = new MyClauseList();
if (1==InitialList->Add(new MyClause(1,2,3,0)))
if (1==InitialList->Add(new MyClause(1,-2,3,0)))
if (1==InitialList->Add(new MyClause(-1,0,3,0)))
if (1==InitialList->Add(new MyClause(0,0,-3,0)))
PropositionalResolution(InitialList, Fi);
delete InitialList;

int Exp = 0;
int Tot = 0;
for (int i1=-1; i1<=1; i1+=1)
for (int i2=-1; i2<=1; i2+=1)
for (int i3=-1; i3<=1; i3+=1)
if (i1*i1+i2*i2+i3*i3 == 2)
for (int j1=-1; j1<=1; j1+=1)
for (int j2=-1; j2<=1; j2+=1)
for (int j3=-1; j3<=1; j3+=1)
if (j1*j1+j2*j2+j3*j3 == 2)
for (int k1=-1; k1<=1; k1+=1)
for (int k2=-1; k2<=1; k2+=1)
for (int k3=-1; k3<=1; k3+=1)
if (k1*k1+k2*k2+k3*k3 == 2)
for (int m1=-1; m1<=1; m1+=1)
for (int m2=-1; m2<=1; m2+=1)
for (int m3=-1; m3<=1; m3+=1)
if (m1*m1+m2*m2+m3*m3 == 2)
{
Tot++;
InitialList = new MyClauseList();
if (1==InitialList->Add(new MyClause(i1,i2,i3,0)))
if (1==InitialList->Add(new MyClause(j1,j2,j3,0)))
if (1==InitialList->Add(new MyClause(k1,k2,k3,0)))
if (1==InitialList->Add(new MyClause(m1,m2,m3,0)))
 {
  if (PropositionalResolution(InitialList, Fi))
   {
    wsprintf(line, "\x0D\x0A\x0D\x0A--- Resolution Experiment %d (%d) -------", ++Exp, Tot);
    fwrite(line, 1, strlen(line), Fi);
    InitialList->Print("\x0D\x0A Clause List:");
    wsprintf(line, "\x0D\x0A XX Contradiction derived.");
    fwrite(line, 1, strlen(line), Fi);
   }; 
 };
delete InitialList;
};

wsprintf(line, "\x0D\x0A\x0D\x0A----------------------- The End ----------------------\x0D\x0A");
fwrite(line, 1, strlen(line), Fi);
fclose(Fi);
}

//---------------------------------------------------------------------------