Skip to content

Latest commit

 

History

History
819 lines (682 loc) · 35.3 KB

doc.md

File metadata and controls

819 lines (682 loc) · 35.3 KB

TheoryDD

This is the documentation for the theorydd python package.

Overview

This package allows you to compile SMT formulas into Decision Diagrams and dDNNF equivalent formulas.
This package was developed for python version 3.10, compatibility with different versions of python is not guaranteed.
This package also expects to be used in a Linux environment, therefore compatibility with any other OS is not guaranteed: this package is currently Linux only.
Currently, this package allows compilation into BDDs, SDDs and d-DNNF, but compilation into different target languages can be achieved by extending the correct interface.
A limitation of this package is that the pysmt package is used for managing SMT formulas, which means that this package is only compatible with SMT formulas that are supported by pysmt.

Installing

This package uses some dependencies that require cython compilation before being ready to use. This makes the installation process slightly harder than simply installing the package through a pip one-liner.
To install the package, first install the dd dependency as follows:

    pip install --upgrade wheel cython
    export DD_FETCH=1 DD_CUDD=1
    pip install dd=0.5.7 -vvv --use-pep517 --no-build-isolation

You can check that the dependency is installed correctly if the following command does not give you ant errors:

    python -c 'import dd.cudd'

Now you can install the theorydd package (this package) directly from this repository using pip:

    pip install theorydd@git+https://github.com/MaxMicheluttiUnitn/TheoryConsistentDecisionDiagrams@main

After the package and all the depemdencies have been installed, use the pysmt-install tool to install the MathSAT SMT-solver. This tool is automatically installed when pysmt is first installed on your machine.
IMPORTANT: In case you are installing this package inside a python virtual environment, install the solver in a subfolder of the virtual environment by adding the option --install-path YOUR_VENV_FOLDER/solvers

    pysmt-install --msat

Now the installation process should be complete, and you can check that everything is installed correctly with the following command:

    python -c "from theorydd.theory_bdd import TheoryBDD as TBDD; import theorydd.formula as f; TBDD(f.default_phi())"

If this command does not raise any error, than the package is ready for use.

Installing binaries

Some modules of this package require a binary to be executed to work correctly. These binaries do not come with the package at installation time and must be installed by the user.
To facilitate this operation, this package comes with a command theorydd_install which allows for easy installing of the required binaries.
The theorydd_install command takes 3 optional arguments:

  • --tabular: installs the tabularSMT solver binary and grants it execution permissions
  • --c2d: installs the c2d d-DNNF compiler and grants it execution permissions
  • --d4: installs the D4 d-DNNF compiler and grants it execution permissions

The following example will try to install all the binaries on your machine:

theorydd_install --tabular --c2d --d4

In alternative, the binaries can be manually installed in the correct location by the user. The folder structure must be as shown below, otherwise the binaries will not be found during execution.
Remember to grant execution privileges (chmod +x) to the binaries before using them.

-theorydd
 |-abstractdd
 | L...
 |-bin
 | |-c2d
 | | L-c2d_linux
 | |-d4
 | | L-d4.bin
 | |-tabular
 | L L-tabularAllSMT.bin
 |-ddnnf
 | L...
 L ...

Constants

All constants for this package are defined inside the constants.py module.
The constant list VALID_SOLVERS contains all valid strings refering to a solver contained in this package.
The constant list VALIC_VTREE contains all valid configuration type for building V-trees for SDDs.

SMT Enumerators

SMTEnumerators are classes that inherit from the abstract class SMTEnumerator and override all the abstract methods defined into it. These classes are defined here.
Furthermore, a module lemma extractor containing some useful functions for enumeration is also defined there.
Available classes and modules:

SMTEnumerator

Defined in the solver.py module.
By extending this interface and implementing all its abstract methods, it is possible to define custom SMTEnumerators that are compatible with the rest of the package.

The abstract methods are:

check_all_sat()

