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
|
/******************************************************************************
* 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.
* ****************************************************************************
*
* Implementation of module for processing the difficulty of input assumptions
* based on proof nodes.
*/
#include "cvc5_private.h"
#ifndef CVC5__SMT__DIFFICULTY_POST_PROCESSOR_H
#define CVC5__SMT__DIFFICULTY_POST_PROCESSOR_H
#include <map>
#include "proof/proof_node_updater.h"
namespace cvc5 {
namespace smt {
/**
* A postprocess callback that computes difficulty based on the structure
* of the proof. In particular, this class assesses what the source of an
* assertion was by considering the shape of the proof. For instance, if
* assertion A entails x=t, and this was used to derive a substitution
* { x -> t } to assertion B, then B is the source of B*{ x -> t }. The
* difficulty of this assertion is carried to B and not A. The reason is that
* A can be understood as a definition, and is eliminated, whereas B was
* persistent if B*{ x -> t } was a prepreprocessed assertion.
*
* Note that this postprocess callback is intended to be run on the proof
* of a single preprocessed assertion C. If C was derived by proof with
* free assumptions A_1, ..., A_n, then for each A_i that is a "source" as
* described above, we increment the difficulty of A_i by the difficulty value
* assigned to C.
*
* This means that the user of this method should:
* (1) assign the current difficulty we are incrementing (setCurrentDifficulty),
* (2) process the proof using a proof node updater with this callback.
* The final difficulty map is accumulated in d_accMap, which can be accessed
* at any time via getDifficultyMap.
*/
class DifficultyPostprocessCallback : public ProofNodeUpdaterCallback
{
public:
DifficultyPostprocessCallback();
~DifficultyPostprocessCallback() {}
/**
* Set current difficulty of the next proof to process to the (integer)
* value stored in Node d. This value will be assigned to all the free
* assumptions of the proof we traverse next. This value is stored in
* d_currDifficulty.
*
* @return true if the difficulty value was successfully extracted
*/
bool setCurrentDifficulty(Node d);
/**
* Should proof pn be updated? This is used to selectively traverse to e.g.
* the source of an assertion.
*/
bool shouldUpdate(std::shared_ptr<ProofNode> pn,
const std::vector<Node>& fa,
bool& continueUpdate) override;
/** Get the (acculumated) difficulty map for the last processed proof node */
void getDifficultyMap(std::map<Node, Node>& dmap) const;
private:
/**
* The current difficulty of the assertion whose proof of preprocessing
* we are considering.
*/
uint64_t d_currDifficulty;
/** The current accumulated difficulty map */
std::map<Node, uint64_t> d_accMap;
};
} // namespace smt
} // namespace cvc5
#endif
|
