CBMC
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
propt Class Referenceabstract

TO_BE_DOCUMENTED. More...

#include <prop.h>

+ Inheritance diagram for propt:
[フレーム]
[legend]
+ Collaboration diagram for propt:
[フレーム]
[legend]

Public Types

enum class   resultt { P_SATISFIABLE , P_UNSATISFIABLE , P_ERROR }
 

Public Member Functions

  propt (message_handlert &message_handler)
 
virtual  ~propt ()
 
virtual literalt  land (literalt a, literalt b)=0
 
virtual literalt  lor (literalt a, literalt b)=0
 
virtual literalt  land (const bvt &bv)=0
 
virtual literalt  lor (const bvt &bv)=0
 
virtual literalt  lxor (literalt a, literalt b)=0
 
virtual literalt  lxor (const bvt &bv)=0
 
virtual literalt  lnand (literalt a, literalt b)=0
 
virtual literalt  lnor (literalt a, literalt b)=0
 
virtual literalt  lequal (literalt a, literalt b)=0
 
virtual literalt  limplies (literalt a, literalt b)=0
 
virtual literalt  lselect (literalt a, literalt b, literalt c)=0
 
virtual void  set_equal (literalt a, literalt b)
  asserts a==b in the propositional formula
 
virtual void  l_set_to (literalt a, bool value)
 
void  l_set_to_true (literalt a)
 
void  l_set_to_false (literalt a)
 
void  lcnf (literalt l0, literalt l1)
 
void  lcnf (literalt l0, literalt l1, literalt l2)
 
void  lcnf (literalt l0, literalt l1, literalt l2, literalt l3)
 
virtual void  lcnf (const bvt &bv)=0
 
virtual bool  has_set_to () const
 
virtual bool  cnf_handled_well () const
 
virtual bool  has_assumptions () const
 
virtual literalt  new_variable ()=0
 
virtual void  set_variable_name (literalt, const irep_idt &)
 
virtual size_t  no_variables () const =0
 
virtual bvt  new_variables (std::size_t width)
  generates a bitvector of given width with new variables
 
virtual std::string  solver_text () const =0
 
resultt  prop_solve ()
 
resultt  prop_solve (const bvt &assumptions)
 
virtual tvt  l_get (literalt a) const =0
 
virtual void  set_assignment (literalt a, bool value)=0
 
virtual bool  is_in_conflict (literalt l) const =0
  Returns true if an assumption is in the final conflict.
 
virtual bool  has_is_in_conflict () const
 
virtual void  set_frozen (literalt)
 
virtual void  set_time_limit_seconds (uint32_t)
 
std::size_t  get_number_of_solver_calls () const
 

Protected Member Functions

virtual resultt  do_prop_solve (const bvt &assumptions)=0
 

Protected Attributes

bvt  lcnf_bv
 
messaget  log
 
std::size_t  number_of_solver_calls = 0
 

Detailed Description

TO_BE_DOCUMENTED.

Definition at line 24 of file prop.h.

Member Enumeration Documentation

◆  resultt

enum class propt::resultt
strong
Enumerator
P_SATISFIABLE 
P_UNSATISFIABLE 
P_ERROR 

Definition at line 101 of file prop.h.

Constructor & Destructor Documentation

◆  propt()

propt::propt ( message_handlert &  message_handler )
inlineexplicit

Definition at line 27 of file prop.h.

◆  ~propt()

virtual propt::~propt ( )
inlinevirtual

Definition at line 31 of file prop.h.

Member Function Documentation

◆  cnf_handled_well()

virtual bool propt::cnf_handled_well ( ) const
inlinevirtual

Definition at line 85 of file prop.h.

◆  do_prop_solve()

◆  get_number_of_solver_calls()

std::size_t propt::get_number_of_solver_calls ( ) const

Definition at line 52 of file prop.cpp.

◆  has_assumptions()

◆  has_is_in_conflict()

◆  has_set_to()

virtual bool propt::has_set_to ( ) const
inlinevirtual

Definition at line 81 of file prop.h.

◆  is_in_conflict()

virtual bool propt::is_in_conflict ( literalt  l ) const
pure virtual

Returns true if an assumption is in the final conflict.

Note that only literals that are assumptions (see set_assumptions) may be queried.

Returns
true iff the given literal is part of the final conflict

Implemented in satcheck_cadical_baset, satcheck_glucose_baset< T >, satcheck_glucose_baset< Glucose::SimpSolver >, satcheck_glucose_baset< Glucose::Solver >, satcheck_ipasirt, satcheck_lingelingt, satcheck_minisat2_baset< T >, satcheck_minisat2_baset< Minisat::SimpSolver >, satcheck_minisat2_baset< Minisat::Solver >, satcheck_picosatt, dimacs_cnft, satcheck_minisat1_baset, and external_satt.

