clause.h File Reference

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

Defines

• #define _cvc3__include__clause_h_

---

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.

---

Define Documentation

#define _cvc3__include__clause_h_

Definition at line 34 of file clause.h.