Tct.Method.Matrix.ArcticMI

Description

Synopsis

• data ArcticOrder = ArcticOrder {
  • ordInter :: MatrixInter ArcInt
  • uargs :: UsablePositions
  }
• data ArcticMI = ArcticMI
• arcticProcessor :: StdProcessor ArcticMI
• arctic :: ProcessorInstance ArcticMI
• bound :: TheProcessor ArcticMI -> Size
• cbits :: TheProcessor ArcticMI -> Maybe Size
• dim :: TheProcessor ArcticMI -> Int
• isUargsOn :: TheProcessor ArcticMI -> Bool
• data MatrixDP
  • = MWithDP
  • | MNoDP
• data MatrixRelativity
  • = MDirect
  • | MRelative [Rule]
• orientDirect :: SolverM m => Strategy -> StartTerms -> Trs -> Signature -> TheProcessor ArcticMI -> m (ProofOf ArcticMI)
• orientRelative :: SolverM m => Strategy -> StartTerms -> Trs -> Trs -> Signature -> TheProcessor ArcticMI -> m (ProofOf ArcticMI)
• orientDp :: SolverM m => Strategy -> StartTerms -> Trs -> Trs -> Signature -> TheProcessor ArcticMI -> m (ProofOf ArcticMI)
• orientPartial :: SolverM m => [Rule] -> Strategy -> StartTerms -> Trs -> Signature -> TheProcessor ArcticMI -> m (ProofOf ArcticMI)
• orientPartialRelative :: SolverM m => [Rule] -> Strategy -> StartTerms -> Trs -> Trs -> Signature -> TheProcessor ArcticMI -> m (ProofOf ArcticMI)
• orientPartialDp :: SolverM m => [Rule] -> Strategy -> StartTerms -> Trs -> Trs -> Signature -> TheProcessor ArcticMI -> m (ProofOf ArcticMI)
• orientMatrix :: SolverM m => (UsablePositions -> StartTerms -> Trs -> Trs -> Signature -> TheProcessor ArcticMI -> DioFormula MiniSatLiteral DioVar ArcInt) -> UsablePositions -> StartTerms -> Trs -> Trs -> Signature -> TheProcessor ArcticMI -> m (ProofOf ArcticMI)
• partialConstraints :: Eq l => [Rule] -> UsablePositions -> StartTerms -> Trs -> Trs -> Signature -> TheProcessor ArcticMI -> DioFormula l DioVar ArcInt
• relativeConstraints :: Eq l => UsablePositions -> StartTerms -> Trs -> Trs -> Signature -> TheProcessor ArcticMI -> DioFormula l DioVar ArcInt
• dpConstraints :: Eq l => UsablePositions -> StartTerms -> Trs -> Trs -> Signature -> TheProcessor ArcticMI -> DioFormula l DioVar ArcInt
• matrixConstraints :: Eq l => MatrixRelativity -> MatrixDP -> UsablePositions -> StartTerms -> Trs -> Trs -> Signature -> TheProcessor ArcticMI -> DioFormula l DioVar ArcInt
• uargMonotoneConstraints :: AbstrOrdSemiring a b => Signature -> UsablePositions -> MatrixInter a -> b
• monotoneConstraints :: AbstrOrdSemiring a b => Signature -> MatrixInter a -> b
• safeRedpairConstraints :: AbstrOrdSemiring a b => Signature -> MatrixInter a -> b
• weakMonotoneConstraints :: AbstrOrdSemiring a b => MatrixInter a -> b
• unaryConstraints :: AbstrOrdSemiring a b => MatrixInter a -> b
• nullaryConstraints :: AbstrOrdSemiring a b => MatrixInter a -> b
• checkDirect :: MatrixInter ArcInt -> Trs -> Signature -> Bool
• strictRules :: MatrixInter ArcInt -> Trs -> Trs
• class AIEntry a

Documentation