clause.h File Reference

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

Go to the source code of this file.

Classes

• class CVC3::ClauseValue
• class CVC3::Clause

  A class representing a CNF clause (a smart pointer). More...
  

• class CVC3::ClauseOwner

  Same as class Clause, but when destroyed, marks the clause as deleted. More...
  

• class CVC3::CompactClause

Namespaces

• namespace CVC3

---

Detailed Description

Author: Sergey Berezin

Created: Fri Mar 7 16:03:38 2003

---

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.

---

Class to represent a clause, which is a disjunction of formulas which are literals for conflict clauses, and possibly more complex formulas for the clauses derived from the user-asserted formulas.

class Clause is implemented as a smart pointer to ClauseValue, so it can be freely copied and assigned with low overhead (like Theorem or Expr).

Definition in file clause.h.