summaryrefslogtreecommitdiff
path: root/src/proof/proof_manager.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/proof_manager.h')
-rw-r--r--src/proof/proof_manager.h6
1 files changed, 6 insertions, 0 deletions
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 89aa66c2d..0342288fe 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -239,6 +239,12 @@ public:
// for SMT variable names that have spaces and other things
static std::string sanitize(TNode var);
+ // wrap term with (p_app ... ) if the term is printed as a boolean, and print
+ // used for "trust" assertions
+ static void printTrustedTerm(Node term,
+ std::ostream& os,
+ ProofLetMap& globalLetMap);
+
/** Add proof assertion - unlike addCoreAssertion this is post definition expansion **/
void addAssertion(Expr formula);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback