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 |
|
#include "theory/theory.h" |
21 |
|
|
22 |
|
namespace cvc5 { |
23 |
|
namespace theory { |
24 |
|
namespace strings { |
25 |
|
|
26 |
63012 |
InferInfo::InferInfo(InferenceId id): TheoryInference(id), d_sim(nullptr), d_idRev(false) |
27 |
|
{ |
28 |
63012 |
} |
29 |
|
|
30 |
17463 |
TrustNode InferInfo::processLemma(LemmaProperty& p) |
31 |
|
{ |
32 |
17463 |
return d_sim->processLemma(*this, p); |
33 |
|
} |
34 |
|
|
35 |
23845 |
Node InferInfo::processFact(std::vector<Node>& exp, ProofGenerator*& pg) |
36 |
|
{ |
37 |
87227 |
for (const Node& ec : d_premises) |
38 |
|
{ |
39 |
63382 |
utils::flattenOp(kind::AND, ec, exp); |
40 |
|
} |
41 |
23845 |
d_sim->processFact(*this, pg); |
42 |
23845 |
return d_conc; |
43 |
|
} |
44 |
|
|
45 |
60089 |
bool InferInfo::isTrivial() const |
46 |
|
{ |
47 |
60089 |
Assert(!d_conc.isNull()); |
48 |
60089 |
return d_conc.isConst() && d_conc.getConst<bool>(); |
49 |
|
} |
50 |
|
|
51 |
60089 |
bool InferInfo::isConflict() const |
52 |
|
{ |
53 |
60089 |
Assert(!d_conc.isNull()); |
54 |
60089 |
return d_conc.isConst() && !d_conc.getConst<bool>() && d_noExplain.empty(); |
55 |
|
} |
56 |
|
|
57 |
26491 |
bool InferInfo::isFact() const |
58 |
|
{ |
59 |
26491 |
Assert(!d_conc.isNull()); |
60 |
52982 |
TNode atom = d_conc.getKind() == kind::NOT ? d_conc[0] : d_conc; |
61 |
|
// we could process inferences with conjunctive conclusions as facts, where |
62 |
|
// the explanation is copied. However, for simplicity, we always send these |
63 |
|
// as lemmas. This case happens very infrequently. |
64 |
79452 |
return !atom.isConst() && Theory::theoryOf(atom) == THEORY_STRINGS |
65 |
104028 |
&& d_noExplain.empty(); |
66 |
|
} |
67 |
|
|
68 |
47690 |
Node InferInfo::getPremises() const |
69 |
|
{ |
70 |
|
// d_noExplain is a subset of d_ant |
71 |
47690 |
return utils::mkAnd(d_premises); |
72 |
|
} |
73 |
|
|
74 |
|
std::ostream& operator<<(std::ostream& out, const InferInfo& ii) |
75 |
|
{ |
76 |
|
out << "(infer " << ii.getId() << " " << ii.d_conc; |
77 |
|
if (ii.d_idRev) |
78 |
|
{ |
79 |
|
out << " :rev"; |
80 |
|
} |
81 |
|
if (!ii.d_premises.empty()) |
82 |
|
{ |
83 |
|
out << " :ant (" << ii.d_premises << ")"; |
84 |
|
} |
85 |
|
if (!ii.d_noExplain.empty()) |
86 |
|
{ |
87 |
|
out << " :no-explain (" << ii.d_noExplain << ")"; |
88 |
|
} |
89 |
|
out << ")"; |
90 |
|
return out; |
91 |
|
} |
92 |
|
|
93 |
|
} // namespace strings |
94 |
|
} // namespace theory |
95 |
22746 |
} // namespace cvc5 |