Quelle est la meilleure façon de rejouer une "session"

Question

Dans une première phase, je collecte une liste de contraintes. Ensuite, je voudrais stocker cette "session", c'est-à-dire toutes les contraintes mais aussi toutes les variables associées dans un fichier pour pouvoir, dans un deuxième temps, relire les contraintes et les affirmer, voire les annuler avant d'affirmer.

Quelle est la meilleure façon (rapide et fiable) de stocker une telle "session" dans un fichier, et de la relire? Est-ce que l'API Z3_parse_smtlib2_file() serait la bonne? J'ai essayé l'API Z3_open_log(), mais je ne trouve pas l'API pour lire le fichier journal généré par Z3_open_log(). Et qu'en est-il de z3_log_replay(). Cette API ne semble pas encore exposée.

Merci d'avance.

AG

Answer 1

Le fichier journal créé par Z3_open_log() peut être rejoué avec Z3.exe (interprète autonome, pas la lib) via l'option de ligne de commande/log monfichier. À ce jour, je n'ai vu aucune API dans la bibliothèque Z3 qui permet une telle relecture. Pour l'instant, j'ai compris que la relecture est réputée pour l'analyse de débogage.

Cependant, vous pouvez pirater la bibliothèque (il suffit d'exposer la classe z3_replayer dans z3_replayer.h) et l'utiliser pour rejouer n'importe quel fichier journal, c'est assez facile. Le code source de ma petite preuve de faisabilité est donné ci-dessous, et fonctionne bien pour autant que je sache. Je pense que c'est très agréable de pouvoir le faire parce que parfois j'ai besoin de rejouer une session à des fins de débogage. C'est bien de pouvoir le rejouer à partir d'un fichier, plutôt que de tout mon programme qui est un peu lourd.

Tous les commentaires seraient les bienvenus. Aussi je serais intéressé de savoir si cette fonctionnalité pourrait être intégrée dans la lib, ou non.

AG.

#include <fstream> 
#include <iostream> 
#include "api/z3_replayer.h" 


int main(int argc, char * argv[]) 
{ 
    const char * filename = argv[1]; 
    std::ifstream in(filename); 
    if (in.bad() || in.fail()) { 
     std::cerr << "Error: failed to open file: " << filename << "\n"; 
     exit(EXIT_FAILURE); 
} 
    z3_replayer r(in); 
    r.parse(); 

    Z3_context ctx = reinterpret_cast<Z3_context>(r.get_obj(0)); 

    check(ctx,Z3_L_TRUE); // this function is taken from the c examples 

    return 0; 
}