查找使二進制表達式計算結果爲真的值

Question

給定一個表達式，如'x < 10和x> = 11或x> 20'，並假設已經有可用表達式的分析樹（例如[或[[和[< [var：x] [10]] [> = [var：x] [11]]]] [> [var：x] [20]]]），我如何找到x的範圍/這導致這個表達式評估爲真？

在語法的一些限制是：在表達

1. 只有一個變量（在本例中x）中，所以沒有這樣的表達式X + 2個<ý
2. 僅對比運算符，但也可以是事像空？ [字符串表達式]在表達式
3. 沒有算術表達式或函數調用 - 所以像X + 2 < 3，或x < someFunc（）是不可能的

Answer 1

這聽起來像一個SMT解算器等Yices或Z3會幫助你。他們對你的問題有點「大槍」，但應該這樣做。 SMT解算器就像SAT類固醇解算器一樣，使用非布爾變量有效地解決了可滿足性問題。

Answer 2

一個簡單的替代一個SMT解算器將是：

1. 提取在表達式中使用
2. 排序號碼列表
3. 對於列表中的X的每個點的所有號碼，評估表達式在x-eps，x和x + eps（其中eps是一個小數字）

表達式的值只能在這些點上改變，並且因爲它們按排序順序可以簡單地加入結果tog以查找x的完整允許值列表。