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.

Sign up for GitHub

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

Jump to bottom

issue with slicing #6

Open
hgvk94 opened this issue Nov 17, 2020 · 3 comments
Open

issue with slicing #6

hgvk94 opened this issue Nov 17, 2020 · 3 comments

Comments

@hgvk94
Copy link
Owner

hgvk94 commented Nov 17, 2020

commit
instance
Issue:
The instance is SAT. If Z3 is run with argument fp.xform.slice=true, Z3 will say UNSAT. If run with the argument fp.xform.slice=false, Z3 will say SAT.
Cause:
The 3rd argument to Inv is not slicable because it is being used in the formula. However, Z3 thinks it is slicable and removes it from Inv. This makes the formula unsatisfiabe.

Another observation is that removing the clause (=> false false) gets rid of the bug. That is, if you remove this clause from the formula, Z3 does not slice the formula.
@hgvk94
Copy link
Owner Author

hgvk94 commented Nov 19, 2020

original instance

@hgvk94
Copy link
Owner Author

hgvk94 commented Nov 19, 2020

note regarding the (=> false false) clause:
The slicing algorithm in Z3 will slice only if the output predicate of the rule set is slicable. I am not sure what the criteria for being an output predicate is. When the (=> false false) clause is added, the rule set passed as input to mk_slice is

; rule count: 3
; predicate count: 2
; output: query!1
<null>:
Inv(true,false,false,true,true,#x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000).
<null>:
Inv(true,#1,false,true,#0,#x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) :- 
 Inv(true,false,#1,true,true,#x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000).
<null>;<null>:
query!1() :- 
 Inv(true,true,#0,true,false,#x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000).

However, when the (=> false false) clause is removed, the rule set is:

; rule count: 3
; predicate count: 2
; output: query!0
<null>:
query!0(#0) :- 
 Inv(true,true,#0,true,false,#x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000).
<null>:
Inv(true,false,false,true,true,#x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000).
<null>:
Inv(true,#1,false,true,#0,#x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) :- 
 Inv(true,false,#1,true,true,#x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000).

@hgvk94
Copy link
Owner Author

hgvk94 commented Nov 23, 2020

The issue is with the logic of slicing.
A simplified example. This example is SAT. If we run it with the fp.xform.slice=true option, z3 will say UNSAT.

In this example, the first argument of inv is removed by slicing. The slicing rule used here is

In a rule     P(x,y) :-   R(x,z), phi(x,y,z)
      x_i is sliceable if x_i does not appear in phi(x,y,z)
      and the positions where x_i is used in P and R are sliceable

a position is slicable in a predicate if a variable is in that position whenever the predicate appears on the tail of a rule.
As the example demonstrates, the rule is not sound.

hgvk94 pushed a commit that referenced this issue Aug 4, 2023
@mtzguido
bool_rewriter: fix possible segfault when disabling rewriter.sort_dis…
7c380fd 
…junctions (Z3Prover#6779)

After introducing the rewriter.sort_disjunctions option (Z3Prover#6774), I
noticed a segfault in a Z3 run that was working fine for me before the
PR.

I traced the difference to a slight discrepancy between the first patch
I submitted and the one we ended up merging: my first version would skip
sorting the disjuncts in mk_nflat_core, but still return BR_DONE, while
the patch in master returns BR_FAILED instead.

This patch fixes that problem, and it makes slightly more sense to me to
return a BR_DONE since, if `s` is true, some disjunct (e.g. a `false`
or a repeat) might have been simplified away. However I don't fully
understand this code.

... and I can't say I understand why the segfault happens. Perhaps that
is a separate issue?

This is the file to reproduce:
 https://gist.github.com/mtzguido/b7360c74d3d2e42d89f1bd9149ad26f6

Here's a stack trace of the failure, mk_nflat_or_core is not involved.
```
 (gdb) where
 #0  0x0000555555b98497 in smt::context::get_lit_assignment(unsigned int) const ()
 #1  0x0000555555b984cb in smt::context::get_assignment(sat::literal) const ()
 #2  0x0000555555b98504 in smt::context::get_assignment(unsigned int) const ()
 #3  0x0000555555ca83b8 in smt::context::get_assignment_core(expr*) const ()
 #4  0x0000555555c9af5a in smt::context::get_assignment(expr*) const ()
 #5  0x0000555555d7bd1d in (anonymous namespace)::has_child_assigned_to(smt::context&, app*, lbool, expr*&, unsigned int) ()
 #6  0x0000555555d7c413 in (anonymous namespace)::rel_case_split_queue::next_case_split_core(ptr_vector<expr>&, unsigned int&, unsigned int&, lbool&) ()
 #7  0x0000555555d7c589 in (anonymous namespace)::rel_case_split_queue::next_case_split(unsigned int&, lbool&) ()
 #8  0x0000555555c9c1b7 in smt::context::decide() ()
 #9  0x0000555555ca39fd in smt::context::bounded_search() ()
 #10 0x0000555555ca30c2 in smt::context::search() ()
 Z3Prover#11 0x0000555555ca273d in smt::context::check(unsigned int, expr* const*, bool) ()
 Z3Prover#12 0x0000555555cb166a in smt::kernel::check(unsigned int, expr* const*) ()
 Z3Prover#13 0x0000555555cb9695 in (anonymous namespace)::smt_solver::check_sat_core2(unsigned int, expr* const*) ()
 Z3Prover#14 0x00005555560dc0c6 in solver_na2as::check_sat_core(unsigned int, expr* const*) ()
 Z3Prover#15 0x00005555560d73f3 in combined_solver::check_sat_core(unsigned int, expr* const*) ()
 Z3Prover#16 0x00005555560d34e3 in solver::check_sat(unsigned int, expr* const*) ()
 Z3Prover#17 0x0000555556097b26 in cmd_context::check_sat(unsigned int, expr* const*) ()
 Z3Prover#18 0x0000555556082ff0 in smt2::parser::parse_check_sat() ()
 Z3Prover#19 0x0000555556084dc0 in smt2::parser::parse_cmd() ()
 Z3Prover#20 0x00005555560861b6 in smt2::parser::operator()() ()
 Z3Prover#21 0x00005555560757e6 in parse_smt2_commands(cmd_context&, std::basic_istream<char, std::char_traits<char> >&, bool, params_ref const&, char const*) ()
 Z3Prover#22 0x00005555555e8f68 in read_smtlib2_commands(char const*) ()
 Z3Prover#23 0x00005555555ee6f6 in main ()
 (gdb)
```
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@hgvk94