Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/theory_inference.h	Lines:	8	11	72.7 %
Date:	2021-05-22	Branches:	1	2	50.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Gereon Kremer
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * The theory inference utility.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__THEORY_INFERENCE_H
#define CVC5__THEORY__THEORY_INFERENCE_H

#include "expr/node.h"
#include "theory/inference_id.h"
#include "theory/output_channel.h"

namespace cvc5 {
namespace theory {

class TheoryInferenceManager;

/**
 * A theory inference base class. This class is an abstract data structure for
 * storing pending lemmas or facts in the buffered inference manager. It can
 * be seen a single use object capturing instructions for making a single
 * call to TheoryInferenceManager for lemmas or facts.
 */
class TheoryInference
{
 public:
  TheoryInference(InferenceId id) : d_id(id) {}
  virtual ~TheoryInference() {}

  /**
   * Process lemma, return the trust node to pass to
   * TheoryInferenceManager::trustedLemma. In addition, the inference should
   * process any internal side effects of the lemma.
   *
   * @param p The property of the lemma which will be passed to trustedLemma
   * for this inference. If this call does not update p, the default value will
   * be used.
   * @return The trust node (of kind TrustNodeKind::LEMMA) corresponding to the
   * lemma and its proof generator.
   */
  virtual TrustNode processLemma(LemmaProperty& p) { return TrustNode::null(); }
  /**
   * Process internal fact, return the conclusion to pass to
   * TheoryInferenceManager::assertInternalFact. In addition, the inference
   * should process any internal side effects of the fact.
   *
   * @param exp The explanation for the returned conclusion. Each node added to
   * exp should be a (conjunction of) literals that hold in the current equality
   * engine.
   * @return The (possibly negated) conclusion.
   */
  virtual Node processFact(std::vector<Node>& exp, ProofGenerator*& pg)
  {
    return Node::null();
  }

  /** Get the InferenceId of this theory inference. */
  InferenceId getId() const { return d_id; }
  /** Set the InferenceId of this theory inference. */
  void setId(InferenceId id) { d_id = id; }

 private:
  InferenceId d_id;
};

/**
 * A simple theory lemma with no side effects. Makes a single call to
 * trustedLemma in its process method.
 */
class SimpleTheoryLemma : public TheoryInference
{
 public:
  SimpleTheoryLemma(InferenceId id, Node n, LemmaProperty p, ProofGenerator* pg);
  virtual ~SimpleTheoryLemma() {}
  /** Process lemma */
  TrustNode processLemma(LemmaProperty& p) override;
  /** The lemma to send */
  Node d_node;
  /** The lemma property (see OutputChannel::lemma) */
  LemmaProperty d_property;
  /**
   * The proof generator for this lemma, which if non-null, is wrapped in a
   * TrustNode to be set on the output channel via trustedLemma at the time
   * the lemma is sent. This proof generator must be able to provide a proof
   * for d_node in the remainder of the user context.
   */
  ProofGenerator* d_pg;
};

/**
 * A simple internal fact with no side effects. Makes a single call to
 * assertInternalFact in its process method.
 */
class SimpleTheoryInternalFact : public TheoryInference
{
 public:
  SimpleTheoryInternalFact(InferenceId id, Node conc, Node exp, ProofGenerator* pg);
  virtual ~SimpleTheoryInternalFact() {}
  /** Process internal fact */
  Node processFact(std::vector<Node>& exp, ProofGenerator*& pg) override;
  /** The lemma to send */
  Node d_conc;
  /** The explanation */
  Node d_exp;
  /** The proof generator */
  ProofGenerator* d_pg;
};

}  // namespace theory
}  // namespace cvc5

#endif


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Gereon Kremer
4		*
5		* This file is part of the cvc5 project.
6		*
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.
11		* ****************************************************************************
12		*
13		* The theory inference utility.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__THEORY_INFERENCE_H
19		#define CVC5__THEORY__THEORY_INFERENCE_H
20
21		#include "expr/node.h"
22		#include "theory/inference_id.h"
23		#include "theory/output_channel.h"
24
25		namespace cvc5 {
26		namespace theory {
27
28		class TheoryInferenceManager;
29
30		/**
31		* A theory inference base class. This class is an abstract data structure for
32		* storing pending lemmas or facts in the buffered inference manager. It can
33		* be seen a single use object capturing instructions for making a single
34		* call to TheoryInferenceManager for lemmas or facts.
35		*/
36	56980	class TheoryInference
37		{
38		public:
39	464779	TheoryInference(InferenceId id) : d_id(id) {}
40	521229	virtual ~TheoryInference() {}
41
42		/**
43		* Process lemma, return the trust node to pass to
44		* TheoryInferenceManager::trustedLemma. In addition, the inference should
45		* process any internal side effects of the lemma.
46		*
47		* @param p The property of the lemma which will be passed to trustedLemma
48		* for this inference. If this call does not update p, the default value will
49		* be used.
50		* @return The trust node (of kind TrustNodeKind::LEMMA) corresponding to the
51		* lemma and its proof generator.
52		*/
53		virtual TrustNode processLemma(LemmaProperty& p) { return TrustNode::null(); }
54		/**
55		* Process internal fact, return the conclusion to pass to
56		* TheoryInferenceManager::assertInternalFact. In addition, the inference
57		* should process any internal side effects of the fact.
58		*
59		* @param exp The explanation for the returned conclusion. Each node added to
60		* exp should be a (conjunction of) literals that hold in the current equality
61		* engine.
62		* @return The (possibly negated) conclusion.
63		*/
64		virtual Node processFact(std::vector<Node>& exp, ProofGenerator*& pg)
65		{
66		return Node::null();
67		}
68
69		/** Get the InferenceId of this theory inference. */
70	855825	InferenceId getId() const { return d_id; }
71		/** Set the InferenceId of this theory inference. */
72	12547	void setId(InferenceId id) { d_id = id; }
73
74		private:
75		InferenceId d_id;
76		};
77
78		/**
79		* A simple theory lemma with no side effects. Makes a single call to
80		* trustedLemma in its process method.
81		*/
82	5526	class SimpleTheoryLemma : public TheoryInference
83		{
84		public:
85		SimpleTheoryLemma(InferenceId id, Node n, LemmaProperty p, ProofGenerator* pg);
86	176291	virtual ~SimpleTheoryLemma() {}
87		/** Process lemma */
88		TrustNode processLemma(LemmaProperty& p) override;
89		/** The lemma to send */
90		Node d_node;
91		/** The lemma property (see OutputChannel::lemma) */
92		LemmaProperty d_property;
93		/**
94		* The proof generator for this lemma, which if non-null, is wrapped in a
95		* TrustNode to be set on the output channel via trustedLemma at the time
96		* the lemma is sent. This proof generator must be able to provide a proof
97		* for d_node in the remainder of the user context.
98		*/
99		ProofGenerator* d_pg;
100		};
101
102		/**
103		* A simple internal fact with no side effects. Makes a single call to
104		* assertInternalFact in its process method.
105		*/
106		class SimpleTheoryInternalFact : public TheoryInference
107		{
108		public:
109		SimpleTheoryInternalFact(InferenceId id, Node conc, Node exp, ProofGenerator* pg);
110	329007	virtual ~SimpleTheoryInternalFact() {}
111		/** Process internal fact */
112		Node processFact(std::vector<Node>& exp, ProofGenerator*& pg) override;
113		/** The lemma to send */
114		Node d_conc;
115		/** The explanation */
116		Node d_exp;
117		/** The proof generator */
118		ProofGenerator* d_pg;
119		};
120
121		} // namespace theory
122		} // namespace cvc5
123
124		#endif