{-# 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
(Point c -> Point c -> Bool)
-> (Point c -> Point c -> Bool) -> Eq (Point c)
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, Eq (Point c)
Eq (Point c)
-> (Point c -> Point c -> Ordering)
-> (Point c -> Point c -> Bool)
-> (Point c -> Point c -> Bool)
-> (Point c -> Point c -> Bool)
-> (Point c -> Point c -> Bool)
-> (Point c -> Point c -> Point c)
-> (Point c -> Point c -> Point c)
-> Ord (Point c)
Point c -> Point c -> Bool
Point c -> Point c -> Ordering
Point c -> Point c -> Point c
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
$cp1Ord :: forall c. Ord c => Eq (Point c)
Ord, Int -> Point c -> ShowS
[Point c] -> ShowS
Point c -> String
(Int -> Point c -> ShowS)
-> (Point c -> String) -> ([Point c] -> ShowS) -> Show (Point c)
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
(Cell c -> Cell c -> Bool)
-> (Cell c -> Cell c -> Bool) -> Eq (Cell c)
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, Eq (Cell c)
Eq (Cell c)
-> (Cell c -> Cell c -> Ordering)
-> (Cell c -> Cell c -> Bool)
-> (Cell c -> Cell c -> Bool)
-> (Cell c -> Cell c -> Bool)
-> (Cell c -> Cell c -> Bool)
-> (Cell c -> Cell c -> Cell c)
-> (Cell c -> Cell c -> Cell c)
-> Ord (Cell c)
Cell c -> Cell c -> Bool
Cell c -> Cell c -> Ordering
Cell c -> Cell c -> Cell c
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
$cp1Ord :: forall c. Ord c => Eq (Cell c)
Ord, Int -> Cell c -> ShowS
[Cell c] -> ShowS
Cell c -> String
(Int -> Cell c -> ShowS)
-> (Cell c -> String) -> ([Cell c] -> ShowS) -> Show (Cell c)
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 :: Cell c -> String
showCell (Point Point c
pt) = Point c -> String
forall c. (Num c, Ord c, PrettyCoeff c) => Point c -> String
showPoint Point c
pt
showCell (Interval Point c
lb Point c
ub) = String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
"(%s, %s)" (Point c -> String
forall c. (Num c, Ord c, PrettyCoeff c) => Point c -> String
showPoint Point c
lb) (Point c -> String
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 :: Point c -> String
showPoint Point c
NegInf = String
"-inf"
showPoint Point c
PosInf = String
"+inf"
showPoint (RootOf UPolynomial c
p Int
n) = String
"rootOf(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ UPolynomial c -> String
forall a. Pretty a => a -> String
prettyShow UPolynomial c
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

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

type SignConf c = [(Cell c, Map (UPolynomial c) Sign)]

emptySignConf :: SignConf c
emptySignConf :: SignConf c
emptySignConf =
  [ (Point c -> Cell c
forall c. Point c -> Cell c
Point Point c
forall c. Point c
NegInf, Map (UPolynomial c) Sign
forall k a. Map k a
Map.empty)
  , (Point c -> Point c -> Cell c
forall c. Point c -> Point c -> Cell c
Interval Point c
forall c. Point c
NegInf Point c
forall c. Point c
PosInf, Map (UPolynomial c) Sign
forall k a. Map k a
Map.empty)
  , (Point c -> Cell c
forall c. Point c -> Cell c
Point Point c
forall c. Point c
PosInf, Map (UPolynomial c) Sign
forall k a. Map k a
Map.empty)
  ]

showSignConf :: forall c. (Num c, Ord c, PrettyCoeff c) => SignConf c -> [String]
showSignConf :: SignConf c -> [String]
showSignConf = SignConf c -> [String]
f
  where
    f :: SignConf c -> [String]
    f :: SignConf c -> [String]
f = ((Cell c, Map (UPolynomial c) Sign) -> [String])
-> SignConf c -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (((Cell c, Map (UPolynomial c) Sign) -> [String])
 -> SignConf c -> [String])
-> ((Cell c, Map (UPolynomial c) Sign) -> [String])
-> SignConf c
-> [String]
forall a b. (a -> b) -> a -> b
$ \(Cell c
cell, Map (UPolynomial c) Sign
m) -> Cell c -> String
forall c. (Num c, Ord c, PrettyCoeff c) => Cell c -> String
showCell Cell c
cell String -> [String] -> [String]
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 =
      [String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
"  %s: %s" (UPolynomial c -> String
forall a. Pretty a => a -> String
prettyShow UPolynomial c
p) (Sign -> String
Sign.symbol Sign
s) | (UPolynomial c
p, Sign
s) <- Map (UPolynomial c) Sign -> [(UPolynomial c, Sign)]
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 :: UPolynomial (Polynomial Rational v)
-> UPolynomial (Polynomial Rational v)
normalizeSignConfKey UPolynomial (Polynomial Rational v)
p
  | UPolynomial (Polynomial Rational v)
p UPolynomial (Polynomial Rational v)
-> UPolynomial (Polynomial Rational v) -> Bool
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 = MonomialOrder v -> Polynomial Rational v -> Rational
forall k v. Num k => MonomialOrder v -> Polynomial k v -> k
P.lc MonomialOrder v
forall v. Ord v => MonomialOrder v
P.grevlex (Polynomial Rational v -> Rational)
-> Polynomial Rational v -> Rational
forall a b. (a -> b) -> a -> b
$ MonomialOrder X
-> UPolynomial (Polynomial Rational v) -> Polynomial Rational v
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 = (Polynomial Rational v -> Polynomial Rational v)
-> UPolynomial (Polynomial Rational v)
-> UPolynomial (Polynomial Rational v)
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff ((Rational -> Rational)
-> Polynomial Rational v -> Polynomial Rational v
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff (Rational -> Rational -> Rational
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 :: 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 UPolynomial (Polynomial Rational v)
-> UPolynomial (Polynomial Rational v) -> Bool
forall a. Eq a => a -> a -> Bool
== UPolynomial (Polynomial Rational v)
0    = Sign
Zero
  | Bool
otherwise = Rational -> Sign
forall a. Real a => a -> Sign
Sign.signOf Rational
c Sign -> Sign -> Sign
`Sign.mult` (Map (UPolynomial (Polynomial Rational v)) Sign
m Map (UPolynomial (Polynomial Rational v)) Sign
-> UPolynomial (Polynomial Rational v) -> Sign
forall k a. Ord k => Map k a -> k -> a
Map.! UPolynomial (Polynomial Rational v)
q)
  where
    c :: Rational
c = MonomialOrder v -> Polynomial Rational v -> Rational
forall k v. Num k => MonomialOrder v -> Polynomial k v -> k
P.lc MonomialOrder v
forall v. Ord v => MonomialOrder v
P.grevlex (Polynomial Rational v -> Rational)
-> Polynomial Rational v -> Rational
forall a b. (a -> b) -> a -> b
$ MonomialOrder X
-> UPolynomial (Polynomial Rational v) -> Polynomial Rational v
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 = (Polynomial Rational v -> Polynomial Rational v)
-> UPolynomial (Polynomial Rational v)
-> UPolynomial (Polynomial Rational v)
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff ((Rational -> Rational)
-> Polynomial Rational v -> Polynomial Rational v
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff (Rational -> Rational -> Rational
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 :: UPolynomial k -> UPolynomial k -> (k, Integer, UPolynomial k)
mr UPolynomial k
p UPolynomial k
q
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
m    = Bool -> (k, Integer, UPolynomial k) -> (k, Integer, UPolynomial k)
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (k -> UPolynomial k
forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant (k
bmk -> Integer -> k
forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1)) UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
* UPolynomial k
p UPolynomial k -> UPolynomial k -> Bool
forall a. Eq a => a -> a -> Bool
== UPolynomial k
q UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
* UPolynomial k
l UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
+ UPolynomial k
r Bool -> Bool -> Bool
&& Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> UPolynomial k -> Integer
forall t. Degree t => t -> Integer
P.deg UPolynomial k
r) ((k, Integer, UPolynomial k) -> (k, Integer, UPolynomial k))
-> (k, Integer, UPolynomial k) -> (k, Integer, UPolynomial k)
forall a b. (a -> b) -> a -> b
$ (k
bm, Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1, UPolynomial k
r)
  | Bool
otherwise = String -> (k, Integer, UPolynomial k)
forall a. (?callStack::CallStack) => String -> a
error String
"mr p q: not (deg p >= deg q)"
  where
    x :: UPolynomial k
x = X -> UPolynomial k
forall a v. Var a v => v -> a
P.var X
X
    n :: Integer
n = UPolynomial k -> Integer
forall t. Degree t => t -> Integer
P.deg UPolynomial k
p
    m :: Integer
m = UPolynomial k -> Integer
forall t. Degree t => t -> Integer
P.deg UPolynomial k
q
    bm :: k
bm = MonomialOrder X -> UPolynomial k -> k
forall k v. Num k => MonomialOrder v -> Polynomial k v -> k
P.lc MonomialOrder X
P.nat UPolynomial k
q
    (UPolynomial k
l,UPolynomial k
r) = UPolynomial k -> Integer -> (UPolynomial k, UPolynomial k)
f UPolynomial k
p Integer
n

    f :: UPolynomial k -> Integer -> (UPolynomial k, UPolynomial k)
    f :: UPolynomial k -> Integer -> (UPolynomial k, UPolynomial k)
f UPolynomial k
p Integer
n
      | Integer
nInteger -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
==Integer
m =
          let l :: Polynomial k v
l = k -> Polynomial k v
forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant k
an
              r :: UPolynomial k
r = k -> UPolynomial k
forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant k
bm UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
* UPolynomial k
p UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
- k -> UPolynomial k
forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant k
an UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
* UPolynomial k
q
          in Bool
-> (UPolynomial k, UPolynomial k) -> (UPolynomial k, UPolynomial k)
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (k -> UPolynomial k
forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant (k
bmk -> Integer -> k
forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1)) UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
* UPolynomial k
p UPolynomial k -> UPolynomial k -> Bool
forall a. Eq a => a -> a -> Bool
== UPolynomial k
qUPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
*UPolynomial k
forall v. Polynomial k v
l UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
+ UPolynomial k
r Bool -> Bool -> Bool
&& Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> UPolynomial k -> Integer
forall t. Degree t => t -> Integer
P.deg UPolynomial k
r) ((UPolynomial k, UPolynomial k) -> (UPolynomial k, UPolynomial k))
-> (UPolynomial k, UPolynomial k) -> (UPolynomial k, UPolynomial k)
forall a b. (a -> b) -> a -> b
$ (UPolynomial k
forall v. Polynomial k v
l, UPolynomial k
r)
      | Bool
otherwise =
          let p' :: UPolynomial k
p'     = (k -> UPolynomial k
forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant k
bm UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
* UPolynomial k
p UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
- k -> UPolynomial k
forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant k
an UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
* UPolynomial k
xUPolynomial k -> Integer -> UPolynomial k
forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
m) UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
* UPolynomial k
q)
              (UPolynomial k
l',UPolynomial k
r) = UPolynomial k -> Integer -> (UPolynomial k, UPolynomial k)
f UPolynomial k
p' (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)
              l :: UPolynomial k
l      = UPolynomial k
l' UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
+ k -> UPolynomial k
forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant (k
ank -> k -> k
forall a. Num a => a -> a -> a
*k
bmk -> Integer -> k
forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
m)) UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
* UPolynomial k
xUPolynomial k -> Integer -> UPolynomial k
forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
m)
          in Bool
-> (UPolynomial k, UPolynomial k) -> (UPolynomial k, UPolynomial k)
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> UPolynomial k -> Integer
forall t. Degree t => t -> Integer
P.deg UPolynomial k
p') ((UPolynomial k, UPolynomial k) -> (UPolynomial k, UPolynomial k))
-> (UPolynomial k, UPolynomial k) -> (UPolynomial k, UPolynomial k)
forall a b. (a -> b) -> a -> b
$
             Bool
-> (UPolynomial k, UPolynomial k) -> (UPolynomial k, UPolynomial k)
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (k -> UPolynomial k
forall k v. (Eq k, Num k) => k -> Polynomial k v
P.constant (k
bmk -> Integer -> k
forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1)) UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
* UPolynomial k
p UPolynomial k -> UPolynomial k -> Bool
forall a. Eq a => a -> a -> Bool
== UPolynomial k
qUPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
*UPolynomial k
l UPolynomial k -> UPolynomial k -> UPolynomial k
forall a. Num a => a -> a -> a
+ UPolynomial k
r Bool -> Bool -> Bool
&& Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> UPolynomial k -> Integer
forall t. Degree t => t -> Integer
P.deg UPolynomial k
r) ((UPolynomial k, UPolynomial k) -> (UPolynomial k, UPolynomial k))
-> (UPolynomial k, UPolynomial k) -> (UPolynomial k, UPolynomial k)
forall a b. (a -> b) -> a -> b
$ (UPolynomial k
l, UPolynomial k
r)
      where
        an :: k
