1 /******************************************************************************
2 * Top contributors (to current version):
5 * This file is part of the cvc5 project.
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 * ****************************************************************************
16 #include "theory/difficulty_manager.h"
18 #include "options/smt_options.h"
20 #include "theory/theory_model.h"
21 #include "util/rational.h"
26 DifficultyManager::DifficultyManager(context::Context
* c
, Valuation val
)
27 : d_val(val
), d_dfmap(c
)
31 void DifficultyManager::getDifficultyMap(std::map
<Node
, Node
>& dmap
)
33 NodeManager
* nm
= NodeManager::currentNM();
34 for (const std::pair
<const Node
, uint64_t> p
: d_dfmap
)
36 dmap
[p
.first
] = nm
->mkConst(Rational(p
.second
));
40 void DifficultyManager::notifyLemma(const std::map
<TNode
, TNode
>& rse
, Node n
)
42 if (options::difficultyMode() != options::DifficultyMode::LEMMA_LITERAL
)
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
;
53 litsToCheck
.insert(litsToCheck
.end(), n
.begin(), n
.end());
55 else if (nk
== kind::IMPLIES
)
57 litsToCheck
.push_back(n
[0].negate());
58 litsToCheck
.push_back(n
[1]);
62 litsToCheck
.push_back(n
);
64 std::map
<TNode
, TNode
>::const_iterator it
;
65 for (TNode nc
: litsToCheck
)
67 bool pol
= nc
.getKind() != kind::NOT
;
68 TNode atom
= pol
? nc
: nc
[0];
72 incrementDifficulty(it
->second
);
77 void DifficultyManager::notifyCandidateModel(const NodeList
& input
,
80 if (options::difficultyMode() != options::DifficultyMode::MODEL_CHECK
)
84 Trace("diff-man") << "DifficultyManager::notifyCandidateModel, #input="
85 << input
.size() << std::endl
;
86 for (const Node
& a
: input
)
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>())
96 Trace("diff-man") << " not true: " << a
<< std::endl
;
97 // not satisfied, increment counter
98 incrementDifficulty(a
);
100 Trace("diff-man") << std::endl
;
102 void DifficultyManager::incrementDifficulty(TNode a
, uint64_t amount
)
104 Assert(a
.getType().isBoolean());
105 d_dfmap
[a
] = d_dfmap
[a
] + amount
;
108 } // namespace theory