GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/unsat_core_manager.cpp Lines: 24 44 54.5 %
Date: 2021-03-23 Branches: 23 164 14.0 %

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