msakai / toysolver / 517

Committed 24 Nov 2024 02:02PM UTC coverage: 69.746% (-0.7%) from 70.447%

Build # 517

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #123 from msakai/feature/reduce-transformers-2

Change SimplifyMaxSAT2Info and SAT3ToMaxSAT2Info to be synonyms of TseitinInfo

Run Details

5 of 5 new or added lines in 1 file covered. (100.0%)

127 existing lines in 13 files now uncovered.

9816 of 14074 relevant lines covered (69.75%)

0.7 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

37.84

/src/ToySolver/Arith/Simplex/Simple.hs

{-# OPTIONS_GHC -Wall #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Arith.Simplex.Simple
-- Copyright   :  (c) Masahiro Sakai 2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  portable
--
-----------------------------------------------------------------------------
module ToySolver.Arith.Simplex.Simple
  ( Model
  , OptDir (..)
  , OptResult (..)
  , check
  , optimize
  ) where

import Control.Monad
import Control.Monad.ST
import Data.Default.Class
import qualified Data.IntMap.Strict as IntMap
import qualified Data.IntSet as IntSet
import qualified ToySolver.Data.LA as LA
import ToySolver.Data.IntVar hiding (Model)
import qualified ToySolver.Arith.Simplex as Simplex
import ToySolver.Arith.Simplex hiding (check, optimize)

check :: VarSet -> [LA.Atom Rational] -> Maybe Model
check vs as = runST $ do
  solver <- Simplex.newSolver
  s <- liftM IntMap.fromAscList $ forM (IntSet.toAscList vs) $ \v -> do
    v2 <- Simplex.newVar solver
    return (v, v2)
  let s' = fmap LA.var s
      mtrans m = fmap (m IntMap.!) s
  forM_ as $ \a -> do
    Simplex.assertAtomEx solver (fmap (LA.applySubst s') a)
  ret <- Simplex.check solver
  if ret then do
    m <- Simplex.getModel solver
    return $ Just $ mtrans m
  else
    return Nothing

optimize :: VarSet -> OptDir -> LA.Expr Rational -> [LA.Atom Rational] -> (OptResult, Maybe Model)
optimize vs dir obj as = runST $ do
  solver <- Simplex.newSolver
  s <- liftM IntMap.fromAscList $ forM (IntSet.toAscList vs) $ \v -> do
    v2 <- Simplex.newVar solver
    return (v, v2)
  let s' = fmap LA.var s
      mtrans m = fmap (m IntMap.!) s
  forM_ as $ \a -> do
    assertAtom solver (fmap (LA.applySubst s') a)
  Simplex.setOptDir solver dir
  Simplex.setObj solver obj
  ret <- Simplex.optimize solver def
  case ret of
    Optimum -> do
      m <- Simplex.getModel solver
      return $ (ret, Just (mtrans m))
    Unsat -> do
      return $ (ret, Nothing)
    Unbounded -> do
      m <- Simplex.getModel solver
      return $ (ret, Just (mtrans m))
    ObjLimit -> do
      error "should not happen"

1	{-# OPTIONS_GHC -Wall #-}
2	-----------------------------------------------------------------------------
3	-- \|
4	-- Module : ToySolver.Arith.Simplex.Simple
5	-- Copyright : (c) Masahiro Sakai 2016
6	-- License : BSD-style
7	--
8	-- Maintainer : masahiro.sakai@gmail.com
9	-- Stability : provisional
10	-- Portability : portable
11	--
12	-----------------------------------------------------------------------------
13	module ToySolver.Arith.Simplex.Simple
14	( Model
15	, OptDir (..)
16	, OptResult (..)
17	, check
18	, optimize
19	) where
20
21	import Control.Monad
22	import Control.Monad.ST
23	import Data.Default.Class
24	import qualified Data.IntMap.Strict as IntMap
25	import qualified Data.IntSet as IntSet
26	import qualified ToySolver.Data.LA as LA
27	import ToySolver.Data.IntVar hiding (Model)
28	import qualified ToySolver.Arith.Simplex as Simplex
29	import ToySolver.Arith.Simplex hiding (check, optimize)
30
31	check :: VarSet -> [LA.Atom Rational] -> Maybe Model
32	check vs as = runST $ do	1✔
33	solver <- Simplex.newSolver	1✔
34	s <- liftM IntMap.fromAscList $ forM (IntSet.toAscList vs) $ \v -> do	1✔
35	v2 <- Simplex.newVar solver	1✔
36	return (v, v2)	1✔
37	let s' = fmap LA.var s	1✔
38	mtrans m = fmap (m IntMap.!) s	1✔
39	forM_ as $ \a -> do	1✔
40	Simplex.assertAtomEx solver (fmap (LA.applySubst s') a)	1✔
41	ret <- Simplex.check solver	1✔
42	if ret then do	1✔
43	m <- Simplex.getModel solver	1✔
44	return $ Just $ mtrans m	1✔
45	else
46	return Nothing	1✔
47
48	optimize :: VarSet -> OptDir -> LA.Expr Rational -> [LA.Atom Rational] -> (OptResult, Maybe Model)
49	optimize vs dir obj as = runST $ do	×
50	solver <- Simplex.newSolver	×
51	s <- liftM IntMap.fromAscList $ forM (IntSet.toAscList vs) $ \v -> do	×
52	v2 <- Simplex.newVar solver	×
53	return (v, v2)	×
54	let s' = fmap LA.var s	×
55	mtrans m = fmap (m IntMap.!) s	×
56	forM_ as $ \a -> do	×
57	assertAtom solver (fmap (LA.applySubst s') a)	×
58	Simplex.setOptDir solver dir	×
59	Simplex.setObj solver obj	×
60	ret <- Simplex.optimize solver def	×
61	case ret of	×
62	Optimum -> do	×
63	m <- Simplex.getModel solver	×
64	return $ (ret, Just (mtrans m))	×
65	Unsat -> do	×
66	return $ (ret, Nothing)	×
67	Unbounded -> do	×
68	m <- Simplex.getModel solver	×
69	return $ (ret, Just (mtrans m))	×
70	ObjLimit -> do	×
71	error "should not happen"	×

msakai / toysolver / 517

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous