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

Check handling of auxiliary variables after inlining #67

Open
blishko opened this issue May 20, 2024 · 0 comments
Open

Check handling of auxiliary variables after inlining #67

blishko opened this issue May 20, 2024 · 0 comments

Comments

@blishko
Copy link
Member

blishko commented May 20, 2024

After resolving on some predicate in multiple clauses, the same auxiliary variable from one clause may end up in multiple clauses. This is undesirable, because it causes problems in engines that make global, not just local satisfiability checks.

Moreover, former state variables may become auxiliary in the new clause and hence they should be renamed, so they do not confuse our versioning system.

Hints:

  • Look at ChcDirectedHyperGraph::contractVertex and its requiresRenamingAuxiliaryVars flag.
  • Possibly add another preprocessing pass that will try to eliminate auxiliary variables after other rewriting passes.
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

1 participant