Tct.Method.Matrix.NaturalMI

Description

Synopsis

• data NaturalMIKind
  • = Algebraic
  • | Automaton
  • | Triangular
  • | Unrestricted
• data MatrixOrder = MatrixOrder {
  • ordInter :: MatrixInter Int
  • param :: MatrixKind
  • miKind :: NaturalMIKind
  • uargs :: UsablePositions
  • input :: Problem
  • argFilter :: Maybe ArgumentFiltering
  • usymbols :: [Symbol]
  }
• data NaturalMI = NaturalMI
• type MatrixOptions = Arg (EnumOf NaturalMIKind) :+: (Arg (Maybe Nat) :+: (Arg Nat :+: (Arg Nat :+: (Arg (Maybe Nat) :+: (Arg (Maybe Nat) :+: (Arg Bool :+: Arg Bool))))))
• matrixOptions :: MatrixOptions
• matrixProcessor :: StdProcessor NaturalMI
• matrix :: ProcessorInstance NaturalMI
• kind :: Domains (ArgumentsOf NaturalMI) -> StartTerms -> MatrixKind
• mikind :: Domains (ArgumentsOf NaturalMI) -> NaturalMIKind
• bound :: Domains (ArgumentsOf NaturalMI) -> Size
• cbits :: Domains (ArgumentsOf NaturalMI) -> Maybe Size
• dim :: Domains (ArgumentsOf NaturalMI) -> Int
• isUargsOn :: Domains (ArgumentsOf NaturalMI) -> Bool
• isUrulesOn :: Domains (ArgumentsOf NaturalMI) -> Bool
• data MatrixDP
  • = MWithDP
  • | MNoDP
• kindConstraints :: Eq l => MatrixKind -> MatrixInter (DioPoly DioVar Int) -> DioFormula l DioVar Int
• solveConstraint :: SolverM m => Problem -> UsablePositions -> MatrixKind -> Signature -> Domains (ArgumentsOf NaturalMI) -> DioFormula MiniSatLiteral DioVar Int -> m (OrientationProof MatrixOrder)
• solveConstraint' :: SolverM m => Problem -> UsablePositions -> MatrixKind -> Signature -> Domains (ArgumentsOf NaturalMI) -> MatrixDP -> Bool -> Bool -> MemoFormula arg MiniSatSolver MiniSatLiteral -> DioFormula MiniSatLiteral DioVar Int -> m (OrientationProof MatrixOrder)
• orient :: SolverM m => SelectorExpression -> Problem -> Domains (ArgumentsOf NaturalMI) -> m (ProofOf NaturalMI)
• data Strict = Strict Rule
• data MatArg
  • = Gt Term Term
  • | Gsq Term Term
  • | Eq Term Term
• filteringConstraints :: (Eq l, Ord l, Show a) => AbstrOrdSemiring a (DioFormula l DioVar Int) => Bool -> Problem -> MatrixInter a -> DioFormula l DioVar Int
• uargMonotoneConstraints :: AbstrOrdSemiring a b => UsablePositions -> MatrixInter a -> b
• monotoneConstraints :: AbstrOrdSemiring a b => MatrixInter a -> b
• safeRedpairConstraints :: AbstrOrdSemiring a b => Signature -> UsablePositions -> Bool -> MatrixInter a -> b
• slmiSafeRedpairConstraints :: (MIEntry a, AbstrOrdSemiring a b) => Signature -> UsablePositions -> MatrixInter a -> b
• positiveConstraints :: AbstrOrdSemiring a b => MatrixInter a -> b
• positiveMatrices :: AbstrOrdSemiring a b => MatrixInter a -> b
• positiveVectors :: AbstrOrdSemiring a b => MatrixInter a -> b
• checkDirect :: MatrixInter Int -> Trs -> Bool
• strictRules :: MatrixInter Int -> Trs -> Trs
• applyAss :: (Ord l, Eq l) => MatrixInter (NatFormula l) -> Assign l -> MatrixInter Int
• data DiagOnesVar = DiagOnesVar Int
• diagOnesConstraints :: Eq l => Int -> MatrixInter (DioPoly DioVar Int) -> DioFormula l DioVar Int
• data XdaVar
  • = Gtwo Int Int Int Int
  • | R Int Int
  • | Done Int Int Int
  • | Dtwo Int Int Int
  • | Gthree Int Int Int Int Int Int
  • | T Int Int Int
  • | I Int Int
  • | J Int Int
  • | H Int Int
• dioAtom :: (PropAtom a, Eq l) => a -> DioFormula l DioVar Int
• edaConstraints :: Eq l => MatrixInter (DioPoly DioVar Int) -> DioFormula l DioVar Int
• idaConstraints :: Eq l => Int -> MatrixInter (DioPoly DioVar Int) -> DioFormula l DioVar Int
• rcConstraints :: Eq l => MatrixInter (DioPoly DioVar Int) -> DioFormula l DioVar Int
• gtwoConstraints :: Eq l => MatrixInter (DioPoly DioVar Int) -> DioFormula l DioVar Int
• ggeq :: Eq l => MatrixInter (DioPoly DioVar Int) -> Int -> Int -> DioFormula l DioVar Int
• ggrt :: Eq l => MatrixInter (DioPoly DioVar Int) -> Int -> Int -> DioFormula l DioVar Int
• gtwo :: Eq l => MatrixInter (DioPoly DioVar Int) -> Int -> Int -> Int -> Int -> DioFormula l DioVar Int
• rConstraints :: Eq l => MatrixInter (DioPoly DioVar Int) -> DioFormula l DioVar Int
• dConstraints :: Eq l => MatrixInter (DioPoly DioVar Int) -> DioFormula l DioVar Int
• gThreeConstraints :: Eq l => MatrixInter (DioPoly DioVar Int) -> DioFormula l DioVar Int
• gthree :: Eq l => MatrixInter (DioPoly DioVar Int) -> Int -> Int -> Int -> Int -> Int -> Int -> DioFormula l DioVar Int
• tConstraints :: Eq l => MatrixInter (DioPoly DioVar Int) -> DioFormula l DioVar Int
• iConstraints :: Eq l => MatrixInter (DioPoly DioVar Int) -> DioFormula l DioVar Int
• jConstraints :: Eq l => MatrixInter (DioPoly DioVar Int) -> DioFormula l DioVar Int
• hConstraints :: Eq l => Int -> MatrixInter (DioPoly DioVar Int) -> DioFormula l DioVar Int
• class MIEntry a

Documentation