michalhe / amaya Goto Github PK

View Code? Open in Web Editor NEW

5.0 3.0 0.0 2.73 MB

License: Mozilla Public License 2.0

Python 16.73% SMT 83.04% Shell 0.01% Makefile 0.01% TeX 0.20% Dockerfile 0.02%

amaya's Introduction

Amaya

Amaya is an experimental, automata-based linear integer arithmetic (LIA) SMT solver.

Amaya supports two execution backends:

a native backend representing transition symbols explicitly. Slow, but offers more experimentation-oriented features such as tracking the semantics of automaton states.
a high-performance MTBDD-based backend representing transition symbols symbolically using MTBDDs.

Installing

All required dependencies can be found in requirements.txt and a virtual environment with these dependencies is all that is needed to run Amaya using the native (default) backend.

Building the high-performance MTBDD backend

Amaya relies on sylvan providing efficient MTBDD implementation. In order to utilize Sylvan, Amaya implements a C++ library with custom MTBDD leaves and automata algorithms. The python frontend then relies on Python's ctypes module to call Amaya's C++ library.

The following steps need to be performed in order to use the MTBDD-backend:

Compile and install sylvan
Compile Amaya's C++ library.
Make sure the resulting shared object is present in amaya/ folder, so that the ctypes wrapper will be able to find it.

Running

The run-amaya.py script provides a user interface to Amaya. This script is current capable of running Amaya in three modes:

get-sat - single execution of the solver, outputting the SAT value (sat/unsat) of the formula
benchmark - executes and measures the decision procedure runtime (hot-start).
convert - Run Amaya's preprocessor and output the result in different formats. The run-amaya.py script also provides options that can tweak the decision procedure regardless of the execution mode (e.g. enable eager minimization). See ./run-amaya.py --help.

Get-Sat

python3 run-amaya.py get-sat FILE

The get-sat command evaluates the given SMTLIB2 file and reports the results (sat/unsat). This command supports various flags for inspecting the evaluation process such as the export of the automatons created during the evaluation, or writing out the runtime for the individual operations performed during the evaluation etc.

To see a full list of supported switches, see:

python3 run-amaya.py get-sat --help

Example - Exporting the intermediate automata created during evaluation of a TPTP benchmark file

The following command will output the automata created during the decision procedure in the order they were created to the provided folder. The output format of the exported automata can be changed by --output-format.

python3 run-amaya.py --backend MTBDD get-sat --output-created-automata smt-files/tptp/ARI005\=1.smt2

Benchmarks

Run Amaya in the benchmarking mode. This mode requires a set of input files to be specified. See python3 run-amaya.py benchmark --help for information about how to specify the input files.

If the benchmarking runner encounters a file for which the evaluation procedure did yield different results as expected (specified in the file via the smt-info statement) the file will not be rerun and will have its failed field in the report set to True.

To see a full list of supported options, see:

python3 run-amaya.py benchmark --help

Example - Running the TPTP benchmark

The following command benchmarks Amaya to be run for all SMTLIB2 files present in the smt-files/tptp folder (will not be searched recursively). The option --backend naive specifies that the slower, native backend should be used. The option --execute-times 10 specifies that every benchmark file should be run 10 times and the average runtime will be returned.

python3 run-amaya.py --backend naive benchmark --add-directory smt-files/tptp/ --execute-times 10

Convert

Convert formula from SMTLIB2 into various output formats.

Example - Convert SMTLIB2 to the LASH format

The following example converts an SMTLIB2 formula into the LASH format and outputs the result to the stdout.

./run-amaya.py -p no-congruences -p assign-new-var-names -p nonlinear-term-use-two-vars \
    benchmarks/formulae/20190429-UltimateAutomizerSvcomp2019/jain_7_true-unreach-call_true-no-overflow_false-termination.i_10.smt2

Since LASH does not support congruences atoms, Amaya's preprocessor must be instructed to not introduce congruences (-p no-congruences) and rather use inequations. Amaya uses congruences by default, as they offer better runtime characteristics when the moduli in formulae are powers of 2. Furthermore, as some benchmarks might use symbols that cannot be part of variable identifiers in the LASH format, the preprocessor is instructed to drop all of the variable names and introduce new ones (-p assign-new-var-names). Finally, the -p nonlinear-term-use-two-vars causes Amaya's preprocessor to use two fresh quantified variables instead of one, causing the automata manipulated by LASH to be smaller at the cost of having more variables.

amaya's People

Contributors

Stargazers

Watchers

amaya's Issues

Algorithms to implement

List of automata algorithms to implement due to various reasons:

Hopcroft minimization
Hopcroft minimization on MTBDDs

Padding closure algorithm does not account for multiple final states.

As the title suggests the algorithm does not account for the possibility of having multiple final states. Overall improvements in terms of readability should be achieved, when this will be fixed according to the new algorithm documented as a part of my Bachelors T.

SMT-LIB Support

Useful SMT features to support:

: (get-model)

Inconsistent verdict on SMT-LIB queries (compared to z3 and CVC5)

Hi,

I got UNSAT verdicts on the following queries from the SMT-LIB repository (non-incremental/QF-LIA):

20180326-Bromberger/more_slacked/CAV_2009_benchmarks/smt/45-vars/v45_problem_2__003.smt2.slack.smt2
20180326-Bromberger/more_slacked/CAV_2009_benchmarks/smt/45-vars/v45_problem__009.smt2.slack.smt2
20180326-Bromberger/more_slacked/CAV_2009_benchmarks/smt/45-vars/v45_problem__017.smt2.slack.smt2

