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
- Writing tests
- Code review
- Other guidelines
Who do I talk to?
- Repo owner or admin
- Other community or team contact
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.
run: sbt clean assembly