GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/engine_output_channel.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 2 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file engine_output_channel.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, 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 The theory engine output channel.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__ENGINE_OUTPUT_CHANNEL_H
18
#define CVC4__THEORY__ENGINE_OUTPUT_CHANNEL_H
19
20
#include "expr/node.h"
21
#include "theory/output_channel.h"
22
#include "theory/theory_id.h"
23
#include "util/statistics_registry.h"
24
25
namespace CVC4 {
26
27
class TheoryEngine;
28
29
namespace theory {
30
31
class Theory;
32
33
/**
34
 * An output channel for Theory that passes messages back to a TheoryEngine
35
 * for a given Theory.
36
 *
37
 * Notice that it has interfaces trustedConflict and trustedLemma which are
38
 * used for ensuring that proof generators are associated with the lemmas
39
 * and conflicts sent on this output channel.
40
 */
41
233916
class EngineOutputChannel : public theory::OutputChannel
42
{
43
  friend class TheoryEngine;
44
45
 public:
46
  EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory);
47
48
  void safePoint(ResourceManager::Resource r) override;
49
50
  void conflict(TNode conflictNode) override;
51
  bool propagate(TNode literal) override;
52
53
  void lemma(TNode lemma, LemmaProperty p = LemmaProperty::NONE) override;
54
55
  void splitLemma(TNode lemma, bool removable = false) override;
56
57
  void demandRestart() override;
58
59
  void requirePhase(TNode n, bool phase) override;
60
61
  void setIncomplete() override;
62
63
  void spendResource(ResourceManager::Resource r) override;
64
65
  void handleUserAttribute(const char* attr, theory::Theory* t) override;
66
67
  /**
68
   * Let pconf be the pair (Node conf, ProofGenerator * pfg). This method
69
   * sends conf on the output channel of this class whose proof can be generated
70
   * by the generator pfg. Apart from pfg, the interface for this method is
71
   * the same as calling OutputChannel::lemma on conf.
72
   */
73
  void trustedConflict(TrustNode pconf) override;
74
  /**
75
   * Let plem be the pair (Node lem, ProofGenerator * pfg).
76
   * Send lem on the output channel of this class whose proof can be generated
77
   * by the generator pfg. Apart from pfg, the interface for this method is
78
   * the same as calling OutputChannel::lemma on lem.
79
   */
80
  void trustedLemma(TrustNode plem,
81
                    LemmaProperty p = LemmaProperty::NONE) override;
82
83
 protected:
84
  /**
85
   * Statistics for a particular theory.
86
   */
87
  class Statistics
88
  {
89
   public:
90
    Statistics(theory::TheoryId theory);
91
    ~Statistics();
92
    /** Number of calls to conflict, propagate, lemma, requirePhase,
93
     * restartDemands */
94
    IntStat conflicts, propagations, lemmas, requirePhase, restartDemands,
95
        trustedConflicts, trustedLemmas;
96
  };
97
  /** The theory engine we're communicating with. */
98
  TheoryEngine* d_engine;
99
  /** The statistics of the theory interractions. */
100
  Statistics d_statistics;
101
  /** The theory owning this channel. */
102
  theory::TheoryId d_theory;
103
  /** A helper function for registering lemma recipes with the proof engine */
104
  void registerLemmaRecipe(Node lemma,
105
                           Node originalLemma,
106
                           bool preprocess,
107
                           theory::TheoryId theoryId);
108
};
109
110
}  // namespace theory
111
}  // namespace CVC4
112
113
#endif /* CVC4__THEORY__ENGINE_OUTPUT_CHANNEL_H */