cprover
|
TO_BE_DOCUMENTED. More...
#include <prop_assignment.h>
Public Member Functions | |
virtual | ~prop_assignmentt () |
virtual tvt | l_get (literalt a) const =0 |
virtual void | set_assignment (literalt a, bool value)=0 |
virtual void | copy_assignment_from (const propt &prop)=0 |
TO_BE_DOCUMENTED.
Definition at line 20 of file prop_assignment.h.
|
virtual |
Definition at line 12 of file prop_assignment.cpp.
|
pure virtual |
Implemented in cnf_clause_list_assignmentt, and propt.
Implemented in aig_prop_solvert, propt, cnf_clause_list_assignmentt, prop_wrappert, qbf_bdd_coret, aig_prop_baset, dimacs_cnf_dumpt, dplib_propt, cvc_propt, pbs_dimacs_cnft, smt2_propt, smt1_propt, qbf_bdd_certificatet, cnf_clause_listt, satcheck_glucose_baset< T >, satcheck_minisat2_baset< T >, satcheck_glucose_baset< Glucose::Solver >, satcheck_glucose_baset< Glucose::SimpSolver >, satcheck_minisat2_baset< Minisat::SimpSolver >, satcheck_minisat2_baset< Minisat::Solver >, qbf_qube_coret, qbf_squolem_coret, qbf_squolemt, satcheck_minisat1_baset, satcheck_zchaff_baset, satcheck_precosatt, satcheck_smvsatt, satcheck_lingelingt, satcheck_picosatt, satcheck_booleforce_baset, satcheck_zcoret, satcheck_limmatt, qbf_quantort, qbf_qubet, qbf_skizzot, and qdimacs_coret.
|
pure virtual |
Implemented in propt, smt2_propt, smt1_propt, satcheck_glucose_baset< T >, satcheck_minisat2_baset< T >, satcheck_glucose_baset< Glucose::Solver >, satcheck_glucose_baset< Glucose::SimpSolver >, satcheck_minisat2_baset< Minisat::SimpSolver >, satcheck_minisat2_baset< Minisat::Solver >, satcheck_minisat1_baset, satcheck_precosatt, satcheck_zchaff_baset, satcheck_lingelingt, and satcheck_picosatt.