Provides management of goal variables that encode properties. More...
#include <goto_symex_property_decider.h>
Collaboration diagram for goto_symex_property_decidert:Classes | |
| struct | goalt |
Public Member Functions | |
| goto_symex_property_decidert (const optionst &options, ui_message_handlert &ui_message_handler, symex_target_equationt &equation, const namespacet &ns) | |
| void | update_properties_goals_from_symex_target_equation (propertiest &properties) |
Get the conditions for the properties from the equation and collect all 'instances' of the properties in the goal_map More... | |
| void | convert_goals () |
| Convert the instances of a property into a goal variable. More... | |
| void | add_constraint_from_goals (std::function< bool(const irep_idt &property_id)> select_property) |
| Add disjunction of negated selected properties to the equation. More... | |
| decision_proceduret::resultt | solve () |
| Calls solve() on the solver instance. More... | |
| decision_proceduret & | get_decision_procedure () const |
| Returns the solver instance. More... | |
| stack_decision_proceduret & | get_stack_decision_procedure () const |
| Returns the solver instance. More... | |
| symex_target_equationt & | get_equation () const |
| Return the equation associated with this instance. More... | |
| void | update_properties_status_from_goals (propertiest &properties, std::unordered_set< irep_idt > &updated_properties, decision_proceduret::resultt dec_result, bool set_pass=true) const |
| Update the property status from the truth value of the goal variable. More... | |
Protected Attributes | |
| const optionst & | options |
| ui_message_handlert & | ui_message_handler |
| symex_target_equationt & | equation |
| std::unique_ptr< solver_factoryt::solvert > | solver |
| std::map< irep_idt, goalt > | goal_map |
| Maintains the relation between a property ID and the corresponding goal variable that encodes the negation of the conjunction of the instances of the property. More... | |
Detailed Description
Provides management of goal variables that encode properties.
Definition at line 23 of file goto_symex_property_decider.h.
Constructor & Destructor Documentation
◆ goto_symex_property_decidert()
| goto_symex_property_decidert::goto_symex_property_decidert | ( | const optionst & | options, |
| ui_message_handlert & | ui_message_handler, | ||
| symex_target_equationt & | equation, | ||
| const namespacet & | ns | ||
| ) |
Definition at line 19 of file goto_symex_property_decider.cpp.
Member Function Documentation
◆ add_constraint_from_goals()
| void goto_symex_property_decidert::add_constraint_from_goals | ( | std::function< bool(const irep_idt &property_id)> | select_property | ) |
Add disjunction of negated selected properties to the equation.
Definition at line 83 of file goto_symex_property_decider.cpp.
◆ convert_goals()
| void goto_symex_property_decidert::convert_goals | ( | ) |
Convert the instances of a property into a goal variable.
Definition at line 72 of file goto_symex_property_decider.cpp.
◆ get_decision_procedure()
| decision_proceduret & goto_symex_property_decidert::get_decision_procedure | ( | ) | const |
Returns the solver instance.
Definition at line 118 of file goto_symex_property_decider.cpp.
◆ get_equation()
| symex_target_equationt & goto_symex_property_decidert::get_equation | ( | ) | const |
Return the equation associated with this instance.
Definition at line 129 of file goto_symex_property_decider.cpp.
◆ get_stack_decision_procedure()
| stack_decision_proceduret & goto_symex_property_decidert::get_stack_decision_procedure | ( | ) | const |
Returns the solver instance.
Definition at line 124 of file goto_symex_property_decider.cpp.
◆ solve()
| decision_proceduret::resultt goto_symex_property_decidert::solve | ( | ) |
Calls solve() on the solver instance.
Definition at line 112 of file goto_symex_property_decider.cpp.
◆ update_properties_goals_from_symex_target_equation()
| void goto_symex_property_decidert::update_properties_goals_from_symex_target_equation | ( | propertiest & | properties | ) |
Get the conditions for the properties from the equation and collect all 'instances' of the properties in the goal_map
Definition at line 43 of file goto_symex_property_decider.cpp.
◆ update_properties_status_from_goals()
| void goto_symex_property_decidert::update_properties_status_from_goals | ( | propertiest & | properties, |
| std::unordered_set< irep_idt > & | updated_properties, | ||
| decision_proceduret::resultt | dec_result, | ||
| bool | set_pass = true |
||
| ) | const |
Update the property status from the truth value of the goal variable.
- Parameters
-
[in,out] properties The status is updated in this data structure [in,out] updated_properties The set of property IDs of updated properties dec_result The result returned by the solver set_pass If true then update UNKNOWN properties to PASS if the solver returns UNSATISFIABLE
Definition at line 134 of file goto_symex_property_decider.cpp.
Member Data Documentation
◆ equation
|
protected |
Definition at line 71 of file goto_symex_property_decider.h.
◆ goal_map
Maintains the relation between a property ID and the corresponding goal variable that encodes the negation of the conjunction of the instances of the property.
Definition at line 88 of file goto_symex_property_decider.h.
◆ options
|
protected |
Definition at line 69 of file goto_symex_property_decider.h.
◆ solver
|
protected |
Definition at line 72 of file goto_symex_property_decider.h.
◆ ui_message_handler
|
protected |
Definition at line 70 of file goto_symex_property_decider.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/goto-checker/goto_symex_property_decider.h
- /home/runner/work/cbmc/cbmc/src/goto-checker/goto_symex_property_decider.cpp