Args:

  • self
  • phi:
    TYPE: FNode
    DESCRIPTION: the formula over which the solver must compute enumeration
  • boolean_mapping:
    TYPE: Dict[FNode,FNode] | None
    DEFAULT VALUE: None DESCRIPTION: a mapping that associates to each fresh boolean variable (keys) a atom that appears in phi (values). When a solver is provided a boolean mapping it will enumerate over the fresh boolean variables instead of the original atoms. Some enumerators may ignore this argument.

Returns:

  • bool:
    DESCRIPTION: the boolean constant SAT if phi is T-satisfiable, the boolean constant UNSAT otherwise

Method description:

  • When this method is called the enumerator must compute AllSMT on phi in order to extract all theory lemmas that allow the solver to trim all T-inconsistent assignments during enumeration and return a boolean constant that describes the satisfiability of phi.

get_theory_lemmas()

Args:

  • self

Returns:

  • List[FNode]:
    DESCRIPTION: the T-lemmas that were extracted during allSMT computation

Method description:

  • When this method is called the enumerator returns a list of theory lemmas.

get_converter()

Args:

  • self

Returns:

  • object:
    DESCRIPTION: the solver's converter which allows for normalization of formulas

Method description:

  • When this method is called the enumerator returns its converter object.

get_models()

Args:

  • self

Returns:

  • List:
    DESCRIPTION: the list of the models that were extracted during allSMT computation

Method description:

  • When this method is called the enumerator returns a list of T-consistent models.

The SMTEnumerator interface also implements a non-abstract method which is inherited by all its children classes.

enumerate_true()

Args:

  • self
  • phi:
    TYPE: FNode
    DESCRIPTION: the formula over which the solver must compute enumeration

Returns:

  • bool:
    DESCRIPTION: always returns the boolean constant SAT, since the boolean formula True is always T-satisfiable (but may not be T-valid depending on which atoms it is defined over!)

Method description:

  • When this method is called, the enumerator computes AllSMT on a set of formulas that are booleanly equivalent to True by repeatedly calling check_all_sat. These formulas are defined on partitions of the atoms that are present in phi. Atoms that share free variables (even if only transitively) are always in the put in the same partition.

MathSATTotalEnumerator

Defined in the mathsat_total.py module.
The MathSATTotalEnumerator is an implementation of SMTEnumerator which always enumerates total truth assignments through the MathSAT SMT solver.
This enumerator allows enumeration over a boolean mapping of the atoms.

MathSATPartialEnumerator

Defined in the mathsat_partial.py module.
The MathSATPartialEnumerator is an implementation of SMTEnumerator which always enumerates partial truth assignments through the MathSAT SMT solver.
This enumerator never enumerates over a boolean mapping of the atoms.

MathSATExtendedPartialEnumerator

Defined in the mathsat_partial_extended.py module.
The MathSATExtendedPartialEnumerator is an implementation of SMTEnumerator which always enumerates totaltruth assignments through the MathSAT SMT solver.
The enumeration is computed as follows:

  • first, partial enumeration is computed and all partial assignments are stored in memory
  • then all incomplete partial assignments are extended to total assignments through incremental calls to the solver

This enumerator never enumerates over a boolean mapping of the atoms.

TabularSMTSolver

Defined in the tabular.py module.
The TabularSMTSolver is an implementation of SMTEnumerator which can both enumerate partial and total truth assignments through the tabularAllSMT SMT solver.
This enumerator never enumerates over a boolean mapping of the atoms.
The constructor for this SMTsolver has an optional parameter is_partial which defaults to False. If this parameter is set to True, than the instance of TabularSMTSolver will enumerate partial truth assignments, while it will enumerate total truth assignments otherwise.

TabularTotalSMTSolver

Defined in the tabular.py module.
A wrapper for the TabularSMTSolver which always enumerates total truth assignments.

TabularPartialSMTSolver

Defined in the tabular.py module.
A wrapper for the TabularSMTSolver which always enumerates partial truth assignments.

Lemma Extractor

Defined in the lemma_extractor.py module are these 2 functions:

extract()

