conjunctive_normal_form.h

Go to the documentation of this file.

 
#pragma once
 
#include <vector>
 
#include "sdfg/symbolic/assumptions.h"
#include "sdfg/symbolic/symbolic.h"
 
namespace sdfg {
namespace symbolic {

class CNFException : public std::exception {
public:
    CNFException(const std::string& message) : message_(message) {
    }
    const char* what() const noexcept override {
        return message_.c_str();
    }
 
private:
    std::string message_;
};

typedef std::vector<std::vector<Condition>> CNF;

CNF conjunctive_normal_form(const Condition cond);

bool is_tautology(const std::vector<symbolic::Condition>& clause);
 
} // namespace symbolic
} // namespace sdfg