Commit f3310efc authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] Test: separation of sol2 text/dimacs => easier to debug

parent dfcc568b
......@@ -522,14 +522,14 @@ def test_init_forward_unfolding_solution_1_dimacs(feed_mclanalyser, numeric_prop
# [[13]], [[12]], [[3]]
query.dim_start, query.dim_inv, query.dim_final = numeric_properties[0]
mcla.unfolder.init_with_query(query)
init_forward_unfolding_solution_1(mcla)
init_forward_unfolding_solution_1(mcla, dimacs_check=False)
## Search solutions
solutions = tuple(mcla.mac_search(query, 3))
assert solutions == ()
def test_init_forward_unfolding_solution_2(feed_mclanalyser, textual_properties, numeric_properties):
def test_init_forward_unfolding_solution_2_text(feed_mclanalyser, textual_properties):
"""
Query:
start, invariant, final: ("", "L", "C and K")
......@@ -552,6 +552,15 @@ def test_init_forward_unfolding_solution_2(feed_mclanalyser, textual_properties,
assert solutions[0].activated_frontier == {"I", "E", "D", "F", "L"}
def test_init_forward_unfolding_solution_2_dimacs(feed_mclanalyser, numeric_properties):
"""
Query:
dim_start, dim_inv, dim_final = [], [[12]], [[3, -47], [11, -47], [-3, -11, 47], [47]]
DIMACS equiv of: start, invariant, final: ("", "L", "C and K")
Solution: D E F I L
"""
mcla = feed_mclanalyser
### DIMACS properties
# "C and K" property requires an auxiliary literal which can only be added
# from the textual version of this property.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment