minisat_types.h File Reference

MiniSat internal types. More...

#include "minisat_global.h"
#include "theorem.h"
#include <vector>

Include dependency graph for minisat_types.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Namespaces

• namespace MiniSat

Classes

• class MiniSat::Lit
• class MiniSat::Clause

Typedefs

• typedef int MiniSat::Var

Functions

• Clause * MiniSat::Clause_new (const vector< Lit > &ps, CVC3::Theorem theorem, int id)
• Clause * MiniSat::Lemma_new (const vector< Lit > &ps, int id, int pushID)

Variables

• const int MiniSat::var_Undef = -1
• const Lit MiniSat::lit_Undef (var_Undef, false)
• const Lit MiniSat::lit_Error (var_Undef, true)

---

Detailed Description

MiniSat internal types.

Author: Alexander Fuchs

Created: Fri Sep 08 11:04:00 2006

---

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 minisat_types.h.

---