A step-by-step tutorial demonstrating how to integrate the Satisfier API (client.cpp
, satisfier.hpp
, satisfier.dll
, libsatisfier.a
) into a Code::Blocks C++ project, using Dynamic Link Library (DLL). For resources on origin of the word "satisfier", read Harvey M. Friedman Adventures in Logic for Undergraduates
, and The Dynmamics of Decision-Making Styles
(Decision Dynamics Europe).
-
Operating System: Windows with Code::Blocks + MinGW
-
Files required in your project folder:
client.cpp
—find it inclients
satisfier.hpp
satisfier.dll
—find it inbin/Debug
libsatisfier.a
—find it inbin/Debug
If you are downloading Code::Blocks for the first time, then you don't need this tutorial. Just download and extract
codeblocks-satisfier-nosetup.zip
via https://huggingface.co/caletechnology/codeblocks-satisfier-nosetup/tree/main, then openclient.cpp
-
Create Console Project
File → New → Project → Console Application (C++)
-
Add files
Copyclient.cpp
,satisfier.hpp
into the project directory. -
Linker Settings
-
Copy .dll
- Comment erroneous code in main function of
client.cpp
- Build your project to compile
.exe
executable - Copy
satisfier.dll
next to the compiled executable - Uncomment code in the main function of
client.cpp
- Comment erroneous code in main function of
-
Build & Run
- Press F9—the project dynamically loads the DLL at runtime.
Regarding context rule, read Yannis Kassios Formal Proof
. Also read A. N. Prior The Runabout Inference-Ticket
, to prove that A. And (B)
is not equivalent to A. Tonk (B)
. Nuel D. Belnap Tonk, Plonk and Plink
says that both A,B
are deducible from A. And (B)
in synthetic mode of logic relying on context.
When using Satisfier API to do formal proof, if you have consecutive disjunctions e.g., A. Or (B). Or (C)
and you supposed only literal C
is true, then type C. Or (A). Or (B)
instead of A. Or (B). Or (C)
to minimize number of recommendations from the API.