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
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds
*
* This file is part of the cvc5 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.
* ****************************************************************************
*
* Difficulty manager.
*/
#include "theory/difficulty_manager.h"
#include "options/smt_options.h"
#include "smt/env.h"
#include "theory/theory_model.h"
#include "util/rational.h"
using namespace cvc5::kind;
namespace cvc5 {
namespace theory {
DifficultyManager::DifficultyManager(context::Context* c, Valuation val)
: d_val(val), d_dfmap(c)
{
}
void DifficultyManager::getDifficultyMap(std::map<Node, Node>& dmap)
{
NodeManager* nm = NodeManager::currentNM();
for (const std::pair<const Node, uint64_t> p : d_dfmap)
{
dmap[p.first] = nm->mkConst(CONST_RATIONAL, Rational(p.second));
}
}
void DifficultyManager::notifyLemma(const std::map<TNode, TNode>& rse, Node n)
{
if (options::difficultyMode() != options::DifficultyMode::LEMMA_LITERAL)
{
return;
}
Trace("diff-man") << "notifyLemma: " << n << std::endl;
Kind nk = n.getKind();
// for lemma (or a_1 ... a_n), if a_i is a literal that is not true in the
// valuation, then we increment the difficulty of that assertion
std::vector<TNode> litsToCheck;
if (nk == kind::OR)
{
litsToCheck.insert(litsToCheck.end(), n.begin(), n.end());
}
else if (nk == kind::IMPLIES)
{
litsToCheck.push_back(n[0].negate());
litsToCheck.push_back(n[1]);
}
else
{
litsToCheck.push_back(n);
}
std::map<TNode, TNode>::const_iterator it;
for (TNode nc : litsToCheck)
{
bool pol = nc.getKind() != kind::NOT;
TNode atom = pol ? nc : nc[0];
it = rse.find(atom);
Trace("diff-man-debug")
<< "Check literal: " << atom << ", has reason = " << (it != rse.end())
<< std::endl;
if (it != rse.end())
{
incrementDifficulty(it->second);
}
}
}
void DifficultyManager::notifyCandidateModel(const NodeList& input,
TheoryModel* m)
{
if (options::difficultyMode() != options::DifficultyMode::MODEL_CHECK)
{
return;
}
Trace("diff-man") << "DifficultyManager::notifyCandidateModel, #input="
<< input.size() << std::endl;
for (const Node& a : input)
{
// should have miniscoped the assertions upstream
Assert(a.getKind() != kind::AND);
// check if each input is satisfied
Node av = m->getValue(a);
if (av.isConst() && av.getConst<bool>())
{
continue;
}
Trace("diff-man") << " not true: " << a << std::endl;
// not satisfied, increment counter
incrementDifficulty(a);
}
Trace("diff-man") << std::endl;
}
void DifficultyManager::incrementDifficulty(TNode a, uint64_t amount)
{
Assert(a.getType().isBoolean());
d_dfmap[a] = d_dfmap[a] + amount;
}
} // namespace theory
} // namespace cvc5
|
