Genau n Codierung in Z3

Question

Ich versuche, "GENAU N" in der UOD (hier Liste) in Z3 zu kodieren. Die Art und Weise habe ich in CBMC (C Bounded Model-Checker) zu erreichen, ist, dass ich Liste definieren _Bool und verwenden Sie einen unsigned int und nur Zustand B1 == N.

// L is the length of the List b1. 
unsigned int B1 = 0 
for i in range(L): 
     B1 = b[i] + B1 
.... 
__CPROVER_assume (B1 == N); 

Es ist nicht gerade nach vorne in Z3 zu sein da die Variablen die Ausdrücke sind, nicht die Typwerte selbst. Also war mein erster Versuch, 'mindestens N' und 'höchstens N' zu kodieren und eine Konjunktion von ihnen zu machen, um 'Exakt N' zu bekommen. Verbessere die ursprüngliche Idee und nutze meine Logik Klasse Ich ersetzte "Höchstens N" durch (Nicht) "Mindestens N + 1". Aber für N> = 5 mit L = ~ 600. Der Code läuft nicht mehr auf meinem 4 Gb RAM-Rechner.

# b1 is the List 
X_list = [] 
for i in range(L-3): 
    for j in range(i+1,L-2): 
    l = And (b1[j], b1[i]) 
    for k in range(j+1,L-1): 
     l1 = And (l, b1[k]) 
     for l in range(k+1,L): 
      X_list.append(And (b1[l], l1)) 
B1 = Or(X_list) 

File "file1.py", line 49, in <module> X_list.append(And (b1[l], l1)) File "/usr/lib/python2.7/dist-packages/z3/z3.py", line 1611, in And return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx) File "/usr/lib/python2.7/dist-packages/z3/z3core.py", line 1653, in Z3_mk_and raise Z3Exception(lib().Z3_get_error_msg(a0, err)) z3.z3types.Z3Exception: out of memory

Gibt es einen besseren Weg, dies in Z3 zu codieren. Vielleicht haben erfahrene Z3-Benutzer eine gute Möglichkeit, sie zu verschlüsseln. Vielen Dank.

Answer 1

Es scheint, Sie wollen pseudo-boolesche Funktionen? Höchstens/genau/genau N Dinge sind wahr? Und möglicherweise mit Koeffizienten?

Wenn ja, hat Z3 direkte Unterstützung für diese Funktionalität, sowohl über SMT-Lib als auch von verschiedenen APIs. siehe Python hier: https://github.com/Z3Prover/z3/blob/b27a4a3593fd15c003d3e30da20b35ac96b7218e/src/api/python/z3/z3.py#L7718-L7793

für SMTLib siehe die Diskussion hier: K-out-of-N constraint in Z3Py