All files in this repository were authored by Junwei Xiong.

This project requires minisat installed to run and compile. Instruction for installing minisat are available here.

A statically compiled file is already available in the repo - compiled on Ubuntu 20.04.3.

Run ./compile.sh to compile CEGARBox

CEGARBox accepts file input. Input is terminated by a newline and valid input formula are defined by the following grammar:

Atom ::= Alphanumeric String
Formula ::=
 Atom || $true || $false || ~Formula ||
 [] Formula || <> Formula || 
 Formula | Formula || Formula & Formula || Formula => Formula || 
 Formula <=> Formula || (Formula) 

./main <input_file>

MQBF, 3CNF and LWB_K benchmarks can be downloaded from here ALC benchmarks can be downloaded from here

Use Experiment/convert.py to convert the benchmarks into a valid format.

Experiments can be run using Experiment/experiment.py and Exeriment/experiment_reflexive.py