◆  l_get()

◆  l_set_to()

virtual void propt::l_set_to ( literalt  a,
bool  value 
)
inlinevirtual

Definition at line 47 of file prop.h.

◆  l_set_to_false()

void propt::l_set_to_false ( literalt  a )
inline

Definition at line 54 of file prop.h.

◆  l_set_to_true()

void propt::l_set_to_true ( literalt  a )
inline

Definition at line 52 of file prop.h.

◆  land() [1/2]

virtual literalt propt::land ( const bvt &  bv )
pure virtual

Implemented in cnft.

◆  land() [2/2]

virtual literalt propt::land ( literalt  a,
literalt  b 
)
pure virtual

Implemented in cnft.

◆  lcnf() [1/4]

◆  lcnf() [2/4]

void propt::lcnf ( literalt  l0,
literalt  l1 
)
inline

Definition at line 58 of file prop.h.

◆  lcnf() [3/4]

void propt::lcnf ( literalt  l0,
literalt  l1,
literalt  l2 
)
inline

Definition at line 61 of file prop.h.

◆  lcnf() [4/4]

void propt::lcnf ( literalt  l0,
literalt  l1,
literalt  l2,
literalt  l3 
)
inline

Definition at line 70 of file prop.h.

◆  lequal()

virtual literalt propt::lequal ( literalt  a,
literalt  b 
)
pure virtual

Implemented in cnft.

◆  limplies()

virtual literalt propt::limplies ( literalt  a,
literalt  b 
)
pure virtual

Implemented in cnft.

◆  lnand()

virtual literalt propt::lnand ( literalt  a,
literalt  b 
)
pure virtual

Implemented in cnft.

◆  lnor()

virtual literalt propt::lnor ( literalt  a,
literalt  b 
)
pure virtual

Implemented in cnft.

◆  lor() [1/2]

virtual literalt propt::lor ( const bvt &  bv )
pure virtual

Implemented in qbf_bdd_coret, and cnft.

◆  lor() [2/2]

virtual literalt propt::lor ( literalt  a,
literalt  b 
)
pure virtual

Implemented in qbf_bdd_coret, and cnft.

◆  lselect()

virtual literalt propt::lselect ( literalt  a,
literalt  b,
literalt  c 
)
pure virtual

Implemented in cnft.

◆  lxor() [1/2]

virtual literalt propt::lxor ( const bvt &  bv )
pure virtual

Implemented in cnft.

◆  lxor() [2/2]

virtual literalt propt::lxor ( literalt  a,
literalt  b 
)
pure virtual

Implemented in cnft.

◆  new_variable()

virtual literalt propt::new_variable ( )
pure virtual

Implemented in qbf_bdd_coret, cnft, and qbf_bdd_certificatet.

◆  new_variables()

bvt propt::new_variables ( std::size_t  width )
virtual

generates a bitvector of given width with new variables

Returns
bitvector

Reimplemented in cnft.

Definition at line 30 of file prop.cpp.

◆  no_variables()

virtual size_t propt::no_variables ( ) const
pure virtual

Implemented in cnft.

◆  prop_solve() [1/2]

propt::resultt propt::prop_solve ( )

Definition at line 39 of file prop.cpp.

◆  prop_solve() [2/2]

propt::resultt propt::prop_solve ( const bvt &  assumptions )

Definition at line 46 of file prop.cpp.

◆  set_assignment()

◆  set_equal()

void propt::set_equal ( literalt  a,
literalt  b 
)
virtual

asserts a==b in the propositional formula

Definition at line 12 of file prop.cpp.

◆  set_frozen()

virtual void propt::set_frozen ( literalt  )
inlinevirtual

Reimplemented in satcheck_glucose_simplifiert, satcheck_lingelingt, and satcheck_minisat_simplifiert.

Definition at line 117 of file prop.h.

◆  set_time_limit_seconds()

virtual void propt::set_time_limit_seconds ( uint32_t  )
inlinevirtual

◆  set_variable_name()

virtual void propt::set_variable_name ( literalt  ,
const irep_idt &   
)
inlinevirtual

Definition at line 95 of file prop.h.

◆  solver_text()

Member Data Documentation

◆  lcnf_bv

bvt propt::lcnf_bv
protected

Definition at line 132 of file prop.h.

◆  log

messaget propt::log
protected

Definition at line 134 of file prop.h.

◆  number_of_solver_calls

std::size_t propt::number_of_solver_calls = 0
protected

Definition at line 135 of file prop.h.

The documentation for this class was generated from the following files:
  • /home/runner/work/cbmc/cbmc/src/solvers/prop/prop.h
  • /home/runner/work/cbmc/cbmc/src/solvers/prop/prop.cpp

AltStyle によって変換されたページ (->オリジナル) /