Проверка синтаксической эквивалентности двух ограничений эффективно Z3

Question

Предполагаемые У меня есть два ограничения (c1, c2), и я хочу, чтобы проверить, являются ли они синтаксической идентичны:

c1: f(x)>1 && g(y)=2 
c2: f(x)>1 && g(y)=2 

Вариант 1: Мы могли бы превратить это в выполнимости проблема, как этот пост: Whether two boolexpr are equal

Вариант 2: Мы также могли бы превратить их в строки и сравнить равенство:

if(c1.toString().equals(c2.toString())) 
    ///do somthing 

Но оба этих варианта имеют большие накладные расходы, поскольку размер ограничений увеличивается. например вызывая метод toString() в Expr очень дорог для больших ограничений.

Два вопроса:

1. Как проверить, являются ли два ограничения синтаксически идентичны эффективно Z3 (Java версия)?

2. Если мы не имеем хорошее решение для 1, я рассматриваю писать обертку для Expr объекта и используя фабричный метод, чтобы избежать генераторной дублируется (синтаксически) объектов из Z3. Затем я должен создать свои собственные функции equal() и hashCode(). Но до сих пор я до сих пор не могу найти эффективный способ.

Answer 1

Класс Exprs относится к AST, который имеет equals, compareTo и hashCode функции для этой цели. Поскольку Z3 использует хеш-consing, это очень эффективно, по сути, просто сравнение указателей (и, в Java, литье).

Answer 2

Не совсем ответ, но слишком длинный для комментария.

, вызывающий метод toString() в Expr, очень дорог для больших ограничений.

Я предлагаю рассмотреть реализацию toString. Есть одна возможная причина для медленного: немой конкатенации строк вместо использования StringBuilder. Если это так, то вы можете захотеть обеспечить более быструю реализацию. Однако решение CSP, чья печать занимает слишком много времени, в любом случае довольно бесполезна.

Как проверить, являются ли два ограничения синтаксически идентичны эффективно Z3

Держу пари, что использование toString не путь, как a && b и b && a эквивалентны, но их строковые представления не являются ,

Возможно, вам потребуется нормализовать выражения, используя коммутативность, ассоциативность и, возможно, другие правила. Для этого вам нужны некоторые произвольные, но equals -consistent порядок на условиях.

Вы, разумеется, не хотите проверять все пары ограничений на равенство. Здесь, помещая ограничения в ведра в соответствии с их хеш-кодом, помогает. Не знаю, если предоставленный hashCode можно использовать для этой цели.

Затем я должен создать свои собственные функции equal() и hashCode(). Но до сих пор я до сих пор не могу найти эффективный способ.

После нормализации это должно быть довольно просто. Если вы выполните нормализацию и сопоставьте каждое выражение с каноническим представлением (как это делает String#intern), вы можете использовать ссылочное равенство для equals. Для hashCode вам нужна формула комбинирования для каждого узла дерева, например, можно вычислить хэш-код, как a && bf(111 * ha + hb), где ha и hb являются хэш-коды a и b, соответственно, и f(x) = x^(x>>15) или что-то подобное.