wmpy.core.weightsΒΆ

Classes

CNFPreprocessor

Converts nested ORs and ANDs into flat lists of ORs and ANDs, and Implies into Or.

PolarityCNFizer

Implements the Plaisted&Greenbaum CNF conversion algorithm.

WeightAtomsFinder

TODO

WeightConverterSkeleton

This internal class implements the conversion of a weight function into a weight skeleton, as described in "Enhancing SMT-based Weighted Model Integration by structure awareness" (Spallitta et al., 2024).

Weights

This class encodes a piecewise weight function.

WeightsEvaluator

This internal class implements the weight evaluation given a truth assignment to its conditions.