Как объявить константы для использования в качестве связанных переменных в Z3_mk_forall_const?

Question

Предположим, я хочу количественно определить x и y в следующей формуле:

f(x,y) <=> x=y 

с помощью Z3_mk_forall_const, Сначала мне нужно построить формулу, которая требует констант х и у типа Z3_ast, С помощью Z3_mk_const создать x и y приводит к глобальной декларации. В идеале я бы хотел этого избежать. Есть ли альтернатива?

Answer 1

Да, есть альтернатива; Вы можете использовать Z3_mk_forall, который использует переменные индексы де Бруйина. Вместо констант вы можете создавать индексированные переменные, используя Z3_mk_bound, а затем передавать массив их сортировок (сортов) и имен (decl_names) в mk_forall или mk_exists.