cprover
|
#include <prop_conv.h>
Public Member Functions | |
prop_convt (const namespacet &_ns) | |
virtual | ~prop_convt () |
virtual literalt | convert (const exprt &expr)=0 |
literalt | operator() (const exprt &expr) |
virtual tvt | l_get (literalt a) const =0 |
virtual void | set_frozen (literalt a) |
virtual void | set_frozen (const bvt &) |
virtual void | set_assumptions (const bvt &_assumptions) |
virtual bool | has_set_assumptions () const |
virtual void | set_all_frozen () |
virtual bool | is_in_conflict (literalt l) const |
determine whether a variable is in the final conflict More... | |
virtual bool | has_is_in_conflict () const |
virtual void | set_time_limit_seconds (uint32_t) |
![]() | |
decision_proceduret (const namespacet &_ns) | |
virtual | ~decision_proceduret () |
virtual exprt | get (const exprt &expr) const =0 |
virtual void | print_assignment (std::ostream &out) const =0 |
virtual void | set_to (const exprt &expr, bool value)=0 |
void | set_to_true (const exprt &expr) |
void | set_to_false (const exprt &expr) |
virtual resultt | dec_solve ()=0 |
resultt | operator() () |
virtual std::string | decision_procedure_text () const =0 |
Additional Inherited Members | |
![]() | |
enum | resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR } |
![]() | |
const namespacet & | ns |
Definition at line 27 of file prop_conv.h.
|
inlineexplicit |
Definition at line 30 of file prop_conv.h.
|
inlinevirtual |
Definition at line 33 of file prop_conv.h.
Implemented in smt2_convt, and prop_conv_solvert.
Referenced by prop_minimizet::constraint(), symex_target_equationt::convert_assertions(), symex_target_equationt::convert_assumptions(), symex_target_equationt::convert_decls(), symex_target_equationt::convert_goto_instructions(), symex_target_equationt::convert_guards(), bmc_all_propertiest::operator()(), operator()(), and bmc_covert::operator()().
|
inlinevirtual |
Reimplemented in prop_conv_solvert.
Definition at line 57 of file prop_conv.h.
|
inlinevirtual |
Reimplemented in prop_conv_solvert, and smt2_dect.
Definition at line 52 of file prop_conv.h.
Referenced by prop_minimizet::operator()().
|
virtual |
determine whether a variable is in the final conflict
Reimplemented in prop_conv_solvert.
Definition at line 13 of file prop_conv.cpp.
References UNREACHABLE.
Implemented in smt2_convt, and prop_conv_solvert.
Referenced by build_goto_trace(), prop_minimizet::fix_objectives(), counterexample_beautificationt::get_failed_property(), fault_localizationt::get_failed_property(), counterexample_beautificationt::get_minimization_list(), bmc_all_propertiest::goal_covered(), fault_localizationt::goal_covered(), is_failed_assertion_step(), is_failed_assumption_step(), cover_goalst::mark(), bmc_covert::satisfying_assignment(), and fault_localizationt::update_scores().
Definition at line 38 of file prop_conv.h.
References convert().
|
inlinevirtual |
Reimplemented in prop_conv_solvert.
Definition at line 53 of file prop_conv.h.
|
virtual |
Reimplemented in smt2_convt, prop_conv_solvert, and bv_refinementt.
Definition at line 19 of file prop_conv.cpp.
References UNREACHABLE.
Referenced by fault_localizationt::check(), prop_minimizet::operator()(), and fault_localizationt::run().
|
virtual |
Reimplemented in smt2_convt, and prop_conv_solvert.
Definition at line 24 of file prop_conv.cpp.
References UNREACHABLE.
Referenced by cover_goalst::freeze_goal_variables(), fault_localizationt::freeze_guards(), and set_frozen().
|
virtual |
Definition at line 29 of file prop_conv.cpp.
References set_frozen().
|
inlinevirtual |
Reimplemented in prop_conv_solvert.
Definition at line 60 of file prop_conv.h.