SAT::Var Class Reference

#include <cnf.h>

List of all members.

Public Types

• enum Val { UNKNOWN = -1, FALSE_VAL, TRUE_VAL }

  Public Member Functions

  • Var ()
  • Var (int index)
  • operator int ()
  • bool isNull () const
  • void reset ()
  • int getIndex () const
  • bool isVar () const
  • bool operator== (const Var &var) const

  Static Public Member Functions

  • static Val invertValue (Val)

  Private Attributes

  • int d_index

  ---

  Detailed Description

  Definition at line 34 of file cnf.h.

  ---

  Member Enumeration Documentation

  enum SAT::Var::Val

  Enumerator:

  UNKNOWN
  FALSE_VAL
  TRUE_VAL

  Definition at line 37 of file cnf.h.

  ---

  Constructor & Destructor Documentation

  SAT::Var::Var

  (

  )

  [inline]

  Definition at line 39 of file cnf.h.

  SAT::Var::Var

  (

  int

  index

  )

  [inline]

  Definition at line 40 of file cnf.h.

  ---

  Member Function Documentation

  Var::Val SAT::Var::invertValue

  (

  Var::Val

  v

  )

  [inline, static]

  Definition at line 48 of file cnf.h.

  References UNKNOWN.

  Referenced by CVC3::SearchSat::getValue().

  SAT::Var::operator int

  (

  )

  [inline]

  Definition at line 41 of file cnf.h.

  References d_index.

  bool SAT::Var::isNull

  (

  )

  const [inline]

  Definition at line 42 of file cnf.h.

  References d_index.

  Referenced by SAT::CNF_Manager::concreteVar(), SAT::Lit::Lit(), and CVC3::SearchSat::setValue().

  void SAT::Var::reset

  (

  )

  [inline]

  Definition at line 43 of file cnf.h.

  References d_index.

  int SAT::Var::getIndex

  (

  )

  const [inline]

  Definition at line 44 of file cnf.h.

  References d_index.

  Referenced by MiniSat::cvcToMiniSat().

  bool SAT::Var::isVar

  (

  )

  const [inline]

  Definition at line 45 of file cnf.h.

  References d_index.

  Referenced by CVC3::SearchSat::getValue(), SAT::CNF_Manager::numFanins(), and SAT::CNF_Manager::numFanouts().

  bool SAT::Var::operator==

  (

  const Var &

  var

  )

  const [inline]

  Definition at line 46 of file cnf.h.

  References d_index.

  ---

  Member Data Documentation

  int SAT::Var::d_index [private]

  Definition at line 35 of file cnf.h.

  Referenced by getIndex(), isNull(), isVar(), operator int(), operator==(), and reset().

  ---

  The documentation for this class was generated from the following file:
  • cnf.h