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

TermTranslator unhelpful rewrite. #326

Open
kunalsheth opened this issue Jul 14, 2023 · 2 comments
Open

TermTranslator unhelpful rewrite. #326

kunalsheth opened this issue Jul 14, 2023 · 2 comments
Assignees

Comments

@kunalsheth
Copy link

When fed the CVC5 term:
(let ((_let_1 (f y))) (let ((_let_2 (f x))) (and (<= 0 _let_2) (<= 0 _let_1) (<= (+ _let_2 _let_1) 1) (not (p 0)) (p _let_1))))

The TermTranslator (to any solver), rewrites it as:
(let ((_let_1 (f y))) (let ((_let_2 (f x))) (and (= (ite (<= 0 _let_2) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (= (ite (<= 0 _let_1) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (= (ite (<= (+ _let_2 _let_1) 1) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (= (ite (not (p 0)) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (= (ite (p _let_1) (_ bv1 1) (_ bv0 1)) (_ bv1 1)))))

We would like the option to disable such a rewrite.

It appears this may be caused by two related bugs:

  1. Because the AND has more than two children, execution goes into the if-statement linked below. We think we would like an option to manually disable this check and/or make smt-switch allow for ANDs to support more than two children. The translated term should have as similar a structure to the original term as possible.
    https://github.com/stanford-centaur/smt-switch/blob/f2d7d3d6dfccc0b4d6b604563acd34629bac884d/src/term_translator.cpp#L269C12-L269C12
  2. It looks like cast_op and/or cast_term are being called twice upon themselves, leading to a Boolean-to-BV rewrite immediately followed by a BV-to-Boolean rewrite— which I do not think is the intended behavior, and we would also like to turn off.
@barrettcw
Copy link
Collaborator

This does look weird. Can you propose a fix and submit a PR?

@barrettcw
Copy link
Collaborator

@makaimann - low priority but could you have a look at this and see if you can tell us where the problem is?

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

3 participants