Enhancement: Use operator overloading in the .NET API #6
Comments
|
I agree, that would be nice, but C# doesn't allow overloading of && and ||. Given that we can't have a complete set of operators, we decided not to go there at all. |
|
I think C# does allow overloading of & and |. Booth are listed as overloadable operators in the documentation as well: Some solvers (Gurobi for example) do provide those overloads and I find them very useful. |
|
Yes, it does, but it doesn't allow overloading of && and ||, which would clearly be the most useful. Note that we also have bit-vectors, so if we use & for Booleans, we can't use it for bv_and anymore. |
|
&& and || are evaluated by calls to & and |, respectively. Shouldn't it all just work, if you implement it this way (examples for &):
Similar to the regular use of & in C#, it should just work for both, bitwise and boolean, scenarios and just return the respective type as result. I'm probably not thinking properly... |
|
Yes, that would be possible, but it would be inconsistent with the C++ and Python APIs, and the Java API as well (Java doesn't support overloading). Note that & and && are not the same in C++ (or any other language), specifically, if their result is used in an if-condition, the result of & will silently be cast to an int and compared to zero, but in Z3 there are no silent casts. If things were the other way around (&& overloadable, not &), we could think about adding just the Boolean case (not everybody needs BitVectors, but everybody needs Booleans), but that isn't the case. So after re-evaluating the situation, I'm still opposed to adding this. |
|
I personally don't see the value of API consistency across programming languages. But it's ok. |
|
Granted for new end-users there is little benefit. It does make it a lot easier to maintain all the different APIs though, because we can basically apply patches to all of them at the same time with little chance of introducing new bugs (e.g., the Java API started as a literal copy of the .NET library with a couple of sed commands run over it).. |
Closed
Closed
This was referenced Jan 31, 2018
agurfinkel
referenced
this issue
in agurfinkel/z3
May 14, 2018
Lookahead clause size optimization. Fixed some missing propagations
Closed
Closed
Merged
mtzguido
added a commit
to mtzguido/z3
that referenced
this issue
Jun 23, 2023
…junctions After introducing the rewriter.sort_disjunctions option, I noticed a segfault in a Z3 run that was working fine for me. 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 the problem for me, 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 () Z3Prover#1 0x0000555555b984cb in smt::context::get_assignment(sat::literal) const () Z3Prover#2 0x0000555555b98504 in smt::context::get_assignment(unsigned int) const () Z3Prover#3 0x0000555555ca83b8 in smt::context::get_assignment_core(expr*) const () Z3Prover#4 0x0000555555c9af5a in smt::context::get_assignment(expr*) const () Z3Prover#5 0x0000555555d7bd1d in (anonymous namespace)::has_child_assigned_to(smt::context&, app*, lbool, expr*&, unsigned int) () Z3Prover#6 0x0000555555d7c413 in (anonymous namespace)::rel_case_split_queue::next_case_split_core(ptr_vector<expr>&, unsigned int&, unsigned int&, lbool&) () Z3Prover#7 0x0000555555d7c589 in (anonymous namespace)::rel_case_split_queue::next_case_split(unsigned int&, lbool&) () Z3Prover#8 0x0000555555c9c1b7 in smt::context::decide() () Z3Prover#9 0x0000555555ca39fd in smt::context::bounded_search() () Z3Prover#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) ```
mtzguido
added a commit
to mtzguido/z3
that referenced
this issue
Jun 23, 2023
…junctions 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 () Z3Prover#1 0x0000555555b984cb in smt::context::get_assignment(sat::literal) const () Z3Prover#2 0x0000555555b98504 in smt::context::get_assignment(unsigned int) const () Z3Prover#3 0x0000555555ca83b8 in smt::context::get_assignment_core(expr*) const () Z3Prover#4 0x0000555555c9af5a in smt::context::get_assignment(expr*) const () Z3Prover#5 0x0000555555d7bd1d in (anonymous namespace)::has_child_assigned_to(smt::context&, app*, lbool, expr*&, unsigned int) () Z3Prover#6 0x0000555555d7c413 in (anonymous namespace)::rel_case_split_queue::next_case_split_core(ptr_vector<expr>&, unsigned int&, unsigned int&, lbool&) () Z3Prover#7 0x0000555555d7c589 in (anonymous namespace)::rel_case_split_queue::next_case_split(unsigned int&, lbool&) () Z3Prover#8 0x0000555555c9c1b7 in smt::context::decide() () Z3Prover#9 0x0000555555ca39fd in smt::context::bounded_search() () Z3Prover#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) ```
NikolajBjorner
pushed a commit
that referenced
this issue
Jun 23, 2023
…junctions (#6779) After introducing the rewriter.sort_disjunctions option (#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() () #11 0x0000555555ca273d in smt::context::check(unsigned int, expr* const*, bool) () #12 0x0000555555cb166a in smt::kernel::check(unsigned int, expr* const*) () #13 0x0000555555cb9695 in (anonymous namespace)::smt_solver::check_sat_core2(unsigned int, expr* const*) () #14 0x00005555560dc0c6 in solver_na2as::check_sat_core(unsigned int, expr* const*) () #15 0x00005555560d73f3 in combined_solver::check_sat_core(unsigned int, expr* const*) () #16 0x00005555560d34e3 in solver::check_sat(unsigned int, expr* const*) () #17 0x0000555556097b26 in cmd_context::check_sat(unsigned int, expr* const*) () #18 0x0000555556082ff0 in smt2::parser::parse_check_sat() () #19 0x0000555556084dc0 in smt2::parser::parse_cmd() () #20 0x00005555560861b6 in smt2::parser::operator()() () #21 0x00005555560757e6 in parse_smt2_commands(cmd_context&, std::basic_istream<char, std::char_traits<char> >&, bool, params_ref const&, char const*) () #22 0x00005555555e8f68 in read_smtlib2_commands(char const*) () #23 0x00005555555ee6f6 in main () (gdb) ```
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
This would make my code much easier to read.
The text was updated successfully, but these errors were encountered: