Skip to content

Commit c79d40e

Browse files
LuccaT95LuccaT95
committed
Fixes after merging of changes regarding renaming.
1 parent 2ef626f commit c79d40e

9 files changed

+72
-59
lines changed

‎src/interpreter.h

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,7 @@ struct finputs {
9696

9797
// Read input from command line and return mapping from in_vars to this input
9898
std::pair<std::optional<assignment<BAs...> >, bool> read(
99-
std::vector<nso<BAs...> >& in_vars, size_t time_step) const {
99+
std::vector<tau<BAs...> >& in_vars, size_t time_step) const {
100100
std::ranges::sort(in_vars, constant_io_comp);
101101
assignment<BAs...> value;
102102
for (const auto& var : in_vars) {
@@ -142,7 +142,7 @@ struct finputs {
142142
return {value, false};
143143
}
144144

145-
std::optional<type> type_of(const nso<BAs...>& var) const {
145+
std::optional<type> type_of(const tau<BAs...>& var) const {
146146
if (auto type = types.find(var); type != types.end())
147147
return type->second;
148148

@@ -157,8 +157,8 @@ struct finputs {
157157
return {};
158158
}
159159

160-
std::map<nso<BAs...>, type> types;
161-
mutable std::map<nso<BAs...>, std::optional<std::ifstream>> streams;
160+
std::map<tau<BAs...>, type> types;
161+
mutable std::map<tau<BAs...>, std::optional<std::ifstream>> streams;
162162
size_t time_point = 0;
163163
};
164164

@@ -185,7 +185,7 @@ struct foutputs {
185185

186186
bool write(const assignment<BAs...>& outputs) {
187187
// Sort variables in output by time
188-
std::vector<nso<BAs...>> io_vars;
188+
std::vector<tau<BAs...>> io_vars;
189189
for (const auto& [var, ass] : outputs) {
190190
assert(is_child_non_terminal(tau_parser::io_var, trim(var)));
191191
io_vars.push_back(var);
@@ -240,7 +240,7 @@ struct foutputs {
240240
return true; // success
241241
}
242242

243-
std::optional<type> type_of(const nso<BAs...>& var) const {
243+
std::optional<type> type_of(const tau<BAs...>& var) const {
244244
if (auto type = types.find(var); type != types.end())
245245
return type->second;
246246

@@ -348,7 +348,7 @@ struct foutputs {
348348

349349
template<typename input_t, typename output_t, typename...BAs>
350350
struct interpreter {
351-
interpreter(const nso<BAs...>& ubt_ctn, assignment<BAs...>& memory,
351+
interpreter(const tau<BAs...>& ubt_ctn, assignment<BAs...>& memory,
352352
const auto& input, const auto& output) :
353353
ubt_ctn(ubt_ctn),
354354
memory(memory),
@@ -366,14 +366,14 @@ struct interpreter {
366366
}
367367

368368
static std::optional<interpreter> make_interpreter(
369-
nso<BAs...> spec, const auto& inputs, const auto& outputs);
369+
tau<BAs...> spec, const auto& inputs, const auto& outputs);
370370

371371
std::pair<std::optional<assignment<BAs...>>, bool> step();
372372

373373
// store all the possible systems to be solved, each system corresponds to a
374374
// different clause.
375375

376-
nso<BAs...> ubt_ctn;
376+
tau<BAs...> ubt_ctn;
377377
assignment<BAs...> memory;
378378
size_t time_point = 0;
379379
// TODO: Remove inputs and outputs, once type inference for variables is ready
@@ -392,32 +392,32 @@ struct interpreter {
392392

393393
// Return typed systems of equations for the solver corresponding to each clause
394394
// in the unbound continuation
395-
static std::vector<system<BAs...>> compute_systems(const nso<BAs...>& ubd_ctn,
395+
static std::vector<system<BAs...>> compute_systems(const tau<BAs...>& ubd_ctn,
396396
const auto& inputs, const auto& outputs);
397397

398398
// Get the type for a clause of a local specification
399-
static std::optional<system<BAs...>> compute_atomic_fm_types(const nso<BAs...>& clause,
399+
static std::optional<system<BAs...>> compute_atomic_fm_types(const tau<BAs...>& clause,
400400
const auto& inputs, const auto& outputs);
401401

402402
// Compute the type of the equation f = 0 or f != 0 stored in fm for the solver
403-
static std::optional<std::pair<type, nso<BAs...>>> get_type_fm(const nso<BAs...>& fm,
403+
static std::optional<std::pair<type, tau<BAs...>>> get_type_fm(const tau<BAs...>& fm,
404404
const auto& inputs, const auto& outputs);
405405

406-
nso<BAs...> update_to_time_point(const nso<BAs...>& f);
406+
tau<BAs...> update_to_time_point(const tau<BAs...>& f);
407407

408408
// If a variable is assigned a variable V in a solution from the solver,
409409
// try to find a non-variable value by checking the solution for V
410410
void resolve_solution_dependencies(solution<BAs...>& s);
411411

412412
// Return the lookback and highest initial position of the given unbound continuation
413-
void compute_lookback_and_initial (const nso<BAs...>& ubd_ctn);
413+
void compute_lookback_and_initial (const tau<BAs...>& ubd_ctn);
414414

415415
// Find an executable specification from DNF
416-
static nso<BAs...> get_executable_spec(const nso<BAs...>& fm);
416+
static tau<BAs...> get_executable_spec(const tau<BAs...>& fm);
417417
};
418418

419419
template<typename input_t, typename output_t, typename...BAs>
420-
void run(const nso<BAs...>& form, input_t& inputs, output_t& outputs) {
420+
void run(const tau<BAs...>& form, input_t& inputs, output_t& outputs) {
421421
auto spec = normalizer(form);
422422
auto intrprtr = interpreter<input_t, output_t, BAs...>
423423
::make_interpreter(spec, inputs, outputs);

‎src/interpreter.impl.h

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -5,12 +5,12 @@
55

66
#include "interpreter.h"
77

8-
namespace idni::tau {
8+
namespace idni::tau_lang {
99

1010
template<typename input_t, typename output_t, typename...BAs>
1111
std::optional<interpreter<input_t, output_t, BAs...>>
1212
interpreter<input_t, output_t, BAs...>::make_interpreter(
13-
nso<BAs...> spec, const auto& inputs, const auto& outputs) {
13+
tau<BAs...> spec, const auto& inputs, const auto& outputs) {
1414
// Find a satisfiable unbound continuation from spec
1515
auto ubd_ctn = get_executable_spec(spec);
1616
if (ubd_ctn == nullptr) {
@@ -223,11 +223,11 @@ bool interpreter<input_t, output_t, BAs...>::calculate_initial_systems() {
223223
}
224224

225225
template<typename input_t, typename output_t, typename...BAs>
226-
nso<BAs...> interpreter<input_t, output_t, BAs...>::update_to_time_point(const nso<BAs...>& f) {
226+
tau<BAs...> interpreter<input_t, output_t, BAs...>::update_to_time_point(const tau<BAs...>& f) {
227227
// update the f according to current time_point, i.e. for each
228228
// input/output var which has a shift, we replace it with the value
229229
// corresponding to the current time_point minus the shift.
230-
std::map<nso<BAs...>, nso<BAs...> > changes;
230+
std::map<tau<BAs...>, tau<BAs...> > changes;
231231
for (const auto& io_var:
232232
select_top(
233233
f, is_non_terminal<tau_parser::io_var, BAs...>))
@@ -279,8 +279,8 @@ void interpreter<input_t, output_t, BAs...>::resolve_solution_dependencies(solut
279279
}
280280

281281
template<typename input_t, typename output_t, typename...BAs>
282-
void interpreter<input_t, output_t, BAs...>::compute_lookback_and_initial( const nso<BAs...>& ubd_ctn) {
283-
std::vector<nso<BAs...> > io_vars = select_top(ubd_ctn,
282+
void interpreter<input_t, output_t, BAs...>::compute_lookback_and_initial( const tau<BAs...>& ubd_ctn) {
283+
std::vector<tau<BAs...> > io_vars = select_top(ubd_ctn,
284284
is_child_non_terminal< tau_parser::io_var , BAs...>);
285285
lookback = get_max_shift(io_vars);
286286
formula_time_point = lookback;
@@ -289,7 +289,7 @@ void interpreter<input_t, output_t, BAs...>::compute_lookback_and_initial( const
289289

290290

291291
template<typename input_t, typename output_t, typename...BAs>
292-
std::vector<system<BAs...>> interpreter<input_t, output_t, BAs...>::compute_systems(const nso<BAs...>& ubd_ctn,
292+
std::vector<system<BAs...>> interpreter<input_t, output_t, BAs...>::compute_systems(const tau<BAs...>& ubd_ctn,
293293
const auto& inputs, const auto& outputs) {
294294
std::vector<system<BAs...>> systems;
295295
// Create blue-print for solver for each clause
@@ -306,9 +306,9 @@ std::vector<system<BAs...>> interpreter<input_t, output_t, BAs...>::compute_syst
306306
}
307307

308308
template<typename input_t, typename output_t, typename...BAs>
309-
std::optional<system<BAs...>> interpreter<input_t, output_t, BAs...>::compute_atomic_fm_types(const nso<BAs...>& clause,
309+
std::optional<system<BAs...>> interpreter<input_t, output_t, BAs...>::compute_atomic_fm_types(const tau<BAs...>& clause,
310310
const auto& inputs, const auto& outputs) {
311-
auto is_atomic_fm = [](const nso<BAs...>& n) {
311+
auto is_atomic_fm = [](const tau<BAs...>& n) {
312312
return is_child_non_terminal<tau_parser::bf_eq, BAs...>(n)
313313
|| is_child_non_terminal<tau_parser::bf_neq, BAs...>(n);
314314
};
@@ -337,7 +337,7 @@ std::optional<system<BAs...>> interpreter<input_t, output_t, BAs...>::compute_at
337337
}
338338

339339
template<typename input_t, typename output_t, typename...BAs>
340-
std::optional<std::pair<type, nso<BAs...>>> interpreter<input_t, output_t, BAs...>::get_type_fm(const nso<BAs...>& fm,
340+
std::optional<std::pair<type, tau<BAs...>>> interpreter<input_t, output_t, BAs...>::get_type_fm(const tau<BAs...>& fm,
341341
const auto& inputs, const auto& outputs) {
342342
if (auto io_var = find_top(fm,
343343
is_non_terminal<tau_parser::io_var, BAs...>); io_var) {
@@ -359,7 +359,7 @@ std::optional<std::pair<type, nso<BAs...>>> interpreter<input_t, output_t, BAs..
359359
}
360360

361361
template<typename input_t, typename output_t, typename...BAs>
362-
nso<BAs...> interpreter<input_t, output_t, BAs...>::get_executable_spec(const nso<BAs...>& fm) {
362+
tau<BAs...> interpreter<input_t, output_t, BAs...>::get_executable_spec(const tau<BAs...>& fm) {
363363
for (auto& clause : get_dnf_wff_clauses(fm)) {
364364
#ifdef DEBUG
365365
BOOST_LOG_TRIVIAL(trace)
@@ -409,5 +409,5 @@ nso<BAs...> interpreter<input_t, output_t, BAs...>::get_executable_spec(const ns
409409
return nullptr;
410410
}
411411

412-
}
412+
} // namespace idni::tau_lang
413413
#endif //INTERPRETER_IMPL_H

‎src/normal_forms.h

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -224,10 +224,10 @@ static auto to_nnf_bf = make_library<BAs...>(
224224
// --------------------------------------------------------------
225225
// General operator for tau<BAs...> function application by pipe
226226
template<typename... BAs>
227-
using nso_transform = tau<BAs...>(*)(const tau<BAs...>&);
227+
using tau_transform = tau<BAs...>(*)(const tau<BAs...>&);
228228

229229
template<typename... BAs>
230-
tau<BAs...> operator| (const tau<BAs...>& fm, const nso_transform<BAs...> func) {
230+
tau<BAs...> operator| (const tau<BAs...>& fm, const tau_transform<BAs...> func) {
231231
return func(fm);
232232
}
233233
// --------------------------------------------------------------
@@ -819,7 +819,7 @@ bool assign_and_reduce(const tau<BAs...>& fm,
819819
if (!is_wff) {
820820
// fm is a Boolean function
821821
// Normalize tau subformulas
822-
fm_simp = fm | (nso_transform<BAs...>)normalize_ba<BAs...>;
822+
fm_simp = fm | (tau_transform<BAs...>)normalize_ba<BAs...>;
823823
fm_simp = to_dnf2(fm_simp, false);
824824
fm_simp = reduce2(fm_simp, tau_parser::bf);
825825

@@ -2423,7 +2423,7 @@ struct sometimes_always_normalization_depreciated {
24232423

24242424
// Adjust the lookback before conjunction of fm1 and fm2
24252425
template<typename...BAs>
2426-
nso<BAs...> always_conjunction (const nso<BAs...>& fm1_aw, const nso<BAs...>& fm2_aw) {
2426+
tau<BAs...> always_conjunction (const tau<BAs...>& fm1_aw, const tau<BAs...>& fm2_aw) {
24272427
using p = tau_parser;
24282428
// Trim the always node if present
24292429
auto fm1 = is_child_non_terminal(p::wff_always, fm1_aw) ? trim2(fm1_aw) : fm1_aw;
@@ -2451,7 +2451,7 @@ nso<BAs...> always_conjunction (const nso<BAs...>& fm1_aw, const nso<BAs...>& fm
24512451

24522452
template<typename... BAs>
24532453
struct sometimes_always_normalization {
2454-
nso<BAs...> operator() (const nso<BAs...>& fm) const {
2454+
tau<BAs...> operator() (const tau<BAs...>& fm) const {
24552455
using p = tau_parser;
24562456
auto st_aw = [](const auto& n) {
24572457
return is_child_non_terminal(p::wff_sometimes, n) ||
@@ -2462,7 +2462,7 @@ struct sometimes_always_normalization {
24622462
}
24632463
// Delete all always/sometimes if they scope no temporal variable
24642464
auto temps = select_top(fm, st_aw);
2465-
std::map<nso<BAs...>, nso<BAs...>> changes;
2465+
std::map<tau<BAs...>, tau<BAs...>> changes;
24662466
for (const auto& temp : temps) {
24672467
if (!has_temp_var(temp))
24682468
changes.emplace(temp, trim2(temp));
@@ -2472,18 +2472,18 @@ struct sometimes_always_normalization {
24722472
changes.empty()
24732473
? fm
24742474
: replace(fm, changes), false));
2475-
nso<BAs...> res = _F<BAs...>;
2476-
nso<BAs...> always_disjuncts = _F<BAs...>;
2477-
for (const nso<BAs...>& clause : clauses) {
2475+
tau<BAs...> res = _F<BAs...>;
2476+
tau<BAs...> always_disjuncts = _F<BAs...>;
2477+
for (const tau<BAs...>& clause : clauses) {
24782478
// If clause does not contain sometimes/always but temporal variables, we add it to always_disjuncts
24792479
if (!find_top(clause, st_aw)) {
24802480
always_disjuncts = build_wff_or(always_disjuncts, clause);
24812481
continue;
24822482
}
24832483
auto conjuncts = get_cnf_wff_clauses(clause);
2484-
nso<BAs...> always_part = _T<BAs...>;
2485-
nso<BAs...> staying = _T<BAs...>;
2486-
for (const nso<BAs...>& conj : conjuncts) {
2484+
tau<BAs...> always_part = _T<BAs...>;
2485+
tau<BAs...> staying = _T<BAs...>;
2486+
for (const tau<BAs...>& conj : conjuncts) {
24872487
if (!st_aw(conj))
24882488
always_part = always_conjunction(always_part, conj);
24892489
else if (is_child_non_terminal(p::wff_always, conj))

‎src/normalizer.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ tau<BAs...> normalizer_step(const tau<BAs...>& form) {
6060

6161
auto result = form
6262
// Push all quantifiers in and eliminate them
63-
| (nso_transform<BAs...>)eliminate_quantifiers<BAs...>
63+
| (tau_transform<BAs...>)eliminate_quantifiers<BAs...>
6464
// After removal of quantifiers, only subformulas previously under the scope of a quantifier
6565
// are reduced
6666
| bf_reduce_canonical<BAs...>()
@@ -82,7 +82,7 @@ tau<BAs...> normalize_non_temp(const tau<BAs...>& fm) {
8282
#endif // TAU_CACHE
8383
auto result = fm
8484
// Push all quantifiers in and eliminate them
85-
| (nso_transform<BAs...>)eliminate_quantifiers<BAs...>
85+
| (tau_transform<BAs...>)eliminate_quantifiers<BAs...>
8686
// After removal of quantifiers, only subformulas previously under the scope of a quantifier
8787
// are reduced
8888
| bf_reduce_canonical<BAs...>();

‎src/repl_evaluator.tmpl.h

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -171,7 +171,7 @@ bool repl_evaluator<BAs...>::contains(const tau_nso_t& n,
171171
tau_parser::nonterminal nt)
172172
{
173173
auto pred = [nt](const auto& n) {
174-
return is_non_terminal<tau_ba<BAs...>, BAs...>(nt, n); };
174+
return is_non_terminal<tau_ba_t, BAs...>(nt, n); };
175175
return find_top<decltype(pred), tau_nso<BAs...>>(n, pred).has_value();
176176
}
177177

@@ -552,7 +552,7 @@ void repl_evaluator<BAs...>::run_cmd(const tau_nso_t& n)
552552
}
553553
}
554554

555-
auto outs = foutputs<tau_ba<BAs...>, BAs...>(current_outputs);
555+
auto outs = foutputs<tau_ba_t, BAs...>(current_outputs);
556556
run(dnf, ins, outs);
557557
return;
558558
}
@@ -589,10 +589,13 @@ void repl_evaluator<BAs...>::solve_cmd(const tau_nso_t& n) {
589589
: get_type_and_arg(n->child[1]); nn)
590590
{
591591
auto [t, program] = nn.value();
592-
auto applied = apply_rr_to_rr_gssotc(t, program);
592+
auto applied = apply_rr_to_rr_tau_nso(t, program);
593593
applied = normalize_non_temp(applied);
594-
if (!nn) { BOOST_LOG_TRIVIAL(error) << "(Error) invalid argument\n"; return; }
595-
auto s = solve<tau_ba<BAs...>, BAs...>(applied, type.value());
594+
if (!nn) {
595+
BOOST_LOG_TRIVIAL(error) <<
596+
"(Error) invalid argument\n"; return;
597+
}
598+
auto s = solve<tau_ba_t, BAs...>(applied, type.value());
596599
if (!s) { std::cout << "no solution\n"; return; }
597600
std::cout << "solution: {" << "\n";
598601
for (auto& [k, v] : s.value()) {
@@ -678,7 +681,7 @@ std::optional<tau_nso<BAs...>>
678681
always_to_unbounded_continuation( normalized_fm));
679682
// Get each clause if there are several always disjuncts
680683
auto clauses = get_leaves(normalized_fm, tau_parser::wff_or, tau_parser::wff);
681-
tau<tau_ba<BAs...>,BAs...> res;
684+
tau<tau_ba_t, BAs...> res;
682685
// Convert each disjunct to unbounded continuation
683686
for (auto& clause : clauses) {
684687
if (res) res = build_wff_or(res, build_wff_always(

‎src/satisfiability.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -956,10 +956,10 @@ tau<BAs...> to_unbounded_continuation(const tau<BAs...>& ubd_aw_continuation,
956956

957957
// Assumes a single normalized Tau DNF clause
958958
template<typename... BAs>
959-
nso<BAs...> transform_to_execution(const nso<BAs...>& fm, const bool output = false) {
959+
tau<BAs...> transform_to_execution(const tau<BAs...>& fm, const bool output = false) {
960960
assert(get_dnf_wff_clauses(fm).size() == 1);
961961
#ifdef TAU_CACHE
962-
static std::map<nso<BAs...>, nso<BAs...>> cache;
962+
static std::map<tau<BAs...>, tau<BAs...>> cache;
963963
if (auto it = cache.find(fm); it != cache.end())
964964
return it->second;
965965
#endif

‎src/solver.h

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -684,8 +684,13 @@ std::optional<solution<BAs...>> solve_system(const equation_system<BAs...>& syst
684684

685685
if (!system.first) return solve_inequality_system<BAs...>(system.second, splitter_one);
686686
if (system.second.empty()) return find_solution(system.first.value());
687+
687688
auto phi = lgrs(system.first.value());
688689
if (!phi.has_value()) return {};
690+
// std::cout << "phi\n";
691+
// for (const auto& [var, val] : phi.value())
692+
// std::cout << "var: " << var << ", val: " << val << "\n";
693+
689694
inequality_system<BAs...> inequalities;
690695
// for each inequality g_i we apply the transformation given by lgrs solution
691696
// of the equality
@@ -703,6 +708,10 @@ std::optional<solution<BAs...>> solve_system(const equation_system<BAs...>& syst
703708
else if (ng_i == _T<BAs...>) continue;
704709
inequalities.insert(ng_i);
705710
}
711+
// std::cout << "inequalities:\n";
712+
// for (const auto& el : inequalities) {
713+
// std::cout << "el: " << el << "\n";
714+
// }
706715
// solve the given system of inequalities
707716
auto inequality_solution = solve_inequality_system<BAs...>(inequalities, splitter_one);
708717
if (!inequality_solution.has_value()) {
@@ -714,6 +723,10 @@ std::optional<solution<BAs...>> solve_system(const equation_system<BAs...>& syst
714723

715724
return {};
716725
}
726+
// std::cout << "inequalities solution: \n";
727+
// for (const auto& [var, val] : inequality_solution.value()) {
728+
// std::cout << "var: " << var << ", val: " << val << "\n";
729+
// }
717730
// and finally, apply the solution to lgrs solution to get the final one (ϕ (T)).
718731
// Solutions coming from inequality_solution for variables appearing also
719732
// in the equality part will be replaced in the next step
@@ -787,7 +800,7 @@ std::optional<solution<BAs...>> solve(const tau<BAs...>& form,
787800
BOOST_LOG_TRIVIAL(info) << "(Warning) Skipped clause with temporal quantifier: " << clause;
788801
continue;
789802
}
790-
auto is_equation = [](const nso<BAs...>& n) {
803+
auto is_equation = [](const tau<BAs...>& n) {
791804
return is_child_non_terminal<tau_parser::bf_eq, BAs...>(n)
792805
|| is_child_non_terminal<tau_parser::bf_neq, BAs...>(n);
793806
};

0 commit comments

Comments
 (0)