diff options
Diffstat (limited to 'src/proof/cnf_proof.h')
| -rw-r--r-- | src/proof/cnf_proof.h | 45 |
1 files changed, 27 insertions, 18 deletions
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 675bd9b9d..a21cb1c0e 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -1,13 +1,13 @@ /********************* */ /*! \file cnf_proof.h ** \verbatim - ** Original author: Liana Hadarean - ** Major contributors: Morgan Deters, Andrew Reynolds - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Liana Hadarean, Guy Katz, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief A manager for CnfProofs. ** @@ -21,14 +21,13 @@ #ifndef __CVC4__CNF_PROOF_H #define __CVC4__CNF_PROOF_H -#include <ext/hash_map> +#include <ext/hash_map> #include <ext/hash_set> #include <iosfwd> #include "context/cdhashmap.h" +#include "proof/clause_id.h" #include "proof/sat_proof.h" -#include "proof/sat_proof.h" -#include "util/proof.h" #include "util/proof.h" namespace CVC4 { @@ -44,6 +43,7 @@ typedef __gnu_cxx::hash_set<ClauseId> ClauseIdSet; typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode; typedef context::CDHashMap<Node, ProofRule, NodeHashFunction> NodeToProofRule; +typedef context::CDHashMap<ClauseId, theory::TheoryId> ClauseIdToTheory; class CnfProof { protected: @@ -55,28 +55,33 @@ protected: /** Map from assertion to reason for adding assertion **/ NodeToProofRule d_assertionToProofRule; + /** Map from assertion to the theory that added this assertion **/ + ClauseIdToTheory d_clauseIdToOwnerTheory; + + /** The last theory to explain a lemma **/ + theory::TheoryId d_explainerTheory; + /** Top of stack is assertion currently being converted to CNF **/ std::vector<Node> d_currentAssertionStack; /** Top of stack is top-level fact currently being converted to CNF **/ std::vector<Node> d_currentDefinitionStack; - /** Map from ClauseId to the top-level fact that lead to adding this clause **/ ClauseIdToNode d_clauseToDefinition; /** Top-level facts that follow from assertions during convertAndAssert **/ NodeSet d_definitions; - + /** Map from top-level fact to facts/assertion that it follows from **/ NodeToNode d_cnfDeps; ClauseIdSet d_explanations; - + bool isDefinition(Node node); Node getDefinitionForClause(ClauseId clause); - + std::string d_name; public: CnfProof(CVC4::prop::CnfStream* cnfStream, @@ -104,10 +109,10 @@ public: /** Clause is one of the clauses defining top-level assertion node*/ void setClauseAssertion(ClauseId clause, Node node); - + void registerAssertion(Node assertion, ProofRule reason); void setCnfDependence(Node from, Node to); - + void pushCurrentAssertion(Node assertion); // the current assertion being converted void popCurrentAssertion(); Node getCurrentAssertion(); @@ -116,14 +121,18 @@ public: void popCurrentDefinition(); Node getCurrentDefinition(); - + void setExplainerTheory(theory::TheoryId theory); + theory::TheoryId getExplainerTheory(); + theory::TheoryId getOwnerTheory(ClauseId clause); + + void registerExplanationLemma(ClauseId clauseId); + // accessors for the leaf assertions that are being converted to CNF bool isAssertion(Node node); ProofRule getProofRule(Node assertion); ProofRule getProofRule(ClauseId clause); Node getAssertionForClause(ClauseId clause); - /** Virtual methods for printing things **/ virtual void printAtomMapping(const NodeSet& atoms, std::ostream& os, @@ -155,7 +164,7 @@ public: void printAtomMapping(const NodeSet& atoms, std::ostream& os, std::ostream& paren); - + void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren); |