Home
last modified time | relevance | path

Searched refs:BITBLAST_MODE_LAZY (Results 1 – 9 of 9) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/options/
H A Dbv_bitblast_mode.h35 BITBLAST_MODE_LAZY, enumerator
H A Dbv_bitblast_mode.cpp25 case theory::bv::BITBLAST_MODE_LAZY: in operator <<()
H A Doptions_handler.cpp1167 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY && in stringToSatSolver()
1187 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY in stringToSatSolver()
1288 return theory::bv::BITBLAST_MODE_LAZY; in stringToBitblastMode()
H A Dbv_options.toml34 default = "CVC4::theory::bv::BITBLAST_MODE_LAZY"
/dports/math/cvc4/CVC4-1.7/src/preprocessing/passes/
H A Dbv_abstraction.cpp56 if (options::bitblastMode() == bv::BITBLAST_MODE_LAZY && changed) in applyInternal()
/dports/math/cvc4/CVC4-1.7/src/theory/bv/
H A Dbv_subtheory_bitblast.cpp123 Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); in check()
H A Dtheory_bv.cpp915 Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); in getEqualityStatus()
H A Dabstraction.cpp1085 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY) { in addInputAtom()
H A Dbv_subtheory_algebraic.cpp256 Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); in check()