This is a fork of Uclid5 that accommodates first-class modules and thus significantly changes the internal representation. This work is possible thanks to these contributors, and all code is covered by this license. The goal is ultimately to combine this fork with the main repository. If you use either version of Uclid5 in your work, please cite the original Uclid5 MEMOCODE'18 paper.
@inproceedings{seshia18uclid5,
author = {Sanjit A. Seshia and Pramod Subramanyan},
title = {{UCLID5:} Integrating Modeling, Verification, Synthesis and Learning},
booktitle = {16th {ACM/IEEE} International Conference on Formal Methods and Models
for System Design ({MEMOCODE})},
pages = {1--10},
publisher = {{IEEE}},
year = {2018},
doi = {10.1109/MEMCOD.2018.8556946},
location = {Beijing, China}
}
Beyond first-class modules, this fork also carefully realizes the synthesis encoding described in this SYNT '20 workshop paper.
- Install SBT
- Install at least one of
Just add the bin folder to your path: uclidfc will automatically compile the
first time you run it. Note, uclidfc will not automatically recompile if you
make changes to its source code. To recompile, run sbt assembly.
uclidfc [options] <file> ...
Basic Usage
-m, --main <module> Name of the main module.
-s, --solver <solver> Solver to use (alt_ergo or cvc4 or vampire or z3). Solver must be in your path.
-t, --timeout <timeout> Timeout (in whole seconds) to give the solver per query.
-w, --write <file> Write query to <file>.
--pretty-print Try to make output queries human readable.
--debug-print Add internal term graph information as SMT comments.
--skip-solver Don't run the solver.
--single-thread Don't run solvers in parallel.
<file> ... List of input files.
Analysis
--print-features Print query features.
Algebraic Datatype Rewrites
--blast-enum-quantifiers Rewrite quantifiers over enums to finite disjunctions/conjunctions.
In SMT mode (when you call uclidfc on .smt2 files) uclidfc will iterate over the
files. If you give uclidfc multiple solver arguments, uclidfc will automatically
select the solver to use. So, the following command will, for each query in
models/tests/smt2/, print the query features, and use either z3 or cvc4 to
solve the query.
uclidfc models/tests/smt2/* --print-features -s cvc4 -s z3
# depends on fswatch (`brew install fswatch`)
uclidfc-live <uclid files to edit> <query file to watch>
sbt jacoco
open target/scala-3.0.0-RC1/jacoco/report/html/index.html
sbt "run [options] <file> ..."
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent