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]