Args:

  • phi:
    TYPE: FNode
    DESCRIPTION: the formula from which to extract theory lemmas
  • smt_solver:
    TYPE: SMTEnumerator
    DESCRIPTION: the SMTEnumerator on which check_all_sat will be called in order to extract theory lemmas
  • _enumerate_true:
    TYPE: bool
    DEFAULT VALUE: False
    DESCRIPTION: if set to True, enumerate_true will be called on smt_solver instead of check_all_sat
  • use_boolean_mapping:
    TYPE: bool
    DEFAULT VALUE: True
    DESCRIPTION: if set to True, the solver that extracts lemmas for phi will be provided with a boolean mapping
  • computation_logger:
    TYPE: Dict | None
    DEFAULT VALUE: None
    DESCRIPTION: a Dict passed by reference which will be updated with details from the computation

Returns (Tuple):

  • bool:
    DESCRIPTION: the boolean constant SAT if phi is T-satisfiable, the boolean constant UNSAT otherwise
  • List[FNode]:
    DESCRIPTION: a list of the extracted theory lemmas
  • Dict[FNode,FNode] | None:
    DESCRIPTION a dictionary representing a boolean mapping between fresh boolean atoms (keys) and the atoms of phi (values) if use_boolean_mapping is set to True, None otherwise

Method description:

  • When this method is called, the provided smt_solver is used in order to extract theory lemmas form the formula phi. These lemmas are then returned together with the satisfiability of phi as a boolean constant and an optional dictionary representing a boolean mapping over the atoms of phi.

find_qvars()

Args:

  • original_phi
    TYPE: FNode
    DESCRIPTION: the formula without the conjunction with the theory lemmas
  • phi_and_lemmas
    TYPE: FNode
    DESCRIPTION: the formula after the conjunction with the theory lemmas
  • computation_logger:
    TYPE: Dict | None
    DEFAULT VALUE: None
    DESCRIPTION: a Dict passed by reference which will be updated with details from the computation

Returns:

  • List[FNode]:
    DESCRIPTION a list of the fresh atoms introduced in the formula from the conjunction with the theory lemmas

Method description:

  • This method takes as input the formula before and after the conjunction with the lemmas and finds which fresh atoms this conjunction introduced, returning them inside a List.

Theory Decision Diagrams

The submodule tdd contains all Desision Diagrams compilers that require computation of AllSMT for compilation into the target language.
All such compilers inherit from the interface class TheoryDD and implement all its abstract methods.

TheoryDD

The TheoryDD abstract class requires implementation of the following abstract methods:

_enumerate_qvars()

Args:

  • self
  • tlemmas_dd:
    TYPE: object DESCRIPTION: the T-DD built from the big and of the theory lemmas
  • mapped_qvars:
    TYPE: List[object]
    DESCRIPTION: a list of all the labels over which to enumerate

Returns:

  • object:
    DESCRIPTION: the root of the tlemma_dd enumerated over the quantified variables

Method description:

  • transforms argument tlemma_dd in { Exists(quantified variables) tlemma_dd } and returns the root of the result of the transformation. This method is used to remove fresh atoms that may be generated by the solver inside the theory lemmas which are not present in the original formula.

_load_from_folder()

Args:

  • self
  • folder_path:
    TYPE: str
    DESCRIPTION: the path to the folder where the T-DD is stored. Notice that different T-DDs may have different formats for serialization.

Method Description:

  • Loads all the data for the T-DD from the specified folder. This function is usually called inside the constructor to load a pre-built T-DD instead of recompiling the same formula.

save_to_folder()

Args:

  • self
  • folder_path:
    TYPE: str
    DESCRIPTION: the path to the folder where the T-DD must be stored

Method description:

  • Serializes the T-DD into the folder specified in folder_path, creating the folder if necessary. If a T-DD is already saved in that folders, its files may be overwritten.

__len__()

Args:

  • self

Returns:

  • int:
    DESCRIPTION: the number of the nodes of the T-DD

Method description:

  • returns the amount of nodes in the T-DD.

count_nodes()

Args:

  • self

