demo_basic_theorem.htm

来自「Delphi脚本控件」· HTM 代码 · 共 551 行 · 第 1/3 页

    NX = A.Number
    NY = B.Number
    ND = LB

    CreateParams(E)
  <font color="blue"><b>End</b></font> <font color="blue"><b>Sub</b></font>

<font color="blue"><b>End</b></font> <font color="blue"><b>Class</b></font>

<font color="blue"><b>Class</b></font> TClauseList
  <font color="blue"><b>Inherits</b></font> TObject
  
  <font color="blue"><b>Dim</b></font> fClauses <font color="blue"><b>As</b></font> TList
  
  <font color="blue"><b>Sub</b></font> <font color="blue"><b>New</b></font>()
    <font color="blue"><b>Me</b></font> = <font color="blue"><b>MyBase</b></font>.Create()
    fClauses = <font color="blue"><b>New</b></font> TList()
  <font color="blue"><b>End</b></font> <font color="blue"><b>Sub</b></font>
  
  <font color="blue"><b>Sub</b></font> Dispose()
    fClauses.Free
    <font color="blue"><b>MyBase</b></font>.Free
  <font color="blue"><b>End</b></font> <font color="blue"><b>Sub</b></font>
  
  <font color="blue"><b>Function</b></font> Add(C <font color="blue"><b>As</b></font> TClause) <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>
    <font color="blue"><b>Return</b></font> fClauses.Add(C)
  <font color="blue"><b>End</b></font> <font color="blue"><b>Function</b></font>
  
  <font color="blue"><b>Sub</b></font> Clear()
    fClauses.Clear
  <font color="blue"><b>End</b></font> <font color="blue"><b>Sub</b></font>
  
  <font color="blue"><b>Function</b></font> Count() <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>
    <font color="blue"><b>return</b></font> fClauses.Count
  <font color="blue"><b>End</b></font> <font color="blue"><b>Function</b></font>
  
  <font color="blue"><b>Sub</b></font> MarkTree(I, N <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>)
    <font color="blue"><b>Dim</b></font> C <font color="blue"><b>As</b></font> TClause
    <font color="blue"><b>If</b></font> I > N <font color="blue"><b>Then</b></font>
      C = Clauses(I - 1)
      C.InProof = true
      MarkTree(C.NX, N)
      MarkTree(C.NY, N)
    <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>
  <font color="blue"><b>End</b></font> <font color="blue"><b>Sub</b></font>
  
  <font color="blue"><b>Sub</b></font> Output(N <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>)
    <font color="blue"><b>Dim</b></font> I, NX, NY, HC <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>, C <font color="blue"><b>As</b></font> TClause
    HC = Count - 1
    <font color="blue"><b>Do</b></font> <font color="blue"><b>While</b></font> (HC > 0)
      C = Clauses(HC)
      <font color="blue"><b>If</b></font> C.E.Length = 0 <font color="blue"><b>Then</b></font>
        <font color="blue"><b>Exit</b></font> <font color="blue"><b>Do</b></font>
      <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>
      HC = HC - 1
    <font color="blue"><b>Loop</b></font>

    <font color="blue"><b>If</b></font> HC = 0 <font color="blue"><b>Then</b></font>
      <font color="blue"><b>println</b></font> <font color="Red">"Not proved"</font>
      <font color="blue"><b>Exit</b></font> <font color="blue"><b>Sub</b></font>
    <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>

    NX = Clauses(HC).NX
    NY = Clauses(HC).NY
    MarkTree(NX, N)
    MarkTree(NY, N)
    <font color="blue"><b>println</b></font> <font color="Red">"Proof: "</font>
    <font color="blue"><b>For</b></font> I = N + 1 <font color="blue"><b>To</b></font> HC
      C = Clauses(I)
      <font color="blue"><b>If</b></font> C.InProof <font color="blue"><b>Then</b></font>
        C.Dump
      <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>
    <font color="blue"><b>Next</b></font>
    <font color="blue"><b>println</b></font> <font color="Red">"Contradiction: "</font>, NX, <font color="Red">" "</font>, NY
    Clauses(HC).Dump
  <font color="blue"><b>End</b></font> <font color="blue"><b>Sub</b></font>
  
  <font color="blue"><b>Sub</b></font> AddClauses(L <font color="blue"><b>As</b></font> TClauseList)
    <font color="blue"><b>Dim</b></font> I <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>
    <font color="blue"><b>For</b></font> I=0 <font color="blue"><b>To</b></font> L.Count - 1
      fClauses.Add(L(I))
    <font color="blue"><b>Next</b></font>
  <font color="blue"><b>End</b></font> <font color="blue"><b>Sub</b></font>

  <font color="blue"><b>Sub</b></font> Dump()
    <font color="blue"><b>Dim</b></font> I <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>
    <font color="blue"><b>For</b></font> I = 0 <font color="blue"><b>To</b></font> Count - 1
      Clauses[I].Dump
    <font color="blue"><b>Next</b></font>
  <font color="blue"><b>End</b></font> <font color="blue"><b>Sub</b></font>

  <font color="blue"><b>Default</b></font> <font color="blue"><b>Property</b></font> Clauses(I <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>) <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>
    <font color="blue"><b>Get</b></font>
      <font color="blue"><b>return</b></font> fClauses(I)
    <font color="blue"><b>End</b></font> <font color="blue"><b>Get</b></font>
    <font color="blue"><b>Set</b></font>
      fClauses(I) = Value
    <font color="blue"><b>End</b></font> <font color="blue"><b>Set</b></font>
  <font color="blue"><b>End</b></font> <font color="blue"><b>Property</b></font>
