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

#include <vcl.h>
#pragma hdrstop

//#include <FileCtrl.hpp>
#include <stdio.h>
//#include <dos.h>
//#include <dir.h>
//#include <fcntl.h>
//#include <io.h>
//#include <sys\stat.h>
//#include <systdate.h>

#include "MyLogicSoftware.h"
#include "LogicExperiment1.h"

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

#pragma package(smart_init)

static int Conj[3][3] = {{0,0,0},{0,1,1},{0,1,2}};
static int Disj[3][3] = {{0,1,2},{1,1,2},{2,2,2}};
static int Impl[3][3] = {{2,2,2},{2,2,2},{0,1,2}};
static int Neg[3] = {2,1,0};

// experiment #1
static int Impl1[3][3] = {{2,2,2},{2,2,2},{0,1,2}};
static int Neg1[3] = {2,1,0};

// experiment #2
static int Impl2[3][3] = {{2,2,2},{0,2,2},{0,1,2}};
static int Neg2[3] = {2,2,1};

// experiment #3
static int Impl3[3][3] = {{2,2,2},{0,2,2},{0,1,2}};
static int Neg3[3] = {2,0,0};

#define Max_Formula 81
#define Num_ConstrFormulas 6
#define Num_ClassFormulas 15

// use parentheses for each operation

static char ConstrFormula[Num_ConstrFormulas][Max_Formula] =
{ "(AvB)->((~A)->B)",
  "((~A)vB)->(A->B)",
  "((~~A)->(~~B))->(~~(A->B))",
  "(~~A)->((~A)->A)",
  "(Av(~A))->((~~A)->A)",
  "~~((~~A)->A)"  };

static char ClassFormula[Num_ClassFormulas][Max_Formula] =
{ "(~~(AvB))->((~~A)v(~~B))",
  "(~(A&B))->((~A)v(~B))",
  "(~~A)->A",
  "((~B)->(~A))->(A->B)",
  "((~A)->B)->((~B)->A)",
  "((~~A)->(~~B))->(A->B)",
  "(A->B)->((~A)vB)",
  "((A->B)->B)->(AvB)",
  "((A->B)->A)->A",
  "(~(A&(~B)))->(A->B)",
  "(A->B)->((~A->B)->B)",
  "(~(A->B))->(A&(~B))",
  "Av(A->B)",
  "(A->B)v(B->A)",
  "(A->B)->(((~A)->(~B))->(B->A))" };

//---------------------------------------------------------------------------
__fastcall MyFormula::MyFormula()
{
this->Text = "";
}

//---------------------------------------------------------------------------
__fastcall MyFormula::MyFormula(AnsiString Text)
{
this->Text = Text;
}

#define myOper_Neg 1
#define myOper_Conj 2
#define myOper_Disj 3
#define myOper_Impl 4

//---------------------------------------------------------------------------
int __fastcall MyFormula::Analyze(int *pOperation,
                          AnsiString *pSubFormula1, AnsiString *pSubFormula2)
{
int i;
int lev = 0;
AnsiString SubFormula1 = "";
AnsiString SubFormula2 = "";
int len = Text.Length();

if (len==1) { *pOperation = 0; SubFormula1=Text; goto norm; };

for (i=1; i<=len; i++)
 {
  switch(Text[i])
   {
    case '(': { lev++; break; };
    case ')': { lev--; break; };
    case '~': { if (lev==0) goto neg; else break; };
    case '&': { if (lev==0) goto conj; else break; };
    case 'v': { if (lev==0) goto disj; else break; };
    case '-': { if (lev==0) goto impl; else break; };
   };
 };
neg:
*pOperation = myOper_Neg;
SubFormula1 = Text.SubString(i+1, len-i);
goto norm;

conj:
*pOperation = myOper_Conj;
SubFormula1 = Text.SubString(1, i-1);
SubFormula2 = Text.SubString(i+1, len-i);
goto norm;

disj:
*pOperation = myOper_Disj;
SubFormula1 = Text.SubString(1, i-1);
SubFormula2 = Text.SubString(i+1, len-i);
goto norm;

impl:
*pOperation = myOper_Impl;
SubFormula1 = Text.SubString(1, i-1);
SubFormula2 = Text.SubString(i+2, len-i);
goto norm;

norm:
if(!SubFormula1.IsEmpty())
{
 if (SubFormula1[1]=='(') SubFormula1.Delete(1,1);
 len = SubFormula1.Length();
 if (SubFormula1[len]==')') SubFormula1.Delete(len,1);
}
if(!SubFormula2.IsEmpty())
{
 if (SubFormula2[1]=='(') SubFormula2.Delete(1,1);
 len = SubFormula2.Length();
 if (SubFormula2[len]==')') SubFormula2.Delete(len,1);
};
*pSubFormula1 = SubFormula1;
*pSubFormula2 = SubFormula2;
return 1;
}

