| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | valuation.cpp | 114 Node Valuation::ensureLiteral(TNode n) { in ensureLiteral() function in CVC4::theory::Valuation
115 return d_engine->ensureLiteral(n); in ensureLiteral()
|
| H A D | valuation.h | 125 Node ensureLiteral(TNode n) CVC4_WARN_UNUSED_RESULT;
|
| H A D | decision_strategy.cpp | 117 lit = d_valuation.ensureLiteral(lit); in getLiteral()
|
| H A D | theory_engine.h | 823 Node ensureLiteral(TNode n);
|
| H A D | theory_engine.cpp | 725 Node e = ensureLiteral(equality); in combineTheories()
1495 Node TheoryEngine::ensureLiteral(TNode n) { in ensureLiteral() function in CVC4::TheoryEngine
1501 d_propEngine->ensureLiteral(preprocessed); in ensureLiteral()
|
| /dports/math/cvc4/CVC4-1.7/src/prop/ |
| H A D | cnf_stream.h | 234 virtual void ensureLiteral(TNode n, bool noPreregistration = false) = 0;
334 void ensureLiteral(TNode n, bool noPreregistration = false) override;
|
| H A D | prop_engine.h | 191 void ensureLiteral(TNode n);
|
| H A D | prop_engine.cpp | 263 void PropEngine::ensureLiteral(TNode n) { in ensureLiteral() function in CVC4::prop::PropEngine
264 d_cnfStream->ensureLiteral(n); in ensureLiteral()
|
| H A D | cnf_stream.cpp | 126 void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) { in ensureLiteral() function in CVC4::prop::TseitinCnfStream
|
| /dports/math/cvc4/CVC4-1.7/src/proof/ |
| H A D | cnf_proof.cpp | 116 d_cnfStream->ensureLiteral(trueNode); in registerTrueUnitClause()
128 d_cnfStream->ensureLiteral(falseNode); in registerFalseUnitClause()
269 void CnfProof::ensureLiteral(TNode atom, bool noPreregistration) { in ensureLiteral() function in CVC4::CnfProof
270 d_cnfStream->ensureLiteral(atom, noPreregistration); in ensureLiteral()
|
| H A D | cnf_proof.h | 101 void ensureLiteral(TNode node, bool noPreregistration = false);
|
| H A D | proof_manager.cpp | 645 … d_cnfProof->ensureLiteral(*it, true); // This disables preregistration with the theory solver. in toStream()
647 d_cnfProof->ensureLiteral(*it); // Normal method, with theory solver preregisteration. in toStream()
1063 void ProofManager::ensureLiteral(Node node) { in ensureLiteral() function in CVC4::ProofManager
1064 d_cnfProof->ensureLiteral(node); in ensureLiteral()
|
| H A D | proof_manager.h | 213 void ensureLiteral(Node node);
|
| H A D | uf_proof.cpp | 604 ProofManager::currentPM()->ensureLiteral( in registerTerm()
606 ProofManager::currentPM()->ensureLiteral( in registerTerm()
|
| H A D | array_proof.cpp | 1098 ProofManager::currentPM()->ensureLiteral( in registerTerm()
1100 ProofManager::currentPM()->ensureLiteral( in registerTerm()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/ |
| H A D | eager_bitblaster.cpp | 81 d_cnfStream->ensureLiteral(node); in bbFormula()
|
| H A D | lazy_bitblaster.cpp | 250 d_cnfStream->ensureLiteral(atom); in addAtom()
|
| /dports/math/cvc4/CVC4-1.7/test/unit/prop/ |
| H A D | cnf_stream_white.h | 292 d_cnfStream->ensureLiteral(a_and_b); in testEnsureLiteral()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | term_util.cpp | 233 Node ceLit = d_quantEngine->getValuation().ensureLiteral( g ); in getCounterexampleLiteral()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | synth_conjecture.cpp | 84 d_feasible_guard = d_qe->getValuation().ensureLiteral(d_feasible_guard); in assign()
|
| H A D | term_database_sygus.cpp | 684 ag = d_quantEngine->getValuation().ensureLiteral(ag); in registerEnumerator()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/arith/ |
| H A D | nonlinear_extension.cpp | 1029 mg = d_containing.getValuation().ensureLiteral(mg); in checkModel()
1865 Node literal = d_containing.getValuation().ensureLiteral(eq); in checkSplitZero()
2466 Node literal = d_containing.getValuation().ensureLiteral(req); in check()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/arrays/ |
| H A D | theory_arrays.cpp | 2078 i_eq_j = d_valuation.ensureLiteral(i.eqNode(j)); // TODO: think about this in queueRowLemma()
|