blob: 9a5815a0c91e52ff75643e94766ef055ea70415e (
plain)
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
|
/******************************************************************************
* 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.
* ****************************************************************************
*
* Justification stack.
*/
#include "cvc5_private.h"
#ifndef CVC5__DECISION__JUSTIFY_STACK_H
#define CVC5__DECISION__JUSTIFY_STACK_H
#include "context/cdlist.h"
#include "context/cdo.h"
#include "decision/justify_info.h"
#include "expr/node.h"
namespace cvc5 {
namespace decision {
/**
* A justify stack, which tracks the progress in justifying a formula. It
* maintains a stack of justification infos in a SAT-context dependent
* manner.
*/
class JustifyStack
{
public:
JustifyStack(context::Context* c);
~JustifyStack();
/** reset the stack */
void reset(TNode curr);
/** clear */
void clear();
/** size */
size_t size() const;
/** Get the current assertion */
TNode getCurrentAssertion() const;
/** Has current assertion */
bool hasCurrentAssertion() const;
/** Get current justify info */
JustifyInfo* getCurrent();
/** Push to stack */
void pushToStack(TNode n, prop::SatValue desiredVal);
/** Pop from stack */
void popStack();
private:
/**
* Get or allocate justify info at position i. This does not impact
* d_stackSizeValid.
*/
JustifyInfo* getOrAllocJustifyInfo(size_t i);
/** The context */
context::Context* d_context;
/** The current assertion we are trying to satisfy */
context::CDO<TNode> d_current;
/**
* Stack of justify info, valid up to index d_stackSizeValid-1. Notice the
* size of this list may be larger than the current size we are using in
* cases where we considered an assertion requiring a larger stack size
* than the current one. This is because we do not erase elements from
* CDList in a context-dependent manner.
*/
context::CDList<std::shared_ptr<JustifyInfo> > d_stack;
/** Current number of entries in the stack that are valid */
context::CDO<size_t> d_stackSizeValid;
};
}
} // namespace cvc5
#endif /* CVC5__DECISION__JUSTIFY_INFO_H */
|
