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

Line Exec Source
1
/*********************                                                        */
2
/*! \file inference.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer
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 Datatypes inference
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__DATATYPES__INFERENCE_H
18
#define CVC4__THEORY__DATATYPES__INFERENCE_H
19
20
#include "expr/node.h"
21
#include "theory/inference_id.h"
22
#include "theory/theory_inference.h"
23
#include "theory/trust_node.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace datatypes {
28
29
class InferenceManager;
30
31
/**
32
 * A custom inference class. The main feature of this class is that it
33
 * dynamically decides whether to process itself as a fact or as a lemma,
34
 * based on the mustCommunicateFact method below.
35
 */
36
856836
class DatatypesInference : public SimpleTheoryInternalFact
37
{
38
 public:
39
  DatatypesInference(InferenceManager* im,
40
                     Node conc,
41
                     Node exp,
42
                     InferenceId i = InferenceId::UNKNOWN);
43
  /**
44
   * Must communicate fact method.
45
   * The datatypes decision procedure makes "internal" inferences :
46
   *  (1) Unification : C( t1...tn ) = C( s1...sn ) => ti = si
47
   *  (2) Label : ~is_C1(t) ... ~is_C{i-1}(t) ~is_C{i+1}(t) ... ~is_Cn(t) =>
48
   * is_Ci( t )
49
   *  (3) Instantiate : is_C( t ) => t = C( sel_1( t ) ... sel_n( t ) )
50
   *  (4) collapse selector : S( C( t1...tn ) ) = t'
51
   *  (5) collapse term size : size( C( t1...tn ) ) = 1 + size( t1 ) + ... +
52
   * size( tn )
53
   *  (6) non-negative size : 0 <= size(t)
54
   * This method returns true if the fact must be sent out as a lemma. If it
55
   * returns false, then we assert the fact internally. We return true for (6)
56
   * and OR conclusions. We also return true if the option dtInferAsLemmas is
57
   * set to true.
58
   */
59
  static bool mustCommunicateFact(Node n, Node exp);
60
  /** Process lemma */
61
  TrustNode processLemma(LemmaProperty& p) override;
62
  /** Process internal fact */
63
  Node processFact(std::vector<Node>& exp, ProofGenerator*& pg) override;
64
65
 private:
66
  /** Pointer to the inference manager */
67
  InferenceManager* d_im;
68
};
69
70
}  // namespace datatypes
71
}  // namespace theory
72
}  // namespace CVC4
73
74
#endif