blob: 558e1b36bd72846d5939b39017b6972e36cb171a (
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
|
/********************* */
/*! \file sygus_explain.cpp
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2017 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.\endverbatim
**
** \brief Implementation of techniques for sygus explanations
**/
#include "theory/quantifiers/sygus_explain.h"
using namespace CVC4::kind;
using namespace std;
namespace CVC4 {
namespace theory {
namespace quantifiers {
void TermRecBuild::addTerm(Node n)
{
d_term.push_back(n);
std::vector<Node> currc;
d_kind.push_back(n.getKind());
if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
{
currc.push_back(n.getOperator());
d_has_op.push_back(true);
}
else
{
d_has_op.push_back(false);
}
for (unsigned i = 0; i < n.getNumChildren(); i++)
{
currc.push_back(n[i]);
}
d_children.push_back(currc);
}
void TermRecBuild::init(Node n)
{
Assert(d_term.empty());
addTerm(n);
}
void TermRecBuild::push(unsigned p)
{
Assert(!d_term.empty());
unsigned curr = d_term.size() - 1;
Assert(d_pos.size() == curr);
Assert(d_pos.size() + 1 == d_children.size());
Assert(p < d_term[curr].getNumChildren());
addTerm(d_term[curr][p]);
d_pos.push_back(p);
}
void TermRecBuild::pop()
{
Assert(!d_pos.empty());
d_pos.pop_back();
d_kind.pop_back();
d_has_op.pop_back();
d_children.pop_back();
d_term.pop_back();
}
void TermRecBuild::replaceChild(unsigned i, Node r)
{
Assert(!d_term.empty());
unsigned curr = d_term.size() - 1;
unsigned o = d_has_op[curr] ? 1 : 0;
d_children[curr][i + o] = r;
}
Node TermRecBuild::getChild(unsigned i)
{
unsigned curr = d_term.size() - 1;
unsigned o = d_has_op[curr] ? 1 : 0;
return d_children[curr][i + o];
}
Node TermRecBuild::build(unsigned d)
{
Assert(d_pos.size() + 1 == d_term.size());
Assert(d < d_term.size());
int p = d < d_pos.size() ? d_pos[d] : -2;
std::vector<Node> children;
unsigned o = d_has_op[d] ? 1 : 0;
for (unsigned i = 0; i < d_children[d].size(); i++)
{
Node nc;
if (p + o == i)
{
nc = build(d + 1);
}
else
{
nc = d_children[d][i];
}
children.push_back(nc);
}
return NodeManager::currentNM()->mkNode(d_kind[d], children);
}
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
|
