From 5aa585b74682a7e92a188548ce582eeb1212e42b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 23 Nov 2020 10:23:00 -0600 Subject: (proof-new) Miscellaneous changes from proof-new (#5445) --- src/expr/term_conversion_proof_generator.cpp | 4 +++- src/expr/type_node.cpp | 4 +--- src/smt/preprocessor.cpp | 1 + 3 files changed, 5 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp index 02613345f..858ca9f64 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/expr/term_conversion_proof_generator.cpp @@ -138,7 +138,9 @@ Node TConvProofGenerator::registerRewriteStep(Node t, Node s, uint32_t tctx) // should not rewrite term to two different things if (!getRewriteStepInternal(thash).isNull()) { - Assert(getRewriteStepInternal(thash) == s); + Assert(getRewriteStepInternal(thash) == s) + << identify() << " rewriting " << t << " to both " << s << " and " + << getRewriteStepInternal(thash); return Node::null(); } d_rewriteMap[thash] = s; diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 0818ca8c1..49fbe73ef 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -589,13 +589,11 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { case kind::SEQUENCE_TYPE: case kind::SET_TYPE: case kind::BAG_TYPE: + case kind::SEXPR_TYPE: { // we don't support subtyping except for built in types Int and Real. return TypeNode(); // return null type } - case kind::SEXPR_TYPE: - Unimplemented() - << "haven't implemented leastCommonType for symbolic expressions yet"; default: Unimplemented() << "don't have a commonType for types `" << t0 << "' and `" << t1 << "'"; diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 98a2a7a36..5a1ce63a4 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -158,6 +158,7 @@ void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg) { Assert(pppg != nullptr); d_pnm = pppg->getManager(); + d_propagator.setProof(d_pnm, d_context, pppg); d_rtf.setProofNodeManager(d_pnm); } -- cgit v1.2.3