From 12c44f0a19a3cfc729370550b3f18d19f3f8633f Mon Sep 17 00:00:00 2001 From: Cesare Tinelli Date: Fri, 30 Aug 2024 14:29:21 -0500 Subject: [PATCH 01/12] Several edits to improve readability and conform to Markdown guidelines --- .DS_Store | Bin 0 -> 8196 bytes user_manual.md | 1021 ++++++++++++++++++++++++++---------------------- 2 files changed, 562 insertions(+), 459 deletions(-) create mode 100644 .DS_Store diff --git a/.DS_Store b/.DS_Store new file mode 100644 index 0000000000000000000000000000000000000000..e9378fd5e1f00250b64b7597856e410349f09352 GIT binary patch literal 8196 zcmeHMJ#Q016r6QzY$=T^6j5!1=#WB2U`ohXU0b5>&4Ttx#y)JWt9(9lrv z15!|>;zQy`P|yGc%-dbtyLUdQAV|EGcIUG1y_?aTb?fHsQ>)orMp>&^dzEo15mFV#=ofd`| z<31i>KhQ zef~Wy=`znB)n~@~?%sYs|NPY4H}>uK*@@o9MD(sv-wB3^Z>`zZG7{_QJ^V1&6Y66A zYBb?%Tj6Wbja8mBw%(-CnD_D7r#Wv_A9JtHNccO?gkJ`a=Wak7Fbi0C^ar?}|Kf%Y zb>Q+GSo72y(*N(&|Neh@0+m@EPzV0F1E$&E?e|C%dg}_I^xBs59;Xb+D?GXqF0LIX hx^|qn_=h2{EmNf?3s`vM4u^gba5m_o4*XRIegZG(532wG literal 0 HcmV?d00001 diff --git a/user_manual.md b/user_manual.md index f2eb8798..44d745c2 100644 --- a/user_manual.md +++ b/user_manual.md @@ -1,111 +1,141 @@ -# Introduction +# The Ethos user manual This is the user manual for the Ethos, an efficient and extensible tool for checking proofs of Satisfiability Modulo Theories (SMT) solvers. -## Building ethos +## Building the Ethos executable -The source code for ethos is available here: https://github.com/cvc5/ethos. +The source code for Ethos is available at . To build ethos, run: -``` + +```shell mkdir build cd build cmake .. ``` + The `ethos` binary will be available in `build/src/`. ### Debug build By default, the above will be a production build of `ethos`. To build a debug version of `ethos`, that is significantly slower but has assertions and trace messages enabled, run: -``` + +```shell mkdir build -DCMAKE_BUILD_TYPE=Debug cd build cmake .. ``` + The `ethos` binary will be available in `build/src/`. -## Command line interface of ethos +## Command line interface -`ethos` can be run from the command line via: -``` +Ethos can be run from the command line via: + +```shell ethos