Classes | Namespaces | Defines

clause.h File Reference

Go to the source code of this file.




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.