Duplizieren eines Z3Context

Question

Ich muss in der Lage sein, eine Z3Context Instanz zu duplizieren, um neue Definitionen zu einer Instanz hinzufügen zu können, ohne die andere zu beeinflussen.

Ist das möglich?

Welchen Teil der API sollte ich betrachten?

Ich erwähne, dass ich die Java API verwende.

Danke

Answer 1

Es gibt keine Methode zum Klonen von Kontexten. Es wäre auch etwas schwierig zu verwenden: Was wären nach dem Klonen eines Kontexts die Zeiger, die den Termen und Formeln im neuen Kontext entsprechen? Stattdessen gibt es verschiedene Übersetzungsmethoden, mit denen Sie Begriffe, Formeln, Löser und Ziele zwischen Kontexten importieren können. Verwenden Sie zum Beispiel

 Z3_ast Z3_API Z3_translate(Z3_context source, Z3_ast a, Z3_context target); 

einen Ausdruck/Formel zwischen zwei Kontexten zu kopieren. Die

 Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target); 

Methode können Sie einen Solver klonen. Sie können den Solver zwischen zwei verschiedenen Kontexten oder demselben Kontext klonen, insbesondere wenn Sie das Klonen nur zum Erkunden verschiedener Varianten von Assertionen verwenden.