<font color="blue"><b>End</b></font> <font color="blue"><b>Class</b></font>

<font color="blue"><b>Function</b></font> Contradict(A <font color="blue"><b>As</b></font> TClauseList, U <font color="blue"><b>As</b></font> TClauseList, V <font color="blue"><b>As</b></font> TClauseList) <font color="blue"><b>As</b></font> <font color="blue"><b>Boolean</b></font>
  <font color="blue"><b>Dim</b></font> I, J <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>
  <font color="blue"><b>Dim</b></font> UI, VJ, R <font color="blue"><b>As</b></font> TClause
  <font color="blue"><b>Dim</b></font> Name <font color="blue"><b>As</b></font> <font color="blue"><b>String</b></font>
  
  <font color="blue"><b>For</b></font> I = 0 <font color="blue"><b>To</b></font> U.Count - 1
    UI = U(I)
    Name = UI.Name(0)
    <font color="blue"><b>For</b></font> J = 0 <font color="blue"><b>To</b></font> V.Count - 1
      VJ = V(J)
      <font color="blue"><b>If</b></font> Name = VJ.Name(0) <font color="blue"><b>Then</b></font>
        UI.Rename(AX)
        VJ.Rename(AY)
        <font color="blue"><b>If</b></font> Unify(2, UI.E(0), VJ.E(0)) <font color="blue"><b>Then</b></font>
          R = <font color="blue"><b>New</b></font> TClause(<font color="blue"><b>NULL</b></font>)
          R.PutResolvent(UI, VJ, 0, 0)
          <font color="blue"><b>println</b></font> <font color="Red">"Resolvent:"</font>
          R.Dump()
          A.Add(R)
          
          <font color="blue"><b>Return</b></font> True
        <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>
      <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>
    <font color="blue"><b>Next</b></font>
  <font color="blue"><b>Next</b></font>
  <font color="blue"><b>Return</b></font> false
<font color="blue"><b>End</b></font> <font color="blue"><b>Function</b></font>

