diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
commit | 904ffb6e73402bae537aa89e7fd8f0ab2e9d60e2 (patch) | |
tree | d96bb0c974bdea6170957d3e39d47a98f5c85ca0 /src/proof/proof_manager.h | |
parent | a0054e9cc78822416d745e955c30f69cbb2a3aa7 (diff) |
update from the master
Diffstat (limited to 'src/proof/proof_manager.h')
-rw-r--r-- | src/proof/proof_manager.h | 58 |
1 files changed, 34 insertions, 24 deletions
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 96c4e1d61..c74aac237 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -1,13 +1,13 @@ /********************* */ /*! \file proof_manager.h ** \verbatim - ** Original author: Liana Hadarean - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): Andrew Reynolds + ** Top contributors (to current version): + ** Liana Hadarean, Morgan Deters, Guy Katz ** 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 Proofs ** @@ -21,8 +21,11 @@ #include <iosfwd> #include <map> - +#include "proof/proof.h" +#include "proof/skolemization_manager.h" +#include "util/proof.h" #include "expr/node.h" +#include "proof/clause_id.h" #include "proof/proof.h" #include "theory/logic_info.h" #include "theory/substitutions.h" @@ -46,13 +49,12 @@ namespace prop { class SmtEngine; -typedef unsigned ClauseId; const ClauseId ClauseIdEmpty(-1); -const ClauseId ClauseIdUndef(-2); +const ClauseId ClauseIdUndef(-2); const ClauseId ClauseIdError(-3); class Proof; -template <class Solver> class TSatProof; +template <class Solver> class TSatProof; typedef TSatProof< CVC4::Minisat::Solver> CoreSatProof; class CnfProof; @@ -60,10 +62,11 @@ class RewriterProof; class TheoryProofEngine; class TheoryProof; class UFProof; +class ArithProof; class ArrayProof; class BitVectorProof; -template <class Solver> class LFSCSatProof; +template <class Solver> class LFSCSatProof; typedef LFSCSatProof< CVC4::Minisat::Solver> LFSCCoreSatProof; class LFSCCnfProof; @@ -74,7 +77,7 @@ class LFSCRewriterProof; template <class Solver> class ProofProxy; typedef ProofProxy< CVC4::Minisat::Solver> CoreProofProxy; -typedef ProofProxy< CVC4::BVMinisat::Solver> BVProofProxy; +typedef ProofProxy< CVC4::BVMinisat::Solver> BVProofProxy; namespace prop { typedef uint64_t SatVariable; @@ -96,8 +99,6 @@ typedef __gnu_cxx::hash_set<Node, NodeHashFunction > NodeSet; typedef __gnu_cxx::hash_map<Node, std::vector<Node>, NodeHashFunction > NodeToNodes; typedef std::hash_set<ClauseId> IdHashSet; -typedef unsigned ClauseId; - enum ProofRule { RULE_GIVEN, /* input assertion */ RULE_DERIVED, /* a "macro" rule */ @@ -107,7 +108,7 @@ enum ProofRule { RULE_CONFLICT, /* re-construct as a conflict */ RULE_TSEITIN, /* Tseitin CNF transformation */ RULE_SPLIT, /* A splitting lemma of the form a v ~ a*/ - + RULE_ARRAYS_EXT, /* arrays, extensional */ RULE_ARRAYS_ROW, /* arrays, read-over-write */ };/* enum ProofRules */ @@ -122,6 +123,8 @@ class ProofManager { ExprSet d_inputCoreFormulas; ExprSet d_outputCoreFormulas; + SkolemizationManager d_skolemizationManager; + int d_nextId; Proof* d_fullProof; @@ -131,6 +134,8 @@ class ProofManager { // trace dependences back to unsat core void traceDeps(TNode n); + std::set<Type> d_printedTypes; + protected: LogicInfo d_logic; @@ -155,6 +160,9 @@ public: static UFProof* getUfProof(); static BitVectorProof* getBitVectorProof(); static ArrayProof* getArrayProof(); + static ArithProof* getArithProof(); + + static SkolemizationManager *getSkolemizationManager(); // iterators over data shared by proofs typedef ExprSet::const_iterator assertions_iterator; @@ -165,17 +173,17 @@ public: } assertions_iterator end_assertions() const { return d_inputFormulas.end(); } size_t num_assertions() const { return d_inputFormulas.size(); } - + //---from Morgan--- Node mkOp(TNode n); Node lookupOp(TNode n) const; bool hasOp(TNode n) const; - + std::map<Node, Node> d_ops; std::map<Node, Node> d_bops; //---end from Morgan--- - - + + // variable prefixes static std::string getInputClauseName(ClauseId id, const std::string& prefix = ""); static std::string getLemmaClauseName(ClauseId id, const std::string& prefix = ""); @@ -183,7 +191,7 @@ public: static std::string getLearntClauseName(ClauseId id, const std::string& prefix = ""); static std::string getPreprocessedAssertionName(Node node, const std::string& prefix = ""); static std::string getAssertionName(Node node, const std::string& prefix = ""); - + static std::string getVarName(prop::SatVariable var, const std::string& prefix = ""); static std::string getAtomName(prop::SatVariable var, const std::string& prefix = ""); static std::string getAtomName(TNode atom, const std::string& prefix = ""); @@ -192,14 +200,13 @@ public: // for SMT variable names that have spaces and other things static std::string sanitize(TNode var); - - /** Add proof assertion - unlinke addCoreAssertion this is post definition expansion **/ + /** Add proof assertion - unlike addCoreAssertion this is post definition expansion **/ void addAssertion(Expr formula); - + /** Public unsat core methods **/ void addCoreAssertion(Expr formula); - + void addDependence(TNode n, TNode dep); void addUnsatCore(Expr formula); @@ -214,6 +221,9 @@ public: const std::string getLogic() const { return d_logic.getLogicString(); } LogicInfo & getLogicInfo() { return d_logic; } + void markPrinted(const Type& type); + bool wasPrinted(const Type& type) const; + };/* class ProofManager */ class LFSCProof : public Proof { |