Executor::getConstraintLog(), Interpreter::LogType and -write-cvcs needs a clean up #382
Labels
Comments
|
This is very straight forward apart from handling the file extension? @ccadar @MartinNowack do you have any preferences on how to handle this? |
|
Oh another idea. Change the interface of to if I don't like mixing |
|
I prefer the variant where we generate proper extensions. |
delcypher
pushed a commit
to delcypher/klee
that referenced
this issue
Mar 23, 2017
There are numerous changes here which removes the assumption that STP is the core solver. * `-write-cvcs` has been renamed to `-write-core-solver-queries` * `LogType::STP` has been renamed to `LogType::CORE_SOLVER_LANG` * `Interpreter::getConstraintLog()` and `Executor::getConstraintLog()` now have a `fileExtension` parameter which returns the file extension for constraint language requested. * The `Solver::getConstraintLog()` and `SolverImpl::getConstraintLog()` methods (and all their decendents) now have a `fileExtension` parameter which will be set (if requested by the client) to file the extension for the core solver's constraint language.
delcypher
pushed a commit
to delcypher/klee
that referenced
this issue
Mar 23, 2017
There are numerous changes here which removes the assumption that STP is the core solver. * `-write-cvcs` has been renamed to `-write-core-solver-queries` * `LogType::STP` has been renamed to `LogType::CORE_SOLVER_LANG` * `Interpreter::getConstraintLog()` and `Executor::getConstraintLog()` now have a `fileExtension` parameter which returns the file extension for constraint language requested. * The `Solver::getConstraintLog()` and `SolverImpl::getConstraintLog()` methods (and all their descendants) now have a `fileExtension` parameter which will be set (if requested by the client) to the file extension for the core solver's constraint language.
Closed
delcypher
pushed a commit
to delcypher/klee
that referenced
this issue
Mar 23, 2017
There are numerous changes here which removes the assumption that STP is the core solver. * `-write-cvcs` has been renamed to `-write-core-solver-queries` * `LogType::STP` has been renamed to `LogType::CORE_SOLVER_LANG` * `Interpreter::getConstraintLog()` and `Executor::getConstraintLog()` now have a `fileExtension` parameter which returns the file extension for constraint language requested. * The `Solver::getConstraintLog()` and `SolverImpl::getConstraintLog()` methods (and all their descendants) now have a `fileExtension` parameter which will be set (if requested by the client) to the file extension for the core solver's constraint language.
delcypher
pushed a commit
to delcypher/klee
that referenced
this issue
Mar 23, 2017
There are numerous changes here which removes the assumption that STP is the core solver. * `-write-cvcs` has been renamed to `-write-core-solver-queries` * `LogType::STP` has been renamed to `LogType::CORE_SOLVER_LANG` * `Interpreter::getConstraintLog()` and `Executor::getConstraintLog()` now have a `fileExtension` parameter which returns the file extension for constraint language requested. * The `Solver::getConstraintLog()` and `SolverImpl::getConstraintLog()` methods (and all their descendants) now have a `fileExtension` parameter which will be set (if requested by the client) to the file extension for the core solver's constraint language.
delcypher
pushed a commit
to delcypher/klee
that referenced
this issue
Mar 24, 2017
There are numerous changes here which removes the assumption that STP is the core solver. * `-write-cvcs` has been renamed to `-write-core-solver-queries` * `LogType::STP` has been renamed to `LogType::CORE_SOLVER_LANG` * `Interpreter::getConstraintLog()` and `Executor::getConstraintLog()` now have a `fileExtension` parameter which returns the file extension for constraint language requested. * The `Solver::getConstraintLog()` and `SolverImpl::getConstraintLog()` methods (and all their descendants) now have a `fileExtension` parameter which will be set (if requested by the client) to the file extension for the core solver's constraint language.
|
This discussion was moved to #512 , closing. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
STP is no longer the only core solver in KLEE so we to clean up a few things
Interpreter::LogType::STPwithInterpreter::LogType::SOLVER_NATIVE_FORMAT-write-cvcsoption should be changed to-write-native-solver-format(similarly for the corresponding variable name)..cvcextension. We either need to add a new method to the solver classes so that we can get the native format's file extension or we should be lazy and just emit.native_solver_formatand let the user figure out what the extension should be.The text was updated successfully, but these errors were encountered: