variable.h File Reference
#include "expr.h"#include "clause.h"
Include dependency graph for variable.h:
This graph shows which files directly or indirectly include this file:
Go to the source code of this file.
Classes
- class CVC3::Variable
- class CVC3::Literal
- class CVC3::VariableValue
- class CVC3::VariableManager
- class CVC3::VariableManager::VariableManager::HashLV
- class CVC3::VariableManager::VariableManager::EqLV
- class CVC3::VariableManagerNotifyObj
- Notifies VariableManager before and after each pop(). More...
- Notifies VariableManager before and after each pop(). More...
Namespaces
- namespace CVC3
Functions
- Literal CVC3::operator! (const Variable &v)
- Literal CVC3::operator! (const Literal &l)
- std::ostream & CVC3::operator<< (std::ostream &os, const Literal &l)
Detailed Description
Author: Sergey BerezinCreated: Fri Apr 25 11:52:17 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.
A data structure representing a variable in the search engine. It is a smart pointer with a uniquifying mechanism similar to Expr, and a variable is uniquely determined by its expression. It can be thought of as an Expr with additional attributes, but the type is different, so it will not be confused with other Exprs.
Definition in file variable.h.
