Home
last modified time | relevance | path

Searched refs:d_proofsEnabled (Results 1 – 4 of 4) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/
H A Dtheory.h231 bool d_proofsEnabled; variable
853 void produceProofs() { d_proofsEnabled = true; } in produceProofs()
H A Dtheory.cpp80 d_proofsEnabled(false) in Theory()
/dports/math/cvc4/CVC4-1.7/src/theory/arrays/
H A Dtheory_arrays.cpp1359 if (!d_proofsEnabled) { in check()
1391 if (d_proofsEnabled) { in check()
1407 if (!d_proofsEnabled) { in check()
2077 if (!d_proofsEnabled) { in queueRowLemma()
2089 if ((options::arraysEagerLemmas() || bothExist) && !d_proofsEnabled) { in queueRowLemma()
2259 std::shared_ptr<eq::EqProof> proof = d_proofsEnabled ? in conflict()
2267 if (d_proofsEnabled) { in conflict()
/dports/math/cvc4/CVC4-1.7/src/theory/uf/
H A Dtheory_uf.cpp720 d_proofsEnabled ? std::make_shared<eq::EqProof>() : nullptr; in conflict()
722 std::unique_ptr<ProofUF> puf(d_proofsEnabled ? new ProofUF(pf) : nullptr); in conflict()