Begrenzte Ganzzahlen in z3 definieren

Gibt es eine intelligente Methode, um in Z3 ganze Zahlen zu definieren?Begrenzte Ganzzahlen in z3 definieren

Zum Beispiel möchte ich eine ganzzahlige Variable "x" definieren, die Werte aus [1,4] nehmen kann. Ich kann die folgende tun (ich bin mit dem Java API)

IntExpr x = ctx.mkIntConst("x"); 
solver.add(ctx.mkGT(x, ctx.mkInt(0))); // (assert (> x 0)) 
solver.add(ctx.mkLT(x, ctx.mkInt(5))); // (assert (< x 5))

Allerdings frage ich mich, ob es eine intelligentere Art und Weise, dies zu tun? Etwas, das bei der Deklaration automatisch Ober-/Untergrenzen für Variablen festlegen kann. Ich bin über Aufzählungen gekommen, aber ich bin mir nicht sicher, ob das die beste Wahl ist.

Dank

Quelle

2017-06-29 Mohammed

Wenn sie Potenzen von zwei sind, verwenden Sie nur Bit-Vektoren. Sonst gibt es keinen einfachen Weg, dies zu tun (d. H. Du machst es richtig).

Quelle

2017-06-29 22:23:14

Leider gibt es keine "gute" Möglichkeit, solche Einschränkungen zu modellieren. Bitvektoren gehen weit, vorausgesetzt, Sie sind in Ordnung mit Rechnerarithmetik (d. H. Modular) und Ihr Bereich passt gut, wie bereits erwähnt. Hier ist eine vorherige verwandte Diskussion: Is there an UnsignedIntSort in Z3?.

Um zu unterstützen, was Sie wollen, würde man Prädikat-Subtyping benötigen. Theorembeweiser wie PVS und ältere Versionen von Yices (Pre-SMTLib-Varianten der 1.X-Serie) unterstützten solche ausgefallenen Typen mit unterschiedlichem Automatisierungsgrad. Wenn Sie sich an einen modernen SMT-Löser halten müssen, haben Sie leider keine andere Wahl, als Ihren Code mit vielen Einschränkungen zu versehen. Es kann natürlich ziemlich schnell ziemlich hässlich werden, da Sie die Grenzen nach jeder Operation überprüfen und definieren müssen, was es bedeutet, zu über-/unterlaufen. Ein geeigneter Theorembeweiser könnte eine bessere Wahl sein, wenn die Grenzen respektiert werden müssen.

Quelle

2017-06-30 05:42:09

Dank Levent, meine einzige Sorge war der Suchraum. Das Hinzufügen der gebundenen Beschränkungen wird Z2 behutsam helfen, eine beträchtliche Anzahl von irrelevanten Lösungen zu reduzieren, aber diese Lösungen sind immer noch da und Z3 betrachtete sie zu einem bestimmten Zeitpunkt. Ich mag mich irren und es könnte dasselbe sein, aber wenn in Z3 beschränkte ganze Zahlen existieren, dann könnte es sein, dass diese irrelevante Lösung von Anfang an nie da war. Wie auch immer, ich werde mich vorerst an die Grenzen halten. – Mohammed

@Mohammed Hinzufügen von * redundanten * oberen und unteren Grenzen zu Variablen oder Kombinationen davon, kann die Suche ein wenig beschleunigen, selbst wenn diese * Constraints * aus bestehenden Constraints abgeleitet werden können (zB siehe [Wie berechnet man WCET .... ] (http://dl.acm.org/citation.cfm?id=2597817&dl=ACM&coll=DL&CFID=780316479&CFTOKEN=19429447)). Nachdem dies gesagt wurde, ist die Vorhersage der Laufzeit eines * smt * Solvers in diesem Fall wie das Werfen einer Münze, es gibt mehrere Faktoren, die ins Spiel kommen, einschließlich der Struktur des betrachteten Problems, d. wie der Boolean Teil mit den LAR Constraints * interagiert. –

Begrenzte Ganzzahlen in z3 definieren

Antwort

Verwandte Themen