Skip to content

Commit ca22ff8

Browse files
alan23273850alan23273850
committed
1. no need to distinguish concrete/symbolic.
2. refine error handling when some variable or predicate is not defined.
1 parent db8d5c0 commit ca22ff8

File tree

3 files changed

+185
-90
lines changed

3 files changed

+185
-90
lines changed

‎cli/autoq.cc

+50-58
Original file line numberDiff line numberDiff line change
@@ -153,36 +153,20 @@ try {
153153
CLI::App app{"AutoQ: An automata-based C++ tool for quantum program verification."};
154154
std::string pre, circuit, post, circuit1, circuit2;
155155

156-
CLI::App* executionC = app.add_subcommand("exC", "Concrete Execution");
157-
executionC->add_option("pre.{hsl|spec}", pre, "the precondition file")->required()->type_name("");
158-
executionC->add_option("circuit.qasm", circuit, "the OpenQASM 3.0 circuit file")->required()->type_name("");
159-
executionC->callback([&]() {
156+
CLI::App* execution = app.add_subcommand("ex", "Execution");
157+
execution->add_option("pre.{hsl|spec}", pre, "the precondition file")->required()->type_name("");
158+
execution->add_option("circuit.qasm", circuit, "the OpenQASM 2.0 circuit file")->required()->type_name("");
159+
execution->callback([&]() {
160160
adjust_N_in_nTuple(circuit);
161161
});
162162

163163
bool latex = false;
164-
CLI::App* verificationC = app.add_subcommand("verC", "Concrete Verification");
165-
verificationC->add_option("pre.{hsl|spec}", pre, "the precondition file")->required()->type_name("");
166-
verificationC->add_option("circuit.qasm", circuit, "the OpenQASM 3.0 circuit file")->required()->type_name("");
167-
verificationC->add_option("post.{hsl|spec}", post, "the postcondition file")->required()->type_name("");
168-
verificationC->add_flag("-l,--latex", latex, "Print the statistics for tables in LaTeX");
169-
verificationC->callback([&]() {
170-
adjust_N_in_nTuple(circuit);
171-
});
172-
173-
CLI::App* executionS = app.add_subcommand("exS", "Symbolic Execution");
174-
executionS->add_option("pre.{hsl|spec}", pre, "the precondition file")->required()->type_name("");
175-
executionS->add_option("circuit.qasm", circuit, "the OpenQASM 3.0 circuit file")->required()->type_name("");
176-
executionS->callback([&]() {
177-
adjust_N_in_nTuple(circuit);
178-
});
179-
180-
CLI::App* verificationS = app.add_subcommand("verS", "Symbolic Verification");
181-
verificationS->add_option("pre.{hsl|spec}", pre, "the precondition file")->required()->type_name("");
182-
verificationS->add_option("circuit.qasm", circuit, "the OpenQASM 3.0 circuit file")->required()->type_name("");
183-
verificationS->add_option("post.{hsl|spec}", post, "the postcondition file")->required()->type_name("");
184-
verificationS->add_flag("-l,--latex", latex, "Print the statistics for tables in LaTeX");
185-
verificationS->callback([&]() {
164+
CLI::App* verification = app.add_subcommand("ver", "Verification");
165+
verification->add_option("pre.{hsl|spec}", pre, "the precondition file")->required()->type_name("");
166+
verification->add_option("circuit.qasm", circuit, "the OpenQASM 2.0 circuit file")->required()->type_name("");
167+
verification->add_option("post.{hsl|spec}", post, "the postcondition file")->required()->type_name("");
168+
verification->add_flag("-l,--latex", latex, "Print the statistics for tables in LaTeX");
169+
verification->callback([&]() {
186170
adjust_N_in_nTuple(circuit);
187171
});
188172

@@ -209,41 +193,49 @@ try {
209193

210194
auto start = chrono::steady_clock::now();
211195
// bool runConcrete; // or runSymbolic
212-
if (executionC->parsed()) {
213-
// runConcrete = true;
214-
AUTOQ::TreeAutomata aut = AUTOQ::Parsing::TimbukParser<AUTOQ::Symbol::Concrete>::ReadAutomaton(pre);
215-
aut.execute(circuit);
216-
aut.print_aut();
217-
} else if (verificationC->parsed()) {
196+
if (execution->parsed()) {
218197
// runConcrete = true;
219-
auto aut = AUTOQ::Parsing::TimbukParser<AUTOQ::Symbol::Concrete>::ReadAutomaton(pre);
220-
auto aut2 = AUTOQ::Parsing::TimbukParser<AUTOQ::Symbol::Concrete>::ReadAutomaton(post);
221-
aut.execute(circuit);
222-
bool verify = aut <= aut2;
223-
if (latex) {
224-
aut.print_stats();
225-
} else {
226-
std::cout << "The quantum program has [" << aut.qubitNum << "] qubits and [" << AUTOQ::TreeAutomata::gateCount << "] gates.\nThe verification process [" << (verify ? "passed" : "failed") << "] in [" << AUTOQ::Util::Convert::toString(chrono::steady_clock::now() - start) << "] with [" << AUTOQ::Util::getPeakRSS() / 1024 / 1024 << "MB] memory usage.\n";
198+
auto aut1 = ReadAutomaton(pre);
199+
try {
200+
auto &aut = std::get<AUTOQ::TreeAutomata>(aut1);
201+
aut.execute(circuit);
202+
aut.print_aut();
203+
} catch (const std::bad_variant_access&) {
204+
auto &aut = std::get<AUTOQ::SymbolicAutomata>(aut1);
205+
aut.execute(circuit);
206+
aut.print_aut();
227207
}
228-
} else if (executionS->parsed()) {
229-
// runConcrete = false;
230-
AUTOQ::SymbolicAutomata aut = AUTOQ::Parsing::TimbukParser<AUTOQ::Symbol::Symbolic>::ReadAutomaton(pre);
231-
aut.execute(circuit);
232-
aut.print_aut();
233-
} else if (verificationS->parsed()) {
208+
} else if (verification->parsed()) {
234209
// runConcrete = false;
235-
AUTOQ::SymbolicAutomata aut = AUTOQ::Parsing::TimbukParser<AUTOQ::Symbol::Symbolic>::ReadAutomaton(pre);
236-
AUTOQ::PredicateAutomata spec = AUTOQ::Parsing::TimbukParser<AUTOQ::Symbol::Predicate>::ReadAutomaton(post);
237-
aut.execute(circuit);
238-
// std::cout << "OUTPUT AUTOMATON:\n";
239-
// std::cout << "=================\n";
240-
// aut.print_aut();
241-
// std::cout << "=================\n";
242-
bool verify = aut <= spec;
243-
if (latex) {
244-
aut.print_stats();
245-
} else {
246-
std::cout << "The quantum program has [" << aut.qubitNum << "] qubits and [" << AUTOQ::SymbolicAutomata::gateCount << "] gates.\nThe verification process [" << (verify ? "passed" : "failed") << "] in [" << AUTOQ::Util::Convert::toString(chrono::steady_clock::now() - start) << "] with [" << AUTOQ::Util::getPeakRSS() / 1024 / 1024 << "MB] memory usage.\n";
210+
auto spec1 = ReadAutomaton(post);
211+
try {
212+
auto &spec = std::get<AUTOQ::PredicateAutomata>(spec1);
213+
auto aut = AUTOQ::Parsing::TimbukParser<AUTOQ::Symbol::Symbolic>::ReadAutomaton(pre);
214+
aut.execute(circuit);
215+
// std::cout << "OUTPUT AUTOMATON:\n";
216+
// std::cout << "=================\n";
217+
// aut.print_aut();
218+
// std::cout << "=================\n";
219+
bool verify = aut <= spec;
220+
if (latex) {
221+
aut.print_stats();
222+
} else {
223+
std::cout << "The quantum program has [" << aut.qubitNum << "] qubits and [" << AUTOQ::SymbolicAutomata::gateCount << "] gates.\nThe verification process [" << (verify ? "passed" : "failed") << "] in [" << AUTOQ::Util::Convert::toString(chrono::steady_clock::now() - start) << "] with [" << AUTOQ::Util::getPeakRSS() / 1024 / 1024 << "MB] memory usage.\n";
224+
}
225+
} catch (const std::bad_variant_access&) {
226+
auto &spec = std::get<AUTOQ::TreeAutomata>(spec1);
227+
auto aut = AUTOQ::Parsing::TimbukParser<AUTOQ::Symbol::Concrete>::ReadAutomaton(pre);
228+
aut.execute(circuit);
229+
// std::cout << "OUTPUT AUTOMATON:\n";
230+
// std::cout << "=================\n";
231+
// aut.print_aut();
232+
// std::cout << "=================\n";
233+
bool verify = aut <= spec;
234+
if (latex) {
235+
aut.print_stats();
236+
} else {
237+
std::cout << "The quantum program has [" << aut.qubitNum << "] qubits and [" << AUTOQ::TreeAutomata::gateCount << "] gates.\nThe verification process [" << (verify ? "passed" : "failed") << "] in [" << AUTOQ::Util::Convert::toString(chrono::steady_clock::now() - start) << "] with [" << AUTOQ::Util::getPeakRSS() / 1024 / 1024 << "MB] memory usage.\n";
238+
}
247239
}
248240
} else if (equivalence_checking->parsed()) {
249241
// runConcrete = true;

‎include/autoq/parsing/timbuk_parser.hh

+5-1
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@
1414
// AUTOQ headers
1515
#include "autoq/aut_description.hh"
1616
#include "autoq/complex/complex.hh"
17+
#include <variant>
1718

1819
namespace AUTOQ
1920
{
@@ -35,7 +36,10 @@ struct AUTOQ::Parsing::TimbukParser
3536
{
3637
// static AUTOQ::Automata<Symbol> ParseString(std::string fileContents);
3738
static AUTOQ::Automata<Symbol> ReadAutomaton(const std::string& filepath);
38-
static AUTOQ::Automata<Symbol> parse_hsl_from_istream(std::istream *is, const std::map<std::string, AUTOQ::Complex::Complex> &constants = {}, const std::map<std::string, std::string> &predicates = {});
39+
static AUTOQ::Automata<Symbol> ReadAutomaton(const std::string& filepath, bool &do_not_throw_term_undefined_error);
40+
static AUTOQ::Automata<Symbol> parse_hsl_from_istream(std::istream *is, bool &do_not_throw_term_undefined_error, const std::map<std::string, AUTOQ::Complex::Complex> &constants = {}, const std::map<std::string, std::string> &predicates = {});
3941
};
4042

43+
std::variant<AUTOQ::Automata<AUTOQ::Symbol::Concrete>, AUTOQ::Automata<AUTOQ::Symbol::Symbolic>, AUTOQ::Automata<AUTOQ::Symbol::Predicate>> ReadAutomaton(const std::string& filepath);
44+
4145
#endif

0 commit comments

Comments
 (0)