//---------------------------------------------------------------------------
int __fastcall MyFormula::AlwaysTrue()
{
for (int A=0; A<=2; A++)
for (int B=0; B<=2; B++)
for (int C=0; C<=2; C++)
 {
  if (ValueAt(A,B,C)!=2) return 0;
 }
return 1;
}

//---------------------------------------------------------------------------
int __fastcall MyFormula::ValueAt(int A, int B, int C)
{
AnsiString SubFormula1;
AnsiString SubFormula2;
int Operation;

Analyze(&Operation, &SubFormula1, &SubFormula2);

switch(Operation)
 {
  case 0: goto argument;
  case myOper_Neg:
   {
    MyFormula *F1 = new MyFormula(SubFormula1);
    int v = Neg[F1->ValueAt(A,B,C)];
    delete F1;
    return v;
   };
  case myOper_Conj:
   {
    MyFormula *F1 = new MyFormula(SubFormula1);
    MyFormula *F2 = new MyFormula(SubFormula2);
    int v = Conj[F1->ValueAt(A,B,C)][F2->ValueAt(A,B,C)];
    delete F1;
    delete F2;
    return v;
   };
  case myOper_Disj:
   {
    MyFormula *F1 = new MyFormula(SubFormula1);
    MyFormula *F2 = new MyFormula(SubFormula2);
    int v = Disj[F1->ValueAt(A,B,C)][F2->ValueAt(A,B,C)];
    delete F1;
    delete F2;
    return v;
   };
  case myOper_Impl:
   {
    MyFormula *F1 = new MyFormula(SubFormula1);
    MyFormula *F2 = new MyFormula(SubFormula2);
    int v = Impl[F1->ValueAt(A,B,C)][F2->ValueAt(A,B,C)];
    delete F1;
    delete F2;
    return v;
   };
 }; // switch

argument:
switch(SubFormula1[1])
 {
  case 'A': return A;
  case 'B': return B;
  case 'C': return C;
 };
return 0;
}

//---------------------------------------------------------------------------
void __fastcall MyF1(FILE *Fi, AnsiString Title, AnsiString S)
{
char line[256];

if (!Title.IsEmpty())
 {
  wsprintf(line, "\x0D\x0A %s ", Title.c_str());
  fwrite(line, 1, strlen(line), Fi);
 };
MyFormula *F = new MyFormula(S);
wsprintf(line, "\x0D\x0A A  %s \x0D\x0A", S.c_str());
fwrite(line, 1, strlen(line), Fi);
for (int A=0; A<=2; A++)
 {
  wsprintf(line, " %d  %d\x0D\x0A", A, F->ValueAt(A,0,0));
  fwrite(line, 1, strlen(line), Fi);
 };
delete F;
}

//---------------------------------------------------------------------------
void __fastcall MyF2(FILE *Fi, AnsiString Title, AnsiString S)
{
char line[256];

if (!Title.IsEmpty())
 {
  wsprintf(line, "\x0D\x0A %s ", Title.c_str());
  fwrite(line, 1, strlen(line), Fi);
 };
MyFormula *F = new MyFormula(S);
wsprintf(line, "\x0D\x0A A B  %s \x0D\x0A", S.c_str());
fwrite(line, 1, strlen(line), Fi);
for (int A=0; A<=2; A++)
for (int B=0; B<=2; B++)
 {
  wsprintf(line, " %d %d  %d\x0D\x0A", A, B, F->ValueAt(A,B,0));
  fwrite(line, 1, strlen(line), Fi);
 };
delete F;
}

