Comments (4)
I'd go with a recursive function:
import Data.SBV
import Data.SBV.List
range :: SInteger -> SInteger -> SList Integer
range = smtFunction "range" $ \lo hi ->
ite (lo .> hi)
nil
(lo .: range (lo+1) hi)
Now you can say things like:
*Main> range 3 0
[] :: [SInteger]
*Main> range (-12) (-4)
[-12,-11,-10,-9,-8,-7,-6,-5,-4] :: [SInteger]
*Main> range 3 3
[3] :: [SInteger]
*Main> range 5 12
[5,6,7,8,9,10,11,12] :: [SInteger]
*Main> sat $ \a b -> Data.SBV.List.length (range a b) .== 10
Satisfiable. Model:
s0 = 14458 :: Integer
s1 = 14467 :: Integer
*Main> sat $ \a b -> Data.SBV.List.length (range a b) .== 0 .&& a .< b
Unsatisfiable
Note that this relies on recursive function definitions on the SMTLib side. What this means is that the logic becomes semi-decidable; so unless your constraints are sufficiently "simple" for the backend solver, you might end-up getting unknown
or, (more likely) the solver might run forever. For instance, if you try:
*Main> prove $ \a -> Data.SBV.List.length (range a a) .== 1
Q.E.D.
which is nice. You can even do:
*Main> prove $ \a b -> Data.SBV.List.length (range a b) .== (b - a + 1)
Falsifiable. Counter-example:
s0 = 0 :: Integer
s1 = -2 :: Integer
But the following won't terminate any time soon:
*Main> prove $ \a b -> a .<= b .=> Data.SBV.List.length (range a b) .== (b - a + 1)
... does not terminate ...
The rule-of-thumb here is that if the solver can prove the property with a finite (and not terribly large!) number of unrollings of the recursive definitions involved, it'll most likely find a model or a proof. But if the proof requires induction, the backend solver will go to an infinite loop.
Hope this helps out!
from sbv.
Aha, this is exactly what I was looking for, thank you! I had noticed smtFunction
, but the type and documentation were slightly confusing to me as to how to make use of it in a case like this one. This is very much appreciated
from sbv.
As to your note at the end, I hope we can give some kind of fact like x \in range a b <--> a <= x <= b
to the solver (and prove it somehow) and it'll be a bit more effective. I have to take a look at our application though, since this might suffice for now
from sbv.
Great.. regarding the confusing documentation: Patches are always welcome that improve the documentation or add interesting examples. Send PR's if you can!
from sbv.
Related Issues (20)
- SBV->C: Support arbitrary size bit-vectors, and in general all(?) SBV types HOT 10
- Create `NonEmpty` instances for `EqSymbolic`, `OrdSymbolic`, `Mergeable`, etc.
- Set support for cvc5 HOT 1
- ExtractIO HOT 1
- Zombie process fixes HOT 5
- Tower example
- Q: Results of 'wpProveWith' HOT 2
- Generating `Num (SBV a)` instances "generically" HOT 10
- CFP case missing in the Eq instance for CVal HOT 5
- Unsound term simplification for ite with SFloatingPoint HOT 2
- FAQ: best practices for records? HOT 4
- Explore `Iso` instances
- Consider removing `Num a => Num (SBV a)` instance
- Make OptimizeResult type dependent on OptimizeStyle HOT 3
- Let 'optimize' return variable values HOT 2
- Using uninterpreted functions in a quantified formula will not declare it in the top-level HOT 10
- Soft Question: Best approach for fixed size symbolic arrays HOT 13
- `checkSatWith` in analogy to `satWith` HOT 1
- Principle of least astonishment violated for symbolic types whose metric space type differs in representation HOT 9
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 sbv.