an = Monomial X -> UPolynomial k -> k
forall k v. (Num k, Ord v) => Monomial v -> Polynomial k v -> k
P.coeff (X -> Monomial X
forall a v. Var a v => v -> a
P.var X
X Monomial X -> Integer -> Monomial X
forall v. Ord v => Monomial v -> Integer -> Monomial v
`P.mpow` Integer
n) UPolynomial k
p

test_mr_1 :: (Coeff Int, Integer, UPolynomial (Coeff Int))
test_mr_1 :: (Coeff Int, Integer, UPolynomial (Coeff Int))
test_mr_1 = UPolynomial (Coeff Int)
-> UPolynomial (Coeff Int)
-> (Coeff Int, Integer, UPolynomial (Coeff Int))
forall k.
(Ord k, Show k, Num k, PrettyCoeff k) =>
UPolynomial k -> UPolynomial k -> (k, Integer, UPolynomial k)
mr (Coeff Int -> Int -> UPolynomial (Coeff Int)
forall k v.
(Ord k, Num k, Ord v) =>
Polynomial k v -> v -> UPolynomial (Polynomial k v)
P.toUPolynomialOf Coeff Int
p Int
3) (Coeff Int -> Int -> UPolynomial (Coeff Int)
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 = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
0
    b :: Coeff Int
b = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
1
    c :: Coeff Int
c = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
2
    x :: Coeff Int
x = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
3
    p :: Coeff Int
p = Coeff Int
aCoeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
*Coeff Int
xCoeff Int -> Int -> Coeff Int
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) Coeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
+ Coeff Int
bCoeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
*Coeff Int
x Coeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
+ Coeff Int
c
    q :: Coeff Int
q = Coeff Int
2Coeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
*Coeff Int
aCoeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
*Coeff Int
x Coeff Int -> Coeff Int -> Coeff Int
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 = UPolynomial (Coeff Int)
-> UPolynomial (Coeff Int)
-> (Coeff Int, Integer, UPolynomial (Coeff Int))
forall k.
(Ord k, Show k, Num k, PrettyCoeff k) =>
UPolynomial k -> UPolynomial k -> (k, Integer, UPolynomial k)
mr (Coeff Int -> Int -> UPolynomial (Coeff Int)
forall k v.
(Ord k, Num k, Ord v) =>
Polynomial k v -> v -> UPolynomial (Polynomial k v)
P.toUPolynomialOf Coeff Int
p Int
3) (Coeff Int -> Int -> UPolynomial (Coeff Int)
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 = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
0
    b :: Coeff Int
b = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
1
    c :: Coeff Int
c = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
2
    x :: Coeff Int
x = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
3
    p :: Coeff Int
p = Coeff Int
aCoeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
*Coeff Int
xCoeff Int -> Int -> Coeff Int
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) Coeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
+ Coeff Int
bCoeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
*Coeff Int
x Coeff Int -> Coeff Int -> Coeff Int
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 :: M v a -> [(a, Assumption v)]
runM M v a
m = M v a -> Assumption v -> [(a, Assumption v)]
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT M v a
m Assumption v
forall v. Assumption v
emptyAssumption

