[commit: ghc] decision-procedure: Hook-up an SMT solver. (74144dd)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : decision-procedure
Link       : http://ghc.haskell.org/trac/ghc/changeset/74144ddd477484466c30ec0788d2bc8161e9d723/ghc

>---------------------------------------------------------------

commit 74144ddd477484466c30ec0788d2bc8161e9d723
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Thu Oct 17 02:13:11 2013 -0700

    Hook-up an SMT solver.
    
    NOTE: This uses a very naive method to call the SMT solver:
    
    * GHC will call a program called cvc4, which better be an SMT solver, which is in the path
    * GHC will create (overwrite!) two files "ghc_input.smt" and "ghc_output,smt"
      two files in the current directory.


>---------------------------------------------------------------

74144ddd477484466c30ec0788d2bc8161e9d723
 compiler/typecheck/TcInteract.lhs |   54 ++-
 compiler/typecheck/TcRnTypes.lhs  |    1 +
 compiler/typecheck/TcSMonad.lhs   |    5 +
 compiler/typecheck/TcTypeNats.hs  |  692 ++++++++++++++++++++++++++++++++++++-
 4 files changed, 738 insertions(+), 14 deletions(-)

Diff suppressed because of size. To see it, use:

    git diff-tree --root --patch-with-stat --no-color --find-copies-harder --ignore-space-at-eol --cc 74144ddd477484466c30ec0788d2bc8161e9d723