alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

aiger: fix forcing of input properties

Browse source 
* spot/twaalgos/aiger.cc: Here.
* tests/python/synthesis.ipynb: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2021-10-07 11:23:51 +02:00
parent 9b3956f892
commit b9a39c5576
2 changed files with 58 additions and 64 deletions
Download patch file Download diff file Expand all files Collapse all files

4
spot/twaalgos/aiger.cc
View file

@ -1872,7 +1872,7 @@ namespace spot
unused_outs.push_back(ao);
for (const auto& ai : ins)
if (!used_aps.count(ai))
unused_outs.push_back(ai);
unused_ins.push_back(ai);
}
// todo Some additional checks?
return auts_to_aiger({{aut, get_synthesis_outputs(aut)}}, mode,
@ -1934,7 +1934,7 @@ namespace spot
unused_outs.push_back(ao);
for (const auto& ai : ins)
if (!used_aps.count(ai))
unused_outs.push_back(ai);
unused_ins.push_back(ai);
return auts_to_aiger(new_vec, mode, unused_ins, unused_outs);
}

116
tests/python/synthesis.ipynb
View file

@ -696,7 +696,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa0f4223360> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8d9c0983f0> >"
]
},
"metadata": {},
@ -2509,7 +2509,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa0f4b39690> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8d9c4f8b10> >"
]
},
"execution_count": 5,
@ -2749,7 +2749,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa0f4b395a0> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8d9c098510> >"
]
},
"execution_count": 6,
@ -2838,7 +2838,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7fa0f4b39b70> >"
"<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f8d9c4f8a80> >"
]
},
"metadata": {},
@ -3056,7 +3056,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa0f4223090> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8d9c098ed0> >"
]
},
"metadata": {},
@ -3133,7 +3133,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7fa0f5be7ed0> >"
"<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f8d9c098d80> >"
]
},
"metadata": {},
@ -3173,27 +3173,27 @@
"<!-- Generated by graphviz version 2.43.0 (0)\n",
" -->\n",
"<!-- Pages: 1 -->\n",
"<svg width=\"344pt\" height=\"352pt\"\n",
" viewBox=\"0.00 0.00 344.50 352.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<svg width=\"328pt\" height=\"352pt\"\n",
" viewBox=\"0.00 0.00 327.70 352.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 348)\">\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-348 340.5,-348 340.5,4 -4,4\"/>\n",
"<!-- 4 -->\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-348 323.7,-348 323.7,4 -4,4\"/>\n",
"<!-- 6 -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>4</title>\n",
"<title>6</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"65,-118 0,-118 0,-82 65,-82 65,-118\"/>\n",
"<text text-anchor=\"middle\" x=\"32.5\" y=\"-96.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0_out</text>\n",
"</g>\n",
"<!-- 6 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>6</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"62.5\" cy=\"-172\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"62.5\" y=\"-168.3\" font-family=\"Times,serif\" font-size=\"14.00\">6</text>\n",
"<!-- 8 -->\n",
"<g id=\"node5\" class=\"node\">\n",
"<title>8</title>\n",
"<ellipse fill=\"none\" stroke=\"black\" cx=\"63.5\" cy=\"-172\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"63.5\" y=\"-168.3\" font-family=\"Times,serif\" font-size=\"14.00\">8</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;6 -->\n",
"<!-- 6&#45;&gt;8 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>4&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M39.92,-118.3C43.66,-127.03 48.25,-137.76 52.32,-147.25\"/>\n",
"<ellipse fill=\"black\" stroke=\"black\" cx=\"54.01\" cy=\"-151.18\" rx=\"4\" ry=\"4\"/>\n",
"<title>6&#45;&gt;8</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M40.16,-118.3C44.12,-127.25 49.01,-138.29 53.29,-147.94\"/>\n",
"<ellipse fill=\"black\" stroke=\"black\" cx=\"54.94\" cy=\"-151.67\" rx=\"4\" ry=\"4\"/>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node2\" class=\"node\">\n",
@ -3201,71 +3201,65 @@
"<polygon fill=\"none\" stroke=\"black\" points=\"93.5,-46 54.51,-11.5 132.49,-11.5 93.5,-46\"/>\n",
"<text text-anchor=\"middle\" x=\"93.5\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i0</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;6 -->\n",
"<!-- 2&#45;&gt;8 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>2&#45;&gt;6</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M89.57,-42.62C84.15,-68.35 74.32,-114.94 68.12,-144.35\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"64.65,-143.84 66.01,-154.35 71.5,-145.28 64.65,-143.84\"/>\n",
"<title>2&#45;&gt;8</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M89.64,-42.92C84.4,-68.61 74.99,-114.68 69.01,-144\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"65.54,-143.48 66.97,-153.98 72.4,-144.88 65.54,-143.48\"/>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>4</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"189.5,-46 150.51,-11.5 228.49,-11.5 189.5,-46\"/>\n",
"<text text-anchor=\"middle\" x=\"189.5\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i1</text>\n",
"</g>\n",
"<!-- L0 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>L0</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"62.5,-262 8.5,-262 8.5,-226 62.5,-226 62.5,-262\"/>\n",
"<text text-anchor=\"middle\" x=\"35.5\" y=\"-240.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0</text>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"63.5,-262 9.5,-262 9.5,-226 63.5,-226 63.5,-262\"/>\n",
"<text text-anchor=\"middle\" x=\"36.5\" y=\"-240.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;L0 -->\n",
"<!-- 8&#45;&gt;L0 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>6&#45;&gt;L0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M56.24,-189.24C53.13,-197.3 49.29,-207.26 45.76,-216.4\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"42.44,-215.29 42.1,-225.88 48.97,-217.81 42.44,-215.29\"/>\n",
"<title>8&#45;&gt;L0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M57.24,-189.24C54.13,-197.3 50.29,-207.26 46.76,-216.4\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"43.44,-215.29 43.1,-225.88 49.97,-217.81 43.44,-215.29\"/>\n",
"</g>\n",
"<!-- o0o0 -->\n",
"<g id=\"node5\" class=\"node\">\n",
"<g id=\"node6\" class=\"node\">\n",
"<title>o0o0</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"90.5,-298 134.89,-332.5 46.11,-332.5 90.5,-298\"/>\n",
"<text text-anchor=\"middle\" x=\"90.5\" y=\"-317.3\" font-family=\"Times,serif\" font-size=\"14.00\">o0</text>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"91.5,-298 135.89,-332.5 47.11,-332.5 91.5,-298\"/>\n",
"<text text-anchor=\"middle\" x=\"91.5\" y=\"-317.3\" font-family=\"Times,serif\" font-size=\"14.00\">o0</text>\n",
"</g>\n",
"<!-- 6&#45;&gt;o0o0 -->\n",
"<!-- 8&#45;&gt;o0o0 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>6&#45;&gt;o0o0:s</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M68.58,-189.32C76.1,-210.91 88.19,-250.57 90.21,-287.63\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"86.72,-288.1 90.5,-298 93.72,-287.91 86.72,-288.1\"/>\n",
"<title>8&#45;&gt;o0o0:s</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M69.58,-189.32C77.1,-210.91 89.19,-250.57 91.21,-287.63\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"87.72,-288.1 91.5,-298 94.72,-287.91 87.72,-288.1\"/>\n",
"</g>\n",
"<!-- o1o1 -->\n",
"<g id=\"node6\" class=\"node\">\n",
"<g id=\"node7\" class=\"node\">\n",
"<title>o1o1</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"196.5,-298 240.89,-332.5 152.11,-332.5 196.5,-298\"/>\n",
"<text text-anchor=\"middle\" x=\"196.5\" y=\"-317.3\" font-family=\"Times,serif\" font-size=\"14.00\">o1</text>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"275.5,-298 319.89,-332.5 231.11,-332.5 275.5,-298\"/>\n",
"<text text-anchor=\"middle\" x=\"275.5\" y=\"-317.3\" font-family=\"Times,serif\" font-size=\"14.00\">o1</text>\n",
"</g>\n",
"<!-- 0 -->\n",
"<g id=\"node7\" class=\"node\">\n",
"<g id=\"node8\" class=\"node\">\n",
"<title>0</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"218.5,-5 276.5,-5 276.5,-41 218.5,-41 218.5,-5\"/>\n",
"<text text-anchor=\"middle\" x=\"247.5\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">Const</text>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"246.5,-5 304.5,-5 304.5,-41 246.5,-41 246.5,-5\"/>\n",
"<text text-anchor=\"middle\" x=\"275.5\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">Const</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;o1o1 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>0&#45;&gt;o1o1:s</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M242.04,-41.1C229.34,-82.44 198.69,-191.49 196.61,-287.82\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"193.11,-287.96 196.5,-298 200.11,-288.04 193.11,-287.96\"/>\n",
"</g>\n",
"<!-- o2i1 -->\n",
"<g id=\"node8\" class=\"node\">\n",
"<title>o2i1</title>\n",
"<polygon fill=\"none\" stroke=\"black\" points=\"297.5,-298 336.49,-332.5 258.51,-332.5 297.5,-298\"/>\n",
"<text text-anchor=\"middle\" x=\"297.5\" y=\"-317.3\" font-family=\"Times,serif\" font-size=\"14.00\">i1</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;o2i1 -->\n",
"<g id=\"edge6\" class=\"edge\">\n",
"<title>0&#45;&gt;o2i1:s</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M252.85,-41.11C265.31,-82.47 295.35,-191.55 297.39,-287.83\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"293.89,-288.04 297.5,-298 300.89,-287.96 293.89,-288.04\"/>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M275.5,-41.31C275.5,-83.11 275.5,-193.09 275.5,-287.99\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"272,-288 275.5,-298 279,-288 272,-288\"/>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/plain": [
"<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7fa0f4223a80> >"
"<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f8d9c5bade0> >"
]
},
"metadata": {},
@ -3424,7 +3418,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7fa0f4223e40> >"
"<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f8d9c4f8a80> >"
]
},
"metadata": {},
@ -3536,7 +3530,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa0f4223c60> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8d9c0720c0> >"
]
},
"execution_count": 14,