Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Dejan Jovanovic, Morgan Deters
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : : * The theory engine output channel.
14 : : */
15 : :
16 : : #include "theory/output_channel.h"
17 : :
18 : : #include "expr/skolem_manager.h"
19 : : #include "prop/prop_engine.h"
20 : : #include "theory/theory_engine.h"
21 : :
22 : : using namespace cvc5::internal::kind;
23 : :
24 : : namespace cvc5::internal {
25 : : namespace theory {
26 : :
27 : 690273 : OutputChannel::Statistics::Statistics(StatisticsRegistry& sr,
28 : 690273 : const std::string& statPrefix)
29 : 690273 : : conflicts(sr.registerInt(statPrefix + "conflicts")),
30 : 690273 : propagations(sr.registerInt(statPrefix + "propagations")),
31 : 690273 : lemmas(sr.registerInt(statPrefix + "lemmas")),
32 : 690273 : preferPhase(sr.registerInt(statPrefix + "preferPhase")),
33 : 690273 : trustedConflicts(sr.registerInt(statPrefix + "trustedConflicts")),
34 : 690273 : trustedLemmas(sr.registerInt(statPrefix + "trustedLemmas"))
35 : : {
36 : 690273 : }
37 : :
38 : 689826 : OutputChannel::OutputChannel(StatisticsRegistry& sr,
39 : : TheoryEngine* engine,
40 : 689826 : theory::TheoryId theory)
41 : : : d_engine(engine),
42 : : d_name(toString(theory)),
43 : 689826 : d_statistics(sr, getStatsPrefix(theory)),
44 : 689826 : d_theory(theory)
45 : : {
46 : 689826 : }
47 : :
48 : 447 : OutputChannel::OutputChannel(StatisticsRegistry& sr,
49 : : TheoryEngine* engine,
50 : : const std::string& name,
51 : 447 : size_t id)
52 : : : d_engine(engine),
53 : : d_name(name),
54 : 447 : d_statistics(sr, name + "::"),
55 : 447 : d_theory(static_cast<TheoryId>(THEORY_NONE + id))
56 : : {
57 : 447 : }
58 : :
59 : 153010 : void OutputChannel::safePoint(Resource r)
60 : : {
61 : 153010 : spendResource(r);
62 [ - + ]: 153010 : if (d_engine->d_interrupted)
63 : : {
64 : 0 : throw theory::Interrupted();
65 : : }
66 : 153010 : }
67 : :
68 : 13 : void OutputChannel::lemma(TNode lemma, InferenceId id, LemmaProperty p)
69 : : {
70 : 13 : trustedLemma(TrustNode::mkTrustLemma(lemma), id, p);
71 : 13 : }
72 : :
73 : 25674600 : bool OutputChannel::propagate(TNode literal)
74 : : {
75 [ + - ]: 51349200 : Trace("theory::propagate") << "OutputChannel<" << d_theory << ">::propagate("
76 : 25674600 : << literal << ")" << std::endl;
77 : 25674600 : ++d_statistics.propagations;
78 : 25674600 : d_engine->d_outputChannelUsed = true;
79 : 25674600 : return d_engine->propagate(literal, d_theory);
80 : : }
81 : :
82 : 0 : void OutputChannel::conflict(TNode conflictNode, InferenceId id)
83 : : {
84 [ - - ]: 0 : Trace("theory::conflict") << "OutputChannel<" << d_theory << ">::conflict("
85 : 0 : << conflictNode << ")" << std::endl;
86 : 0 : ++d_statistics.conflicts;
87 : 0 : d_engine->d_outputChannelUsed = true;
88 : 0 : TrustNode tConf = TrustNode::mkTrustConflict(conflictNode);
89 : 0 : d_engine->conflict(tConf, id, d_theory);
90 : 0 : }
91 : :
92 : 73915 : void OutputChannel::preferPhase(TNode n, bool phase)
93 : : {
94 [ + - ]: 147830 : Trace("theory") << "OutputChannel::preferPhase(" << n << ", " << phase << ")"
95 : 73915 : << std::endl;
96 : 73915 : ++d_statistics.preferPhase;
97 : 73915 : d_engine->getPropEngine()->preferPhase(n, phase);
98 : 73915 : }
99 : :
100 : 9219 : void OutputChannel::setModelUnsound(IncompleteId id)
101 : : {
102 [ + - ]: 9219 : Trace("theory") << "setModelUnsound(" << id << ")" << std::endl;
103 : 9219 : d_engine->setModelUnsound(d_theory, id);
104 : 9219 : }
105 : :
106 : 118 : void OutputChannel::setRefutationUnsound(IncompleteId id)
107 : : {
108 [ + - ]: 118 : Trace("theory") << "setRefutationUnsound(" << id << ")" << std::endl;
109 : 118 : d_engine->setRefutationUnsound(d_theory, id);
110 : 118 : }
111 : :
112 : 16783500 : void OutputChannel::spendResource(Resource r) { d_engine->spendResource(r); }
113 : :
114 : 214493 : void OutputChannel::trustedConflict(TrustNode pconf, InferenceId id)
115 : : {
116 [ - + ][ - + ]: 214493 : Assert(pconf.getKind() == TrustNodeKind::CONFLICT);
[ - - ]
117 [ + - ]: 428986 : Trace("theory::conflict")
118 : 0 : << "OutputChannel<" << d_theory << ">::trustedConflict("
119 [ - + ][ - - ]: 214493 : << pconf.getNode() << ")" << std::endl;
120 [ + + ]: 214493 : if (pconf.getGenerator() != nullptr)
121 : : {
122 : 104985 : ++d_statistics.trustedConflicts;
123 : : }
124 : 214493 : ++d_statistics.conflicts;
125 : 214493 : d_engine->d_outputChannelUsed = true;
126 : 214493 : d_engine->conflict(pconf, id, d_theory);
127 : 214493 : }
128 : :
129 : 657746 : void OutputChannel::trustedLemma(TrustNode plem,
130 : : InferenceId id,
131 : : LemmaProperty p)
132 : : {
133 [ + - ]: 1315490 : Trace("theory::lemma") << "OutputChannel<" << d_theory << ">::trustedLemma("
134 : 657746 : << plem << ")" << std::endl;
135 [ - + ][ - + ]: 657746 : Assert(plem.getKind() == TrustNodeKind::LEMMA);
[ - - ]
136 [ + + ]: 657746 : if (plem.getGenerator() != nullptr)
137 : : {
138 : 257979 : ++d_statistics.trustedLemmas;
139 : : }
140 : 657746 : ++d_statistics.lemmas;
141 : 657746 : d_engine->d_outputChannelUsed = true;
142 [ + + ]: 657746 : if (isLemmaPropertySendAtoms(p))
143 : : {
144 : 967 : d_engine->ensureLemmaAtoms(plem.getNode(), d_theory);
145 : : }
146 : : // now, call the normal interface for lemma
147 : 657746 : d_engine->lemma(plem, id, p, d_theory);
148 : 657745 : }
149 : :
150 : 842 : TheoryId OutputChannel::getId() const { return d_theory; }
151 : :
152 : : } // namespace theory
153 : : } // namespace cvc5::internal
|
