Skip to content

Latest commit

 

History

History
51 lines (40 loc) · 2.12 KB

File metadata and controls

51 lines (40 loc) · 2.12 KB

CFMToolboxPluginSMTEncoding

SMT Multiset Encoding Variant

Searches for Gaps in the CFM with the multiset approach encoding.

python3 -m cfmtoolbox --import Path-TO-JSON-OF-CFM  run-smt-solver-with-multiset-gap-detection

Return the maximum feature instance cardinality for every feature. This methode uses the multiset encoding.

python3 -m cfmtoolbox --import Path-TO-JSON-OF-CFM  run-smt-solver-with-multiset-maximize-cardinalities

Return the minimum feature instance cardinality for every feature. This methode uses the multiset encoding.

python3 -m cfmtoolbox --import Path-TO-JSON-OF-CFM  run-smt-solver-with-multiset-minimize-cardinalities

SMT Cloning Basic Variant

Searches for Gaps in the CFM with the basic cloning approach encoding.

python3 -m cfmtoolbox --import Path-TO-JSON-OF-CFM  run-smt-solver-with-cloning-base-gap-detection

Return the maximum feature instance cardinality for every feature. This methode uses the basic cloning encoding.

python3 -m cfmtoolbox --import Path-TO-JSON-OF-CFM   run-smt-solver-with-cloning-base-maximize-cardinalities

Return the minimum feature instance cardinality for every feature. This methode uses the basic cloning encoding.

python3 -m cfmtoolbox --import Path-TO-JSON-OF-CFM   run-smt-solver-with-cloning-base-minimize-cardinalities

SMT Cloning with Integer Leaves

Searches for Gaps in the CFM with the cloning approach encoding, where the leave nodes are represented as int constants.

python3 -m cfmtoolbox --import Path-TO-JSON-OF-CFM  run-smt-solver-with-cloning-with-child-int-constants-gap-detection

Return the maximum feature instance cardinality for every feature. This methode uses the cloning encoding with integer leaves.

python3 -m cfmtoolbox --import Path-TO-JSON-OF-CFM   run-smt-solver-with-cloning-with-child-int-constants-maximize-cardinalities

Return the minimum feature instance cardinality for every feature. This methode uses the cloning encoding with integer leaves.

python3 -m cfmtoolbox --import Path-TO-JSON-OF-CFM   run-smt-solver-with-cloning-with-child-int-constants-minimize-cardinalities