GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/booleans/theory_bool.cpp Lines: 21 22 95.5 %
Date: 2021-03-23 Branches: 39 74 52.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bool.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Dejan Jovanovic
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 The theory of booleans.
13
 **
14
 ** The theory of booleans.
15
 **/
16
17
#include "theory/booleans/theory_bool.h"
18
19
#include <stack>
20
#include <vector>
21
22
#include "expr/proof_node_manager.h"
23
#include "smt_util/boolean_simplification.h"
24
#include "theory/booleans/circuit_propagator.h"
25
#include "theory/booleans/theory_bool_rewriter.h"
26
#include "theory/substitutions.h"
27
#include "theory/theory.h"
28
#include "theory/trust_substitutions.h"
29
#include "theory/valuation.h"
30
#include "util/hash.h"
31
32
using namespace std;
33
34
namespace CVC4 {
35
namespace theory {
36
namespace booleans {
37
38
8997
TheoryBool::TheoryBool(context::Context* c,
39
                       context::UserContext* u,
40
                       OutputChannel& out,
41
                       Valuation valuation,
42
                       const LogicInfo& logicInfo,
43
8997
                       ProofNodeManager* pnm)
44
8997
    : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo, pnm)
45
{
46
8997
  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
47
8997
  if (pc != nullptr)
48
  {
49
    // add checkers
50
962
    d_bProofChecker.registerTo(pc);
51
  }
52
8997
}
53
54
34967
Theory::PPAssertStatus TheoryBool::ppAssert(
55
    TrustNode tin, TrustSubstitutionMap& outSubstitutions)
56
{
57
69934
  TNode in = tin.getNode();
58
34967
  if (in.getKind() == kind::CONST_BOOLEAN && !in.getConst<bool>()) {
59
    // If we get a false literal, we're in conflict
60
    return PP_ASSERT_STATUS_CONFLICT;
61
  }
62
63
  // Add the substitution from the variable to its value
64
34967
  if (in.getKind() == kind::NOT) {
65
21891
    if (in[0].isVar())
66
    {
67
65646
      outSubstitutions.addSubstitutionSolved(
68
43764
          in[0], NodeManager::currentNM()->mkConst<bool>(false), tin);
69
21882
      return PP_ASSERT_STATUS_SOLVED;
70
    }
71
  } else {
72
13076
    if (in.isVar())
73
    {
74
38952
      outSubstitutions.addSubstitutionSolved(
75
25968
          in, NodeManager::currentNM()->mkConst<bool>(true), tin);
76
12984
      return PP_ASSERT_STATUS_SOLVED;
77
    }
78
  }
79
80
101
  return Theory::ppAssert(tin, outSubstitutions);
81
}
82
83
}/* CVC4::theory::booleans namespace */
84
}/* CVC4::theory namespace */
85
26685
}/* CVC4 namespace */