summaryrefslogtreecommitdiff
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/arith_proof.h24
-rw-r--r--src/proof/array_proof.h28
-rw-r--r--src/proof/bitvector_proof.h49
-rw-r--r--src/proof/cnf_proof.h8
-rw-r--r--src/proof/sat_proof.h16
-rw-r--r--src/proof/theory_proof.h75
-rw-r--r--src/proof/uf_proof.h35
7 files changed, 145 insertions, 90 deletions
diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index 0a44f45c0..677952bf7 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -67,7 +67,7 @@ protected:
public:
ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine);
- virtual void registerTerm(Expr term);
+ void registerTerm(Expr term) override;
};
class LFSCArithProof : public ArithProof {
@@ -75,13 +75,21 @@ public:
LFSCArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine)
: ArithProof(arith, proofEngine)
{}
- virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
- virtual void printOwnedSort(Type type, std::ostream& os);
- virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
- virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
+ void printOwnedTerm(Expr term,
+ std::ostream& os,
+ const ProofLetMap& map) override;
+ void printOwnedSort(Type type, std::ostream& os) override;
+ void printTheoryLemmaProof(std::vector<Expr>& lemma,
+ std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& map) override;
+ void printSortDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printTermDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printDeferredDeclarations(std::ostream& os,
+ std::ostream& paren) override;
+ void printAliasingDeclarations(std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& globalLetMap) override;
};
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index 99ad956a5..779624df0 100644
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -85,7 +85,7 @@ public:
std::string skolemToLiteral(Expr skolem);
- virtual void registerTerm(Expr term);
+ void registerTerm(Expr term) override;
};
class LFSCArrayProof : public ArrayProof {
@@ -94,15 +94,23 @@ public:
: ArrayProof(arrays, proofEngine)
{}
- virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
- virtual void printOwnedSort(Type type, std::ostream& os);
- virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
- virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
-
- bool printsAsBool(const Node &n);
+ void printOwnedTerm(Expr term,
+ std::ostream& os,
+ const ProofLetMap& map) override;
+ void printOwnedSort(Type type, std::ostream& os) override;
+ void printTheoryLemmaProof(std::vector<Expr>& lemma,
+ std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& map) override;
+ void printSortDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printTermDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printDeferredDeclarations(std::ostream& os,
+ std::ostream& paren) override;
+ void printAliasingDeclarations(std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& globalLetMap) override;
+
+ bool printsAsBool(const Node& n) override;
};
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index 69f9e774b..b5487a352 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -110,7 +110,7 @@ public:
void registerTermBB(Expr term);
void registerAtomBB(Expr atom, Expr atom_bb);
- virtual void registerTerm(Expr term);
+ void registerTerm(Expr term) override;
virtual void printTermBitblasting(Expr term, std::ostream& os) = 0;
virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap) = 0;
@@ -143,22 +143,37 @@ public:
LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
:BitVectorProof(bv, proofEngine)
{}
- virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
- virtual void printOwnedSort(Type type, std::ostream& os);
- virtual void printTermBitblasting(Expr term, std::ostream& os);
- virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap);
- virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os);
- virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
- virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
- virtual void printBitblasting(std::ostream& os, std::ostream& paren);
- virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap);
- void calculateAtomsInBitblastingProof();
- const std::set<Node>* getAtomsInBitblastingProof();
- void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
- void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2);
+ void printOwnedTerm(Expr term,
+ std::ostream& os,
+ const ProofLetMap& map) override;
+ void printOwnedSort(Type type, std::ostream& os) override;
+ void printTermBitblasting(Expr term, std::ostream& os) override;
+ void printAtomBitblasting(Expr term, std::ostream& os, bool swap) override;
+ void printAtomBitblastingToFalse(Expr term, std::ostream& os) override;
+ void printTheoryLemmaProof(std::vector<Expr>& lemma,
+ std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& map) override;
+ void printSortDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printTermDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printDeferredDeclarations(std::ostream& os,
+ std::ostream& paren) override;
+ void printAliasingDeclarations(std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& globalLetMap) override;
+ void printBitblasting(std::ostream& os, std::ostream& paren) override;
+ void printResolutionProof(std::ostream& os,
+ std::ostream& paren,
+ ProofLetMap& letMap) override;
+ void calculateAtomsInBitblastingProof() override;
+ const std::set<Node>* getAtomsInBitblastingProof() override;
+ void printConstantDisequalityProof(std::ostream& os,
+ Expr c1,
+ Expr c2,
+ const ProofLetMap& globalLetMap) override;
+ void printRewriteProof(std::ostream& os,
+ const Node& n1,
+ const Node& n2) override;
};
}/* CVC4 namespace */
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index a0d7096c0..9087817b3 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -171,20 +171,20 @@ public:
void printAtomMapping(const std::set<Node>& atoms,
std::ostream& os,
- std::ostream& paren);
+ std::ostream& paren) override;
void printAtomMapping(const std::set<Node>& atoms,
std::ostream& os,
std::ostream& paren,
- ProofLetMap &letMap);
+ ProofLetMap& letMap) override;
void printClause(const prop::SatClause& clause,
std::ostream& os,
- std::ostream& paren);
+ std::ostream& paren) override;
void printCnfProofForClause(ClauseId id,
const prop::SatClause* clause,
std::ostream& os,
- std::ostream& paren);
+ std::ostream& paren) override;
};/* class LFSCCnfProof */
} /* CVC4 namespace */
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 4ed2360c2..19a8d30cf 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -396,13 +396,15 @@ class LFSCSatProof : public TSatProof<SatSolver> {
LFSCSatProof(SatSolver* solver, context::Context* context,
const std::string& name, bool checkRes = false)
: TSatProof<SatSolver>(solver, context, name, checkRes) {}
- virtual void printResolution(ClauseId id, std::ostream& out,
- std::ostream& paren);
- virtual void printResolutions(std::ostream& out, std::ostream& paren);
- virtual void printResolutionEmptyClause(std::ostream& out,
- std::ostream& paren);
- virtual void printAssumptionsResolution(ClauseId id, std::ostream& out,
- std::ostream& paren);
+ void printResolution(ClauseId id,
+ std::ostream& out,
+ std::ostream& paren) override;
+ void printResolutions(std::ostream& out, std::ostream& paren) override;
+ void printResolutionEmptyClause(std::ostream& out,
+ std::ostream& paren) override;
+ void printAssumptionsResolution(ClauseId id,
+ std::ostream& out,
+ std::ostream& paren) override;
}; /* class LFSCSatProof */
template <class Solver>
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 15ac533b7..4e599f570 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -163,23 +163,32 @@ public:
LFSCTheoryProofEngine()
: TheoryProofEngine() {}
- void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map);
+ void printTheoryTerm(Expr term,
+ std::ostream& os,
+ const ProofLetMap& map) override;
- void registerTermsFromAssertions();
+ void registerTermsFromAssertions() override;
void printSortDeclarations(std::ostream& os, std::ostream& paren);
void printTermDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map);
- virtual void printLetTerm(Expr term, std::ostream& os);
- virtual void printBoundTerm(Expr term, std::ostream& os, const ProofLetMap& map);
- virtual void printAssertions(std::ostream& os, std::ostream& paren);
- virtual void printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, std::ostream& paren);
- virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
- virtual void printTheoryLemmas(const IdToSatClause& lemmas,
- std::ostream& os,
+ void printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map);
+ void printLetTerm(Expr term, std::ostream& os) override;
+ void printBoundTerm(Expr term,
+ std::ostream& os,
+ const ProofLetMap& map) override;
+ void printAssertions(std::ostream& os, std::ostream& paren) override;
+ void printLemmaRewrites(NodePairSet& rewrites,
+ std::ostream& os,
+ std::ostream& paren);
+ void printDeferredDeclarations(std::ostream& os,
+ std::ostream& paren) override;
+ void printAliasingDeclarations(std::ostream& os,
std::ostream& paren,
- ProofLetMap& map);
- virtual void printSort(Type type, std::ostream& os);
+ const ProofLetMap& globalLetMap) override;
+ void printTheoryLemmas(const IdToSatClause& lemmas,
+ std::ostream& os,
+ std::ostream& paren,
+ ProofLetMap& map) override;
+ void printSort(Type type, std::ostream& os) override;
void performExtraRegistrations();
@@ -307,16 +316,7 @@ protected:
public:
BooleanProof(TheoryProofEngine* proofEngine);
- virtual void registerTerm(Expr term);
-
- virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
-
- virtual void printOwnedSort(Type type, std::ostream& os) = 0;
- virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) = 0;
- virtual void printSortDeclarations(std::ostream& os, std::ostream& paren) = 0;
- virtual void printTermDeclarations(std::ostream& os, std::ostream& paren) = 0;
- virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
- virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) = 0;
+ void registerTerm(Expr term) override;
};
class LFSCBooleanProof : public BooleanProof {
@@ -324,16 +324,27 @@ public:
LFSCBooleanProof(TheoryProofEngine* proofEngine)
: BooleanProof(proofEngine)
{}
- virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
- virtual void printOwnedSort(Type type, std::ostream& os);
- virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
- virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
+ void printOwnedTerm(Expr term,
+ std::ostream& os,
+ const ProofLetMap& map) override;
+ void printOwnedSort(Type type, std::ostream& os) override;
+ void printTheoryLemmaProof(std::vector<Expr>& lemma,
+ std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& map) override;
+ void printSortDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printTermDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printDeferredDeclarations(std::ostream& os,
+ std::ostream& paren) override;
+ void printAliasingDeclarations(std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& globalLetMap) override;
- bool printsAsBool(const Node &n);
- void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
+ bool printsAsBool(const Node& n) override;
+ void printConstantDisequalityProof(std::ostream& os,
+ Expr c1,
+ Expr c2,
+ const ProofLetMap& globalLetMap) override;
};
} /* CVC4 namespace */
diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h
index 1b14bd15f..7aa00cc35 100644
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -66,7 +66,7 @@ protected:
public:
UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine);
- virtual void registerTerm(Expr term);
+ void registerTerm(Expr term) override;
};
class LFSCUFProof : public UFProof {
@@ -74,17 +74,28 @@ public:
LFSCUFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine)
: UFProof(uf, proofEngine)
{}
- virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
- virtual void printOwnedSort(Type type, std::ostream& os);
- virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
- virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
-
- bool printsAsBool(const Node &n);
-
- void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
+ void printOwnedTerm(Expr term,
+ std::ostream& os,
+ const ProofLetMap& map) override;
+ void printOwnedSort(Type type, std::ostream& os) override;
+ void printTheoryLemmaProof(std::vector<Expr>& lemma,
+ std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& map) override;
+ void printSortDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printTermDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printDeferredDeclarations(std::ostream& os,
+ std::ostream& paren) override;
+ void printAliasingDeclarations(std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& globalLetMap) override;
+
+ bool printsAsBool(const Node& n) override;
+
+ void printConstantDisequalityProof(std::ostream& os,
+ Expr c1,
+ Expr c2,
+ const ProofLetMap& globalLetMap) override;
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback