GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/proof/cnf_proof.cpp Lines: 47 47 100.0 %
Date: 2021-03-23 Branches: 73 190 38.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cnf_proof.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Andres Noetzli, 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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "proof/cnf_proof.h"
19
20
#include "proof/clause_id.h"
21
#include "proof/proof_manager.h"
22
#include "prop/cnf_stream.h"
23
#include "prop/minisat/minisat.h"
24
#include "prop/sat_solver_types.h"
25
26
namespace CVC4 {
27
28
1826
CnfProof::CnfProof(prop::CnfStream* stream,
29
                   context::Context* ctx,
30
1826
                   const std::string& name)
31
  : d_cnfStream(stream)
32
  , d_clauseToAssertion(ctx)
33
  , d_currentAssertionStack()
34
  , d_cnfDeps()
35
1826
  , d_name(name)
36
{
37
  // Setting the proof object for the CnfStream
38
1826
  d_cnfStream->setProof(this);
39
1826
}
40
41
1826
CnfProof::~CnfProof() {}
42
43
27920
Node CnfProof::getAssertionForClause(ClauseId clause) {
44
27920
  ClauseIdToNode::const_iterator it = d_clauseToAssertion.find(clause);
45
27920
  Assert(it != d_clauseToAssertion.end() && !(*it).second.isNull());
46
27920
  return (*it).second;
47
}
48
49
289451
void CnfProof::registerConvertedClause(ClauseId clause)
50
{
51
289451
  Assert(clause != ClauseIdUndef && clause != ClauseIdError
52
         && clause != ClauseIdEmpty);
53
578902
  Node current_assertion = getCurrentAssertion();
54
55
578902
  Debug("proof:cnf") << "CnfProof::registerConvertedClause " << clause
56
289451
                     << " assertion = " << current_assertion << std::endl;
57
58
289451
  setClauseAssertion(clause, current_assertion);
59
289451
}
60
61
490974
void CnfProof::setClauseAssertion(ClauseId clause, Node expr) {
62
981948
  Debug("proof:cnf") << "CnfProof::setClauseAssertion "
63
490974
                     << clause << " assertion " << expr << std::endl;
64
  // We can add the same clause from different assertions.  In this
65
  // case we keep the first assertion. For example asserting a /\ b
66
  // and then b /\ c where b is an atom, would assert b twice (note
67
  // that since b is top level, it is not cached by the CnfStream)
68
  //
69
  // Note: If the current assertion associated with the clause is null, we
70
  // update it because it means that it was previously added the clause without
71
  // associating it with an assertion.
72
490974
  const auto& it = d_clauseToAssertion.find(clause);
73
490974
  if (it != d_clauseToAssertion.end() && (*it).second != Node::null())
74
  {
75
18727
    return;
76
  }
77
78
472247
  d_clauseToAssertion.insert(clause, expr);
79
}
80
81
217522
void CnfProof::pushCurrentAssertion(Node assertion, bool isInput)
82
{
83
435044
  Debug("proof:cnf") << "CnfProof::pushCurrentAssertion " << assertion
84
217522
                     << std::endl;
85
86
217522
  d_currentAssertionStack.push_back(std::pair<Node, bool>(assertion, isInput));
87
88
435044
  Debug("proof:cnf") << "CnfProof::pushCurrentAssertion "
89
435044
                     << "new stack size = " << d_currentAssertionStack.size()
90
217522
                     << std::endl;
91
217522
}
92
93
217522
void CnfProof::popCurrentAssertion() {
94
217522
  Assert(d_currentAssertionStack.size());
95
96
435044
  Debug("proof:cnf") << "CnfProof::popCurrentAssertion "
97
217522
                     << d_currentAssertionStack.back().first << std::endl;
98
99
217522
  d_currentAssertionStack.pop_back();
100
101
435044
  Debug("proof:cnf") << "CnfProof::popCurrentAssertion "
102
435044
                     << "new stack size = " << d_currentAssertionStack.size()
103
217522
                     << std::endl;
104
217522
}
105
106
490982
Node CnfProof::getCurrentAssertion() {
107
490982
  Assert(d_currentAssertionStack.size());
108
490982
  return d_currentAssertionStack.back().first;
109
}
110
111
250012
bool CnfProof::getCurrentAssertionKind()
112
{
113
250012
  return d_currentAssertionStack.back().second;
114
}
115
116
26685
} /* CVC4 namespace */