#include <prop_conv.h>
+ Inheritance diagram for prop_convt:
+ Collaboration diagram for prop_convt:
Convert a Boolean expression and return the corresponding literal.
Return value of literal l from satisfying assignment.
Pushes a new context on the stack that consists of the given (possibly empty vector of) assumptions.
Push a new context on the stack This context becomes a child context nested in the current context.
Pop whatever is on top of the stack.
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
For a Boolean expression expr, add the constraint 'expr'.
For a Boolean expression expr, add the constraint 'not expr'.
Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to
get or
set_to.
Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat.
Run the decision procedure to solve the problem under the given assumption.
Return expr with variables replaced by values from satisfying assignment if available.
Print satisfying assignment to out.
Return a textual description of the decision procedure.
Return the number of incremental solver calls.
Additional Inherited Members
Result of running the decision procedure.
More...
Implementation of the decision procedure.
Detailed Description
Constructor & Destructor Documentation
◆ ~prop_convt()
virtual prop_convt::~prop_convt
(
)
inlinevirtual
Member Function Documentation
◆ convert()
Convert a Boolean expression and return the corresponding literal.
Implemented in prop_conv_solvert.
◆ l_get()
Return value of literal l from satisfying assignment.
Return tvt::UNKNOWN if not available
Implemented in prop_conv_solvert.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/solvers/prop/prop_conv.h
