GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arrays/skolem_cache.cpp Lines: 23 24 95.8 %
Date: 2021-03-22 Branches: 56 176 31.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file skolem_cache.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Arrays skolem cache
13
 **/
14
15
#include "theory/arrays/skolem_cache.h"
16
17
#include "expr/attribute.h"
18
#include "expr/bound_var_manager.h"
19
#include "expr/skolem_manager.h"
20
#include "expr/type_node.h"
21
22
using namespace CVC4::kind;
23
24
namespace CVC4 {
25
namespace theory {
26
namespace arrays {
27
28
/**
29
 * A bound variable corresponding to an index for witnessing the satisfiability
30
 * of array disequalities.
31
 */
32
struct ExtIndexVarAttributeId
33
{
34
};
35
typedef expr::Attribute<ExtIndexVarAttributeId, Node> ExtIndexVarAttribute;
36
37
SkolemCache::SkolemCache() {}
38
39
705
Node SkolemCache::getExtIndexSkolem(Node deq)
40
{
41
705
  Assert(deq.getKind() == NOT && deq[0].getKind() == EQUAL);
42
1410
  Node a = deq[0][0];
43
1410
  Node b = deq[0][1];
44
705
  Assert(a.getType().isArray());
45
705
  Assert(b.getType() == a.getType());
46
47
705
  NodeManager* nm = NodeManager::currentNM();
48
49
  // get the reference index, which notice is deterministic for a, b in the
50
  // lifetime of the node manager
51
1410
  Node x = getExtIndexVar(deq);
52
53
  // make the axiom for x
54
1410
  Node as = nm->mkNode(SELECT, a, x);
55
1410
  Node bs = nm->mkNode(SELECT, b, x);
56
1410
  Node deqIndex = as.eqNode(bs).notNode();
57
1410
  Node axiom = nm->mkNode(IMPLIES, deq, deqIndex);
58
59
  // make the skolem that witnesses the above axiom
60
705
  SkolemManager* sm = nm->getSkolemManager();
61
  return sm->mkSkolem(
62
      x,
63
      axiom,
64
      "array_ext_index",
65
1410
      "an extensional lemma index variable from the theory of arrays");
66
}
67
68
705
Node SkolemCache::getExtIndexVar(Node deq)
69
{
70
1410
  Node a = deq[0][0];
71
1410
  TypeNode atn = a.getType();
72
705
  Assert(atn.isArray());
73
705
  Assert(atn == deq[0][1].getType());
74
1410
  TypeNode atnIndex = atn.getArrayIndexType();
75
705
  BoundVarManager* bvm = NodeManager::currentNM()->getBoundVarManager();
76
1410
  return bvm->mkBoundVar<ExtIndexVarAttribute>(deq, atnIndex);
77
}
78
79
}  // namespace arrays
80
}  // namespace theory
81
26676
}  // namespace CVC4