smt

0Hitze

1Antwort

So erstellen Sie eine Schnittstelle für Solver-Objekt und verwenden Sie es (Z3-Solver)

Ich bin neu in C#. Ich habe eine Klasse mit einigen Methoden, die das Solver-Objekt verwenden. Aber für jede Methode muss ich erneut eine Instanz des Solver-Objekts erstellen, um es zu verwenden. Kann

2Hitze

1Antwort

y = 1/x, x = 0 erfüllbar in den Realen?

In SMT-LIB: (declare-fun y() Real) (declare-fun x() Real) (assert (= 0.0 x)) (assert (= y (/ 1.0 x))) (check-sat) Sollte dieses Modell SAT oder UNSAT sein?

2Hitze

1Antwort

Gibt es eine Möglichkeit, SMT-Solver zu verwenden, um herauszufinden, wie Funktionen zusammengesetzt werden?

Ich bin ein Anfänger zu SMT-Lösern und ich versuche, sie für eine Variation der Programmsynthese zu verwenden. Wie auch immer, worauf das Problem hinausläuft, ist eine Folge von angewandten Operatione

1Hitze

1Antwort

Definieren einer Funktion in Z3 durch seine Java-Implementierung?

Also hier ist was ich versuche zu tun. Lassen Sie uns sagen, dass ich den Wert von op mit Z3 (und seine Java-Bindung) in einem Ausdruck ähnlich wie diese finden wollen: ((exists (op Int)) (= (foo op)

0Hitze

1Antwort

Multiplikation mit Konstante in den wenigsten Hinzufügungen und Verschiebungen

Es ist möglich, zwei Zahlen zu multiplizieren, indem Sie nur addition, subtraction and shift verwenden. Der wichtige Teil des Verfahrens besteht darin, die minimale (optimale) Abfolge solcher Operatio

2Hitze

1Antwort

Z3Opt C++ API: parse smtlib2 Formel aus Datei

Gibt es eine Möglichkeit in der Z3Opt C++ API smtlib2 Datei zu analysieren? Also, im Grunde versuche ich, die Z3Opt-Formel in eine Datei zu schreiben und sie dann in einem anderen Programm zu lesen. D

3Hitze

1Antwort

Unterschied zwischen `Z3_mk_forall` und` Z3_mk_forall_const` in C-API für Z3?

Ich bin durch die 2 Funktionen verwirrt. Sie scheinen ungefähr die gleichen Argumente zu haben (eine, die einfach in eine andere konvertierbar ist) und jeder gibt eine AST zurück. Tun die Funktionen d

1Hitze

1Antwort

Warum kann Z3 nicht beweisen/zugeben, dass `is_int` bei einigen Operationen geschlossen ist?

Zum Beispiel der folgenden Abfrage mal aus: (declare-const x Real) (declare-const y Real) (assert (is_int x)) (assert (is_int y)) (assert (not (is_int (+ x y)))) (check-sat) Soweit ich, die Z3

0Hitze

1Antwort

z3 falsch sagen UNSAT

Für das Problem unten existiert Lösung, aber z3 sagt UNSAT. (set-logic QF_UFNRA) (declare-fun a() Real) (declare-fun b() Real) (declare-fun c() Real) (declare-fun d() Real) (declare-fun e() Real)

0Hitze

1Antwort

Ändern der Reihenfolge der Z3 fixepoint Abfragen ändert das Ergebnis

Ich versuche, herauszufinden, warum Abfrage Aufträge Swapping kann die Antwort von Z3 FixedPoint Motor ändern: (declare-rel fib (Int Int)) (declare-rel q1()) (declare-rel q2()) (declare-var n Int)