GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arrays/inference_manager.cpp Lines: 50 58 86.2 %
Date: 2021-03-22 Branches: 78 202 38.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inference_manager.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer
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 inference manager
13
 **/
14
15
#include "theory/arrays/inference_manager.h"
16
17
#include "options/smt_options.h"
18
#include "theory/theory.h"
19
#include "theory/theory_state.h"
20
#include "theory/uf/equality_engine.h"
21
22
using namespace CVC4::kind;
23
24
namespace CVC4 {
25
namespace theory {
26
namespace arrays {
27
28
8995
InferenceManager::InferenceManager(Theory& t,
29
                                   TheoryState& state,
30
8995
                                   ProofNodeManager* pnm)
31
    : TheoryInferenceManager(t, state, pnm, "theory::arrays", false),
32
      d_lemmaPg(pnm ? new EagerProofGenerator(pnm,
33
962
                                              state.getUserContext(),
34
962
                                              "ArrayLemmaProofGenerator")
35
10919
                    : nullptr)
36
{
37
8995
}
38
39
13252
bool InferenceManager::assertInference(TNode atom,
40
                                       bool polarity,
41
                                       InferenceId id,
42
                                       TNode reason,
43
                                       PfRule pfr)
44
{
45
26504
  Trace("arrays-infer") << "TheoryArrays::assertInference: "
46
26504
                        << (polarity ? Node(atom) : atom.notNode()) << " by "
47
13252
                        << reason << "; " << id << std::endl;
48
13252
  Assert(atom.getKind() == EQUAL);
49
  // if proofs are enabled, we determine which proof rule to add, otherwise
50
  // we simply assert the internal fact
51
13252
  if (isProofEnabled())
52
  {
53
2436
    Node fact = polarity ? Node(atom) : atom.notNode();
54
2436
    std::vector<Node> children;
55
2436
    std::vector<Node> args;
56
    // convert to proof rule application
57
1218
    convert(pfr, fact, reason, children, args);
58
1218
    return assertInternalFact(atom, polarity, id, pfr, children, args);
59
  }
60
12034
  return assertInternalFact(atom, polarity, id, reason);
61
}
62
63
6934
bool InferenceManager::arrayLemma(
64
    Node conc, InferenceId id, Node exp, PfRule pfr, LemmaProperty p)
65
{
66
13868
  Trace("arrays-infer") << "TheoryArrays::arrayLemma: " << conc << " by " << exp
67
6934
                        << "; " << id << std::endl;
68
6934
  NodeManager* nm = NodeManager::currentNM();
69
6934
  if (isProofEnabled())
70
  {
71
880
    std::vector<Node> children;
72
880
    std::vector<Node> args;
73
    // convert to proof rule application
74
440
    convert(pfr, conc, exp, children, args);
75
    // make the trusted lemma based on the eager proof generator and send
76
880
    TrustNode tlem = d_lemmaPg->mkTrustNode(conc, pfr, children, args);
77
440
    return trustedLemma(tlem, id, p);
78
  }
79
  // send lemma without proofs
80
12988
  Node lem = nm->mkNode(IMPLIES, exp, conc);
81
6494
  return lemma(lem, id, p);
82
}
83
84
1658
void InferenceManager::convert(PfRule& id,
85
                               Node conc,
86
                               Node exp,
87
                               std::vector<Node>& children,
88
                               std::vector<Node>& args)
89
{
90
  // note that children must contain something equivalent to exp,
91
  // regardless of the PfRule.
92
1658
  switch (id)
93
  {
94
35
    case PfRule::MACRO_SR_PRED_INTRO:
95
35
      Assert(exp.isConst());
96
35
      args.push_back(conc);
97
35
      break;
98
1158
    case PfRule::ARRAYS_READ_OVER_WRITE:
99
1158
      if (exp.isConst())
100
      {
101
        // Premise can be shown by rewriting, use standard predicate intro rule.
102
        // This is the case where we have 2 constant indices.
103
21
        id = PfRule::MACRO_SR_PRED_INTRO;
104
21
        args.push_back(conc);
105
      }
106
      else
107
      {
108
1137
        children.push_back(exp);
109
1137
        args.push_back(conc[0]);
110
      }
111
1158
      break;
112
    case PfRule::ARRAYS_READ_OVER_WRITE_CONTRA: children.push_back(exp); break;
113
279
    case PfRule::ARRAYS_READ_OVER_WRITE_1:
114
279
      Assert(exp.isConst());
115
279
      args.push_back(conc[0]);
116
279
      break;
117
186
    case PfRule::ARRAYS_EXT: children.push_back(exp); break;
118
    default:
119
      if (id != PfRule::ARRAYS_TRUST)
120
      {
121
        Assert(false) << "Unknown rule " << id << "\n";
122
      }
123
      children.push_back(exp);
124
      args.push_back(conc);
125
      id = PfRule::ARRAYS_TRUST;
126
      break;
127
  }
128
1658
}
129
130
}  // namespace arrays
131
}  // namespace theory
132
26676
}  // namespace CVC4