GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/datatypes/inference.cpp Lines: 18 24 75.0 %
Date: 2021-03-23 Branches: 39 110 35.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inference.cpp
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 "theory/datatypes/inference.h"
16
17
#include "expr/dtype.h"
18
#include "options/datatypes_options.h"
19
#include "theory/datatypes/inference_manager.h"
20
#include "theory/theory.h"
21
22
using namespace CVC4::kind;
23
24
namespace CVC4 {
25
namespace theory {
26
namespace datatypes {
27
28
435879
DatatypesInference::DatatypesInference(InferenceManager* im,
29
                                       Node conc,
30
                                       Node exp,
31
435879
                                       InferenceId i)
32
435879
    : SimpleTheoryInternalFact(i, conc, exp, nullptr), d_im(im)
33
{
34
  // false is not a valid explanation
35
435879
  Assert(d_exp.isNull() || !d_exp.isConst() || d_exp.getConst<bool>());
36
435879
}
37
38
411653
bool DatatypesInference::mustCommunicateFact(Node n, Node exp)
39
{
40
411653
  Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl;
41
  // Force lemmas if option is set
42
823306
  if (options::dtInferAsLemmas())
43
  {
44
    Trace("dt-lemma-debug")
45
        << "Communicate " << n << " due to option" << std::endl;
46
    return true;
47
  }
48
  // Note that equalities due to instantiate are forced as lemmas if
49
  // necessary as they are created. This ensures that terms are shared with
50
  // external theories when necessary. We send the lemma here only if the
51
  // conclusion has kind LEQ (for datatypes size) or OR. Notice that
52
  // all equalities are kept internal, apart from those forced as lemmas
53
  // via instantiate.
54
411653
  else if (n.getKind() == LEQ || n.getKind() == OR)
55
  {
56
    Trace("dt-lemma-debug")
57
        << "Communicate " << n << " due to kind" << std::endl;
58
    return true;
59
  }
60
411653
  Trace("dt-lemma-debug") << "Do not communicate " << n << std::endl;
61
411653
  return false;
62
}
63
64
9279
TrustNode DatatypesInference::processLemma(LemmaProperty& p)
65
{
66
  // we don't pass lemma property p currently, as it is always default
67
9279
  return d_im->processDtLemma(d_conc, d_exp, getId());
68
}
69
70
407283
Node DatatypesInference::processFact(std::vector<Node>& exp,
71
                                     ProofGenerator*& pg)
72
{
73
  // add to the explanation vector if applicable (when non-trivial)
74
407283
  if (!d_exp.isNull() && !d_exp.isConst())
75
  {
76
388275
    exp.push_back(d_exp);
77
  }
78
407283
  return d_im->processDtFact(d_conc, d_exp, getId(), pg);
79
}
80
81
}  // namespace datatypes
82
}  // namespace theory
83
438338
}  // namespace CVC4