Returns:

  • int:
    DESCRIPTION: the number of the nodes of the T-DD

Method description:

  • returns the amount of nodes in the T-DD (same as __len__()).

count_vertices()

Args:

  • self

Returns:

  • int:
    DESCRIPTION: the number of links between the nodes of the T-DD.

Method description:

  • returns the amount of vertices in the T-DD.

count_models()

Args:

  • self

Returns:

  • int:
    DESCRIPTION: the amount of models encoded in the T-DD.

Method description:

  • returns the amount of models encoded in the T-DD.

graphics_dump()

Args:

  • self
  • output_file:
    TYPE: str
    DESCRIPTION: the path to a file where a graphical representation of the T-DD will be saved.

Method description:

  • A graphical representation of T-DD is saved inside output_file. This method may raise errors if GraphViz is not installed on the user's machine or if the size of the T-DD is high.

pick()

Args:

  • self

Returns:

  • Dict[FNode, bool] | None:
    DESCRIPTION: a model of the encoded DD, None if the DD has no models.

Method description:

  • returns a model of the encoded DD, None if the DD has no models.

pick_all()

Args:

  • self

Returns:

  • List[Dict[FNode, bool]]:
    DESCRIPTION: a list of all the models of the DD

Method description:

  • returns a list of all the models encoded in the DD, if the encoded formula is TRUE or unsatisfiable, an empty list will be returned.

pick_all_iter()

Args:

  • self

Returns:

  • Iterator[Dict[FNode, bool]]:
    DESCRIPTION: an iterator that enumerates all encoded models

Method description:

  • this method returns an iterator which yields the models encoded in the DD one at a time as Dict[FNode,bool].

is_sat()

Args:

  • self

Returns:

  • bool:
    DESCRIPTION: True if the encoded formula is satisfiable, False otherwise

Method description:

  • this method checks the satisfiability of the compiled formula.

is_valid()

Args:

  • self

Returns:

  • bool:
    DESCRIPTION: True if the encoded formula is valid, False otherwise

Method description:

  • this method checks the validity of the compiled formula.

The theory_dd class also implements some useful private methods for the construction of T-DDs:

_normalize_input()

Args:

  • self
  • phi:
    TYPE: FNode
    DESCRIPTION: the formula that has to be encoded into a T-DD
  • solver:
    TYPE: SMTEnumerator
    DESCRIPTION: an SMTEnumerator that is only used for normalization
  • computation_logger:
    TYPE: Dict
    DESCRIPTION: a Dict passed by reference which will be updated with details from the computation

Returns:

  • FNode:
    DESCRIPTION: the normalized input formula

Method description:

  • Normalizes the input formula phi using the converter that solver owns and logs the time elapsed during this operation in the computation_logger.

_load_lemmas()

Args:

  • self
  • phi:
    TYPE: FNode
    DESCRIPTION: the formula that has to be encoded into a T-DD
  • smt_solver:
    TYPE: SMTEnumerator:
    DESCRIPTION: an SMTEnumerator that is used for normalization of the theory lemmas and theory lemma extraction if necessary
  • tlemmas:
    TYPE: List[FNode] | None
    DESCRIPTION: the theory lemmas of phi, or None if the theory lemmas are not available in memory yet
  • load_lemmas:
    TYPE: str | None
    DESCRIPTION: the path to a .smt2 file where the theory lemmas are stored, None if such a file is not available
  • sat_result:
    TYPE: bool | None
    DESCRIPTION: the T-satisfiability of phi if known, None otherwise
  • computation_logger:
    TYPE: Dict
    DESCRIPTION: a Dict passed by reference which will be updated with details from the computation

Returns:

  • List[FNode]:
    DESCRIPTION: the theory lemmas of the input formula, already normalized.
  • bool | None:
    DESCRIPTION: the T-satisfiability of phi if available, None otherwise

