Added c_interface function vc_parseSMTLIB2Expr to parse smtlib2 string and...
Added c_interface function vc_parseSMTLIB2Expr to parse smtlib2 string and load the asserts and querie into the solver. Added c_interface function vc_getQueryStateAsCNF to return the solver query state as a Cnf_Dat_t struct (internal struct of STP) moved some functionality that was done by the CNF_PrintBack function into vc_printQueryStateAsCNFToBuffer so its consistent with vc_getQueryStateAsCNF
Showing
- .vscode/settings.json 5 additions, 1 deletion.vscode/settings.json
- CMakeLists.txt 1 addition, 0 deletionsCMakeLists.txt
- include/stp/Parser/parser.h 2 additions, 1 deletioninclude/stp/Parser/parser.h
- include/stp/Printer/printers.h 4 additions, 3 deletionsinclude/stp/Printer/printers.h
- include/stp/STPManager/STPManager.h 3 additions, 0 deletionsinclude/stp/STPManager/STPManager.h
- include/stp/c_interface.h 27 additions, 15 deletionsinclude/stp/c_interface.h
- lib/Interface/c_interface.cpp 104 additions, 14 deletionslib/Interface/c_interface.cpp
- lib/Parser/smt2.lex 1 addition, 0 deletionslib/Parser/smt2.lex
- lib/Printer/CNFPrinter.cpp 3 additions, 20 deletionslib/Printer/CNFPrinter.cpp
- lib/STPManager/STPManager.cpp 58 additions, 0 deletionslib/STPManager/STPManager.cpp
- lib/extlib-abc/aig/cnf/cnfMan.c 2 additions, 2 deletionslib/extlib-abc/aig/cnf/cnfMan.c
- lib/extlib-abc/cnf.h 1 addition, 1 deletionlib/extlib-abc/cnf.h
- lib/extlib-abc/cnf_short.h 1 addition, 1 deletionlib/extlib-abc/cnf_short.h
- output_0.cnf 15 additions, 66 deletionsoutput_0.cnf
Loading
Please register or sign in to comment