<font color="blue"><b>Function</b></font> STest(S <font color="blue"><b>As</b></font> TClauseList, U <font color="blue"><b>As</b></font> TClause) <font color="blue"><b>As</b></font> <font color="blue"><b>Boolean</b></font>
  <font color="blue"><b>Dim</b></font> Name <font color="blue"><b>As</b></font> <font color="blue"><b>String</b></font>
  <font color="blue"><b>Dim</b></font> I <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>
  <font color="blue"><b>Dim</b></font> SI <font color="blue"><b>As</b></font> TClause
  
  Name = U.Name(0)
  <font color="blue"><b>For</b></font> I = 0 <font color="blue"><b>to</b></font> S.Count - 1
    SI = S(I)
    <font color="blue"><b>If</b></font> Name = SI.Name(0) <font color="blue"><b>Then</b></font>
      SI.Rename(ArrConst)
      U.Rename(AX)
      <font color="blue"><b>If</b></font> Unify(2, SI.E[0], U.E[0]) <font color="blue"><b>Then</b></font>
        <font color="blue"><b>Return</b></font> true
      <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>
    <font color="blue"><b>End</b></font> <font color="blue"><b>If</b></font>
  <font color="blue"><b>Next</b></font>
  <font color="blue"><b>Return</b></font> false
<font color="blue"><b>End</b></font> <font color="blue"><b>Function</b></font>

<font color="blue"><b>Function</b></font> GUnit(A <font color="blue"><b>As</b></font> TClauseList, S1 <font color="blue"><b>As</b></font> TClauseList, S2 <font color="blue"><b>As</b></font> TClauseList, W <font color="blue"><b>As</b></font> TClauseList, C <font color="blue"><b>As</b></font> TClause) <font color="blue"><b>As</b></font> <font color="blue"><b>Boolean</b></font>
  <font color="blue"><b>Dim</b></font> P, S, POS, NEG <font color="blue"><b>As</b></font> TList
  <font color="blue"><b>Dim</b></font> I, J <font color="blue"><b>As</b></font> <font color="blue"><b>Integer</b></font>
  <font color="blue"><b>Dim</b></font> U, R <font color="blue"><b>As</b></font> TClause
  <font color="blue"><b>Dim</b></font> Sign, Name <font color="blue"><b>As</b></font> <font color="blue"><b>String</b></font>
  <font color="blue"><b>Dim</b></font> Stack <font color="blue"><b>As</b></font> TStack
  <font color="blue"><b>Dim</b></font> result <font color="blue"><b>As</b></font> <font color="blue"><b>Boolean</b></font>
  
  POS = <font color="blue"><b>new</b></font> TClauseList()
  NEG = <font color="blue"><b>new</b></font> TClauseList()
  Stack = <font color="blue"><b>new</b></font> TStack()

  <font color="blue"><b>Try</b></font>
    Stack.Push(C)

    <font color="blue"><b>Do</b></font>
      C = Stack.Pop

      <font color="blue"><b>For</b></font> I = 0 <font color="blue"><b>to</b></font> W.Count - 1
        U = W[I]
        <font color="blue"><b>If</b></font> U.Number < C.NX <font color="blue"><b>Then</b></font>
          Sign = U.Sign(0)
          Name = U.Name(0)
          <font color="blue"><b>For</b></font> J=0 <font color="blue"><b>to</b></font> C.length - 1
            <font color="blue"><b>If</b></font> (Sign <> C.Sign(J)) <font color="blue"><b>And</b></font> (Name = C.Name(J)) <font color="blue"><b>Then</b></font>
              U.Rename(AX)
              C.Rename(AY)

              <font color="blue"><b>If</b></font> Unify(1, U.E(0), C.E(J)) <font color="blue"><b>Then</b></font>
                R = <font color="blue"><b>new</b></font> TClause(<font color="blue"><b>NULL</b></font>)
                R.PutResolvent(U, C, 0, J)

                <font color="blue"><b>println</b></font> <font color="Red">"Resolvent:"</font>
                R.Dump()
                
                A.Add(R)