"Toy" SMT Solver for Educational Purposes
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
Language/Nano/SMT
LICENSE
Makefile
README.md
Setup.hs
nano-smt.cabal

README.md

nano-smt

NanoSMT is a "toy" SMT Solver for educational purposes.

NanoSMT will combine a basic

  1. Propositional Logic (DPLL)

with a Nelson-Oppen combination of theory solvers for

  1. Equality & Uninterpreted Functions (Congruence Closure)
  2. Difference Constraints (Bellman-Ford)

Over time, we may add:

  • Fancy SAT heuristics like non-chronological backtrack, etc.
  • Linear Arithmetic via Simplex.

TODO

  • Write SAT solver

  • Test SAT solver

  • Write EQ solver

    • Write UnionFind
    • Write HashCons [see undefined in NelsonOppen] <--------- HEREHEREHEREHERE
  • Test EQ solver

  • Write NO = SAT + EQ

  • Test NO solver


  • Add UIF/CC to EQ solver
  • Test EUF
  • Test SAT+EUF
  • Write DIFF solver
  • Test DIFF solver
  • Test SAT+EUF+DIFF



{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-}

module Foo where

class Foo a where zz :: a -> String

data Obj = forall a. (Foo a) => Obj a

instance Show a => Foo a where zz = show

xs :: [Obj] xs = [Obj 1, Obj "foo", Obj 'c']

doShow :: [Obj] -> String doShow [] = "" doShow ((Obj x):xs) = zz x ++ doShow xs

bob :: [Obj] -> [String] bob xs = map ((Obj x) -> zz x) xs