OCaml的satisfable邏輯運算

Question

我試圖寫在OCaml的一個函數，得到一個邏輯運算作爲參數（這樣定義:)

type oper = B of bool 
      | V of string 
      | Neg of oper 
      | And of oper * oper 
      | Or of oper * oper 
      | Impl of oper * oper 

，並返回「真」如果操作satisfable（它在至少一個情況下返回true），如果不滿足則返回「false」（它在所有情況下都返回false）。爲此，我試圖用V true或B false替代V，直到我變爲true並引發Do_it異常。如果在任何情況下我都不是真的，我會拋出Not_found異常並評估在程序結束時我得到的異常。

let satisfable operation= 
    let switch x var tf= 
     let rec aux1 =function 
      |B b->B b 
      |V s when s=var ->aux1 (B tf) 
      |V s->V s 
      |And(e1,e2)->(match aux1 e1, aux1 e2 with 
         |(B false,_)|(_,B false)->B false 
         |(B true, x)|(x,B true)->aux1 x 
         |(x1,x2)->And(x1,x2)) 
      |Or(e1,e2)->(match aux1 e1,aux1 e2 with 
         |(B true, _)|(_,B true)->B true 
         |(B false, x)|(x,B false)->aux1 x 
         |(x1,x2)->Or(x1,x2)) 
      |Impl(e1,e2)->(match aux1 e1,aux1 e2 with 
        |(B false,_)->B false 
        |(B true,x)->aux1 x 
        |(x1,x2)->Impl(x1,x2)) 
      |Neg b->(match b with 
        |B b-> B (not b) 
        |s->Neg (aux1 s)) 
     in aux1 x  
    in let rec aux = function 
     |B b->B b 
     |V s->(match switch operation s true with 
       |B true->raise Do_it 
       |x-> aux (switch operation s true) 
       ) 
     |V s->(match switch operation s false with 
       |B true->raise Do_it 
       |x-> aux (switch operation s false) 
       ) 
     |V s->raise Not_found 
      |And(e1,e2)->(match aux e1, aux e2 with 
         |(B false,_)|(_,B false)->B false 
         |(B true, x)|(x,B true)->aux x 
         |(x1,x2)->And(x1,x2)) 
      |Or(e1,e2)->(match aux e1,aux e2 with 
         |(B true, _)|(_,B true)->B true 
         |(B false, x)|(x,B false)->aux x 
         |(x1,x2)->Or(x1,x2)) 
      |Impl(e1,e2)->(match aux e1,aux e2 with 
        |(B false,_)->B false 
        |(B true,x)->aux x 
        |(x1,x2)->Impl(x1,x2)) 
      |Neg b->(match b with 
        |B b-> B (not b) 
        |s->Neg (aux s)) 
        in if(try aux operation with Do_it->B true|Not_found->B false)=B false then false else true;; 

但它不工作，我想要的方式，在某些情況下甚至會引發堆棧溢出異常。

函數「開關」返回其中字符串變量「VAR」被取代成TF（真/假）

Answer 1

在功能aux的值的操作中，將在V s匹配三次。只有第一個案例將被分析。此外，撥打兩次switch operation s true不是一個好主意，您可以通過聲明let case_true = switch operation s true來避免重複兩次相同的計算。

Answer 2

您的功能aux使用operation的外部定義，每個遞歸調用都不會改變。