Pellet/ConceptCache.c at master · ardax/Pellet · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
#include "ConceptCache.h"
#include "ReazienerUtils.h"
#include "Individual.h"

extern int g_iCommentIndent;

ConceptCache::ConceptCache()
{

}

bool ConceptCache::putSat(ExprNode* pC, bool bIsSatisfiable)
{
  START_DECOMMENT2("ConceptCache::putSat");
  DECOMMENT1("isSatisfiable=%d\n", bIsSatisfiable);
  printExprNodeWComment("[pC]=", pC);

  CachedNode* pCached = NULL;
  ExprNode2CachedNodeMap::iterator iFind = m_mCache.find(pC);
  if( iFind != m_mCache.end() )
    pCached = (CachedNode*)iFind->second;

  if( pCached )
    {
      if( bIsSatisfiable != !pCached->isBottom() )
	assertFALSE("Caching inconsistent results for ");
      END_DECOMMENT("ConceptCache::putSat");
      return FALSE;
    }
  else if( bIsSatisfiable )
    {
      m_mCache[pC] = CachedNode::createSatisfiableNode();
    }
  else
    {
      ExprNode* pNotC = negate2(pC);
      m_mCache[pC] = CachedNode::createBottomNode();
      m_mCache[pNotC] = CachedNode::createTopNode();
    }

  END_DECOMMENT("ConceptCache::putSat");
  return TRUE;
}

bool ConceptCache::put(ExprNode* pC, CachedNode* pCachedNode)
{
  START_DECOMMENT2("ConceptCache::put");
  printExprNodeWComment("[pC]=", pC);
  printExprNodeWComment("CachedNode=", pCachedNode->m_pNode->m_pName);

  if( m_mCache.find(pC) != m_mCache.end() )
    {
      END_DECOMMENT("ConceptCache::putSat");
      return FALSE;
    }

  m_mCache[pC] = pCachedNode;
  END_DECOMMENT("ConceptCache::putSat");
  return TRUE;
}

CachedNode* ConceptCache::getCached(ExprNode* pC)
{
  ExprNode2CachedNodeMap::iterator i = m_mCache.find(pC);
  if( i != m_mCache.end() )
    return (CachedNode*)i->second;
  return NULL;
}

int ConceptCache::getSat(ExprNode* pC)
{
  CachedNode* pCached = getCached(pC);
  return (pCached==NULL)?-1:(pCached->isBottom()?0:1);
}