Comments (13)
You shouldn't use an SArray
. Instead, use a regular Haskell array which stores symbolic values. (When the container is concrete, go with the concrete representation.)
So, you'd use something like: Array (Int, Int) SInteger
.
Only use an SArray
if the array itself is completely symbolic. Also, SMTLib arrays are indexed by types, not by bounds. (i.e., they're indexed by the entire domain.) This is an SMT restriction, not an SBV one.
from sbv.
Ah okay perfect, that makes sense. How would I retrieve a value based on a symbolic index in this case? If i want to write \Forall ix -> arr ! ix .== literal 1
from sbv.
You shouldn't be using symbolic indexes. (In that case you'd need an SArray
.) Once you commit to Array
, you do just your regular haskell programming. (i.e., you wouldn't do Forall
, you'd do a recursive loop and put a constraint on each element)
from sbv.
Ah ok thanks, I follow!
from sbv.
The underlying issue I really want to solve is deciding whether two array 'cells' lie in the same connected component. This would be very nicely expressed with a symbolic index:
If there isn't a way to do this with Array
is there a way to restrict the indices of SArray
?
from sbv.
You can use an SArray
if you like. You're just making the problem a bit harder for the solver, but for these sorts of puzzles It should work just fine I suppose.
You don't really need to "restrict" the indices. (You can't do it anyhow, look at how the array logic in SMT is defined: https://smt-lib.org/theories-ArraysEx.shtml). Simply program with the indices you care about and extract the values you care about. The remaining entries will go unconstrained by the solver.
I'd still suggest trying to make it work with a regular Haskell Array
, but if you really need symbolic indices then you have to use an SArray
. (But the latter is costly and harder to program with.)
from sbv.
There's a tower-puzzle solver that uses arrays filled with symbolic values: https://github.com/LeventErkok/sbv/blob/master/Documentation/SBV/Examples/Puzzles/Tower.hs
You might want to study that to see if it helps.
There's also a Sudoku solver (https://github.com/LeventErkok/sbv/blob/master/Documentation/SBV/Examples/Puzzles/Sudoku.hs) though that uses a list-of-lists..
from sbv.
Ah thanks very much. The tower puzzle looks very useful. If I were to use SArray
instead how would I go about extracting values from a SatResult
? - I'd only be concerned with a certain range of indices
from sbv.
There are several different ways to do this, but the easiest would be to use the query mode:
{-# OPTIONS_GHC -Wall -Werror #-}
module T where
import Data.SBV
import Data.SBV.Control
import Data.SBV.Tuple
example1 :: IO (Integer, Integer)
example1 = runSMT $ do
a :: SArray (Integer, Integer) Integer <- newArray_ Nothing
let a14 = a `readArray` tuple (1, 4)
a25 = a `readArray` tuple (2, 5)
constrain $ a14 + 1 .== a25
query $ do ensureSat
(,) <$> getValue a14 <*> getValue a25
This produces:
*T> example1
(-1,0)
Note that mixing arrays with quantified constraints (which is something you probably will end up doing if you use SArray
) can lead to the solver not terminating. Consider:
example2 :: IO Integer
example2 = runSMTWith z3{verbose=True} $ do
a :: SArray (Integer, Integer) Integer <- newArray_ Nothing
constrain $ \(Forall i) (Forall j) -> readArray a (tuple (i, j)) .== i+j
query $ do ensureSat
getValue (readArray a (tuple (1, 2)))
If you run this, you'll see that z3 fails to terminate. Typically, adding quantifiers to the problems will make the logic semi-decidable, which will typically lead to non-termination or unknown
answers from the solver.
This is why I'm recommending using a regular Haskell array and store symbolic values instead of SArray
. Encoding your problem that way (assuming it's possible) will lead to much easier problems for the backend solver to deal with.
from sbv.
If you want to stick to SArray
, and if you have quantifiers involved, it's best to avoid SBV's Forall
/Exists
quantifiers, and instead rely on sAll
, sAny
for a limited range. For instance, let's say we want to model an array a
, such that a[i]
equals the i
'th fibonacci number. The natural way to write this would be:
fib10 :: IO Integer
fib10 = runSMT $ do
a :: SArray Integer Integer <- newArray_ Nothing
constrain $ a `readArray` 0 .== 0
constrain $ a `readArray` 1 .== 1
constrain $ \(Forall i) ->
let aim2 = a `readArray` (i - 2)
aim1 = a `readArray` (i - 1)
ai = a `readArray` i
in ai .== aim1 + aim2
query $ do ensureSat
getValue (a `readArray` 10)
But if you run it, you'll see that the solver fails to terminate. But if you only care for a limited subset, let's say the first 50 entries only, then you can write:
fib10' :: IO Integer
fib10' = runSMT $ do
a :: SArray Integer Integer <- newArray_ Nothing
constrain $ a `readArray` 0 .== 0
constrain $ a `readArray` 1 .== 1
constrain $ flip sAll (map literal [0..49]) $ \i ->
let aim2 = a `readArray` (i - 2)
aim1 = a `readArray` (i - 1)
ai = a `readArray` i
in ai .== aim1 + aim2
query $ do ensureSat
getValue (a `readArray` 10)
And this will terminate with the correct answer 55
as the 10th fibonacci number. Obviously this'll produce (correct) but arbitrary results for values outside the range [0 .. 49]
, but sounds like bounded ranges are all you care about to start with.
To summarize: Use concrete Haskell data-structures so long as you can, storing symbolic values as elements. If you can't do that, make sure your quantification is bounded, i.e., only applies to a finite range and concrete range of the data-structure. If you can't do that either, you can still express the problem in SBV, but an SMT solver is just not the right tool for the kind of problem you're modeling. (Use a proper theorem prover instead.)
from sbv.
Ah I see, yeah concrete data structures would make more sense. Your first example I managed to make work using .=>
:
example2 :: IO Integer
example2 = runSMTWith z3 {verbose = True} $ do
a :: SArray (Integer, Integer) Integer <- newArray_ Nothing
constrain $ \(Forall i) (Forall j) -> onBoard i j .=> readArray a (tuple (i, j)) .== i + j
query $ do
ensureSat
getValue (readArray a (tuple (1, 2)))
onBoard :: SInteger -> SInteger -> SBool
onBoard x y =
sAnd
[ x .> 0,
x .< 10,
y .> 0,
y .< 10
]
However the fibonacci example doesn't:
fib10 :: IO Integer
fib10 = runSMT $ do
a :: SArray Integer Integer <- newArray_ Nothing
constrain $ a `readArray` 0 .== 0
constrain $ a `readArray` 1 .== 1
constrain $ \(Forall i) ->
let aim2 = a `readArray` (i - 2)
aim1 = a `readArray` (i - 1)
ai = a `readArray` i
in sAnd [i .>= 2, i .< 50] .=> (ai .== aim1 + aim2)
query $ do
ensureSat
getValue (a `readArray` 10)
Concrete data structure seems simpler.
from sbv.
Quantifiers are handled via e-matching and a slew of heuristics. When they'll kick in and when they won't is very hard to predict. Even different versions of z3 (or any other solver) might exhibit differing behavior. Try avoiding quantifiers as much as you can, unless absolutely necessary.
from sbv.
Guess we can close this ticket now. Feel free to reopen if you have further issues.
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
- Ranges over SIntegers HOT 4
- Let 'optimize' return variable values HOT 2
- Using uninterpreted functions in a quantified formula will not declare it in the top-level HOT 10
- `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.