diff --git a/3rdparty/solvers/MiniSat.14_linux b/3rdparty/solvers/MiniSat.14_linux new file mode 100755 index 000000000..a62456a48 Binary files /dev/null and b/3rdparty/solvers/MiniSat.14_linux differ diff --git a/3rdparty/solvers/caqe b/3rdparty/solvers/caqe new file mode 100755 index 000000000..d0dcc086e Binary files /dev/null and b/3rdparty/solvers/caqe differ diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh index d9fb15e7b..374a20fdb 100644 --- a/include/mata/nfa/nfa.hh +++ b/include/mata/nfa/nfa.hh @@ -19,6 +19,7 @@ #include #include #include +#include #include "mata/alphabet.hh" #include "mata/parser/parser.hh" @@ -530,20 +531,54 @@ Nfa minimize(const Nfa &aut, const ParameterMap& params = {{ "algorithm", "brzoz */ Nfa determinize(const Nfa& aut, std::unordered_map *subset_map = nullptr); +/** + * @brief A CNF transformation to the provided clause in form of disjunctions of long and-not clauses, + * utilized for reduction using SAT and QBF solvers, printed to output + * @param[in] input Vector with the clause in DNF form to transform + * @param[in] max_index Starting index of free variables used for new generated variables + * @param[in] output Output stream + * @return The first variable index that was not utilized +*/ +size_t reduction_tseytin(const std::vector & input, size_t max_index, std::ostream& output); + +/** + * @brief Experimental reduction using sat solver MiniSat with idea of creating minimal nondeterministic automaton, + * is not possible to use for normal sized automata (around 10 states max), requires the alphabet of input automaton + * to be a continuous sequence of numbers strating from 0 + * @param[in] aut Automaton to reduce + * @param[in] params Optional pamaters to control the reduction: + * - "solver": "sat"/"sat_nfa" (sat for the dfa complete automaton with single initial state) + * @param[in] debug Flag for debug output as the reduction can take some time to get the info about the current status + * @return Reduced automaton +*/ +Nfa reduce_sat(const Nfa &aut, const ParameterMap& params = {{"solver", "sat"}}, bool debug = false); + +/** + * @brief Experimental reduction using qbf solver CAQE with idea of creating minimal nondeterministic automaton, + * is not possible to use for normal sized automata (around 10 states max), requires the alphabet of input automaton + * to be a continuous sequence of numbers strating from 0 + * @param[in] aut Automaton to reduce + * @param[in] debug Flag for debug output as the reduction can take some time to get the info about the current status + * @return Reduced automaton +*/ +Nfa reduce_qbf(const Nfa &aut, bool debug = false); + /** * @brief Reduce the size of the automaton. * * @param[in] aut Automaton to reduce. * @param[out] state_renaming Mapping of original states to reduced states. * @param[in] params Optional parameters to control the reduction algorithm: - * - "algorithm": "simulation", "residual", - * and options to parametrize residual reduction, not utilized in simulation + * - "algorithm": "simulation", "residual", "solvers", + * options to parametrize residual reduction, not utilized in other reductions * - "type": "after", "with", - * - "direction": "forward", "backward". + * - "direction": "forward", "backward", + * options to parametrize reduction using solvers, not utilized in other reductions + * - "solver": "sat"/"sat_nfa"/"qbf". * @return Reduced automaton. */ Nfa reduce(const Nfa &aut, StateRenaming *state_renaming = nullptr, - const ParameterMap& params = {{ "algorithm", "simulation" }, { "type", "after" }, { "direction", "forward" } }); + const ParameterMap& params = {{ "algorithm", "simulation" }, { "type", "after" }, { "direction", "forward" }, {"solver", "nfa"} }); /** * @brief Checks inclusion of languages of two NFAs: @p smaller and @p bigger (smaller <= bigger). @@ -574,6 +609,8 @@ inline bool is_included(const Nfa& smaller, const Nfa& bigger, const Alphabet* c return is_included(smaller, bigger, nullptr, alphabet, params); } +// static default value for empty run pair +static std::pair default_runs(nullptr, nullptr); /** * @brief Perform equivalence check of two NFAs: @p lhs and @p rhs. * @@ -582,10 +619,13 @@ inline bool is_included(const Nfa& smaller, const Nfa& bigger, const Alphabet* c * @param[in] alphabet Alphabet of both NFAs to compute with. * @param[in] params[ Optional parameters to control the equivalence check algorithm: * - "algorithm": "naive", "antichains" (Default: "antichains") + * @param[out] default_runs Optional parameter for intersection runs to return the found word + * that differs the input automata, used for solver reduction * @return True if @p lhs and @p rhs are equivalent, false otherwise. */ bool are_equivalent(const Nfa& lhs, const Nfa& rhs, const Alphabet* alphabet, - const ParameterMap& params = {{ "algorithm", "antichains"}}); + const ParameterMap& params = {{ "algorithm", "antichains"}}, + std::pair& runs = default_runs); /** * @brief Perform equivalence check of two NFAs: @p lhs and @p rhs. @@ -602,9 +642,12 @@ bool are_equivalent(const Nfa& lhs, const Nfa& rhs, const Alphabet* alphabet, * @param[in] rhs Second automaton to concatenate. * @param[in] params Optional parameters to control the equivalence check algorithm: * - "algorithm": "naive", "antichains" (Default: "antichains") + * * @param[out] default_runs Optional parameter for intersection runs to return the found word + * that differs the input automata, used for solver reduction * @return True if @p lhs and @p rhs are equivalent, false otherwise. */ -bool are_equivalent(const Nfa& lhs, const Nfa& rhs, const ParameterMap& params = {{ "algorithm", "antichains"}}); +bool are_equivalent(const Nfa& lhs, const Nfa& rhs, const ParameterMap& params = {{ "algorithm", "antichains"}}, + std::pair& runs = default_runs); // Reverting the automaton by one of the three functions below, // currently simple_revert seems best (however, not tested enough). diff --git a/include/mata/nfa/types.hh b/include/mata/nfa/types.hh index 40a016d7f..f573fc45f 100644 --- a/include/mata/nfa/types.hh +++ b/include/mata/nfa/types.hh @@ -7,6 +7,8 @@ #include "mata/parser/parser.hh" #include +#include +#include namespace mata::nfa { @@ -48,6 +50,315 @@ struct Nfa; ///< A non-deterministic finite automaton. /// An epsilon symbol which is now defined as the maximal value of data type used for symbols. constexpr Symbol EPSILON = Limits::max_symbol; +// defining indexes of logic operators used in an input vector for tseytin transformation +#define TSEY_AND -1 +#define TSEY_OR -2 +#define TSEY_NOT -3 + +// define charactes used for SAT and QBF solvers +#define SOL_EOL std::string("0\n") +#define SOL_NEG std::string("-") +#define SOL_DELIM std::string(" ") +#define SOL_HEADER std::string("p cnf ") +#define SOL_FORALL std::string("a") +#define SOL_EXISTS std::string("e") + +/** + * Base class for representing the input parameters for SAT and QBF reduction + */ +struct AutStats { +public: + /** holds the number of states of the created automaton*/ + size_t state_num; + /** holds the number of symbols of the created automaton*/ + size_t alpha_num; + + /** sets of example words defining the automaton's language*/ + std::set accept; + std::set reject; + + /** output stream*/ + std::ostream& output; + +public: + + /** Constructor for AutStats */ + AutStats(size_t states, size_t alphabet, std::ostream& out, std::set acc = {}, std::set rej = {}) + : state_num(states), alpha_num(alphabet), accept(acc), reject(rej), output(out) {} + + /** + * Debug function printing the members of the class to the output + */ + void print(std::ostream &output){ + output << "States = " << this->state_num << ", Symbols = " << this->alpha_num << std::endl; + output << "Accept:"; + for (const auto& word: this->accept){ + for (size_t i = 0; i < word.size(); i++){ + output << " " << word[i]; + } + output << ","; + } + + output << std::endl << "Reject:"; + for (const auto& word: this->reject){ + for (size_t i = 0; i < word.size(); i++){ + output << " " << word[i]; + } + output << ","; + } + output << std::endl << "---------------------------"<< std::endl; + } + + /*** + * @brief Create the instance of Nfa from the result of the solver reduction from the given input, depends on the solver + * @param solver_result Input stream of the solver result + * @param params Selected solver reduction + * @return Nfa instance corresponding to the solver generated automaton + */ + Nfa build_result(std::istream& solver_result, const ParameterMap& params); +}; + +/** + * Class for input parameters for SAT reduction, inherits from AutStats + * Variables indexed by rows for N=3 S=2: + * 1 - T1a1 2 - T1a2 3 - T1a3 4 - T2a1 5 - T2a2 6 - T2a3 + * 7 - T3a1 8 - T3a2 9 - T3a3 10 - T1b1 11 - T1b2 12 - T1b3 + * 13 - T2b1 14 - T2b2 15 - T2b3 16 - T3b1 17 - T3a2 18 - T3b3 + * 19 - F1 20 - F2 21 - F3 + */ +struct SatStats : public AutStats{ +public: + + /** + * @brief Construct a new explicit SatStats from other SatStats. + */ + SatStats(const SatStats& other) = default; + + explicit SatStats(const size_t num_of_states, const size_t size_of_alphabet, std::ostream& out, std::set acc = {}, + std::set rej = {}) : AutStats(num_of_states, size_of_alphabet, out, acc, rej) {} + + /** + * Generates the clauses for determinism of the automaton + * -1 or -2 and -1 or -3 and -2 or -3 + */ + void determine_clauses() const; + + /** + * Generates the clauses for completeness of the automaton + * 1 or 2 or 3 + */ + void complete_clauses() const; + + /** + * @brief Generates the clauses for accepting and rejecting words, calls recurse_tseytin and recurse_tseytin_reject + * @param max_index First free variable that can be used for CNF transformation + * @return New max_index representing the first free variable that is possible to use for CNF transformation + */ + size_t example_clauses(size_t max_index); + + /** + * @brief Recursively generates and stores the clauses for accepting a word in DNF + * @param base Partial vector for storage for the result + * @param state State where the previous transition ended + * @param word Word that is being accepted + * @param pos Current position in the word + * @param [out] result Output vector with the formula for CNF transformation + * @param skip_init Number of variables to skip in case of initial variables for nfa (default is 0) + */ + void recurse_tseytin_accept(const std::vector& base, size_t state, Word word, const unsigned pos, + std::vector& result, size_t skip_init = 0); + + /** + * @brief Recursively generates and prints the clauses on output for rejecting a word + * @param base Partial string for storage fo the output + * @param state State where the previous transition ended + * @param pos Current position in the word + * @param word Word that is being rejected + * @param skip_init Number of variables to skip in case of initial variables for nfa (default is 0) + */ + void recurse_tseytin_reject(const std::string& base, size_t state, Word word, const unsigned pos, size_t skip_init = 0); + + /** + * @brief Generates the clauses for accepting and rejecting words for a nondeterministic automaton, + * possibility of multiple initial states, calls recurse_tseytin and recurse_tseytin_reject + * @param max_index First free variable that can be used for CNF transformation + * @return New max_index representing the first free variable that is possible to use for CNF transformation + */ + size_t example_nfa_clauses(size_t max_index); + +}; // struct SatStats + +/** + * Class for input parameters for QBF reduction, inherits from AutStats + * Variables indexed by rows for N=3 S=2: + * 1 - T1a1 2 - T1a2 3 - T1a3 4 - T2a1 5 - T2a2 6 - T2a3 + * 7 - T3a1 8 - T3a2 9 - T3a3 10 - T1b1 11 - T1b2 12 - T1b3 + * 13 - T2b1 14 - T2b2 15 - T2b3 16 - T3b1 17 - T3a2 18 - T3b3 + * 19 - I1 20 - I2 21 - I3 22 - F1 23 - F2 24 - F3 + */ +struct QbfStats : public AutStats { +public: + /** size of the binary vector representing the state*/ + unsigned state_bin; + + /** + * @brief Construct a new explicit QbfStats from other QbfStats. + */ + QbfStats(const QbfStats& other) = default; + + explicit QbfStats(const size_t num_of_states, const size_t size_of_alphabet, std::ostream& out, std::set acc = {}, + std::set rej = {}) : AutStats(num_of_states, size_of_alphabet, out, acc, rej), + state_bin(static_cast(ceil(log2(static_cast(num_of_states))))){} + + /** + * @brief Recompute the state_bin value from the number of states + */ + void recompute_bin(){ + this->state_bin = static_cast(ceil(log2(static_cast(this->state_num)))); + } + + /** + * @brief Generates and prints clauses for setting the initial and final states for accepting a word + * @param state_base First variable of the first state + * @param end_base First variable of the last state + */ + void init_final_clauses(size_t state_base, size_t end_base); + + /** + * @brief Generates the clauses for initial and final states when accepting a word by iterating through + * the combinations of the binary vector + * @param var_base First quantified variable of binary vector of the initial/final state + * @param result_base Starting initial/final static variables + */ + void init_final(size_t var_base, size_t result_base); + + /** + * @brief Generates and stores the clauses for initial and final states when rejecting a word + * by iterating thought the combinations of the binary vector + * @param var_base First quantified variable of binary vector of the initial/final state + * @param result_base Starting initial/final static variables + * @param [out] result Output vector with the generated clauses + */ + void init_final_reject(size_t var_base, size_t result_base, std::vector& result); + + /*** + * @brief Generates and stores clauses for setting the initial and final state for rejecting the word + * @param state_base First variable of the first state + * @param end_base First variable of the last state + * @param [out] result Vector where the generated clauses are stored for CNF transformation + */ + void init_final_clauses_reject(size_t state_base, size_t end_base, std::vector& result); + + /** + * @brief Prints the clauses for covering the invalid combinations of the binary vector for accepting a word + * that have to be rejected + * @param start First variable of the given state to invalidate + */ + void valid_combinations(size_t start); + + /** + * @brief Stores the clauses for covering the invalid combinations of the binary vector for a rejected word + * that have to be accepted + * @param start First variable of the given state to validate + * @param [out] input Vector where the generated clauses are stored for CNF transformation + */ + void valid_combinations_reject(size_t start, std::vector & input); + + /** + * @brief Generates the transition clauses for accepting a word for a single symbol + * @param var First variable of the given state + * @param trans First transition variable for the required symbol + */ + void accept_clauses(size_t var, size_t curr_trans); + + /** + * @brief Generates and stores the transition clauses for rejecting a word + * @param var First variable of the given state + * @param trans First transition variable for the required symbol + * @param [out] result Vector where the generated clauses are stored for CNF transformation + */ + void reject_clauses(size_t free_var, size_t curr_trans, std::vector & result); + + /*** + * @brief Generates the clauses for example words that should be accepted or rejected by the automaton + * @param max_index Index of the first variable that is free and + * can be used for new variables for CNF transformation (includes the state variables) + */ + void example_clauses(size_t max_index); + + /*** + * @brief Prints the number of variables, clauses and quantified variables for QDIMACS FORMAT + * @return First free index of the variable for CNF transformation (including state variables) + */ + size_t print_qbf_header(){ + size_t states = this->state_num; // number of states + size_t alpha = this->alpha_num; // number of symbols + size_t bin = this->state_bin; // size of binary vector + size_t un_var = states * states * alpha + 2 * states; // number of unquantified variables + size_t acc_var = 0, rej_var = 0, claus = 0, dynamic_tsei_vars = 0; + + for (auto word: this->accept){ + if (word.empty()){ + claus++; // epsilon clause, no vars + continue; + } + acc_var += (word.size() + 1) * bin; // new quant vars for a word, state variables + + claus += 2*states + states*states*word.size(); // init + final + transition clauses + claus += (static_cast(pow(2, static_cast(bin))) - states) * (word.size()+1); // valid clauses + } + + for (auto word: this->reject){ + if (word.empty()){ + claus += states; // epsilon clauses, no vars + continue; + } + rej_var += (word.size() + 1) * bin; // new quant vars for a word, state variables + + // dynamic tseytin clauses + dynamic_tsei_vars += 2*states + states*states*word.size(); // single var for each init, final + dynamic_tsei_vars += (static_cast(pow(2, static_cast(bin))) - states) * (word.size()+1); // trans clauses + + claus += 2 * states * ((bin+1)+1); // init + final clauses + claus += states*states*word.size() * ((2*bin+1)+1); // trans clauses + claus += (static_cast(pow(2, static_cast(bin))) - states) * (word.size()+1) * (bin+1); // valid clauses + claus++; // add tseitsen result clause + } + + claus++; // add the clause for setting 0 as initial state + + // header line with the number fo used variables and clauses + this->output << SOL_HEADER << un_var + acc_var + rej_var + dynamic_tsei_vars << SOL_DELIM << claus << std::endl; + + // print quantified variables + if (rej_var != 0){ + this->output << SOL_FORALL; + this->print_quant_vars(un_var+acc_var+1, rej_var); + this->output << SOL_DELIM << SOL_EOL; + } + + if (acc_var != 0 && dynamic_tsei_vars != 0){ + this->output << SOL_EXISTS; + this->print_quant_vars(un_var+1, acc_var); + this->print_quant_vars(un_var+acc_var+rej_var+1, dynamic_tsei_vars); + this->output << SOL_DELIM << SOL_EOL; + } + + return un_var+acc_var+rej_var+1; + } + + /*** + * @brief Prints quantified variables + * @param from Starting index of the variable + * @param num Number of variables + */ + void print_quant_vars(size_t from, size_t num){ + for (size_t i = 0; i < num; i++){ + this->output << SOL_DELIM << from+i; + } + } +}; // struct QbfStats + } // namespace mata::nfa. #endif //MATA_TYPES_HH diff --git a/src/nfa/inclusion.cc b/src/nfa/inclusion.cc index 96d60ec88..cbe0e8675 100644 --- a/src/nfa/inclusion.cc +++ b/src/nfa/inclusion.cc @@ -224,14 +224,14 @@ bool mata::nfa::algorithms::is_included_antichains( namespace { using AlgoType = decltype(algorithms::is_included_naive)*; - bool compute_equivalence(const Nfa &lhs, const Nfa &rhs, const mata::Alphabet *const alphabet, const AlgoType &algo) { + bool compute_equivalence(const Nfa &lhs, const Nfa &rhs, const mata::Alphabet *const alphabet, const AlgoType &algo, + std::pair& runs = default_runs) { //alphabet should not be needed as input parameter - if (algo(lhs, rhs, alphabet, nullptr)) { - if (algo(rhs, lhs, alphabet, nullptr)) { + if (algo(lhs, rhs, alphabet, runs.first)) { + if (algo(rhs, lhs, alphabet, runs.second)) { return true; } } - return false; } @@ -269,7 +269,8 @@ bool mata::nfa::is_included( return algo(smaller, bigger, alphabet, cex); } // is_included }}} -bool mata::nfa::are_equivalent(const Nfa& lhs, const Nfa& rhs, const Alphabet *alphabet, const ParameterMap& params) +bool mata::nfa::are_equivalent(const Nfa& lhs, const Nfa& rhs, const Alphabet *alphabet, const ParameterMap& params, + std::pair& runs) { //TODO: add comment on what this is doing, what is __func__ ... AlgoType algo{ set_algorithm(std::to_string(__func__), params) }; @@ -277,13 +278,14 @@ bool mata::nfa::are_equivalent(const Nfa& lhs, const Nfa& rhs, const Alphabet *a if (params.at("algorithm") == "naive") { if (alphabet == nullptr) { const auto computed_alphabet{create_alphabet(lhs, rhs) }; - return compute_equivalence(lhs, rhs, &computed_alphabet, algo); + return compute_equivalence(lhs, rhs, &computed_alphabet, algo, runs); } } - return compute_equivalence(lhs, rhs, alphabet, algo); + return compute_equivalence(lhs, rhs, alphabet, algo, runs); } -bool mata::nfa::are_equivalent(const Nfa& lhs, const Nfa& rhs, const ParameterMap& params) { - return are_equivalent(lhs, rhs, nullptr, params); +bool mata::nfa::are_equivalent(const Nfa& lhs, const Nfa& rhs, const ParameterMap& params, + std::pair& runs) { + return are_equivalent(lhs, rhs, nullptr, params, runs); } diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc index ea04a0bfb..04b366c85 100644 --- a/src/nfa/operations.cc +++ b/src/nfa/operations.cc @@ -12,11 +12,13 @@ #include "mata/nfa/nfa.hh" #include "mata/nfa/algorithms.hh" #include "mata/nfa/builder.hh" +#include "mata/nfa/strings.hh" #include using std::tie; using namespace mata::utils; +using namespace mata::strings; using namespace mata::nfa; using mata::Symbol; @@ -1031,6 +1033,20 @@ Nfa mata::nfa::reduce(const Nfa &aut, StateRenaming *state_renaming, const Param const std::string& residual_direction = params.at("direction"); result = reduce_size_by_residual(aut, reduced_state_map, residual_type, residual_direction); + } + else if ("solvers" == algorithm) { // reduction using solvers, does not work with state_renaming + if (!haskey(params, "solver")) { + throw std::runtime_error(std::to_string(__func__) + + " requires setting the \"solver\" key in the \"params\" argument; " + "received: " + std::to_string(params)); + } + const std::string& solver_type = params.at("solver"); + + if (solver_type == "qbf") { + result = reduce_qbf(aut); + } else { + result = reduce_sat(aut, params); + } } else { throw std::runtime_error(std::to_string(__func__) + " received an unknown value of the \"algorithm\" key: " + algorithm); @@ -1208,3 +1224,737 @@ std::set mata::nfa::Nfa::get_words(unsigned max_length) { return result; } + +void work_and_not_chain(std::queue & and_chain, size_t max_index, std::ostream& output) { + std::string save; + bool not_flag = false; + + while (and_chain.empty() == false) { + int elem = and_chain.front(); // get the first element + and_chain.pop(); + + if (elem == TSEY_NOT) { // negate the variable for the output + output << SOL_NEG; + not_flag = true; + } + else if (elem == TSEY_OR) { + throw std::runtime_error("Unexpected format for tseytin."); + } + else if (elem != TSEY_AND) { // variable + output << elem << SOL_DELIM << SOL_NEG << max_index << SOL_DELIM << SOL_EOL; + if (not_flag == false) // save the opposite variable + save += SOL_NEG; + + save += std::to_string(elem) + SOL_DELIM; + not_flag = false; + } + } + + // print the last saved clause + output << save << max_index << SOL_DELIM << SOL_EOL; +} + + +void work_or_chain(const std::vector & or_chain, std::ostream& output) { + // as the output is set to be true, clauses can be optimised + // clauses where output is not negated don't affect the result and can be omitted + // the last clause where output is negated is printed, + // but as the output doesn't affect the clause, it can be left out + + for (auto elem: or_chain) { + output << elem << SOL_DELIM; + } + output << SOL_EOL; +} + +// expects a clause in form of disjunctions of long and-not clauses +size_t mata::nfa::reduction_tseytin(const std::vector & input, size_t max_index, std::ostream& output) { + std::queue part; // and-clause, queue to keep the correct order of the operators + std::vector or_chain; // or-clause + + for (auto index: input) { + if (index != TSEY_OR) { // until or is found save the and-clause + part.push(index); + } else { // resolve the and-clause + work_and_not_chain(part, max_index, output); + part = std::queue (); // clear queue + or_chain.push_back(static_cast (max_index)); // save created variable to or-clause + ++max_index; + } + } + + if (part.empty() == false) { // finish the last clause + work_and_not_chain(part, max_index, output); + or_chain.push_back(static_cast (max_index)); + ++max_index; + } + + work_or_chain(or_chain, output); // resolve or-clause + return max_index; +} + +Nfa mata::nfa::AutStats::build_result(std::istream& solver_result, const ParameterMap& params) { + if (!haskey(params, "solver")) { + throw std::runtime_error(std::to_string(__func__) + + " requires setting the \"solver\" key in the \"params\" argument; " + "received: " + std::to_string(params)); + } + + const std::string& solver_type = params.at("solver"); + if (solver_type != "sat" && solver_type != "sat_nfa" &&solver_type != "qbf") { + throw std::runtime_error(std::to_string(__func__) + + " received an unknown value of the \"solver\" key: " + solver_type); + } + + Nfa result(this->state_num); + mata::utils::SparseSet new_initial = {0}; // always the initial state + mata::utils::SparseSet new_final; + + std::string line; + getline(solver_result, line); // skip first line + if (solver_type == "qbf") + getline(solver_result, line); // skip the second line for qbf + + std::string token; + size_t index = 0; + size_t trans_vars = this->state_num * this->state_num * this->alpha_num; + size_t max_vars = trans_vars + this->state_num; + bool end = false; + + if (solver_type != "sat") { // add initial state variables for nfa + max_vars += this->state_num; + } + + while (getline(solver_result, line)) { + std::stringstream stream(line); + while (std::getline(stream, token, ' ')) { // split line by spaces + if (token.empty() || token == "v" || token == "V" || token == "0") { + continue; + } + else if (token == "c") { // skip comments + break; + } + + try { + index = static_cast(std::abs(std::stoi(token))-1); // try catch + } catch (const std::exception& e) { + throw std::runtime_error(std::to_string(__func__) + " encountered exception: " + e.what()); + } + + if (index >= max_vars) { // no more variables, end + end = true; + break; + } + else if (token[0] == '-') { // ignore false variables + continue; + } + else if (index < trans_vars) { // transition variables + State from = (index % (this->state_num * this->state_num)) / this->state_num; + State to = (index % this->state_num); + Symbol symbol = static_cast(index / (this->state_num * this->state_num)); + result.delta.add(from, symbol, to); + } + else if (solver_type != "sat" && index < trans_vars + this->state_num){ // initial variables + new_initial.insert(index - trans_vars); + } else { // final variables + new_final.insert(index - (max_vars - this->state_num)); + } + } + + if (end) { + break; + } + } + + result.initial = std::move(new_initial); + result.final = std::move(new_final); + return result; +} + +void mata::nfa::SatStats::determine_clauses() const{ + size_t transitions_num = this->alpha_num * this->state_num * this->state_num; + for (size_t index = 1; index <= transitions_num; index += this->state_num) { // every row + for (size_t j = 0; j < this->state_num; ++j) { // elements in row + for (size_t k = j+1; k < this->state_num; ++k) { // combinations + this->output << SOL_NEG << index + j << SOL_DELIM << SOL_NEG << index + k << SOL_DELIM << SOL_EOL; // determinism + } + } + } +} + +void mata::nfa::SatStats::complete_clauses() const{ + size_t transitions_num = this->alpha_num * this->state_num * this->state_num; + for (size_t index = 1; index <= transitions_num; index += this->state_num) { // every row + for (size_t j = 0; j < this->state_num; ++j) { // elements in a row + this->output << index+j << SOL_DELIM; // completeness + } + this->output << SOL_EOL; + } +} + +size_t mata::nfa::SatStats::example_clauses(size_t max_index) { + size_t transitions_num = this->alpha_num * this->state_num * this->state_num; + + for(auto word: this->accept) { + std::vector word_expression; // partial expression + std::vector accept_result; // output for tseytin + + if (word.empty()){ // special case epsilon, set state 1 to be final + this->output << transitions_num + 1 << SOL_DELIM << SOL_EOL; + continue; + } + + unsigned start_index = word.front(); // get symbol + size_t start_row = start_index * this->state_num * this->state_num; + + for (size_t i = 1; i <= this->state_num; ++i) { + word_expression.clear(); + // add transition + word_expression.push_back(static_cast (start_row + i)); + word_expression.push_back(TSEY_AND); + + if (word.size() == 1) { // accepts a single letter, final state + word_expression.push_back(static_cast (transitions_num + i)); + accept_result.insert(accept_result.end(), word_expression.begin(), word_expression.end()); + accept_result.push_back(TSEY_OR); + } else { + this->recurse_tseytin_accept(word_expression, i, word, 1, accept_result); + } + } + + max_index = reduction_tseytin(accept_result, max_index, output); + } + + for (auto word: this->reject) { + if (word.empty()) { // special case epsilon, state 1 cannot be final + this->output << SOL_NEG << transitions_num + 1 << SOL_DELIM << SOL_EOL; + continue; + } + + unsigned start_index = word.front(); // get symbol + size_t start_row = start_index * this->state_num * this->state_num; + + for (size_t i = 1; i <= this->state_num; ++i) { + std::string word_expression = SOL_NEG + std::to_string(start_row + i) + SOL_DELIM + SOL_NEG; + + if (word.size() == 1) { // rejects a single letter + this->output << word_expression; + this->output << transitions_num + i << SOL_DELIM << SOL_EOL; + } else { + this->recurse_tseytin_reject(word_expression, i, word, 1); + } + } + } + + return max_index; +} + +void mata::nfa::SatStats::recurse_tseytin_accept(const std::vector& base, size_t state, Word word, const unsigned pos, + std::vector& result, size_t skip_init) { + unsigned symb_index = word[pos]; // get current symbol + + size_t current_row = symb_index * this->state_num * this->state_num + (state - 1) * this->state_num; + size_t transitions_num = this->state_num * this->state_num * this->alpha_num; + + for (size_t i = 1; i <= this->state_num; ++i) { // for variable in a row + std::vector addition = base; + addition.push_back(static_cast (current_row + i)); + addition.push_back(TSEY_AND); + + if (pos == word.size() - 1) { // end of the word + addition.push_back(static_cast (transitions_num + skip_init + i)); + result.insert(result.end(), addition.begin(), addition.end()); + result.push_back(TSEY_OR); + } else { + this->recurse_tseytin_accept(addition, i, word, pos+1, result, skip_init); + } + } +} + +void SatStats::recurse_tseytin_reject(const std::string& base, size_t state, Word word, const unsigned pos, + size_t skip_init) { + unsigned symb_index = word[pos]; // get current symbol + + size_t current_row = symb_index * this->state_num * this->state_num + (state - 1) * this->state_num; + size_t transitions_num = this->state_num * this->state_num * this->alpha_num; + + for (size_t i = 1; i <= this->state_num; ++i) { + std::string addition = base; + addition += std::to_string(current_row + i) + SOL_DELIM + SOL_NEG; + + if (pos == word.size()-1) { // end of the word + this->output << addition; + this->output << transitions_num + skip_init + i << SOL_DELIM << SOL_EOL; + } else { + this->recurse_tseytin_reject(addition, i, word, pos+1, skip_init); + } + } +} + +size_t mata::nfa::SatStats::example_nfa_clauses(size_t max_index) { + size_t transitions_num = this->state_num * this->state_num * this->alpha_num; + this->output << transitions_num + 1 << SOL_DELIM << SOL_EOL; // force the first state 0 to be an initial state + + for (auto word: this->accept) { + std::vector expression; // partial expression + std::vector result; // output for tseitin + + if (word.empty()) { // special case epsilon, set state 1 to be final state + this->output << transitions_num + state_num + 1 << SOL_DELIM << SOL_EOL; // skip initial states + continue; + } + + unsigned start_index = word.front(); + size_t start_row = start_index * this->state_num * this->state_num; + + for (size_t j = 0; j < this->state_num; ++j) { // for each possible initial state + size_t start_state = j * this->state_num; + + for (size_t i = 1; i <= this->state_num; ++i) { + expression.clear(); + // set init + expression.push_back(static_cast (transitions_num + j + 1)); + expression.push_back(TSEY_AND); + // add transitions + expression.push_back(static_cast (start_row + start_state + i)); + expression.push_back(TSEY_AND); + + if (word.size() == 1) { // accepts a single letter, add final state + expression.push_back(static_cast (transitions_num + this->state_num + i)); // skip initial states + result.insert(result.end(), expression.begin(), expression.end()); + result.push_back(TSEY_OR); + } else { + this->recurse_tseytin_accept(expression, i, word, 1, result, this->state_num); + } + } + } + + max_index = reduction_tseytin(result, max_index, output); + } + + for (auto word: this->reject) { + std::string expression; + + if (word.empty()) { // special case epsilon + for (size_t i = 1; i <= this->state_num; ++i) { // not initial or not final + this->output << SOL_NEG << transitions_num + i << SOL_DELIM << SOL_NEG << transitions_num + this->state_num + i << SOL_DELIM << SOL_EOL; + } + continue; + } + + unsigned start_index = word.front(); + size_t start_row = start_index * this->state_num * this->state_num; + + for (size_t j = 0; j < this->state_num; ++j) { + size_t start_state = j * this->state_num; + + for (size_t i = 1; i <= this->state_num; ++i) { + expression = SOL_NEG + std::to_string(transitions_num + j + 1); + expression += SOL_DELIM + SOL_NEG + std::to_string(start_row + start_state + i) + SOL_DELIM + SOL_NEG; + + if (word.size() == 1) { // rejects a single letter + this->output << expression; + this->output << transitions_num + this->state_num + i << SOL_DELIM << SOL_EOL; + } else { + this->recurse_tseytin_reject(expression, i, word, 1, this->state_num); + } + } + } + } + return max_index; +} + +void mata::nfa::QbfStats::init_final(size_t var_base, size_t result_base) { + for (size_t i = 0; i < this->state_num; i++) { // for every possible vector combination + size_t start_index = var_base; + for (int j = static_cast(this->state_bin-1); j >= 0; j--) { + if (i & (1 << j)) // get the bit value + this->output << SOL_NEG; + this->output << start_index << SOL_DELIM; + start_index++; // next bit vector variable + } + this->output << result_base << SOL_DELIM << SOL_EOL; + result_base++; // next init/final variable + } +} + +void mata::nfa::QbfStats::init_final_clauses(size_t state_base, size_t end_base) { + size_t trans_vars = this->state_num * this->state_num * this->alpha_num + 1; // number of trans vars + 1 + this->init_final(state_base, trans_vars); // initial clauses + this->init_final(end_base, trans_vars + this->state_num); // final clauses +} + +void mata::nfa::QbfStats::init_final_reject(size_t var_base, size_t result_base, std::vector& result) { + for (size_t i = 0; i < this->state_num; i++) { // for every possible vector combination + int start_index = static_cast(var_base); + for (int j = static_cast(this->state_bin-1); j >= 0; j--) { + if ((i & (1 << j)) == 0) // get the bit value + result.push_back(TSEY_NOT); + + result.push_back(start_index); + result.push_back(TSEY_AND); + start_index++; // next bit vector variable + } + result.push_back(TSEY_NOT); + result.push_back(static_cast (result_base)); + result.push_back(TSEY_OR); + result_base++; // next init/final variable + } +} + +void mata::nfa::QbfStats::init_final_clauses_reject(size_t state_base, size_t end_base, std::vector & result) { + size_t trans_vars = this->state_num * this->state_num * this->alpha_num + 1; // number of trans vars + 1 + this->init_final_reject(state_base, trans_vars, result); // init clauses + this->init_final_reject(end_base, trans_vars + this->state_num, result); // final clauses +} + +void mata::nfa::QbfStats::valid_combinations(size_t start) { + size_t range = (1 << this->state_bin); // number of states possible for the given bit vector + for (size_t i = this->state_num; i < range; i++) { // for every invalid combination + this->output << SOL_NEG << start << SOL_DELIM; // first bit cannot be true + + unsigned cnt_back = this->state_bin-1; + for (size_t tmp = i; tmp > 1; tmp = tmp >> 1) { + if (tmp & 1) + this->output << SOL_NEG; + + this->output << start + cnt_back << SOL_DELIM; + cnt_back--; // counting from the back + } + this->output << SOL_EOL; + } +} + +void mata::nfa::QbfStats::valid_combinations_reject(size_t start, std::vector & input) { + size_t range = (1 << this->state_bin); // number of states possible for the given bit vector + for (size_t i = this->state_num; i < range; i++) { // for every invalid combination + input.push_back(static_cast (start)); // first bit must be true + + unsigned cnt_back = this->state_bin-1; + for (size_t tmp = i; tmp > 1; tmp = tmp >> 1) { // binary representation + input.push_back(TSEY_AND); + if ((tmp & 1) == 0) + input.push_back(TSEY_NOT); + + input.push_back(static_cast (start + cnt_back)); + cnt_back--; // counting from the back + } + input.push_back(TSEY_OR); + } +} + +void mata::nfa::QbfStats::accept_clauses(size_t free_var, size_t curr_trans) { + for (size_t i = 0; i < this->state_num; i++) { // from state binary vector combinations + for (size_t j = 0; j < this->state_num; j++) { // to state binary vector combinations + size_t from_state = free_var; + size_t to_state = free_var + this->state_bin; + + for (int k = static_cast(this->state_bin-1); k >= 0; k--) { // from state + if (i & (1 << k)) // binary representation + this->output << SOL_NEG; + this->output << from_state << SOL_DELIM; + from_state++; + } + + for (int l = static_cast(this->state_bin-1); l >= 0; l--) { // to state + if (j & (1 << l)) // binary representation + this->output << SOL_NEG; + this->output << to_state << SOL_DELIM; + to_state++; + } + this->output << curr_trans << SOL_DELIM << SOL_EOL; + curr_trans++; // transition variables + } + } +} + +void mata::nfa::QbfStats::reject_clauses(size_t free_var, size_t curr_trans, std::vector & result) { + for (size_t i = 0; i < this->state_num; i++) { // from state binary vector combinations + for (size_t j = 0; j < this->state_num; j++) { // to state binary vector combinations + int from_state = static_cast(free_var); + int to_state = static_cast(free_var + this->state_bin); + + for (int k = static_cast(this->state_bin-1); k >= 0; k--) { // from state + if ((i & (1 << k)) == 0) // binary representation + result.push_back(TSEY_NOT); + result.push_back(from_state); + result.push_back(TSEY_AND); + from_state++; + } + + for (int l = static_cast(this->state_bin-1); l >= 0; l--) { // to state + if ((j & (1 << l)) == 0) // binary representation + result.push_back(TSEY_NOT); + result.push_back(to_state); + result.push_back(TSEY_AND); + to_state++; + } + result.push_back(TSEY_NOT); + result.push_back(static_cast (curr_trans)); + result.push_back(TSEY_OR); + curr_trans++; // transition variables + } + } +} + +void mata::nfa::QbfStats::example_clauses(size_t max_index){ + size_t transitions_num = this->state_num * this->state_num * this->alpha_num; // number of transitions + size_t free_var = transitions_num + 2 * this->state_num + 1; // first free index possible to use for Tseytin transformation + + this->output << transitions_num + 1 << SOL_DELIM << SOL_EOL; // force the first state 0 to be an initial state + + for (auto word: this->accept) { + if (word.empty()) { // special case epsilon, force state 0 to be final state + this->output << transitions_num + 1 + this->state_num << SOL_DELIM << SOL_EOL; + continue; + } + + this->init_final_clauses(free_var, free_var + this->state_bin * word.size()); // initial and final clauses + this->valid_combinations(free_var); // valid combination for the first binary vector + + for (auto symbol: word) { + accept_clauses(free_var, 1 + symbol * this->state_num * this->state_num); // transition clauses + free_var += this->state_bin; // next binary vector + this->valid_combinations(free_var); // valid combinations for new binary vector + } + free_var += this->state_bin; + } + + for (auto word: this->reject) { + std::vector result; + + if (word.empty()) { // special case epsilon, if state is initial then cannot be final + for (size_t i = 1; i <= this->state_num; i++) { + this->output << SOL_NEG << transitions_num + i << SOL_DELIM << SOL_NEG + << transitions_num + i + this->state_num << SOL_DELIM << SOL_EOL; + } + continue; + } + + this->init_final_clauses_reject(free_var, free_var + this->state_bin * word.size(), result); // initial and final clauses + this->valid_combinations_reject(free_var, result); // valid combinations for the first state + + for (auto symbol: word) { + reject_clauses(free_var, 1 + symbol * this->state_num * this->state_num, result); // transition clauses + free_var += this->state_bin; // next binary vector + this->valid_combinations_reject(free_var, result); // valid combinations for new binary vector + } + free_var += this->state_bin; + + result.pop_back(); // remove the last operator + max_index = reduction_tseytin(result, max_index, output); // CNF transformation + result.clear(); + } +} + +std::filesystem::path get_path_to_solvers() { + std::filesystem::path current_file_path = __FILE__; // absolute path to the current file + std::filesystem::path current_directory = current_file_path.parent_path(); + + // path to solvers dir + std::filesystem::path target_file_path = current_directory / "../../3rdparty/solvers/"; + target_file_path = std::filesystem::canonical(target_file_path); // resolve the relative path to an absolute path + + return target_file_path; +} + +std::string create_temp_file() { + char temp_name[] = "/tmp/solverXXXXXX"; // template for solver tmp files + + int fd = mkstemp(temp_name); // create a unique temporary file + if (fd == -1) { + throw std::runtime_error("Failed to create a temporary file"); + } + close(fd); + + return std::string(temp_name); // return the name of the tmp file +} + +Nfa mata::nfa::reduce_sat(const Nfa &aut, const ParameterMap& params, bool debug){ + if (!haskey(params, "solver")) { + throw std::runtime_error(std::to_string(__func__) + + " requires setting the \"solver\" key in the \"params\" argument; " + "received: " + std::to_string(params)); + } + + const std::string& solver_type = params.at("solver"); + if (solver_type != "sat" && solver_type != "sat_nfa") + throw std::runtime_error(std::to_string(__func__) + + " received an unknown value of the \"solver\" key: " + solver_type); + + std::filesystem::path solver_dir = get_path_to_solvers(); // get path to the solvers + std::string clauses = create_temp_file(); // create temp files + std::string solver_out = create_temp_file(); + + // construct the command to run solver + std::string command = (solver_dir / "MiniSat.14_linux").string() + " " + clauses + " " + solver_out + " > /dev/null"; + + std::ofstream clauses_file(clauses, std::ios::out); // output file for the generated clauses + if (clauses_file.is_open() == false) { + throw std::runtime_error("Failed to open file: " + clauses); + } + + SatStats sat(1, aut.delta.get_used_symbols().size(), clauses_file, {}, {}); // initial values + SatStats partial_sat(sat); // help stats for partial generation of clauses + sat.accept = std::move(get_shortest_words(aut)); + + Run* reject_run = new Run(); // variables to return the words that differ the original and created automata + Run* accept_run = new Run(); + std::pair equal_runs = std::make_pair(reject_run, accept_run); + + bool found = false; + Nfa sat_result; + size_t max_var; + + while (found != true) { + clauses_file.close(); // clear the file from the previous clauses + clauses_file.open(clauses, std::ios::out); + if (clauses_file.is_open() == false) { + throw std::runtime_error("Failed to open file: " + clauses); + } + + if (solver_type == "sat"){ // complete dfa automaton with single initial state + sat.determine_clauses(); + sat.complete_clauses(); + max_var = sat.example_clauses(sat.state_num * sat.state_num * sat.alpha_num + sat.state_num + 1); + } else { // nfa automaton + max_var = sat.example_nfa_clauses(sat.state_num * sat.state_num * sat.alpha_num + 2*sat.state_num + 1); + } + clauses_file.flush(); // flush the contents into the file + + bool unsat = false; + while (unsat != true) { + if (debug) { + sat.print(std::cout); // debug output + sleep(1); // to be able to read the output + } + + int result = system(command.c_str()); // run the solver + + if (result == 2560) { // satisfiable + std::ifstream result_file(solver_out, std::ios::in); // read solver solution + sat_result = sat.build_result(result_file, params); + result_file.close(); + if (are_equivalent(aut, sat_result, {{"algorithm", "naive"}}, equal_runs)) { + found = true; // found solution + break; + } else { + partial_sat.reject.clear(); // clear partial stats + partial_sat.accept.clear(); + + if (equal_runs.first->path.size() != 0){ + sat.accept.emplace(equal_runs.first->word); + partial_sat.accept.emplace(equal_runs.first->word); + equal_runs.first->path.clear(); + } + + if (equal_runs.second->path.size() != 0){ + sat.reject.emplace(equal_runs.second->word); + partial_sat.reject.emplace(equal_runs.second->word); + equal_runs.second->path.clear(); + } + + if (solver_type == "sat") + max_var = partial_sat.example_clauses(max_var); // additional clauses for found word + else + max_var = partial_sat.example_nfa_clauses(max_var); // additional clauses for found word + clauses_file.flush(); + } + } + else if (result == 5120){ // unsatisfiable + unsat = true; + sat.state_num++; // raise the number of states + partial_sat.state_num++; + } + else { // error occured + throw std::runtime_error("SAT solver ended in failure"); + } + } + } + + // free memory + delete(accept_run); + delete(reject_run); + + clauses_file.close(); + + return sat_result; +} + +Nfa mata::nfa::reduce_qbf(const Nfa &aut, bool debug) { + std::filesystem::path solver_dir = get_path_to_solvers(); // get path to the solvers + std::string clauses = create_temp_file(); // create temp files + std::string solver_out = create_temp_file(); + + // construct the command to run solver + std::string command = (solver_dir / "caqe").string() + " --qdo " + clauses + " > " + solver_out; + + std::ofstream clauses_file(clauses, std::ios::out); // output file for the generated clauses + if (clauses_file.is_open() == false) { + throw std::runtime_error("Failed to open file: " + clauses); + } + + QbfStats qbf(1, aut.delta.get_used_symbols().size(), clauses_file, {}, {}); // initial values + qbf.accept = std::move(get_shortest_words(aut)); + + Run* reject_run = new Run(); // variables to return the words that differ the original and created automata + Run* accept_run = new Run(); + std::pair equal_runs = std::make_pair(reject_run, accept_run); + + bool found = false; + Nfa qbf_result; + + while (found != true) { + clauses_file.close(); // clear the file from the previous clauses + clauses_file.open(clauses, std::ios::out); + if (clauses_file.is_open() == false) { + throw std::runtime_error("Failed to open file: " + clauses); + } + + size_t start_index = qbf.print_qbf_header(); + qbf.example_clauses(start_index); + clauses_file.flush(); // flush the contents into the file + + if (debug) { + qbf.print(std::cout); // debug output + sleep(1); // to be able to read the output + } + + int result = system(command.c_str()); // run the solver + + if (result == 2560) { // satisfiable + std::ifstream result_file(solver_out, std::ios::in); // read solver solution + qbf_result = qbf.build_result(result_file, {{"solver", "qbf"}}); + result_file.close(); + + if (are_equivalent(aut, qbf_result, {{"algorithm", "naive"}}, equal_runs)) { + found = true; // found solution + } else { + if (equal_runs.first->path.size() != 0) { + qbf.accept.emplace(equal_runs.first->word); + equal_runs.first->path.clear(); + } + + if (equal_runs.second->path.size() != 0){ + qbf.reject.emplace(equal_runs.second->word); + equal_runs.second->path.clear(); + } + } + } + else if (result == 5120){ // unsatisfiable + qbf.state_num++; // raise the number of states + qbf.recompute_bin(); + } + else { // error occured + throw std::runtime_error("QBF solver ended in failure"); + } + } + + // free memory + delete(accept_run); + delete(reject_run); + + clauses_file.close(); + + return qbf_result; +} diff --git a/tests/nfa/nfa.cc b/tests/nfa/nfa.cc index 275d7f30e..4a338c2b6 100644 --- a/tests/nfa/nfa.cc +++ b/tests/nfa/nfa.cc @@ -2466,6 +2466,190 @@ TEST_CASE("mata::nfa::reduce_size_by_residual()") { } } +TEST_CASE("mata::nfa::reduce_size_using_solvers()") { + Nfa aut; + StateRenaming state_renaming; + ParameterMap params; + params["algorithm"] = "solvers"; + + SECTION("empty automaton") + { + params["solver"] = "sat"; + Nfa result_sat = reduce(aut, &state_renaming, params); + + params["solver"] = "sat_nfa"; + Nfa result_sat_nfa = reduce(aut, &state_renaming, params); + + params["solver"] = "qbf"; + Nfa result_qbf = reduce(aut, &state_renaming, params); + + REQUIRE(result_sat.delta.empty()); + REQUIRE(result_sat.initial.size() == 1); + REQUIRE(result_sat.final.empty()); + REQUIRE(result_sat.num_of_states() == 1); + + REQUIRE(result_sat_nfa.delta.empty()); + REQUIRE(result_sat_nfa.final.empty()); + REQUIRE(result_sat_nfa.num_of_states() == 1); + + REQUIRE(result_qbf.delta.empty()); + REQUIRE(result_qbf.final.empty()); + REQUIRE(result_qbf.num_of_states() == 1); + + REQUIRE(are_equivalent(aut, result_sat)); + REQUIRE(are_equivalent(result_sat, result_sat_nfa)); + REQUIRE(result_sat_nfa.is_identical(result_qbf)); + } + + SECTION("reduce empty automaton") + { + aut.initial = { 0 }; + aut.delta.add(0, 0, 1); + aut.delta.add(0, 1, 0); + aut.delta.add(1, 1, 1); + aut.delta.add(1, 2, 2); + + params["solver"] = "sat"; + Nfa result_sat = reduce(aut, &state_renaming, params); + + params["solver"] = "sat_nfa"; + Nfa result_sat_nfa = reduce(aut, &state_renaming, params); + + params["solver"] = "qbf"; + Nfa result_qbf = reduce(aut, &state_renaming, params); + + REQUIRE(!result_sat.delta.empty()); + REQUIRE(result_sat.initial.size() == 1); + REQUIRE(result_sat.final.empty()); + REQUIRE(result_sat.num_of_states() == 1); + + REQUIRE(result_sat_nfa.final.empty()); + REQUIRE(result_sat_nfa.num_of_states() == 1); + + REQUIRE(result_qbf.final.empty()); + REQUIRE(result_qbf.num_of_states() == 1); + + REQUIRE(are_equivalent(aut, result_sat)); + REQUIRE(are_equivalent(result_sat, result_sat_nfa)); + REQUIRE(result_sat_nfa.is_identical(result_qbf)); + } + + SECTION("simple automaton") + { + aut.initial = { 1 }; + aut.final = { 3 }; + aut.delta.add(1, 0, 2); + aut.delta.add(2, 1, 3); + aut.delta.add(3, 0, 3); + aut.delta.add(3, 1, 3); + + params["solver"] = "sat"; + Nfa result_sat = reduce(aut, &state_renaming, params); + + params["solver"] = "sat_nfa"; + Nfa result_sat_nfa = reduce(aut, &state_renaming, params); + + params["solver"] = "qbf"; + Nfa result_qbf = reduce(aut, &state_renaming, params); + + REQUIRE(!result_sat.delta.empty()); + REQUIRE(result_sat.initial.size() == 1); + REQUIRE(!result_sat.final.empty()); + REQUIRE(result_sat.num_of_states() == 4); + + REQUIRE(!result_sat_nfa.initial.empty()); + REQUIRE(!result_sat_nfa.final.empty()); + REQUIRE(result_sat_nfa.num_of_states() == 3); + + REQUIRE(!result_qbf.initial.empty()); + REQUIRE(!result_qbf.final.empty()); + REQUIRE(result_qbf.num_of_states() == 3); + + REQUIRE(are_equivalent(aut, result_sat)); + REQUIRE(are_equivalent(result_sat, result_sat_nfa)); + REQUIRE(are_equivalent(result_sat_nfa, result_qbf)); + } + + SECTION("reduce simple automaton sat") + { + aut.initial = { 1 }; + aut.final = { 4 }; + aut.delta.add(1, 0, 2); + aut.delta.add(1, 1, 3); + aut.delta.add(1, 2, 1); + aut.delta.add(1, 2, 2); + aut.delta.add(1, 2, 3); + aut.delta.add(2, 0, 4); + aut.delta.add(2, 1, 4); + aut.delta.add(3, 0, 4); + aut.delta.add(3, 1, 4); + aut.delta.add(4, 2, 1); + + params["solver"] = "sat"; + Nfa result_sat = reduce(aut, &state_renaming, params); + + params["solver"] = "sat_nfa"; + Nfa result_sat_nfa = reduce(aut, &state_renaming, params); + + REQUIRE(!result_sat.delta.empty()); + REQUIRE(result_sat.initial.size() == 1); + REQUIRE(result_sat.final.size() == 2); + REQUIRE(result_sat.num_of_states() == 6); + + REQUIRE(!result_sat_nfa.initial.empty()); + REQUIRE(!result_sat_nfa.final.empty()); + REQUIRE(result_sat_nfa.num_of_states() == 3); + + REQUIRE(are_equivalent(aut, result_sat)); + REQUIRE(are_equivalent(result_sat, result_sat_nfa)); + } + + SECTION("reduce simple automaton qbf") + { + aut.initial = { 1 }; + aut.final = { 4 }; + aut.delta.add(1, 0, 2); + aut.delta.add(1, 1, 3); + aut.delta.add(2, 0, 4); + aut.delta.add(2, 1, 4); + aut.delta.add(3, 0, 4); + aut.delta.add(3, 1, 4); + aut.delta.add(4, 0, 4); + aut.delta.add(4, 1, 4); + + params["solver"] = "sat_nfa"; + Nfa result_sat_nfa = reduce(aut, &state_renaming, params); + + params["solver"] = "qbf"; + Nfa result_qbf = reduce(aut, &state_renaming, params); + + REQUIRE(!result_qbf.initial.empty()); + REQUIRE(!result_qbf.final.empty()); + REQUIRE(result_qbf.num_of_states() == 3); + REQUIRE(result_qbf.num_of_states() == result_sat_nfa.num_of_states()); + + REQUIRE(are_equivalent(aut, result_sat_nfa)); + REQUIRE(are_equivalent(result_sat_nfa, result_qbf)); + } + + SECTION("error checking") + { + CHECK_THROWS_WITH(reduce(aut, &state_renaming, params), + Catch::Contains("requires setting the \"solver\" key in the \"params\" argument;")); + + params["solver"] = "bad_solver"; + CHECK_THROWS_WITH(reduce(aut, &state_renaming, params), + Catch::Contains("received an unknown value of the \"solver\" key")); + + params["solver"] = "sat"; + CHECK_NOTHROW(reduce(aut, &state_renaming, params)); + + params["solver"] = "qbf"; + CHECK_NOTHROW(reduce(aut, &state_renaming, params)); + + } +} + TEST_CASE("mata::nfa::union_norename()") { Run one{{1},{}}; Run zero{{0}, {}};