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

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.