1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
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 |
|
* Difficulty manager. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/difficulty_manager.h" |
17 |
|
|
18 |
|
#include "options/smt_options.h" |
19 |
|
#include "smt/env.h" |
20 |
|
#include "theory/theory_model.h" |
21 |
|
#include "util/rational.h" |
22 |
|
|
23 |
|
namespace cvc5 { |
24 |
|
namespace theory { |
25 |
|
|
26 |
|
DifficultyManager::DifficultyManager(context::Context* c, Valuation val) |
27 |
|
: d_val(val), d_dfmap(c) |
28 |
|
{ |
29 |
|
} |
30 |
|
|
31 |
|
void DifficultyManager::getDifficultyMap(std::map<Node, Node>& dmap) |
32 |
|
{ |
33 |
|
NodeManager* nm = NodeManager::currentNM(); |
34 |
|
for (const std::pair<const Node, uint64_t> p : d_dfmap) |
35 |
|
{ |
36 |
|
dmap[p.first] = nm->mkConst(Rational(p.second)); |
37 |
|
} |
38 |
|
} |
39 |
|
|
40 |
|
void DifficultyManager::notifyLemma(const std::map<TNode, TNode>& rse, Node n) |
41 |
|
{ |
42 |
|
if (options::difficultyMode() != options::DifficultyMode::LEMMA_LITERAL) |
43 |
|
{ |
44 |
|
return; |
45 |
|
} |
46 |
|
Trace("diff-man") << "notifyLemma: " << n << std::endl; |
47 |
|
Kind nk = n.getKind(); |
48 |
|
// for lemma (or a_1 ... a_n), if a_i is a literal that is not true in the |
49 |
|
// valuation, then we increment the difficulty of that assertion |
50 |
|
std::vector<TNode> litsToCheck; |
51 |
|
if (nk == kind::OR) |
52 |
|
{ |
53 |
|
litsToCheck.insert(litsToCheck.end(), n.begin(), n.end()); |
54 |
|
} |
55 |
|
else if (nk == kind::IMPLIES) |
56 |
|
{ |
57 |
|
litsToCheck.push_back(n[0].negate()); |
58 |
|
litsToCheck.push_back(n[1]); |
59 |
|
} |
60 |
|
else |
61 |
|
{ |
62 |
|
litsToCheck.push_back(n); |
63 |
|
} |
64 |
|
std::map<TNode, TNode>::const_iterator it; |
65 |
|
for (TNode nc : litsToCheck) |
66 |
|
{ |
67 |
|
bool pol = nc.getKind() != kind::NOT; |
68 |
|
TNode atom = pol ? nc : nc[0]; |
69 |
|
it = rse.find(atom); |
70 |
|
if (it != rse.end()) |
71 |
|
{ |
72 |
|
incrementDifficulty(it->second); |
73 |
|
} |
74 |
|
} |
75 |
|
} |
76 |
|
|
77 |
|
void DifficultyManager::notifyCandidateModel(const NodeList& input, |
78 |
|
TheoryModel* m) |
79 |
|
{ |
80 |
|
if (options::difficultyMode() != options::DifficultyMode::MODEL_CHECK) |
81 |
|
{ |
82 |
|
return; |
83 |
|
} |
84 |
|
Trace("diff-man") << "DifficultyManager::notifyCandidateModel, #input=" |
85 |
|
<< input.size() << std::endl; |
86 |
|
for (const Node& a : input) |
87 |
|
{ |
88 |
|
// should have miniscoped the assertions upstream |
89 |
|
Assert(a.getKind() != kind::AND); |
90 |
|
// check if each input is satisfied |
91 |
|
Node av = m->getValue(a); |
92 |
|
if (av.isConst() && av.getConst<bool>()) |
93 |
|
{ |
94 |
|
continue; |
95 |
|
} |
96 |
|
Trace("diff-man") << " not true: " << a << std::endl; |
97 |
|
// not satisfied, increment counter |
98 |
|
incrementDifficulty(a); |
99 |
|
} |
100 |
|
Trace("diff-man") << std::endl; |
101 |
|
} |
102 |
|
void DifficultyManager::incrementDifficulty(TNode a, uint64_t amount) |
103 |
|
{ |
104 |
|
Assert(a.getType().isBoolean()); |
105 |
|
d_dfmap[a] = d_dfmap[a] + amount; |
106 |
|
} |
107 |
|
|
108 |
|
} // namespace theory |
109 |
29502 |
} // namespace cvc5 |