//---------------------------------------------------------------------------
void __fastcall MyF3(FILE *Fi, AnsiString Title, AnsiString S)
{
char line[256];

if (!Title.IsEmpty())
 {
  wsprintf(line, "\x0D\x0A %s ", Title.c_str());
  fwrite(line, 1, strlen(line), Fi);
 };
MyFormula *F = new MyFormula(S);
wsprintf(line, "\x0D\x0A A B C  %s \x0D\x0A", S.c_str());
fwrite(line, 1, strlen(line), Fi);
for (int A=0; A<=2; A++)
for (int B=0; B<=2; B++)
for (int C=0; C<=2; C++)
 {
  wsprintf(line, " %d %d %d  %d\x0D\x0A", A, B, C, F->ValueAt(A,B,C));
  fwrite(line, 1, strlen(line), Fi);
 };
delete F;
}

//---------------------------------------------------------------------------
void __fastcall MyLogicExperiment1(int experiment)
// experiment = 1, 2, 3
{
char line[1025];

wsprintf(line, "%s\\kp_log%d.txt", MyGetModulePath().c_str(), experiment);
FILE *Fi = fopen(line, "w");

switch (experiment)
 {
  case 1:
   {
    memcpy(Impl, Impl1, sizeof(Impl));
    memcpy(Neg, Neg1, sizeof(Neg));
    wsprintf(line, "Independence of L9 from L1-L8,L10 (L1-L8,L10 - true, L9,L11 - not)\x0D\x0A");
    fwrite(line, 1, strlen(line), Fi);
    break;
   };
  case 2:
   {
    memcpy(Impl, Impl2, sizeof(Impl));
    memcpy(Neg, Neg2, sizeof(Neg));
    wsprintf(line, "Independence of L10 from L1-L9,L11 (L1-L9,L11 - true, L10 - not)\x0D\x0A");
    fwrite(line, 1, strlen(line), Fi);
    break;
   };
  case 3:
   {
    memcpy(Impl, Impl3, sizeof(Impl));
    memcpy(Neg, Neg3, sizeof(Neg));
    wsprintf(line, "Independence of L11 from L1-L10 (L1-L10 - true, L11 - not)\x0D\x0A");
    fwrite(line, 1, strlen(line), Fi);
    break;
   };
 };

MyF1(Fi, "Negation truth table", "~A");
MyF2(Fi, "Implication truth table", "A->B");
MyF2(Fi, "Conjunction truth table", "A&B");
MyF2(Fi, "Disjunction truth table", "AvB");

MyF2(Fi, "Axiom L1", "A->(B->A)");
MyF3(Fi, "Axiom L2", "(A->(B->C))->((A->B)->(A->C))");
MyF2(Fi, "Axiom L3", "A->(B->(A&B))");
MyF2(Fi, "Axiom L4", "(A&B)->A");
MyF2(Fi, "Axiom L5", "(A&B)->B");
MyF2(Fi, "Axiom L6", "A->(AvB)");
MyF2(Fi, "Axiom L7", "B->(AvB)");
MyF3(Fi, "Axiom L8", "(A->C)->((B->C)->((AvB)->C))");
MyF2(Fi, "Axiom L9", "(A->B)->((A->(~B))->(~A))");

MyF2(Fi, "Axiom L10", "(~A)->(A->B)");
MyF1(Fi, "Axiom L11", "Av(~A)");

wsprintf(line, "\x0D\x0A Constructively provable formulas\x0D\x0A");
fwrite(line, 1, strlen(line), Fi);

for (int i=0; i<Num_ConstrFormulas; i++)
 {
  char *Fla;
  Fla = &ConstrFormula[i][0];
  MyF2(Fi, "", Fla);
 };

wsprintf(line, "\x0D\x0A Classically provable formulas\x0D\x0A");
fwrite(line, 1, strlen(line), Fi);

for (int i=0; i<Num_ClassFormulas; i++)
 {
  char *Fla;
  Fla = &ClassFormula[i][0];
  MyF2(Fi, "", Fla);
 };

fclose(Fi);
}

//---------------------------------------------------------------------------
int __fastcall AlwaysTrue(AnsiString S)
{
MyFormula *F;

F = new MyFormula(S);
int rc = F->AlwaysTrue();
delete F;
return rc;
}

//---------------------------------------------------------------------------
void __fastcall MyFF(FILE *Fi, AnsiString S)
{
MyFormula *F;
char line[256];

F = new MyFormula(S);
if (F->AlwaysTrue())
 wsprintf(line, "True: %s\x0D\x0A", S.c_str());
else
 wsprintf(line, "Not true: %s\x0D\x0A", S.c_str());
fwrite(line, 1, strlen(line), Fi);
delete F;
}