I compared the results with two SMT solvers (z3 and cvc5) and both returned SAT.

I ran the following command : ./run-amaya.py --fast -O all --verbose get-sat <query.smt2>.

Perhaps I am missing something in the use or configuration of Amaya.

Bellow is the output from Amaya:

[2024/08/19 16:43:01](INFO): Executing evaluation procedure with configuration: SolverConfig(solution_domain=<SolutionDomain.INTEGERS: 1>, minimization_method=<MinimizationAlgorithms.HOPCROFT: 1>, backend_type=<BackendType.MTBDD: 2>, track_operation_runtime=False, track_state_semantics=False, optimizations=OptimizationsConfig(allow_sharding=False, simplify_variable_bounds=True, rewrite_existential_equations_via_gcd=True, push_negation_towards_atoms=True, do_interval_analysis=True, do_light_sat_reasoning=True, do_lazy_evaluation=True, do_miniscoping=True, do_gcd_divide=True, rewrite_congruences_with_unbound_terms=True, detect_isomorphic_conflicts=True, linearize_similar_mod_terms=True, reorder_conjunctions=True, do_interval_reasonining_twice=True, linearize_congruences=True, optimize_bottom_quantifiers=True), vis_display_only_free_vars=False, print_stats=False, preprocessing=PreprocessingConfig(perform_prenexing=False, perform_antiprenexing=False, disambiguate_variables=True, assign_new_variable_names=False, use_congruences_when_rewriting_modulo=True, use_two_vars_when_rewriting_nonlin_terms=False, show_preprocessed_formula=False, display_var_table=False), current_formula_path='/home/nicolas.amat/Presburger-automata/Experimental_Evaluation/non-incremental/QF_LIA/20180326-Bromberger/more_slacked/CAV_2009_benchmarks/smt/45-vars/v45_problem_2__003.smt2.slack.smt2', export_counter=0, disambiguation_scope_separator='_', report_highly_effective_minimizations=False, max_allowed_states=None)
[2024/08/19 16:43:01](INFO): [Preprocessing] Rewriting if-then-else expressions.
[2024/08/19 16:43:01](INFO): First pass stats:
[2024/08/19 16:43:01](INFO): Replaced 0 forall quantifiers with exists.
[2024/08/19 16:43:01](INFO): Expanded 0 implications.
[2024/08/19 16:43:01](INFO): Entering the third preprocessing pass: double negation removal.
[2024/08/19 16:43:01](INFO): Removed 0 negation pairs.
[2024/08/19 16:43:01](INFO): Condensing atomic relation ASTs into AST leaves.
[2024/08/19 16:43:01](INFO): Preprocessing resulted in the following AST: ['and', Relation(-1.Var(id=1) <= 0), Relation(-1.Var(id=2) <= 0), Relation(-1.Var(id=3) <= 0), Relation(-1.Var(id=4) <= 0), Relation(-1.Var(id=5) <= 0), Relation(-1.Var(id=6) <= 0), Relation(-1.Var(id=7) <= 0), Relation(-1.Var(id=8) <= 0), Relation(-1.Var(id=9) <= 0), Relation(-1.Var(id=10) <= 0), Relation(-1.Var(id=11) <= 0), Relation(-1.Var(id=12) <= 0), Relation(-1.Var(id=13) <= 0), Relation(-1.Var(id=14) <= 0), Relation(-1.Var(id=15) <= 0), Relation(-1.Var(id=16) <= 0), Relation(-1.Var(id=17) <= 0), Relation(-1.Var(id=18) <= 0), Relation(-1.Var(id=19) <= 0), Relation(-1.Var(id=20) <= 0), Relation(-1.Var(id=21) <= 0), Relation(-1.Var(id=22) <= 0), Relation(-1.Var(id=23) <= 0), Relation(-1.Var(id=24) <= 0), Relation(-1.Var(id=25) <= 0), Relation(-1.Var(id=26) <= 0), Relation(-1.Var(id=27) <= 0), Relation(-1.Var(id=28) <= 0), Relation(-1.Var(id=29) <= 0), Relation(-1.Var(id=30) <= 0), Relation(-1.Var(id=31) <= 0), Relation(-1.Var(id=32) <= 0), Relation(-1.Var(id=33) <= 0), Relation(-1.Var(id=34) <= 0), Relation(-1.Var(id=35) <= 0), Relation(-1.Var(id=36) <= 0), Relation(-1.Var(id=37) <= 0), Relation(-1.Var(id=38) <= 0), Relation(-1.Var(id=39) <= 0), Relation(-1.Var(id=40) <= 0), Relation(-1.Var(id=41) <= 0), Relation(-1.Var(id=42) <= 0), Relation(-1.Var(id=43) <= 0), Relation(-1.Var(id=44) <= 0), Relation(-1.Var(id=45) <= 0), Relation(-1.Var(id=46) <= 0), Relation(-1.Var(id=47) <= 0), Relation(-1.Var(id=48) <= 0), Relation(-1.Var(id=49) <= 0), Relation(-1.Var(id=50) <= 0), Relation(-1.Var(id=51) <= 0), Relation(-1.Var(id=52) <= 0), Relation(-1.Var(id=53) <= 0), Relation(-1.Var(id=54) <= 0), Relation(-1.Var(id=55) <= 0), Relation(-1.Var(id=56) <= 0), Relation(-1.Var(id=57) <= 0), Relation(-1.Var(id=58) <= 0), Relation(-1.Var(id=59) <= 0), Relation(-1.Var(id=60) <= 0), Relation(-1.Var(id=61) <= 0), Relation(-1.Var(id=62) <= 0), Relation(-1.Var(id=63) <= 0), Relation(-1.Var(id=64) <= 0), Relation(-1.Var(id=65) <= 0), Relation(-1.Var(id=66) <= 0), Relation(-1.Var(id=67) <= 0), Relation(-1.Var(id=68) <= 0), Relation(-1.Var(id=69) <= 0), Relation(-1.Var(id=70) <= 0), Relation(-1.Var(id=71) <= 0), Relation(-1.Var(id=72) <= 0), Relation(-1.Var(id=73) <= 0), Relation(-1.Var(id=74) <= 0), Relation(-1.Var(id=75) <= 0), Relation(-1.Var(id=76) <= 0), Relation(-1.Var(id=77) <= 0), Relation(-1.Var(id=78) <= 0), Relation(-1.Var(id=79) <= 0), Relation(-1.Var(id=80) <= 0), Relation(-1.Var(id=81) <= 0), Relation(-1.Var(id=82) <= 0), Relation(-1.Var(id=83) <= 0), Relation(-1.Var(id=84) <= 0), Relation(-1.Var(id=85) <= 0), Relation(-1.Var(id=86) <= 0), Relation(-1.Var(id=87) <= 0), Relation(-1.Var(id=88) <= 0), Relation(-1.Var(id=89) <= 0), Relation(-1.Var(id=90) <= 0), Relation(+1.Var(id=1) -1.Var(id=2) -1.Var(id=3) +1.Var(id=4) +1.Var(id=5) -1.Var(id=6) +2.Var(id=7) -2.Var(id=8) -1.Var(id=9) +1.Var(id=10) +1.Var(id=11) -1.Var(id=12) +1.Var(id=13) -1.Var(id=14) +1.Var(id=15) -1.Var(id=16) -1.Var(id=17) +1.Var(id=18) -1.Var(id=19) +1.Var(id=20) -1.Var(id=21) +1.Var(id=22) -1.Var(id=23) +1.Var(id=24) -1.Var(id=25) +1.Var(id=26) +1.Var(id=27) -1.Var(id=28) +1.Var(id=29) -1.Var(id=30) +1.Var(id=31) -1.Var(id=32) -1.Var(id=33) +1.Var(id=34) -1.Var(id=35) +1.Var(id=36) +1.Var(id=37) -1.Var(id=38) +1.Var(id=39) -1.Var(id=40) <= -1), Relation(+1.Var(id=1) -1.Var(id=2) +1.Var(id=3) -1.Var(id=4) +2.Var(id=15) -2.Var(id=16) +1.Var(id=23) -1.Var(id=24) +1.Var(id=27) -1.Var(id=28) +1.Var(id=31) -1.Var(id=32) -1.Var(id=35) +1.Var(id=36) +2.Var(id=37) -2.Var(id=38) +1.Var(id=39) -1.Var(id=40) +1.Var(id=41) -1.Var(id=42) -1.Var(id=43) +1.Var(id=44) +1.Var(id=45) -1.Var(id=46) -1.Var(id=47) +1.Var(id=48) -1.Var(id=49) +1.Var(id=50) -1.Var(id=51) +1.Var(id=52) +1.Var(id=53) -1.Var(id=54) -1.Var(id=55) +1.Var(id=56) -1.Var(id=57) +1.Var(id=58) -1.Var(id=59) +1.Var(id=60) +1.Var(id=61) -1.Var(id=62) <= 0), Relation(+1.Var(id=1) -1.Var(id=2) +1.Var(id=3) -1.Var(id=4) -1.Var(id=5) +1.Var(id=6) -1.Var(id=7) +1.Var(id=8) -1.Var(id=11) +1.Var(id=12) +2.Var(id=15) -2.Var(id=16) -1.Var(id=19) +1.Var(id=20) -1.Var(id=21) +1.Var(id=22) +2.Var(id=27) -2.Var(id=28) +1.Var(id=35) -1.Var(id=36) -1.Var(id=39) +1.Var(id=40) +1.Var(id=47) -1.Var(id=48) -1.Var(id=49) +1.Var(id=50) -1.Var(id=55) +1.Var(id=56) +1.Var(id=61) -1.Var(id=62) +1.Var(id=63) -1.Var(id=64) -1.Var(id=65) +1.Var(id=66) -1.Var(id=67) +1.Var(id=68) -1.Var(id=69) +1.Var(id=70) <= 0), Relation(+1.Var(id=5) -1.Var(id=6) -1.Var(id=17) +1.Var(id=18) -1.Var(id=23) +1.Var(id=24) +1.Var(id=25) -1.Var(id=26) +1.Var(id=33) -1.Var(id=34) +1.Var(id=35) -1.Var(id=36) +1.Var(id=37) -1.Var(id=38) -2.Var(id=39) +2.Var(id=40) +1.Var(id=41) -1.Var(id=42) -1.Var(id=43) +1.Var(id=44) +2.Var(id=47) -2.Var(id=48) +1.Var(id=59) -1.Var(id=60) -1.Var(id=61) +1.Var(id=62) +4.Var(id=65) -4.Var(id=66) +1.Var(id=69) -1.Var(id=70) -1.Var(id=71) +1.Var(id=72) -1.Var(id=73) +1.Var(id=74) -2.Var(id=75) +2.Var(id=76) -1.Var(id=77) +1.Var(id=78) <= -1), Relation(-1.Var(id=1) +1.Var(id=2) -2.Var(id=3) +2.Var(id=4) +1.Var(id=9) -1.Var(id=10) -2.Var(id=13) +2.Var(id=14) -2.Var(id=17) +2.Var(id=18) +1.Var(id=19) -1.Var(id=20) +1.Var(id=23) -1.Var(id=24) +1.Var(id=27) -1.Var(id=28) +1.Var(id=33) -1.Var(id=34) -1.Var(id=37) +1.Var(id=38) +2.Var(id=39) -2.Var(id=40) +1.Var(id=43) -1.Var(id=44) -1.Var(id=53) +1.Var(id=54) -1.Var(id=57) +1.Var(id=58) -1.Var(id=61) +1.Var(id=62) +1.Var(id=77) -1.Var(id=78) +1.Var(id=79) -1.Var(id=80) +1.Var(id=81) -1.Var(id=82) <= -1), Relation(+1.Var(id=7) -1.Var(id=8) -1.Var(id=11) +1.Var(id=12) +1.Var(id=13) -1.Var(id=14) +1.Var(id=17) -1.Var(id=18) -1.Var(id=21) +1.Var(id=22) +1.Var(id=23) -1.Var(id=24) -1.Var(id=25) +1.Var(id=26) -1.Var(id=27) +1.Var(id=28) -1.Var(id=33) +1.Var(id=34) +1.Var(id=35) -1.Var(id=36) -1.Var(id=37) +1.Var(id=38) +1.Var(id=41) -1.Var(id=42) +1.Var(id=47) -1.Var(id=48) +1.Var(id=49) -1.Var(id=50) -1.Var(id=71) +1.Var(id=72) -2.Var(id=73) +2.Var(id=74) +1.Var(id=79) -1.Var(id=80) <= 0), Relation(-1.Var(id=9) +1.Var(id=10) -1.Var(id=15) +1.Var(id=16) -1.Var(id=17) +1.Var(id=18) -1.Var(id=19) +1.Var(id=20) +1.Var(id=21) -1.Var(id=22) +1.Var(id=37) -1.Var(id=38) +1.Var(id=41) -1.Var(id=42) +1.Var(id=49) -1.Var(id=50) +1.Var(id=51) -1.Var(id=52) +2.Var(id=53) -2.Var(id=54) +2.Var(id=59) -2.Var(id=60) -1.Var(id=61) +1.Var(id=62) +2.Var(id=73) -2.Var(id=74) -1.Var(id=75) +1.Var(id=76) +2.Var(id=83) -2.Var(id=84) -1.Var(id=85) +1.Var(id=86) <= 0), Relation(-1.Var(id=1) +1.Var(id=2) +2.Var(id=5) -2.Var(id=6) +2.Var(id=11) -2.Var(id=12) +1.Var(id=19) -1.Var(id=20) +1.Var(id=25) -1.Var(id=26) +1.Var(id=31) -1.Var(id=32) +1.Var(id=33) -1.Var(id=34) -1.Var(id=39) +1.Var(id=40) +2.Var(id=43) -2.Var(id=44) +1.Var(id=45) -1.Var(id=46) +1.Var(id=63) -1.Var(id=64) +1.Var(id=67) -1.Var(id=68) -1.Var(id=71) +1.Var(id=72) -1.Var(id=81) +1.Var(id=82) -1.Var(id=83) +1.Var(id=84) -2.Var(id=87) +2.Var(id=88) <= -1), Relation(-2.Var(id=5) +2.Var(id=6) +2.Var(id=7) -2.Var(id=8) +1.Var(id=9) -1.Var(id=10) +1.Var(id=11) -1.Var(id=12) -1.Var(id=15) +1.Var(id=16) -2.Var(id=29) +2.Var(id=30) +1.Var(id=37) -1.Var(id=38) +1.Var(id=45) -1.Var(id=46) -1.Var(id=51) +1.Var(id=52) +1.Var(id=57) -1.Var(id=58) +1.Var(id=59) -1.Var(id=60) -1.Var(id=69) +1.Var(id=70) +1.Var(id=73) -1.Var(id=74) +1.Var(id=75) -1.Var(id=76) -1.Var(id=79) +1.Var(id=80) +1.Var(id=81) -1.Var(id=82) <= 1), Relation(-1.Var(id=1) +1.Var(id=2) +1.Var(id=3) -1.Var(id=4) -1.Var(id=7) +1.Var(id=8) -2.Var(id=9) +2.Var(id=10) +1.Var(id=15) -1.Var(id=16) -1.Var(id=21) +1.Var(id=22) +1.Var(id=23) -1.Var(id=24) -1.Var(id=27) +1.Var(id=28) -1.Var(id=39) +1.Var(id=40) +1.Var(id=45) -1.Var(id=46) +1.Var(id=49) -1.Var(id=50) -1.Var(id=51) +1.Var(id=52) +1.Var(id=69) -1.Var(id=70) -1.Var(id=81) +1.Var(id=82) +2.Var(id=85) -2.Var(id=86) <= 0), Relation(+1.Var(id=1) -1.Var(id=2) -1.Var(id=9) +1.Var(id=10) +1.Var(id=13) -1.Var(id=14) -2.Var(id=17) +2.Var(id=18) -1.Var(id=23) +1.Var(id=24) -1.Var(id=27) +1.Var(id=28) -1.Var(id=29) +1.Var(id=30) -1.Var(id=51) +1.Var(id=52) +1.Var(id=63) -1.Var(id=64) +1.Var(id=65) -1.Var(id=66) -1.Var(id=67) +1.Var(id=68) +1.Var(id=69) -1.Var(id=70) +1.Var(id=79) -1.Var(id=80) -1.Var(id=81) +1.Var(id=82) <= 0), Relation(+1.Var(id=13) -1.Var(id=14) +1.Var(id=17) -1.Var(id=18) +1.Var(id=21) -1.Var(id=22) -1.Var(id=23) +1.Var(id=24) -1.Var(id=25) +1.Var(id=26) -1.Var(id=35) +1.Var(id=36) -1.Var(id=37) +1.Var(id=38) +1.Var(id=49) -1.Var(id=50) +1.Var(id=55) -1.Var(id=56) -2.Var(id=59) +2.Var(id=60) -1.Var(id=67) +1.Var(id=68) -1.Var(id=69) +1.Var(id=70) +1.Var(id=81) -1.Var(id=82) +1.Var(id=83) -1.Var(id=84) <= 0), Relation(-1.Var(id=3) +1.Var(id=4) +2.Var(id=7) -2.Var(id=8) -1.Var(id=9) +1.Var(id=10) +2.Var(id=25) -2.Var(id=26) +1.Var(id=31) -1.Var(id=32) +1.Var(id=35) -1.Var(id=36) -1.Var(id=39) +1.Var(id=40) -1.Var(id=47) +1.Var(id=48) -1.Var(id=59) +1.Var(id=60) +1.Var(id=63) -1.Var(id=64) -1.Var(id=75) +1.Var(id=76) +1.Var(id=85) -1.Var(id=86) +1.Var(id=89) -1.Var(id=90) <= 1), Relation(+1.Var(id=1) -1.Var(id=2) -1.Var(id=5) +1.Var(id=6) +1.Var(id=9) -1.Var(id=10) -1.Var(id=11) +1.Var(id=12) +1.Var(id=13) -1.Var(id=14) -1.Var(id=17) +1.Var(id=18) -1.Var(id=19) +1.Var(id=20) -2.Var(id=25) +2.Var(id=26) -1.Var(id=27) +1.Var(id=28) -1.Var(id=35) +1.Var(id=36) -1.Var(id=37) +1.Var(id=38) +1.Var(id=45) -1.Var(id=46) -1.Var(id=49) +1.Var(id=50) +1.Var(id=55) -1.Var(id=56) +1.Var(id=57) -1.Var(id=58) -1.Var(id=59) +1.Var(id=60) -1.Var(id=63) +1.Var(id=64) +1.Var(id=65) -1.Var(id=66) -2.Var(id=77) +2.Var(id=78) +1.Var(id=79) -1.Var(id=80) -1.Var(id=85) +1.Var(id=86) <= 0), Relation(-1.Var(id=3) +1.Var(id=4) -1.Var(id=5) +1.Var(id=6) -2.Var(id=7) +2.Var(id=8) +2.Var(id=11) -2.Var(id=12) -1.Var(id=13) +1.Var(id=14) -1.Var(id=17) +1.Var(id=18) +1.Var(id=21) -1.Var(id=22) -1.Var(id=23) +1.Var(id=24) +1.Var(id=33) -1.Var(id=34) -1.Var(id=39) +1.Var(id=40) -1.Var(id=43) +1.Var(id=44) -1.Var(id=47) +1.Var(id=48) +1.Var(id=49) -1.Var(id=50) -1.Var(id=53) +1.Var(id=54) +1.Var(id=55) -1.Var(id=56) +1.Var(id=61) -1.Var(id=62) -1.Var(id=67) +1.Var(id=68) -1.Var(id=83) +1.Var(id=84) +1.Var(id=85) -1.Var(id=86) +1.Var(id=89) -1.Var(id=90) <= -1), Relation(-1.Var(id=1) +1.Var(id=2) +1.Var(id=3) -1.Var(id=4) +1.Var(id=9) -1.Var(id=10) +1.Var(id=11) -1.Var(id=12) +1.Var(id=13) -1.Var(id=14) -2.Var(id=17) +2.Var(id=18) -1.Var(id=19) +1.Var(id=20) -1.Var(id=21) +1.Var(id=22) +1.Var(id=23) -1.Var(id=24) -2.Var(id=25) +2.Var(id=26) +1.Var(id=35) -1.Var(id=36) +1.Var(id=39) -1.Var(id=40) -1.Var(id=41) +1.Var(id=42) -1.Var(id=47) +1.Var(id=48) +1.Var(id=55) -1.Var(id=56) -1.Var(id=59) +1.Var(id=60) -1.Var(id=65) +1.Var(id=66) -1.Var(id=67) +1.Var(id=68) +2.Var(id=87) -2.Var(id=88) <= -1), Relation(-1.Var(id=1) +1.Var(id=2) +1.Var(id=5) -1.Var(id=6) -1.Var(id=9) +1.Var(id=10) +1.Var(id=21) -1.Var(id=22) -1.Var(id=23) +1.Var(id=24) -1.Var(id=27) +1.Var(id=28) -2.Var(id=31) +2.Var(id=32) +1.Var(id=33) -1.Var(id=34) +1.Var(id=35) -1.Var(id=36) +1.Var(id=37) -1.Var(id=38) -1.Var(id=39) +1.Var(id=40) +1.Var(id=55) -1.Var(id=56) -1.Var(id=57) +1.Var(id=58) -1.Var(id=79) +1.Var(id=80) -1.Var(id=83) +1.Var(id=84) +1.Var(id=87) -1.Var(id=88) <= 0), Relation(+1.Var(id=11) -1.Var(id=12) +1.Var(id=13) -1.Var(id=14) +1.Var(id=15) -1.Var(id=16) +1.Var(id=19) -1.Var(id=20) -1.Var(id=21) +1.Var(id=22) -2.Var(id=23) +2.Var(id=24) -1.Var(id=27) +1.Var(id=28) +1.Var(id=37) -1.Var(id=38) -1.Var(id=43) +1.Var(id=44) -1.Var(id=49) +1.Var(id=50) -1.Var(id=55) +1.Var(id=56) +2.Var(id=59) -2.Var(id=60) +1.Var(id=63) -1.Var(id=64) +1.Var(id=67) -1.Var(id=68) -1.Var(id=69) +1.Var(id=70) +1.Var(id=89) -1.Var(id=90) <= -1), Relation(-1.Var(id=7) +1.Var(id=8) +1.Var(id=11) -1.Var(id=12) -1.Var(id=21) +1.Var(id=22) -1.Var(id=25) +1.Var(id=26) +1.Var(id=29) -1.Var(id=30) -1.Var(id=31) +1.Var(id=32) -1.Var(id=37) +1.Var(id=38) -1.Var(id=39) +1.Var(id=40) -1.Var(id=45) +1.Var(id=46) -1.Var(id=51) +1.Var(id=52) -1.Var(id=55) +1.Var(id=56) -1.Var(id=69) +1.Var(id=70) -1.Var(id=73) +1.Var(id=74) +2.Var(id=79) -2.Var(id=80) -1.Var(id=89) +1.Var(id=90) <= 1), Relation(+1.Var(id=5) -1.Var(id=6) +2.Var(id=11) -2.Var(id=12) -1.Var(id=13) +1.Var(id=14) +1.Var(id=25) -1.Var(id=26) +4.Var(id=31) -4.Var(id=32) -1.Var(id=35) +1.Var(id=36) -1.Var(id=37) +1.Var(id=38) +1.Var(id=47) -1.Var(id=48) -1.Var(id=59) +1.Var(id=60) -1.Var(id=67) +1.Var(id=68) -1.Var(id=71) +1.Var(id=72) +1.Var(id=77) -1.Var(id=78) +1.Var(id=81) -1.Var(id=82) -1.Var(id=85) +1.Var(id=86) <= 0)]
[2024/08/19 16:43:01](INFO): Setup done. Proceeding to AST evaluation (backend: MTBDD).
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=2, automaton_id=0), operation_id=0, runtime_ns=0)
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=2, automaton_id=1), operation_id=1, runtime_ns=0)
[2024/08/19 16:43:01](INFO): Performing intersection of two automata of size 2 and 2
[2024/08/19 16:43:01](INFO): Intersection done: result size=4, left operand size: 2 , right operand size: 2
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_INTERSECT: 'intersection'>, operand1=AutomatonInfo(size=2, automaton_id=0), operand2=AutomatonInfo(size=2, automaton_id=1), output=AutomatonInfo(size=4, automaton_id=2), operation_id=2, runtime_ns=0)
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_DETERMINIZE: 'determinize'>, operand1=AutomatonInfo(size=4, automaton_id=2), operand2=None, output=AutomatonInfo(size=3, automaton_id=3), operation_id=3, runtime_ns=0)
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Entering minimization routine - serializing data.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Serialisation done.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Minimizing.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Done.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Exiting minimization routine
[2024/08/19 16:43:01](INFO): Minimization applied - inputs has 3 states, result 3.
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.MINIMIZE: 'minimization'>, operand1=AutomatonInfo(size=4, automaton_id=2), operand2=None, output=AutomatonInfo(size=3, automaton_id=4), operation_id=4, runtime_ns=0)
[2024/08/19 16:43:01](INFO):  >> ParsingOperation.NFA_INTERSECT(lhs, rhs) (result size: 3, automaton_type=2)
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=5, automaton_id=5), operation_id=5, runtime_ns=0)
[2024/08/19 16:43:01](INFO): Performing intersection of two automata of size 3 and 5
[2024/08/19 16:43:01](INFO): Intersection done: result size=11, left operand size: 3 , right operand size: 5
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_INTERSECT: 'intersection'>, operand1=AutomatonInfo(size=3, automaton_id=4), operand2=AutomatonInfo(size=5, automaton_id=5), output=AutomatonInfo(size=11, automaton_id=6), operation_id=6, runtime_ns=0)
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_DETERMINIZE: 'determinize'>, operand1=AutomatonInfo(size=11, automaton_id=6), operand2=None, output=AutomatonInfo(size=14, automaton_id=7), operation_id=7, runtime_ns=0)
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Entering minimization routine - serializing data.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Serialisation done.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Minimizing.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Done.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Exiting minimization routine
[2024/08/19 16:43:01](INFO): Minimization applied - inputs has 14 states, result 5.
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.MINIMIZE: 'minimization'>, operand1=AutomatonInfo(size=11, automaton_id=6), operand2=None, output=AutomatonInfo(size=5, automaton_id=8), operation_id=8, runtime_ns=0)
[2024/08/19 16:43:01](INFO):  >> ParsingOperation.NFA_INTERSECT(lhs, rhs) (result size: 5, automaton_type=2)
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=15, automaton_id=9), operation_id=9, runtime_ns=0)
[2024/08/19 16:43:01](INFO): Performing intersection of two automata of size 5 and 15
[2024/08/19 16:43:01](INFO): Intersection done: result size=41, left operand size: 5 , right operand size: 15
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_INTERSECT: 'intersection'>, operand1=AutomatonInfo(size=5, automaton_id=8), operand2=AutomatonInfo(size=15, automaton_id=9), output=AutomatonInfo(size=41, automaton_id=10), operation_id=10, runtime_ns=0)
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_DETERMINIZE: 'determinize'>, operand1=AutomatonInfo(size=41, automaton_id=10), operand2=None, output=AutomatonInfo(size=61, automaton_id=11), operation_id=11, runtime_ns=0)
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Entering minimization routine - serializing data.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Serialisation done.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Minimizing.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Done.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Exiting minimization routine
[2024/08/19 16:43:01](INFO): Minimization applied - inputs has 61 states, result 11.
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.MINIMIZE: 'minimization'>, operand1=AutomatonInfo(size=41, automaton_id=10), operand2=None, output=AutomatonInfo(size=11, automaton_id=12), operation_id=12, runtime_ns=0)
[2024/08/19 16:43:01](INFO):  >> ParsingOperation.NFA_INTERSECT(lhs, rhs) (result size: 11, automaton_type=2)
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=11, automaton_id=13), operation_id=13, runtime_ns=0)
[2024/08/19 16:43:01](INFO): Performing intersection of two automata of size 11 and 11
[2024/08/19 16:43:01](INFO): Intersection done: result size=61, left operand size: 11 , right operand size: 11
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_INTERSECT: 'intersection'>, operand1=AutomatonInfo(size=11, automaton_id=12), operand2=AutomatonInfo(size=11, automaton_id=13), output=AutomatonInfo(size=61, automaton_id=14), operation_id=14, runtime_ns=0)
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_DETERMINIZE: 'determinize'>, operand1=AutomatonInfo(size=61, automaton_id=14), operand2=None, output=AutomatonInfo(size=79, automaton_id=15), operation_id=15, runtime_ns=0)
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Entering minimization routine - serializing data.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Serialisation done.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Minimizing.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Done.
[2024/08/19 16:43:01](INFO): [MTBDD Hopcroft minimization] Exiting minimization routine
[2024/08/19 16:43:01](INFO): Minimization applied - inputs has 79 states, result 21.
[2024/08/19 16:43:01](INFO): Operation finished: StatPoint(operation=<ParsingOperation.MINIMIZE: 'minimization'>, operand1=AutomatonInfo(size=61, automaton_id=14), operand2=None, output=AutomatonInfo(size=21, automaton_id=16), operation_id=16, runtime_ns=0)
[2024/08/19 16:43:01](INFO):  >> ParsingOperation.NFA_INTERSECT(lhs, rhs) (result size: 21, automaton_type=2)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=17, automaton_id=17), operation_id=17, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Performing intersection of two automata of size 21 and 17
[2024/08/19 16:43:02](INFO): Intersection done: result size=115, left operand size: 21 , right operand size: 17
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_INTERSECT: 'intersection'>, operand1=AutomatonInfo(size=21, automaton_id=16), operand2=AutomatonInfo(size=17, automaton_id=17), output=AutomatonInfo(size=115, automaton_id=18), operation_id=18, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_DETERMINIZE: 'determinize'>, operand1=AutomatonInfo(size=115, automaton_id=18), operand2=None, output=AutomatonInfo(size=159, automaton_id=19), operation_id=19, runtime_ns=0)
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Entering minimization routine - serializing data.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Serialisation done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Minimizing.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Exiting minimization routine
[2024/08/19 16:43:02](INFO): Minimization applied - inputs has 159 states, result 21.
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.MINIMIZE: 'minimization'>, operand1=AutomatonInfo(size=115, automaton_id=18), operand2=None, output=AutomatonInfo(size=21, automaton_id=20), operation_id=20, runtime_ns=0)
[2024/08/19 16:43:02](INFO):  >> ParsingOperation.NFA_INTERSECT(lhs, rhs) (result size: 21, automaton_type=2)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=3, automaton_id=21), operation_id=21, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Performing intersection of two automata of size 21 and 3
[2024/08/19 16:43:02](INFO): Intersection done: result size=47, left operand size: 21 , right operand size: 3
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_INTERSECT: 'intersection'>, operand1=AutomatonInfo(size=21, automaton_id=20), operand2=AutomatonInfo(size=3, automaton_id=21), output=AutomatonInfo(size=47, automaton_id=22), operation_id=22, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_DETERMINIZE: 'determinize'>, operand1=AutomatonInfo(size=47, automaton_id=22), operand2=None, output=AutomatonInfo(size=45, automaton_id=23), operation_id=23, runtime_ns=0)
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Entering minimization routine - serializing data.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Serialisation done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Minimizing.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Exiting minimization routine
[2024/08/19 16:43:02](INFO): Minimization applied - inputs has 45 states, result 21.
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.MINIMIZE: 'minimization'>, operand1=AutomatonInfo(size=47, automaton_id=22), operand2=None, output=AutomatonInfo(size=21, automaton_id=24), operation_id=24, runtime_ns=0)
[2024/08/19 16:43:02](INFO):  >> ParsingOperation.NFA_INTERSECT(lhs, rhs) (result size: 21, automaton_type=2)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=7, automaton_id=25), operation_id=25, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Performing intersection of two automata of size 21 and 7
[2024/08/19 16:43:02](INFO): Intersection done: result size=47, left operand size: 21 , right operand size: 7
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_INTERSECT: 'intersection'>, operand1=AutomatonInfo(size=21, automaton_id=24), operand2=AutomatonInfo(size=7, automaton_id=25), output=AutomatonInfo(size=47, automaton_id=26), operation_id=26, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_DETERMINIZE: 'determinize'>, operand1=AutomatonInfo(size=47, automaton_id=26), operand2=None, output=AutomatonInfo(size=34, automaton_id=27), operation_id=27, runtime_ns=0)
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Entering minimization routine - serializing data.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Serialisation done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Minimizing.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Exiting minimization routine
[2024/08/19 16:43:02](INFO): Minimization applied - inputs has 34 states, result 21.
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.MINIMIZE: 'minimization'>, operand1=AutomatonInfo(size=47, automaton_id=26), operand2=None, output=AutomatonInfo(size=21, automaton_id=28), operation_id=28, runtime_ns=0)
[2024/08/19 16:43:02](INFO):  >> ParsingOperation.NFA_INTERSECT(lhs, rhs) (result size: 21, automaton_type=2)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=3, automaton_id=29), operation_id=29, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Performing intersection of two automata of size 21 and 3
[2024/08/19 16:43:02](INFO): Intersection done: result size=43, left operand size: 21 , right operand size: 3
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_INTERSECT: 'intersection'>, operand1=AutomatonInfo(size=21, automaton_id=28), operand2=AutomatonInfo(size=3, automaton_id=29), output=AutomatonInfo(size=43, automaton_id=30), operation_id=30, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_DETERMINIZE: 'determinize'>, operand1=AutomatonInfo(size=43, automaton_id=30), operand2=None, output=AutomatonInfo(size=26, automaton_id=31), operation_id=31, runtime_ns=0)
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Entering minimization routine - serializing data.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Serialisation done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Minimizing.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Exiting minimization routine
[2024/08/19 16:43:02](INFO): Minimization applied - inputs has 26 states, result 21.
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.MINIMIZE: 'minimization'>, operand1=AutomatonInfo(size=43, automaton_id=30), operand2=None, output=AutomatonInfo(size=21, automaton_id=32), operation_id=32, runtime_ns=0)
[2024/08/19 16:43:02](INFO):  >> ParsingOperation.NFA_INTERSECT(lhs, rhs) (result size: 21, automaton_type=2)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.BUILD_NFA_FROM_INEQ: 'build_nfa_from_ineq'>, operand1=None, operand2=None, output=AutomatonInfo(size=11, automaton_id=33), operation_id=33, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Performing intersection of two automata of size 21 and 11
[2024/08/19 16:43:02](INFO): Intersection done: result size=31, left operand size: 21 , right operand size: 11
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_INTERSECT: 'intersection'>, operand1=AutomatonInfo(size=21, automaton_id=32), operand2=AutomatonInfo(size=11, automaton_id=33), output=AutomatonInfo(size=31, automaton_id=34), operation_id=34, runtime_ns=0)
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.NFA_DETERMINIZE: 'determinize'>, operand1=AutomatonInfo(size=31, automaton_id=34), operand2=None, output=AutomatonInfo(size=39, automaton_id=35), operation_id=35, runtime_ns=0)
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Entering minimization routine - serializing data.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Serialisation done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Minimizing.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Done.
[2024/08/19 16:43:02](INFO): [MTBDD Hopcroft minimization] Exiting minimization routine
[2024/08/19 16:43:02](INFO): Minimization applied - inputs has 39 states, result 0.
[2024/08/19 16:43:02](INFO): Operation finished: StatPoint(operation=<ParsingOperation.MINIMIZE: 'minimization'>, operand1=AutomatonInfo(size=31, automaton_id=34), operand2=None, output=AutomatonInfo(size=0, automaton_id=36), operation_id=36, runtime_ns=0)
[2024/08/19 16:43:02](INFO):  >> ParsingOperation.NFA_INTERSECT(lhs, rhs) (result size: 0, automaton_type=2)
[2024/08/19 16:43:02](INFO): The SAT value of the result automaton is unsat
unsat

Following the corresponding query in the SMT-LIB format: v45_problem_2__003.smt2.slack.smt2.txt.

Best regards,
Nicolas

Refactoring

This issue is for collecting various refactoring tasks that need to be performed

Remove the automaton_id field from mtbdd_automata, mtbdd_transitions (including the C++ backend)
Move *automatons.py to *automata.py

Backlog

Move presburger expr into relations_structures
Fix typo in modulo term "coeficients -> coefficients"
Fix typo in relation "coeficients -> coefficients"

Recommend Projects

React

A declarative, efficient, and flexible JavaScript library for building user interfaces.
Vue.js

🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
TensorFlow

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
D3

Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

javascript

JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
web

Some thing interesting about web. New door for the world.
server

A server is a program made to process requests and deliver data to clients.
Machine learning

Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.