Skip to content

Commit c6f282e

Browse files
aehyvariaehyvari
committed
TermPrinter: the initial version of DAG printer
1 parent 8142f04 commit c6f282e

File tree

4 files changed

+330
-1
lines changed

4 files changed

+330
-1
lines changed

‎src/common/CMakeLists.txt‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,12 +19,14 @@ target_sources(common
1919
"${CMAKE_CURRENT_LIST_DIR}/PartitionInfo.cc"
2020
"${CMAKE_CURRENT_LIST_DIR}/VerificationUtils.cc"
2121
"${CMAKE_CURRENT_LIST_DIR}/ReportUtils.h"
22+
"${CMAKE_CURRENT_LIST_DIR}/TermPrinter.h"
23+
"${CMAKE_CURRENT_LIST_DIR}/TermPrinter.cc"
2224
)
2325

2426
install(FILES
2527
Integer.h Number.h FastRational.h XAlloc.h Alloc.h StringMap.h Timer.h osmtinttypes.h
2628
TreeOps.h Real.h FlaPartitionMap.h PartitionInfo.h OsmtApiException.h TypeUtils.h
27-
NumberUtils.h NatSet.h
29+
NumberUtils.h NatSet.h TermPrinter.h
2830
DESTINATION ${INSTALL_HEADERS_DIR})
2931

3032

‎src/common/TermPrinter.cc‎

Lines changed: 187 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,187 @@
1+
//
2+
// Created by prova on 28.03.22.
3+
//
4+
5+
#include "TermPrinter.h"
6+
#include <iostream>
7+
8+
bool ReferenceCounterConfig::previsit(PTRef tr) {
9+
if (not previsitCount.has(tr)) {
10+
// The first visit
11+
previsitCount.insert(tr, 1);
12+
} else {
13+
// Visit because of the nth child
14+
auto n = previsitCount[tr] - 1;
15+
PTRef child = logic.getPterm(tr)[n];
16+
if (referenceCounts.find(child) == referenceCounts.end()) {
17+
referenceCounts.insert({child, 1});
18+
} else {
19+
++referenceCounts[child];
20+
}
21+
++previsitCount[tr];
22+
}
23+
return true;
24+
}
25+
26+
void TermPrinterConfig::visit(PTRef tr) {
27+
assert(termStrings.find(tr) == termStrings.end());
28+
Pterm const & term = logic.getPterm(tr);
29+
30+
std::string termString = logic.printSym(term.symb());
31+
32+
if (term.size() == 0) {
33+
termStrings.emplace(tr, std::move(termString));
34+
return;
35+
}
36+
assert(term.size() > 0);
37+
termString = '(' + termString + ' ';
38+
for (int i = 0; i < term.size(); i++) {
39+
PTRef child = term[i];
40+
assert(termStrings.find(child) != termStrings.end());
41+
termString += termStrings.at(child) + (i < term.size()-1 ? " " : "");
42+
-- refCounts[child];
43+
if (refCounts[child] == 0) {
44+
termStrings.erase(child);
45+
}
46+
}
47+
termString += ')';
48+
termStrings.emplace(tr, std::move(termString));
49+
}
50+
51+
void DagPrinterConfig::visit(PTRef tr) {
52+
// Todo: Ensure that the let identifier does not also appear as a symbol
53+
auto getLetSymbol = [](PTRef tr) { return "?l" + std::to_string(tr.x); };
54+
55+
assert(termStrings.find(tr) == termStrings.end());
56+
Pterm const & term = logic.getPterm(tr);
57+
58+
std::string symString = logic.printSym(term.symb());
59+
60+
if (term.size() == 0) {
61+
assert(definitions.find(tr) == definitions.end());
62+
termStrings.emplace(tr, std::move(symString));
63+
return;
64+
}
65+
66+
assert(term.size() > 0);
67+
auto defsInNode = definitions.find(tr);
68+
std::string openLetStatements;
69+
std::string closeLetStatements;
70+
if (defsInNode != definitions.end()) {
71+
auto const & defTerms = defsInNode->second;
72+
for (int i = defTerms.size()-1; i >= 0; i--) {
73+
// Note: Reverse order guarantees that dependencies are respected in let terms
74+
// Todo: Figure out if there is a dependency between two definitions
75+
PTRef def = defTerms[i];
76+
std::string letSymbol = getLetSymbol(def);
77+
openLetStatements += "(let ((" + letSymbol + " " + termStrings.at(def) + ")) ";
78+
closeLetStatements += ')';
79+
termStrings.erase(def);
80+
}
81+
}
82+
std::string termString = symString + ' ';
83+
for (int i = 0; i < term.size(); i++) {
84+
PTRef child = term[i];
85+
bool letDefined = isLetDefined(child);
86+
assert((termStrings.find(child) != termStrings.end()) or letDefined);
87+
termString += (letDefined ? getLetSymbol(child) : termStrings.at(child)) + (i < term.size()-1 ? " " : "");
88+
if (not letDefined) {
89+
-- refCounts[child];
90+
if (refCounts[child] == 0) {
91+
termStrings.erase(child);
92+
}
93+
}
94+
}
95+
termString = openLetStatements + '(' + termString + ')' + closeLetStatements;
96+
termStrings.emplace(tr, std::move(termString));
97+
}
98+
99+
bool SubGraphVisitorConfig::isAnAncestor(PTRef t, PTRef ancestor){
100+
auto rootNode = nodeFactory.findNode(t);
101+
assert(rootNode != nullptr);
102+
auto processed = logic.getTermMarks(logic.getPterm(root).getId());
103+
104+
std::vector<DFSElement> stack{DFSElement{rootNode, 0}};
105+
while (not stack.empty()) {
106+
auto & el = stack.back();
107+
auto & parents = el.node->parents;
108+
if (el.processedEdges < parents.size()) {
109+
auto nextParent = el.node->parents[el.processedEdges++];
110+
if (nextParent->tr == ancestor) {
111+
return true;
112+
}
113+
auto parentId = logic.getPterm(nextParent->tr).getId();
114+
if (not processed.isMarked(parentId)) {
115+
stack.emplace_back(nextParent, 0);
116+
}
117+
continue;
118+
}
119+
120+
auto currentId = logic.getPterm(el.node->tr).getId();
121+
122+
assert(not processed.isMarked(currentId));
123+
processed.mark(currentId);
124+
stack.pop_back();
125+
}
126+
return false;
127+
}
128+
129+
std::vector<PTRef> SubGraphVisitorConfig::removeReversePath(PTRef n, PTRef tr) {
130+
std::vector<PTRef> path{n};
131+
while (n != tr) {
132+
auto &node = *nodeFactory.findNode(n);
133+
assert(not node.parents.empty());
134+
n = node.parents.back()->tr;
135+
node.parents.pop_back();
136+
path.push_back(n);
137+
}
138+
return path;
139+
}
140+
141+
PTRef SubGraphVisitorConfig::findFirstMissingEdge(std::vector<PTRef> const & path) const {
142+
assert(not path.empty());
143+
PTRef child = path[0];
144+
if (path.size() == 1) {
145+
return child;
146+
}
147+
for (unsigned i = 1; i < path.size(); i++) {
148+
bool found = false;
149+
for (NodeFactory::Node * parent : nodeFactory.findNode(child)->parents) {
150+
if (parent->tr == path[i]) {
151+
found = true;
152+
break;
153+
}
154+
}
155+
if (not found) {
156+
return path[i-1];
157+
}
158+
child = path[i];
159+
}
160+
assert(false);
161+
return PTRef_Undef;
162+
}
163+
164+
std::string DagPrinter::print(PTRef tr) {
165+
ReferenceCounterConfig counter(logic);
166+
TermVisitor(logic, counter).visit(tr);
167+
std::unordered_map<PTRef,vec<PTRef>,PTRefHash> definitions;
168+
std::unordered_set<PTRef,PTRefHash> letDefinedTerms;
169+
for (auto [n, count] : counter.getReferences()) {
170+
if (not logic.isVar(n) and count > 1) {
171+
letDefinedTerms.insert(n);
172+
SubGraphVisitorConfig subGraphVisitorConfig(logic, tr);
173+
TermVisitor(logic, subGraphVisitorConfig).visit(tr);
174+
std::vector<PTRef> path = subGraphVisitorConfig.removeReversePath(n, tr);
175+
assert(not path.empty());
176+
PTRef definitionTerm = subGraphVisitorConfig.isAnAncestor(n, tr) ? tr : subGraphVisitorConfig.findFirstMissingEdge(path);
177+
if (definitions.find(definitionTerm) == definitions.end()) {
178+
definitions.insert({definitionTerm, vec<PTRef>{n}});
179+
} else {
180+
definitions.at(definitionTerm).push(n);
181+
}
182+
}
183+
}
184+
DagPrinterConfig printer(logic, counter.getReferences(), definitions, letDefinedTerms);
185+
TermVisitor(logic, printer).visit(tr);
186+
return printer.print(tr);
187+
}

‎src/common/TermPrinter.h‎

Lines changed: 130 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,130 @@
1+
//
2+
// Created by prova on 28.03.22.
3+
//
4+
5+
#ifndef OPENSMT_TERMPRINTER_H
6+
#define OPENSMT_TERMPRINTER_H
7+
8+
#include "TreeOps.h"
9+
#include "PTRef.h"
10+
11+
class ReferenceCounterConfig : public DefaultVisitorConfig {
12+
Logic const &logic;
13+
Map<PTRef, int, PTRefHash> previsitCount;
14+
std::unordered_map<PTRef, int, PTRefHash> referenceCounts;
15+
public:
16+
ReferenceCounterConfig(Logic const &logic) : logic(logic) {}
17+
bool previsit(PTRef tr);
18+
std::unordered_map<PTRef, int, PTRefHash> & getReferences() { return referenceCounts; };
19+
};
20+
21+
class TermPrinterConfig : public DefaultVisitorConfig {
22+
Logic const & logic;
23+
std::unordered_map<PTRef, int, PTRefHash> & refCounts;
24+
std::unordered_map<PTRef,std::string,PTRefHash> termStrings;
25+
public:
26+
TermPrinterConfig(Logic const & logic, std::unordered_map<PTRef, int, PTRefHash> & refCounts) : logic(logic), refCounts(refCounts) {}
27+
void visit(PTRef tr);
28+
std::string print(PTRef tr) { return termStrings.at(tr); }
29+
};
30+
31+
class TermPrinter {
32+
Logic const & logic;
33+
std::unordered_map<PTRef, std::string, PTRefHash> termStrings;
34+
public:
35+
TermPrinter(Logic const & logic) : logic(logic) {}
36+
std::string print(PTRef tr) {
37+
ReferenceCounterConfig counter(logic);
38+
TermVisitor(logic, counter).visit(tr);
39+
TermPrinterConfig printer(logic, counter.getReferences());
40+
TermVisitor(logic, printer).visit(tr);
41+
return printer.print(tr);
42+
}
43+
};
44+
45+
class DagPrinterConfig : public DefaultVisitorConfig {
46+
Logic const & logic;
47+
std::unordered_map<PTRef, int, PTRefHash> & refCounts;
48+
49+
std::unordered_map<PTRef,std::string,PTRefHash> termStrings;
50+
std::unordered_map<PTRef,vec<PTRef>,PTRefHash> const & definitions;
51+
std::unordered_set<PTRef,PTRefHash> const & letDefinedTerms;
52+
bool isLetDefined(PTRef tr) const { return letDefinedTerms.find(tr) != letDefinedTerms.end(); }
53+
public:
54+
DagPrinterConfig(Logic const & logic,
55+
std::unordered_map<PTRef, int, PTRefHash> & refCounts,
56+
std::unordered_map<PTRef,vec<PTRef>,PTRefHash> const & definitions,
57+
std::unordered_set<PTRef,PTRefHash> const & letDefinedTerms)
58+
: logic(logic)
59+
, refCounts(refCounts)
60+
, definitions(definitions)
61+
, letDefinedTerms(letDefinedTerms)
62+
{}
63+
void visit(PTRef tr) override;
64+
std::string print(PTRef tr) { assert(termStrings.size() == 1); return termStrings[tr]; }
65+
};
66+
67+
class SubGraphVisitorConfig : public DefaultVisitorConfig {
68+
Logic const & logic;
69+
PTRef root;
70+
class NodeFactory {
71+
public:
72+
struct Node {
73+
std::vector<Node *> parents;
74+
PTRef tr;
75+
void addParent(Node *c) {
76+
parents.push_back(c);
77+
}
78+
};
79+
std::vector<Node *> nodes;
80+
std::unordered_map<PTRef,NodeFactory::Node *,PTRefHash> ptrefToNode;
81+
public:
82+
~NodeFactory() {
83+
for (auto n : nodes) {
84+
delete n;
85+
}
86+
}
87+
Node * addNode(PTRef tr) {
88+
auto n = new Node{{}, tr};
89+
nodes.push_back(n);
90+
ptrefToNode.insert({tr, n});
91+
return n;
92+
}
93+
Node * findNode(PTRef tr) const { auto el = ptrefToNode.find(tr); return (el == ptrefToNode.end()) ? nullptr : el->second; }
94+
};
95+
96+
NodeFactory nodeFactory;
97+
98+
struct DFSElement {
99+
NodeFactory::Node * node;
100+
unsigned processedEdges;
101+
DFSElement(NodeFactory::Node * node, int processedEdges) : node(node), processedEdges(processedEdges) {}
102+
};
103+
104+
public:
105+
SubGraphVisitorConfig(Logic const & logic, PTRef root) : logic(logic), root(root) {}
106+
107+
bool isAnAncestor(PTRef t, PTRef ancestor);
108+
109+
void visit(PTRef tr) override {
110+
assert(nodeFactory.findNode(tr) == nullptr);
111+
auto node = nodeFactory.addNode(tr);
112+
for (auto childRef: logic.getPterm(tr)) {
113+
auto child = nodeFactory.findNode(childRef);
114+
assert(child);
115+
child->addParent(node);
116+
}
117+
}
118+
119+
std::vector<PTRef> removeReversePath(PTRef n, PTRef tr);
120+
PTRef findFirstMissingEdge(std::vector<PTRef> const & path) const;
121+
};
122+
123+
class DagPrinter {
124+
Logic const & logic;
125+
public:
126+
DagPrinter(Logic const & logic) : logic(logic) {}
127+
std::string print(PTRef tr);
128+
};
129+
130+
#endif //OPENSMT_TERMPRINTER_H

‎test/unit/test_TermPrinter.cc‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,17 @@ TEST_F(TermPrinterTest, test_TermPrinting) {
6060
PTRef ex2 = buildExampleFormula2();
6161
PTRef ex3 = buildExampleFormula3();
6262
for (PTRef ex : {ex1, ex2, ex3}) {
63+
ReferenceCounterConfig refCounter(logic);
64+
TermVisitor(logic, refCounter).visit(ex);
6365
std::cout << TermPrinter(logic).print(ex) << std::endl;
6466
ASSERT_EQ (TermPrinter(logic).print(ex), logic.pp(ex));
6567
}
68+
69+
for (PTRef ex : {ex1, ex2, ex3}) {
70+
DagPrinter printer(logic);
71+
std::cout << "===================================" << std::endl;
72+
std::cout << logic.pp(ex) << std::endl;
73+
std::cout << " -> " << std::endl;
74+
std::cout << printer.print(ex) << std::endl;
75+
}
6676
}

0 commit comments

Comments
 (0)