1 /********************* */
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Guy Katz, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief A manager for CnfProofs.
14 ** A manager for CnfProofs.
19 #include "cvc4_private.h"
21 #ifndef __CVC4__CNF_PROOF_H
22 #define __CVC4__CNF_PROOF_H
25 #include <unordered_map>
26 #include <unordered_set>
28 #include "context/cdhashmap.h"
29 #include "proof/clause_id.h"
30 #include "proof/lemma_proof.h"
31 #include "proof/sat_proof.h"
32 #include "util/proof.h"
37 }/* CVC4::prop namespace */
41 typedef std::unordered_map
<prop::SatVariable
, Expr
> SatVarToExpr
;
42 typedef std::unordered_map
<Node
, Node
, NodeHashFunction
> NodeToNode
;
43 typedef std::unordered_set
<ClauseId
> ClauseIdSet
;
45 typedef context::CDHashMap
<ClauseId
, Node
> ClauseIdToNode
;
46 typedef context::CDHashMap
<Node
, ProofRule
, NodeHashFunction
> NodeToProofRule
;
47 typedef std::map
<std::set
<Node
>, LemmaProofRecipe
> LemmaToRecipe
;
48 typedef std::pair
<Node
, Node
> NodePair
;
49 typedef std::set
<NodePair
> NodePairSet
;
53 CVC4::prop::CnfStream
* d_cnfStream
;
55 /** Map from ClauseId to the assertion that lead to adding this clause **/
56 ClauseIdToNode d_clauseToAssertion
;
58 /** Map from assertion to reason for adding assertion **/
59 NodeToProofRule d_assertionToProofRule
;
61 /** Map from lemma to the recipe for proving it **/
62 LemmaToRecipe d_lemmaToProofRecipe
;
64 /** Top of stack is assertion currently being converted to CNF **/
65 std::vector
<Node
> d_currentAssertionStack
;
67 /** Top of stack is top-level fact currently being converted to CNF **/
68 std::vector
<Node
> d_currentDefinitionStack
;
70 /** Map from ClauseId to the top-level fact that lead to adding this clause **/
71 ClauseIdToNode d_clauseToDefinition
;
73 /** Top-level facts that follow from assertions during convertAndAssert **/
74 NodeSet d_definitions
;
76 /** Map from top-level fact to facts/assertion that it follows from **/
79 ClauseIdSet d_explanations
;
81 bool isDefinition(Node node
);
83 Node
getDefinitionForClause(ClauseId clause
);
87 CnfProof(CVC4::prop::CnfStream
* cnfStream
,
88 context::Context
* ctx
,
89 const std::string
& name
);
92 Node
getAtom(prop::SatVariable var
);
93 prop::SatLiteral
getLiteral(TNode node
);
94 bool hasLiteral(TNode node
);
95 void ensureLiteral(TNode node
, bool noPreregistration
= false);
97 void collectAtoms(const prop::SatClause
* clause
,
98 std::set
<Node
>& atoms
);
99 void collectAtomsForClauses(const IdToSatClause
& clauses
,
100 std::set
<Node
>& atoms
);
101 void collectAtomsAndRewritesForLemmas(const IdToSatClause
& lemmaClauses
,
102 std::set
<Node
>& atoms
,
103 NodePairSet
& rewrites
);
104 void collectAssertionsForClauses(const IdToSatClause
& clauses
,
105 NodeSet
& assertions
);
107 /** Methods for logging what the CnfStream does **/
108 // map the clause back to the current assertion where it came from
109 // if it is an explanation, it does not have a CNF proof since it is
111 void registerConvertedClause(ClauseId clause
, bool explanation
=false);
113 /** Clause is one of the clauses defining the node expression*/
114 void setClauseDefinition(ClauseId clause
, Node node
);
116 /** Clause is one of the clauses defining top-level assertion node*/
117 void setClauseAssertion(ClauseId clause
, Node node
);
119 void registerAssertion(Node assertion
, ProofRule reason
);
120 void setCnfDependence(Node from
, Node to
);
122 void pushCurrentAssertion(Node assertion
); // the current assertion being converted
123 void popCurrentAssertion();
124 Node
getCurrentAssertion();
126 void pushCurrentDefinition(Node assertion
); // the current Tseitin definition being converted
127 void popCurrentDefinition();
128 Node
getCurrentDefinition();
130 void setProofRecipe(LemmaProofRecipe
* proofRecipe
);
131 LemmaProofRecipe
getProofRecipe(const std::set
<Node
> &lemma
);
132 bool haveProofRecipe(const std::set
<Node
> &lemma
);
134 // accessors for the leaf assertions that are being converted to CNF
135 bool isAssertion(Node node
);
136 ProofRule
getProofRule(Node assertion
);
137 ProofRule
getProofRule(ClauseId clause
);
138 Node
getAssertionForClause(ClauseId clause
);
140 /** Virtual methods for printing things **/
141 virtual void printAtomMapping(const std::set
<Node
>& atoms
,
143 std::ostream
& paren
) = 0;
144 virtual void printAtomMapping(const std::set
<Node
>& atoms
,
147 ProofLetMap
&letMap
) = 0;
149 virtual void printClause(const prop::SatClause
& clause
,
151 std::ostream
& paren
) = 0;
152 virtual void printCnfProofForClause(ClauseId id
,
153 const prop::SatClause
* clause
,
155 std::ostream
& paren
) = 0;
157 };/* class CnfProof */
159 class LFSCCnfProof
: public CnfProof
{
160 Node
clauseToNode( const prop::SatClause
& clause
,
161 std::map
<Node
, unsigned>& childIndex
,
162 std::map
<Node
, bool>& childPol
);
163 bool printProofTopLevel(Node e
, std::ostream
& out
);
165 LFSCCnfProof(CVC4::prop::CnfStream
* cnfStream
,
166 context::Context
* ctx
,
167 const std::string
& name
)
168 : CnfProof(cnfStream
, ctx
, name
)
172 void printAtomMapping(const std::set
<Node
>& atoms
,
174 std::ostream
& paren
) override
;
176 void printAtomMapping(const std::set
<Node
>& atoms
,
179 ProofLetMap
& letMap
) override
;
181 void printClause(const prop::SatClause
& clause
,
183 std::ostream
& paren
) override
;
184 void printCnfProofForClause(ClauseId id
,
185 const prop::SatClause
* clause
,
187 std::ostream
& paren
) override
;
188 };/* class LFSCCnfProof */
190 } /* CVC4 namespace */
192 #endif /* __CVC4__CNF_PROOF_H */