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

using namespace z3;


/**
   De Morgan's Duality Law: {e not(x and y) <-> (not x) or ( not y) }
*/
 
 
int main(){

context c; 
expr  x  = c.bool_const("x"); 
expr  y  = c.bool_const("y"); 
expr conjecture = !(x && y) == (!x || !y); 

//create a solver 
solver s(c); 

//assert the negation of conjecture 
s.add(!conjecture); 

std::cout << s << "\n";
std::cout << s.to_smt2() << "\n"; 

//check if the result if unsat
switch (s.check()) {
case unsat: std::cout << "demorgan is valid\n"; break;
case sat: std::cout << "demorgan is not valid\n"; break;
case unknown: std::cout <<"unknown\n"; break; 
}
} //end of function