README

This README would normally document whatever steps are necessary to get your application up and running.

What is this repository for?

• Quick summary: Metasearch solver that use enumerative search for synthesis. It takes as input a SyGuS file, and produce a solution that satisfies the constraints in the SyGuS.
• Version: beta
• Learn Markdown

How do I get set up?

• Summary of set up:
  - need scala 2.10.3 and Java 8 (u161). I am using Intellij IDEA as the IDE to develop this framework so I would recommend using this IDE.
  - add all the libraries in lib folder to your class path for dependencies.

Main Class for the enumerative solver

Entry class is engines.RepairDriver, which will call the MetaSeachSolver. Note that the RepairDriver can call to four solvers, and MetaSearchSolver is just only one of them.

extsolvers.metasearch.MetaSearchSolver.scala is the enumerative solver

Finally it all boils down to the Searcher in extsolvers.metasearch..searcher.Searcher

Feature unique code

CosineSim = 2
VarLoc = 7
GumTree = 5

Nodup = 3
ModelCount = 6
AngelicVal = 8

Contribution guidelines

• Writing tests
• Code review
• Other guidelines

Who do I talk to?

• Repo owner or admin
• Other community or team contact

INSTALLATION

Need to install Latte form UC Davis for model counting: https://www.math.ucdavis.edu/~latte/
After installation, the binary "count" should be available at /usr/bin/count.
clone repo
run: sbt clean assembly