content: -- |
  -- Copyright   : (c) 2010-2012 Benedikt Schmidt & Simon Meier
  -- License     : GPL v3 (see LICENSE)
  --
  -- Portability : GHC only
  --
  -- The public interface of the constraint solver, which implements all
  -- constraint reduction rules and together with a rule application heuristic.
  module Theory.Constraint.Solver (
  
    -- * Constraint systems
      module Theory.Constraint.System
  
  --   , ProofContext(..)
  --   , DiffProofContext(..)
  --   , pcSignature
  --   , pcRules
  --   , pcSources
  --   , pcUseInduction
  --   , pcSourceKind
  --   , pcTraceQuantifier
  --   , pcInjectiveFactInsts
  -- 
  --   , InductionHint(..)
  -- 
  --   , ClassifiedRules(..)
  --   , joinAllRules
  --   , crProtocol
  --   , crConstruct
  --   , crDestruct
  
    -- * Constraint reduction rules
  
    -- ** Contradictions
    -- | All rules that reduce a constraint system to the empty set of
    -- constraint systems. The 'Contradiction' datatype stores the information
    -- about the contradiction for later display to the user.
    , Contradiction
    , contradictions
  
  --   , Source
  --   , cdGoal
  --   , cdCases
  
    , precomputeSources
    , refineWithSourceAsms
    , unsolvedChainConstraints
  
    -- * Proof methods
    -- | Proof methods are the external to the constraint solver. They allow its
    -- small step execution. This module also provides the heuristics for
    -- selecting the best proof method to apply to a constraint system.
    , module Theory.Constraint.Solver.ProofMethod
    -- , module Theory.Constraint.Solver.Heuristics
  
    -- ** Convenience export
    , module Logic.Connectives
  
    ) where
  
  import           Logic.Connectives
  import           Theory.Constraint.Solver.Sources
  import           Theory.Constraint.Solver.Contradictions
  import           Theory.Constraint.Solver.ProofMethod
  --import           Theory.Constraint.Solver.Heuristics
  import           Theory.Constraint.System
  
  
  