Z3: Можно ли упростить только часть утверждений?

Question

Я использую Java-API для Z3 версии 4.3.2 для 64-разрядной версии Windows 7, а также для Java 7 64-bit, но я не думаю, что Java - это необходимость ответить на этот вопрос.

Прямо сейчас я использую следующий Java-код, чтобы упростить подмножество моих утверждений в Z3:

Tactic simplifyTactic = ctx.mkTactic("ctx-solver-simplify"); 
Goal goal = ctx.mkGoal(true, false, false); 
goal.add(bel.toArray(new BoolExpr[0])); // bel is List<BoolExpr> 
ApplyResult applyResult = simplifyTactic.apply(goal); 

До сих пор я фильтруется утверждения должны быть упрощены, прежде чем их упрощения с помощью приведенного выше кода, который работает, как ожидалось.

После некоторого тестирования я пришел к выводу, что мне нужно также вставить отфильтрованные утверждения (содержащие некоторую метаинформацию, такую ​​как мощность) модели.

Можно ли упростить некоторое множество утверждений А, в то время как другое множество утверждений В все еще рассматривается, но не изменяется?

Следующий пример может прояснить этот вопрос немного:

(declare-const a Bool) 
(declare-const b Bool) 
(declare-const c Bool) 
(declare-const d Bool) 

(assert (=> a c)); member of set A 
(assert (=> b d)); member of set A 
(assert a); member of set A 

; member of set B 
(assert 
    (<= 
     (+ (ite (= c true) 1 0) (ite (= d true) 1 0)) 
     1 
    ) 
) 

; member of set B 
(assert 
    (>= 
     (+ (ite (= c true) 1 0) (ite (= d true) 1 0)) 
     1 
    ) 
) 

(apply ctx-solver-simplify) 

Если это SMT-LIB V2 код выполняется с помощью Z3 результат:

(goals 
    (goal 
     c 
     (not b) 
     a 
     (<= (+ (ite (= c true) 1 0) (ite (= d true) 1 0)) 1) 
     :precision precise :depth 1 
    ) 
) 

В этом простом примере результат вполне нормально. Ограничения (первые три утверждения (мой набор А)) были упрощены, как ожидалось. Также было упрощено следующее два утверждения (с моей информацией о мощности (множество B)). Теперь я хочу, чтобы Z3 выполнял упрощения, но не смешивая результаты множества A и B. Учитывая более сложные утверждения, это произойдет (и произошло в моем случае).

Как это делается?

Answer 1

Для упрощения необходимо добавить как A, так и B. Следующий сценарий использует идею проверки того, что каждое утверждение e в упрощенном результате равно любому утверждению edel в наборе B, и если да, то без учета e в упрощенном результате все выполняется после первоначального упрощения с использованием как A, так и B , Разумеется, вы также можете просто удалить все утверждения в B из упрощенного результата указателями, но это может завершиться неудачно, если утверждения в B будут преобразованы (как в случае, когда я запустил ваш пример в z3py вместо SMT-интерфейса Z3) поэтому это мотивирует доказательство того, являются ли утверждения равными или нет, как это делает сценарий.

Он дополнительно проверяет соединение всех утверждений в B. В общем, вам, возможно, придется рассмотреть их перестановки (например, соединения пар, тройки и т. Д. Утверждений в B), что может сделать его нецелесообразным, но, возможно, оно будет работать для ваших целей. Он работает для приведенного примера. Вот сценарий в z3py (ссылка на rise4fun: http://rise4fun.com/Z3Py/slY6):

a,b,c,d = Bools('a b c d') 
g = Goal() 

A = [] 
A.append(Implies(a, c)) 
A.append(Implies(b, d)) 
A.append(a) 

B = [] 
B.append((If(c == True, 1, 0) + (If(d == True, 1, 0))) <= 1) 
B.append((If(c == True, 1, 0) + (If(d == True, 1, 0))) >= 1) 

g.add(A) 
g.add(B) 

#t = Tactic('simplify') 
#print t(g) # note difference 

t = Tactic('ctx-solver-simplify') 
ar = t(g) 
print ar # [[c, Not(b), a, If(d, 1, 0) <= 0]] 

s = Solver() 
s.add(A) 
result = [] 
for e in ar[0]: # iterate over expressions in result 
    # try to prove equal 
    s.push() 
    s.add(Not(e == And(B))) # conunction of all assertions in B 
    satres = s.check() 
    s.pop() 
    if satres == unsat: 
    continue 

    # check each in B individually 
    for edel in B: 
    # try to prove equal 
    s.push() 
    s.add(Not(e == edel)) 
    satres = s.check() 
    s.pop() 
    if satres != unsat: 
     result.append(e) 
     break 

print result # [c, Not(b), a]