blob: 28c285a8f9e771e00420962104dff0641ecfbe12 (
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
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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
/******************************************************************************
* 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 assertion list
*/
#include "decision/assertion_list.h"
namespace cvc5 {
namespace decision {
const char* toString(DecisionStatus s)
{
switch (s)
{
case DecisionStatus::INACTIVE: return "INACTIVE";
case DecisionStatus::NO_DECISION: return "NO_DECISION";
case DecisionStatus::DECISION: return "DECISION";
case DecisionStatus::BACKTRACK: return "BACKTRACK";
default: return "?";
}
}
std::ostream& operator<<(std::ostream& out, DecisionStatus s)
{
out << toString(s);
return out;
}
AssertionList::AssertionList(context::Context* ac,
context::Context* ic,
bool useDyn)
: d_assertions(ac),
d_assertionIndex(ic),
d_usingDynamic(useDyn),
d_dindex(ic)
{
}
void AssertionList::presolve()
{
Trace("jh-status") << "AssertionList::presolve" << std::endl;
d_assertionIndex = 0;
d_dlist.clear();
d_dindex = 0;
}
void AssertionList::addAssertion(TNode n) { d_assertions.push_back(n); }
TNode AssertionList::getNextAssertion()
{
size_t fromIndex;
if (d_usingDynamic)
{
// is a dynamic assertion ready?
fromIndex = d_dindex.get();
if (fromIndex < d_dlist.size())
{
d_dindex = d_dindex.get() + 1;
Trace("jh-status") << "Assertion " << d_dlist[fromIndex].getId()
<< " from dynamic list" << std::endl;
return d_dlist[fromIndex];
}
}
// check if dynamic assertions
fromIndex = d_assertionIndex.get();
Assert(fromIndex <= d_assertions.size());
if (fromIndex == d_assertions.size())
{
return Node::null();
}
// increment for the next iteration
d_assertionIndex = d_assertionIndex + 1;
Trace("jh-status") << "Assertion " << d_assertions[fromIndex].getId()
<< std::endl;
return d_assertions[fromIndex];
}
size_t AssertionList::size() const { return d_assertions.size(); }
void AssertionList::notifyStatus(TNode n, DecisionStatus s)
{
Trace("jh-status") << "Assertion status " << s << " for " << n.getId()
<< ", current " << d_dindex.get() << "/" << d_dlist.size()
<< std::endl;
if (!d_usingDynamic)
{
// not using dynamic ordering, return
return;
}
if (s == DecisionStatus::NO_DECISION)
{
// no decision does not impact the decision order
return;
}
std::unordered_set<TNode>::iterator it = d_dlistSet.find(n);
if (s == DecisionStatus::DECISION)
{
if (it == d_dlistSet.end())
{
// if we just had a status on an assertion and it didn't occur in dlist,
// then our index should have exhausted dlist
Assert(d_dindex.get() == d_dlist.size());
if (d_dindex.get() == d_dlist.size())
{
d_dindex = d_dindex.get() + 1;
}
// add to back of the decision list if not already there
d_dlist.push_back(n);
d_dlistSet.insert(n);
Trace("jh-status") << "...push due to decision" << std::endl;
}
return;
}
if (s == DecisionStatus::BACKTRACK)
{
// backtrack inserts at the current position
if (it == d_dlistSet.end())
{
d_dlist.insert(d_dlist.begin(), n);
d_dlistSet.insert(n);
}
}
}
} // namespace decision
} // namespace cvc5
|
