1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
|
/********************* */
/*! \file infer_info.cpp
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Mudathir Mohamed, Gereon Kremer
** This file is part of the CVC4 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.\endverbatim
**
** \brief Implementation of inference information utility.
**/
#include "theory/strings/infer_info.h"
#include "theory/strings/inference_manager.h"
#include "theory/strings/theory_strings_utils.h"
namespace CVC5 {
namespace theory {
namespace strings {
InferInfo::InferInfo(InferenceId id): TheoryInference(id), d_sim(nullptr), d_idRev(false)
{
}
TrustNode InferInfo::processLemma(LemmaProperty& p)
{
return d_sim->processLemma(*this, p);
}
Node InferInfo::processFact(std::vector<Node>& exp, ProofGenerator*& pg)
{
for (const Node& ec : d_premises)
{
utils::flattenOp(kind::AND, ec, exp);
}
d_sim->processFact(*this, pg);
return d_conc;
}
bool InferInfo::isTrivial() const
{
Assert(!d_conc.isNull());
return d_conc.isConst() && d_conc.getConst<bool>();
}
bool InferInfo::isConflict() const
{
Assert(!d_conc.isNull());
return d_conc.isConst() && !d_conc.getConst<bool>() && d_noExplain.empty();
}
bool InferInfo::isFact() const
{
Assert(!d_conc.isNull());
TNode atom = d_conc.getKind() == kind::NOT ? d_conc[0] : d_conc;
// we could process inferences with conjunctive conclusions as facts, where
// the explanation is copied. However, for simplicity, we always send these
// as lemmas. This case happens very infrequently.
return !atom.isConst() && atom.getKind() != kind::OR
&& atom.getKind() != kind::AND && d_noExplain.empty();
}
Node InferInfo::getPremises() const
{
// d_noExplain is a subset of d_ant
return utils::mkAnd(d_premises);
}
std::ostream& operator<<(std::ostream& out, const InferInfo& ii)
{
out << "(infer " << ii.getId() << " " << ii.d_conc;
if (ii.d_idRev)
{
out << " :rev";
}
if (!ii.d_premises.empty())
{
out << " :ant (" << ii.d_premises << ")";
}
if (!ii.d_noExplain.empty())
{
out << " :no-explain (" << ii.d_noExplain << ")";
}
out << ")";
return out;
}
} // namespace strings
} // namespace theory
} // namespace CVC5
|