assume :: (Ord v, Show v, PrettyVar v) => Polynomial Rational v -> [Sign] -> M v ()
assume :: 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) <- StateT
  (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
  []
  (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
forall s (m :: * -> *). MonadState s m => m s
get
  Polynomial Rational v
p <- Polynomial Rational v
-> StateT
     (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
     []
     (Polynomial Rational v)
forall (m :: * -> *) a. Monad m => a -> m a
return (Polynomial Rational v
 -> StateT
      (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
      []
      (Polynomial Rational v))
-> Polynomial Rational v
-> StateT
     (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
     []
     (Polynomial Rational v)
forall a b. (a -> b) -> a -> b
$ MonomialOrder v
-> Polynomial Rational v
-> [Polynomial Rational v]
-> Polynomial Rational v
forall k v.
(Eq k, Fractional k, Ord v) =>
MonomialOrder v
-> Polynomial k v -> [Polynomial k v] -> Polynomial k v
P.reduce MonomialOrder v
forall v. Ord v => MonomialOrder v
P.grevlex Polynomial Rational v
p [Polynomial Rational v]
gb
  Set Sign
ss <- Set Sign
-> StateT
     (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
     []
     (Set Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set Sign
 -> StateT
      (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
      []
      (Set Sign))
-> Set Sign
-> StateT
     (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
     []
     (Set Sign)
forall a b. (a -> b) -> a -> b
$ [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign]
ss
  Set Sign
ss <- Set Sign
-> StateT
     (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
     []
     (Set Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set Sign
 -> StateT
      (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
      []
      (Set Sign))
-> Set Sign
-> StateT
     (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
     []
     (Set Sign)
forall a b. (a -> b) -> a -> b
$ Set Sign
ss Set Sign -> Set Sign -> Set Sign
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Map (Polynomial Rational v) (Set Sign)
-> Polynomial Rational v -> Set Sign
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
  Bool -> M v ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> M v ()) -> Bool -> M v ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set Sign -> Bool
forall a. Set a -> Bool
Set.null Set Sign
ss
  Bool -> M v () -> M v ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Polynomial Rational v -> Integer
forall t. Degree t => t -> Integer
P.deg Polynomial Rational v
p Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0) (M v () -> M v ()) -> M v () -> M v ()
forall a b. (a -> b) -> a -> b
$ do
    let c :: Rational
c = MonomialOrder v -> Polynomial Rational v -> Rational
forall k v. Num k => MonomialOrder v -> Polynomial k v -> k
P.lc MonomialOrder v
forall v. Ord v => MonomialOrder v
P.grlex Polynomial Rational v
p
    (Polynomial Rational v
p,Set Sign
ss) <- (Polynomial Rational v, Set Sign)
-> StateT
     (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
     []
     (Polynomial Rational v, Set Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Polynomial Rational v, Set Sign)
 -> StateT
      (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
      []
      (Polynomial Rational v, Set Sign))
-> (Polynomial Rational v, Set Sign)
-> StateT
     (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
     []
     (Polynomial Rational v, Set Sign)
forall a b. (a -> b) -> a -> b
$ ((Rational -> Rational)
-> Polynomial Rational v -> Polynomial Rational v
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff (Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/Rational
c) Polynomial Rational v
p, (Sign -> Sign) -> Set Sign -> Set Sign
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\Sign
s -> Sign
s Sign -> Sign -> Sign
`Sign.div` Rational -> Sign
forall a. Real a => a -> Sign
Sign.signOf Rational
c) Set Sign
ss)
    let ss_orig :: Set Sign
ss_orig = Set Sign
-> Polynomial Rational v
-> Map (Polynomial Rational v) (Set Sign)
-> Set Sign
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Sign] -> Set Sign
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 <- Set Sign
-> StateT
     (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
     []
     (Set Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set Sign
 -> StateT
      (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
      []
      (Set Sign))
-> Set Sign
-> StateT
     (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
     []
     (Set Sign)
forall a b. (a -> b) -> a -> b
$ Set Sign -> Set Sign -> Set Sign
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set Sign
ss Set Sign
ss_orig
    Bool -> M v ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> M v ()) -> Bool -> M v ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set Sign -> Bool
forall a. Set a -> Bool
Set.null Set Sign
ss
    case (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
-> Maybe
     (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
forall v. Ord v => Assumption v -> Maybe (Assumption v)
propagate ((Set Sign -> Set Sign -> Set Sign)
-> Polynomial Rational v
-> Set Sign
-> Map (Polynomial Rational v) (Set Sign)
-> Map (Polynomial Rational v) (Set Sign)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Set Sign -> Set Sign -> Set Sign
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
  (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
Nothing -> M v ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
      Just (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
a -> (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
-> M v ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational 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' :: [(UPolynomial (Polynomial Rational v), [Sign])]
-> [([(Polynomial Rational v, [Sign])],
     [Cell (Polynomial Rational v)])]
project' [(UPolynomial (Polynomial Rational v), [Sign])]
cs = [ (Assumption v -> [(Polynomial Rational v, [Sign])]
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 = M v [Cell (Polynomial Rational v)]
-> [([Cell (Polynomial Rational v)], Assumption v)]
forall v a. M v a -> [(a, Assumption v)]
runM (M v [Cell (Polynomial Rational v)]
 -> [([Cell (Polynomial Rational v)], Assumption v)])
-> M v [Cell (Polynomial Rational v)]
-> [([Cell (Polynomial Rational v)], Assumption v)]
forall a b. (a -> b) -> a -> b
$ do
      [(UPolynomial (Polynomial Rational v), [Sign])]
-> ((UPolynomial (Polynomial Rational v), [Sign])
    -> StateT (Assumption v) [] ())
-> StateT (Assumption v) [] ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(UPolynomial (Polynomial Rational v), [Sign])]
cs (((UPolynomial (Polynomial Rational v), [Sign])
  -> StateT (Assumption v) [] ())
 -> StateT (Assumption v) [] ())
-> ((UPolynomial (Polynomial Rational v), [Sign])
    -> StateT (Assumption v) [] ())
-> StateT (Assumption v) [] ()
forall a b. (a -> b) -> a -> b
$ \(UPolynomial (Polynomial Rational v)
p,[Sign]
ss) -> do
        Bool -> StateT (Assumption v) [] () -> StateT (Assumption v) [] ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> UPolynomial (Polynomial Rational v) -> Integer
forall t. Degree t => t -> Integer
P.deg UPolynomial (Polynomial Rational v)
p) (StateT (Assumption v) [] () -> StateT (Assumption v) [] ())
-> StateT (Assumption v) [] () -> StateT (Assumption v) [] ()
forall a b. (a -> b) -> a -> b
$ Polynomial Rational v -> [Sign] -> StateT (Assumption v) [] ()
forall v.
(Ord v, Show v, PrettyVar v) =>
Polynomial Rational v -> [Sign] -> M v ()
assume (Monomial X
-> UPolynomial (Polynomial Rational v) -> Polynomial Rational v
forall k v. (Num k, Ord v) => Monomial v -> Polynomial k v -> k
P.coeff Monomial X
forall v. Monomial v
P.mone UPolynomial (Polynomial Rational v)
p) [Sign]
ss
      SignConf (Polynomial Rational v)
conf <- [UPolynomial (Polynomial Rational v)]
-> M v (SignConf (Polynomial Rational v))
forall v.
(Ord v, Show v, PrettyVar v) =>
[UPolynomial (Polynomial Rational v)]
-> M v (SignConf (Polynomial Rational v))
buildSignConf (((UPolynomial (Polynomial Rational v), [Sign])
 -> UPolynomial (Polynomial Rational v))
-> [(UPolynomial (Polynomial Rational v), [Sign])]
-> [UPolynomial (Polynomial Rational v)]
forall a b. (a -> b) -> [a] -> [b]
map (UPolynomial (Polynomial Rational v), [Sign])
-> UPolynomial (Polynomial Rational v)
forall a b. (a, b) -> a
fst [(UPolynomial (Polynomial Rational v), [Sign])]
cs)
      -- normalizePoly前に次数が1以上で、normalizePoly結果の次数が0以下の時のための処理が必要なので注意
      [(UPolynomial (Polynomial Rational v), [Sign])]
cs' <- ([Maybe (UPolynomial (Polynomial Rational v), [Sign])]
 -> [(UPolynomial (Polynomial Rational v), [Sign])])
-> StateT
     (Assumption v)
     []
     [Maybe (UPolynomial (Polynomial Rational v), [Sign])]
-> StateT
     (Assumption v) [] [(UPolynomial (Polynomial Rational v), [Sign])]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Maybe (UPolynomial (Polynomial Rational v), [Sign])]
-> [(UPolynomial (Polynomial Rational v), [Sign])]
forall a. [Maybe a] -> [a]
catMaybes (StateT
   (Assumption v)
   []
   [Maybe (UPolynomial (Polynomial Rational v), [Sign])]
 -> StateT
      (Assumption v) [] [(UPolynomial (Polynomial Rational v), [Sign])])
-> StateT
     (Assumption v)
     []
     [Maybe (UPolynomial (Polynomial Rational v), [Sign])]
-> StateT
     (Assumption v) [] [(UPolynomial (Polynomial Rational v), [Sign])]
forall a b. (a -> b) -> a -> b
$ [(UPolynomial (Polynomial Rational v), [Sign])]
-> ((UPolynomial (Polynomial Rational v), [Sign])
    -> StateT
         (Assumption v)
         []
         (Maybe (UPolynomial (Polynomial Rational v), [Sign])))
-> StateT
     (Assumption v)
     []
     [Maybe (UPolynomial (Polynomial Rational v), [Sign])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(UPolynomial (Polynomial Rational v), [Sign])]
cs (((UPolynomial (Polynomial Rational v), [Sign])
  -> StateT
       (Assumption v)
       []
       (Maybe (UPolynomial (Polynomial Rational v), [Sign])))
 -> StateT
      (Assumption v)
      []
      [Maybe (UPolynomial (Polynomial Rational v), [Sign])])
-> ((UPolynomial (Polynomial Rational v), [Sign])
    -> StateT
         (Assumption v)
         []
         (Maybe (UPolynomial (Polynomial Rational v), [Sign])))
-> StateT
     (Assumption v)
     []
     [Maybe (UPolynomial (Polynomial Rational v), [Sign])]
forall a b. (a -> b) -> a -> b
$ \(UPolynomial (Polynomial Rational v)
p,[Sign]
ss) -> do
        UPolynomial (Polynomial Rational v)
p' <- UPolynomial (Polynomial Rational v)
-> M v (UPolynomial (Polynomial Rational v))
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> UPolynomial (Polynomial Rational v) -> Integer
forall t. Degree t => t -> Integer
P.deg UPolynomial (Polynomial Rational v)
p')
          then Polynomial Rational v -> [Sign] -> StateT (Assumption v) [] ()
forall v.
(Ord v, Show v, PrettyVar v) =>
Polynomial Rational v -> [Sign] -> M v ()
assume (Monomial X
-> UPolynomial (Polynomial Rational v) -> Polynomial Rational v
forall k v. (Num k, Ord v) => Monomial v -> Polynomial k v -> k
P.coeff Monomial X
forall v. Monomial v
P.mone UPolynomial (Polynomial Rational v)
p') [Sign]
ss StateT (Assumption v) [] ()
-> StateT
     (Assumption v)
     []
     (Maybe (UPolynomial (Polynomial Rational v), [Sign]))
-> StateT
     (Assumption v)
     []
     (Maybe (UPolynomial (Polynomial Rational v), [Sign]))
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe (UPolynomial (Polynomial Rational v), [Sign])
-> StateT
     (Assumption v)
     []
     (Maybe (UPolynomial (Polynomial Rational v), [Sign]))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (UPolynomial (Polynomial Rational v), [Sign])
forall a. Maybe a
Nothing
          else Maybe (UPolynomial (Polynomial Rational v), [Sign])
-> StateT
     (Assumption v)
     []
     (Maybe (UPolynomial (Polynomial Rational v), [Sign]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (UPolynomial (Polynomial Rational v), [Sign])
 -> StateT
      (Assumption v)
      []
      (Maybe (UPolynomial (Polynomial Rational v), [Sign])))
-> Maybe (UPolynomial (Polynomial Rational v), [Sign])
-> StateT
     (Assumption v)
     []
     (Maybe (UPolynomial (Polynomial Rational v), [Sign]))
forall a b. (a -> b) -> a -> b
$ (UPolynomial (Polynomial Rational v), [Sign])
-> Maybe (UPolynomial (Polynomial Rational v), [Sign])
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 Cell (Polynomial Rational v)
-> Cell (Polynomial Rational v) -> Bool
forall a. Eq a => a -> a -> Bool
/= Point (Polynomial Rational v) -> Cell (Polynomial Rational v)
forall c. Point c -> Cell c
Point Point (Polynomial Rational v)
forall c. Point c
NegInf, Cell (Polynomial Rational v)
cell Cell (Polynomial Rational v)
-> Cell (Polynomial Rational v) -> Bool
forall a. Eq a => a -> a -> Bool
/= Point (Polynomial Rational v) -> Cell (Polynomial Rational v)
forall c. Point c -> Cell c
Point Point (Polynomial Rational v)
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]
      Bool -> StateT (Assumption v) [] ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> StateT (Assumption v) [] ())
-> Bool -> StateT (Assumption v) [] ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Cell (Polynomial Rational v)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Cell (Polynomial Rational v)]
satCells
      [Cell (Polynomial Rational v)]
-> M v [Cell (Polynomial Rational v)]
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 = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Map (UPolynomial (Polynomial Rational v)) Sign
-> UPolynomial (Polynomial Rational v) -> [Sign] -> Bool
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 = UPolynomial (Polynomial Rational v)
-> Map (UPolynomial (Polynomial Rational v)) Sign -> Sign
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 Sign -> t Sign -> Bool
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 :: [UPolynomial (Polynomial Rational v)]
-> M v (SignConf (Polynomial Rational v))
buildSignConf [UPolynomial (Polynomial Rational v)]
ps = do
  [UPolynomial (Polynomial Rational v)]
ps2 <- [UPolynomial (Polynomial Rational v)]
-> M v [UPolynomial (Polynomial Rational v)]
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 = (UPolynomial (Polynomial Rational v) -> Integer)
-> [UPolynomial (Polynomial Rational v)]
-> [UPolynomial (Polynomial Rational v)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn UPolynomial (Polynomial Rational v) -> Integer
forall t. Degree t => t -> Integer
P.deg [UPolynomial (Polynomial Rational v)]
ps2
  --trace ("collected polynomials: " ++ prettyShow ts) $ return ()
  (SignConf (Polynomial Rational v)
 -> UPolynomial (Polynomial Rational v)
 -> M v (SignConf (Polynomial Rational v)))
-> SignConf (Polynomial Rational v)
-> [UPolynomial (Polynomial Rational v)]
-> M v (SignConf (Polynomial Rational v))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((UPolynomial (Polynomial Rational v)
 -> SignConf (Polynomial Rational v)
 -> M v (SignConf (Polynomial Rational v)))
-> SignConf (Polynomial Rational v)
-> UPolynomial (Polynomial Rational v)
-> M v (SignConf (Polynomial Rational v))
forall a b c. (a -> b -> c) -> b -> a -> c
flip UPolynomial (Polynomial Rational v)
-> SignConf (Polynomial Rational v)
-> M v (SignConf (Polynomial Rational v))
forall v.
(Show v, Ord v, PrettyVar v) =>
UPolynomial (Polynomial Rational v)
-> SignConf (Polynomial Rational v)
-> M v (SignConf (Polynomial Rational v))
refineSignConf) SignConf (Polynomial Rational v)
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 :: [UPolynomial (Polynomial Rational v)]
-> M v [UPolynomial (Polynomial Rational v)]
collectPolynomials [UPolynomial (Polynomial Rational v)]
ps = Set (UPolynomial (Polynomial Rational v))
-> Set (UPolynomial (Polynomial Rational v))
-> M v [UPolynomial (Polynomial Rational v)]
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 Set (UPolynomial (Polynomial Rational v))
forall a. Set a
Set.empty (Set (UPolynomial (Polynomial Rational v))
 -> M v [UPolynomial (Polynomial Rational v)])
-> StateT
     (Assumption v) [] (Set (UPolynomial (Polynomial Rational v)))
-> M v [UPolynomial (Polynomial Rational v)]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [UPolynomial (Polynomial Rational v)]
-> StateT
     (Assumption v) [] (Set (UPolynomial (Polynomial Rational v)))
forall v.
(Ord v, Show v, PrettyVar v) =>
[UPolynomial (Polynomial Rational v)]
-> StateT
     (Assumption v) [] (Set (UPolynomial (Polynomial Rational v)))
f [UPolynomial (Polynomial Rational v)]
ps
  where
    f :: [UPolynomial (Polynomial Rational v)]
-> StateT
     (Assumption v) [] (Set (UPolynomial (Polynomial Rational v)))
f [UPolynomial (Polynomial Rational v)]
ps = do
      [UPolynomial (Polynomial Rational v)]
ps' <- (UPolynomial (Polynomial Rational v)
 -> StateT (Assumption v) [] (UPolynomial (Polynomial Rational v)))
-> [UPolynomial (Polynomial Rational v)]
-> StateT (Assumption v) [] [UPolynomial (Polynomial Rational v)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM UPolynomial (Polynomial Rational v)
-> StateT (Assumption v) [] (UPolynomial (Polynomial Rational v))
forall v.
(Ord v, Show v, PrettyVar v) =>
UPolynomial (Polynomial Rational v)
-> M v (UPolynomial (Polynomial Rational v))
normalizePoly ([UPolynomial (Polynomial Rational v)]
 -> StateT (Assumption v) [] [UPolynomial (Polynomial Rational v)])
-> [UPolynomial (Polynomial Rational v)]
-> StateT (Assumption v) [] [UPolynomial (Polynomial Rational v)]
forall a b. (a -> b) -> a -> b
$ Set (UPolynomial (Polynomial Rational v))
-> [UPolynomial (Polynomial Rational v)]
forall a. Set a -> [a]
Set.toList (Set (UPolynomial (Polynomial Rational v))
 -> [UPolynomial (Polynomial Rational v)])
-> Set (UPolynomial (Polynomial Rational v))
-> [UPolynomial (Polynomial Rational v)]
forall a b. (a -> b) -> a -> b
$ [UPolynomial (Polynomial Rational v)]
-> Set (UPolynomial (Polynomial Rational v))
forall a. Ord a => [a] -> Set a
Set.fromList ([UPolynomial (Polynomial Rational v)]
 -> Set (UPolynomial (Polynomial Rational v)))
-> [UPolynomial (Polynomial Rational v)]
-> Set (UPolynomial (Polynomial Rational v))
forall a b. (a -> b) -> a -> b
$ [UPolynomial (Polynomial Rational v)
p | UPolynomial (Polynomial Rational v)
p <- [UPolynomial (Polynomial Rational v)]
ps, UPolynomial (Polynomial Rational v) -> Integer
forall t. Degree t => t -> Integer
P.deg UPolynomial (Polynomial Rational v)
p Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0]
      Set (UPolynomial (Polynomial Rational v))
-> StateT
     (Assumption v) [] (Set (UPolynomial (Polynomial Rational v)))
forall (m :: * -> *) a. Monad m => a -> m a
return (Set (UPolynomial (Polynomial Rational v))
 -> StateT
      (Assumption v) [] (Set (UPolynomial (Polynomial Rational v))))
-> Set (UPolynomial (Polynomial Rational v))
-> StateT
     (Assumption v) [] (Set (UPolynomial (Polynomial Rational v)))
forall a b. (a -> b) -> a -> b
$ [UPolynomial (Polynomial Rational v)]
-> Set (UPolynomial (Polynomial Rational v))
forall a. Ord a => [a] -> Set a
Set.fromList ([UPolynomial (Polynomial Rational v)]
 -> Set (UPolynomial (Polynomial Rational v)))
-> [UPolynomial (Polynomial Rational v)]
-> Set (UPolynomial (Polynomial Rational v))
forall a b. (a -> b) -> a -> b
$ (UPolynomial (Polynomial Rational v)
 -> UPolynomial (Polynomial Rational v))
-> [UPolynomial (Polynomial Rational v)]
-> [UPolynomial (Polynomial Rational v)]
forall a b. (a -> b) -> [a] -> [b]
map UPolynomial (Polynomial Rational v)
-> UPolynomial (Polynomial Rational v)
forall v.
Ord v =>
UPolynomial (Polynomial Rational v)
-> UPolynomial (Polynomial Rational v)
normalizeSignConfKey ([UPolynomial (Polynomial Rational v)]
 -> [UPolynomial (Polynomial Rational v)])
-> [UPolynomial (Polynomial Rational v)]
-> [UPolynomial (Polynomial Rational v)]
forall a b. (a -> b) -> a -> b
$ (UPolynomial (Polynomial Rational v) -> Bool)
-> [UPolynomial (Polynomial Rational v)]
-> [UPolynomial (Polynomial Rational v)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\UPolynomial (Polynomial Rational v)
p -> UPolynomial (Polynomial Rational v) -> Integer
forall t. Degree t => t -> Integer
P.deg UPolynomial (Polynomial Rational v)
p Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0) [UPolynomial (Polynomial Rational v)]
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 | Set (Polynomial (Polynomial Rational v) X) -> Bool
forall a. Set a -> Bool
Set.null Set (Polynomial (Polynomial Rational v) X)
ps = [Polynomial (Polynomial Rational v) X]
-> StateT (Assumption v) [] [Polynomial (Polynomial Rational v) X]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Polynomial (Polynomial Rational v) X]
 -> StateT (Assumption v) [] [Polynomial (Polynomial Rational v) X])
-> [Polynomial (Polynomial Rational v) X]
-> StateT (Assumption v) [] [Polynomial (Polynomial Rational v) X]
forall a b. (a -> b) -> a -> b
$ Set (Polynomial (Polynomial Rational v) X)
-> [Polynomial (Polynomial Rational v) X]
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 <- [Polynomial (Polynomial Rational v) X]
-> StateT
     (Assumption v) [] (Set (Polynomial (Polynomial Rational v) X))
forall v.
(Ord v, Show v, PrettyVar v) =>
[UPolynomial (Polynomial Rational v)]
-> StateT
     (Assumption v) [] (Set (UPolynomial (Polynomial Rational v)))
f [Polynomial (Polynomial Rational v) X
-> X -> Polynomial (Polynomial Rational v) X
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 <- Set (Polynomial (Polynomial Rational v) X)
-> [Polynomial (Polynomial Rational v) X]
forall a. Set a -> [a]
Set.toList Set (Polynomial (Polynomial Rational v) X)
ps]
      [Set (Polynomial (Polynomial Rational v) X)]
rss <-
        [(Polynomial (Polynomial Rational v) X,
  Polynomial (Polynomial Rational v) X)]
-> ((Polynomial (Polynomial Rational v) X,
     Polynomial (Polynomial Rational v) X)
    -> StateT
         (Assumption v) [] (Set (Polynomial (Polynomial Rational v) X)))
-> StateT
     (Assumption v) [] [Set (Polynomial (Polynomial Rational v) X)]
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 <- Set (Polynomial (Polynomial Rational v) X)
-> [Polynomial (Polynomial Rational v) X]
forall a. Set a -> [a]
Set.toList Set (Polynomial (Polynomial Rational v) X)
ps, Polynomial (Polynomial Rational v) X
p2 <- Set (Polynomial (Polynomial Rational v) X)
-> [Polynomial (Polynomial Rational v) X]
forall a. Set a -> [a]
Set.toList Set (Polynomial (Polynomial Rational v) X)
ps [Polynomial (Polynomial Rational v) X]
-> [Polynomial (Polynomial Rational v) X]
-> [Polynomial (Polynomial Rational v) X]
forall a. [a] -> [a] -> [a]
++ Set (Polynomial (Polynomial Rational v) X)
-> [Polynomial (Polynomial Rational v) X]
forall a. Set a -> [a]
Set.toList Set (Polynomial (Polynomial Rational v) X)
result, Polynomial (Polynomial Rational v) X
p1 Polynomial (Polynomial Rational v) X
-> Polynomial (Polynomial Rational v) X -> Bool
forall a. Eq a => a -> a -> Bool
/= Polynomial (Polynomial Rational v) X
p2] (((Polynomial (Polynomial Rational v) X,
   Polynomial (Polynomial Rational v) X)
  -> StateT
       (Assumption v) [] (Set (Polynomial (Polynomial Rational v) X)))
 -> StateT
      (Assumption v) [] [Set (Polynomial (Polynomial Rational v) X)])
-> ((Polynomial (Polynomial Rational v) X,
     Polynomial (Polynomial Rational v) X)
    -> StateT
         (Assumption v) [] (Set (Polynomial (Polynomial Rational v) X)))
-> StateT
     (Assumption v) [] [Set (Polynomial (Polynomial Rational v) X)]
forall a b. (a -> b) -> a -> b
$ \(Polynomial (Polynomial Rational v) X
p1,Polynomial (Polynomial Rational v) X
p2) -> do
          let d :: Integer
d = Polynomial (Polynomial Rational v) X -> Integer
forall t. Degree t => t -> Integer
P.deg Polynomial (Polynomial Rational v) X
p1
              e :: Integer
e = Polynomial (Polynomial Rational v) X -> Integer
forall t. Degree t => t -> Integer
P.deg Polynomial (Polynomial Rational v) X
p2
          [Polynomial (Polynomial Rational v) X]
-> StateT
     (Assumption v) [] (Set (Polynomial (Polynomial Rational v) X))
forall v.
(Ord v, Show v, PrettyVar v) =>
[UPolynomial (Polynomial Rational v)]
-> StateT
     (Assumption v) [] (Set (UPolynomial (Polynomial Rational v)))
f [Polynomial (Polynomial Rational v) X
r | (Polynomial Rational v
_,Integer
_,Polynomial (Polynomial Rational v) X
r) <- [Polynomial (Polynomial Rational v) X
-> Polynomial (Polynomial Rational v) X
-> (Polynomial Rational v, Integer,
    Polynomial (Polynomial Rational v) X)
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
e] [(Polynomial Rational v, Integer,
  Polynomial (Polynomial Rational v) X)]
-> [(Polynomial Rational v, Integer,
     Polynomial (Polynomial Rational v) X)]
-> [(Polynomial Rational v, Integer,
     Polynomial (Polynomial Rational v) X)]
forall a. [a] -> [a] -> [a]
++ [Polynomial (Polynomial Rational v) X
-> Polynomial (Polynomial Rational v) X
-> (Polynomial Rational v, Integer,
    Polynomial (Polynomial Rational v) X)
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
d]]
      let ps' :: Set (Polynomial (Polynomial Rational v) X)
ps' = [Set (Polynomial (Polynomial Rational v) X)]
-> Set (Polynomial (Polynomial Rational v) X)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (Set (Polynomial (Polynomial Rational v) X)
rsSet (Polynomial (Polynomial Rational v) X)
-> [Set (Polynomial (Polynomial Rational v) X)]
-> [Set (Polynomial (Polynomial Rational v) X)]
forall 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 Set (Polynomial (Polynomial Rational v) X)
-> Set (Polynomial (Polynomial Rational v) X)
-> Set (Polynomial (Polynomial Rational v) X)
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' Set (Polynomial (Polynomial Rational v) X)
-> Set (Polynomial (Polynomial Rational v) X)
-> Set (Polynomial (Polynomial Rational v) X)
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 :: UPolynomial (Polynomial Rational v)
-> M v (UPolynomial (Polynomial Rational v))
normalizePoly UPolynomial (Polynomial Rational v)
p = ([Term (Polynomial Rational v) X]
 -> UPolynomial (Polynomial Rational v))
-> StateT (Assumption v) [] [Term (Polynomial Rational v) X]
-> M v (UPolynomial (Polynomial Rational v))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Term (Polynomial Rational v) X]
-> UPolynomial (Polynomial Rational v)
forall k v. (Eq k, Num k, Ord v) => [Term k v] -> Polynomial k v
P.fromTerms (StateT (Assumption v) [] [Term (Polynomial Rational v) X]
 -> M v (UPolynomial (Polynomial Rational v)))
-> StateT (Assumption v) [] [Term (Polynomial Rational v) X]
-> M v (UPolynomial (Polynomial Rational v))
forall a b. (a -> b) -> a -> b
$ [Term (Polynomial Rational v) X]
-> StateT (Assumption v) [] [Term (Polynomial Rational v) X]
forall v b.
(Ord v, Show v, PrettyVar v) =>
[(Polynomial Rational v, b)]
-> StateT (Assumption v) [] [(Polynomial Rational v, b)]
go ([Term (Polynomial Rational v) X]
 -> StateT (Assumption v) [] [Term (Polynomial Rational v) X])
-> [Term (Polynomial Rational v) X]
-> StateT (Assumption v) [] [Term (Polynomial Rational v) X]
forall a b. (a -> b) -> a -> b
$ (Term (Polynomial Rational v) X -> Down Integer)
-> [Term (Polynomial Rational v) X]
-> [Term (Polynomial Rational v) X]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (Integer -> Down Integer
forall a. a -> Down a
Down (Integer -> Down Integer)
-> (Term (Polynomial Rational v) X -> Integer)
-> Term (Polynomial Rational v) X
-> Down Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Monomial X -> Integer
forall t. Degree t => t -> Integer
P.deg (Monomial X -> Integer)
-> (Term (Polynomial Rational v) X -> Monomial X)
-> Term (Polynomial Rational v) X
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (Polynomial Rational v) X -> Monomial X
forall a b. (a, b) -> b
snd) ([Term (Polynomial Rational v) X]
 -> [Term (Polynomial Rational v) X])
-> [Term (Polynomial Rational v) X]
-> [Term (Polynomial Rational v) X]
forall a b. (a -> b) -> a -> b
$ UPolynomial (Polynomial Rational v)
-> [Term (Polynomial Rational v) X]
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 [] = [(Polynomial Rational v, b)]
-> StateT (Assumption v) [] [(Polynomial Rational v, b)]
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) =
      StateT (Assumption v) [] [(Polynomial Rational v, b)]
-> StateT (Assumption v) [] [(Polynomial Rational v, b)]
-> StateT (Assumption v) [] [(Polynomial Rational v, b)]
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus
        (Polynomial Rational v -> [Sign] -> M v ()
forall v.
(Ord v, Show v, PrettyVar v) =>
Polynomial Rational v -> [Sign] -> M v ()
assume Polynomial Rational v
c [Sign
Pos, Sign
Neg] M v ()
-> StateT (Assumption v) [] [(Polynomial Rational v, b)]
-> StateT (Assumption v) [] [(Polynomial Rational v, b)]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [(Polynomial Rational v, b)]
-> StateT (Assumption v) [] [(Polynomial Rational v, b)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Polynomial Rational v, b)]
xxs)
        (Polynomial Rational v -> [Sign] -> M v ()
forall v.
(Ord v, Show v, PrettyVar v) =>
Polynomial Rational v -> [Sign] -> M v ()
assume Polynomial Rational v
c [Sign
Zero] M v ()
-> StateT (Assumption v) [] [(Polynomial Rational v, b)]
-> StateT (Assumption v) [] [(Polynomial Rational v, b)]
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 :: 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 = (SignConf (Polynomial Rational v)
 -> SignConf (Polynomial Rational v))
-> M v (SignConf (Polynomial Rational v))
-> M v (SignConf (Polynomial Rational v))
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) (M v (SignConf (Polynomial Rational v))
 -> M v (SignConf (Polynomial Rational v)))
-> M v (SignConf (Polynomial Rational v))
-> M v (SignConf (Polynomial Rational v))
forall a b. (a -> b) -> a -> b
$ ((Cell (Polynomial Rational v),
  Map (UPolynomial (Polynomial Rational v)) Sign)
 -> StateT
      (Assumption v)
      []
      (Cell (Polynomial Rational v),
       Map (UPolynomial (Polynomial Rational v)) Sign))
-> SignConf (Polynomial Rational v)
-> M v (SignConf (Polynomial Rational v))
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)
-> StateT
     (Assumption 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)
-> StateT
     (Assumption 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
      (Cell (Polynomial Rational v),
 Map (UPolynomial (Polynomial Rational v)) Sign)
-> StateT
     (Assumption v)
     []
     (Cell (Polynomial Rational v),
      Map (UPolynomial (Polynomial Rational v)) Sign)
forall (m :: * -> *) a. Monad m => a -> m a
return (Point (Polynomial Rational v) -> Cell (Polynomial Rational v)
forall c. Point c -> Cell c
Point Point (Polynomial Rational v)
pt, UPolynomial (Polynomial Rational v)
-> Sign
-> Map (UPolynomial (Polynomial Rational v)) Sign
-> Map (UPolynomial (Polynomial Rational v)) Sign
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 = (Cell (Polynomial Rational v),
 Map (UPolynomial (Polynomial Rational v)) Sign)
-> StateT
     (Assumption v)
     []
     (Cell (Polynomial Rational v),
      Map (UPolynomial (Polynomial Rational v)) Sign)
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 (Cell (Polynomial Rational v),
 Map (UPolynomial (Polynomial Rational v)) Sign)
-> SignConf (Polynomial Rational v)
-> SignConf (Polynomial Rational v)
forall a. a -> [a] -> [a]
: SignConf (Polynomial Rational v)
ys SignConf (Polynomial Rational v)
-> SignConf (Polynomial Rational v)
-> SignConf (Polynomial Rational v)
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 (Cell (Polynomial Rational v),
 Map (UPolynomial (Polynomial Rational v)) Sign)
-> SignConf (Polynomial Rational v)
-> SignConf (Polynomial Rational v)
forall a. a -> [a] -> [a]
: SignConf (Polynomial Rational v)
xs)
      where
        s1 :: Sign
s1 = UPolynomial (Polynomial Rational v)
-> Map (UPolynomial (Polynomial Rational v)) Sign -> Sign
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 = UPolynomial (Polynomial Rational v)
-> Map (UPolynomial (Polynomial Rational v)) Sign -> Sign
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 Sign -> Sign -> Bool
forall a. Eq a => a -> a -> Bool
== Sign
Zero then Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 else Int
n
        root :: Point (Polynomial Rational v)
root = UPolynomial (Polynomial Rational v)
-> Int -> Point (Polynomial Rational v)
forall c. UPolynomial c -> Int -> Point c
RootOf UPolynomial (Polynomial Rational v)
p Int
n1
        (SignConf (Polynomial Rational v)
ys, Int
n2)
           | Sign
s1 Sign -> Sign -> Bool
forall a. Eq a => a -> a -> Bool
== Sign
s2   = ( [ (Point (Polynomial Rational v)
-> Point (Polynomial Rational v) -> Cell (Polynomial Rational v)
forall c. Point c -> Point c -> Cell c
Interval Point (Polynomial Rational v)
lb Point (Polynomial Rational v)
ub, UPolynomial (Polynomial Rational v)
-> Sign
-> Map (UPolynomial (Polynomial Rational v)) Sign
-> Map (UPolynomial (Polynomial Rational v)) Sign
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 Sign -> Sign -> Bool
forall a. Eq a => a -> a -> Bool
== Sign
Zero = ( [ (Point (Polynomial Rational v)
-> Point (Polynomial Rational v) -> Cell (Polynomial Rational v)
forall c. Point c -> Point c -> Cell c
Interval Point (Polynomial Rational v)
lb Point (Polynomial Rational v)
ub, UPolynomial (Polynomial Rational v)
-> Sign
-> Map (UPolynomial (Polynomial Rational v)) Sign
-> Map (UPolynomial (Polynomial Rational v)) Sign
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 Sign -> Sign -> Bool
forall a. Eq a => a -> a -> Bool
== Sign
Zero = ( [ (Point (Polynomial Rational v)
-> Point (Polynomial Rational v) -> Cell (Polynomial Rational v)
forall c. Point c -> Point c -> Cell c
Interval Point (Polynomial Rational v)
lb Point (Polynomial Rational v)
ub, UPolynomial (Polynomial Rational v)
-> Sign
-> Map (UPolynomial (Polynomial Rational v)) Sign
-> Map (UPolynomial (Polynomial Rational v)) Sign
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  = ( [ (Point (Polynomial Rational v)
-> Point (Polynomial Rational v) -> Cell (Polynomial Rational v)
forall c. Point c -> Point c -> Cell c
Interval Point (Polynomial Rational v)
lb Point (Polynomial Rational v)
root, UPolynomial (Polynomial Rational v)
-> Sign
-> Map (UPolynomial (Polynomial Rational v)) Sign
-> Map (UPolynomial (Polynomial Rational v)) Sign
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)
                            , (Point (Polynomial Rational v) -> Cell (Polynomial Rational v)
forall c. Point c -> Cell c
Point Point (Polynomial Rational v)
root,       UPolynomial (Polynomial Rational v)
-> Sign
-> Map (UPolynomial (Polynomial Rational v)) Sign
-> Map (UPolynomial (Polynomial Rational v)) Sign
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)
                            , (Point (Polynomial Rational v)
-> Point (Polynomial Rational v) -> Cell (Polynomial Rational v)
forall c. Point c -> Point c -> Cell c
Interval Point (Polynomial Rational v)
root Point (Polynomial Rational v)
ub, UPolynomial (Polynomial Rational v)
-> Sign
-> Map (UPolynomial (Polynomial Rational v)) Sign
-> Map (UPolynomial (Polynomial Rational v)) Sign
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 Int -> Int -> Int
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 (MonomialOrder X
-> UPolynomial (Polynomial Rational v) -> Polynomial Rational v
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) = MonomialOrder X
-> UPolynomial (Polynomial Rational v)
-> (Polynomial Rational v, Monomial X)
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 Integer -> Bool
forall a. Integral a => a -> Bool
even (Monomial X -> Integer
forall t. Degree t => t -> Integer
P.deg Monomial X
mm)
        then Polynomial Rational v -> M v Sign
signCoeff Polynomial Rational v
c
        else (Sign -> Sign) -> M v Sign -> M v Sign
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Sign -> Sign
Sign.negate (M v Sign -> M v Sign) -> M v Sign -> M v Sign
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) = UPolynomial (Polynomial Rational v)
-> UPolynomial (Polynomial Rational v)
-> (Polynomial Rational v, Integer,
    UPolynomial (Polynomial Rational v))
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 <- UPolynomial (Polynomial Rational v)
-> M v (UPolynomial (Polynomial Rational v))
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 UPolynomial (Polynomial Rational v) -> Integer
forall t. Degree t => t -> Integer
P.deg UPolynomial (Polynomial Rational v)
r Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0
            then Sign -> M v Sign
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign -> M v Sign) -> Sign -> M v Sign
forall a b. (a -> b) -> a -> b
$ UPolynomial (Polynomial Rational v)
-> Map (UPolynomial (Polynomial Rational v)) Sign -> Sign
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 (Polynomial Rational v -> M v Sign)
-> Polynomial Rational v -> M v Sign
forall a b. (a -> b) -> a -> b
$ Monomial X
-> UPolynomial (Polynomial Rational v) -> Polynomial Rational v
forall k v. (Num k, Ord v) => Monomial v -> Polynomial k v -> k
P.coeff Monomial X
forall v. Monomial v
P.mone UPolynomial (Polynomial Rational v)
r
      -- 場合分けを出来るだけ避ける
      if Integer -> Bool
forall a. Integral a => a -> Bool
even Integer
k
        then Sign -> M v Sign
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
          Sign -> M v Sign
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign -> M v Sign) -> Sign -> M v Sign
forall a b. (a -> b) -> a -> b
$ Sign
s1 Sign -> Sign -> Sign
`Sign.div` Sign -> Integer -> Sign
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 =
      [M v Sign] -> M v Sign
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ Polynomial Rational v -> [Sign] -> M v ()
forall v.
(Ord v, Show v, PrettyVar v) =>
Polynomial Rational v -> [Sign] -> M v ()
assume Polynomial Rational v
c [Sign
s] M v () -> M v Sign -> M v Sign
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Sign -> M v Sign
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 :: Assumption v
emptyAssumption = (Map (Polynomial Rational v) (Set Sign)
forall k a. Map k a
Map.empty, [])

propagate :: Ord v => Assumption v -> Maybe (Assumption v)
propagate :: Assumption v -> Maybe (Assumption v)
propagate = Assumption v -> Maybe (Assumption v)
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' <- Assumption v -> Maybe (Assumption v)
forall v. Ord v => Assumption v -> Maybe (Assumption v)
f Assumption v
a
      if Assumption v
a Assumption v -> Assumption v -> Bool
forall a. Eq a => a -> a -> Bool
== Assumption v
a'
        then Assumption v -> Maybe (Assumption v)
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 = (Assumption v -> Assumption v)
-> Maybe (Assumption v) -> Maybe (Assumption v)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Assumption v -> Assumption v
forall v. Ord v => Assumption v -> Assumption v
dropConstants (Maybe (Assumption v) -> Maybe (Assumption v))
-> Maybe (Assumption v) -> Maybe (Assumption v)
forall a b. (a -> b) -> a -> b
$ Assumption v -> Maybe (Assumption v)
forall v. Ord v => Assumption v -> Maybe (Assumption v)
propagateSign (Assumption v -> Maybe (Assumption v))
-> Maybe (Assumption v) -> Maybe (Assumption v)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Assumption v -> Maybe (Assumption v)
forall v. Ord v => Assumption v -> Maybe (Assumption v)
propagateEq Assumption v
a

propagateEq :: forall v. Ord v => Assumption v -> Maybe (Assumption v)
propagateEq :: Assumption v -> Maybe (Assumption v)
propagateEq (Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb)
  | ((Polynomial Rational v, Set Sign) -> Bool)
-> [(Polynomial Rational v, Set Sign)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\(Polynomial Rational v
p,Set Sign
ss) -> Sign -> Set Sign
forall a. a -> Set a
Set.singleton Sign
Zero Set Sign -> Set Sign -> Bool
forall a. Eq a => a -> a -> Bool
== Set Sign
ss) (Map (Polynomial Rational v) (Set Sign)
-> [(Polynomial Rational v, Set Sign)]
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') <- Assumption v -> Maybe (Assumption v)
f (Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb)
      Assumption v -> Maybe (Assumption v)
forall v. Ord v => Assumption v -> Maybe (Assumption v)
propagateEq (Map (Polynomial Rational v) (Set Sign)
m', [Polynomial Rational v]
gb')
  | Bool
otherwise =
      Assumption v -> Maybe (Assumption v)
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 :: Assumption v -> Maybe (Assumption v)
f (Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb) =
      case (Set Sign -> Bool)
-> Map (Polynomial Rational v) (Set Sign)
-> (Map (Polynomial Rational v) (Set Sign),
    Map (Polynomial Rational v) (Set Sign))
forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partition (Sign -> Set Sign
forall a. a -> Set a
Set.singleton Sign
Zero Set Sign -> Set Sign -> Bool
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' = MonomialOrder v
-> [Polynomial Rational v] -> [Polynomial Rational v]
forall k v.
(Eq k, Fractional k, Ord k, Ord v) =>
MonomialOrder v -> [Polynomial k v] -> [Polynomial k v]
GB.basis MonomialOrder v
forall v. Ord v => MonomialOrder v
P.grevlex (Map (Polynomial Rational v) (Set Sign) -> [Polynomial Rational v]
forall k a. Map k a -> [k]
Map.keys Map (Polynomial Rational v) (Set Sign)
m0 [Polynomial Rational v]
-> [Polynomial Rational v] -> [Polynomial Rational v]
forall a. [a] -> [a] -> [a]
++ [Polynomial Rational v]
gb)
              m' :: Map (Polynomial Rational v) (Set Sign)
m'  = (Set Sign -> Set Sign -> Set Sign)
-> [(Polynomial Rational v, Set Sign)]
-> Map (Polynomial Rational v) (Set Sign)
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Set Sign -> Set Sign -> Set Sign
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection ([(Polynomial Rational v, Set Sign)]
 -> Map (Polynomial Rational v) (Set Sign))
-> [(Polynomial Rational v, Set Sign)]
-> Map (Polynomial Rational v) (Set Sign)
forall a b. (a -> b) -> a -> b
$ do
                      (Polynomial Rational v
p,Set Sign
ss) <- Map (Polynomial Rational v) (Set Sign)
-> [(Polynomial Rational v, Set Sign)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Polynomial Rational v) (Set Sign)
m
                      let p' :: Polynomial Rational v
p'   = MonomialOrder v
-> Polynomial Rational v
-> [Polynomial Rational v]
-> Polynomial Rational v
forall k v.
(Eq k, Fractional k, Ord v) =>
MonomialOrder v
-> Polynomial k v -> [Polynomial k v] -> Polynomial k v
P.reduce MonomialOrder v
forall v. Ord v => MonomialOrder v
P.grevlex Polynomial Rational v
p [Polynomial Rational v]
gb'
                          c :: Rational
c    = MonomialOrder v -> Polynomial Rational v -> Rational
forall k v. Num k => MonomialOrder v -> Polynomial k v -> k
P.lc MonomialOrder v
forall v. Ord v => MonomialOrder v
P.grlex Polynomial Rational v
p'
                          (Polynomial Rational v
p'',Set Sign
ss')
                            | Rational
c Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
0    = (Polynomial Rational v
p', Set Sign
ss)
                            | Bool
otherwise = ((Rational -> Rational)
-> Polynomial Rational v -> Polynomial Rational v
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff (Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/Rational
c) Polynomial Rational v
p', (Sign -> Sign) -> Set Sign -> Set Sign
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\Sign
s -> Sign
s Sign -> Sign -> Sign
`Sign.div` Rational -> Sign
forall a. Real a => a -> Sign
Sign.signOf Rational
c) Set Sign
ss)
                      (Polynomial Rational v, Set Sign)
-> [(Polynomial Rational v, Set Sign)]
forall (m :: * -> *) a. Monad m => a -> m a
return (Polynomial Rational v
p'', Set Sign
ss')
          Assumption v -> Maybe (Assumption v)
forall (m :: * -> *) a. Monad m => a -> m a
return (Assumption v -> Maybe (Assumption v))
-> Assumption v -> Maybe (Assumption v)
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 :: Assumption v -> Maybe (Assumption v)
propagateSign (Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb) = Assumption v -> Maybe (Assumption v)
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 ((Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
-> Bool
forall v. Ord v => Assumption v -> Bool
isOkay (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
a) = Maybe
  (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
forall a. Maybe a
Nothing
      | Map (Polynomial Rational v) (Set Sign)
m Map (Polynomial Rational v) (Set Sign)
-> Map (Polynomial Rational v) (Set Sign) -> Bool
forall a. Eq a => a -> a -> Bool
== Map (Polynomial Rational v) (Set Sign)
m'   = (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
-> Maybe
     (Map (Polynomial Rational v) (Set Sign), [Polynomial Rational v])
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' = (Polynomial Rational v -> Set Sign -> Set Sign)
-> Map (Polynomial Rational v) (Set Sign)
-> Map (Polynomial Rational v) (Set Sign)
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (\Polynomial Rational v
p Set Sign
ss -> Set Sign -> Set Sign -> Set Sign
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set Sign
ss (Map (Polynomial Rational v) (Set Sign)
-> Polynomial Rational v -> Set Sign
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 :: Assumption v -> Bool
isOkay (Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb) =
  [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool -> Bool
not (Set Sign -> Bool
forall a. Set a -> Bool
Set.null Set Sign
ss) | (Polynomial Rational v
_,Set Sign
ss) <- Map (Polynomial Rational v) (Set Sign)
-> [(Polynomial Rational v, Set Sign)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Polynomial Rational v) (Set Sign)
m] Bool -> Bool -> Bool
&&
  [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Sign -> Set Sign -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Sign
Zero (Map (Polynomial Rational v) (Set Sign)
-> Polynomial Rational v -> Set Sign
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 :: Assumption v -> Assumption v
dropConstants (Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb) = ((Polynomial Rational v -> Set Sign -> Bool)
-> Map (Polynomial Rational v) (Set Sign)
-> Map (Polynomial Rational v) (Set Sign)
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\Polynomial Rational v
p Set Sign
_ -> Polynomial Rational v -> Integer
forall t. Degree t => t -> Integer
P.deg Polynomial Rational v
p Integer -> Integer -> Bool
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 :: Assumption v -> [(Polynomial Rational v, [Sign])]
assumption2cond (Map (Polynomial Rational v) (Set Sign)
m, [Polynomial Rational v]
gb) = [(Polynomial Rational v
p, Set Sign -> [Sign]
forall a. Set a -> [a]
Set.toList Set Sign
ss)  | (Polynomial Rational v
p, Set Sign
ss) <- Map (Polynomial Rational v) (Set Sign)
-> [(Polynomial Rational v, Set Sign)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Polynomial Rational v) (Set Sign)
m] [(Polynomial Rational v, [Sign])]
-> [(Polynomial Rational v, [Sign])]
-> [(Polynomial Rational v, [Sign])]
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 :: Map (Polynomial Rational v) (Set Sign)
-> Polynomial Rational v -> Set Sign
computeSignSet Map (Polynomial Rational v) (Set Sign)
m Polynomial Rational v
p = (v -> Set Sign) -> Polynomial (Set Sign) v -> Set Sign
forall k v. Num k => (v -> k) -> Polynomial k v -> k
P.eval v -> Set Sign
env ((Rational -> Set Sign)
-> Polynomial Rational v -> Polynomial (Set Sign) v
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff Rational -> Set Sign
forall a. Fractional a => Rational -> a
fromRational Polynomial Rational v
p)
  where
    env :: v -> Set Sign
env v
v =
      case Polynomial Rational v
-> Map (Polynomial Rational v) (Set Sign) -> Maybe (Set Sign)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (v -> Polynomial Rational v
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 -> [Sign] -> Set Sign
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 :: Model v -> Cell (Polynomial Rational v) -> Maybe AReal
findSample Model v
m Cell (Polynomial Rational v)
cell =
  case Model v -> Cell (Polynomial Rational v) -> Cell Rational
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) ->
      AReal -> Maybe AReal
forall a. a -> Maybe a
Just (AReal -> Maybe AReal) -> AReal -> Maybe AReal
forall a b. (a -> b) -> a -> b
$ UPolynomial Rational -> [AReal]
AReal.realRoots UPolynomial Rational
p [AReal] -> Int -> AReal
forall a. [a] -> Int -> a
!! Int
n
    Interval Point Rational
lb Point Rational
ub ->
      case Interval AReal -> Maybe Rational
forall r. RealFrac r => Interval r -> Maybe Rational
I.simplestRationalWithin (Point Rational -> Extended AReal
f Point Rational
lb Extended AReal -> Extended AReal -> Interval AReal
forall r. Ord r => Extended r -> Extended r -> Interval r
I.<..< Point Rational -> Extended AReal
f Point Rational
ub) of
        Maybe Rational
Nothing -> String -> Maybe AReal
forall a. (?callStack::CallStack) => String -> a
error (String -> Maybe AReal) -> String -> Maybe AReal
forall a b. (a -> b) -> a -> b
$ String
"ToySolver.CAD.findSample: should not happen"
        Just Rational
r  -> AReal -> Maybe AReal
forall a. a -> Maybe a
Just (AReal -> Maybe AReal) -> AReal -> Maybe AReal
forall a b. (a -> b) -> a -> b
$ Rational -> AReal
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       = Extended AReal
forall r. Extended r
I.NegInf
    f Point Rational
PosInf       = Extended AReal
forall r. Extended r
I.PosInf
    f (RootOf UPolynomial Rational
p Int
n) = AReal -> Extended AReal
forall r. r -> Extended r
I.Finite (UPolynomial Rational -> [AReal]
AReal.realRoots UPolynomial Rational
p [AReal] -> Int -> AReal
forall a. [a] -> Int -> a
!! Int
n)

evalCell :: Ord v => Model v -> Cell (Polynomial Rational v) -> Cell Rational
evalCell :: Model v -> Cell (Polynomial Rational v) -> Cell Rational
evalCell Model v
m (Point Point (Polynomial Rational v)
pt)         = Point Rational -> Cell Rational
forall c. Point c -> Cell c
Point (Point Rational -> Cell Rational)
-> Point Rational -> Cell Rational
forall a b. (a -> b) -> a -> b
$ Model v -> Point (Polynomial Rational v) -> Point Rational
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) = Point Rational -> Point Rational -> Cell Rational
forall c. Point c -> Point c -> Cell c
Interval (Model v -> Point (Polynomial Rational v) -> Point Rational
forall v.
Ord v =>
Model v -> Point (Polynomial Rational v) -> Point Rational
evalPoint Model v
m Point (Polynomial Rational v)
pt1) (Model v -> Point (Polynomial Rational v) -> Point Rational
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 :: Model v -> Point (Polynomial Rational v) -> Point Rational
evalPoint Model v
_ Point (Polynomial Rational v)
NegInf = Point Rational
forall c. Point c
NegInf
evalPoint Model v
_ Point (Polynomial Rational v)
PosInf = Point Rational
forall c. Point c
PosInf
evalPoint Model v
m (RootOf UPolynomial (Polynomial Rational v)
p Int
n) = UPolynomial Rational -> Int -> Point Rational
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 ((Polynomial Rational v -> AReal)
-> UPolynomial (Polynomial Rational v) -> UPolynomial AReal
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff ((v -> AReal) -> Polynomial AReal v -> AReal
forall k v. Num k => (v -> k) -> Polynomial k v -> k
P.eval (Model v
m Model v -> v -> AReal
forall k a. Ord k => Map k a -> k -> a
Map.!) (Polynomial AReal v -> AReal)
-> (Polynomial Rational v -> Polynomial AReal v)
-> Polynomial Rational v
-> AReal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rational -> AReal) -> Polynomial Rational v -> Polynomial AReal v
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff Rational -> AReal
forall a. Fractional a => Rational -> a
fromRational) UPolynomial (Polynomial Rational v)
p) [AReal] -> Int -> AReal
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 :: v
-> [OrdRel (Polynomial Rational v)]
-> [([OrdRel (Polynomial Rational v)], Model v -> Model v)]
project v
v [OrdRel (Polynomial Rational v)]
cs = Set v
-> [OrdRel (Polynomial Rational v)]
-> [([OrdRel (Polynomial Rational v)], Model v -> Model v)]
forall v.
(Ord v, Show v, PrettyVar v) =>
Set v
-> [OrdRel (Polynomial Rational v)]
-> [([OrdRel (Polynomial Rational v)], Model v -> Model v)]
projectN (v -> Set v
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 :: 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) <- Set v
-> [(Polynomial Rational v, [Sign])]
-> [([(Polynomial Rational v, [Sign])], Model v -> Model v)]
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 ((OrdRel (Polynomial Rational v) -> (Polynomial Rational v, [Sign]))
-> [OrdRel (Polynomial Rational v)]
-> [(Polynomial Rational v, [Sign])]
forall a b. (a -> b) -> [a] -> [b]
map OrdRel (Polynomial Rational v) -> (Polynomial Rational v, [Sign])
forall a. Num a => OrdRel a -> (a, [Sign])
f [OrdRel (Polynomial Rational v)]
cs)
  ([OrdRel (Polynomial Rational v)], Model v -> Model v)
-> [([OrdRel (Polynomial Rational v)], Model v -> Model v)]
forall (m :: * -> *) a. Monad m => a -> m a
return (((Polynomial Rational v, [Sign]) -> OrdRel (Polynomial Rational v))
-> [(Polynomial Rational v, [Sign])]
-> [OrdRel (Polynomial Rational v)]
forall a b. (a -> b) -> [a] -> [b]
map (Polynomial Rational v, [Sign]) -> OrdRel (Polynomial Rational v)
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 a -> a -> a
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) = (e -> RelOp -> e -> OrdRel e
forall e. e -> RelOp -> e -> OrdRel e
OrdRel e
p RelOp
op e
0)
      where
        ss' :: Set Sign
ss' = [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign]
ss
        op :: RelOp
op
          | Set Sign
ss' Set Sign -> Set Sign -> Bool
forall a. Eq a => a -> a -> Bool
== [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Zero, Sign
Neg] = RelOp
Le
          | Set Sign
ss' Set Sign -> Set Sign -> Bool
forall a. Eq a => a -> a -> Bool
== [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Zero, Sign
Pos] = RelOp
Ge
          | Set Sign
ss' Set Sign -> Set Sign -> Bool
forall a. Eq a => a -> a -> Bool
== [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Neg]       = RelOp
Lt
          | Set Sign
ss' Set Sign -> Set Sign -> Bool
forall a. Eq a => a -> a -> Bool
== [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Pos]       = RelOp
Gt
          | Set Sign
ss' Set Sign -> Set Sign -> Bool
forall a. Eq a => a -> a -> Bool
== [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Zero]      = RelOp
Eql
          | Set Sign
ss' Set Sign -> Set Sign -> Bool
forall a. Eq a => a -> a -> Bool
== [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Pos,Sign
Neg]   = RelOp
NEq
          | Bool
otherwise = String -> RelOp
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' :: Set v
-> [(Polynomial Rational v, [Sign])]
-> [([(Polynomial Rational v, [Sign])], Model v -> Model v)]
projectN' Set v
vs = [v]
-> [(Polynomial Rational v, [Sign])]
-> [([(Polynomial Rational v, [Sign])], Model v -> Model v)]
forall v.
(Show v, PrettyVar v, Ord v) =>
[v]
-> [(Polynomial Rational v, [Sign])]
-> [([(Polynomial Rational v, [Sign])],
     Map v AReal -> Map v AReal)]
loop (Set v -> [v]
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 = ([(Polynomial Rational v, [Sign])], Map v AReal -> Map v AReal)
-> [([(Polynomial Rational v, [Sign])],
     Map v AReal -> Map v AReal)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Polynomial Rational v, [Sign])]
cs, Map v AReal -> Map v AReal
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)]
_) <- [(UPolynomial (Polynomial Rational v), [Sign])]
-> [([(Polynomial Rational v, [Sign])],
     [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' [(Polynomial Rational v -> v -> UPolynomial (Polynomial Rational v)
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 = Map v AReal -> Cell (Polynomial Rational v) -> Maybe AReal
forall v.
Ord v =>
Model v -> Cell (Polynomial Rational v) -> Maybe AReal
findSample Map v AReal
m Cell (Polynomial Rational v)
cell
            in AReal -> Map v AReal -> Map v AReal
seq AReal
val (Map v AReal -> Map v AReal) -> Map v AReal -> Map v AReal
forall a b. (a -> b) -> a -> b
$ v -> AReal -> Map v AReal -> Map v AReal
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
      ([(Polynomial Rational v, [Sign])], Map v AReal -> Map v AReal)
-> [([(Polynomial Rational v, [Sign])],
     Map v AReal -> Map v AReal)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Polynomial Rational v, [Sign])]
cs3, Map v AReal -> Map v AReal
mt1 (Map v AReal -> Map v AReal)
-> (Map v AReal -> Map v AReal) -> Map v AReal -> Map v AReal
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 :: Set v -> [OrdRel (Polynomial Rational v)] -> Maybe (Model v)
solve Set v
vs [OrdRel (Polynomial Rational v)]
cs0 = Set v -> [(Polynomial Rational v, [Sign])] -> Maybe (Model v)
forall v.
(Ord v, Show v, PrettyVar v) =>
Set v -> [(Polynomial Rational v, [Sign])] -> Maybe (Model v)
solve' Set v
vs ((OrdRel (Polynomial Rational v) -> (Polynomial Rational v, [Sign]))
-> [OrdRel (Polynomial Rational v)]
-> [(Polynomial Rational v, [Sign])]
forall a b. (a -> b) -> [a] -> [b]
map OrdRel (Polynomial Rational v) -> (Polynomial Rational v, [Sign])
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 a -> a -> a
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' :: Set v -> [(Polynomial Rational v, [Sign])] -> Maybe (Model v)
solve' Set v
vs [(Polynomial Rational v, [Sign])]
cs0 = [Model v] -> Maybe (Model v)
forall a. [a] -> Maybe a
listToMaybe ([Model v] -> Maybe (Model v)) -> [Model v] -> Maybe (Model v)
forall a b. (a -> b) -> a -> b
$ do
  ([(Polynomial Rational v, [Sign])]
cs,Model v -> Model v
mt) <- Set v
-> [(Polynomial Rational v, [Sign])]
-> [([(Polynomial Rational v, [Sign])], Model v -> Model v)]
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 = Map k a
forall k a. Map k a
Map.empty
  Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Rational -> Sign
forall a. Real a => a -> Sign
Sign.signOf Rational
v Sign -> [Sign] -> Bool
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 = (v -> Rational) -> Polynomial Rational v -> Rational
forall k v. Num k => (v -> k) -> Polynomial k v -> k
P.eval (Map v Rational
forall k a. Map k a
m Map v Rational -> v -> Rational
forall k a. Ord k => Map k a -> k -> a
Map.!) Polynomial Rational v
p]
  Model v -> [Model v]
forall (m :: * -> *) a. Monad m => a -> m a
return (Model v -> [Model v]) -> Model v -> [Model v]
forall a b. (a -> b) -> a -> b
$ Model v -> Model v
mt Model v
forall k a. Map k a
m

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

showDNF :: (Ord v, Show v, PrettyVar v) => DNF (Polynomial Rational v, [Sign]) -> String
showDNF :: DNF (Polynomial Rational v, [Sign]) -> String
showDNF (DNF [[(Polynomial Rational v, [Sign])]]
xss) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" | " [[(Polynomial Rational v, [Sign])] -> 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
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" & " [a -> [Sign] -> String
forall a. Pretty a => a -> [Sign] -> String
f a
p [Sign]
ss | (a
p,[Sign]
ss) <- [(a, [Sign])]
xs] String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
    f :: a -> [Sign] -> String
f a
p [Sign]
ss = a -> String
forall a. Pretty a => a -> String
prettyShow a
p String -> ShowS
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
      | [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign]
xs Set Sign -> Set Sign -> Bool
forall a. Eq a => a -> a -> Bool
== [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Pos,Sign
Neg] = String
"/= 0"
      | [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign]
xs Set Sign -> Set Sign -> Bool
forall a. Eq a => a -> a -> Bool
== [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Zero,Sign
Pos] = String
">= 0"
      | [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign]
xs Set Sign -> Set Sign -> Bool
forall a. Eq a => a -> a -> Bool
== [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Zero,Sign
Neg] = String
"<= 0"
      | Bool
otherwise = ShowS
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 :: [([(Polynomial Rational v, [Sign])],
  [Cell (Polynomial Rational v)])]
-> IO ()
dumpProjection [([(Polynomial Rational v, [Sign])],
  [Cell (Polynomial Rational v)])]
xs =
  [([(Polynomial Rational v, [Sign])],
  [Cell (Polynomial Rational v)])]
-> (([(Polynomial Rational v, [Sign])],
     [Cell (Polynomial Rational v)])
    -> IO ())
-> IO ()
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 ((([(Polynomial Rational v, [Sign])],
   [Cell (Polynomial Rational v)])
  -> IO ())
 -> IO ())
-> (([(Polynomial Rational v, [Sign])],
     [Cell (Polynomial Rational v)])
    -> IO ())
-> IO ()
forall a b. (a -> b) -> a -> b
$ \([(Polynomial Rational v, [Sign])]
gs, [Cell (Polynomial Rational v)]
cells) -> do
    String -> IO ()
putStrLn String
"============"
    [(Polynomial Rational v, [Sign])]
-> ((Polynomial Rational v, [Sign]) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Polynomial Rational v, [Sign])]
gs (((Polynomial Rational v, [Sign]) -> IO ()) -> IO ())
-> ((Polynomial Rational v, [Sign]) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Polynomial Rational v
p, [Sign]
ss) -> do
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Polynomial Rational v -> [Sign] -> String
forall a. Pretty a => a -> [Sign] -> String
f Polynomial Rational v
p [Sign]
ss
    String -> IO ()
putStrLn String
" =>"
    [Cell (Polynomial Rational v)]
-> (Cell (Polynomial Rational v) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Cell (Polynomial Rational v)]
cells ((Cell (Polynomial Rational v) -> IO ()) -> IO ())
-> (Cell (Polynomial Rational v) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Cell (Polynomial Rational v)
cell -> do
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Cell (Polynomial Rational v) -> String
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 = a -> String
forall a. Pretty a => a -> String
prettyShow a
p String -> ShowS
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
      | [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign]
xs Set Sign -> Set Sign -> Bool
forall a. Eq a => a -> a -> Bool
== [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Pos,Sign
Neg]  = String
"/= 0"
      | [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign]
xs Set Sign -> Set Sign -> Bool
forall a. Eq a => a -> a -> Bool
== [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Zero,Sign
Pos] = String
">= 0"
      | [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign]
xs Set Sign -> Set Sign -> Bool
forall a. Eq a => a -> a -> Bool
== [Sign] -> Set Sign
forall a. Ord a => [a] -> Set a
Set.fromList [Sign
Zero,Sign
Neg] = String
"<= 0"
      | Bool
otherwise = ShowS
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 :: [(SignConf (Polynomial Rational v), Assumption v)] -> IO ()
dumpSignConf [(SignConf (Polynomial Rational v), Assumption v)]
x =
  [(SignConf (Polynomial Rational v), Assumption v)]
-> ((SignConf (Polynomial Rational v), Assumption v) -> IO ())
-> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(SignConf (Polynomial Rational v), Assumption v)]
x (((SignConf (Polynomial Rational v), Assumption v) -> IO ())
 -> IO ())
-> ((SignConf (Polynomial Rational v), Assumption v) -> IO ())
-> IO ()
forall a b. (a -> b) -> a -> b
$ \(SignConf (Polynomial Rational v)
conf, Assumption v
as) -> do
    String -> IO ()
putStrLn String
"============"
    (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn ([String] -> IO ()) -> [String] -> IO ()
forall a b. (a -> b) -> a -> b
$ SignConf (Polynomial Rational v) -> [String]
forall c. (Num c, Ord c, PrettyCoeff c) => SignConf c -> [String]
showSignConf SignConf (Polynomial Rational v)
conf
    [(Polynomial Rational v, [Sign])]
-> ((Polynomial Rational v, [Sign]) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_  (Assumption v -> [(Polynomial Rational v, [Sign])]
forall v.
Ord v =>
Assumption v -> [(Polynomial Rational v, [Sign])]
assumption2cond Assumption v
as) (((Polynomial Rational v, [Sign]) -> IO ()) -> IO ())
-> ((Polynomial Rational v, [Sign]) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Polynomial Rational v
p, [Sign]
ss) ->
      String -> String -> String -> IO ()
forall r. PrintfType r => String -> r
printf String
"%s %s\n" (Polynomial Rational v -> String
forall a. Pretty a => a -> String
prettyShow Polynomial Rational v
p) ([Sign] -> String
forall a. Show a => a -> String
show [Sign]
ss)

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

test1a :: IO ()
test1a :: IO ()
test1a = (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn ([String] -> IO ()) -> [String] -> IO ()
forall a b. (a -> b) -> a -> b
$ SignConf (Coeff Int) -> [String]
forall c. (Num c, Ord c, PrettyCoeff c) => SignConf c -> [String]
showSignConf SignConf (Coeff Int)
conf
  where
    x :: UPolynomial (Coeff Int)
x = X -> UPolynomial (Coeff Int)
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 UPolynomial (Coeff Int)
-> UPolynomial (Coeff Int) -> UPolynomial (Coeff Int)
forall a. Num a => a -> a -> a
+ UPolynomial (Coeff Int)
1, -UPolynomial (Coeff Int)
2UPolynomial (Coeff Int)
-> UPolynomial (Coeff Int) -> UPolynomial (Coeff Int)
forall a. Num a => a -> a -> a
*UPolynomial (Coeff Int)
x UPolynomial (Coeff Int)
-> UPolynomial (Coeff Int) -> UPolynomial (Coeff Int)
forall a. Num a => a -> a -> a
+ UPolynomial (Coeff Int)
3, UPolynomial (Coeff Int)
x]
    [(SignConf (Coeff Int)
conf, Assumption Int
_)] = M Int (SignConf (Coeff Int))
-> [(SignConf (Coeff Int), Assumption Int)]
forall v a. M v a -> [(a, Assumption v)]
runM (M Int (SignConf (Coeff Int))
 -> [(SignConf (Coeff Int), Assumption Int)])
-> M Int (SignConf (Coeff Int))
-> [(SignConf (Coeff Int), Assumption Int)]
forall a b. (a -> b) -> a -> b
$ [UPolynomial (Coeff Int)] -> M Int (SignConf (Coeff Int))
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 = Maybe (Model X) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Model X) -> Bool) -> Maybe (Model X) -> Bool
forall a b. (a -> b) -> a -> b
$ Set X -> [OrdRel (UPolynomial Rational)] -> Maybe (Model X)
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 = X -> UPolynomial Rational
forall a v. Var a v => v -> a
P.var X
X
    vs :: Set X
vs = X -> Set X
forall a. a -> Set a
Set.singleton X
X
    cs :: [OrdRel (UPolynomial Rational)]
cs = [UPolynomial Rational
x UPolynomial Rational
-> UPolynomial Rational -> UPolynomial Rational
forall a. Num a => a -> a -> a
+ UPolynomial Rational
1 UPolynomial Rational
-> UPolynomial Rational -> OrdRel (UPolynomial Rational)
forall e r. IsOrdRel e r => e -> e -> r
.>. UPolynomial Rational
0, -UPolynomial Rational
2UPolynomial Rational
-> UPolynomial Rational -> UPolynomial Rational
forall a. Num a => a -> a -> a
*UPolynomial Rational
x UPolynomial Rational
-> UPolynomial Rational -> UPolynomial Rational
forall a. Num a => a -> a -> a
+ UPolynomial Rational
3 UPolynomial Rational
-> UPolynomial Rational -> OrdRel (UPolynomial Rational)
forall e r. IsOrdRel e r => e -> e -> r
.>. UPolynomial Rational
0, UPolynomial Rational
x UPolynomial Rational
-> UPolynomial Rational -> OrdRel (UPolynomial Rational)
forall e r. IsOrdRel e r => e -> e -> r
.>. UPolynomial Rational
0]

test1c :: Bool
test1c :: Bool
test1c = Maybe () -> Bool
forall a. Maybe a -> Bool
isJust (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do
  Model X
m <- Set X -> [(UPolynomial Rational, [Sign])] -> Maybe (Model X)
forall v.
(Ord v, Show v, PrettyVar v) =>
Set v -> [(Polynomial Rational v, [Sign])] -> Maybe (Model v)
solve' (X -> Set X
forall a. a -> Set a
Set.singleton X
X) [(UPolynomial Rational, [Sign])]
cs
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ do
    (UPolynomial Rational
p, [Sign]
ss) <- [(UPolynomial Rational, [Sign])]
cs
    let val :: AReal
val = (X -> AReal) -> UPolynomial AReal -> AReal
forall k v. Num k => (v -> k) -> Polynomial k v -> k
P.eval (Model X
m Model X -> X -> AReal
forall k a. Ord k => Map k a -> k -> a
Map.!) ((Rational -> AReal) -> UPolynomial Rational -> UPolynomial AReal
forall k1 k v.
(Eq k1, Num k1) =>
(k -> k1) -> Polynomial k v -> Polynomial k1 v
P.mapCoeff Rational -> AReal
forall a. Fractional a => Rational -> a
fromRational UPolynomial Rational
p)
    Bool -> [Bool]
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> [Bool]) -> Bool -> [Bool]
forall a b. (a -> b) -> a -> b
$ AReal -> Sign
forall a. Real a => a -> Sign
Sign.signOf AReal
val Sign -> [Sign] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Sign]
ss
  where
    x :: UPolynomial Rational
x = X -> UPolynomial Rational
forall a v. Var a v => v -> a
P.var X
X
    cs :: [(UPolynomial Rational, [Sign])]
cs = [(UPolynomial Rational
x UPolynomial Rational
-> UPolynomial Rational -> UPolynomial Rational
forall a. Num a => a -> a -> a
+ UPolynomial Rational
1, [Sign
Pos]), (-UPolynomial Rational
2UPolynomial Rational
-> UPolynomial Rational -> UPolynomial Rational
forall a. Num a => a -> a -> a
*UPolynomial Rational
x UPolynomial Rational
-> UPolynomial Rational -> UPolynomial Rational
forall a. Num a => a -> a -> a
+ UPolynomial Rational
3, [Sign
Pos]), (UPolynomial Rational
x, [Sign
Pos])]

test2a :: IO ()
test2a :: IO ()
test2a = (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn ([String] -> IO ()) -> [String] -> IO ()
forall a b. (a -> b) -> a -> b
$ SignConf (Coeff Int) -> [String]
forall c. (Num c, Ord c, PrettyCoeff c) => SignConf c -> [String]
showSignConf SignConf (Coeff Int)
conf
  where
    x :: UPolynomial (Coeff Int)
x = X -> UPolynomial (Coeff Int)
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)
xUPolynomial (Coeff Int) -> Int -> UPolynomial (Coeff Int)
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int)]
    [(SignConf (Coeff Int)
conf, Assumption Int
_)] = M Int (SignConf (Coeff Int))
-> [(SignConf (Coeff Int), Assumption Int)]
forall v a. M v a -> [(a, Assumption v)]
runM (M Int (SignConf (Coeff Int))
 -> [(SignConf (Coeff Int), Assumption Int)])
-> M Int (SignConf (Coeff Int))
-> [(SignConf (Coeff Int), Assumption Int)]
forall a b. (a -> b) -> a -> b
$ [UPolynomial (Coeff Int)] -> M Int (SignConf (Coeff Int))
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 = Maybe (Model X) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe (Model X) -> Bool) -> Maybe (Model X) -> Bool
forall a b. (a -> b) -> a -> b
$ Set X -> [OrdRel (UPolynomial Rational)] -> Maybe (Model X)
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 = X -> UPolynomial Rational
forall a v. Var a v => v -> a
P.var X
X
    vs :: Set X
vs = X -> Set X
forall a. a -> Set a
Set.singleton X
X
    cs :: [OrdRel (UPolynomial Rational)]
cs = [UPolynomial Rational
xUPolynomial Rational -> Int -> UPolynomial Rational
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) UPolynomial Rational
-> UPolynomial Rational -> OrdRel (UPolynomial Rational)
forall e r. IsOrdRel e r => e -> e -> r
.<. UPolynomial Rational
0]

test :: Bool
test = [Bool] -> Bool
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 = [[(Coeff Int, [Sign])]] -> DNF (Coeff Int, [Sign])
forall lit. [[lit]] -> DNF lit
DNF ([[(Coeff Int, [Sign])]] -> DNF (Coeff Int, [Sign]))
-> [[(Coeff Int, [Sign])]] -> DNF (Coeff Int, [Sign])
forall a b. (a -> b) -> a -> b
$ (([(Coeff Int, [Sign])], [Cell (Coeff Int)])
 -> [(Coeff Int, [Sign])])
-> [([(Coeff Int, [Sign])], [Cell (Coeff Int)])]
-> [[(Coeff Int, [Sign])]]
forall a b. (a -> b) -> [a] -> [b]
map ([(Coeff Int, [Sign])], [Cell (Coeff Int)])
-> [(Coeff Int, [Sign])]
forall a b. (a, b) -> a
fst ([([(Coeff Int, [Sign])], [Cell (Coeff Int)])]
 -> [[(Coeff Int, [Sign])]])
-> [([(Coeff Int, [Sign])], [Cell (Coeff Int)])]
-> [[(Coeff Int, [Sign])]]
forall a b. (a -> b) -> a -> b
$ [(UPolynomial (Coeff Int), [Sign])]
-> [([(Coeff Int, [Sign])], [Cell (Coeff Int)])]
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 = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
0
    b :: Coeff Int
b = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
1
    c :: Coeff Int
c = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
2
    x :: Coeff Int
x = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
3
    p :: Polynomial Rational Int
    p :: Coeff Int
p = Coeff Int
aCoeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
*Coeff Int
xCoeff Int -> Int -> Coeff Int
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) Coeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
+ Coeff Int
bCoeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
*Coeff Int
x Coeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
+ Coeff Int
c
    p' :: UPolynomial (Coeff Int)
p' = Coeff Int -> Int -> UPolynomial (Coeff Int)
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 (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ DNF (Coeff Int, [Sign]) -> String
forall v.
(Ord v, Show v, PrettyVar v) =>
DNF (Polynomial Rational v, [Sign]) -> String
showDNF (DNF (Coeff Int, [Sign]) -> String)
-> DNF (Coeff Int, [Sign]) -> String
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 = [(UPolynomial (Coeff Int), [Sign])]
-> [([(Coeff Int, [Sign])], [Cell (Coeff Int)])]
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 = X -> UPolynomial (Coeff Int)
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)
xUPolynomial (Coeff Int) -> Int -> UPolynomial (Coeff Int)
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) UPolynomial (Coeff Int)
-> UPolynomial (Coeff Int) -> UPolynomial (Coeff Int)
forall a. Num a => a -> a -> a
+ UPolynomial (Coeff Int)
4UPolynomial (Coeff Int)
-> UPolynomial (Coeff Int) -> UPolynomial (Coeff Int)
forall a. Num a => a -> a -> a
*UPolynomial (Coeff Int)
x UPolynomial (Coeff Int)
-> UPolynomial (Coeff Int) -> UPolynomial (Coeff Int)
forall a. Num a => a -> a -> a
- UPolynomial (Coeff Int)
10

test_project_3_print :: IO ()
test_project_3_print =  [([(Coeff Int, [Sign])], [Cell (Coeff Int)])] -> IO ()
forall v.
(Ord v, Show v, PrettyVar v) =>
[([(Polynomial Rational v, [Sign])],
  [Cell (Polynomial Rational v)])]
-> IO ()
dumpProjection ([([(Coeff Int, [Sign])], [Cell (Coeff Int)])] -> IO ())
-> [([(Coeff Int, [Sign])], [Cell (Coeff Int)])] -> IO ()
forall a b. (a -> b) -> a -> b
$ [(UPolynomial (Coeff Int), [Sign])]
-> [([(Coeff Int, [Sign])], [Cell (Coeff Int)])]
forall v.
(Ord v, Show v, PrettyVar v) =>
[(UPolynomial (Polynomial Rational v), [Sign])]
-> [([(Polynomial Rational v, [Sign])],
     [Cell (Polynomial Rational v)])]
project' [(Coeff Int -> Int -> UPolynomial (Coeff Int)
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 = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
0
    b :: Coeff Int
b = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
1
    c :: Coeff Int
c = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
2
    p :: Polynomial Rational Int
    p :: Coeff Int
p = Coeff Int
aCoeff Int -> Int -> Coeff Int
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) Coeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
+ Coeff Int
bCoeff Int -> Int -> Coeff Int
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) Coeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
+ Coeff Int
cCoeff Int -> Int -> Coeff Int
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) Coeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
- Coeff Int
1

test_solve :: Maybe (Model Int)
test_solve = Set Int -> [OrdRel (Coeff Int)] -> Maybe (Model Int)
forall v.
(Ord v, Show v, PrettyVar v) =>
Set v -> [OrdRel (Polynomial Rational v)] -> Maybe (Model v)
solve Set Int
vs [Coeff Int
p Coeff Int -> Coeff Int -> OrdRel (Coeff Int)
forall e r. IsOrdRel e r => e -> e -> r
.<. Coeff Int
0]
  where
    a :: Coeff Int
a = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
0
    b :: Coeff Int
b = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
1
    c :: Coeff Int
c = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
2
    vs :: Set Int
vs = [Int] -> Set Int
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
aCoeff Int -> Int -> Coeff Int
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) Coeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
+ Coeff Int
bCoeff Int -> Int -> Coeff Int
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) Coeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
+ Coeff Int
cCoeff Int -> Int -> Coeff Int
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) Coeff Int -> Coeff Int -> Coeff 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 = M Int [UPolynomial (Coeff Int)]
-> [([UPolynomial (Coeff Int)], Assumption Int)]
forall v a. M v a -> [(a, Assumption v)]
runM (M Int [UPolynomial (Coeff Int)]
 -> [([UPolynomial (Coeff Int)], Assumption Int)])
-> M Int [UPolynomial (Coeff Int)]
-> [([UPolynomial (Coeff Int)], Assumption Int)]
forall a b. (a -> b) -> a -> b
$ [UPolynomial (Coeff Int)] -> M Int [UPolynomial (Coeff Int)]
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 = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
0
    b :: Coeff Int
b = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
1
    c :: Coeff Int
c = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
2
    x :: Coeff Int
x = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
3
    p :: Polynomial Rational Int
    p :: Coeff Int
p = Coeff Int
aCoeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
*Coeff Int
xCoeff Int -> Int -> Coeff Int
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) Coeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
+ Coeff Int
bCoeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
*Coeff Int
x Coeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
+ Coeff Int
c
    p' :: UPolynomial (Coeff Int)
p' = Coeff Int -> Int -> UPolynomial (Coeff Int)
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
  [([UPolynomial (Coeff Int)], Assumption Int)]
-> (([UPolynomial (Coeff Int)], Assumption Int) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [([UPolynomial (Coeff Int)], Assumption Int)]
test_collectPolynomials ((([UPolynomial (Coeff Int)], Assumption Int) -> IO ()) -> IO ())
-> (([UPolynomial (Coeff Int)], Assumption Int) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \([UPolynomial (Coeff Int)]
ps,Assumption Int
g) -> do
    String -> IO ()
putStrLn String
"============"
    (UPolynomial (Coeff Int) -> IO ())
-> [UPolynomial (Coeff Int)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> IO ()
putStrLn (String -> IO ())
-> (UPolynomial (Coeff Int) -> String)
-> UPolynomial (Coeff Int)
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UPolynomial (Coeff Int) -> String
forall a. Pretty a => a -> String
prettyShow) [UPolynomial (Coeff Int)]
ps
    [(Coeff Int, [Sign])] -> ((Coeff Int, [Sign]) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_  (Assumption Int -> [(Coeff Int, [Sign])]
forall v.
Ord v =>
Assumption v -> [(Polynomial Rational v, [Sign])]
assumption2cond Assumption Int
g) (((Coeff Int, [Sign]) -> IO ()) -> IO ())
-> ((Coeff Int, [Sign]) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Coeff Int
p, [Sign]
ss) ->
      String -> String -> String -> IO ()
forall r. PrintfType r => String -> r
printf String
"%s %s\n" (Coeff Int -> String
forall a. Pretty a => a -> String
prettyShow Coeff Int
p) ([Sign] -> String
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 = M Int (SignConf (Coeff Int))
-> [(SignConf (Coeff Int), Assumption Int)]
forall v a. M v a -> [(a, Assumption v)]
runM (M Int (SignConf (Coeff Int))
 -> [(SignConf (Coeff Int), Assumption Int)])
-> M Int (SignConf (Coeff Int))
-> [(SignConf (Coeff Int), Assumption Int)]
forall a b. (a -> b) -> a -> b
$ [UPolynomial (Coeff Int)] -> M Int (SignConf (Coeff Int))
forall v.
(Ord v, Show v, PrettyVar v) =>
[UPolynomial (Polynomial Rational v)]
-> M v (SignConf (Polynomial Rational v))
buildSignConf [Coeff Int -> Int -> UPolynomial (Coeff Int)
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 = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
0
    b :: Coeff Int
b = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
1
    c :: Coeff Int
c = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
2
    x :: Coeff Int
x = Int -> Coeff Int
forall a v. Var a v => v -> a
P.var Int
3
    p :: Polynomial Rational Int
    p :: Coeff Int
p = Coeff Int
aCoeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
*Coeff Int
xCoeff Int -> Int -> Coeff Int
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
2::Int) Coeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
+ Coeff Int
bCoeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
*Coeff Int
x Coeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
+ Coeff Int
c

test_buildSignConf_print :: IO ()
test_buildSignConf_print :: IO ()
test_buildSignConf_print = [(SignConf (Coeff Int), Assumption Int)] -> IO ()
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 = M Int (SignConf (Coeff Int))
-> [(SignConf (Coeff Int), Assumption Int)]
forall v a. M v a -> [(a, Assumption v)]
runM (M Int (SignConf (Coeff Int))
 -> [(SignConf (Coeff Int), Assumption Int)])
-> M Int (SignConf (Coeff Int))
-> [(SignConf (Coeff Int), Assumption Int)]
forall a b. (a -> b) -> a -> b
$ [UPolynomial (Coeff Int)] -> M Int (SignConf (Coeff Int))
forall v.
(Ord v, Show v, PrettyVar v) =>
[UPolynomial (Polynomial Rational v)]
-> M v (SignConf (Polynomial Rational v))
buildSignConf [Coeff Int -> Int -> UPolynomial (Coeff Int)
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 = Int -> Coeff Int
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 -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
+ Coeff Int
1, -Coeff Int
2Coeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
*Coeff Int
x Coeff Int -> Coeff Int -> Coeff Int
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 = [(SignConf (Coeff Int), Assumption Int)] -> IO ()
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 = M Int (SignConf (Coeff Int))
-> [(SignConf (Coeff Int), Assumption Int)]
forall v a. M v a -> [(a, Assumption v)]
runM (M Int (SignConf (Coeff Int))
 -> [(SignConf (Coeff Int), Assumption Int)])
-> M Int (SignConf (Coeff Int))
-> [(SignConf (Coeff Int), Assumption Int)]
forall a b. (a -> b) -> a -> b
$ [UPolynomial (Coeff Int)] -> M Int (SignConf (Coeff Int))
forall v.
(Ord v, Show v, PrettyVar v) =>
[UPolynomial (Polynomial Rational v)]
-> M v (SignConf (Polynomial Rational v))
buildSignConf [Coeff Int -> Int -> UPolynomial (Coeff Int)
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 = Int -> Coeff Int
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
2Coeff Int -> Coeff Int -> Coeff Int
forall a. Num a => a -> a -> a
*Coeff Int
x]

test_buildSignConf_3_print :: IO ()
test_buildSignConf_3_print :: IO ()
test_buildSignConf_3_print = [(SignConf (Coeff Int), Assumption Int)] -> IO ()
forall v.
(Ord v, PrettyVar v, Show v) =>
[(SignConf (Polynomial Rational v), Assumption v)] -> IO ()
dumpSignConf [(SignConf (Coeff Int), Assumption Int)]
test_buildSignConf_3

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