Comments (7)
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.
from z3.
I think C# does allow overloading of & and |. Booth are listed as overloadable operators in the documentation as well:
https://msdn.microsoft.com/en-us/library/8edha89s.aspx?f=255&MSPPError=-2147217396
Some solvers (Gurobi for example) do provide those overloads and I find them very useful.
from z3.
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.
from z3.
&& and || are evaluated by calls to & and |, respectively. Shouldn't it all just work, if you implement it this way (examples for &):
- BoolExpr & BoolExpr --> BoolExpr
- BitVecExpr & BitVecExpr --> BitVecExpr
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...
from z3.
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.
from z3.
I personally don't see the value of API consistency across programming languages. But it's ok.
from z3.
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)..
from z3.
Related Issues (20)
- reading string value from the output of z3 consequence API throws exception HOT 1
- Alternative solutions for z3-solver without using SharedArrayBuffer or COOP/COEP headers
- Semantics of "box" for "opt.priority" optimization HOT 2
- Z3 proves `(= 0.0 (^ 0 (- 2))` HOT 1
- is there an implementation available in the high level api for string variables/sorts in typescript?
- Non-deterministic correctness bug in QF_LIA optimization
- Segfault is triggered when push is before logic set
- rlimit fails to stop z3 HOT 1
- Performance on solve a logical problem about unexplained functions HOT 1
- Solving problems with formulas related to square roots HOT 1
- Multiple Segmentation Faults When Producing Proofs with "sat.euf=true tactic.default_tactic=smt..." HOT 2
- Segfault on a nested re.loop formula
- conflicts with libgc HOT 2
- Possible regression between 4.12.1 and 4.13.0 HOT 1
- Z3 does not recognize the QF_DTLIA logic HOT 1
- ASSERTION VIOLATION, File: ../src/qe/qe_mbp.cpp Line: 404 HOT 1
- `Z3_solver_reset` may not properly reset parser context
- Optimization in combination with custom data-types gives unexpected results HOT 1
- Error when using `model.completion=true` with DT
- Unexpected code reached HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from z3.