summaryrefslogtreecommitdiff
path: root/src/proof/theory_proof.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/theory_proof.h')
-rw-r--r--src/proof/theory_proof.h127
1 files changed, 91 insertions, 36 deletions
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index d14704760..b04dd4c60 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -39,14 +39,14 @@ struct LetCount {
static unsigned counter;
static void resetCounter() { counter = 0; }
static unsigned newId() { return ++counter; }
-
+
unsigned count;
unsigned id;
LetCount()
: count(0)
, id(-1)
{}
-
+
void increment() { ++count; }
LetCount(unsigned i)
: count(1)
@@ -65,7 +65,7 @@ struct LetCount {
count = rhs.count;
return *this;
}
-};
+};
struct LetOrderElement {
Expr expr;
@@ -84,7 +84,7 @@ struct LetOrderElement {
typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause;
typedef __gnu_cxx::hash_map<Expr, LetCount, ExprHashFunction> LetMap;
-typedef std::vector<LetOrderElement> Bindings;
+typedef std::vector<LetOrderElement> Bindings;
class TheoryProof;
@@ -124,6 +124,14 @@ public:
virtual void printSort(Type type, std::ostream& os) = 0;
/**
+ * Go over the assertions and register all terms with the theories.
+ *
+ * @param os
+ * @param paren closing parenthesis
+ */
+ virtual void registerTermsFromAssertions() = 0;
+
+ /**
* Print the theory assertions (arbitrary formulas over
* theory atoms)
*
@@ -131,6 +139,14 @@ public:
* @param paren closing parenthesis
*/
virtual void printAssertions(std::ostream& os, std::ostream& paren) = 0;
+ /**
+ * Print variable declarations that need to appear within the proof,
+ * e.g. skolemized variables.
+ *
+ * @param os
+ * @param paren closing parenthesis
+ */
+ virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
/**
* Print proofs of all the theory lemmas (must prove
@@ -168,11 +184,14 @@ public:
LFSCTheoryProofEngine()
: TheoryProofEngine() {}
- void printDeclarations(std::ostream& os, std::ostream& paren);
+ void registerTermsFromAssertions();
+ 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 LetMap& map);
virtual void printLetTerm(Expr term, std::ostream& os);
virtual void printBoundTerm(Expr term, std::ostream& os, const LetMap& map);
virtual void printAssertions(std::ostream& os, std::ostream& paren);
+ virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
virtual void printTheoryLemmas(const IdToSatClause& lemmas,
std::ostream& os,
std::ostream& paren);
@@ -189,41 +208,74 @@ public:
: d_theory(th)
, d_proofEngine(proofEngine)
{}
- virtual ~TheoryProof() {};
- /**
- * Print a term belonging to this theory.
- *
+ virtual ~TheoryProof() {};
+ /**
+ * Print a term belonging some theory, not neccessarily this one.
+ *
* @param term expresion representing term
* @param os output stream
*/
- virtual void printTerm(Expr term, std::ostream& os, const LetMap& map) = 0;
- /**
- * Print the proof representation of the given type.
- *
- * @param type
- * @param os
+ void printTerm(Expr term, std::ostream& os, const LetMap& map) {
+ d_proofEngine->printBoundTerm(term, os, map);
+ }
+ /**
+ * Print a term belonging to THIS theory.
+ *
+ * @param term expresion representing term
+ * @param os output stream
+ */
+ virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) = 0;
+ /**
+ * Print the proof representation of the given type that belongs to some theory.
+ *
+ * @param type
+ * @param os
*/
- virtual void printSort(Type type, std::ostream& os) = 0;
- /**
+ void printSort(Type type, std::ostream& os) {
+ d_proofEngine->printSort(type, os);
+ }
+ /**
+ * Print the proof representation of the given type that belongs to THIS theory.
+ *
+ * @param type
+ * @param os
+ */
+ virtual void printOwnedSort(Type type, std::ostream& os) = 0;
+ /**
* Print a proof for the theory lemmas. Must prove
* clause representing lemmas to be used in resolution proof.
- *
+ *
* @param os output stream
*/
virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
- /**
- * Print the variable/sorts declarations for this theory.
- *
- * @param os
- * @param paren
+ /**
+ * Print the sorts declarations for this theory.
+ *
+ * @param os
+ * @param paren
*/
- virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 0;
- /**
+ virtual void printSortDeclarations(std::ostream& os, std::ostream& paren) = 0;
+ /**
+ * Print the term declarations for this theory.
+ *
+ * @param os
+ * @param paren
+ */
+ virtual void printTermDeclarations(std::ostream& os, std::ostream& paren) = 0;
+ /**
+ * Print any deferred variable/sorts declarations for this theory
+ * (those that need to appear inside the actual proof).
+ *
+ * @param os
+ * @param paren
+ */
+ virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
+ /**
* Register a term of this theory that appears in the proof.
- *
- * @param term
+ *
+ * @param term
*/
- virtual void registerTerm(Expr term) = 0;
+ virtual void registerTerm(Expr term) = 0;
};
class BooleanProof : public TheoryProof {
@@ -233,12 +285,14 @@ public:
BooleanProof(TheoryProofEngine* proofEngine);
virtual void registerTerm(Expr term);
-
- virtual void printTerm(Expr term, std::ostream& os, const LetMap& map) = 0;
- virtual void printSort(Type type, std::ostream& os) = 0;
+ virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) = 0;
+
+ virtual void printOwnedSort(Type type, std::ostream& os) = 0;
virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) = 0;
- virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 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;
};
class LFSCBooleanProof : public BooleanProof {
@@ -246,13 +300,14 @@ public:
LFSCBooleanProof(TheoryProofEngine* proofEngine)
: BooleanProof(proofEngine)
{}
- virtual void printTerm(Expr term, std::ostream& os, const LetMap& map);
- virtual void printSort(Type type, std::ostream& os);
+ virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
+ virtual void printOwnedSort(Type type, std::ostream& os);
virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
- virtual void printDeclarations(std::ostream& os, std::ostream& paren);
+ 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);
};
-
} /* CVC4 namespace */
#endif /* __CVC4__THEORY_PROOF_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback