cnf.h File Reference

Basic classes for reasoning about formulas in CNF. More...

#include <deque>
#include "compat_hash_map.h"
#include "cvc_util.h"
#include "cdo.h"
#include "cdlist.h"
#include "theorem.h"

Go to the source code of this file.

Classes

• class SAT::Var
• class SAT::Lit
• class SAT::Clause
• class SAT::CNF_Formula
• class SAT::CNF_Formula_Impl
• class SAT::CD_CNF_Formula

Namespaces

• namespace SAT

---

Detailed Description

Basic classes for reasoning about formulas in CNF.

Author: Clark Barrett

Created: Mon Dec 12 20:32:33 2005

---

License to use, copy, modify, sell and/or distribute this software and its documentation for any purpose is hereby granted without royalty, subject to the terms and conditions defined in the LICENSE file provided with this distribution.

---

Definition in file cnf.h.