Comments (4)
easychair
commented on July 26, 2024
As Andrei pointed out, the check in SortInference.cpp could be stronger:
(2) If some of the t_i's are unifiable, the bound can be made lower.
You discussed below an example: X = Y | X = c, for which the bound is
1 since one can derive X = c from it.
However, this is further complicated by the fact that SortInference sees the FMB-proprocessed clauses. Often general splitting destroys the necessary structure as in:
I am not sure what it means, you forgot to include the example.
from vampire.
quickbeam123
commented on July 26, 2024
I just pressed Enter too early. Now, the example is in there. Sure the main trick will be to move upper bound detection after clausification but before general splitting, but with that I kind of wanted to pass the ball to @selig who knows the FMB pipeline better than me.
from vampire.
easychair
commented on July 26, 2024
The example is not there but the solution seems to be right. Not sure
though if this is likely to occur in real problems.
A
…On Wed, 20 Jul 2022 at 14:18, Martin Suda ***@***.***> wrote:
I just pressed Enter too early. Now, the example is in there. Sure the
main trick will be to move upper bound detection after clausification by
before general splitting, but with that I kind of wanted to pass the ball
to @selig <https://github.com/selig> who knows the FMB pipeline better
than me.
—
Reply to this email directly, view it on GitHub
<#398 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ABVY4BN5SKQE4DSHRBHUFMLVU7VB5ANCNFSM54C76E6A>
.
You are receiving this because you commented.Message ID:
***@***.***>
from vampire.
selig
commented on July 26, 2024
I agree it could be stronger but the current implementation should at least capture the common case, which is an explicit domain axiom using constants (e.g. X = a | X = b | X = c). Previously I tried to write a general solution and there was a bug and we removed it, leaving us without support for this simple common case (for many years).
Before we make changes I'd want to do an analysis of some real problems to see if the more general case actually occurs with any frequency.
from vampire.
Related Issues (20)
- Suboptimal job distribution on multicore HOT 4
- Join the two mechanisms that do "Unification with abstraction" around in substitution trees HOT 1
- Possible issue in substitution trees - check whether _nextVar really needs to keep growing forever HOT 3
- A bug with fmbswo was fixed by disabling the option
- Sorts in FMB are unsigned
- smt2 input not satisfiable, but preprocessed & fixed up input is HOT 7
- Imperfect Filtering HOT 8
- Parse errors for polymorphic problems HOT 4
- Skolem type in same block as term causes assertion violation. HOT 10
- Hey
- Hey
- Question about bitvector HOT 2
- Question answering HOT 10
- Lost sort information in quantifier blocks causes problems later.
- RobSubstitution::match is unsound HOT 4
- Time-out with satisfiable problems in SMT-LIB2 HOT 2
- `(expt 2 8)` induction? HOT 7
- Polymorphism and Z3 not playing nicely HOT 5
- Incorrect saturations for problems containing FOOL HOT 4
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 vampire.