diff --git a/src/aalwines/query/QueryBuilder.cpp b/src/aalwines/query/QueryBuilder.cpp index 2390232..782543d 100644 --- a/src/aalwines/query/QueryBuilder.cpp +++ b/src/aalwines/query/QueryBuilder.cpp @@ -109,16 +109,22 @@ namespace aalwines Builder::labelset_t Builder::expand_labels(Query::label_t label) { if(!_expand) return {label}; - + Builder::labelset_t res; if(label.type() == Query::ANYMPLS) { - return _network.get_labels(0, 255, _sticky ? Query::STICKY_MPLS : Query::MPLS); + res = _network.get_labels(0, 255, _sticky ? Query::STICKY_MPLS : Query::MPLS); } else if(label.type() == Query::ANYSTICKY) { - return _network.get_labels(0, 255, Query::STICKY_MPLS); + res = _network.get_labels(0, 255, Query::STICKY_MPLS); } - return _network.get_labels(label.value(), label.mask(), label.type()); + else + { + res = _network.get_labels(label.value(), label.mask(), label.type()); + } + if(res.empty()) + throw no_match_error(_location, "Empty match of labels"); + return res; } Builder::labelset_t Builder::match_ip4(int i1, int i2, int i3, int i4, int mask) @@ -168,7 +174,10 @@ namespace aalwines ptr[6] = i2; ptr[7] = i1; val = ((val << mask) >> mask); // canonize - return expand_labels(Query::label_t(Query::IP6, static_cast(mask), val)); + auto res = expand_labels(Query::label_t(Query::IP6, static_cast(mask), val)); + if(res.empty()) + throw no_match_error(_location, "Empty match of IPv6"); + return res; } filter_t Builder::match_exact(const std::string& str) @@ -224,7 +233,10 @@ namespace aalwines Builder::labelset_t Builder::find_label(uint64_t label, uint64_t mask) { - return _network.get_labels(label, mask, _sticky ? Query::STICKY_MPLS : Query::MPLS, !_expand); + auto res = _network.get_labels(label, mask, _sticky ? Query::STICKY_MPLS : Query::MPLS, !_expand); + if(res.empty()) + throw no_match_error(_location, "Empty match of labels"); + return res; } filter_t Builder::discard_id() @@ -251,12 +263,17 @@ namespace aalwines Builder::labelset_t Builder::filter(filter_t& f) { - return _network.interfaces(f); + auto res = _network.interfaces(f); + if(res.empty()) + throw no_match_error(_location, "Empty match of labels"); + return res; } Builder::labelset_t Builder::filter_and_merge(filter_t& f, labelset_t& r) { auto res = filter(f); + if(res.empty()) + throw no_match_error(_location, "Empty match of labels"); res.insert(r.begin(), r.end()); return res; } diff --git a/src/aalwines/query/QueryBuilder.h b/src/aalwines/query/QueryBuilder.h index 71438dd..e02b5e4 100644 --- a/src/aalwines/query/QueryBuilder.h +++ b/src/aalwines/query/QueryBuilder.h @@ -107,7 +107,7 @@ namespace aalwines { void error(const std::string &m); Network& _network; - location _location; + location _location; std::vector _result; // filtering diff --git a/src/aalwines/query/parsererrors.h b/src/aalwines/query/parsererrors.h index ba5bc35..10b7373 100644 --- a/src/aalwines/query/parsererrors.h +++ b/src/aalwines/query/parsererrors.h @@ -34,88 +34,63 @@ namespace aalwines { struct base_parser_error : public base_error { - + location _location; base_parser_error(const location &l, std::string m) - : base_error(m), _location() { - std::stringstream ss; - ss << "[" << l << "]"; - _location = ss.str(); + : base_error(m), _location(l) { } explicit base_parser_error(std::string m) : base_error(std::move(m)) { } - std::string _location; const char *what() const noexcept override { return _message.c_str(); } - virtual std::string prefix() const { - return "base error "; - } - - virtual void print(std::ostream &os) const { - os << prefix() << " " << _location << " : " << what() << std::endl; + void print_json(std::ostream& os) const override + { + start(os); + if(_location.begin.filename) + os << R"(,"inputName":")" << _location.begin.filename; + os << R"(,"lineStart":")" << _location.begin.line; + os << R"(,"lineEnd":")" << _location.end.line; + os << R"(,"columnStart":")" << _location.begin.column; + os << R"(,"columnEnd":")" << _location.end.column; + finish(os); } - friend std::ostream &operator<<(std::ostream &os, const base_parser_error &el) { - el.print(os); - return os; + protected: + [[nodiscard]] std::string type() const override { + return "parser_error"; } }; - struct file_not_found_error : public base_parser_error { - using base_parser_error::base_parser_error; - - std::string prefix() const override { - return "file not found error"; - } - }; struct syntax_error : public base_parser_error { using base_parser_error::base_parser_error; - - std::string prefix() const override { - return "syntax error"; + protected: + [[nodiscard]] std::string type() const override { + return "syntax_error"; } }; struct type_error : public base_parser_error { using base_parser_error::base_parser_error; - - std::string prefix() const override { - return "type error"; + protected: + [[nodiscard]] std::string type() const override { + return "type_error"; } }; - struct undeclared_error : public base_parser_error { - - undeclared_error(const location &l, const std::string &name, const std::string &m) - : base_parser_error("variable " + name + " " + m) { - } - - std::string prefix() const override { - return "undeclared error"; + struct no_match_error : public base_parser_error { + using base_parser_error::base_parser_error; + protected: + [[nodiscard]] std::string type() const override { + return "no_match_error"; } }; - struct redeclare_error : public base_parser_error { - - redeclare_error(const location &l, - const std::string &name, - const std::string &message, - const location &ol) - : base_parser_error("redeclaration of " + name + " " + message), _other_location(ol) { - }; - - std::string prefix() const override { - return "redeclare error"; - } - - location _other_location; - }; } #endif //PROJECT_ERRORS_H diff --git a/src/aalwines/utils/errors.h b/src/aalwines/utils/errors.h index 7053831..74dbb6d 100644 --- a/src/aalwines/utils/errors.h +++ b/src/aalwines/utils/errors.h @@ -26,29 +26,85 @@ #ifndef ERRORS_H #define ERRORS_H + #include #include #include +#include struct base_error : public std::exception { std::string _message; explicit base_error(std::string m) - : _message(std::move(m)) { + : _message(std::move(m)) { } const char *what() const noexcept override { return _message.c_str(); } - virtual void print(std::ostream &os) const { - os << what() << std::endl; + virtual void print_json(std::ostream &os) const { + start(os); + finish(os); } + friend std::ostream &operator<<(std::ostream &os, const base_error &el) { - el.print(os); + el.print_json(os); return os; } +protected: + void start(std::ostream& os) const + { + os << R"({"type":")" << type() << R"(","message":")" << what() << '"'; + } + + void finish(std::ostream& os) const + { + os << "}"; + } + + [[nodiscard]] virtual std::string type() const + { + return "base"; + } +}; + +struct file_not_found_error : public base_error { + std::string _path; + + file_not_found_error(std::string message, std::string path) + : base_error(std::move(message)), _path(std::move(path)) { + } + + void print_json(std::ostream &os) const override { + start(os); + os << R"(", "path":")" + _path << "\""; + finish(os); + } + + [[nodiscard]] std::string type() const override + { + return "file_not_found"; + } +}; + +struct illegal_option_error : public base_error { + std::string _option; + std::string _value; + + illegal_option_error(std::string message, std::string option, std::string value) + : base_error(std::move(message)), _option(std::move(option)), _value(std::move(value)) { + } + + void print_json(std::ostream &os) const override { + os << R"(", "option":")" + _option + R"(","value":")" + _value + "\""; + } + + [[nodiscard]] std::string type() const override + { + return "illegal_option_error"; + } }; #endif /* ERRORS_H */ diff --git a/src/main.cpp b/src/main.cpp index 9b46fcc..6640d28 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -106,7 +106,7 @@ bool do_verification(stopwatch& compilation_time, stopwatch& reduction_time, sto break; } default: - throw base_error("Unsupported --engine value given"); + throw illegal_option_error("Unsupported value", "--engine", std::to_string(engine)); } return engine_outcome; } @@ -120,326 +120,278 @@ bool do_verification(stopwatch& compilation_time, stopwatch& reduction_time, sto */ int main(int argc, const char** argv) { - po::options_description opts; - opts.add_options() - ("help,h", "produce help message"); - - po::options_description output("Output Options"); - po::options_description input("Input Options"); - po::options_description verification("Verification Options"); - - bool print_dot = false; - bool print_net = false; - bool no_parser_warnings = false; - bool silent = false; - bool dump_to_moped = false; - bool no_timing = false; - std::string topology_destination; - std::string routing_destination; - - output.add_options() - ("dot", po::bool_switch(&print_dot), "A dot output will be printed to cout when set.") - ("net", po::bool_switch(&print_net), "A json output of the network will be printed to cout when set.") - ("disable-parser-warnings,W", po::bool_switch(&no_parser_warnings), "Disable warnings from parser.") - ("silent,s", po::bool_switch(&silent), "Disables non-essential output (implies -W).") - ("no-timing", po::bool_switch(&no_timing), "Disables timing output") - ("dump-for-moped", po::bool_switch(&dump_to_moped), "Dump the constructed PDA in a MOPED format (expects a singleton query-file).") - ("write-topology", po::value(&topology_destination), "Write the topology in the P-Rex format to the given file.") - ("write-routing", po::value(&routing_destination), "Write the Routing in the P-Rex format to the given file.") - ; - - - std::string junos_config, prex_topo, prex_routing; - bool skip_pfe = false; - input.add_options() - ("juniper", po::value(&junos_config), - "A file containing a network-description; each line is a router in the format \"name,alias1,alias2:adjacency.xml,mpls.xml,pfe.xml\". ") - ("topology", po::value(&prex_topo), - "An xml-file defining the topology in the P-Rex format") - ("routing", po::value(&prex_routing), - "An xml-file defining the routing in the P-Rex format") - ("skip-pfe", po::bool_switch(&skip_pfe), - "Skip \"indirect\" cases of juniper-routing as package-drops (compatability with P-Rex semantics).") - ; - - std::string query_file; - std::string weight_file; - unsigned int link_failures = 0; - size_t tos = 0; - size_t engine = 0; - bool get_trace = false; - bool no_ip_swap = false; - verification.add_options() - ("query,q", po::value(&query_file), - "A file containing valid queries over the input network.") - ("trace,t", po::bool_switch(&get_trace), "Get a trace when possible") - ("no-ip-route", po::bool_switch(&no_ip_swap), "Disable encoding of routing via IP") - ("link,l", po::value(&link_failures), "Number of link-failures to model.") - ("tos-reduction,r", po::value(&tos), "0=none,1=simple,2=dual-stack,3=dual-stack+backup") - ("engine,e", po::value(&engine), "0=no verification,1=moped,2=post*,3=pre*") - ("weight,w", po::value(&weight_file), "A file containing the weight function expression") - ; - - opts.add(input); - opts.add(output); - opts.add(verification); - - po::variables_map vm; - po::store(po::parse_command_line(argc, argv, opts), vm); - po::notify(vm); - - if (vm.count("help")) { - std::cout << opts << "\n"; - return 1; - } - - if(tos > 3) - { - std::cerr << "Unknown value for --tos-reduction : " << tos << std::endl; - exit(-1); - } - - if(engine > 3) - { - std::cerr << "Unknown value for --engine : " << engine << std::endl; - exit(-1); - } + std::stringstream outstream; + try { + po::options_description opts; + opts.add_options() + ("help,h", "produce help message"); - if(engine != 0 && dump_to_moped) - { - std::cerr << "Cannot both verify (--engine > 0) and dump model (--dump-for-moped) to stdout" << std::endl; - exit(-1); - } + po::options_description output("Output Options"); + po::options_description input("Input Options"); + po::options_description verification("Verification Options"); - if(!junos_config.empty() && (!prex_routing.empty() || !prex_topo.empty())) - { - std::cerr << "--junos cannot be used with --topology or --routing." << std::endl; - exit(-1); - } - - if(prex_routing.empty() != prex_topo.empty()) - { - std::cerr << "Both --topology and --routing have to be non-empty." << std::endl; - exit(-1); - } - - if(junos_config.empty() && prex_routing.empty() && prex_topo.empty()) - { - std::cerr << "Either a Junos configuration or a P-Rex configuration must be given." << std::endl; - exit(-1); - } - - if(skip_pfe && junos_config.empty()) - { - std::cerr << "--skip-pfe is only avaliable for --junos configurations." << std::endl; - exit(-1); - } - - if(silent) no_parser_warnings = true; - - std::stringstream dummy; - std::ostream& warnings = no_parser_warnings ? dummy : std::cerr; - - stopwatch parsingwatch; - auto network = junos_config.empty() ? - PRexBuilder::parse(prex_topo, prex_routing, warnings) : - JuniperBuilder::parse(junos_config, warnings, skip_pfe); - parsingwatch.stop(); - - if (print_dot) { - network.print_dot(std::cout); - } - - if(!topology_destination.empty()) - { - std::ofstream out(topology_destination); - if(out.is_open()) - network.write_prex_topology(out); - else - { - std::cerr << "Could not open --write-topology\"" << topology_destination << "\" for writing" << std::endl, - exit(-1); + bool print_dot = false; + bool print_net = false; + bool no_parser_warnings = false; + bool silent = false; + bool dump_to_moped = false; + bool no_timing = false; + std::string topology_destination; + std::string routing_destination; + + output.add_options() + ("dot", po::bool_switch(&print_dot), "A dot output will be printed to cout when set.") + ("net", po::bool_switch(&print_net), "A json output of the network will be printed to cout when set.") + ("disable-parser-warnings,W", po::bool_switch(&no_parser_warnings), "Disable warnings from parser.") + ("silent,s", po::bool_switch(&silent), "Disables non-essential output (implies -W).") + ("no-timing", po::bool_switch(&no_timing), "Disables timing output") + ("dump-for-moped", po::bool_switch(&dump_to_moped), + "Dump the constructed PDA in a MOPED format (expects a singleton query-file).") + ("write-topology", po::value(&topology_destination), + "Write the topology in the P-Rex format to the given file.") + ("write-routing", po::value(&routing_destination), + "Write the Routing in the P-Rex format to the given file."); + + + std::string junos_config, prex_topo, prex_routing; + bool skip_pfe = false; + input.add_options() + ("juniper", po::value(&junos_config), + "A file containing a network-description; each line is a router in the format \"name,alias1,alias2:adjacency.xml,mpls.xml,pfe.xml\". ") + ("topology", po::value(&prex_topo), + "An xml-file defining the topology in the P-Rex format") + ("routing", po::value(&prex_routing), + "An xml-file defining the routing in the P-Rex format") + ("skip-pfe", po::bool_switch(&skip_pfe), + "Skip \"indirect\" cases of juniper-routing as package-drops (compatability with P-Rex semantics)."); + + std::string query_file; + std::string weight_file; + unsigned int link_failures = 0; + size_t tos = 0; + size_t engine = 0; + bool get_trace = false; + bool no_ip_swap = false; + verification.add_options() + ("query,q", po::value(&query_file), + "A file containing valid queries over the input network.") + ("trace,t", po::bool_switch(&get_trace), "Get a trace when possible") + ("no-ip-route", po::bool_switch(&no_ip_swap), "Disable encoding of routing via IP") + ("link,l", po::value(&link_failures), "Number of link-failures to model.") + ("tos-reduction,r", po::value(&tos), "0=none,1=simple,2=dual-stack,3=dual-stack+backup") + ("engine,e", po::value(&engine), "0=no verification,1=moped,2=post*,3=pre*") + ("weight,w", po::value(&weight_file), "A file containing the weight function expression"); + + opts.add(input); + opts.add(output); + opts.add(verification); + + po::variables_map vm; + po::store(po::parse_command_line(argc, argv, opts), vm); + po::notify(vm); + + if (vm.count("help")) { + std::cout << opts << "\n"; + return 1; } - } - if(!routing_destination.empty()) - { - std::ofstream out(routing_destination); - if(out.is_open()) - network.write_prex_routing(out); - else - { - std::cerr << "Could not open --write-routing\"" << topology_destination << "\" for writing" << std::endl, - exit(-1); + + if (tos > 3) + throw illegal_option_error("Unknown value for", "--tos-reduction", std::to_string(tos)); + + if (engine > 3) + throw illegal_option_error("Unknown value for", "--engine", std::to_string(engine)); + + if (engine != 0 && dump_to_moped) + throw base_error("Cannot both verify (--engine > 0) and dump model (--dump-for-moped) to stdout"); + + if (!junos_config.empty() && (!prex_routing.empty() || !prex_topo.empty())) + throw base_error("--junos cannot be used with --topology or --routing."); + + if (prex_routing.empty() != prex_topo.empty()) + throw base_error("Both --topology and --routing have to be non-empty (or both have to be empty)."); + + if (junos_config.empty() && prex_routing.empty() && prex_topo.empty()) + throw base_error("Either a Junos configuration or a P-Rex configuration must be given."); + + if (skip_pfe && junos_config.empty()) + throw base_error("--skip-pfe is only avaliable for --junos configurations."); + + if (silent) no_parser_warnings = true; + + std::stringstream dummy; + std::ostream &warnings = no_parser_warnings ? dummy : std::cerr; + + stopwatch parsingwatch; + auto network = junos_config.empty() ? + PRexBuilder::parse(prex_topo, prex_routing, warnings) : + JuniperBuilder::parse(junos_config, warnings, skip_pfe); + parsingwatch.stop(); + + if (print_dot) { + network.print_dot(outstream); } - } - - if (!dump_to_moped && (print_net || !query_file.empty())) - { - std::cout << "{\n"; - if (print_net) { - network.print_json(std::cout); - if (!query_file.empty()) - { - std::cout << ",\n"; - } + + if (!topology_destination.empty()) { + std::ofstream out(topology_destination); + if (out.is_open()) + network.write_prex_topology(out); + else throw file_not_found_error("Could not open --write-topology", topology_destination); } - } + if (!routing_destination.empty()) { + std::ofstream out(routing_destination); + if (out.is_open()) + network.write_prex_routing(out); + else throw file_not_found_error("Could not open --write-routing", topology_destination); - if(!query_file.empty()) - { - stopwatch queryparsingwatch; - Builder builder(network); - { - std::ifstream qstream(query_file); - if (!qstream.is_open()) { - std::cerr << "Could not open Query-file\"" << query_file << "\"" << std::endl; - exit(-1); + } + + if (!dump_to_moped && (print_net || !query_file.empty())) { + outstream << "{\n"; + if (print_net) { + network.print_json(outstream); + if (!query_file.empty()) { + outstream << ",\n"; + } } - try { + } + + if (!query_file.empty()) { + stopwatch queryparsingwatch; + Builder builder(network); + { + std::ifstream qstream(query_file); + if (!qstream.is_open()) + throw file_not_found_error("Could not open --query", query_file); + builder.do_parse(qstream); qstream.close(); - } - catch(base_parser_error& error) - { - std::cerr << "Error during parsing:\n" << error << std::endl; - exit(-1); } - } - queryparsingwatch.stop(); + queryparsingwatch.stop(); - std::optional weight_fn; - if (!weight_file.empty()) { - if (engine != 2) { - std::cerr << "Shortest trace using weights is only implemented for --engine 2 (post*). Not for --engine " << engine << std::endl; - exit(-1); - } - // TODO: Implement parsing of latency info here. - NetworkWeight network_weight; - { - std::ifstream wstream(weight_file); - if (!wstream.is_open()) { - std::cerr << "Could not open Weight-file\"" << weight_file << "\"" << std::endl; - exit(-1); - } - try { + std::optional weight_fn; + if (!weight_file.empty()) { + if (engine != 2) + throw base_error("Shortest trace using weights is only implemented for --engine 2 (post*). Not for --engine " + std::to_string(engine)); + // TODO: Implement parsing of latency info here. + NetworkWeight network_weight; + { + std::ifstream wstream(weight_file); + if (!wstream.is_open()) + throw file_not_found_error("Could not open --weight", weight_file); weight_fn.emplace(network_weight.parse(wstream)); wstream.close(); - } catch (base_error& error) { - std::cerr << "Error while parsing weight function:" << error << std::endl; - exit(-1); - } catch (nlohmann::detail::parse_error& error) { - std::cerr << "Error while parsing weight function:" << error.what() << std::endl; - exit(-1); } + } else { + weight_fn = std::nullopt; } - } else { - weight_fn = std::nullopt; - } - if(!dump_to_moped) - { - if(!no_timing) - { - std::cout << "\t\"network-parsing-time\":" << (parsingwatch.duration()) - << ", \"query-parsing-time\":" << (queryparsingwatch.duration()) << ",\n"; + if (!dump_to_moped) { + if (!no_timing) { + outstream << "\t\"network-parsing-time\":" << (parsingwatch.duration()) + << ", \"query-parsing-time\":" << (queryparsingwatch.duration()) << ",\n"; + } + outstream << "\t\"answers\":{\n"; } - std::cout << "\t\"answers\":{\n"; - } - Moped moped; - SolverAdapter solver; - size_t query_no = 0; - for(auto& q : builder._result) - { - ++query_no; - stopwatch compilation_time(false); - if(dump_to_moped) - { - compilation_time.start(); - NetworkPDAFactory factory(q, network, no_ip_swap); - auto pda = factory.compile(); - Moped::dump_pda(pda, std::cout); - } - else - { - std::vector modes{q.approximation()}; - bool was_dual = q.approximation() == Query::DUAL; - if(was_dual) - modes = std::vector{Query::OVER, Query::UNDER}; - std::pair reduction; - utils::outcome_t result = utils::MAYBE; - stopwatch reduction_time(false); - stopwatch verification_time(false); - std::vector::tracestate_t > trace; - std::stringstream proof; - bool need_trace = was_dual || get_trace; - for(auto m : modes) { - bool engine_outcome; - if (weight_fn) { - engine_outcome = do_verification(compilation_time, reduction_time, - verification_time,q, m, network, no_ip_swap, reduction, tos, need_trace, engine, - moped, solver,result, trace, proof, weight_fn.value()); + Moped moped; + SolverAdapter solver; + size_t query_no = 0; + for (auto &q : builder._result) { + ++query_no; + stopwatch compilation_time(false); + if (dump_to_moped) { + compilation_time.start(); + NetworkPDAFactory factory(q, network, no_ip_swap); + auto pda = factory.compile(); + Moped::dump_pda(pda, outstream); } else { - engine_outcome = do_verification>(compilation_time, reduction_time, - verification_time,q, m,network, no_ip_swap, reduction, tos, need_trace, engine, - moped, solver,result, trace, proof, [](){}); - } - if(q.number_of_failures() == 0) - result = engine_outcome ? utils::YES : utils::NO; - - if(result == utils::MAYBE && m == Query::OVER && !engine_outcome) - result = utils::NO; - if(result != utils::MAYBE) - break; - /*else - trace.clear();*/ - } + std::vector modes{q.approximation()}; + bool was_dual = q.approximation() == Query::DUAL; + if (was_dual) + modes = std::vector{Query::OVER, Query::UNDER}; + std::pair reduction; + utils::outcome_t result = utils::MAYBE; + stopwatch reduction_time(false); + stopwatch verification_time(false); + std::vector::tracestate_t> trace; + std::stringstream proof; + bool need_trace = was_dual || get_trace; + for (auto m : modes) { + bool engine_outcome; + if (weight_fn) { + engine_outcome = do_verification(compilation_time, reduction_time, + verification_time, q, m, network, no_ip_swap, reduction, + tos, need_trace, engine, + moped, solver, result, trace, proof, weight_fn.value()); + } else { + engine_outcome = do_verification>(compilation_time, + reduction_time, + verification_time, q, m, + network, no_ip_swap, reduction, + tos, need_trace, engine, + moped, solver, result, trace, + proof, []() {}); + } + if (q.number_of_failures() == 0) + result = engine_outcome ? utils::YES : utils::NO; - // move this into function that generalizes - // and extracts trace at the same time. + if (result == utils::MAYBE && m == Query::OVER && !engine_outcome) + result = utils::NO; + if (result != utils::MAYBE) + break; + /*else + trace.clear();*/ + } - std::cout << "\t\"Q" << query_no << "\" : {\n\t\t\"result\":"; - switch(result) - { - case utils::MAYBE: - std::cout << "null"; - break; - case utils::NO: - std::cout << "false"; - break; - case utils::YES: - std::cout << "true"; - break; - } - std::cout << ",\n"; - std::cout << "\t\t\"reduction\":[" << reduction.first << ", " << reduction.second << "]"; - if(get_trace && result == utils::YES) - { - std::cout << ",\n\t\t\"trace\":[\n"; - std::cout << proof.str(); - std::cout << "\n\t\t]"; - } - if(!no_timing) - { - std::cout << ",\n\t\t\"compilation-time\":" << (compilation_time.duration()) - << ",\n\t\t\"reduction-time\":" << (reduction_time.duration()) - << ",\n\t\t\"verification-time\":" << (verification_time.duration()); + // move this into function that generalizes + // and extracts trace at the same time. + + outstream << "\t\"Q" << query_no << "\" : {\n\t\t\"result\":"; + switch (result) { + case utils::MAYBE: + outstream << "null"; + break; + case utils::NO: + outstream << "false"; + break; + case utils::YES: + outstream << "true"; + break; + } + outstream << ",\n"; + outstream << "\t\t\"reduction\":[" << reduction.first << ", " << reduction.second << "]"; + if (get_trace && result == utils::YES) { + outstream << ",\n\t\t\"trace\":[\n"; + outstream << proof.str(); + outstream << "\n\t\t]"; + } + if (!no_timing) { + outstream << ",\n\t\t\"compilation-time\":" << (compilation_time.duration()) + << ",\n\t\t\"reduction-time\":" << (reduction_time.duration()) + << ",\n\t\t\"verification-time\":" << (verification_time.duration()); + } + outstream << "\n\t}"; + if (query_no != builder._result.size()) + outstream << ","; + outstream << "\n"; + } } - std::cout << "\n\t}"; - if(query_no != builder._result.size()) - std::cout << ","; - std::cout << "\n"; + + if (!dump_to_moped) { + outstream << "\n}"; } } - - if(!dump_to_moped) - { - std::cout << "\n}"; + if (!dump_to_moped && (print_net || !query_file.empty())) { + outstream << "\n}\n"; } } - if (!dump_to_moped && (print_net || !query_file.empty())) + catch(base_error& error) { - std::cout << "\n}\n"; + std::cout << "{\"error\":\n"; + error.print_json(std::cout); + std::cout << "\n}" << std::endl; + return -1; } + std::cout << outstream.str() << std::endl; return 0; }