{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Arith.CAD
-- Copyright   :  (c) Masahiro Sakai 2012
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- References:
--
-- *  Christian Michaux and Adem Ozturk.
--    Quantifier Elimination following Muchnik
--    <https://math.umons.ac.be/preprints/src/Ozturk020411.pdf>
--
-- *  Arnab Bhattacharyya.
--    Something you should know about: Quantifier Elimination (Part I)
--    <http://cstheory.blogoverflow.com/2011/11/something-you-should-know-about-quantifier-elimination-part-i/>
--
-- *  Arnab Bhattacharyya.
--    Something you should know about: Quantifier Elimination (Part II)
--    <http://cstheory.blogoverflow.com/2012/02/something-you-should-know-about-quantifier-elimination-part-ii/>
--
-----------------------------------------------------------------------------
module ToySolver.Arith.CAD
  (
  -- * Basic data structures
    Point (..)
  , Cell (..)

  -- * Projection
  , project
  , project'
  , projectN
  , projectN'

  -- * Solving
  , solve
  , solve'

  -- * Model
  , 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

-- ---------------------------------------------------------------------------

-- modified reminder
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)
      -- normalizePoly前に次数が1以上で、normalizePoly結果の次数が0以下の時のための処理が必要なので注意
      [(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
  -- normalizePoly後の多項式の次数でソートしておく必要があるので注意
  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
  --trace ("collected polynomials: " ++ prettyShow ts) $ return ()
  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

-- ---------------------------------------------------------------------------