Method description:

  • Loads the theory lemmas fro the correct source and logs the time elapsed during this operation in the computation_logger. If the theory lemmas are provided in the tlemmas argument, then those lemmas are normalized and returned. If the load_lemmas argument is not None and the theory lemmas are not provided, then the theory lemmas are loaded from the specified file. If both tlemmas and load_leamms are None, the theory lemmas are extracted from the formula by computing AllSMT with the provided smt_solver.

_build()

Args:

  • self
  • phi:
    TYPE: FNode
    DESCRIPTION: the formula that has to be encoded in the T-DD
  • tlemmas:
    TYPE: List[FNode]
    DESCRIPTION: the list of the theory lemmas of phi
  • walker:
    TYPE: DagWalker
    DESCRIPTION: a walker that walks over phi in order to call the correct apply function of the T-DD
  • computation_logger:
    TYPE: Dict
    DESCRIPTION: a Dict passed by reference which will be updated with details from the computation Returns:
  • object: DESCIPTION: the root of the T-DD of phi

Method description:

  • builds the T-DD for phi and tlemmas which only encodes consistent truth assignments and returns its root

_build_unsat()

Args:

  • self
  • walker:
    TYPE: DagWalker
    DESCRIPTION: a walker that walks over an FNode in order to call the correct apply function of the T-DD
  • computation_logger:
    TYPE: Dict
    DESCRIPTION: a Dict passed by reference which will be updated with details from the computation Returns:
  • object: DESCIPTION: the root of the T-DD of the SMT formuala FALSE

Method description:

  • builds the T-DD for an unsatisfiable SMT formula in an efficient way and returns its root

Finally, the TheoryDD class implements the following public methods that are available to all its children classes:

get_mapping()

Method description: Same as get_abstraction().

get_abstraction()

Args:

  • self

Returns:

  • Dict[FNode,object]: DECRIPTION: a dictionary defining the abstraction function used when building the DD

Method description:

  • Returns a dictionary which describes the abstraction function that the DD uses.

get_refinement()

Args:

  • self

Returns:

  • Dict[object,FNode]: DECRIPTION: a dictionary defining the refinement function

Method description:

  • Returns a dictionary which describes the abstraction function that the DD uses, which is used to decode the models of the DD when pick(), _pick_all() or pick_all_iter() are called.

TheoryBDD

A TheoryBDD instance is an instance of a TheoryDD which implements all abstract methods and builds the DD through the CUDD library wrapper provided by the dd Python package.

Constructor parameters:

  • self
  • phi:
    TYPE: FNode
    DESCRIPTION: the formula that has to be compiled into a T-BDD
  • solver:
    TYPE: SMTEnumerator | str
    DEFAULT VALUE: "total"
    DESCRIPTION: if a string is provided, a new SMTEnumerator of the type specified from the string will be used during construction, otherwise the provided enumerator will be used. This parameter is used to compute enumeration (if necessary) and to apply normalization to theory atoms while building the DD.
  • tlemmas:
    TYPE: List[FNode] | None
    DEFAULT VALUE: None
    DESCRIPTION: if a list of FNode is provided, the theory lemmas will not be enumerated and the procided lemmas will be used instead, skipping enumeration
  • load_lemmas:
    TYPE: str | None
    DEFAULT VALUE: None
    DESCRIPTION: if a string is provided, the theory lemmas will be loaded from the SMT file located at the path specified in that string, skipping enumeration. If the tlemmas parameter for this function is not None, this parameter is ignored.
  • sat_result: TYPE: bool | None
    DEFAULT VALUE: None
    DESCRIPTION: provide one of the boolean constant SAT or UNSAT defined in the constants module to signal to the constructor that it is dealing with a satisfiable/unsatisfiable formula in order to speed up compilation time. If None is provided, than the constructor does not assume that the formula is either satisfiable or unsatisfiable.
  • use_ordering:
    TYPE: List[FNode] | None
    DEFAULT VALUE: None
    DESCRIPTION: if a list of FNode is provided, this class will respect the provided ordering of variables when building the DD
  • folder_name:
    TYPE: str | None
    DEFAULT VALUE: None
    DESCRIPTION: if a string is provided, all other parameters except for solver will be ignored and the TheoryBDD will be loaded from the specified path
  • computation_logger:
    TYPE: Dict | None
    DEFAULT VALUE: None
    DESCRIPTION: a Dict passed by reference which will be updated with details from the computation

In addition to implemnting all abstract methods from the TheoryDD interfece, this class also provides these public methods:

get_ordering()

Args:

  • self

Returns:

  • List[FNode]:
    DESCRIPTION: the ordering of atoms used while building the T-BDD

Method description:

  • The ordering used for building the DD is returned

condition()

Args:

  • self
  • condition:
    TYPE: str
    DESCRIPTION: a string contained in the values of the abstraction dictionary which corresponds to the abstraction of the atom that you want to condition over. Start the string with a - symbol in order to indicate a negation of the atom (condition over Not atom).

Method description:

  • Transform the TheoryBDD of phi into the ThoeryBDD of phi | condition.

TheorySDD

A TheorySDD instance is an instance of a TheoryDD which implements all abstract methods and builds the DD through the SDD library wrapper provided by the PySDD Python package.

Constructor parameters:

  • self
  • phi:
    TYPE: FNode
    DESCRIPTION: the formula that has to be compiled into a T-SDD
  • solver:
    TYPE: SMTEnumerator | str
    DEFAULT VALUE: "total"
    DESCRIPTION: if a string is provided, a new SMTEnumerator of the type specified from the string will be used during construction, otherwise the provided enumerator will be used. This parameter is used to compute enumeration (if necessary) and to apply normalization to theory atoms while building the DD.
  • tlemmas:
    TYPE: List[FNode] | None
    DEFAULT VALUE: None
    DESCRIPTION: if a list of FNode is provided, the theory lemmas will not be enumerated and the procided lemmas will be used instead, skipping enumeration
  • load_lemmas:
    TYPE: str | None
    DEFAULT VALUE: None
    DESCRIPTION: if a string is provided, the theory lemmas will be loaded from the SMT file located at the path specified in that string, skipping enumeration. If the tlemmas parameter for this function is not None, this parameter is ignored.
  • sat_result: TYPE: bool | None
    DEFAULT VALUE: None
    DESCRIPTION: provide one of the boolean constant SAT or UNSAT defined in the constants module to signal to the constructor that it is dealing with a satisfiable/unsatisfiable formula in order to speed up compilation time. If None is provided, than the constructor does not assume that the formula is either satisfiable or unsatisfiable.
  • vtree_type:
    TYPE: str
    DEFAULT VALUE: "balanced"
    DESCRIPTION: an indication of the shape of the V-Tree used for the construction of the SDD. Valid values for this parameter are specified in the VALID_VTREE constant in the constants module.
  • _use_vtree:
    TYPE: Vtree | None
    DEFAULT VALUE: None
    DESCRIPTION: if a Vtree is provided, the specified V-Tree will be used and the vtree_type parameter will be ignored. It is important to use this parameter together with the use_abstraction parameter since the Vtree ordering in the resulting structure may be shuffled otherwise.
  • use_abstraction:
    TYPE: Dict[Fnode,int] | None
    DEFAULT VALUE: None
    DESCRIPTION: if a Dict[FNode,int] is provided, the specified abstraction function will be used while building the DD. It is important to use this parameter together with the use_vtree parameter since the Vtree ordering in the resulting structure may be shuffled otherwise.
  • folder_name:
    TYPE: str | None
    DEFAULT VALUE: None
    DESCRIPTION: if a string is provided, all other parameters except for solver will be ignored and the TheorySDD will be loaded from the specified path
  • computation_logger:
    TYPE: Dict | None
    DEFAULT VALUE: None
    DESCRIPTION: a Dict passed by reference which will be updated with details from the computation

In addition to implemnting all abstract methods from the TheoryDD interfece, this class also provides these public methods:

graphic_dump_vtree()

Args:

  • self
  • output_file:
    TYPE: str
    DESCRIPTION: a path where a graphical representation of the Vtree will be dumped

