Home
last modified time | relevance | path

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

/dports/math/cvc4/CVC4-1.7/src/proof/
H A Dsimplify_boolean_node.cpp44 std::string litName = ProofManager::getLitName(n.negate()); in simplifyBooleanNode()
62 std::string simplifiedLitName = ProofManager::getLitName(simplified.negate()); in simplifyBooleanNode()
73 std::string simplifiedLitName = ProofManager::getLitName(simplified.negate()); in simplifyBooleanNode()
84 std::string simplifiedLitName = ProofManager::getLitName(simplified.negate()); in simplifyBooleanNode()
95 std::string simplifiedLitName = ProofManager::getLitName(simplified.negate()); in simplifyBooleanNode()
147 std::string simplifiedLitName = ProofManager::getLitName(simplified.negate()); in simplifyBooleanNode()
155 std::string simplifiedLitName = ProofManager::getLitName(simplified.negate()); in simplifyBooleanNode()
163 std::string simplifiedLitName = ProofManager::getLitName(simplified.negate()); in simplifyBooleanNode()
171 std::string simplifiedLitName = ProofManager::getLitName(simplified.negate()); in simplifyBooleanNode()
H A Dcnf_proof.cpp483 ProofManager::getLitName((*clause)[negIndexInClause], d_name); in printCnfProofForClause()
485 ProofManager::getLitName((*clause)[posIndexInClause], d_name); in printCnfProofForClause()
533 os_base << ProofManager::getLitName(blit, d_name); in printCnfProofForClause()
551 os << os_base.str() << " " << ProofManager::getLitName(lit, d_name); in printCnfProofForClause()
555 os << ProofManager::getLitName(lit, d_name) << " " << os_base.str(); in printCnfProofForClause()
594 os_main << ProofManager::getLitName(lit, d_name) << " "; in printCnfProofForClause()
754 os_base_n << ProofManager::getLitName(lit1, d_name) << " "; in printCnfProofForClause()
774 os << ProofManager::getLitName(lit2, d_name); in printCnfProofForClause()
814 os_main << ProofManager::getLitName(lit1, d_name) << " "; in printCnfProofForClause()
821 os << ProofManager::getLitName(lit2, d_name) << " " << os_main.str(); in printCnfProofForClause()
[all …]
H A Darith_proof.cpp237 out << ") (pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl; in toStreamRecLFSC()
245 out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl; in toStreamRecLFSC()
407 out << ProofManager::getLitName(pf.d_node.negate()); in toStreamRecLFSC()
1030 << ProofManager::getLitName(antecedent.negate(), in printTheoryLemmaProof()
1045 << ProofManager::getLitName(antecedent.negate(), linearizedProofPrefix) in printTheoryLemmaProof()
1055 << ProofManager::getLitName(antecedent.negate(), in printTheoryLemmaProof()
1057 << " " << ProofManager::getLitName(antecedent.negate(), "") in printTheoryLemmaProof()
1064 << ProofManager::getLitName(antecedent.negate(), in printTheoryLemmaProof()
1066 << " " << ProofManager::getLitName(antecedent.negate(), "") << ")"; in printTheoryLemmaProof()
1142 os << " " << ProofManager::getLitName(lit.negate(), linearizedProofPrefix) in printTheoryLemmaProof()
H A Dresolution_bitvector_proof.cpp284 os << pm->getLitName(main_lit); in printTheoryLemmaProof()
386 os << pm->getLitName(main_lit); in printTheoryLemmaProof()
414 os << pm->getLitName(main_lit); in printTheoryLemmaProof()
443 os << ProofManager::getLitName(lemma[i]); in printTheoryLemmaProof()
H A Duf_proof.cpp68 out << ProofManager::getLitName(NodeManager::currentNM()->mkConst(false).notNode()); in toStreamRecLFSC()
118 out << "(pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl; in toStreamRecLFSC()
120 out << ss.str() << " " << ProofManager::getLitName(n2[0]) << "))"; in toStreamRecLFSC()
128 out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl; in toStreamRecLFSC()
317 out << ProofManager::getLitName(pf.d_node.negate()); in toStreamRecLFSC()
H A Dproof_manager.h237 static std::string getLitName(prop::SatLiteral lit, const std::string& prefix = "");
238 static std::string getLitName(TNode lit, const std::string& prefix = "");
H A Dtheory_proof.cpp671 rewritten << pm->getLitName(explanation); in printTheoryLemmas()
679 rewritten << pm->getLitName(explanation); in printTheoryLemmas()
686 << pm->getLitName(*missingAssertion) << " --> " << rewritten.str() in printTheoryLemmas()
690 pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str()); in printTheoryLemmas()
793 rewritten << pm->getLitName(explanation); in printTheoryLemmas()
801 rewritten << pm->getLitName(explanation); in printTheoryLemmas()
808 << pm->getLitName(*missingAssertion) << " --> " << rewritten.str() in printTheoryLemmas()
812 pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str()); in printTheoryLemmas()
H A Darray_proof.cpp153 … out << ") (pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl; in toStreamRecLFSC()
162 ProofManager::getLitName(n2[0]) << std::endl; in toStreamRecLFSC()
164 out << " " << ProofManager::getLitName(n2[0]); in toStreamRecLFSC()
449 ProofManager::getLitName(pf.d_node.negate()) << std::endl; in toStreamRecLFSC()
450 out << ProofManager::getLitName(pf.d_node.negate()); in toStreamRecLFSC()
1051 out << ProofManager::getLitName(child_proof->d_node[0]); in toStreamRecLFSC()
H A Dproof_manager.cpp209 std::string ProofManager::getLitName(prop::SatLiteral lit, in getLitName() function in CVC4::ProofManager
238 std::string ProofManager::getLitName(TNode lit, in getLitName() function in CVC4::ProofManager
240 std::string litName = getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix); in getLitName()
932 std::string litName = getLitName(currentPM()->d_cnfProof->getLiteral(lit)); in haveRewriteFilter()