1 /********************* */
2 /*! \file theory_inference.h
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief The theory inference utility
15 #include "cvc4_private.h"
17 #ifndef CVC4__THEORY__THEORY_INFERENCE_H
18 #define CVC4__THEORY__THEORY_INFERENCE_H
20 #include "expr/node.h"
21 #include "theory/inference_id.h"
22 #include "theory/output_channel.h"
27 class TheoryInferenceManager
;
30 * A theory inference base class. This class is an abstract data structure for
31 * storing pending lemmas or facts in the buffered inference manager. It can
32 * be seen a single use object capturing instructions for making a single
33 * call to TheoryInferenceManager for lemmas or facts.
38 TheoryInference(InferenceId id
) : d_id(id
) {}
39 virtual ~TheoryInference() {}
41 * Called by the provided inference manager to process this inference. This
42 * method should make call(s) to inference manager to process this
43 * inference, as well as processing any specific side effects. This method
44 * typically makes a single call to the provided inference manager e.g.
45 * d_im->trustedLemma or d_im->assertInternalFact. Notice it is the sole
46 * responsibility of this class to make this call; the inference manager
47 * does not call itself otherwise when processing pending inferences.
49 * @param im The inference manager to use
50 * @param asLemma Whether this inference is being processed as a lemma
51 * during doPendingLemmas (otherwise it is being processed in doPendingFacts).
52 * Typically, this method calls lemma or conflict when asLemma is
53 * true, and assertInternalFact when this flag is false, although this
54 * behavior is (intentionally) not strictly enforced. In particular, the
55 * choice to send a conflict, lemma or fact may depend on local state of the
56 * theory, which may change while the inference is pending. Hence the
57 * implementation of this method may choose to implement any call to the
58 * inference manager. This flag simply serves to track whether the inference
59 * initially was added a pending lemma or not.
60 * @return true if the inference was successfully processed by the inference
61 * manager. This method for instance returns false if it corresponds to a
62 * lemma that was already cached by im and hence was discarded.
64 virtual bool process(TheoryInferenceManager
* im
, bool asLemma
) = 0;
66 /** Get the InferenceId of this theory inference. */
67 InferenceId
getId() const { return d_id
; }
68 /** Set the InferenceId of this theory inference. */
69 void setId(InferenceId id
) { d_id
= id
; }
76 * A simple theory lemma with no side effects. Makes a single call to
77 * trustedLemma in its process method.
79 class SimpleTheoryLemma
: public TheoryInference
82 SimpleTheoryLemma(InferenceId id
, Node n
, LemmaProperty p
, ProofGenerator
* pg
);
83 virtual ~SimpleTheoryLemma() {}
85 * Send the lemma using inference manager im, return true if the lemma was
86 * sent. It should be the case that asLemma = true or an assertion failure
89 virtual bool process(TheoryInferenceManager
* im
, bool asLemma
) override
;
90 /** The lemma to send */
92 /** The lemma property (see OutputChannel::lemma) */
93 LemmaProperty d_property
;
95 * The proof generator for this lemma, which if non-null, is wrapped in a
96 * TrustNode to be set on the output channel via trustedLemma at the time
97 * the lemma is sent. This proof generator must be able to provide a proof
98 * for d_node in the remainder of the user context.
100 ProofGenerator
* d_pg
;
104 * A simple internal fact with no side effects. Makes a single call to
105 * assertInternalFact in its process method.
107 class SimpleTheoryInternalFact
: public TheoryInference
110 SimpleTheoryInternalFact(InferenceId id
, Node conc
, Node exp
, ProofGenerator
* pg
);
111 virtual ~SimpleTheoryInternalFact() {}
113 * Send the lemma using inference manager im, return true if the lemma was
114 * sent. It should be the case that asLemma = false or an assertion failure
117 virtual bool process(TheoryInferenceManager
* im
, bool asLemma
) override
;
118 /** The lemma to send */
120 /** The explanation */
122 /** The proof generator */
123 ProofGenerator
* d_pg
;
126 } // namespace theory