GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/unsat_core_manager.cpp Lines: 42 45 93.3 %
Date: 2021-08-01 Branches: 62 168 36.9 %

Line Exec Source
1
/******************************************************************************
2
 * Top contributors (to current version):
3
 *   Haniel Barbosa
4
 *
5
 * This file is part of the cvc5 project.
6
 *
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.
11
 * ****************************************************************************
12
 *
13
 * Implementation of the unsat core manager of SmtEngine.
14
 */
15
16
#include "unsat_core_manager.h"
17
18
#include "proof/proof_node_algorithm.h"
19
#include "smt/assertions.h"
20
21
namespace cvc5 {
22
namespace smt {
23
24
1419
void UnsatCoreManager::getUnsatCore(std::shared_ptr<ProofNode> pfn,
25
                                    Assertions& as,
26
                                    std::vector<Node>& core)
27
{
28
2838
  Trace("unsat-core") << "UCManager::getUnsatCore: final proof: " << *pfn.get()
29
1419
                      << "\n";
30
1419
  Assert(pfn->getRule() == PfRule::SCOPE);
31
2838
  std::vector<Node> fassumps;
32
1419
  expr::getFreeAssumptions(pfn->getChildren()[0].get(), fassumps);
33
2838
  Trace("unsat-core") << "UCManager::getUnsatCore: free assumptions: "
34
1419
                      << fassumps << "\n";
35
1419
  context::CDList<Node>* al = as.getAssertionList();
36
1419
  Assert(al != nullptr);
37
19722
  for (context::CDList<Node>::const_iterator i = al->begin(); i != al->end();
38
       ++i)
39
  {
40
18303
    Trace("unsat-core") << "is assertion " << *i << " there?\n";
41
18303
    if (std::find(fassumps.begin(), fassumps.end(), *i) != fassumps.end())
42
    {
43
6080
      Trace("unsat-core") << "\tyes\n";
44
6080
      core.push_back(*i);
45
    }
46
  }
47
1419
  if (Trace.isOn("unsat-core"))
48
  {
49
    Trace("unsat-core") << "UCManager::getUnsatCore():\n";
50
    for (const Node& n : core)
51
    {
52
      Trace("unsat-core") << "- " << n << "\n";
53
    }
54
  }
55
1419
}
56
57
7
void UnsatCoreManager::getRelevantInstantiations(
58
    std::shared_ptr<ProofNode> pfn,
59
    std::map<Node, std::vector<std::vector<Node>>>& insts)
60
{
61
14
  std::unordered_map<ProofNode*, bool> visited;
62
7
  std::unordered_map<ProofNode*, bool>::iterator it;
63
14
  std::vector<std::shared_ptr<ProofNode>> visit;
64
65
14
  std::shared_ptr<ProofNode> cur;
66
7
  visit.push_back(pfn);
67
317
  do
68
  {
69
324
    cur = visit.back();
70
324
    visit.pop_back();
71
324
    it = visited.find(cur.get());
72
324
    if (it != visited.end())
73
    {
74
38
      continue;
75
    }
76
286
    visited[cur.get()] = true;
77
286
    const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
78
286
    if (cur->getRule() == PfRule::INSTANTIATE)
79
    {
80
17
      const std::vector<Node>& instTerms = cur->getArguments();
81
17
      Assert(cs.size() == 1);
82
34
      Node q = cs[0]->getResult();
83
      // the instantiation is a prefix of the arguments up to the number of
84
      // variables
85
51
      insts[q].push_back(
86
51
          {instTerms.begin(), instTerms.begin() + q[0].getNumChildren()});
87
    }
88
603
    for (const std::shared_ptr<ProofNode>& cp : cs)
89
    {
90
317
      visit.push_back(cp);
91
    }
92
324
  } while (!visit.empty());
93
7
}
94
95
}  // namespace smt
96
29280
}  // namespace cvc5