|
| 1 | +/*******************************************************************\ |
| 2 | +
|
| 3 | +Module: SMT2 solver |
| 4 | +
|
| 5 | +Author: Romain Brenguier, [email protected] |
| 6 | +
|
| 7 | +\*******************************************************************/ |
| 8 | + |
| 9 | +#include "smt2_ast.h" |
| 10 | +#include <deque> |
| 11 | +#include <util/as_const.h> |
| 12 | +#include <util/make_unique.h> |
| 13 | +#include <util/mp_arith.h> |
| 14 | +#include <util/range.h> |
| 15 | + |
| 16 | +struct smt2_ast_strategyt |
| 17 | +{ |
| 18 | + std::function<void(const smt2_astt &)> data; |
| 19 | + std::function<void(const smt2_astt &)> parent; |
| 20 | + std::function<void(const smt2_astt &)> first_child; |
| 21 | + std::function<void(const smt2_astt &)> next_sibling; |
| 22 | +}; |
| 23 | + |
| 24 | +/// Intermediary types for the \ref smt2_dfs_stackt definition |
| 25 | +using tree_iteratort = smt2_astt::tree_implementationt::subt::const_iterator; |
| 26 | +using stack_elementt = ranget<tree_iteratort>; |
| 27 | + |
| 28 | +/// Stack class to help with DFS exploration of smt2_astt. |
| 29 | +/// The stack stores an iterator for each level above the current position, |
| 30 | +/// as well as the corresponding \c end iterator |
| 31 | +class smt2_dfs_stackt : public std::deque<stack_elementt> |
| 32 | +{ |
| 33 | +public: |
| 34 | + /// Current node if the stack is currently pointing to one, nullptr if it |
| 35 | + /// needs to come back to its parent. |
| 36 | + const smt2_astt *current_node() const |
| 37 | + { |
| 38 | + PRECONDITION(!empty()); |
| 39 | + if(back().empty()) |
| 40 | + return nullptr; |
| 41 | + return &(*back().begin()); |
| 42 | + } |
| 43 | + |
| 44 | + bool has_next_sibling() const |
| 45 | + { |
| 46 | + PRECONDITION(!empty()); |
| 47 | + auto it = back().begin(); |
| 48 | + it++; |
| 49 | + return it != back().end(); |
| 50 | + } |
| 51 | + |
| 52 | + /// Advance to next sibling if it exists, otherwise render the `back` |
| 53 | + /// element of the stack empty. |
| 54 | + void go_to_next_sibling() |
| 55 | + { |
| 56 | + PRECONDITION(!empty()); |
| 57 | + back() = std::move(back()).drop(1); |
| 58 | + } |
| 59 | + |
| 60 | + const smt2_astt *parent() const |
| 61 | + { |
| 62 | + if(this->empty()) |
| 63 | + return nullptr; |
| 64 | + auto it = this->end(); |
| 65 | + (it--)--; |
| 66 | + return &(*it->begin()); |
| 67 | + } |
| 68 | +}; |
| 69 | + |
| 70 | +static void dfs(const smt2_astt &ast, const smt2_ast_strategyt &strategy) |
| 71 | +{ |
| 72 | + strategy.data(ast); |
| 73 | + auto begin = ast.read().sub.begin(); |
| 74 | + auto end = ast.read().sub.end(); |
| 75 | + if(begin == end) |
| 76 | + return; |
| 77 | + strategy.first_child(ast); |
| 78 | + smt2_dfs_stackt stack; |
| 79 | + stack.emplace_back(begin, end); |
| 80 | + |
| 81 | + while(!stack.empty()) |
| 82 | + { |
| 83 | + const auto current = stack.current_node(); |
| 84 | + INVARIANT( |
| 85 | + current != nullptr, |
| 86 | + "at each iteration of the loop, the stack should be positioned on an " |
| 87 | + "existing element"); |
| 88 | + strategy.data(*current); |
| 89 | + const smt2_astt::tree_implementationt::subt &children = current->read().sub; |
| 90 | + if(!children.empty()) |
| 91 | + { |
| 92 | + stack.emplace_back(children.begin(), children.end()); |
| 93 | + strategy.first_child(*current); |
| 94 | + } |
| 95 | + else |
| 96 | + { |
| 97 | + if(stack.has_next_sibling()) |
| 98 | + { |
| 99 | + auto p = stack.parent(); |
| 100 | + INVARIANT(p, "siblings must have a parent"); |
| 101 | + strategy.next_sibling(*p); |
| 102 | + } |
| 103 | + stack.go_to_next_sibling(); |
| 104 | + while(!stack.empty() && stack.current_node() == nullptr) |
| 105 | + { |
| 106 | + stack.pop_back(); |
| 107 | + if(!stack.empty()) |
| 108 | + { |
| 109 | + auto current = stack.current_node(); |
| 110 | + INVARIANT( |
| 111 | + current != nullptr, |
| 112 | + "ranges in the stack should be positioned on existing nodes"); |
| 113 | + // We came back to current after all its children |
| 114 | + strategy.parent(*current); |
| 115 | + if(stack.has_next_sibling()) |
| 116 | + { |
| 117 | + auto p = stack.parent(); |
| 118 | + INVARIANT(p, "siblings must have a parent"); |
| 119 | + strategy.next_sibling(*p); |
| 120 | + } |
| 121 | + stack.go_to_next_sibling(); |
| 122 | + } |
| 123 | + else |
| 124 | + { |
| 125 | + strategy.parent(ast); |
| 126 | + } |
| 127 | + } |
| 128 | + } |
| 129 | + } |
| 130 | +} |
| 131 | + |
| 132 | +static void print_data(std::ostream &stream, const smt2_astt &ast) |
| 133 | +{ |
| 134 | + if(ast.id() == ID_symbol || ast.id() == ID_constant) |
| 135 | + { |
| 136 | + INVARIANT( |
| 137 | + ast.read().named_sub.has_value(), |
| 138 | + "constant and symbols should have an non-empty `named_sub` field"); |
| 139 | + stream << ast.read().named_sub.value(); |
| 140 | + } |
| 141 | + else if(ast.id() == ID_string_constant) |
| 142 | + { |
| 143 | + stream << '\"' << ast.read().sub[0].id() << '\"'; |
| 144 | + } |
| 145 | + else if(ast.id() == ID_tuple && ast.read().sub.empty()) |
| 146 | + { |
| 147 | + stream << "()"; |
| 148 | + } |
| 149 | +} |
| 150 | + |
| 151 | +std::ostream &operator<<(std::ostream &stream, const smt2_astt &ast) |
| 152 | +{ |
| 153 | + smt2_ast_strategyt print_visitor; |
| 154 | + print_visitor.data = [&stream](const smt2_astt &ast) { |
| 155 | + print_data(stream, ast); |
| 156 | + }; |
| 157 | + print_visitor.first_child = [&stream](const smt2_astt &ast) { |
| 158 | + if(ast.id() == ID_identifier) |
| 159 | + stream << "(_ "; |
| 160 | + else if(ast.id() == ID_forall) |
| 161 | + stream << "(forall "; |
| 162 | + else if(ast.id() == ID_exists) |
| 163 | + stream << "(exists "; |
| 164 | + else if(ast.id() == ID_let) |
| 165 | + stream << "(let "; |
| 166 | + else if(ast.id() == ID_par) |
| 167 | + stream << "(par "; |
| 168 | + else |
| 169 | + stream << "("; |
| 170 | + }; |
| 171 | + print_visitor.next_sibling = [&stream](const smt2_astt &ast) { |
| 172 | + stream << " "; |
| 173 | + }; |
| 174 | + print_visitor.parent = [&stream](const smt2_astt &ast) { stream << ")"; }; |
| 175 | + dfs(ast, print_visitor); |
| 176 | + return stream; |
| 177 | +} |
| 178 | + |
| 179 | +smt2_sortt::smt2_sortt( |
| 180 | + smt2_identifiert identifier, |
| 181 | + std::vector<smt2_sortt> &¶meters) |
| 182 | + : smt2_astt(ID_type) |
| 183 | +{ |
| 184 | + if(!parameters.empty()) |
| 185 | + { |
| 186 | + auto &subs = write().sub; |
| 187 | + subs.emplace_back(std::move(identifier)); |
| 188 | + std::move(parameters.begin(), parameters.end(), std::back_inserter(subs)); |
| 189 | + } |
| 190 | + else |
| 191 | + *this = smt2_sortt(std::move(identifier)); |
| 192 | +} |
0 commit comments