diff options
author | lianah <lianahady@gmail.com> | 2013-10-08 16:50:28 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-10-08 16:50:28 -0400 |
commit | 3361081acd11178d0eb580ce91279a2ecaa7aa65 (patch) | |
tree | a1ea60d22fadc2d2ebefca3ab561fbcf74a6936b /src/proof/proof_manager.h | |
parent | ba8efaff308ef1eb14ec40dd74e0e18c16126d2c (diff) |
fixed uf proof with holes bugs
Diffstat (limited to 'src/proof/proof_manager.h')
-rw-r--r-- | src/proof/proof_manager.h | 24 |
1 files changed, 17 insertions, 7 deletions
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 4ae8a6dae..d4f1d6528 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -25,6 +25,7 @@ #include "proof/proof.h" #include "util/proof.h" + // forward declarations namespace Minisat { class Solver; @@ -35,6 +36,7 @@ namespace CVC4 { namespace prop { class CnfStream; } +typedef int ClauseId; class Proof; class SatProof; @@ -44,13 +46,20 @@ class TheoryProof; class LFSCSatProof; class LFSCCnfProof; class LFSCTheoryProof; - + +namespace prop { +typedef uint64_t SatVariable; +class SatLiteral; +} + // different proof modes enum ProofFormat { LFSC, NATIVE };/* enum ProofFormat */ +std::string append(const std::string& str, uint64_t num); + class ProofManager { SatProof* d_satProof; CnfProof* d_cnfProof; @@ -74,12 +83,13 @@ public: static TheoryProof* getTheoryProof(); // variable prefixes - static std::string getInputClausePrefix() { return "pb"; } - static std::string getLemmaClausePrefix() { return "lem"; } - static std::string getLearntClausePrefix() { return "cl"; } - static std::string getVarPrefix() { return "v"; } - static std::string getAtomPrefix() { return "a"; } - static std::string getLitPrefix() {return "l"; } + static std::string printInputClauseName(ClauseId id); + static std::string printLemmaClauseName(ClauseId id); + static std::string printLearntClauseName(ClauseId id); + + static std::string printVarName(prop::SatVariable var); + static std::string printAtomName(prop::SatVariable var); + static std::string printLitName(prop::SatLiteral lit); };/* class ProofManager */ class LFSCProof : public Proof { |