Spatial and Action Based Resolver
Fetching latest commit…
Cannot retrieve the latest commit at this time
SABR (Spatial and Action Based Resolver) ------------ GENERAL ------------ SABR (Spatial and Action Based Resolver) is a constraint programming language designed with an emphasis on spatial and temporal logic. Programs compile to CNF (Conjunctive Normal Form), which is then solved by a CNF solver, whose results are processed into human readable form. The goal of the language is to make representing puzzles and operations research problems not just possible, but also intuitive and the solving of these problems efficient. From a theoretical perspective, the language can also be used to prove a problem is NP-Easy and can be used to verify properties about automata and systems that can be modeled as automata such as circuits and programs. website: sabrlang.org ------------ INSTALL ------------ SABR is installed using setup.py python setup.py depend This command will create a dependency diagram using a dot file indicating which files primarilly use which other files and how the program progresses and place it in doc/depend. python setup.py minisat This will install the default cnf solver used SABR. The default cnf solver is minisat. More information can be found at https://github.com/niklasso/minisat. python setup.py parser This will use flex and bison to create the c files from the lex and yacc files in the parser directory. python setup.py build This will build SABR from core utils and parser. python setup.py clean This will clear all unnesary files in the SABR directory. python setup.py cleanall This will also clear minisat installation. ------------ RUN ------------ To run SABR, you must provide the number of stages as the first argument. An optional type of compilation flag. Then input the SABR program to run. The output file will appear as result.out. For more information on the language view doc/LANGUAGE. Example: ./sabr 20 -all < test/Simple/simple.tb Flags none No flag will produce the dimin.in for the cnf and execute and process it to human readable form. -initial This will only produce the dimin.in. After this, a more advanced sat solver could be used. -debug This will be like initial, but will output dimin.in debug information. -result This will assume dimout.out will come from another cnf solver. -all This will run like with no flag, but also output debug results. ------------ TESTING ------------ Testing is done with test.py -full can be added where indicated to fill in debug results python test.py debug Tests compiler post-process syntax checking. python test.py simple python test.py simple-full Does simple tests for compiler functionality. python test.py adv python test.py adv-full Does advanced tests for compiler functionality. python test.py hard python test.py hard-full Does difficult tests for compiler functionality. python test.py all python test.py all-full Does all tests for compiler functionality. python test.py clear-debug Clears the debug results for all tests (reduces project size).