CVC3  2.4.1
sat Directory Reference

Files

file  cnf.cpp [code]
 Implementation of classes used for generic CNF formulas.
 
file  cnf_manager.cpp [code]
 Implementation of CNF_Manager.
 
file  cnf_rules.h [code]
 Abstract proof rules for CNF conversion.
 
file  cnf_theorem_producer.cpp [code]
 Implementation of CNF_TheoremProducer.
 
file  cnf_theorem_producer.h [code]
 Implementation of CNF_Rules API.
 
file  dpllt_basic.cpp [code]
 Basic implementation of dpllt module using generic sat solver.
 
file  dpllt_minisat.cpp [code]
 Implementation of dpllt module using MiniSat.
 
file  minisat_derivation.cpp [code]
 MiniSat proof logging.
 
file  minisat_derivation.h [code]
 MiniSat proof logging.
 
file  minisat_global.h [code]
 MiniSat global functions.
 
file  minisat_heap.h [code]
 MiniSat internal heap implementation.
 
file  minisat_solver.cpp [code]
 Adaptation of MiniSat to DPLL(T)
 
file  minisat_solver.h [code]
 Adaptation of MiniSat to DPLL(T)
 
file  minisat_types.cpp [code]
 MiniSat internal types.
 
file  minisat_types.h [code]
 MiniSat internal types.
 
file  minisat_varorder.h [code]
 MiniSat decision heuristics.
 
file  sat_api.cpp [code]
 
file  sat_proof.h [code]
 Sat solver proof representation.
 
file  xchaff.cpp [code]
 
file  xchaff.h [code]
 
file  xchaff_base.h [code]
 
file  xchaff_dbase.cpp [code]
 
file  xchaff_dbase.h [code]
 
file  xchaff_solver.cpp [code]
 
file  xchaff_solver.h [code]
 
file  xchaff_utils.cpp [code]
 
file  xchaff_utils.h [code]