Skip to content

Commit

Permalink
Update Github links (#329)
Browse files Browse the repository at this point in the history
  • Loading branch information
CyanoKobalamyne committed Jul 5, 2024
1 parent 0fa32fd commit 972e7b2
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 4 deletions.
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
[![CI](https://github.com/upscale-project/pono/actions/workflows/ci.yml/badge.svg)](https://github.com/upscale-project/pono/actions/workflows/ci.yml)

# Pono: A Flexible and Extensible SMT-Based Model Checker
Pono is a performant, adaptable, and extensible SMT-based model checker implemented in C++. It leverages [Smt-Switch](https://github.com/makaimann/smt-switch), a generic C++ API for SMT solving. Pono was developed as the next
Pono is a performant, adaptable, and extensible SMT-based model checker implemented in C++. It leverages [Smt-Switch](https://github.com/stanford-centaur/smt-switch), a generic C++ API for SMT solving. Pono was developed as the next
generation of [CoSA](https://github.com/cristian-mattarei/CoSA) and thus was originally named _cosa2_.

[Pono](http://wehewehe.org/gsdl2.85/cgi-bin/hdict?e=q-11000-00---off-0hdict--00-1----0-10-0---0---0direct-10-ED--4--textpukuielbert%2ctextmamaka-----0-1l--11-en-Zz-1---Zz-1-home-pono--00-3-1-00-0--4----0-0-11-10-0utfZz-8-00&a=d&d=D18537) is the Hawaiian word for proper, correct, or goodness. It is often used colloquially in the moral sense of "goodness" or "rightness," but also refers to "proper procedure" or "correctness." We use the word for multiple meanings. Our goal is that Pono can be a useful tool for people to verify the _correctness_ of systems, which is surely the _right_ thing to do.
Expand Down Expand Up @@ -72,7 +72,7 @@ There are two Transition System interfaces:
### Smt-Switch
[Smt-switch](https://github.com/stanford-centaur/smt-switch) is a C++ solver-agnostic API for SMT solvers. The main thing to remember is that everything is a pointer. Objects might be "typedef-ed" with `using` statements, but they're still `shared_ptr`s. Thus, when using a solver or a term, you need to use `->` accesses.

For more information, see the example usage in the [smt-switch tests](https://github.com/makaimann/smt-switch/tree/master/tests/btor).
For more information, see the example usage in the [smt-switch tests](https://github.com/stanford-centaur/smt-switch/tree/master/tests/btor).
Other useful files to visit include:
* `smt-switch/include/solver.h`: this is the main interface you will be using
* `smt-switch/include/ops.h`: this contains all the ops you might need
Expand Down
4 changes: 2 additions & 2 deletions contrib/setup-smt-switch.sh
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ mkdir -p $DEPS

if [ ! -d "$DEPS/smt-switch" ]; then
cd $DEPS
git clone https://github.com/makaimann/smt-switch
git clone https://github.com/stanford-centaur/smt-switch
cd smt-switch
git checkout -f $SMT_SWITCH_VERSION
./contrib/setup-btor.sh
Expand All @@ -84,6 +84,6 @@ if [ 0 -lt $(ls $DEPS/smt-switch/local/lib/libsmt-switch* 2>/dev/null | wc -w) ]
else
echo "Building smt-switch failed."
echo "You might be missing some dependencies."
echo "Please see the github page for installation instructions: https://github.com/makaimann/smt-switch"
echo "Please see the github page for installation instructions: https://github.com/stanford-centaur/smt-switch"
exit 1
fi

0 comments on commit 972e7b2

Please sign in to comment.