Bogdan Stroe 
 Jonas Lindmark 

Links on SMT Solvers

Links on deciding quantifier-free algebraic data types:

• An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types
• Greg Nelson paper
• On the Theory of Structural Subtyping (see Section 3.4 on term algebras)

Suggested formulation:

• INPUT:
  • list of constructors and selectors and number of their arguments (example: cons(x,y), head(z), tail(z))
  • list of literals (equalities and disequalities between terms)
• OUTPUT:
  • SAT, and one solution (mapping of variables to ground terms) - if there exists a solution
  • UNSAT - if there are no solutions where variables denote ground terms

Final project report:

• PDF file: File

Scala source code :

• Sat.scala : 1st decision procedure
• NelsonSat.scala : 2nd decision procedure
• Theory.Scala : the grammar