diff options
Diffstat (limited to 'src/proof/proof_manager.h')
-rw-r--r-- | src/proof/proof_manager.h | 6 |
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); |