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