1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Implementation of assertion list |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "decision/assertion_list.h" |
17 |
|
|
18 |
|
namespace cvc5 { |
19 |
|
namespace decision { |
20 |
|
|
21 |
|
const char* toString(DecisionStatus s) |
22 |
|
{ |
23 |
|
switch (s) |
24 |
|
{ |
25 |
|
case DecisionStatus::INACTIVE: return "INACTIVE"; |
26 |
|
case DecisionStatus::NO_DECISION: return "NO_DECISION"; |
27 |
|
case DecisionStatus::DECISION: return "DECISION"; |
28 |
|
case DecisionStatus::BACKTRACK: return "BACKTRACK"; |
29 |
|
default: return "?"; |
30 |
|
} |
31 |
|
} |
32 |
|
|
33 |
|
std::ostream& operator<<(std::ostream& out, DecisionStatus s) |
34 |
|
{ |
35 |
|
out << toString(s); |
36 |
|
return out; |
37 |
|
} |
38 |
|
|
39 |
9924 |
AssertionList::AssertionList(context::Context* ac, |
40 |
|
context::Context* ic, |
41 |
9924 |
bool useDyn) |
42 |
|
: d_assertions(ac), |
43 |
|
d_assertionIndex(ic), |
44 |
|
d_usingDynamic(useDyn), |
45 |
9924 |
d_dindex(ic) |
46 |
|
{ |
47 |
9924 |
} |
48 |
|
|
49 |
12478 |
void AssertionList::presolve() |
50 |
|
{ |
51 |
12478 |
Trace("jh-status") << "AssertionList::presolve" << std::endl; |
52 |
12478 |
d_assertionIndex = 0; |
53 |
12478 |
d_dlist.clear(); |
54 |
12478 |
d_dindex = 0; |
55 |
12478 |
} |
56 |
|
|
57 |
260917 |
void AssertionList::addAssertion(TNode n) { d_assertions.push_back(n); } |
58 |
|
|
59 |
9009113 |
TNode AssertionList::getNextAssertion() |
60 |
|
{ |
61 |
|
size_t fromIndex; |
62 |
9009113 |
if (d_usingDynamic) |
63 |
|
{ |
64 |
|
// is a dynamic assertion ready? |
65 |
10677 |
fromIndex = d_dindex.get(); |
66 |
10677 |
if (fromIndex < d_dlist.size()) |
67 |
|
{ |
68 |
5392 |
d_dindex = d_dindex.get() + 1; |
69 |
10784 |
Trace("jh-status") << "Assertion " << d_dlist[fromIndex].getId() |
70 |
5392 |
<< " from dynamic list" << std::endl; |
71 |
5392 |
return d_dlist[fromIndex]; |
72 |
|
} |
73 |
|
} |
74 |
|
// check if dynamic assertions |
75 |
9003721 |
fromIndex = d_assertionIndex.get(); |
76 |
9003721 |
Assert(fromIndex <= d_assertions.size()); |
77 |
9003721 |
if (fromIndex == d_assertions.size()) |
78 |
|
{ |
79 |
4251368 |
return Node::null(); |
80 |
|
} |
81 |
|
// increment for the next iteration |
82 |
4752353 |
d_assertionIndex = d_assertionIndex + 1; |
83 |
9504706 |
Trace("jh-status") << "Assertion " << d_assertions[fromIndex].getId() |
84 |
4752353 |
<< std::endl; |
85 |
4752353 |
return d_assertions[fromIndex]; |
86 |
|
} |
87 |
260917 |
size_t AssertionList::size() const { return d_assertions.size(); } |
88 |
|
|
89 |
4490186 |
void AssertionList::notifyStatus(TNode n, DecisionStatus s) |
90 |
|
{ |
91 |
8980372 |
Trace("jh-status") << "Assertion status " << s << " for " << n.getId() |
92 |
8980372 |
<< ", current " << d_dindex.get() << "/" << d_dlist.size() |
93 |
4490186 |
<< std::endl; |
94 |
4490186 |
if (!d_usingDynamic) |
95 |
|
{ |
96 |
|
// not using dynamic ordering, return |
97 |
8969564 |
return; |
98 |
|
} |
99 |
10572 |
if (s == DecisionStatus::NO_DECISION) |
100 |
|
{ |
101 |
|
// no decision does not impact the decision order |
102 |
9724 |
return; |
103 |
|
} |
104 |
848 |
std::unordered_set<TNode>::iterator it = d_dlistSet.find(n); |
105 |
848 |
if (s == DecisionStatus::DECISION) |
106 |
|
{ |
107 |
612 |
if (it == d_dlistSet.end()) |
108 |
|
{ |
109 |
|
// if we just had a status on an assertion and it didn't occur in dlist, |
110 |
|
// then our index should have exhausted dlist |
111 |
28 |
Assert(d_dindex.get() == d_dlist.size()); |
112 |
28 |
if (d_dindex.get() == d_dlist.size()) |
113 |
|
{ |
114 |
28 |
d_dindex = d_dindex.get() + 1; |
115 |
|
} |
116 |
|
// add to back of the decision list if not already there |
117 |
28 |
d_dlist.push_back(n); |
118 |
28 |
d_dlistSet.insert(n); |
119 |
28 |
Trace("jh-status") << "...push due to decision" << std::endl; |
120 |
|
} |
121 |
612 |
return; |
122 |
|
} |
123 |
236 |
if (s == DecisionStatus::BACKTRACK) |
124 |
|
{ |
125 |
|
// backtrack inserts at the current position |
126 |
236 |
if (it == d_dlistSet.end()) |
127 |
|
{ |
128 |
15 |
d_dlist.insert(d_dlist.begin(), n); |
129 |
15 |
d_dlistSet.insert(n); |
130 |
|
} |
131 |
|
} |
132 |
|
} |
133 |
|
|
134 |
|
} // namespace decision |
135 |
22746 |
} // namespace cvc5 |