Comments (7)
@joe-hauns - when you get a minute, should the current theory machinery handle this "evaluation" use case somehow in your view? Otherwise I'll close as I don't think we can do much better here at present.
from vampire.
thi all
is going to fill up the search space a lot, it's unlikely it's the best option compared to other theory instantiation options; it also works well when combined with a uwa
option.
What kind of induction are you hoping to do here (I haven't looked closely at the actual problem)? You have integers but you've picked the structural induction schedule, which is over datatypes and recursive functions (which you also have). I think just picking the induction
schedule will try and detect which kinds of induction might apply. Although I don't think any of the induction schedules make broad use of all of the arithmetic reasoning options.
from vampire.
Thanks for the hints! All I can say right now about this is that the struct_induction
schedule is significantly faster compared to the integer_induction
and induction
schedules (~33s vs ~54s on my laptop), and that there are some interesting lines that appear to be options lines e.g.
% lrs+10_1_drc=off:ind=struct:sos=theory:sstl=1:to=lpo_89 on expt.smt2 for (89ds/0Mi)
that might suggest that uwa
should be off. And without thi all
, Vampire doesn't succeed in proving in 60s "(= (expt 2 3) 8)
" much less "(= (expt 2 7) 128)
". All of this is very interesting tbh.
It's just that I'm not sure whether I can or should be poring over papers, logs and source code to see what every option does (and how small changes in the problem affect the proving process). Still, I might come back to this when I have the chance.
from vampire.
Well i don't really know anything about how we handle define-fun-rec
and how induction is being performed for such functions. I think @mezpusz knows best about that.
Recursive function mechanisms are definitely separate from the usual theory evaluation i've been working on.
from vampire.
@joe-hauns I think handling define-fun-rec
is orthogonal. If this needs the all
then it's needing to do arithmetic reasoning involving constraint solving that seems relevant to your work.... however, these are integers.
@kazarmy ... I feel your pain. The current schedules are generated based on sample problems and it sounds like your use case doesn't fall nicely into any of those sets. The issue you're facing is that some combinations of options probably weren't explored when generating those schedules so we don't see them.
If I had your problem I'd define an experiment that searched the option space to find a nice set of complementary options for a representative set of problems but that's a lot of compute and requires extra knowledge in which strategies you should be trying. Over the last 10 years we keep discussing whether this is a service we could provide to users but it's a big effort that nobody's working on.
from vampire.
Sadly I think this is something we're not expecting to work well (yet). I looked vaguely at proof search and I'd expect this to rewrite "backwards" from the goal, but it doesn't because the symbol precedence forbids it, I think.Perhaps future work with arithmetic or recursive functions will improve matters. @mezpusz I think you're the expert here, if you've got anything to add please do!
from vampire.
Sorry for the late reply! As far as I see, induction won't help here since we cannot generalize (= (expt 2 8) 256)
to any universal statement, and the arithemetic axioms + the above function definitions should be enough to solve this. I guess the proof search simply diverges due to superposition trying to expand the expt
definition which results in larger and larger terms and more and more time is spent on useless superpositions between the axioms..
from vampire.
Related Issues (20)
- Smart ep=RSTC skips congruences for introduced symbols for which it shouldn't? HOT 2
- [macOS] Build uses unsupported flags which break it: `cc1plus: error: '-fno-fat-lto-objects' are supported only with linker plugin` HOT 40
- Revive `gcov` HOT 2
- Linking error when building Debug version in Cygwin HOT 8
- Miscellanious Crashes HOT 14
- 3 tests fail on Sonoma / aarch64 HOT 3
- don't synchronise proofs if we don't print them HOT 1
- Unexpected "User error: This version cannot be used with this logic!" HOT 1
- Reimplement Lib/Set.hpp as a wrapper of std::unordered_set HOT 9
- A different operator precedence when parsing HOL? HOT 1
- FDI is really not very good and not type-safe.
- Crash on `PUZ091^5` with NewCNF HOT 4
- Bad saturation on `SYO500_8.008` HOT 11
- How make Vampire return true/false for a given problem (question)? HOT 5
- UPDR incorrect (deletes too much) in the presence of specially parsed function definitions from SMT HOT 4
- SaturationAlgorithm::addInputSOSClause is currently skipping forwardSimplify
- No proof with implies-transitive SMT problem (regression) HOT 4
- Vampire crashing when printing a finite model: HOT 1
- Printing some large proofs kills us? HOT 2
- bad test id errors 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 vampire.