Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

add TDDFunction::eval? #27

Open
carljm opened this issue Dec 18, 2024 · 2 comments
Open

add TDDFunction::eval? #27

carljm opened this issue Dec 18, 2024 · 2 comments

Comments

@carljm
Copy link

carljm commented Dec 18, 2024

Thank you for this library!

I notice that the version of oxidd released on crates.rs doesn't appear to include oxidd::tdd.

In experimentation locally with the git main branch, I can construct a TDDFunction, but it seems to missing all methods for evaluation/satisfiability.

How far is the TDD implementation from usability?

@nhusung
Copy link
Member

nhusung commented Dec 18, 2024

I notice that the version of oxidd released on crates.rs doesn't appear to include oxidd::tdd.

Did you enable the tdd feature of the oxidd crate, e.g., using oxidd = { version = "0.9.0", features = ["tdd"] } in your Cargo.toml?

In experimentation locally with the git main branch, I can construct a TDDFunction, but it seems to missing all methods for evaluation/satisfiability.

How far is the TDD implementation from usability?

The TDD implementation is certainly not as feature-rich as the B(C)DD/ZBDD implementations yet. Currently, the API mostly consists of methods to apply operators like conjunction etc., but it is not difficult to add methods for evaluation/satisfiablity checking. I have to admit that I’m not too deep into the common terminology for three-valued logic, so I’d need to think a bit about what satisfiability etc. actually mean: For example, in Boolean logic/BDDs, satisfiability of a function $f$ is equivalent to $f \neq \bot$ and there being a path from the node representing $f$ to the $\top$ terminal. For TDDs, there are nodes different from $\bot$ that do not have a path to $\top$.

If you have concrete requests for new methods along with a short specification, then I should be able to implement them rather quickly.

@carljm
Copy link
Author

carljm commented Dec 18, 2024

Did you enable the tdd feature of the oxidd crate, e.g., using oxidd = { version = "0.9.0", features = ["tdd"] } in your Cargo.toml?

Oops, I thought I had, but I think I had introduced the dependency in my workspace Cargo.toml and failed to introduce it in my crate Cargo.toml; sorry for the noise! (For what it's worth, what led me to jump too quickly to the conclusion that it's not there in the released crate 0.9.0 is missing documentation: there's no tdd submodule listed in the docs at https://docs.rs/oxidd/0.9.0/oxidd/, nor is it present at https://docs.rs/oxidd/0.9.0/src/oxidd/lib.rs.html.)

I’d need to think a bit about what satisfiability etc. actually mean

If you have concrete requests for new methods along with a short specification

Yes, I shouldn't have even mentioned satisfiability, I agree the definition is not obvious. All I'm actually looking for is the eval method which is present on BDDFunction, to which I could pass a value (true/false/undetermined) for each variable, and get back true/false/undetermined.

@carljm carljm changed the title status of TDD implementation? add TDDFunction::eval? Dec 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants