diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-05-20 15:29:32 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-20 18:29:32 +0000 |
| commit | a0644780130dd0ed86a9486e29aa326b3fe5d804 (patch) | |
| tree | 8cd1f0e0b18e67fa91dfff48eac5204eaf4ee3fc /src/prop/cnf_stream.h | |
| parent | 61b14cbbbb1665496913e047d14fedee610efef1 (diff) | |
Remove old unsat cores (#6581)
This commit removes the remaining old proof code and the code to produce unsat cores based on it.
Diffstat (limited to 'src/prop/cnf_stream.h')
| -rw-r--r-- | src/prop/cnf_stream.h | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 9901fb18b..264e26777 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -30,7 +30,6 @@ #include "context/cdinsert_hashmap.h" #include "context/cdlist.h" #include "expr/node.h" -#include "proof/proof_manager.h" #include "prop/proof_cnf_stream.h" #include "prop/registrar.h" #include "prop/sat_solver_types.h" @@ -164,8 +163,6 @@ class CnfStream { /** Retrieves map from literals to nodes. */ const CnfStream::LiteralToNodeMap& getNodeCache() const; - void setProof(CnfProof* proof); - protected: /** * Same as above, except that uses the saved d_removable flag. It calls the @@ -243,9 +240,6 @@ class CnfStream { /** The name of this CNF stream*/ std::string d_name; - /** Pointer to the proof corresponding to this CnfStream */ - CnfProof* d_cnfProof; - /** * Are we asserting a removable clause (true) or a permanent clause (false). * This is set at the beginning of convertAndAssert so that it doesn't |