clause.h File Reference

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

Go to the source code of this file.

Namespaces

Classes


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.


Generated on Wed Nov 18 16:13:39 2009 for CVC3 by  doxygen 1.5.2