//---------------------------------------------------------------------------
void __fastcall MyLogicExperiment2(int experiment)
// experiment = 0, 1, 2, 3, 4
{
char line[1025];
int rc9, rc10, rc11;

wsprintf(line, "%s\\kp_log0%d.txt", MyGetModulePath().c_str(), experiment);
FILE *Fi = fopen(line, "w");

int impl_variant = 0;
int variant = 0;

for (int i4=0; i4<=2; i4++)
for (int i7=0; i7<=1; i7++)
for (int i8=0; i8<=1; i8++)
{
Impl[1][0] = i4;
Impl[2][0] = i7;
Impl[2][1] = i8;

if (!AlwaysTrue("(A->(B->C))->((A->B)->(A->C))")) continue;
if (!AlwaysTrue("A->(B->(A&B))")) continue;
if (!AlwaysTrue("(A->C)->((B->C)->((AvB)->C))")) continue;

wsprintf(line, "\x0D\x0A------------------------------------------------\x0D\x0A");
fwrite(line, 1, strlen(line), Fi);
wsprintf(line, "Implication variant #%d:\x0D\x0A", ++impl_variant);
fwrite(line, 1, strlen(line), Fi);
for (int i=0; i<=2; i++)
for (int j=0; j<=2; j++)
 {
  wsprintf(line, " %d", Impl[i][j]);
  fwrite(line, 1, strlen(line), Fi);
 };
wsprintf(line, " L1-L8 true. ");
fwrite(line, 1, strlen(line), Fi);

for (int ia=0; ia<=2; ia++)
for (int ib=0; ib<=2; ib++)
for (int ic=0; ic<=2; ic++)
{
Neg[0] = ia;
Neg[1] = ib;
Neg[2] = ic;

rc9 = AlwaysTrue("(A->B)->((A->(~B))->(~A))");
rc10 = AlwaysTrue("(~A)->(A->B)");
rc11 = AlwaysTrue("Av(~A)");

switch (experiment)
 {
  case 0: // explore all variants where L1-L8 are true
   {
    break;
   };
  case 1: // explore all variants where L1-L8 are true, L9 false, L10 true
   {
    if (rc9) continue;
    if (!rc10) continue;
    break;
   };
  case 2: // explore all variants where L1-L8 are true, L9 true, L10 false, L11 true
   {
    if (!rc9) continue;
    if (rc10) continue;
    if (!rc11) continue;
    break;
   };
  case 3: // explore all variants where L1-L8 are true, L9 true, L10 true, L11 false
   {
    if (!rc9) continue;
    if (!rc10) continue;
    if (rc11) continue;
    break;
   };
  case 4: // explore all variants where L1-L8 are true, L9 true, L10 false
   {
    if (!rc9) continue;
    if (rc10) continue;
    break;
   };
 };

wsprintf(line, "\x0D\x0A Variant #%d. Negation:", ++variant);
fwrite(line, 1, strlen(line), Fi);
for (int i=0; i<=2; i++)
 {
  wsprintf(line, " %d", Neg[i]);
  fwrite(line, 1, strlen(line), Fi);
 };

if (rc9)
 wsprintf(line, " L9 true.");
else
 wsprintf(line, " L9 not true.");
fwrite(line, 1, strlen(line), Fi);

if (rc10)
 wsprintf(line, " L10 true.");
else
 wsprintf(line, " L10 not true.");
fwrite(line, 1, strlen(line), Fi);

if (rc11)
 wsprintf(line, " L11 true.");
else
 wsprintf(line, " L11 not true.");
fwrite(line, 1, strlen(line), Fi);

wsprintf(line, "\x0D\x0A Constructively provable formulas\x0D\x0A");
fwrite(line, 1, strlen(line), Fi);

for (int i=0; i<Num_ConstrFormulas; i++)
 {
  char *Fla;
  Fla = &ConstrFormula[i][0];
  MyFF(Fi, Fla);
 };

wsprintf(line, "\x0D\x0A Classically provable formulas\x0D\x0A");
fwrite(line, 1, strlen(line), Fi);

for (int i=0; i<Num_ClassFormulas; i++)
 {
  char *Fla;
  Fla = &ClassFormula[i][0];
  MyFF(Fi, Fla);
 };

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

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