{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
module ToySolver.Arith.CAD
(
Point (..)
, Cell (..)
, project
, project'
, projectN
, projectN'
, solve
, solve'
, Model
, findSample
, evalCell
, evalPoint
) where
import Control.Exception
import Control.Monad.State
import Data.List
import Data.Maybe
import Data.Ord
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Text.Printf
import Text.PrettyPrint.HughesPJClass
import qualified Data.Interval as I
import Data.Sign (Sign (..))
import qualified Data.Sign as Sign
import ToySolver.Data.OrdRel
import ToySolver.Data.AlgebraicNumber.Real (AReal)
import qualified ToySolver.Data.AlgebraicNumber.Real as AReal
import ToySolver.Data.DNF
import ToySolver.Data.Polynomial (Polynomial, UPolynomial, X (..), PrettyVar, PrettyCoeff)
import qualified ToySolver.Data.Polynomial as P
import qualified ToySolver.Data.Polynomial.GroebnerBasis as GB
import Debug.Trace
data Point c = NegInf | RootOf (UPolynomial c) Int | PosInf
deriving (Point c -> Point c -> Bool
forall c. Eq c => Point c -> Point c -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Point c -> Point c -> Bool
$c/= :: forall c. Eq c => Point c -> Point c -> Bool
== :: Point c -> Point c -> Bool
$c== :: forall c. Eq c => Point c -> Point c -> Bool
Eq, Point c -> Point c -> Bool
Point c -> Point c -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {c}. Ord c => Eq (Point c)
forall c. Ord c => Point c -> Point c -> Bool
forall c. Ord c => Point c -> Point c -> Ordering
forall c. Ord c => Point c -> Point c -> Point c
min :: Point c -> Point c -> Point c
$cmin :: forall c. Ord c => Point c -> Point c -> Point c
max :: Point c -> Point c -> Point c
$cmax :: forall c. Ord c => Point c -> Point c -> Point c
>= :: Point c -> Point c -> Bool
$c>= :: forall c. Ord c => Point c -> Point c -> Bool
> :: Point c -> Point c -> Bool
$c> :: forall c. Ord c => Point c -> Point c -> Bool
<= :: Point c -> Point c -> Bool
$c<= :: forall c. Ord c => Point c -> Point c -> Bool
< :: Point c -> Point c -> Bool
$c< :: forall c. Ord c => Point c -> Point c -> Bool
compare :: Point c -> Point c -> Ordering
$ccompare :: forall c. Ord c => Point c -> Point c -> Ordering
Ord, Int -> Point c -> ShowS
forall c. Show c => Int -> Point c -> ShowS
forall c. Show c => [Point c] -> ShowS
forall c. Show c => Point c -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Point c] -> ShowS
$cshowList :: forall c. Show c => [Point c] -> ShowS
show :: Point c -> String
$cshow :: forall c. Show c => Point c -> String
showsPrec :: Int -> Point c -> ShowS
$cshowsPrec :: forall c. Show c => Int -> Point c -> ShowS
Show)
data Cell c
= Point (Point c)
| Interval (Point c) (Point c)
deriving (Cell c -> Cell c -> Bool
forall c. Eq c => Cell c -> Cell c -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Cell c -> Cell c -> Bool
$c/= :: forall c. Eq c => Cell c -> Cell c -> Bool
== :: Cell c -> Cell c -> Bool
$c== :: forall c. Eq c => Cell c -> Cell c -> Bool
Eq, Cell c -> Cell c -> Bool
Cell c -> Cell c -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {c}. Ord c => Eq (Cell c)
forall c. Ord c => Cell c -> Cell c -> Bool
forall c. Ord c => Cell c -> Cell c -> Ordering
forall c. Ord c => Cell c -> Cell c -> Cell c
min :: Cell c -> Cell c -> Cell c
$cmin :: forall c. Ord c => Cell c -> Cell c -> Cell c
max :: Cell c -> Cell c -> Cell c
$cmax :: forall c. Ord c => Cell c -> Cell c -> Cell c
>= :: Cell c -> Cell c -> Bool
$c>= :: forall c. Ord c => Cell c -> Cell c -> Bool
> :: Cell c -> Cell c -> Bool
$c> :: forall c. Ord c => Cell c -> Cell c -> Bool
<= :: Cell c -> Cell c -> Bool
$c<= :: forall c. Ord c => Cell c -> Cell c -> Bool
< :: Cell c -> Cell c -> Bool
$c< :: forall c. Ord c => Cell c -> Cell c -> Bool
compare :: Cell c -> Cell c -> Ordering
$ccompare :: forall c. Ord c => Cell c -> Cell c -> Ordering
Ord, Int -> Cell c -> ShowS
forall c. Show c => Int -> Cell c -> ShowS
forall c. Show c => [Cell c] -> ShowS
forall c. Show c => Cell c -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Cell c] -> ShowS
$cshowList :: forall c. Show c => [Cell c] -> ShowS
show :: Cell c -> String
$cshow :: forall c. Show c => Cell c -> String
showsPrec :: Int -> Cell c -> ShowS
$cshowsPrec :: forall c. Show c => Int -> Cell c -> ShowS
Show)
showCell :: (Num c, Ord c, PrettyCoeff c) => Cell c -> String
showCell :: forall c. (Num c, Ord c, PrettyCoeff c) => Cell c -> String
showCell (Point Point c
pt) = forall c. (Num c, Ord c, PrettyCoeff c) => Point c -> String
showPoint Point c
pt
showCell (Interval Point c
lb Point c
ub) = forall r. PrintfType r => String -> r
printf String
"(%s, %s)" (forall c. (Num c, Ord c, PrettyCoeff c) => Point c -> String
showPoint Point c
lb) (forall c. (Num c, Ord c, PrettyCoeff c) => Point c -> String
showPoint Point c
ub)
showPoint :: (Num c, Ord c, PrettyCoeff c) => Point c -> String
showPoint :: forall c. (Num c, Ord c, PrettyCoeff c) => Point c -> String
showPoint Point c
NegInf = String
"-inf"
showPoint Point c
PosInf = String
"+inf"
showPoint (RootOf UPolynomial c
p Int
n) = String
"rootOf(" forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow UPolynomial c
p forall a. [a] -> [a] -> [a]
++ String
", " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
")"
type SignConf c = [(Cell c, Map (UPolynomial c) Sign)]
emptySignConf :: SignConf c
emptySignConf :: forall c. SignConf c
emptySignConf =
[ (forall c. Point c -> Cell c
Point forall c. Point c
NegInf, forall k a. Map k a
Map.empty)
, (forall c. Point c -> Point c -> Cell c
Interval forall c. Point c
NegInf forall c. Point c
PosInf, forall k a. Map k a
Map.empty)
, (forall c. Point c -> Cell c
Point forall c. Point c
PosInf, forall k a. Map k a
Map.empty)
]
showSignConf :: forall c. (Num c, Ord c, PrettyCoeff c) => SignConf c -> [String]
showSignConf :: forall c. (Num c, Ord c, PrettyCoeff c) => SignConf c -> [String]
showSignConf = SignConf c -> [String]
f
where
f :: SignConf c -> [String]
f :: SignConf c -> [String]
f = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a b. (a -> b) -> a -> b
$ \(Cell c
cell, Map (UPolynomial c) Sign
m) -> forall c. (Num c, Ord c, PrettyCoeff c) => Cell c -> String
showCell Cell c
cell forall a. a -> [a] -> [a]
: Map (UPolynomial c) Sign -> [String]
g Map (UPolynomial c) Sign
m
g :: Map (UPolynomial c) Sign -> [String]
g :: Map (UPolynomial c) Sign -> [String]
g Map (UPolynomial c) Sign
m =
[forall r. PrintfType r => String -> r
printf String
" %s: %s" (forall a. Pretty a => a -> String
prettyShow UPolynomial c
p) (Sign -> String
Sign.symbol Sign
s) | (UPolynomial c
p, Sign
s) <- forall k a. Map k a -> [(k, a)]
Map.toList Map (UPolynomial c) Sign
m]
normalizeSignConfKey :: Ord v => UPolynomial (Polynomial Rational v) -> UPolynomial (Polynomial Rational v)
normalizeSignConfKey :: forall v.
Ord v =>
UPolynomial (Polynomial Rational v)
-> UPolynomial (Polynomial Rational v)
normalizeSignConfKey UPolynomial (Polynomial Rational v)
p
| UPolynomial (Polynomial Rational v)
p forall a. Eq a => a -> a -> Bool
== UPolynomial (Polynomial Rational v)
0 = UPolynomial (Polynomial Rational v)
0
| Bool
otherwise = UPolynomial (Polynomial Rational v)
q
where
c :: Rational
c = forall k v. Num k => MonomialOrder v -> Polynomial k v -> k
P.lc forall v. Ord v => MonomialOrder v
P.grevlex forall a b. (a -> b) -> a -> b
$ forall k v. Num k => MonomialOrder v -> Polynomial k v -> k
P.lc MonomialOrder X
P.nat UPolynomial (Polynomial Rational v)
p
q :: UPolynomial (Polynomial Rational v)
q = forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff (forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff (forall a. Fractional a => a -> a -> a
/ Rational
c)) UPolynomial (Polynomial Rational v)
p
lookupSignConf :: Ord v => UPolynomial (Polynomial Rational v) -> Map (UPolynomial (Polynomial Rational v)) Sign -> Sign
lookupSignConf :: forall v.
Ord v =>
UPolynomial (Polynomial Rational v)
-> Map (UPolynomial (Polynomial Rational v)) Sign -> Sign
lookupSignConf UPolynomial (Polynomial Rational v)
p Map (UPolynomial (Polynomial Rational v)) Sign
m
| UPolynomial (Polynomial Rational v)
p forall a. Eq a => a -> a -> Bool
== UPolynomial (Polynomial Rational v)
0 = Sign
Zero
| Bool
otherwise = forall a. Real a => a -> Sign
Sign.signOf Rational
c Sign -> Sign -> Sign
`Sign.mult` (Map (UPolynomial (Polynomial Rational v)) Sign
m forall k a. Ord k => Map k a -> k -> a
Map.! UPolynomial (Polynomial Rational v)
q)
where
c :: Rational
c = forall k v. Num k => MonomialOrder v -> Polynomial k v -> k
P.lc forall v. Ord v => MonomialOrder v
P.grevlex forall a b. (a -> b) -> a -> b
$ forall k v. Num k => MonomialOrder v -> Polynomial k v -> k
P.lc MonomialOrder X
P.nat UPolynomial (Polynomial Rational v)
p
q :: UPolynomial (Polynomial Rational v)
q = forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff (forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff (forall a. Fractional a => a -> a -> a
/ Rational
c)) UPolynomial (Polynomial Rational v)
p
mr
:: forall k. (Ord k, Show k, Num k, PrettyCoeff k)
=> UPolynomial k
-> UPolynomial k
-> (k, Integer, UPolynomial k)
mr :: forall k.
(Ord k, Show k, Num k, PrettyCoeff k) =>
UPolynomial k -> UPolynomial k -> (k, Integer, UPolynomial k)
mr Polynomial k X
p Polynomial k X
q
| Integer
n forall a. Ord a => a -> a -> Bool
>= Integer
m = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant (k
bmforall a b. (Num a, Integral b) => a -> b -> a
^(Integer
nforall a. Num a => a -> a -> a
-Integer
mforall a. Num a => a -> a -> a
+Integer
1)) forall a. Num a => a -> a -> a
* Polynomial k X
p forall a. Eq a => a -> a -> Bool
== Polynomial k X
q forall a. Num a => a -> a -> a
* Polynomial k X
l forall a. Num a => a -> a -> a
+ Polynomial k X
r Bool -> Bool -> Bool
&& Integer
m forall a. Ord a => a -> a -> Bool
> forall t. Degree t => t -> Integer
P.deg Polynomial k X
r) forall a b. (a -> b) -> a -> b
$ (k
bm, Integer
nforall a. Num a => a -> a -> a
-Integer
mforall a. Num a => a -> a -> a
+Integer
1, Polynomial k X
r)
| Bool
otherwise = forall a. (?callStack::CallStack) => String -> a
error String
"mr p q: not (deg p >= deg q)"
where
x :: Polynomial k X
x = forall a v. Var a v => v -> a
P.var X
X
n :: Integer
n = forall t. Degree t => t -> Integer
P.deg Polynomial k X
p
m :: Integer
m = forall t. Degree t => t -> Integer
P.deg Polynomial k X
q
bm :: k
bm = forall k v. Num k => MonomialOrder v -> Polynomial k v -> k
P.lc MonomialOrder X
P.nat Polynomial k X
q
(Polynomial k X
l,Polynomial k X
r) = Polynomial k X -> Integer -> (Polynomial k X, Polynomial k X)
f Polynomial k X
p Integer
n
f :: UPolynomial k -> Integer -> (UPolynomial k, UPolynomial k)
f :: Polynomial k X -> Integer -> (Polynomial k X, Polynomial k X)
f Polynomial k X
p Integer
n
| Integer
nforall a. Eq a => a -> a -> Bool
==Integer
m =
let l :: Polynomial k v
l = forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant k
an
r :: Polynomial k X
r = forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant k
bm forall a. Num a => a -> a -> a
* Polynomial k X
p forall a. Num a => a -> a -> a
- forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant k
an forall a. Num a => a -> a -> a
* Polynomial k X
q
in forall a. (?callStack::CallStack) => Bool -> a -> a
assert (forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant (k
bmforall a b. (Num a, Integral b) => a -> b -> a
^(Integer
nforall a. Num a => a -> a -> a
-Integer
mforall a. Num a => a -> a -> a
+Integer
1)) forall a. Num a => a -> a -> a
* Polynomial k X
p forall a. Eq a => a -> a -> Bool
== Polynomial k X
qforall a. Num a => a -> a -> a
*forall {v}. Polynomial k v
l forall a. Num a => a -> a -> a
+ Polynomial k X
r Bool -> Bool -> Bool
&& Integer
m forall a. Ord a => a -> a -> Bool
> forall t. Degree t => t -> Integer
P.deg Polynomial k X
r) forall a b. (a -> b) -> a -> b
$ (forall {v}. Polynomial k v
l, Polynomial k X
r)
| Bool
otherwise =
let p' :: Polynomial k X
p' = (forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant k
bm forall a. Num a => a -> a -> a
* Polynomial k X
p forall a. Num a => a -> a -> a
- forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant k
an forall a. Num a => a -> a -> a
* Polynomial k X
xforall a b. (Num a, Integral b) => a -> b -> a
^(Integer
nforall a. Num a => a -> a -> a
-Integer
m) forall a. Num a => a -> a -> a
* Polynomial k X
q)
(Polynomial k X
l',Polynomial k X
r) = Polynomial k X -> Integer -> (Polynomial k X, Polynomial k X)
f Polynomial k X
p' (Integer
nforall a. Num a => a -> a -> a
-Integer
1)
l :: Polynomial k X
l = Polynomial k X
l' forall a. Num a => a -> a -> a
+ forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant (k
anforall a. Num a => a -> a -> a
*k
bmforall a b. (Num a, Integral b) => a -> b -> a
^(Integer
nforall a. Num a => a -> a -> a
-Integer
m)) forall a. Num a => a -> a -> a
* Polynomial k X
xforall a b. (Num a, Integral b) => a -> b -> a
^(Integer
nforall a. Num a => a -> a -> a
-Integer
m)
in forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Integer
n forall a. Ord a => a -> a -> Bool
> forall t. Degree t => t -> Integer
P.deg Polynomial k X
p') forall a b. (a -> b) -> a -> b
$
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant (k
bmforall a b. (Num a, Integral b) => a -> b -> a
^(Integer
nforall a. Num a => a -> a -> a
-Integer
mforall a. Num a => a -> a -> a
+Integer
1)) forall a. Num a => a -> a -> a
* Polynomial k X
p forall a. Eq a => a -> a -> Bool
== Polynomial k X
qforall a. Num a => a -> a -> a
*Polynomial k X
l forall a. Num a => a -> a -> a
+ Polynomial k X
r Bool -> Bool -> Bool
&& Integer
m forall a. Ord a => a -> a -> Bool
> forall t. Degree t => t -> Integer
P.deg Polynomial k X
r) forall a b. (a -> b) -> a -> b
$ (Polynomial k X
l, Polynomial k X
r)
where
an :: k
an = forall k v. (Num k, Ord v) => Monomial v -> Polynomial k v -> k
P.coeff (forall a v. Var a v => v -> a
P.var X
X forall v. Ord v => Monomial v -> Integer -> Monomial v
`P.mpow` Integer
n) Polynomial k X
p
test_mr_1 :: (Coeff Int, Integer, UPolynomial (Coeff Int))
test_mr_1 :: (Coeff Int, Integer, UPolynomial (Coeff Int))
test_mr_1 = forall k.
(Ord k, Show k, Num k, PrettyCoeff k) =>
UPolynomial k -> UPolynomial k -> (k, Integer, UPolynomial k)
mr (forall k v.
(Ord k, Num k, Ord v) =>
Polynomial k v -> v -> UPolynomial (Polynomial k v)
P.toUPolynomialOf Coeff Int
p Int
3) (forall k v.
(Ord k, Num k, Ord v) =>
Polynomial k v -> v -> UPolynomial (Polynomial k v)
P.toUPolynomialOf Coeff Int
q Int
3)
where
a :: Coeff Int
a = forall a v. Var a v => v -> a
P.var Int
0
b :: Coeff Int
b = forall a v. Var a v => v -> a
P.var Int
1
c :: Coeff Int
c = forall a v. Var a v => v -> a
P.var Int
2
x :: Coeff Int
x = forall a v. Var a v => v -> a
P.var Int
3
p :: Coeff Int
p = Coeff Int
aforall a. Num a => a -> a -> a
*Coeff Int
xforall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) forall a. Num a => a -> a -> a
+ Coeff Int
bforall a. Num a => a -> a -> a
*Coeff Int
x forall a. Num a => a -> a -> a
+ Coeff Int
c
q :: Coeff Int
q = Coeff Int
2forall a. Num a => a -> a -> a
*Coeff Int
aforall a. Num a => a -> a -> a
*Coeff Int
x forall a. Num a => a -> a -> a
+ Coeff Int
b
test_mr_2 :: (Coeff Int, Integer, UPolynomial (Coeff Int))
test_mr_2 :: (Coeff Int, Integer, UPolynomial (Coeff Int))
test_mr_2 = forall k.
(Ord k, Show k, Num k, PrettyCoeff k) =>
UPolynomial k -> UPolynomial k -> (k, Integer, UPolynomial k)
mr (forall k v.
(Ord k, Num k, Ord v) =>
Polynomial k v -> v -> UPolynomial (Polynomial k v)
P.toUPolynomialOf Coeff Int
p Int
3) (forall k v.
(Ord k, Num k, Ord v) =>
Polynomial k v -> v -> UPolynomial (Polynomial k v)
P.toUPolynomialOf Coeff Int
p Int
3)
where
a :: Coeff Int
a = forall a v. Var a v => v -> a
P.var Int
0
b :: Coeff Int
b = forall a v. Var a v => v -> a
P.var Int
1
c :: Coeff Int
c = forall a v. Var a v => v -> a
P.var Int
2
x :: Coeff Int
x = forall a v. Var a v => v -> a
P.var Int
3
p :: Coeff Int
p = Coeff Int
aforall a. Num a => a -> a -> a
*Coeff Int
xforall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) forall a. Num a => a -> a -> a
+ Coeff Int
bforall a. Num a => a -> a -> a
*Coeff Int
x forall a. Num a => a -> a -> a
+ Coeff Int
c
type Coeff v = Polynomial Rational v
type M v = StateT (Assumption v) []
runM :: M v a -> [(a, Assumption v)]
runM :: forall v a. M v a -> [(a, Assumption v)]
runM M v a
m = forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT M v a
m forall v. Assumption v
emptyAssumption
assume :: (Ord v, Show v, PrettyVar v) => Polynomial Rational v -> [Sign] -> M v ()
assume :: forall v.
(Ord v, Show v, PrettyVar v) =>
Polynomial Rational v -> [Sign] -> M v ()
assume Polynomial Rational v
p [Sign]
ss = do
(Map (Polynomial Rational v) (Set Sign)
m,[Polynomial Rational v]
gb) <- forall s (m :: * -> *). MonadState s m => m s
get
Polynomial Rational v
p <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k v.
(Eq k, Fractional k, Ord v) =>
MonomialOrder v
-> Polynomial k v -> [Polynomial k v] -> Polynomial k v
P.reduce forall v. Ord v => MonomialOrder v
P.grevlex Polynomial Rational v
p [Polynomial Rational v]
gb
Set Sign
ss <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList [Sign]
ss
Set Sign
ss <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Set Sign
ss forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` forall v.
Ord v =>
Map (Polynomial Rational v) (Set Sign)
-> Polynomial Rational v -> Set Sign
computeSignSet Map (Polynomial Rational v) (Set Sign)
m Polynomial Rational v
p
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Set a -> Bool
Set.null Set Sign
ss
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall t. Degree t => t -> Integer
P.deg Polynomial Rational v
p forall a. Ord a => a -> a -> Bool
> Integer
0) forall a b. (a -> b) -> a -> b
$ do
let c :: Rational
c = forall k v. Num k => MonomialOrder v -> Polynomial k v -> k
P.lc forall v. Ord v => MonomialOrder v
P.grlex Polynomial Rational v
p
(Polynomial Rational v
p,Set Sign
ss) <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff (forall a. Fractional a => a -> a -> a
/Rational
c) Polynomial Rational v
p, forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\Sign
s -> Sign
s Sign -> Sign -> Sign
`Sign.div` forall a. Real a => a -> Sign
Sign.signOf Rational
c) Set Sign
ss)
let ss_orig :: Set Sign
ss_orig = forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Neg,Sign
Zero,Sign
Pos]) Polynomial Rational v
p Map (Polynomial Rational v) (Set Sign)
m
Set Sign
ss <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set Sign
ss Set Sign
ss_orig
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Set a -> Bool
Set.null Set Sign
ss
case forall v. Ord v => Assumption v -> Maybe (Assumption v)
propagate (forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Polynomial Rational v
p Set Sign
ss Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb) of
Maybe (Assumption v)
Nothing -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
Just Assumption v
a -> forall s (m :: * -> *). MonadState s m => s -> m ()
put Assumption v
a
project'
:: forall v. (Ord v, Show v, PrettyVar v)
=> [(UPolynomial (Polynomial Rational v), [Sign])]
-> [([(Polynomial Rational v, [Sign])], [Cell (Polynomial Rational v)])]
project' :: forall v.
(Ord v, Show v, PrettyVar v) =>
[(UPolynomial (Polynomial Rational v), [Sign])]
-> [([(Polynomial Rational v, [Sign])],
[Cell (Polynomial Rational v)])]
project' [(UPolynomial (Polynomial Rational v), [Sign])]
cs = [ (forall v.
Ord v =>
Assumption v -> [(Polynomial Rational v, [Sign])]
assumption2cond Assumption v
gs, [Cell (Polynomial Rational v)]
cells) | ([Cell (Polynomial Rational v)]
cells, Assumption v
gs) <- [([Cell (Polynomial Rational v)], Assumption v)]
result ]
where
result :: [([Cell (Polynomial Rational v)], Assumption v)]
result :: [([Cell (Polynomial Rational v)], Assumption v)]
result = forall v a. M v a -> [(a, Assumption v)]
runM forall a b. (a -> b) -> a -> b
$ do
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(UPolynomial (Polynomial Rational v), [Sign])]
cs forall a b. (a -> b) -> a -> b
$ \(UPolynomial (Polynomial Rational v)
p,[Sign]
ss) -> do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
1 forall a. Ord a => a -> a -> Bool
> forall t. Degree t => t -> Integer
P.deg UPolynomial (Polynomial Rational v)
p) forall a b. (a -> b) -> a -> b
$ forall v.
(Ord v, Show v, PrettyVar v) =>
Polynomial Rational v -> [Sign] -> M v ()
assume (forall k v. (Num k, Ord v) => Monomial v -> Polynomial k v -> k
P.coeff forall v. Monomial v
P.mone UPolynomial (Polynomial Rational v)
p) [Sign]
ss
SignConf (Polynomial Rational v)
conf <- forall v.
(Ord v, Show v, PrettyVar v) =>
[UPolynomial (Polynomial Rational v)]
-> M v (SignConf (Polynomial Rational v))
buildSignConf (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(UPolynomial (Polynomial Rational v), [Sign])]
cs)
[(UPolynomial (Polynomial Rational v), [Sign])]
cs' <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. [Maybe a] -> [a]
catMaybes forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(UPolynomial (Polynomial Rational v), [Sign])]
cs forall a b. (a -> b) -> a -> b
$ \(UPolynomial (Polynomial Rational v)
p,[Sign]
ss) -> do
UPolynomial (Polynomial Rational v)
p' <- forall v.
(Ord v, Show v, PrettyVar v) =>
UPolynomial (Polynomial Rational v)
-> M v (UPolynomial (Polynomial Rational v))
normalizePoly UPolynomial (Polynomial Rational v)
p
if (Integer
1 forall a. Ord a => a -> a -> Bool
> forall t. Degree t => t -> Integer
P.deg UPolynomial (Polynomial Rational v)
p')
then forall v.
(Ord v, Show v, PrettyVar v) =>
Polynomial Rational v -> [Sign] -> M v ()
assume (forall k v. (Num k, Ord v) => Monomial v -> Polynomial k v -> k
P.coeff forall v. Monomial v
P.mone UPolynomial (Polynomial Rational v)
p') [Sign]
ss forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
else forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (UPolynomial (Polynomial Rational v)
p',[Sign]
ss)
let satCells :: [Cell (Polynomial Rational v)]
satCells = [Cell (Polynomial Rational v)
cell | (Cell (Polynomial Rational v)
cell, Map (UPolynomial (Polynomial Rational v)) Sign
m) <- SignConf (Polynomial Rational v)
conf, Cell (Polynomial Rational v)
cell forall a. Eq a => a -> a -> Bool
/= forall c. Point c -> Cell c
Point forall c. Point c
NegInf, Cell (Polynomial Rational v)
cell forall a. Eq a => a -> a -> Bool
/= forall c. Point c -> Cell c
Point forall c. Point c
PosInf, [(UPolynomial (Polynomial Rational v), [Sign])]
-> Map (UPolynomial (Polynomial Rational v)) Sign -> Bool
ok [(UPolynomial (Polynomial Rational v), [Sign])]
cs' Map (UPolynomial (Polynomial Rational v)) Sign
m]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Cell (Polynomial Rational v)]
satCells
forall (m :: * -> *) a. Monad m => a -> m a
return [Cell (Polynomial Rational v)]
satCells
ok :: [(UPolynomial (Polynomial Rational v), [Sign])] -> Map (UPolynomial (Polynomial Rational v)) Sign -> Bool
ok :: [(UPolynomial (Polynomial Rational v), [Sign])]
-> Map (UPolynomial (Polynomial Rational v)) Sign -> Bool
ok [(UPolynomial (Polynomial Rational v), [Sign])]
cs Map (UPolynomial (Polynomial Rational v)) Sign
m = forall (t :: * -> *). Foldable t => t Bool -> Bool
and [forall {t :: * -> *} {v}.
(Foldable t, Ord v) =>
Map (UPolynomial (Polynomial Rational v)) Sign
-> UPolynomial (Polynomial Rational v) -> t Sign -> Bool
checkSign Map (UPolynomial (Polynomial Rational v)) Sign
m UPolynomial (Polynomial Rational v)
p [Sign]
ss | (UPolynomial (Polynomial Rational v)
p,[Sign]
ss) <- [(UPolynomial (Polynomial Rational v), [Sign])]
cs]
where
checkSign :: Map (UPolynomial (Polynomial Rational v)) Sign
-> UPolynomial (Polynomial Rational v) -> t Sign -> Bool
checkSign Map (UPolynomial (Polynomial Rational v)) Sign
m UPolynomial (Polynomial Rational v)
p t Sign
ss = forall v.
Ord v =>
UPolynomial (Polynomial Rational v)
-> Map (UPolynomial (Polynomial Rational v)) Sign -> Sign
lookupSignConf UPolynomial (Polynomial Rational v)
p Map (UPolynomial (Polynomial Rational v)) Sign
m forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Sign
ss
buildSignConf
:: (Ord v, Show v, PrettyVar v)
=> [UPolynomial (Polynomial Rational v)]
-> M v (SignConf (Polynomial Rational v))
buildSignConf :: forall v.
(Ord v, Show v, PrettyVar v) =>
[UPolynomial (Polynomial Rational v)]
-> M v (SignConf (Polynomial Rational v))
buildSignConf [UPolynomial (Polynomial Rational v)]
ps = do
[UPolynomial (Polynomial Rational v)]
ps2 <- forall v.
(Ord v, Show v, PrettyVar v) =>
[UPolynomial (Polynomial Rational v)]
-> M v [UPolynomial (Polynomial Rational v)]
collectPolynomials [UPolynomial (Polynomial Rational v)]
ps
let ts :: [UPolynomial (Polynomial Rational v)]
ts = forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn forall t. Degree t => t -> Integer
P.deg [UPolynomial (Polynomial Rational v)]
ps2
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall v.
(Show v, Ord v, PrettyVar v) =>
UPolynomial (Polynomial Rational v)
-> SignConf (Polynomial Rational v)
-> M v (SignConf (Polynomial Rational v))
refineSignConf) forall c. SignConf c
emptySignConf [UPolynomial (Polynomial Rational v)]
ts
collectPolynomials
:: (Ord v, Show v, PrettyVar v)
=> [UPolynomial (Polynomial Rational v)]
-> M v [UPolynomial (Polynomial Rational v)]
collectPolynomials :: forall v.
(Ord v, Show v, PrettyVar v) =>
[UPolynomial (Polynomial Rational v)]
-> M v [UPolynomial (Polynomial Rational v)]
collectPolynomials [UPolynomial (Polynomial Rational v)]
ps = forall {v}.
(Show v, PrettyVar v, Ord v) =>
Set (Polynomial (Polynomial Rational v) X)
-> Set (Polynomial (Polynomial Rational v) X)
-> StateT (Assumption v) [] [Polynomial (Polynomial Rational v) X]
go forall a. Set a
Set.empty forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall {v}.
(Ord v, Show v, PrettyVar v) =>
[Polynomial (Polynomial Rational v) X]
-> StateT
(Assumption v) [] (Set (Polynomial (Polynomial Rational v) X))
f [UPolynomial (Polynomial Rational v)]
ps
where
f :: [Polynomial (Polynomial Rational v) X]
-> StateT
(Assumption v) [] (Set (Polynomial (Polynomial Rational v) X))
f [Polynomial (Polynomial Rational v) X]
ps = do
[Polynomial (Polynomial Rational v) X]
ps' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall v.
(Ord v, Show v, PrettyVar v) =>
UPolynomial (Polynomial Rational v)
-> M v (UPolynomial (Polynomial Rational v))
normalizePoly forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ [Polynomial (Polynomial Rational v) X
p | Polynomial (Polynomial Rational v) X
p <- [Polynomial (Polynomial Rational v) X]
ps, forall t. Degree t => t -> Integer
P.deg Polynomial (Polynomial Rational v) X
p forall a. Ord a => a -> a -> Bool
> Integer
0]
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall v.
Ord v =>
UPolynomial (Polynomial Rational v)
-> UPolynomial (Polynomial Rational v)
normalizeSignConfKey forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (\Polynomial (Polynomial Rational v) X
p -> forall t. Degree t => t -> Integer
P.deg Polynomial (Polynomial Rational v) X
p forall a. Ord a => a -> a -> Bool
> Integer
0) [Polynomial (Polynomial Rational v) X]
ps'
go :: Set (Polynomial (Polynomial Rational v) X)
-> Set (Polynomial (Polynomial Rational v) X)
-> StateT (Assumption v) [] [Polynomial (Polynomial Rational v) X]
go Set (Polynomial (Polynomial Rational v) X)
result Set (Polynomial (Polynomial Rational v) X)
ps | forall a. Set a -> Bool
Set.null Set (Polynomial (Polynomial Rational v) X)
ps = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set (Polynomial (Polynomial Rational v) X)
result
go Set (Polynomial (Polynomial Rational v) X)
result Set (Polynomial (Polynomial Rational v) X)
ps = do
Set (Polynomial (Polynomial Rational v) X)
rs <- forall {v}.
(Ord v, Show v, PrettyVar v) =>
[Polynomial (Polynomial Rational v) X]
-> StateT
(Assumption v) [] (Set (Polynomial (Polynomial Rational v) X))
f [forall k v.
(Eq k, Num k, Ord v) =>
Polynomial k v -> v -> Polynomial k v
P.deriv Polynomial (Polynomial Rational v) X
p X
X | Polynomial (Polynomial Rational v) X
p <- forall a. Set a -> [a]
Set.toList Set (Polynomial (Polynomial Rational v) X)
ps]
[Set (Polynomial (Polynomial Rational v) X)]
rss <-
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Polynomial (Polynomial Rational v) X
p1,Polynomial (Polynomial Rational v) X
p2) | Polynomial (Polynomial Rational v) X
p1 <- forall a. Set a -> [a]
Set.toList Set (Polynomial (Polynomial Rational v) X)
ps, Polynomial (Polynomial Rational v) X
p2 <- forall a. Set a -> [a]
Set.toList Set (Polynomial (Polynomial Rational v) X)
ps forall a. [a] -> [a] -> [a]
++ forall a. Set a -> [a]
Set.toList Set (Polynomial (Polynomial Rational v) X)
result, Polynomial (Polynomial Rational v) X
p1 forall a. Eq a => a -> a -> Bool
/= Polynomial (Polynomial Rational v) X
p2] forall a b. (a -> b) -> a -> b
$ \(Polynomial (Polynomial Rational v) X
p1,Polynomial (Polynomial Rational v) X
p2) -> do
let d :: Integer
d = forall t. Degree t => t -> Integer
P.deg Polynomial (Polynomial Rational v) X
p1
e :: Integer
e = forall t. Degree t => t -> Integer
P.deg Polynomial (Polynomial Rational v) X
p2
forall {v}.
(Ord v, Show v, PrettyVar v) =>
[Polynomial (Polynomial Rational v) X]
-> StateT
(Assumption v) [] (Set (Polynomial (Polynomial Rational v) X))
f [Polynomial (Polynomial Rational v) X
r | (Polynomial Rational v
_,Integer
_,Polynomial (Polynomial Rational v) X
r) <- [forall k.
(Ord k, Show k, Num k, PrettyCoeff k) =>
UPolynomial k -> UPolynomial k -> (k, Integer, UPolynomial k)
mr Polynomial (Polynomial Rational v) X
p1 Polynomial (Polynomial Rational v) X
p2 | Integer
d forall a. Ord a => a -> a -> Bool
>= Integer
e] forall a. [a] -> [a] -> [a]
++ [forall k.
(Ord k, Show k, Num k, PrettyCoeff k) =>
UPolynomial k -> UPolynomial k -> (k, Integer, UPolynomial k)
mr Polynomial (Polynomial Rational v) X
p2 Polynomial (Polynomial Rational v) X
p1 | Integer
e forall a. Ord a => a -> a -> Bool
>= Integer
d]]
let ps' :: Set (Polynomial (Polynomial Rational v) X)
ps' = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (Set (Polynomial (Polynomial Rational v) X)
rsforall a. a -> [a] -> [a]
:[Set (Polynomial (Polynomial Rational v) X)]
rss)
Set (Polynomial (Polynomial Rational v) X)
-> Set (Polynomial (Polynomial Rational v) X)
-> StateT (Assumption v) [] [Polynomial (Polynomial Rational v) X]
go (Set (Polynomial (Polynomial Rational v) X)
result forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set (Polynomial (Polynomial Rational v) X)
ps) (Set (Polynomial (Polynomial Rational v) X)
ps' forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set (Polynomial (Polynomial Rational v) X)
result)
normalizePoly
:: forall v. (Ord v, Show v, PrettyVar v)
=> UPolynomial (Polynomial Rational v)
-> M v (UPolynomial (Polynomial Rational v))
normalizePoly :: forall v.
(Ord v, Show v, PrettyVar v) =>
UPolynomial (Polynomial Rational v)
-> M v (UPolynomial (Polynomial Rational v))
normalizePoly UPolynomial (Polynomial Rational v)
p = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall k v. (Eq k, Num k, Ord v) => [Term k v] -> Polynomial k v
P.fromTerms forall a b. (a -> b) -> a -> b
$ forall {v} {b}.
(Ord v, Show v, PrettyVar v) =>
[(Polynomial Rational v, b)]
-> StateT (Assumption v) [] [(Polynomial Rational v, b)]
go forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (forall a. a -> Down a
Down forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Degree t => t -> Integer
P.deg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ forall k v. Polynomial k v -> [Term k v]
P.terms UPolynomial (Polynomial Rational v)
p
where
go :: [(Polynomial Rational v, b)]
-> StateT (Assumption v) [] [(Polynomial Rational v, b)]
go [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
go xxs :: [(Polynomial Rational v, b)]
xxs@((Polynomial Rational v
c,b
d):[(Polynomial Rational v, b)]
xs) =
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus
(forall v.
(Ord v, Show v, PrettyVar v) =>
Polynomial Rational v -> [Sign] -> M v ()
assume Polynomial Rational v
c [Sign
Pos, Sign
Neg] forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return [(Polynomial Rational v, b)]
xxs)
(forall v.
(Ord v, Show v, PrettyVar v) =>
Polynomial Rational v -> [Sign] -> M v ()
assume Polynomial Rational v
c [Sign
Zero] forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [(Polynomial Rational v, b)]
-> StateT (Assumption v) [] [(Polynomial Rational v, b)]
go [(Polynomial Rational v, b)]
xs)
refineSignConf
:: forall v. (Show v, Ord v, PrettyVar v)
=> UPolynomial (Polynomial Rational v)
-> SignConf (Polynomial Rational v)
-> M v (SignConf (Polynomial Rational v))
refineSignConf :: forall v.
(Show v, Ord v, PrettyVar v) =>
UPolynomial (Polynomial Rational v)
-> SignConf (Polynomial Rational v)
-> M v (SignConf (Polynomial Rational v))
refineSignConf UPolynomial (Polynomial Rational v)
p SignConf (Polynomial Rational v)
conf = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int
-> SignConf (Polynomial Rational v)
-> SignConf (Polynomial Rational v)
extendIntervals Int
0) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Cell (Polynomial Rational v),
Map (UPolynomial (Polynomial Rational v)) Sign)
-> M v
(Cell (Polynomial Rational v),
Map (UPolynomial (Polynomial Rational v)) Sign)
extendPoint SignConf (Polynomial Rational v)
conf
where
extendPoint
:: (Cell (Polynomial Rational v), Map (UPolynomial (Polynomial Rational v)) Sign)
-> M v (Cell (Polynomial Rational v), Map (UPolynomial (Polynomial Rational v)) Sign)
extendPoint :: (Cell (Polynomial Rational v),
Map (UPolynomial (Polynomial Rational v)) Sign)
-> M v
(Cell (Polynomial Rational v),
Map (UPolynomial (Polynomial Rational v)) Sign)
extendPoint (Point Point (Polynomial Rational v)
pt, Map (UPolynomial (Polynomial Rational v)) Sign
m) = do
Sign
s <- Point (Polynomial Rational v)
-> Map (UPolynomial (Polynomial Rational v)) Sign -> M v Sign
signAt Point (Polynomial Rational v)
pt Map (UPolynomial (Polynomial Rational v)) Sign
m
forall (m :: * -> *) a. Monad m => a -> m a
return (forall c. Point c -> Cell c
Point Point (Polynomial Rational v)
pt, forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert UPolynomial (Polynomial Rational v)
p Sign
s Map (UPolynomial (Polynomial Rational v)) Sign
m)
extendPoint (Cell (Polynomial Rational v),
Map (UPolynomial (Polynomial Rational v)) Sign)
x = forall (m :: * -> *) a. Monad m => a -> m a
return (Cell (Polynomial Rational v),
Map (UPolynomial (Polynomial Rational v)) Sign)
x
extendIntervals
:: Int
-> [(Cell (Polynomial Rational v), Map (UPolynomial (Polynomial Rational v)) Sign)]
-> [(Cell (Polynomial Rational v), Map (UPolynomial (Polynomial Rational v)) Sign)]
extendIntervals :: Int
-> SignConf (Polynomial Rational v)
-> SignConf (Polynomial Rational v)
extendIntervals !Int
n (pt1 :: (Cell (Polynomial Rational v),
Map (UPolynomial (Polynomial Rational v)) Sign)
pt1@(Point Point (Polynomial Rational v)
_, Map (UPolynomial (Polynomial Rational v)) Sign
m1) : (Interval Point (Polynomial Rational v)
lb Point (Polynomial Rational v)
ub, Map (UPolynomial (Polynomial Rational v)) Sign
m) : pt2 :: (Cell (Polynomial Rational v),
Map (UPolynomial (Polynomial Rational v)) Sign)
pt2@(Point Point (Polynomial Rational v)
_, Map (UPolynomial (Polynomial Rational v)) Sign
m2) : SignConf (Polynomial Rational v)
xs) =
(Cell (Polynomial Rational v),
Map (UPolynomial (Polynomial Rational v)) Sign)
pt1 forall a. a -> [a] -> [a]
: SignConf (Polynomial Rational v)
ys forall a. [a] -> [a] -> [a]
++ Int
-> SignConf (Polynomial Rational v)
-> SignConf (Polynomial Rational v)
extendIntervals Int
n2 ((Cell (Polynomial Rational v),
Map (UPolynomial (Polynomial Rational v)) Sign)
pt2 forall a. a -> [a] -> [a]
: SignConf (Polynomial Rational v)
xs)
where
s1 :: Sign
s1 = forall v.
Ord v =>
UPolynomial (Polynomial Rational v)
-> Map (UPolynomial (Polynomial Rational v)) Sign -> Sign
lookupSignConf UPolynomial (Polynomial Rational v)
p Map (UPolynomial (Polynomial Rational v)) Sign
m1
s2 :: Sign
s2 = forall v.
Ord v =>
UPolynomial (Polynomial Rational v)
-> Map (UPolynomial (Polynomial Rational v)) Sign -> Sign
lookupSignConf UPolynomial (Polynomial Rational v)
p Map (UPolynomial (Polynomial Rational v)) Sign
m2
n1 :: Int
n1 = if Sign
s1 forall a. Eq a => a -> a -> Bool
== Sign
Zero then Int
nforall a. Num a => a -> a -> a
+Int
1 else Int
n
root :: Point (Polynomial Rational v)
root = forall c. UPolynomial c -> Int -> Point c
RootOf UPolynomial (Polynomial Rational v)
p Int
n1
(SignConf (Polynomial Rational v)
ys, Int
n2)
| Sign
s1 forall a. Eq a => a -> a -> Bool
== Sign
s2 = ( [ (forall c. Point c -> Point c -> Cell c
Interval Point (Polynomial Rational v)
lb Point (Polynomial Rational v)
ub, forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert UPolynomial (Polynomial Rational v)
p Sign
s1 Map (UPolynomial (Polynomial Rational v)) Sign
m) ], Int
n1 )
| Sign
s1 forall a. Eq a => a -> a -> Bool
== Sign
Zero = ( [ (forall c. Point c -> Point c -> Cell c
Interval Point (Polynomial Rational v)
lb Point (Polynomial Rational v)
ub, forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert UPolynomial (Polynomial Rational v)
p Sign
s2 Map (UPolynomial (Polynomial Rational v)) Sign
m) ], Int
n1 )
| Sign
s2 forall a. Eq a => a -> a -> Bool
== Sign
Zero = ( [ (forall c. Point c -> Point c -> Cell c
Interval Point (Polynomial Rational v)
lb Point (Polynomial Rational v)
ub, forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert UPolynomial (Polynomial Rational v)
p Sign
s1 Map (UPolynomial (Polynomial Rational v)) Sign
m) ], Int
n1 )
| Bool
otherwise = ( [ (forall c. Point c -> Point c -> Cell c
Interval Point (Polynomial Rational v)
lb Point (Polynomial Rational v)
root, forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert UPolynomial (Polynomial Rational v)
p Sign
s1 Map (UPolynomial (Polynomial Rational v)) Sign
m)
, (forall c. Point c -> Cell c
Point Point (Polynomial Rational v)
root, forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert UPolynomial (Polynomial Rational v)
p Sign
Zero Map (UPolynomial (Polynomial Rational v)) Sign
m)
, (forall c. Point c -> Point c -> Cell c
Interval Point (Polynomial Rational v)
root Point (Polynomial Rational v)
ub, forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert UPolynomial (Polynomial Rational v)
p Sign
s2 Map (UPolynomial (Polynomial Rational v)) Sign
m)
]
, Int
n1 forall a. Num a => a -> a -> a
+ Int
1
)
extendIntervals Int
_ SignConf (Polynomial Rational v)
xs = SignConf (Polynomial Rational v)
xs
signAt :: Point (Polynomial Rational v) -> Map (UPolynomial (Polynomial Rational v)) Sign -> M v Sign
signAt :: Point (Polynomial Rational v)
-> Map (UPolynomial (Polynomial Rational v)) Sign -> M v Sign
signAt Point (Polynomial Rational v)
PosInf Map (UPolynomial (Polynomial Rational v)) Sign
_ = Polynomial Rational v -> M v Sign
signCoeff (forall k v. Num k => MonomialOrder v -> Polynomial k v -> k
P.lc MonomialOrder X
P.nat UPolynomial (Polynomial Rational v)
p)
signAt Point (Polynomial Rational v)
NegInf Map (UPolynomial (Polynomial Rational v)) Sign
_ = do
let (Polynomial Rational v
c,Monomial X
mm) = forall k v. Num k => MonomialOrder v -> Polynomial k v -> Term k v
P.lt MonomialOrder X
P.nat UPolynomial (Polynomial Rational v)
p
if forall a. Integral a => a -> Bool
even (forall t. Degree t => t -> Integer
P.deg Monomial X
mm)
then Polynomial Rational v -> M v Sign
signCoeff Polynomial Rational v
c
else forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Sign -> Sign
Sign.negate forall a b. (a -> b) -> a -> b
$ Polynomial Rational v -> M v Sign
signCoeff Polynomial Rational v
c
signAt (RootOf UPolynomial (Polynomial Rational v)
q Int
_) Map (UPolynomial (Polynomial Rational v)) Sign
m = do
let (Polynomial Rational v
bm,Integer
k,UPolynomial (Polynomial Rational v)
r) = forall k.
(Ord k, Show k, Num k, PrettyCoeff k) =>
UPolynomial k -> UPolynomial k -> (k, Integer, UPolynomial k)
mr UPolynomial (Polynomial Rational v)
p UPolynomial (Polynomial Rational v)
q
UPolynomial (Polynomial Rational v)
r <- forall v.
(Ord v, Show v, PrettyVar v) =>
UPolynomial (Polynomial Rational v)
-> M v (UPolynomial (Polynomial Rational v))
normalizePoly UPolynomial (Polynomial Rational v)
r
Sign
s1 <- if forall t. Degree t => t -> Integer
P.deg UPolynomial (Polynomial Rational v)
r forall a. Ord a => a -> a -> Bool
> Integer
0
then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall v.
Ord v =>
UPolynomial (Polynomial Rational v)
-> Map (UPolynomial (Polynomial Rational v)) Sign -> Sign
lookupSignConf UPolynomial (Polynomial Rational v)
r Map (UPolynomial (Polynomial Rational v)) Sign
m
else Polynomial Rational v -> M v Sign
signCoeff forall a b. (a -> b) -> a -> b
$ forall k v. (Num k, Ord v) => Monomial v -> Polynomial k v -> k
P.coeff forall v. Monomial v
P.mone UPolynomial (Polynomial Rational v)
r
if forall a. Integral a => a -> Bool
even Integer
k
then forall (m :: * -> *) a. Monad m => a -> m a
return Sign
s1
else do
Sign
s2 <- Polynomial Rational v -> M v Sign
signCoeff Polynomial Rational v
bm
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sign
s1 Sign -> Sign -> Sign
`Sign.div` forall x. Integral x => Sign -> x -> Sign
Sign.pow Sign
s2 Integer
k
signCoeff :: Polynomial Rational v -> M v Sign
signCoeff :: Polynomial Rational v -> M v Sign
signCoeff Polynomial Rational v
c =
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ forall v.
(Ord v, Show v, PrettyVar v) =>
Polynomial Rational v -> [Sign] -> M v ()
assume Polynomial Rational v
c [Sign
s] forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Sign
s
| Sign
s <- [Sign
Neg, Sign
Zero, Sign
Pos]
]
type Assumption v = (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
emptyAssumption :: Assumption v
emptyAssumption :: forall v. Assumption v
emptyAssumption = (forall k a. Map k a
Map.empty, [])
propagate :: Ord v => Assumption v -> Maybe (Assumption v)
propagate :: forall v. Ord v => Assumption v -> Maybe (Assumption v)
propagate = forall v. Ord v => Assumption v -> Maybe (Assumption v)
go
where
go :: Assumption v -> Maybe (Assumption v)
go Assumption v
a = do
Assumption v
a' <- forall v. Ord v => Assumption v -> Maybe (Assumption v)
f Assumption v
a
if Assumption v
a forall a. Eq a => a -> a -> Bool
== Assumption v
a'
then forall (m :: * -> *) a. Monad m => a -> m a
return Assumption v
a
else Assumption v -> Maybe (Assumption v)
go Assumption v
a'
f :: Assumption v -> Maybe (Assumption v)
f Assumption v
a = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall v. Ord v => Assumption v -> Assumption v
dropConstants forall a b. (a -> b) -> a -> b
$ forall v. Ord v => Assumption v -> Maybe (Assumption v)
propagateSign forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall v. Ord v => Assumption v -> Maybe (Assumption v)
propagateEq Assumption v
a
propagateEq :: forall v. Ord v => Assumption v -> Maybe (Assumption v)
propagateEq :: forall v. Ord v => Assumption v -> Maybe (Assumption v)
propagateEq (Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb)
| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\(Polynomial Rational v
p,Set Sign
ss) -> forall a. a -> Set a
Set.singleton Sign
Zero forall a. Eq a => a -> a -> Bool
== Set Sign
ss) (forall k a. Map k a -> [(k, a)]
Map.toList Map (Polynomial Rational v) (Set Sign)
m) = do
(Map (Polynomial Rational v) (Set Sign)
m', [Polynomial Rational v]
gb') <- (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
-> Maybe
(Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
f (Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb)
forall v. Ord v => Assumption v -> Maybe (Assumption v)
propagateEq (Map (Polynomial Rational v) (Set Sign)
m', [Polynomial Rational v]
gb')
| Bool
otherwise =
forall (m :: * -> *) a. Monad m => a -> m a
return (Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb)
where
f :: Assumption v -> Maybe (Assumption v)
f :: (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
-> Maybe
(Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
f (Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb) =
case forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partition (forall a. a -> Set a
Set.singleton Sign
Zero forall a. Eq a => a -> a -> Bool
==) Map (Polynomial Rational v) (Set Sign)
m of
(Map (Polynomial Rational v) (Set Sign)
m0, Map (Polynomial Rational v) (Set Sign)
m) -> do
let gb' :: [Polynomial Rational v]
gb' = forall k v.
(Eq k, Fractional k, Ord k, Ord v) =>
MonomialOrder v -> [Polynomial k v] -> [Polynomial k v]
GB.basis forall v. Ord v => MonomialOrder v
P.grevlex (forall k a. Map k a -> [k]
Map.keys Map (Polynomial Rational v) (Set Sign)
m0 forall a. [a] -> [a] -> [a]
++ [Polynomial Rational v]
gb)
m' :: Map (Polynomial Rational v) (Set Sign)
m' = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. Ord a => Set a -> Set a -> Set a
Set.intersection forall a b. (a -> b) -> a -> b
$ do
(Polynomial Rational v
p,Set Sign
ss) <- forall k a. Map k a -> [(k, a)]
Map.toList Map (Polynomial Rational v) (Set Sign)
m
let p' :: Polynomial Rational v
p' = forall k v.
(Eq k, Fractional k, Ord v) =>
MonomialOrder v
-> Polynomial k v -> [Polynomial k v] -> Polynomial k v
P.reduce forall v. Ord v => MonomialOrder v
P.grevlex Polynomial Rational v
p [Polynomial Rational v]
gb'
c :: Rational
c = forall k v. Num k => MonomialOrder v -> Polynomial k v -> k
P.lc forall v. Ord v => MonomialOrder v
P.grlex Polynomial Rational v
p'
(Polynomial Rational v
p'',Set Sign
ss')
| Rational
c forall a. Eq a => a -> a -> Bool
== Rational
0 = (Polynomial Rational v
p', Set Sign
ss)
| Bool
otherwise = (forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff (forall a. Fractional a => a -> a -> a
/Rational
c) Polynomial Rational v
p', forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\Sign
s -> Sign
s Sign -> Sign -> Sign
`Sign.div` forall a. Real a => a -> Sign
Sign.signOf Rational
c) Set Sign
ss)
forall (m :: * -> *) a. Monad m => a -> m a
return (Polynomial Rational v
p'', Set Sign
ss')
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Map (Polynomial Rational v) (Set Sign)
m', [Polynomial Rational v]
gb')
propagateSign :: Ord v => Assumption v -> Maybe (Assumption v)
propagateSign :: forall v. Ord v => Assumption v -> Maybe (Assumption v)
propagateSign (Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb) = forall v. Ord v => Assumption v -> Maybe (Assumption v)
go (Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb)
where
go :: (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
-> Maybe
(Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
go a :: (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
a@(Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb)
| Bool -> Bool
not (forall v. Ord v => Assumption v -> Bool
isOkay (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
a) = forall a. Maybe a
Nothing
| Map (Polynomial Rational v) (Set Sign)
m forall a. Eq a => a -> a -> Bool
== Map (Polynomial Rational v) (Set Sign)
m' = forall a. a -> Maybe a
Just (Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb)
| Bool
otherwise = (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
-> Maybe
(Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
go (Map (Polynomial Rational v) (Set Sign)
m', [Polynomial Rational v]
gb)
where
m' :: Map (Polynomial Rational v) (Set Sign)
m' = forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (\Polynomial Rational v
p Set Sign
ss -> forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set Sign
ss (forall v.
Ord v =>
Map (Polynomial Rational v) (Set Sign)
-> Polynomial Rational v -> Set Sign
computeSignSet Map (Polynomial Rational v) (Set Sign)
m Polynomial Rational v
p)) Map (Polynomial Rational v) (Set Sign)
m
isOkay :: Ord v => Assumption v -> Bool
isOkay :: forall v. Ord v => Assumption v -> Bool
isOkay (Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb) =
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool -> Bool
not (forall a. Set a -> Bool
Set.null Set Sign
ss) | (Polynomial Rational v
_,Set Sign
ss) <- forall k a. Map k a -> [(k, a)]
Map.toList Map (Polynomial Rational v) (Set Sign)
m] Bool -> Bool -> Bool
&&
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [forall a. Ord a => a -> Set a -> Bool
Set.member Sign
Zero (forall v.
Ord v =>
Map (Polynomial Rational v) (Set Sign)
-> Polynomial Rational v -> Set Sign
computeSignSet Map (Polynomial Rational v) (Set Sign)
m Polynomial Rational v
p) | Polynomial Rational v
p <- [Polynomial Rational v]
gb]
dropConstants :: Ord v => Assumption v -> Assumption v
dropConstants :: forall v. Ord v => Assumption v -> Assumption v
dropConstants (Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb) = (forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\Polynomial Rational v
p Set Sign
_ -> forall t. Degree t => t -> Integer
P.deg Polynomial Rational v
p forall a. Ord a => a -> a -> Bool
> Integer
0) Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb)
assumption2cond :: Ord v => Assumption v -> [(Polynomial Rational v, [Sign])]
assumption2cond :: forall v.
Ord v =>
Assumption v -> [(Polynomial Rational v, [Sign])]
assumption2cond (Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb) = [(Polynomial Rational v
p, forall a. Set a -> [a]
Set.toList Set Sign
ss) | (Polynomial Rational v
p, Set Sign
ss) <- forall k a. Map k a -> [(k, a)]
Map.toList Map (Polynomial Rational v) (Set Sign)
m] forall a. [a] -> [a] -> [a]
++ [(Polynomial Rational v
p, [Sign
Zero]) | Polynomial Rational v
p <- [Polynomial Rational v]
gb]
computeSignSet :: Ord v => Map (Polynomial Rational v) (Set Sign) -> Polynomial Rational v -> Set Sign
computeSignSet :: forall v.
Ord v =>
Map (Polynomial Rational v) (Set Sign)
-> Polynomial Rational v -> Set Sign
computeSignSet Map (Polynomial Rational v) (Set Sign)
m Polynomial Rational v
p = forall k v. Num k => (v -> k) -> Polynomial k v -> k
P.eval v -> Set Sign
env (forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff forall a. Fractional a => Rational -> a
fromRational Polynomial Rational v
p)
where
env :: v -> Set Sign
env v
v =
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (forall a v. Var a v => v -> a
P.var v
v) Map (Polynomial Rational v) (Set Sign)
m of
Just Set Sign
ss -> Set Sign
ss
Maybe (Set Sign)
Nothing -> forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Neg,Sign
Zero,Sign
Pos]
type Model v = Map v AReal
findSample :: Ord v => Model v -> Cell (Polynomial Rational v) -> Maybe AReal
findSample :: forall v.
Ord v =>
Model v -> Cell (Polynomial Rational v) -> Maybe AReal
findSample Model v
m Cell (Polynomial Rational v)
cell =
case forall v.
Ord v =>
Model v -> Cell (Polynomial Rational v) -> Cell Rational
evalCell Model v
m Cell (Polynomial Rational v)
cell of
Point (RootOf UPolynomial Rational
p Int
n) ->
forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ UPolynomial Rational -> [AReal]
AReal.realRoots UPolynomial Rational
p forall a. [a] -> Int -> a
!! Int
n
Interval Point Rational
lb Point Rational
ub ->
case forall r. RealFrac r => Interval r -> Maybe Rational
I.simplestRationalWithin (Point Rational -> Extended AReal
f Point Rational
lb forall r. Ord r => Extended r -> Extended r -> Interval r
I.<..< Point Rational -> Extended AReal
f Point Rational
ub) of
Maybe Rational
Nothing -> forall a. (?callStack::CallStack) => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"ToySolver.CAD.findSample: should not happen"
Just Rational
r -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Fractional a => Rational -> a
fromRational Rational
r
where
f :: Point Rational -> I.Extended AReal
f :: Point Rational -> Extended AReal
f Point Rational
NegInf = forall r. Extended r
I.NegInf
f Point Rational
PosInf = forall r. Extended r
I.PosInf
f (RootOf UPolynomial Rational
p Int
n) = forall r. r -> Extended r
I.Finite (UPolynomial Rational -> [AReal]
AReal.realRoots UPolynomial Rational
p forall a. [a] -> Int -> a
!! Int
n)
evalCell :: Ord v => Model v -> Cell (Polynomial Rational v) -> Cell Rational
evalCell :: forall v.
Ord v =>
Model v -> Cell (Polynomial Rational v) -> Cell Rational
evalCell Model v
m (Point Point (Polynomial Rational v)
pt) = forall c. Point c -> Cell c
Point forall a b. (a -> b) -> a -> b
$ forall v.
Ord v =>
Model v -> Point (Polynomial Rational v) -> Point Rational
evalPoint Model v
m Point (Polynomial Rational v)
pt
evalCell Model v
m (Interval Point (Polynomial Rational v)
pt1 Point (Polynomial Rational v)
pt2) = forall c. Point c -> Point c -> Cell c
Interval (forall v.
Ord v =>
Model v -> Point (Polynomial Rational v) -> Point Rational
evalPoint Model v
m Point (Polynomial Rational v)
pt1) (forall v.
Ord v =>
Model v -> Point (Polynomial Rational v) -> Point Rational
evalPoint Model v
m Point (Polynomial Rational v)
pt2)
evalPoint :: Ord v => Model v -> Point (Polynomial Rational v) -> Point Rational
evalPoint :: forall v.
Ord v =>
Model v -> Point (Polynomial Rational v) -> Point Rational
evalPoint Model v
_ Point (Polynomial Rational v)
NegInf = forall c. Point c
NegInf
evalPoint Model v
_ Point (Polynomial Rational v)
PosInf = forall c. Point c
PosInf
evalPoint Model v
m (RootOf UPolynomial (Polynomial Rational v)
p Int
n) = forall c. UPolynomial c -> Int -> Point c
RootOf (AReal -> UPolynomial Rational
AReal.minimalPolynomial AReal
a) (AReal -> Int
AReal.rootIndex AReal
a)
where
a :: AReal
a = UPolynomial AReal -> [AReal]
AReal.realRootsEx (forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff (forall k v. Num k => (v -> k) -> Polynomial k v -> k
P.eval (Model v
m forall k a. Ord k => Map k a -> k -> a
Map.!) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff forall a. Fractional a => Rational -> a
fromRational) UPolynomial (Polynomial Rational v)
p) forall a. [a] -> Int -> a
!! Int
n
project
:: (Ord v, Show v, PrettyVar v)
=> v
-> [OrdRel (Polynomial Rational v)]
-> [([OrdRel (Polynomial Rational v)], Model v -> Model v)]
project :: forall v.
(Ord v, Show v, PrettyVar v) =>
v
-> [OrdRel (Polynomial Rational v)]
-> [([OrdRel (Polynomial Rational v)], Model v -> Model v)]
project v
v [OrdRel (Polynomial Rational v)]
cs = forall v.
(Ord v, Show v, PrettyVar v) =>
Set v
-> [OrdRel (Polynomial Rational v)]
-> [([OrdRel (Polynomial Rational v)], Model v -> Model v)]
projectN (forall a. a -> Set a
Set.singleton v
v) [OrdRel (Polynomial Rational v)]
cs
projectN
:: (Ord v, Show v, PrettyVar v)
=> Set v
-> [OrdRel (Polynomial Rational v)]
-> [([OrdRel (Polynomial Rational v)], Model v -> Model v)]
projectN :: forall v.
(Ord v, Show v, PrettyVar v) =>
Set v
-> [OrdRel (Polynomial Rational v)]
-> [([OrdRel (Polynomial Rational v)], Model v -> Model v)]
projectN Set v
vs [OrdRel (Polynomial Rational v)]
cs = do
([(Polynomial Rational v, [Sign])]
cs', Model v -> Model v
mt) <- forall v.
(Ord v, Show v, PrettyVar v) =>
Set v
-> [(Polynomial Rational v, [Sign])]
-> [([(Polynomial Rational v, [Sign])], Model v -> Model v)]
projectN' Set v
vs (forall a b. (a -> b) -> [a] -> [b]
map forall {a}. Num a => OrdRel a -> (a, [Sign])
f [OrdRel (Polynomial Rational v)]
cs)
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map forall {e}. Num e => (e, [Sign]) -> OrdRel e
g [(Polynomial Rational v, [Sign])]
cs', Model v -> Model v
mt)
where
f :: OrdRel a -> (a, [Sign])
f (OrdRel a
lhs RelOp
op a
rhs) = (a
lhs forall a. Num a => a -> a -> a
- a
rhs, RelOp -> [Sign]
h RelOp
op)
where
h :: RelOp -> [Sign]
h RelOp
Le = [Sign
Zero, Sign
Neg]
h RelOp
Ge = [Sign
Zero, Sign
Pos]
h RelOp
Lt = [Sign
Neg]
h RelOp
Gt = [Sign
Pos]
h RelOp
Eql = [Sign
Zero]
h RelOp
NEq = [Sign
Pos,Sign
Neg]
g :: (e, [Sign]) -> OrdRel e
g (e
p,[Sign]
ss) = (forall e. e -> RelOp -> e -> OrdRel e
OrdRel e
p RelOp
op e
0)
where
ss' :: Set Sign
ss' = forall a. Ord a => [a] -> Set a
Set.fromList [Sign]
ss
op :: RelOp
op
| Set Sign
ss' forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Zero, Sign
Neg] = RelOp
Le
| Set Sign
ss' forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Zero, Sign
Pos] = RelOp
Ge
| Set Sign
ss' forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Neg] = RelOp
Lt
| Set Sign
ss' forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Pos] = RelOp
Gt
| Set Sign
ss' forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Zero] = RelOp
Eql
| Set Sign
ss' forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Pos,Sign
Neg] = RelOp
NEq
| Bool
otherwise = forall a. (?callStack::CallStack) => String -> a
error String
"should not happen"
projectN'
:: (Ord v, Show v, PrettyVar v)
=> Set v
-> [(Polynomial Rational v, [Sign])]
-> [([(Polynomial Rational v, [Sign])], Model v -> Model v)]
projectN' :: forall v.
(Ord v, Show v, PrettyVar v) =>
Set v
-> [(Polynomial Rational v, [Sign])]
-> [([(Polynomial Rational v, [Sign])], Model v -> Model v)]
projectN' Set v
vs = forall {v}.
(Show v, PrettyVar v, Ord v) =>
[v]
-> [(Polynomial Rational v, [Sign])]
-> [([(Polynomial Rational v, [Sign])],
Map v AReal -> Map v AReal)]
loop (forall a. Set a -> [a]
Set.toList Set v
vs)
where
loop :: [v]
-> [(Polynomial Rational v, [Sign])]
-> [([(Polynomial Rational v, [Sign])],
Map v AReal -> Map v AReal)]
loop [] [(Polynomial Rational v, [Sign])]
cs = forall (m :: * -> *) a. Monad m => a -> m a
return ([(Polynomial Rational v, [Sign])]
cs, forall a. a -> a
id)
loop (v
v:[v]
vs) [(Polynomial Rational v, [Sign])]
cs = do
([(Polynomial Rational v, [Sign])]
cs2, Cell (Polynomial Rational v)
cell:[Cell (Polynomial Rational v)]
_) <- forall v.
(Ord v, Show v, PrettyVar v) =>
[(UPolynomial (Polynomial Rational v), [Sign])]
-> [([(Polynomial Rational v, [Sign])],
[Cell (Polynomial Rational v)])]
project' [(forall k v.
(Ord k, Num k, Ord v) =>
Polynomial k v -> v -> UPolynomial (Polynomial k v)
P.toUPolynomialOf Polynomial Rational v
p v
v, [Sign]
ss) | (Polynomial Rational v
p, [Sign]
ss) <- [(Polynomial Rational v, [Sign])]
cs]
let mt1 :: Map v AReal -> Map v AReal
mt1 Map v AReal
m =
let Just AReal
val = forall v.
Ord v =>
Model v -> Cell (Polynomial Rational v) -> Maybe AReal
findSample Map v AReal
m Cell (Polynomial Rational v)
cell
in seq :: forall a b. a -> b -> b
seq AReal
val forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert v
v AReal
val Map v AReal
m
([(Polynomial Rational v, [Sign])]
cs3, Map v AReal -> Map v AReal
mt2) <- [v]
-> [(Polynomial Rational v, [Sign])]
-> [([(Polynomial Rational v, [Sign])],
Map v AReal -> Map v AReal)]
loop [v]
vs [(Polynomial Rational v, [Sign])]
cs2
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Polynomial Rational v, [Sign])]
cs3, Map v AReal -> Map v AReal
mt1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map v AReal -> Map v AReal
mt2)
solve
:: forall v. (Ord v, Show v, PrettyVar v)
=> Set v
-> [(OrdRel (Polynomial Rational v))]
-> Maybe (Model v)
solve :: forall v.
(Ord v, Show v, PrettyVar v) =>
Set v -> [OrdRel (Polynomial Rational v)] -> Maybe (Model v)
solve Set v
vs [OrdRel (Polynomial Rational v)]
cs0 = forall v.
(Ord v, Show v, PrettyVar v) =>
Set v -> [(Polynomial Rational v, [Sign])] -> Maybe (Model v)
solve' Set v
vs (forall a b. (a -> b) -> [a] -> [b]
map forall {a}. Num a => OrdRel a -> (a, [Sign])
f [OrdRel (Polynomial Rational v)]
cs0)
where
f :: OrdRel a -> (a, [Sign])
f (OrdRel a
lhs RelOp
op a
rhs) = (a
lhs forall a. Num a => a -> a -> a
- a
rhs, RelOp -> [Sign]
g RelOp
op)
g :: RelOp -> [Sign]
g RelOp
Le = [Sign
Zero, Sign
Neg]
g RelOp
Ge = [Sign
Zero, Sign
Pos]
g RelOp
Lt = [Sign
Neg]
g RelOp
Gt = [Sign
Pos]
g RelOp
Eql = [Sign
Zero]
g RelOp
NEq = [Sign
Pos,Sign
Neg]
solve'
:: forall v. (Ord v, Show v, PrettyVar v)
=> Set v
-> [(Polynomial Rational v, [Sign])]
-> Maybe (Model v)
solve' :: forall v.
(Ord v, Show v, PrettyVar v) =>
Set v -> [(Polynomial Rational v, [Sign])] -> Maybe (Model v)
solve' Set v
vs [(Polynomial Rational v, [Sign])]
cs0 = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ do
([(Polynomial Rational v, [Sign])]
cs,Model v -> Model v
mt) <- forall v.
(Ord v, Show v, PrettyVar v) =>
Set v
-> [(Polynomial Rational v, [Sign])]
-> [([(Polynomial Rational v, [Sign])], Model v -> Model v)]
projectN' Set v
vs [(Polynomial Rational v, [Sign])]
cs0
let m :: Map k a
m = forall k a. Map k a
Map.empty
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Bool -> Bool
and [forall a. Real a => a -> Sign
Sign.signOf Rational
v forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Sign]
ss | (Polynomial Rational v
p,[Sign]
ss) <- [(Polynomial Rational v, [Sign])]
cs, let v :: Rational
v = forall k v. Num k => (v -> k) -> Polynomial k v -> k
P.eval (forall k a. Map k a
m forall k a. Ord k => Map k a -> k -> a
Map.!) Polynomial Rational v
p]
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Model v -> Model v
mt forall k a. Map k a
m
showDNF :: (Ord v, Show v, PrettyVar v) => DNF (Polynomial Rational v, [Sign]) -> String
showDNF :: forall v.
(Ord v, Show v, PrettyVar v) =>
DNF (Polynomial Rational v, [Sign]) -> String
showDNF (DNF [[(Polynomial Rational v, [Sign])]]
xss) = forall a. [a] -> [[a]] -> [a]
intercalate String
" | " [forall {a}. Pretty a => [(a, [Sign])] -> String
showConj [(Polynomial Rational v, [Sign])]
xs | [(Polynomial Rational v, [Sign])]
xs <- [[(Polynomial Rational v, [Sign])]]
xss]
where
showConj :: [(a, [Sign])] -> String
showConj [(a, [Sign])]
xs = String
"(" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
" & " [forall {a}. Pretty a => a -> [Sign] -> String
f a
p [Sign]
ss | (a
p,[Sign]
ss) <- [(a, [Sign])]
xs] forall a. [a] -> [a] -> [a]
++ String
")"
f :: a -> [Sign] -> String
f a
p [Sign]
ss = forall a. Pretty a => a -> String
prettyShow a
p forall a. [a] -> [a] -> [a]
++ [Sign] -> String
g [Sign]
ss
g :: [Sign] -> String
g [Sign
Zero] = String
" = 0"
g [Sign
Pos] = String
" > 0"
g [Sign
Neg] = String
" < 0"
g [Sign]
xs
| forall a. Ord a => [a] -> Set a
Set.fromList [Sign]
xs forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Pos,Sign
Neg] = String
"/= 0"
| forall a. Ord a => [a] -> Set a
Set.fromList [Sign]
xs forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Zero,Sign
Pos] = String
">= 0"
| forall a. Ord a => [a] -> Set a
Set.fromList [Sign]
xs forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Zero,Sign
Neg] = String
"<= 0"
| Bool
otherwise = forall a. (?callStack::CallStack) => String -> a
error String
"showDNF: should not happen"
dumpProjection
:: (Ord v, Show v, PrettyVar v)
=> [([(Polynomial Rational v, [Sign])], [Cell (Polynomial Rational v)])]
-> IO ()
dumpProjection :: forall v.
(Ord v, Show v, PrettyVar v) =>
[([(Polynomial Rational v, [Sign])],
[Cell (Polynomial Rational v)])]
-> IO ()
dumpProjection [([(Polynomial Rational v, [Sign])],
[Cell (Polynomial Rational v)])]
xs =
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [([(Polynomial Rational v, [Sign])],
[Cell (Polynomial Rational v)])]
xs forall a b. (a -> b) -> a -> b
$ \([(Polynomial Rational v, [Sign])]
gs, [Cell (Polynomial Rational v)]
cells) -> do
String -> IO ()
putStrLn String
"============"
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Polynomial Rational v, [Sign])]
gs forall a b. (a -> b) -> a -> b
$ \(Polynomial Rational v
p, [Sign]
ss) -> do
String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall {a}. Pretty a => a -> [Sign] -> String
f Polynomial Rational v
p [Sign]
ss
String -> IO ()
putStrLn String
" =>"
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Cell (Polynomial Rational v)]
cells forall a b. (a -> b) -> a -> b
$ \Cell (Polynomial Rational v)
cell -> do
String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall c. (Num c, Ord c, PrettyCoeff c) => Cell c -> String
showCell Cell (Polynomial Rational v)
cell
where
f :: a -> [Sign] -> String
f a
p [Sign]
ss = forall a. Pretty a => a -> String
prettyShow a
p forall a. [a] -> [a] -> [a]
++ [Sign] -> String
g [Sign]
ss
g :: [Sign] -> String
g [Sign
Zero] = String
" = 0"
g [Sign
Pos] = String
" > 0"
g [Sign
Neg] = String
" < 0"
g [Sign]
xs
| forall a. Ord a => [a] -> Set a
Set.fromList [Sign]
xs forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Pos,Sign
Neg] = String
"/= 0"
| forall a. Ord a => [a] -> Set a
Set.fromList [Sign]
xs forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Zero,Sign
Pos] = String
">= 0"
| forall a. Ord a => [a] -> Set a
Set.fromList [Sign]
xs forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Zero,Sign
Neg] = String
"<= 0"
| Bool
otherwise = forall a. (?callStack::CallStack) => String -> a
error String
"showDNF: should not happen"
dumpSignConf
:: forall v.
(Ord v, PrettyVar v, Show v)
=> [(SignConf (Polynomial Rational v), Assumption v)]
-> IO ()
dumpSignConf :: forall v.
(Ord v, PrettyVar v, Show v) =>
[(SignConf (Polynomial Rational v), Assumption v)] -> IO ()
dumpSignConf [(SignConf (Polynomial Rational v), Assumption v)]
x =
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(SignConf (Polynomial Rational v), Assumption v)]
x forall a b. (a -> b) -> a -> b
$ \(SignConf (Polynomial Rational v)
conf, Assumption v
as) -> do
String -> IO ()
putStrLn String
"============"
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall c. (Num c, Ord c, PrettyCoeff c) => SignConf c -> [String]
showSignConf SignConf (Polynomial Rational v)
conf
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall v.
Ord v =>
Assumption v -> [(Polynomial Rational v, [Sign])]
assumption2cond Assumption v
as) forall a b. (a -> b) -> a -> b
$ \(Polynomial Rational v
p, [Sign]
ss) ->
forall r. PrintfType r => String -> r
printf String
"%s %s\n" (forall a. Pretty a => a -> String
prettyShow Polynomial Rational v
p) (forall a. Show a => a -> String
show [Sign]
ss)
test1a :: IO ()
test1a :: IO ()
test1a = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall c. (Num c, Ord c, PrettyCoeff c) => SignConf c -> [String]
showSignConf SignConf (Coeff Int)
conf
where
x :: UPolynomial (Coeff Int)
x = forall a v. Var a v => v -> a
P.var X
X
ps :: [UPolynomial (Polynomial Rational Int)]
ps :: [UPolynomial (Coeff Int)]
ps = [UPolynomial (Coeff Int)
x forall a. Num a => a -> a -> a
+ UPolynomial (Coeff Int)
1, -UPolynomial (Coeff Int)
2forall a. Num a => a -> a -> a
*UPolynomial (Coeff Int)
x forall a. Num a => a -> a -> a
+ UPolynomial (Coeff Int)
3, UPolynomial (Coeff Int)
x]
[(SignConf (Coeff Int)
conf, Assumption Int
_)] = forall v a. M v a -> [(a, Assumption v)]
runM forall a b. (a -> b) -> a -> b
$ forall v.
(Ord v, Show v, PrettyVar v) =>
[UPolynomial (Polynomial Rational v)]
-> M v (SignConf (Polynomial Rational v))
buildSignConf [UPolynomial (Coeff Int)]
ps
test1b :: Bool
test1b :: Bool
test1b = forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall v.
(Ord v, Show v, PrettyVar v) =>
Set v -> [OrdRel (Polynomial Rational v)] -> Maybe (Model v)
solve Set X
vs [OrdRel (UPolynomial Rational)]
cs
where
x :: UPolynomial Rational
x = forall a v. Var a v => v -> a
P.var X
X
vs :: Set X
vs = forall a. a -> Set a
Set.singleton X
X
cs :: [OrdRel (UPolynomial Rational)]
cs = [UPolynomial Rational
x forall a. Num a => a -> a -> a
+ UPolynomial Rational
1 forall e r. IsOrdRel e r => e -> e -> r
.>. UPolynomial Rational
0, -UPolynomial Rational
2forall a. Num a => a -> a -> a
*UPolynomial Rational
x forall a. Num a => a -> a -> a
+ UPolynomial Rational
3 forall e r. IsOrdRel e r => e -> e -> r
.>. UPolynomial Rational
0, UPolynomial Rational
x forall e r. IsOrdRel e r => e -> e -> r
.>. UPolynomial Rational
0]
test1c :: Bool
test1c :: Bool
test1c = forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ do
Model X
m <- forall v.
(Ord v, Show v, PrettyVar v) =>
Set v -> [(Polynomial Rational v, [Sign])] -> Maybe (Model v)
solve' (forall a. a -> Set a
Set.singleton X
X) [(UPolynomial Rational, [Sign])]
cs
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall a b. (a -> b) -> a -> b
$ do
(UPolynomial Rational
p, [Sign]
ss) <- [(UPolynomial Rational, [Sign])]
cs
let val :: AReal
val = forall k v. Num k => (v -> k) -> Polynomial k v -> k
P.eval (Model X
m forall k a. Ord k => Map k a -> k -> a
Map.!) (forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff forall a. Fractional a => Rational -> a
fromRational UPolynomial Rational
p)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Real a => a -> Sign
Sign.signOf AReal
val forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Sign]
ss
where
x :: UPolynomial Rational
x = forall a v. Var a v => v -> a
P.var X
X
cs :: [(UPolynomial Rational, [Sign])]
cs = [(UPolynomial Rational
x forall a. Num a => a -> a -> a
+ UPolynomial Rational
1, [Sign
Pos]), (-UPolynomial Rational
2forall a. Num a => a -> a -> a
*UPolynomial Rational
x forall a. Num a => a -> a -> a
+ UPolynomial Rational
3, [Sign
Pos]), (UPolynomial Rational
x, [Sign
Pos])]
test2a :: IO ()
test2a :: IO ()
test2a = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall c. (Num c, Ord c, PrettyCoeff c) => SignConf c -> [String]
showSignConf SignConf (Coeff Int)
conf
where
x :: UPolynomial (Coeff Int)
x = forall a v. Var a v => v -> a
P.var X
X
ps :: [UPolynomial (Polynomial Rational Int)]
ps :: [UPolynomial (Coeff Int)]
ps = [UPolynomial (Coeff Int)
xforall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int)]
[(SignConf (Coeff Int)
conf, Assumption Int
_)] = forall v a. M v a -> [(a, Assumption v)]
runM forall a b. (a -> b) -> a -> b
$ forall v.
(Ord v, Show v, PrettyVar v) =>
[UPolynomial (Polynomial Rational v)]
-> M v (SignConf (Polynomial Rational v))
buildSignConf [UPolynomial (Coeff Int)]
ps
test2b :: Bool
test2b :: Bool
test2b = forall a. Maybe a -> Bool
isNothing forall a b. (a -> b) -> a -> b
$ forall v.
(Ord v, Show v, PrettyVar v) =>
Set v -> [OrdRel (Polynomial Rational v)] -> Maybe (Model v)
solve Set X
vs [OrdRel (UPolynomial Rational)]
cs
where
x :: UPolynomial Rational
x = forall a v. Var a v => v -> a
P.var X
X
vs :: Set X
vs = forall a. a -> Set a
Set.singleton X
X
cs :: [OrdRel (UPolynomial Rational)]
cs = [UPolynomial Rational
xforall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) forall e r. IsOrdRel e r => e -> e -> r
.<. UPolynomial Rational
0]
test :: Bool
test = forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool
test1b, Bool
test1c, Bool
test2b]
test_project :: DNF (Polynomial Rational Int, [Sign])
test_project :: DNF (Coeff Int, [Sign])
test_project = forall lit. [[lit]] -> DNF lit
DNF forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall v.
(Ord v, Show v, PrettyVar v) =>
[(UPolynomial (Polynomial Rational v), [Sign])]
-> [([(Polynomial Rational v, [Sign])],
[Cell (Polynomial Rational v)])]
project' [(UPolynomial (Coeff Int)
p', [Sign
Zero])]
where
a :: Coeff Int
a = forall a v. Var a v => v -> a
P.var Int
0
b :: Coeff Int
b = forall a v. Var a v => v -> a
P.var Int
1
c :: Coeff Int
c = forall a v. Var a v => v -> a
P.var Int
2
x :: Coeff Int
x = forall a v. Var a v => v -> a
P.var Int
3
p :: Polynomial Rational Int
p :: Coeff Int
p = Coeff Int
aforall a. Num a => a -> a -> a
*Coeff Int
xforall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) forall a. Num a => a -> a -> a
+ Coeff Int
bforall a. Num a => a -> a -> a
*Coeff Int
x forall a. Num a => a -> a -> a
+ Coeff Int
c
p' :: UPolynomial (Coeff Int)
p' = forall k v.
(Ord k, Num k, Ord v) =>
Polynomial k v -> v -> UPolynomial (Polynomial k v)
P.toUPolynomialOf Coeff Int
p Int
3
test_project_print :: IO ()
test_project_print :: IO ()
test_project_print = String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall v.
(Ord v, Show v, PrettyVar v) =>
DNF (Polynomial Rational v, [Sign]) -> String
showDNF forall a b. (a -> b) -> a -> b
$ DNF (Coeff Int, [Sign])
test_project
test_project_2 :: [([(Coeff Int, [Sign])], [Cell (Coeff Int)])]
test_project_2 = forall v.
(Ord v, Show v, PrettyVar v) =>
[(UPolynomial (Polynomial Rational v), [Sign])]
-> [([(Polynomial Rational v, [Sign])],
[Cell (Polynomial Rational v)])]
project' [(UPolynomial (Coeff Int)
p, [Sign
Zero]), (UPolynomial (Coeff Int)
x, [Sign
Pos])]
where
x :: UPolynomial (Coeff Int)
x = forall a v. Var a v => v -> a
P.var X
X
p :: UPolynomial (Polynomial Rational Int)
p :: UPolynomial (Coeff Int)
p = UPolynomial (Coeff Int)
xforall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) forall a. Num a => a -> a -> a
+ UPolynomial (Coeff Int)
4forall a. Num a => a -> a -> a
*UPolynomial (Coeff Int)
x forall a. Num a => a -> a -> a
- UPolynomial (Coeff Int)
10
test_project_3_print :: IO ()
test_project_3_print = forall v.
(Ord v, Show v, PrettyVar v) =>
[([(Polynomial Rational v, [Sign])],
[Cell (Polynomial Rational v)])]
-> IO ()
dumpProjection forall a b. (a -> b) -> a -> b
$ forall v.
(Ord v, Show v, PrettyVar v) =>
[(UPolynomial (Polynomial Rational v), [Sign])]
-> [([(Polynomial Rational v, [Sign])],
[Cell (Polynomial Rational v)])]
project' [(forall k v.
(Ord k, Num k, Ord v) =>
Polynomial k v -> v -> UPolynomial (Polynomial k v)
P.toUPolynomialOf Coeff Int
p Int
0, [Sign
Neg])]
where
a :: Coeff Int
a = forall a v. Var a v => v -> a
P.var Int
0
b :: Coeff Int
b = forall a v. Var a v => v -> a
P.var Int
1
c :: Coeff Int
c = forall a v. Var a v => v -> a
P.var Int
2
p :: Polynomial Rational Int
p :: Coeff Int
p = Coeff Int
aforall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) forall a. Num a => a -> a -> a
+ Coeff Int
bforall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) forall a. Num a => a -> a -> a
+ Coeff Int
cforall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) forall a. Num a => a -> a -> a
- Coeff Int
1
test_solve :: Maybe (Model Int)
test_solve = forall v.
(Ord v, Show v, PrettyVar v) =>
Set v -> [OrdRel (Polynomial Rational v)] -> Maybe (Model v)
solve Set Int
vs [Coeff Int
p forall e r. IsOrdRel e r => e -> e -> r
.<. Coeff Int
0]
where
a :: Coeff Int
a = forall a v. Var a v => v -> a
P.var Int
0
b :: Coeff Int
b = forall a v. Var a v => v -> a
P.var Int
1
c :: Coeff Int
c = forall a v. Var a v => v -> a
P.var Int
2
vs :: Set Int
vs = forall a. Ord a => [a] -> Set a
Set.fromList [Int
0,Int
1,Int
2]
p :: Polynomial Rational Int
p :: Coeff Int
p = Coeff Int
aforall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) forall a. Num a => a -> a -> a
+ Coeff Int
bforall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) forall a. Num a => a -> a -> a
+ Coeff Int
cforall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) forall a. Num a => a -> a -> a
- Coeff Int
1
test_collectPolynomials
:: [( [UPolynomial (Polynomial Rational Int)]
, Assumption Int
)]
test_collectPolynomials :: [([UPolynomial (Coeff Int)], Assumption Int)]
test_collectPolynomials = forall v a. M v a -> [(a, Assumption v)]
runM forall a b. (a -> b) -> a -> b
$ forall v.
(Ord v, Show v, PrettyVar v) =>
[UPolynomial (Polynomial Rational v)]
-> M v [UPolynomial (Polynomial Rational v)]
collectPolynomials [UPolynomial (Coeff Int)
p']
where
a :: Coeff Int
a = forall a v. Var a v => v -> a
P.var Int
0
b :: Coeff Int
b = forall a v. Var a v => v -> a
P.var Int
1
c :: Coeff Int
c = forall a v. Var a v => v -> a
P.var Int
2
x :: Coeff Int
x = forall a v. Var a v => v -> a
P.var Int
3
p :: Polynomial Rational Int
p :: Coeff Int
p = Coeff Int
aforall a. Num a => a -> a -> a
*Coeff Int
xforall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) forall a. Num a => a -> a -> a
+ Coeff Int
bforall a. Num a => a -> a -> a
*Coeff Int
x forall a. Num a => a -> a -> a
+ Coeff Int
c
p' :: UPolynomial (Coeff Int)
p' = forall k v.
(Ord k, Num k, Ord v) =>
Polynomial k v -> v -> UPolynomial (Polynomial k v)
P.toUPolynomialOf Coeff Int
p Int
3
test_collectPolynomials_print :: IO ()
test_collectPolynomials_print :: IO ()
test_collectPolynomials_print = do
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [([UPolynomial (Coeff Int)], Assumption Int)]
test_collectPolynomials forall a b. (a -> b) -> a -> b
$ \([UPolynomial (Coeff Int)]
ps,Assumption Int
g) -> do
String -> IO ()
putStrLn String
"============"
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> IO ()
putStrLn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> String
prettyShow) [UPolynomial (Coeff Int)]
ps
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall v.
Ord v =>
Assumption v -> [(Polynomial Rational v, [Sign])]
assumption2cond Assumption Int
g) forall a b. (a -> b) -> a -> b
$ \(Coeff Int
p, [Sign]
ss) ->
forall r. PrintfType r => String -> r
printf String
"%s %s\n" (forall a. Pretty a => a -> String
prettyShow Coeff Int
p) (forall a. Show a => a -> String
show [Sign]
ss)
test_buildSignConf :: [(SignConf (Polynomial Rational Int), Assumption Int)]
test_buildSignConf :: [(SignConf (Coeff Int), Assumption Int)]
test_buildSignConf = forall v a. M v a -> [(a, Assumption v)]
runM forall a b. (a -> b) -> a -> b
$ forall v.
(Ord v, Show v, PrettyVar v) =>
[UPolynomial (Polynomial Rational v)]
-> M v (SignConf (Polynomial Rational v))
buildSignConf [forall k v.
(Ord k, Num k, Ord v) =>
Polynomial k v -> v -> UPolynomial (Polynomial k v)
P.toUPolynomialOf Coeff Int
p Int
3]
where
a :: Coeff Int
a = forall a v. Var a v => v -> a
P.var Int
0
b :: Coeff Int
b = forall a v. Var a v => v -> a
P.var Int
1
c :: Coeff Int
c = forall a v. Var a v => v -> a
P.var Int
2
x :: Coeff Int
x = forall a v. Var a v => v -> a
P.var Int
3
p :: Polynomial Rational Int
p :: Coeff Int
p = Coeff Int
aforall a. Num a => a -> a -> a
*Coeff Int
xforall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) forall a. Num a => a -> a -> a
+ Coeff Int
bforall a. Num a => a -> a -> a
*Coeff Int
x forall a. Num a => a -> a -> a
+ Coeff Int
c
test_buildSignConf_print :: IO ()
test_buildSignConf_print :: IO ()
test_buildSignConf_print = forall v.
(Ord v, PrettyVar v, Show v) =>
[(SignConf (Polynomial Rational v), Assumption v)] -> IO ()
dumpSignConf [(SignConf (Coeff Int), Assumption Int)]
test_buildSignConf
test_buildSignConf_2 :: [(SignConf (Polynomial Rational Int), Assumption Int)]
test_buildSignConf_2 :: [(SignConf (Coeff Int), Assumption Int)]
test_buildSignConf_2 = forall v a. M v a -> [(a, Assumption v)]
runM forall a b. (a -> b) -> a -> b
$ forall v.
(Ord v, Show v, PrettyVar v) =>
[UPolynomial (Polynomial Rational v)]
-> M v (SignConf (Polynomial Rational v))
buildSignConf [forall k v.
(Ord k, Num k, Ord v) =>
Polynomial k v -> v -> UPolynomial (Polynomial k v)
P.toUPolynomialOf Coeff Int
p Int
0 | Coeff Int
p <- [Coeff Int]
ps]
where
x :: Coeff Int
x = forall a v. Var a v => v -> a
P.var Int
0
ps :: [Polynomial Rational Int]
ps :: [Coeff Int]
ps = [Coeff Int
x forall a. Num a => a -> a -> a
+ Coeff Int
1, -Coeff Int
2forall a. Num a => a -> a -> a
*Coeff Int
x forall a. Num a => a -> a -> a
+ Coeff Int
3, Coeff Int
x]
test_buildSignConf_2_print :: IO ()
test_buildSignConf_2_print :: IO ()
test_buildSignConf_2_print = forall v.
(Ord v, PrettyVar v, Show v) =>
[(SignConf (Polynomial Rational v), Assumption v)] -> IO ()
dumpSignConf [(SignConf (Coeff Int), Assumption Int)]
test_buildSignConf_2
test_buildSignConf_3 :: [(SignConf (Polynomial Rational Int), Assumption Int)]
test_buildSignConf_3 :: [(SignConf (Coeff Int), Assumption Int)]
test_buildSignConf_3 = forall v a. M v a -> [(a, Assumption v)]
runM forall a b. (a -> b) -> a -> b
$ forall v.
(Ord v, Show v, PrettyVar v) =>
[UPolynomial (Polynomial Rational v)]
-> M v (SignConf (Polynomial Rational v))
buildSignConf [forall k v.
(Ord k, Num k, Ord v) =>
Polynomial k v -> v -> UPolynomial (Polynomial k v)
P.toUPolynomialOf Coeff Int
p Int
0 | Coeff Int
p <- [Coeff Int]
ps]
where
x :: Coeff Int
x = forall a v. Var a v => v -> a
P.var Int
0
ps :: [Polynomial Rational Int]
ps :: [Coeff Int]
ps = [Coeff Int
x, Coeff Int
2forall a. Num a => a -> a -> a
*Coeff Int
x]
test_buildSignConf_3_print :: IO ()
test_buildSignConf_3_print :: IO ()
test_buildSignConf_3_print = forall v.
(Ord v, PrettyVar v, Show v) =>
[(SignConf (Polynomial Rational v), Assumption v)] -> IO ()
dumpSignConf [(SignConf (Coeff Int), Assumption Int)]
test_buildSignConf_3