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 "cvc5_private.h"
18 #ifndef CVC5__THEORY__DIFFICULTY_MANAGER__H
19 #define CVC5__THEORY__DIFFICULTY_MANAGER__H
21 #include "context/cdhashmap.h"
22 #include "context/cdlist.h"
23 #include "expr/node.h"
24 #include "theory/valuation.h"
32 * Difficulty manager, which tracks an estimate of the difficulty of each
33 * preprocessed assertion during solving.
35 class DifficultyManager
37 typedef context::CDList
<Node
> NodeList
;
38 typedef context::CDHashMap
<Node
, uint64_t> NodeUIntMap
;
41 DifficultyManager(context::Context
* c
, Valuation val
);
43 * Get difficulty map, which populates dmap mapping preprocessed assertions
44 * to a difficulty measure (a constant integer).
46 void getDifficultyMap(std::map
<Node
, Node
>& dmap
);
48 * Notify lemma, for difficulty measurements. This increments the difficulty
49 * of assertions that share literals with that lemma if the difficulty mode
50 * is LEMMA_LITERAL. In particular, for each literal lit in the lemma lem, we
51 * increment the difficulty of the assertion res[lit], which corresponds to
52 * the assertion that was the reason why the literal is relevant in the
55 * @param rse Mapping from literals to the preprocessed assertion that was
56 * the reason why that literal was relevant in the current context
57 * @param lem The lemma
59 void notifyLemma(const std::map
<TNode
, TNode
>& rse
, Node lem
);
61 * Notify that `m` is a (candidate) model. This increments the difficulty
62 * of assertions that are not satisfied by that model.
64 * @param input The list of preprocessed assertions
65 * @param m The candidate model.
67 void notifyCandidateModel(const NodeList
& input
, TheoryModel
* m
);
70 /** Increment difficulty on assertion a */
71 void incrementDifficulty(TNode a
, uint64_t amount
= 1);
72 /** The valuation object, used to query current value of theory literals */
75 * User-context dependent mapping from input assertions to difficulty measure
83 #endif /* CVC5__THEORY__DIFFICULTY_MANAGER__H */