Skip to content

Commit

Permalink
Fix type errors
Browse files Browse the repository at this point in the history
  • Loading branch information
gruhn committed Mar 11, 2023
1 parent 36c6661 commit d45d9be
Show file tree
Hide file tree
Showing 2 changed files with 11 additions and 9 deletions.
2 changes: 1 addition & 1 deletion SMT.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ library
, Theory.NonLinearRealArithmatic.Constraint
, Theory.NonLinearRealArithmatic.BoundedFloating
, Theory.NonLinearRealArithmatic.IntervalConstraintPropagation
, Theory.NonLinearRealArithmatic.Subtropical
-- , Theory.NonLinearRealArithmatic.Subtropical
, Theory.NonLinearRealArithmatic.VirtualSubstitution
, Theory.NonLinearRealArithmatic.CAD
other-modules: Utils
Expand Down
18 changes: 10 additions & 8 deletions src/Theory/NonLinearRealArithmatic/Subtropical.hs
Original file line number Diff line number Diff line change
Expand Up @@ -45,11 +45,11 @@ findDominatingDirection terms = undefined
-- |
-- Returns True iff the polynomial evaluates to something positive under
-- the given variable assignment.
isPositiveSolution :: (Num a, Ord a) => Polynomial a -> IntMap a -> Bool
isPositiveSolution :: (Num a, Ord a, Assignable a) => Polynomial a -> IntMap a -> Bool
isPositiveSolution polynomial solution = eval solution polynomial > 0

-- |
positiveSolution :: (Num a, Ord a) => Polynomial a -> Maybe (IntMap a)
positiveSolution :: (Num a, Ord a, Assignable a) => Polynomial a -> Maybe (IntMap a)
positiveSolution polynomial = do
normal_vector <- findDominatingDirection polynomial

Expand All @@ -73,17 +73,14 @@ positiveSolution polynomial = do
-- |
-- Returns True if the polynomial evaluates to 0 under the given
-- variable assignment.
isSolution :: (Num a, Ord a) => Polynomial a -> IntMap a -> Bool
isSolution :: (Num a, Ord a, Assignable a) => Polynomial a -> IntMap a -> Bool
isSolution polynomial solution = eval solution polynomial == 0

{-|
-}
subtropical :: forall a. (Ord a, Assignable a) => Polynomial a -> Maybe (Assignment a)
subtropical polynomial
| eval one polynomial < 0 = go one polynomial
| eval one polynomial > 0 = go one (negate polynomial)
| otherwise = Just one
where
subtropical polynomial =
let
-- solution that maps all variables to one
one :: Assignment a
one = M.fromList $ zip (varsIn polynomial) (repeat 1)
Expand All @@ -100,4 +97,9 @@ subtropical polynomial
$ M.unionWith (+) neg_sol
$ M.map (* t)
$ M.unionWith (-) pos_sol neg_sol
in
case eval one polynomial `compare` 0 of
LT -> go one polynomial
GT -> go one (negate polynomial)
EQ -> Just one

0 comments on commit d45d9be

Please sign in to comment.