Z3 C# API Assertion entfernen

Question

Ich verwende Z3-Solver und Hinzufügen und Verfolgen bestimmter Assertionen. Ich führe meine Analyse in Iterationen durch. Ich habe mich gefragt, ob es möglich ist, eine bestimmte Behauptung zu entfernen und sie durch eine andere zu ersetzen.

Answer 1

Ja, das ist möglich, aber nur indirekt, entweder über Annahmen (die später deaktiviert werden können), oder mit Push/Pop. Siehe auch die folgenden Beiträge und die Verbindungen bereitgestellt:

Soft/Hard constraints in Z3

Incremental solving in Z3 using push command

What is the benifits of incremental solving?