This file is indexed.

/usr/share/doc/libghc-presburger-doc/html/Data-Integer-SAT.html is in libghc-presburger-doc 1.3.1-3build1.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Data.Integer.SAT</title><link href="ocean.css" rel="stylesheet" type="text/css" title="Ocean" /><script src="haddock-util.js" type="text/javascript"></script><script src="file:///usr/share/javascript/mathjax/MathJax.js" type="text/javascript"></script><script type="text/javascript">//<![CDATA[
window.onload = function () {pageLoad();setSynopsis("mini_Data-Integer-SAT.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Data-Integer-SAT.html">Source</a></li><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul><p class="caption">presburger-1.3.1: A decision procedure for quantifier-free linear arithmetic.</p></div><div id="content"><div id="module-header"><table class="info"><tr><th>Safe Haskell</th><td>Trustworthy</td></tr><tr><th>Language</th><td>Haskell98</td></tr></table><p class="caption">Data.Integer.SAT</p></div><div id="table-of-contents"><p class="caption">Contents</p><ul><li><a href="#g:1">Iterators</a></li><li><a href="#g:2">Debug</a></li><li><a href="#g:3">For QuickCheck</a></li></ul></div><div id="description"><p class="caption">Description</p><div class="doc"><p>This module implements a decision procedure for quantifier-free linear
arithmetic.  The algorithm is based on the following paper:</p><p>An Online Proof-Producing Decision Procedure for
  Mixed-Integer Linear Arithmetic
  by
  Sergey Berezin, Vijay Ganesh, and David L. Dill</p></div></div><div id="synopsis"><p id="control.syn" class="caption expander" onclick="toggleSection('syn')">Synopsis</p><ul id="section.syn" class="hide" onclick="toggleSection('syn')"><li class="src short"><span class="keyword">data</span> <a href="#t:PropSet">PropSet</a></li><li class="src short"><a href="#v:noProps">noProps</a> :: <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a></li><li class="src short"><a href="#v:checkSat">checkSat</a> :: <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> [(<a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Int.html#t:Int">Int</a>, <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a>)]</li><li class="src short"><a href="#v:assert">assert</a> :: <a href="Data-Integer-SAT.html#t:Prop">Prop</a> -&gt; <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> -&gt; <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:Prop">Prop</a><ul class="subs"><li>= <a href="#v:PTrue">PTrue</a></li><li>| <a href="#v:PFalse">PFalse</a></li><li>| <a href="Data-Integer-SAT.html#t:Prop">Prop</a> <a href="#v::-124--124-">:||</a> <a href="Data-Integer-SAT.html#t:Prop">Prop</a></li><li>| <a href="Data-Integer-SAT.html#t:Prop">Prop</a> <a href="#v::-38--38-">:&amp;&amp;</a> <a href="Data-Integer-SAT.html#t:Prop">Prop</a></li><li>| <a href="#v:Not">Not</a> <a href="Data-Integer-SAT.html#t:Prop">Prop</a></li><li>| <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a href="#v::-61--61-">:==</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a></li><li>| <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a href="#v::-47--61-">:/=</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a></li><li>| <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a href="#v::-60-">:&lt;</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a></li><li>| <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a href="#v::-62-">:&gt;</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a></li><li>| <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a href="#v::-60--61-">:&lt;=</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a></li><li>| <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a href="#v::-62--61-">:&gt;=</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a></li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:Expr">Expr</a><ul class="subs"><li>= <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a href="#v::-43-">:+</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a></li><li>| <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a href="#v::-45-">:-</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a></li><li>| <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a> <a href="#v::-42-">:*</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a></li><li>| <a href="#v:Negate">Negate</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a></li><li>| <a href="#v:Var">Var</a> <a href="Data-Integer-SAT.html#t:Name">Name</a></li><li>| <a href="#v:K">K</a> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a></li><li>| <a href="#v:If">If</a> <a href="Data-Integer-SAT.html#t:Prop">Prop</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a></li><li>| <a href="#v:Div">Div</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a></li><li>| <a href="#v:Mod">Mod</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a></li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:BoundType">BoundType</a><ul class="subs"><li>= <a href="#v:Lower">Lower</a></li><li>| <a href="#v:Upper">Upper</a></li></ul></li><li class="src short"><a href="#v:getExprBound">getExprBound</a> :: <a href="Data-Integer-SAT.html#t:BoundType">BoundType</a> -&gt; <a href="Data-Integer-SAT.html#t:Expr">Expr</a> -&gt; <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a></li><li class="src short"><a href="#v:getExprRange">getExprRange</a> :: <a href="Data-Integer-SAT.html#t:Expr">Expr</a> -&gt; <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> [<a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a>]</li><li class="src short"><span class="keyword">data</span> <a href="#t:Name">Name</a></li><li class="src short"><a href="#v:toName">toName</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Int.html#t:Int">Int</a> -&gt; <a href="Data-Integer-SAT.html#t:Name">Name</a></li><li class="src short"><a href="#v:fromName">fromName</a> :: <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Int.html#t:Int">Int</a></li><li class="src short"><a href="#v:allSolutions">allSolutions</a> :: <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> -&gt; [Solutions]</li><li class="src short"><a href="#v:slnCurrent">slnCurrent</a> :: Solutions -&gt; [(<a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Int.html#t:Int">Int</a>, <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a>)]</li><li class="src short"><a href="#v:slnNextVal">slnNextVal</a> :: Solutions -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> Solutions</li><li class="src short"><a href="#v:slnNextVar">slnNextVar</a> :: Solutions -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> Solutions</li><li class="src short"><a href="#v:slnEnumerate">slnEnumerate</a> :: Solutions -&gt; [Solutions]</li><li class="src short"><a href="#v:dotPropSet">dotPropSet</a> :: <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/pretty-1.1.3.3/Text-PrettyPrint.html#t:Doc">Doc</a></li><li class="src short"><a href="#v:sizePropSet">sizePropSet</a> :: <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> -&gt; (<a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a>, <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a>, <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a>)</li><li class="src short"><a href="#v:allInerts">allInerts</a> :: <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> -&gt; [Inerts]</li><li class="src short"><a href="#v:ppInerts">ppInerts</a> :: Inerts -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/pretty-1.1.3.3/Text-PrettyPrint.html#t:Doc">Doc</a></li><li class="src short"><a href="#v:iPickBounded">iPickBounded</a> :: <a href="Data-Integer-SAT.html#t:BoundType">BoundType</a> -&gt; [<a href="Data-Integer-SAT.html#t:Bound">Bound</a>] -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:Bound">Bound</a> = <a href="#v:Bound">Bound</a> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a> Term</li><li class="src short"><a href="#v:tConst">tConst</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a> -&gt; Term</li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><span class="keyword">data</span> <a id="t:PropSet" class="def">PropSet</a> <a href="src/Data-Integer-SAT.html#PropSet" class="link">Source</a> <a href="#t:PropSet" class="selflink">#</a></p><div class="doc"><p>A collection of propositions.</p></div><div class="subs instances"><p id="control.i:PropSet" class="caption collapser" onclick="toggleSection('i:PropSet')">Instances</p><div id="section.i:PropSet" class="show"><table><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:PropSet:Show:1" class="instance expander" onclick="toggleSection('i:id:PropSet:Show:1')"></span> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Show.html#t:Show">Show</a> <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a></span> <a href="src/Data-Integer-SAT.html#line-65" class="link">Source</a> <a href="#t:PropSet" class="selflink">#</a></td><td class="doc empty">&nbsp;</td></tr><tr><td colspan="2"><div id="section.i:id:PropSet:Show:1" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:showsPrec">showsPrec</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Int.html#t:Int">Int</a> -&gt; <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Show.html#t:ShowS">ShowS</a> <a href="#v:showsPrec" class="selflink">#</a></p><p class="src"><a href="#v:show">show</a> :: <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-String.html#t:String">String</a> <a href="#v:show" class="selflink">#</a></p><p class="src"><a href="#v:showList">showList</a> :: [<a href="Data-Integer-SAT.html#t:PropSet">PropSet</a>] -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Show.html#t:ShowS">ShowS</a> <a href="#v:showList" class="selflink">#</a></p></div></div></td></tr></table></div></div></div><div class="top"><p class="src"><a id="v:noProps" class="def">noProps</a> :: <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> <a href="src/Data-Integer-SAT.html#noProps" class="link">Source</a> <a href="#v:noProps" class="selflink">#</a></p><div class="doc"><p>An empty collection of propositions.</p></div></div><div class="top"><p class="src"><a id="v:checkSat" class="def">checkSat</a> :: <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> [(<a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Int.html#t:Int">Int</a>, <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a>)] <a href="src/Data-Integer-SAT.html#checkSat" class="link">Source</a> <a href="#v:checkSat" class="selflink">#</a></p><div class="doc"><p>Extract a model from a consistent set of propositions.
 Returns <code><a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Maybe.html#v:Nothing">Nothing</a></code> if the assertions have no model.
 If a variable does not appear in the assignment, then it is 0 (?).</p></div></div><div class="top"><p class="src"><a id="v:assert" class="def">assert</a> :: <a href="Data-Integer-SAT.html#t:Prop">Prop</a> -&gt; <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> -&gt; <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> <a href="src/Data-Integer-SAT.html#assert" class="link">Source</a> <a href="#v:assert" class="selflink">#</a></p><div class="doc"><p>Add a new proposition to an existing collection.</p></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a id="t:Prop" class="def">Prop</a> <a href="src/Data-Integer-SAT.html#Prop" class="link">Source</a> <a href="#t:Prop" class="selflink">#</a></p><div class="doc"><p>The type of proposition.</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a id="v:PTrue" class="def">PTrue</a></td><td class="doc empty">&nbsp;</td></tr><tr><td class="src"><a id="v:PFalse" class="def">PFalse</a></td><td class="doc empty">&nbsp;</td></tr><tr><td class="src"><a href="Data-Integer-SAT.html#t:Prop">Prop</a> <a id="v::-124--124-" class="def">:||</a> <a href="Data-Integer-SAT.html#t:Prop">Prop</a> <span class="fixity">infixr 2</span><span class="rightedge"></span></td><td class="doc empty">&nbsp;</td></tr><tr><td class="src"><a href="Data-Integer-SAT.html#t:Prop">Prop</a> <a id="v::-38--38-" class="def">:&amp;&amp;</a> <a href="Data-Integer-SAT.html#t:Prop">Prop</a> <span class="fixity">infixr 3</span><span class="rightedge"></span></td><td class="doc empty">&nbsp;</td></tr><tr><td class="src"><a id="v:Not" class="def">Not</a> <a href="Data-Integer-SAT.html#t:Prop">Prop</a></td><td class="doc empty">&nbsp;</td></tr><tr><td class="src"><a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a id="v::-61--61-" class="def">:==</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <span class="fixity">infix 4</span><span class="rightedge"></span></td><td class="doc empty">&nbsp;</td></tr><tr><td class="src"><a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a id="v::-47--61-" class="def">:/=</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <span class="fixity">infix 4</span><span class="rightedge"></span></td><td class="doc empty">&nbsp;</td></tr><tr><td class="src"><a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a id="v::-60-" class="def">:&lt;</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <span class="fixity">infix 4</span><span class="rightedge"></span></td><td class="doc empty">&nbsp;</td></tr><tr><td class="src"><a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a id="v::-62-" class="def">:&gt;</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <span class="fixity">infix 4</span><span class="rightedge"></span></td><td class="doc empty">&nbsp;</td></tr><tr><td class="src"><a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a id="v::-60--61-" class="def">:&lt;=</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <span class="fixity">infix 4</span><span class="rightedge"></span></td><td class="doc empty">&nbsp;</td></tr><tr><td class="src"><a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a id="v::-62--61-" class="def">:&gt;=</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <span class="fixity">infix 4</span><span class="rightedge"></span></td><td class="doc empty">&nbsp;</td></tr></table></div><div class="subs instances"><p id="control.i:Prop" class="caption collapser" onclick="toggleSection('i:Prop')">Instances</p><div id="section.i:Prop" class="show"><table><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:Prop:Read:1" class="instance expander" onclick="toggleSection('i:id:Prop:Read:1')"></span> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Read.html#t:Read">Read</a> <a href="Data-Integer-SAT.html#t:Prop">Prop</a></span> <a href="src/Data-Integer-SAT.html#line-138" class="link">Source</a> <a href="#t:Prop" class="selflink">#</a></td><td class="doc empty">&nbsp;</td></tr><tr><td colspan="2"><div id="section.i:id:Prop:Read:1" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:readsPrec">readsPrec</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Int.html#t:Int">Int</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-ParserCombinators-ReadP.html#t:ReadS">ReadS</a> <a href="Data-Integer-SAT.html#t:Prop">Prop</a> <a href="#v:readsPrec" class="selflink">#</a></p><p class="src"><a href="#v:readList">readList</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-ParserCombinators-ReadP.html#t:ReadS">ReadS</a> [<a href="Data-Integer-SAT.html#t:Prop">Prop</a>] <a href="#v:readList" class="selflink">#</a></p><p class="src"><a href="#v:readPrec">readPrec</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-ParserCombinators-ReadPrec.html#t:ReadPrec">ReadPrec</a> <a href="Data-Integer-SAT.html#t:Prop">Prop</a> <a href="#v:readPrec" class="selflink">#</a></p><p class="src"><a href="#v:readListPrec">readListPrec</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-ParserCombinators-ReadPrec.html#t:ReadPrec">ReadPrec</a> [<a href="Data-Integer-SAT.html#t:Prop">Prop</a>] <a href="#v:readListPrec" class="selflink">#</a></p></div></div></td></tr><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:Prop:Show:2" class="instance expander" onclick="toggleSection('i:id:Prop:Show:2')"></span> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Show.html#t:Show">Show</a> <a href="Data-Integer-SAT.html#t:Prop">Prop</a></span> <a href="src/Data-Integer-SAT.html#line-138" class="link">Source</a> <a href="#t:Prop" class="selflink">#</a></td><td class="doc empty">&nbsp;</td></tr><tr><td colspan="2"><div id="section.i:id:Prop:Show:2" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:showsPrec">showsPrec</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Int.html#t:Int">Int</a> -&gt; <a href="Data-Integer-SAT.html#t:Prop">Prop</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Show.html#t:ShowS">ShowS</a> <a href="#v:showsPrec" class="selflink">#</a></p><p class="src"><a href="#v:show">show</a> :: <a href="Data-Integer-SAT.html#t:Prop">Prop</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-String.html#t:String">String</a> <a href="#v:show" class="selflink">#</a></p><p class="src"><a href="#v:showList">showList</a> :: [<a href="Data-Integer-SAT.html#t:Prop">Prop</a>] -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Show.html#t:ShowS">ShowS</a> <a href="#v:showList" class="selflink">#</a></p></div></div></td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a id="t:Expr" class="def">Expr</a> <a href="src/Data-Integer-SAT.html#Expr" class="link">Source</a> <a href="#t:Expr" class="selflink">#</a></p><div class="doc"><p>The type of integer expressions.
 Variable names must be non-negative.</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a id="v::-43-" class="def">:+</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <span class="fixity">infixl 6</span><span class="rightedge"></span></td><td class="doc"><p>Addition</p></td></tr><tr><td class="src"><a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a id="v::-45-" class="def">:-</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <span class="fixity">infixl 6</span><span class="rightedge"></span></td><td class="doc"><p>Subtraction</p></td></tr><tr><td class="src"><a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a> <a id="v::-42-" class="def">:*</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <span class="fixity">infixl 7</span><span class="rightedge"></span></td><td class="doc"><p>Multiplication by a constant</p></td></tr><tr><td class="src"><a id="v:Negate" class="def">Negate</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a></td><td class="doc"><p>Negation</p></td></tr><tr><td class="src"><a id="v:Var" class="def">Var</a> <a href="Data-Integer-SAT.html#t:Name">Name</a></td><td class="doc"><p>Variable</p></td></tr><tr><td class="src"><a id="v:K" class="def">K</a> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a></td><td class="doc"><p>Constant</p></td></tr><tr><td class="src"><a id="v:If" class="def">If</a> <a href="Data-Integer-SAT.html#t:Prop">Prop</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a></td><td class="doc"><p>A conditional expression</p></td></tr><tr><td class="src"><a id="v:Div" class="def">Div</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a></td><td class="doc"><p>Division, rounds down</p></td></tr><tr><td class="src"><a id="v:Mod" class="def">Mod</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a></td><td class="doc"><p>Non-negative remainder</p></td></tr></table></div><div class="subs instances"><p id="control.i:Expr" class="caption collapser" onclick="toggleSection('i:Expr')">Instances</p><div id="section.i:Expr" class="show"><table><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:Expr:Read:1" class="instance expander" onclick="toggleSection('i:id:Expr:Read:1')"></span> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Read.html#t:Read">Read</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a></span> <a href="src/Data-Integer-SAT.html#line-151" class="link">Source</a> <a href="#t:Expr" class="selflink">#</a></td><td class="doc empty">&nbsp;</td></tr><tr><td colspan="2"><div id="section.i:id:Expr:Read:1" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:readsPrec">readsPrec</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Int.html#t:Int">Int</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-ParserCombinators-ReadP.html#t:ReadS">ReadS</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a href="#v:readsPrec" class="selflink">#</a></p><p class="src"><a href="#v:readList">readList</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-ParserCombinators-ReadP.html#t:ReadS">ReadS</a> [<a href="Data-Integer-SAT.html#t:Expr">Expr</a>] <a href="#v:readList" class="selflink">#</a></p><p class="src"><a href="#v:readPrec">readPrec</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-ParserCombinators-ReadPrec.html#t:ReadPrec">ReadPrec</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a> <a href="#v:readPrec" class="selflink">#</a></p><p class="src"><a href="#v:readListPrec">readListPrec</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-ParserCombinators-ReadPrec.html#t:ReadPrec">ReadPrec</a> [<a href="Data-Integer-SAT.html#t:Expr">Expr</a>] <a href="#v:readListPrec" class="selflink">#</a></p></div></div></td></tr><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:Expr:Show:2" class="instance expander" onclick="toggleSection('i:id:Expr:Show:2')"></span> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Show.html#t:Show">Show</a> <a href="Data-Integer-SAT.html#t:Expr">Expr</a></span> <a href="src/Data-Integer-SAT.html#line-151" class="link">Source</a> <a href="#t:Expr" class="selflink">#</a></td><td class="doc empty">&nbsp;</td></tr><tr><td colspan="2"><div id="section.i:id:Expr:Show:2" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:showsPrec">showsPrec</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Int.html#t:Int">Int</a> -&gt; <a href="Data-Integer-SAT.html#t:Expr">Expr</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Show.html#t:ShowS">ShowS</a> <a href="#v:showsPrec" class="selflink">#</a></p><p class="src"><a href="#v:show">show</a> :: <a href="Data-Integer-SAT.html#t:Expr">Expr</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-String.html#t:String">String</a> <a href="#v:show" class="selflink">#</a></p><p class="src"><a href="#v:showList">showList</a> :: [<a href="Data-Integer-SAT.html#t:Expr">Expr</a>] -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Show.html#t:ShowS">ShowS</a> <a href="#v:showList" class="selflink">#</a></p></div></div></td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a id="t:BoundType" class="def">BoundType</a> <a href="src/Data-Integer-SAT.html#BoundType" class="link">Source</a> <a href="#t:BoundType" class="selflink">#</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a id="v:Lower" class="def">Lower</a></td><td class="doc empty">&nbsp;</td></tr><tr><td class="src"><a id="v:Upper" class="def">Upper</a></td><td class="doc empty">&nbsp;</td></tr></table></div><div class="subs instances"><p id="control.i:BoundType" class="caption collapser" onclick="toggleSection('i:BoundType')">Instances</p><div id="section.i:BoundType" class="show"><table><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:BoundType:Show:1" class="instance expander" onclick="toggleSection('i:id:BoundType:Show:1')"></span> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Show.html#t:Show">Show</a> <a href="Data-Integer-SAT.html#t:BoundType">BoundType</a></span> <a href="src/Data-Integer-SAT.html#line-242" class="link">Source</a> <a href="#t:BoundType" class="selflink">#</a></td><td class="doc empty">&nbsp;</td></tr><tr><td colspan="2"><div id="section.i:id:BoundType:Show:1" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:showsPrec">showsPrec</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Int.html#t:Int">Int</a> -&gt; <a href="Data-Integer-SAT.html#t:BoundType">BoundType</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Show.html#t:ShowS">ShowS</a> <a href="#v:showsPrec" class="selflink">#</a></p><p class="src"><a href="#v:show">show</a> :: <a href="Data-Integer-SAT.html#t:BoundType">BoundType</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-String.html#t:String">String</a> <a href="#v:show" class="selflink">#</a></p><p class="src"><a href="#v:showList">showList</a> :: [<a href="Data-Integer-SAT.html#t:BoundType">BoundType</a>] -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Show.html#t:ShowS">ShowS</a> <a href="#v:showList" class="selflink">#</a></p></div></div></td></tr></table></div></div></div><div class="top"><p class="src"><a id="v:getExprBound" class="def">getExprBound</a> :: <a href="Data-Integer-SAT.html#t:BoundType">BoundType</a> -&gt; <a href="Data-Integer-SAT.html#t:Expr">Expr</a> -&gt; <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a> <a href="src/Data-Integer-SAT.html#getExprBound" class="link">Source</a> <a href="#v:getExprBound" class="selflink">#</a></p><div class="doc"><p>Computes bounds on the expression that are compatible with the model.
 Returns <code><a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Maybe.html#v:Nothing">Nothing</a></code> if the bound is not known.</p></div></div><div class="top"><p class="src"><a id="v:getExprRange" class="def">getExprRange</a> :: <a href="Data-Integer-SAT.html#t:Expr">Expr</a> -&gt; <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> [<a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a>] <a href="src/Data-Integer-SAT.html#getExprRange" class="link">Source</a> <a href="#v:getExprRange" class="selflink">#</a></p><div class="doc"><p>Compute the range of possible values for an expression.
 Returns <code><a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Maybe.html#v:Nothing">Nothing</a></code> if the bound is not known.</p></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a id="t:Name" class="def">Name</a> <a href="src/Data-Integer-SAT.html#Name" class="link">Source</a> <a href="#t:Name" class="selflink">#</a></p><div class="subs instances"><p id="control.i:Name" class="caption collapser" onclick="toggleSection('i:Name')">Instances</p><div id="section.i:Name" class="show"><table><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:Name:Eq:1" class="instance expander" onclick="toggleSection('i:id:Name:Eq:1')"></span> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Data-Integer-SAT.html#t:Name">Name</a></span> <a href="src/Data-Integer-SAT.html#line-807" class="link">Source</a> <a href="#t:Name" class="selflink">#</a></td><td class="doc empty">&nbsp;</td></tr><tr><td colspan="2"><div id="section.i:id:Name:Eq:1" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:-61--61-">(==)</a> :: <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a> <a href="#v:-61--61-" class="selflink">#</a></p><p class="src"><a href="#v:-47--61-">(/=)</a> :: <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a> <a href="#v:-47--61-" class="selflink">#</a></p></div></div></td></tr><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:Name:Ord:2" class="instance expander" onclick="toggleSection('i:id:Name:Ord:2')"></span> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Ord.html#t:Ord">Ord</a> <a href="Data-Integer-SAT.html#t:Name">Name</a></span> <a href="src/Data-Integer-SAT.html#line-807" class="link">Source</a> <a href="#t:Name" class="selflink">#</a></td><td class="doc empty">&nbsp;</td></tr><tr><td colspan="2"><div id="section.i:id:Name:Ord:2" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:compare">compare</a> :: <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Ord.html#t:Ordering">Ordering</a> <a href="#v:compare" class="selflink">#</a></p><p class="src"><a href="#v:-60-">(&lt;)</a> :: <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a> <a href="#v:-60-" class="selflink">#</a></p><p class="src"><a href="#v:-60--61-">(&lt;=)</a> :: <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a> <a href="#v:-60--61-" class="selflink">#</a></p><p class="src"><a href="#v:-62-">(&gt;)</a> :: <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a> <a href="#v:-62-" class="selflink">#</a></p><p class="src"><a href="#v:-62--61-">(&gt;=)</a> :: <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a> <a href="#v:-62--61-" class="selflink">#</a></p><p class="src"><a href="#v:max">max</a> :: <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="Data-Integer-SAT.html#t:Name">Name</a> <a href="#v:max" class="selflink">#</a></p><p class="src"><a href="#v:min">min</a> :: <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="Data-Integer-SAT.html#t:Name">Name</a> <a href="#v:min" class="selflink">#</a></p></div></div></td></tr><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:Name:Read:3" class="instance expander" onclick="toggleSection('i:id:Name:Read:3')"></span> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Read.html#t:Read">Read</a> <a href="Data-Integer-SAT.html#t:Name">Name</a></span> <a href="src/Data-Integer-SAT.html#line-807" class="link">Source</a> <a href="#t:Name" class="selflink">#</a></td><td class="doc empty">&nbsp;</td></tr><tr><td colspan="2"><div id="section.i:id:Name:Read:3" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:readsPrec">readsPrec</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Int.html#t:Int">Int</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-ParserCombinators-ReadP.html#t:ReadS">ReadS</a> <a href="Data-Integer-SAT.html#t:Name">Name</a> <a href="#v:readsPrec" class="selflink">#</a></p><p class="src"><a href="#v:readList">readList</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-ParserCombinators-ReadP.html#t:ReadS">ReadS</a> [<a href="Data-Integer-SAT.html#t:Name">Name</a>] <a href="#v:readList" class="selflink">#</a></p><p class="src"><a href="#v:readPrec">readPrec</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-ParserCombinators-ReadPrec.html#t:ReadPrec">ReadPrec</a> <a href="Data-Integer-SAT.html#t:Name">Name</a> <a href="#v:readPrec" class="selflink">#</a></p><p class="src"><a href="#v:readListPrec">readListPrec</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-ParserCombinators-ReadPrec.html#t:ReadPrec">ReadPrec</a> [<a href="Data-Integer-SAT.html#t:Name">Name</a>] <a href="#v:readListPrec" class="selflink">#</a></p></div></div></td></tr><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:Name:Show:4" class="instance expander" onclick="toggleSection('i:id:Name:Show:4')"></span> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Show.html#t:Show">Show</a> <a href="Data-Integer-SAT.html#t:Name">Name</a></span> <a href="src/Data-Integer-SAT.html#line-807" class="link">Source</a> <a href="#t:Name" class="selflink">#</a></td><td class="doc empty">&nbsp;</td></tr><tr><td colspan="2"><div id="section.i:id:Name:Show:4" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:showsPrec">showsPrec</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Int.html#t:Int">Int</a> -&gt; <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Show.html#t:ShowS">ShowS</a> <a href="#v:showsPrec" class="selflink">#</a></p><p class="src"><a href="#v:show">show</a> :: <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-String.html#t:String">String</a> <a href="#v:show" class="selflink">#</a></p><p class="src"><a href="#v:showList">showList</a> :: [<a href="Data-Integer-SAT.html#t:Name">Name</a>] -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Show.html#t:ShowS">ShowS</a> <a href="#v:showList" class="selflink">#</a></p></div></div></td></tr></table></div></div></div><div class="top"><p class="src"><a id="v:toName" class="def">toName</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Int.html#t:Int">Int</a> -&gt; <a href="Data-Integer-SAT.html#t:Name">Name</a> <a href="src/Data-Integer-SAT.html#toName" class="link">Source</a> <a href="#v:toName" class="selflink">#</a></p></div><div class="top"><p class="src"><a id="v:fromName" class="def">fromName</a> :: <a href="Data-Integer-SAT.html#t:Name">Name</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Int.html#t:Int">Int</a> <a href="src/Data-Integer-SAT.html#fromName" class="link">Source</a> <a href="#v:fromName" class="selflink">#</a></p></div><h1 id="g:1">Iterators</h1><div class="top"><p class="src"><a id="v:allSolutions" class="def">allSolutions</a> :: <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> -&gt; [Solutions] <a href="src/Data-Integer-SAT.html#allSolutions" class="link">Source</a> <a href="#v:allSolutions" class="selflink">#</a></p></div><div class="top"><p class="src"><a id="v:slnCurrent" class="def">slnCurrent</a> :: Solutions -&gt; [(<a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Int.html#t:Int">Int</a>, <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a>)] <a href="src/Data-Integer-SAT.html#slnCurrent" class="link">Source</a> <a href="#v:slnCurrent" class="selflink">#</a></p></div><div class="top"><p class="src"><a id="v:slnNextVal" class="def">slnNextVal</a> :: Solutions -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> Solutions <a href="src/Data-Integer-SAT.html#slnNextVal" class="link">Source</a> <a href="#v:slnNextVal" class="selflink">#</a></p></div><div class="top"><p class="src"><a id="v:slnNextVar" class="def">slnNextVar</a> :: Solutions -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> Solutions <a href="src/Data-Integer-SAT.html#slnNextVar" class="link">Source</a> <a href="#v:slnNextVar" class="selflink">#</a></p></div><div class="top"><p class="src"><a id="v:slnEnumerate" class="def">slnEnumerate</a> :: Solutions -&gt; [Solutions] <a href="src/Data-Integer-SAT.html#slnEnumerate" class="link">Source</a> <a href="#v:slnEnumerate" class="selflink">#</a></p></div><h1 id="g:2">Debug</h1><div class="top"><p class="src"><a id="v:dotPropSet" class="def">dotPropSet</a> :: <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/pretty-1.1.3.3/Text-PrettyPrint.html#t:Doc">Doc</a> <a href="src/Data-Integer-SAT.html#dotPropSet" class="link">Source</a> <a href="#v:dotPropSet" class="selflink">#</a></p></div><div class="top"><p class="src"><a id="v:sizePropSet" class="def">sizePropSet</a> :: <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> -&gt; (<a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a>, <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a>, <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a>) <a href="src/Data-Integer-SAT.html#sizePropSet" class="link">Source</a> <a href="#v:sizePropSet" class="selflink">#</a></p></div><div class="top"><p class="src"><a id="v:allInerts" class="def">allInerts</a> :: <a href="Data-Integer-SAT.html#t:PropSet">PropSet</a> -&gt; [Inerts] <a href="src/Data-Integer-SAT.html#allInerts" class="link">Source</a> <a href="#v:allInerts" class="selflink">#</a></p></div><div class="top"><p class="src"><a id="v:ppInerts" class="def">ppInerts</a> :: Inerts -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/pretty-1.1.3.3/Text-PrettyPrint.html#t:Doc">Doc</a> <a href="src/Data-Integer-SAT.html#ppInerts" class="link">Source</a> <a href="#v:ppInerts" class="selflink">#</a></p></div><h1 id="g:3">For QuickCheck</h1><div class="top"><p class="src"><a id="v:iPickBounded" class="def">iPickBounded</a> :: <a href="Data-Integer-SAT.html#t:BoundType">BoundType</a> -&gt; [<a href="Data-Integer-SAT.html#t:Bound">Bound</a>] -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a> <a href="src/Data-Integer-SAT.html#iPickBounded" class="link">Source</a> <a href="#v:iPickBounded" class="selflink">#</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a id="t:Bound" class="def">Bound</a> <a href="src/Data-Integer-SAT.html#Bound" class="link">Source</a> <a href="#t:Bound" class="selflink">#</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a id="v:Bound" class="def">Bound</a> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a> Term</td><td class="doc"><p>The integer is strictly positive</p></td></tr></table></div><div class="subs instances"><p id="control.i:Bound" class="caption collapser" onclick="toggleSection('i:Bound')">Instances</p><div id="section.i:Bound" class="show"><table><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:Bound:Show:1" class="instance expander" onclick="toggleSection('i:id:Bound:Show:1')"></span> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Show.html#t:Show">Show</a> <a href="Data-Integer-SAT.html#t:Bound">Bound</a></span> <a href="src/Data-Integer-SAT.html#line-239" class="link">Source</a> <a href="#t:Bound" class="selflink">#</a></td><td class="doc empty">&nbsp;</td></tr><tr><td colspan="2"><div id="section.i:id:Bound:Show:1" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:showsPrec">showsPrec</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-Int.html#t:Int">Int</a> -&gt; <a href="Data-Integer-SAT.html#t:Bound">Bound</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Show.html#t:ShowS">ShowS</a> <a href="#v:showsPrec" class="selflink">#</a></p><p class="src"><a href="#v:show">show</a> :: <a href="Data-Integer-SAT.html#t:Bound">Bound</a> -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Data-String.html#t:String">String</a> <a href="#v:show" class="selflink">#</a></p><p class="src"><a href="#v:showList">showList</a> :: [<a href="Data-Integer-SAT.html#t:Bound">Bound</a>] -&gt; <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Text-Show.html#t:ShowS">ShowS</a> <a href="#v:showList" class="selflink">#</a></p></div></div></td></tr></table></div></div></div><div class="top"><p class="src"><a id="v:tConst" class="def">tConst</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.9.1.0/Prelude.html#t:Integer">Integer</a> -&gt; Term <a href="src/Data-Integer-SAT.html#tConst" class="link">Source</a> <a href="#v:tConst" class="selflink">#</a></p><div class="doc"><p>A constant term.</p></div></div></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.17.3</p></div></body></html>