TermPrinter: the initial version of DAG printer

src/common/CMakeLists.txt

@@ -19,12 +19,14 @@ target_sources(common
     "${CMAKE_CURRENT_LIST_DIR}/PartitionInfo.cc"
     "${CMAKE_CURRENT_LIST_DIR}/VerificationUtils.cc"
     "${CMAKE_CURRENT_LIST_DIR}/ReportUtils.h"
+    "${CMAKE_CURRENT_LIST_DIR}/TermPrinter.h"
+    "${CMAKE_CURRENT_LIST_DIR}/TermPrinter.cc"
 )
 
 install(FILES
         Integer.h Number.h FastRational.h XAlloc.h Alloc.h StringMap.h Timer.h osmtinttypes.h
         TreeOps.h Real.h FlaPartitionMap.h PartitionInfo.h OsmtApiException.h TypeUtils.h 
-        NumberUtils.h NatSet.h
+        NumberUtils.h NatSet.h TermPrinter.h
 DESTINATION ${INSTALL_HEADERS_DIR})
 
 

src/common/TermPrinter.cc

@@ -0,0 +1,187 @@
+//
+// Created by prova on 28.03.22.
+//
+
+#include "TermPrinter.h"
+#include <iostream>
+
+bool ReferenceCounterConfig::previsit(PTRef tr) {
+    if (not previsitCount.has(tr)) {
+        // The first visit
+        previsitCount.insert(tr, 1);
+    } else {
+        // Visit because of the nth child
+        auto n = previsitCount[tr] - 1;
+        PTRef child = logic.getPterm(tr)[n];
+        if (referenceCounts.find(child) == referenceCounts.end()) {
+            referenceCounts.insert({child, 1});
+        } else {
+            ++referenceCounts[child];
+        }
+        ++previsitCount[tr];
+    }
+    return true;
+}
+
+void TermPrinterConfig::visit(PTRef tr) {
+    assert(termStrings.find(tr) == termStrings.end());
+    Pterm const & term = logic.getPterm(tr);
+
+    std::string termString = logic.printSym(term.symb());
+
+    if (term.size() == 0) {
+        termStrings.emplace(tr, std::move(termString));
+        return;
+    }
+    assert(term.size() > 0);
+    termString = '(' + termString + ' ';
+    for (int i = 0; i < term.size(); i++) {
+        PTRef child = term[i];
+        assert(termStrings.find(child) != termStrings.end());
+        termString += termStrings.at(child) + (i < term.size()-1 ? " " : "");
+        -- refCounts[child];
+        if (refCounts[child] == 0) {
+            termStrings.erase(child);
+        }
+    }
+    termString += ')';
+    termStrings.emplace(tr, std::move(termString));
+}
+
+void DagPrinterConfig::visit(PTRef tr) {
+    // Todo: Ensure that the let identifier does not also appear as a symbol
+    auto getLetSymbol = [](PTRef tr) { return "?l" + std::to_string(tr.x); };
+
+    assert(termStrings.find(tr) == termStrings.end());
+    Pterm const & term = logic.getPterm(tr);
+
+    std::string symString = logic.printSym(term.symb());
+
+    if (term.size() == 0) {
+        assert(definitions.find(tr) == definitions.end());
+        termStrings.emplace(tr, std::move(symString));
+        return;
+    }
+
+    assert(term.size() > 0);
+    auto defsInNode = definitions.find(tr);
+    std::string openLetStatements;
+    std::string closeLetStatements;
+    if (defsInNode != definitions.end()) {
+        auto const & defTerms = defsInNode->second;
+        for (int i = defTerms.size()-1; i >= 0; i--) {
+            // Note: Reverse order guarantees that dependencies are respected in let terms
+            // Todo: Figure out if there is a dependency between two definitions
+            PTRef def = defTerms[i];
+            std::string letSymbol = getLetSymbol(def);
+            openLetStatements += "(let ((" + letSymbol + " " + termStrings.at(def) + ")) ";
+            closeLetStatements += ')';
+            termStrings.erase(def);
+        }
+    }
+    std::string termString = symString + ' ';
+    for (int i = 0; i < term.size(); i++) {
+        PTRef child = term[i];
+        bool letDefined = isLetDefined(child);
+        assert((termStrings.find(child) != termStrings.end()) or letDefined);
+        termString += (letDefined  ? getLetSymbol(child) : termStrings.at(child)) + (i < term.size()-1 ? " " : "");
+        if (not letDefined) {
+            -- refCounts[child];
+            if (refCounts[child] == 0) {
+                termStrings.erase(child);
+            }
+        }
+    }
+    termString = openLetStatements + '(' + termString + ')' + closeLetStatements;
+    termStrings.emplace(tr, std::move(termString));
+}
+
+bool SubGraphVisitorConfig::isAnAncestor(PTRef t, PTRef ancestor){
+    auto rootNode = nodeFactory.findNode(t);
+    assert(rootNode != nullptr);
+    auto processed = logic.getTermMarks(logic.getPterm(root).getId());
+
+    std::vector<DFSElement> stack{DFSElement{rootNode, 0}};
+    while (not stack.empty()) {
+        auto & el = stack.back();
+        auto & parents = el.node->parents;
+        if (el.processedEdges < parents.size()) {
+            auto nextParent = el.node->parents[el.processedEdges++];
+            if (nextParent->tr == ancestor) {
+                return true;
+            }
+            auto parentId = logic.getPterm(nextParent->tr).getId();
+            if (not processed.isMarked(parentId)) {
+                stack.emplace_back(nextParent, 0);
+            }
+            continue;
+        }
+
+        auto currentId = logic.getPterm(el.node->tr).getId();
+
+        assert(not processed.isMarked(currentId));
+        processed.mark(currentId);
+        stack.pop_back();
+    }
+    return false;
+}
+
+std::vector<PTRef> SubGraphVisitorConfig::removeReversePath(PTRef n, PTRef tr) {
+    std::vector<PTRef> path{n};
+    while (n != tr) {
+        auto &node = *nodeFactory.findNode(n);
+        assert(not node.parents.empty());
+        n = node.parents.back()->tr;
+        node.parents.pop_back();
+        path.push_back(n);
+    }
+    return path;
+}
+
+PTRef SubGraphVisitorConfig::findFirstMissingEdge(std::vector<PTRef> const & path) const {
+    assert(not path.empty());
+    PTRef child = path[0];
+    if (path.size() == 1) {
+        return child;
+    }
+    for (unsigned i = 1; i < path.size(); i++) {
+        bool found = false;
+        for (NodeFactory::Node * parent : nodeFactory.findNode(child)->parents) {
+            if (parent->tr == path[i]) {
+                found = true;
+                break;
+            }
+        }
+        if (not found) {
+            return path[i-1];
+        }
+        child = path[i];
+    }
+    assert(false);
+    return PTRef_Undef;
+}
+
+std::string DagPrinter::print(PTRef tr) {
+    ReferenceCounterConfig counter(logic);
+    TermVisitor(logic, counter).visit(tr);
+    std::unordered_map<PTRef,vec<PTRef>,PTRefHash> definitions;
+    std::unordered_set<PTRef,PTRefHash> letDefinedTerms;
+    for (auto [n, count] : counter.getReferences()) {
+        if (not logic.isVar(n) and count > 1) {
+            letDefinedTerms.insert(n);
+            SubGraphVisitorConfig subGraphVisitorConfig(logic, tr);
+            TermVisitor(logic, subGraphVisitorConfig).visit(tr);
+            std::vector<PTRef> path = subGraphVisitorConfig.removeReversePath(n, tr);
+            assert(not path.empty());
+            PTRef definitionTerm = subGraphVisitorConfig.isAnAncestor(n, tr) ? tr : subGraphVisitorConfig.findFirstMissingEdge(path);
+            if (definitions.find(definitionTerm) == definitions.end()) {
+                definitions.insert({definitionTerm, vec<PTRef>{n}});
+            } else {
+                definitions.at(definitionTerm).push(n);
+            }
+        }
+    }
+    DagPrinterConfig printer(logic, counter.getReferences(), definitions, letDefinedTerms);
+    TermVisitor(logic, printer).visit(tr);
+    return printer.print(tr);
+}

src/common/TermPrinter.h

@@ -0,0 +1,130 @@
+//
+// Created by prova on 28.03.22.
+//
+
+#ifndef OPENSMT_TERMPRINTER_H
+#define OPENSMT_TERMPRINTER_H
+
+#include "TreeOps.h"
+#include "PTRef.h"
+
+class ReferenceCounterConfig : public DefaultVisitorConfig {
+    Logic const &logic;
+    Map<PTRef, int, PTRefHash> previsitCount;
+    std::unordered_map<PTRef, int, PTRefHash> referenceCounts;
+public:
+    ReferenceCounterConfig(Logic const &logic) : logic(logic) {}
+    bool previsit(PTRef tr);
+    std::unordered_map<PTRef, int, PTRefHash> & getReferences() { return referenceCounts; };
+};
+
+class TermPrinterConfig : public DefaultVisitorConfig {
+    Logic const & logic;
+    std::unordered_map<PTRef, int, PTRefHash> & refCounts;
+    std::unordered_map<PTRef,std::string,PTRefHash> termStrings;
+public:
+    TermPrinterConfig(Logic const & logic, std::unordered_map<PTRef, int, PTRefHash> & refCounts) : logic(logic), refCounts(refCounts) {}
+    void visit(PTRef tr);
+    std::string print(PTRef tr) { return termStrings.at(tr); }
+};
+
+class TermPrinter {
+    Logic const & logic;
+    std::unordered_map<PTRef, std::string, PTRefHash> termStrings;
+public:
+    TermPrinter(Logic const & logic) : logic(logic) {}
+    std::string print(PTRef tr) {
+        ReferenceCounterConfig counter(logic);
+        TermVisitor(logic, counter).visit(tr);
+        TermPrinterConfig printer(logic, counter.getReferences());
+        TermVisitor(logic, printer).visit(tr);
+        return printer.print(tr);
+    }
+};
+
+class DagPrinterConfig : public DefaultVisitorConfig {
+    Logic const & logic;
+    std::unordered_map<PTRef, int, PTRefHash> & refCounts;
+
+    std::unordered_map<PTRef,std::string,PTRefHash> termStrings;
+    std::unordered_map<PTRef,vec<PTRef>,PTRefHash> const & definitions;
+    std::unordered_set<PTRef,PTRefHash> const & letDefinedTerms;
+    bool isLetDefined(PTRef tr) const { return letDefinedTerms.find(tr) != letDefinedTerms.end(); }
+public:
+    DagPrinterConfig(Logic const & logic,
+                     std::unordered_map<PTRef, int, PTRefHash> & refCounts,
+                     std::unordered_map<PTRef,vec<PTRef>,PTRefHash> const & definitions,
+                     std::unordered_set<PTRef,PTRefHash> const & letDefinedTerms)
+    : logic(logic)
+    , refCounts(refCounts)
+    , definitions(definitions)
+    , letDefinedTerms(letDefinedTerms)
+    {}
+    void visit(PTRef tr) override;
+    std::string print(PTRef tr) { assert(termStrings.size() == 1); return termStrings[tr]; }
+};
+
+class SubGraphVisitorConfig : public DefaultVisitorConfig {
+    Logic const & logic;
+    PTRef root;
+    class NodeFactory {
+    public:
+        struct Node {
+            std::vector<Node *> parents;
+            PTRef tr;
+            void addParent(Node *c) {
+                parents.push_back(c);
+            }
+        };
+        std::vector<Node *> nodes;
+        std::unordered_map<PTRef,NodeFactory::Node *,PTRefHash> ptrefToNode;
+    public:
+        ~NodeFactory() {
+            for (auto n : nodes) {
+                delete n;
+            }
+        }
+        Node * addNode(PTRef tr) {
+            auto n = new Node{{}, tr};
+            nodes.push_back(n);
+            ptrefToNode.insert({tr, n});
+            return n;
+        }
+        Node * findNode(PTRef tr) const { auto el = ptrefToNode.find(tr); return (el == ptrefToNode.end()) ? nullptr : el->second; }
+    };
+
+    NodeFactory nodeFactory;
+
+    struct DFSElement {
+        NodeFactory::Node * node;
+        unsigned processedEdges;
+        DFSElement(NodeFactory::Node * node, int processedEdges) : node(node), processedEdges(processedEdges) {}
+    };
+
+public:
+    SubGraphVisitorConfig(Logic const & logic, PTRef root) : logic(logic), root(root) {}
+
+    bool isAnAncestor(PTRef t, PTRef ancestor);
+
+    void visit(PTRef tr) override {
+        assert(nodeFactory.findNode(tr) == nullptr);
+        auto node = nodeFactory.addNode(tr);
+        for (auto childRef: logic.getPterm(tr)) {
+            auto child = nodeFactory.findNode(childRef);
+            assert(child);
+            child->addParent(node);
+        }
+    }
+
+    std::vector<PTRef> removeReversePath(PTRef n, PTRef tr);
+    PTRef findFirstMissingEdge(std::vector<PTRef> const & path) const;
+};
+
+class DagPrinter {
+    Logic const & logic;
+public:
+    DagPrinter(Logic const & logic) : logic(logic) {}
+    std::string print(PTRef tr);
+};
+
+#endif //OPENSMT_TERMPRINTER_H

test/unit/test_TermPrinter.cc

@@ -60,7 +60,17 @@ TEST_F(TermPrinterTest, test_TermPrinting) {
     PTRef ex2 = buildExampleFormula2();
     PTRef ex3 = buildExampleFormula3();
     for (PTRef ex : {ex1, ex2, ex3}) {
+        ReferenceCounterConfig refCounter(logic);
+        TermVisitor(logic, refCounter).visit(ex);
         std::cout << TermPrinter(logic).print(ex) << std::endl;
         ASSERT_EQ (TermPrinter(logic).print(ex), logic.pp(ex));
     }
+
+    for (PTRef ex : {ex1, ex2, ex3}) {
+        DagPrinter printer(logic);
+        std::cout << "===================================" << std::endl;
+        std::cout << logic.pp(ex) << std::endl;
+        std::cout << " -> " << std::endl;
+        std::cout << printer.print(ex) << std::endl;
+    }
 }