Method description:

  • A graphical representation of the Vtree is dumped in the specified output_file.

condition()

Args:

  • self
  • condition:
    TYPE: int
    DESCRIPTION: an integer contained in the values of the abstraction dictionary which corresponds to the abstraction of the atom that you want to condition over. Provide the opposite integer of the abstraction index in order to indicate a negation of the atom (condition over Not atom).

Method description:

  • Transform the TheorySDD of phi into the ThoerySDD of phi | condition.

get_vtree()

Args:

  • self

Returns:

  • Vtree:
    DESCRIPTION: the Vtree used for the construction of the T-SDD

Method description:

  • Returns the Vtree used for the construction of the T-SDD.

Abstract Decision Diagrams

The submodule abstractdd contains all Desision Diagrams compilers that do not require computation of AllSMT for compilation into the target language, whic are AbstractionBDD and AbstractionSDD.

AbstractionBDD

The AbstractionBDD class inherits from TheoryBDD and describes the BDD of an SMT formula without adding any theory lemmas.

Constructor parameters:

  • self
  • phi:
    TYPE: FNode
    DESCRIPTION: the formula that has to be compiled into an AbstractionBDD
  • solver:
    TYPE: SMTEnumerator | str
    DEFAULT VALUE: "total"
    DESCRIPTION: if a string is provided, a new SMTEnumerator of the type specified from the string will be used during construction, otherwise the provided enumerator will be used. This parameter is only used to apply normalization to theory atoms while building the DD.
  • use_ordering:
    TYPE: List[FNode] | None
    DEFAULT VALUE: None
    DESCRIPTION: if a list of FNode is provided, this class will respect the provided ordering of variables when building the DD
  • folder_name:
    TYPE: str | None
    DEFAULT VALUE: None
    DESCRIPTION: if a string is provided, all other parameters except for solver will be ignored and the AbstractionBDD will be loaded from the specified path
  • computation_logger:
    TYPE: Dict | None
    DEFAULT VALUE: None
    DESCRIPTION: a Dict passed by reference which will be updated with details from the computation

AbstractionSDD

The AbstractionSDD class inherits from TheorySDD and describes the SDD of an SMT formula without adding any theory lemmas.

Constructor parameters:

  • self
  • phi:
    TYPE: FNode
    DESCRIPTION: the formula that has to be compiled into an AbstractionSDD
  • solver:
    TYPE: SMTEnumerator | str
    DEFAULT VALUE: "total"
    DESCRIPTION: if a string is provided, a new SMTEnumerator of the type specified from the string will be used during construction, otherwise the provided enumerator will be used. This parameter is only used to apply normalization to theory atoms while building the DD.
  • vtree_type:
    TYPE: str
    DEFAULT VALUE: "balanced"
    DESCRIPTION: an indication of the shape of the V-Tree used for the construction of the SDD. Valid values for this parameter are specified in the VALID_VTREE constant in the constants module.
  • _use_vtree:
    TYPE: Vtree | None
    DEFAULT VALUE: None
    DESCRIPTION: if a Vtree is provided, the specified V-Tree will be used and the vtree_type parameter will be ignored. It is important to use this parameter together with the use_abstraction parameter since the Vtree ordering in the resulting structure may be shuffled otherwise.
  • use_abstraction:
    TYPE: Dict[Fnode,int] | None
    DEFAULT VALUE: None
    DESCRIPTION: if a Dict[FNode,int] is provided, the specified abstraction function will be used while building the DD. It is important to use this parameter together with the use_vtree parameter since the Vtree ordering in the resulting structure may be shuffled otherwise.
  • folder_name:
    TYPE: str | None
    DEFAULT VALUE: None
    DESCRIPTION: if a string is provided, all other parameters except for solver will be ignored and the AbstractionSDD will be loaded from the specified path
  • computation_logger:
    TYPE: Dict | None
    DEFAULT VALUE: None
    DESCRIPTION: a Dict passed by reference which will be updated with details from the computation

d-DNNF

d-DNNF compilers

Utility

General utility