C++ z3

Da Andreabont's Wiki.

z3 è una libreria C++ che fornisce un risolutore automatico di teoremi. Per maggiori informazioni vedere qui.

Compilare

g++ <file_sorgente> -lz3

Codice

#include<vector>
#include"z3++.h"

int main() {
    
    // Creo contesto
    z3::context c;
    z3::expr x = c.bool_const("x");
    z3::expr y = c.bool_const("y");
    
    // Creo congettua
    z3::expr conjecture = (!(x && y)) == (!x || !y);
    
    std::cout << "Congettura: " << conjecture << "\n\n";
    
    // Creo risolutore
    z3::solver s(c);
    
    // Aggiungo la negazione della congettura come asserzione
    s.add(!conjecture);
    
    std::cout << "Rappresentazione: \n" << s << "\n";

    std::cout << "La congettura è ";
    
    switch (s.check()) {
        case z3::unsat:   std::cout << "valida!\n"; break;
        case z3::sat:     std::cout << "non valida!\n"; break;
        case z3::unknown: std::cout << "sconosciuta!\n"; break;
    }

}