CVC3  2.4.1
Classes | Namespaces | Macros
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

Macros

#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.


Macro Definition Documentation

#define _cvc3__include__clause_h_

Definition at line 34 of file clause.h.