diff --git a/flamapy/metamodels/bdd_metamodel/transformations/sat_to_bdd.py b/flamapy/metamodels/bdd_metamodel/transformations/sat_to_bdd.py new file mode 100644 index 0000000..2884b39 --- /dev/null +++ b/flamapy/metamodels/bdd_metamodel/transformations/sat_to_bdd.py @@ -0,0 +1,35 @@ +from flamapy.core.transformations import ModelToModel + +from flamapy.metamodels.bdd_metamodel.models import BDDModel +from flamapy.metamodels.pysat_metamodel.models import PySATModel + + +class SATToBDD(ModelToModel): + + @staticmethod + def get_source_extension() -> str: + return 'pysat' + + @staticmethod + def get_destination_extension() -> str: + return 'bdd' + + def __init__(self, source_model: PySATModel) -> None: + self.source_model = source_model + self.destination_model = BDDModel() + + def transform(self) -> BDDModel: + # Transform clauses to textual CNF notation required by the BDD + not_connective = BDDModel.NOT + or_connective = ' ' + BDDModel.OR + ' ' + and_connective = ' ' + BDDModel.AND + ' ' + cnf_list = [] + for clause in self.source_model.get_all_clauses().clauses: + cnf_list.append('(' + or_connective.join(list(map(lambda l: + not_connective + self.source_model.features[abs(l)] if l < 0 else + self.source_model.features[abs(l)], clause))) + ')') + + cnf_formula = and_connective.join(cnf_list) + self.destination_model.from_textual_cnf(cnf_formula, list(self.source_model.variables.keys())) + + return self.destination_model