CVCL::SVC_API_impl Class Reference

#include <vc_api.h>

List of all members.

Public Member Functions

• SVC_API_impl (Expr_Manager *pem)
• ~SVC_API_impl ()
• bool CheckSat (const Expr &e)
• void Push ()
• void Pop ()
• bool SVCAssert (long lVar)
• bool SVCDeny (long lVar)
• bool GetConfClause (std::vector< int > *literals)
• bool IsConsistent ()
• bool HasSVCExpr (long lVar)
• bool OKToSplit (long lVar)
• void ResetVariable (long v)
• void Connect (const Expr &e, long v)
• void Connect1 (const Expr &eFrom, const Expr &eTo)
• bool FindSplitter (long *v)
• void GetImplications (long *pv, int *pvalue)
• void SetVerbosity (int i)
• int Verbosity ()
• void PrintVar (long lVar)
• void PrintWithType (const Expr &e)
• void Reset (void)
• bool Ready (void)
• PSAT_API SatAPI ()
• std::vector< Expr > & VecMap ()

Protected Member Functions

• bool AddConditions (long lVar)
• void UpdateValue (long v, int value)
• bool FindSplitterRec (long v, int value, long *pv)
• bool GetImplicationsRec (long v, long *pv, int *pvalue)
• bool IsStable ()

Protected Attributes

• Expr_Manager * _pem
• Prop_Var_Manager * _ppvm
• std::hash_map< int, std::vector<
  Expr > * > * _pfanout_table
• std::vector< Expr > _vecMap
• std::vector< Expr > _connectQueue
• std::vector< Expr > _conditions
• std::vector< int > _conditionVars
• std::vector< int > _conditionIndex
• std::vector< Expr > _assumptionStack
• std::vector< int > _assumptionIndex
• int _verbosity
• PAtomifier _patomifier
• CNF_Formula_For_Exprs * _cnfFormula
• CNF_Converter * _cnfConverter
• PSAT_API _psatapi
• bool _ready
• std::vector< varinfo > _vars
• int _splitterCacheTag
• int _splitterCacheTag2

Classes

• class varinfo

---

Detailed Description

Definition at line 18 of file vc_api.h.

---

Constructor & Destructor Documentation

CVCL::SVC_API_impl::SVC_API_impl (  Expr_Manager *  pem  )

CVCL::SVC_API_impl::~SVC_API_impl (   )

---

Member Function Documentation

bool CVCL::SVC_API_impl::AddConditions (  long  lVar  )  [protected]

void CVCL::SVC_API_impl::UpdateValue (  long  v, int  value )  [protected]

bool CVCL::SVC_API_impl::FindSplitterRec (  long  v, int  value, long *  pv )  [protected]

bool CVCL::SVC_API_impl::GetImplicationsRec (  long  v, long *  pv, int *  pvalue )  [protected]

bool CVCL::SVC_API_impl::IsStable (   )  [inline, protected]

Definition at line 57 of file vc_api.h.

bool CVCL::SVC_API_impl::CheckSat (  const Expr &  e  )

void CVCL::SVC_API_impl::Push (   )

void CVCL::SVC_API_impl::Pop (   )

bool CVCL::SVC_API_impl::SVCAssert (  long  lVar  )

bool CVCL::SVC_API_impl::SVCDeny (  long  lVar  )

bool CVCL::SVC_API_impl::GetConfClause (  std::vector< int > *  literals  )

bool CVCL::SVC_API_impl::IsConsistent (   )

bool CVCL::SVC_API_impl::HasSVCExpr (  long  lVar  )

bool CVCL::SVC_API_impl::OKToSplit (  long  lVar  )

void CVCL::SVC_API_impl::ResetVariable (  long  v  )

void CVCL::SVC_API_impl::Connect (  const Expr &  e, long  v )

void CVCL::SVC_API_impl::Connect1 (  const Expr &  eFrom, const Expr &  eTo )

bool CVCL::SVC_API_impl::FindSplitter (  long *  v  )

void CVCL::SVC_API_impl::GetImplications (  long *  pv, int *  pvalue )

void CVCL::SVC_API_impl::SetVerbosity (  int  i  )  [inline]

Definition at line 81 of file vc_api.h. References _patomifier, and _verbosity.

int CVCL::SVC_API_impl::Verbosity (   )  [inline]

Definition at line 82 of file vc_api.h. References _verbosity.

void CVCL::SVC_API_impl::PrintVar (  long  lVar  )

void CVCL::SVC_API_impl::PrintWithType (  const Expr &  e  )

void CVCL::SVC_API_impl::Reset (  void   )

bool CVCL::SVC_API_impl::Ready (  void   )

PSAT_API CVCL::SVC_API_impl::SatAPI (   )  [inline]

Definition at line 88 of file vc_api.h. References _psatapi.

std::vector<Expr>& CVCL::SVC_API_impl::VecMap (   )  [inline]

Definition at line 89 of file vc_api.h. References _vecMap.

---

Member Data Documentation

Expr_Manager* CVCL::SVC_API_impl::_pem [protected]

Definition at line 20 of file vc_api.h.

Prop_Var_Manager* CVCL::SVC_API_impl::_ppvm [protected]

Definition at line 21 of file vc_api.h.

std::hash_map<int, std::vector<Expr>*>* CVCL::SVC_API_impl::_pfanout_table [protected]

Definition at line 22 of file vc_api.h.

std::vector<Expr> CVCL::SVC_API_impl::_vecMap [protected]

Definition at line 23 of file vc_api.h. Referenced by VecMap().

std::vector<Expr> CVCL::SVC_API_impl::_connectQueue [protected]

Definition at line 24 of file vc_api.h.

std::vector<Expr> CVCL::SVC_API_impl::_conditions [protected]

Definition at line 25 of file vc_api.h.

std::vector<int> CVCL::SVC_API_impl::_conditionVars [protected]

Definition at line 26 of file vc_api.h.

std::vector<int> CVCL::SVC_API_impl::_conditionIndex [protected]

Definition at line 27 of file vc_api.h.

std::vector<Expr> CVCL::SVC_API_impl::_assumptionStack [protected]

Definition at line 28 of file vc_api.h.

std::vector<int> CVCL::SVC_API_impl::_assumptionIndex [protected]

Definition at line 29 of file vc_api.h.

int CVCL::SVC_API_impl::_verbosity [protected]

Definition at line 30 of file vc_api.h. Referenced by SetVerbosity(), and Verbosity().

PAtomifier CVCL::SVC_API_impl::_patomifier [protected]

Definition at line 32 of file vc_api.h. Referenced by SetVerbosity().

CNF_Formula_For_Exprs* CVCL::SVC_API_impl::_cnfFormula [protected]

Definition at line 33 of file vc_api.h.

CNF_Converter* CVCL::SVC_API_impl::_cnfConverter [protected]

Definition at line 34 of file vc_api.h.

PSAT_API CVCL::SVC_API_impl::_psatapi [protected]

Definition at line 35 of file vc_api.h. Referenced by SatAPI().

bool CVCL::SVC_API_impl::_ready [protected]

Definition at line 36 of file vc_api.h.

std::vector<varinfo> CVCL::SVC_API_impl::_vars [protected]

Definition at line 49 of file vc_api.h.

int CVCL::SVC_API_impl::_splitterCacheTag [protected]

Definition at line 50 of file vc_api.h.

int CVCL::SVC_API_impl::_splitterCacheTag2 [protected]

Definition at line 51 of file vc_api.h.

---

The documentation for this class was generated from the following file:

• vc_api.h

---