Quelltextausschnitt

Das Herzstück des Formelanalysators

program Formel_Analysator;       (* Das Program ermittelt für eine vollständig
                                 geklammerte Formel F in den Atomen A,B,...
                                 alle Interpretationen, die Modell für F sind,
                                 mittels Auswertung von F bei allen Interpre-
                                 tationen. Damit wird die Auswertung von
                                 Formeln in mehr als 16 Atomen aufgrund der
                                 Zeitkomplexität unrealistisch.  *)

                                 (* copyright kp ndf 1991-96 *)

uses crt, dos;

label Start;

const MaxLastAtom = 'Z';
      LastAtom : char = MaxLastAtom;
      Wahr = chr(64);
      Falsch = chr(63);
      Erfuellbar : boolean = false;
      Widerspruchsvoll : boolean = false;
      Allgemeingueltig : boolean = true;
      FileName : string[80] = 'aufg.FRM';

type Atomar = Falsch .. MaxLastAtom;
     BetaWerte = array[Atomar] of boolean;
     Charset = set of char;

const Atome = [Falsch, Wahr, 'A' ..MaxLastAtom];
      OPZ = ['-','v','&','>','='];        (*  nicht,oder,und,folgt,gdw. *)
      KLAMMER = ['(',')'];
      W : array[false..true] of char =  ('0','1');
      OnFile : boolean = false;
      Str : string[4] = 'Nein';

var FormelFile : text;
    Formel : string;
    Atom : Atomar;
    OP,Ch : CHAR;
    Beta : BetaWerte;               (* Interpretation der Atome *)
    LastWert : boolean;
    Changed : boolean;
    FormelAnf, FormelEnd, F1A, F1E, F2A, F2E: integer;
                                 (* Position (Anfang und Ende) im String
                                    für Formel,
                                    für Ersten Operand (F1A,F1E) und
                                    für Zweiten Operand (F2A,F2E)
                                    mit Operator OP *)
    X : integer;
    LastPos : integer;

...

procedure BetaInit;
var Atom: Atomar;
begin
  for Atom:= Falsch to LastAtom do
    Beta[Atom] := false;
  Beta[Wahr] := true;
end;

procedure WerteGenerator(var Beta: BetaWerte; LastAtom: Char;
                         var LastWert: boolean);
var Atom: Atomar;
begin
  LastWert := false;
  Atom:= LastAtom;
  Beta[Atom] := not(Beta[Atom]);
  while Beta[Atom] = false do
  begin
    Atom := pred(Atom);
    if Atom < 'A' then
    begin
      LastWert := true;
      exit
    end;
    Beta[Atom] := not(Beta[Atom]);
  end;
end;

function Value(FormelAnf,FormelEnd:integer):boolean;
(* rekursive Funktion zur Funktionswertbestimmung einer Formel bzgl. einer
   vorgegebenen Interpretation Beta der Atome A,B,... *)
var H:boolean;
    A1,E1,A2,E2:integer;
begin
  Find_OPZ(FormelAnf,FormelEnd,F1A,F1E,F2A,F2E,OP);
  A1:=F1A;E1:=F1E;
  A2:=F2A;E2:=F2E;
  case OP of
    '-': H:= not Value(A1,E1);
    'v': H:= Value(A1,E1) or Value(A2,E2);
    '&': H:= Value(A1,E1) and Value(A2,E2);
    '>': H:= not Value(A1,E1) or Value(A2,E2);
    '=': H:= Value(A1,E1) and Value(A2,E2) or not Value(A1,E1) and not Value(A2,E2);
  else
    Ch := Formel[FormelAnf];
    if Ch in ['0','1'] then Atom := chr(ord(Ch)+15)
    else Atom := Ch;
    if Atom in Atome then
      H := Beta[Atom]
    else
    begin
      writeln('Fehler in Formel');
      halt
    end
  end;
  Value := H;
end;
...
begin (* main *)
...
  repeat
  Start:
    Choose('<F>ile oder <E>ingabe oder <Q>uit?',Ch, ['E','F','Q']);
    if Ch = 'F' then
    begin
      Choose('Formel <L>esen vom oder <S>chreiben auf`s File',Ch,['L','S']);
      if Ch = 'S' then
      begin
        Formel_to_File;
        goto Start
      end
      else
        Formel_from_File;
    end
    else
    if upcase(Ch) = 'E' then
    begin
      clrscr;
      EingabeString('[ vollständig geklammerte Formel in Atomen A,B,C,... mit Operatoren  -,&,v,>,= ]',Formel);
    end;
    if (Formel='') or not Klammertest(Formel) or (upcase(Ch) = 'Q') then
      exit;
   

    EingabeInt('Anzahl Atome = ',X);
    LastAtom := chr(64 + X);
    DelSpaces(Formel);
    BetaInit;

    EinText('Resultat auf das Eingabefile? [J/N] ',Str);
    Schalt(Str,OnFile);
    if OnFile = true then
      append(FormelFile);
    writeln;
    writeln('Auswertung:');
    if OnFile = true then
    begin
      writeln(FormelFile);
      writeln(FormelFile,'Auswertung:');
    end;

    FormelAnf := 1;
    FormelEnd := length(Formel);
    repeat
      if Value(FormelAnf,FormelEnd) = true then
      begin
        Erfuellbar := true;
        write('Interpretation der Atome mit   ');
        if OnFile = true then
          write(FormelFile,'Interpretation der Atome mit   ');
        WerteAusgabe(Beta);
        writeln('   liefert value   ',W[true]);
        if OnFile = true then
          writeln(FormelFile,'   liefert value   ',W[true]);
      end
      else ...
    ...