LARA

Decision Procedures for Satisfiability in the Equality Theory of Lists

 Bogdan Stroe 
 Jonas Lindmark 

Links on SMT Solvers

Links on deciding quantifier-free algebraic data types:

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:

Scala source code :