ExpandDefs::ExpandDefs(SmtEngine& smt,
ResourceManager& rm,
SmtEngineStatistics& stats)
- : d_smt(smt), d_resourceManager(rm), d_smtStats(stats)
+ : d_smt(smt), d_resourceManager(rm), d_smtStats(stats), d_tpg(nullptr)
{
}
std::unordered_map<Node, Node, NodeHashFunction>& cache,
bool expandOnly)
{
+ TrustNode trn = expandDefinitions(n, cache, expandOnly, nullptr);
+ return trn.isNull() ? Node(n) : trn.getNode();
+}
+
+TrustNode ExpandDefs::expandDefinitions(
+ TNode n,
+ std::unordered_map<Node, Node, NodeHashFunction>& cache,
+ bool expandOnly,
+ TConvProofGenerator* tpg)
+{
+ const TNode orig = n;
NodeManager* nm = d_smt.getNodeManager();
std::stack<std::tuple<Node, Node, bool>> worklist;
std::stack<Node> result;
if (i != dfuns->end())
{
Node f = (*i).second.getFormula();
- // must expand its definition
- Node fe = expandDefinitions(f, cache, expandOnly);
+ const std::vector<Node>& formals = (*i).second.getFormals();
// replacement must be closed
- if ((*i).second.getFormals().size() > 0)
+ if (!formals.empty())
+ {
+ f = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, formals), f);
+ }
+ // are we are producing proofs for this call?
+ if (tpg != nullptr)
{
- result.push(
- nm->mkNode(LAMBDA,
- nm->mkNode(BOUND_VAR_LIST, (*i).second.getFormals()),
- fe));
- continue;
+ // if this is a variable, we can simply assume it
+ // ------- ASSUME
+ // n = f
+ Node conc = n.eqNode(f);
+ tpg->addRewriteStep(n, f, PfRule::ASSUME, {}, {conc});
}
+ // must recursively expand its definition
+ TrustNode tfe = expandDefinitions(f, cache, expandOnly, tpg);
+ Node fe = tfe.isNull() ? f : tfe.getNode();
// don't bother putting in the cache
result.push(fe);
continue;
doExpand = d_smt.isDefinedFunction(n.getOperator().toExpr());
}
}
+ // the premise of the proof of expansion (if we are expanding a definition
+ // and proofs are enabled)
+ std::vector<Node> pfExpChildren;
if (doExpand)
{
std::vector<Node> formals;
}
fm = def.getFormula();
+ // are we producing proofs for this call?
+ if (tpg != nullptr)
+ {
+ Node pfRhs = fm;
+ if (!formals.empty())
+ {
+ Node bvl = nm->mkNode(BOUND_VAR_LIST, formals);
+ pfRhs = nm->mkNode(LAMBDA, bvl, pfRhs);
+ }
+ Assert(func.getType().isComparableTo(pfRhs.getType()));
+ pfExpChildren.push_back(func.eqNode(pfRhs));
+ }
}
Node instance = fm.substitute(formals.begin(),
n.begin(),
n.begin() + formals.size());
Debug("expand") << "made : " << instance << std::endl;
-
- Node expanded = expandDefinitions(instance, cache, expandOnly);
- cache[n] = (n == expanded ? Node::null() : expanded);
+ // are we producing proofs for this call?
+ if (tpg != nullptr)
+ {
+ if (n != instance)
+ {
+ // This code is run both when we are doing expand definitions and
+ // simple beta reduction.
+ //
+ // f = (lambda ((x T)) t) [if we are expanding a definition]
+ // ---------------------- MACRO_SR_PRED_INTRO
+ // n = instance
+ Node conc = n.eqNode(instance);
+ tpg->addRewriteStep(n,
+ instance,
+ PfRule::MACRO_SR_PRED_INTRO,
+ pfExpChildren,
+ {conc});
+ }
+ }
+ // now, call expand definitions again on the result
+ TrustNode texp = expandDefinitions(instance, cache, expandOnly, tpg);
+ Node expanded = texp.isNull() ? instance : texp.getNode();
+ cache[n] = n == expanded ? Node::null() : expanded;
result.push(expanded);
continue;
}
Assert(t != NULL);
TrustNode trn = t->expandDefinition(n);
- node = trn.isNull() ? Node(n) : trn.getNode();
+ if (!trn.isNull())
+ {
+ node = trn.getNode();
+ if (tpg != nullptr)
+ {
+ tpg->addRewriteStep(
+ n, node, trn.getGenerator(), PfRule::THEORY_EXPAND_DEF);
+ }
+ }
+ else
+ {
+ node = n;
+ }
}
// the partial functions can fall through, in which case we still
AlwaysAssert(result.size() == 1);
- return result.top();
+ Node res = result.top();
+
+ if (res == orig)
+ {
+ return TrustNode::null();
+ }
+ return TrustNode::mkTrustRewrite(orig, res, tpg);
}
void ExpandDefs::expandAssertions(AssertionPipeline& assertions,
bool expandOnly)
{
Chat() << "expanding definitions in assertions..." << std::endl;
- Trace("simplify") << "ExpandDefs::simplify(): expanding definitions"
+ Trace("exp-defs") << "ExpandDefs::simplify(): expanding definitions"
<< std::endl;
TimerStat::CodeTimer codeTimer(d_smtStats.d_definitionExpansionTime);
std::unordered_map<Node, Node, NodeHashFunction> cache;
for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i)
{
Node assert = assertions[i];
- Node expd = expandDefinitions(assert, cache, expandOnly);
- if (expd != assert)
+ // notice we call this method with only one value of expandOnly currently,
+ // hence we maintain only a single set of proof steps in d_tpg.
+ TrustNode expd = expandDefinitions(assert, cache, expandOnly, d_tpg.get());
+ if (!expd.isNull())
{
- assertions.replace(i, expd);
+ Trace("exp-defs") << "ExpandDefs::expandAssertions: " << assert << " -> "
+ << expd.getNode() << std::endl;
+ assertions.replaceTrusted(i, expd);
}
}
}
+void ExpandDefs::setProofNodeManager(ProofNodeManager* pnm)
+{
+ if (d_tpg == nullptr)
+ {
+ d_tpg.reset(new TConvProofGenerator(pnm,
+ d_smt.getUserContext(),
+ TConvPolicy::FIXPOINT,
+ TConvCachePolicy::NEVER,
+ "ExpandDefs::TConvProofGenerator",
+ nullptr,
+ true));
+ }
+}
+
} // namespace smt
} // namespace CVC4
#include <unordered_map>
#include "expr/node.h"
+#include "expr/term_conversion_proof_generator.h"
#include "preprocessing/assertion_pipeline.h"
#include "smt/smt_engine_stats.h"
#include "util/resource_manager.h"
void expandAssertions(preprocessing::AssertionPipeline& assertions,
bool expandOnly = false);
+ /**
+ * Set proof node manager, which signals this class to enable proofs using the
+ * given proof node manager.
+ */
+ void setProofNodeManager(ProofNodeManager* pnm);
+
private:
+ /**
+ * Helper function for above, called to specify if we want proof production
+ * based on the optional argument tpg.
+ */
+ theory::TrustNode expandDefinitions(
+ TNode n,
+ std::unordered_map<Node, Node, NodeHashFunction>& cache,
+ bool expandOnly,
+ TConvProofGenerator* tpg);
/** Reference to the SMT engine */
SmtEngine& d_smt;
/** Reference to resource manager */
ResourceManager& d_resourceManager;
/** Reference to the SMT stats */
SmtEngineStatistics& d_smtStats;
+ /** A proof generator for the term conversion. */
+ std::unique_ptr<TConvProofGenerator> d_tpg;
};
} // namespace smt
pc->registerTrustedChecker(PfRule::PREPROCESS_LEMMA, this, 3);
pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS, this, 3);
pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS_LEMMA, this, 3);
+ pc->registerTrustedChecker(PfRule::THEORY_EXPAND_DEF, this, 3);
pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 3);
pc->registerTrustedChecker(PfRule::TRUST_REWRITE, this, 1);
pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1);
- pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 3);
+ pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1);
}
Node BuiltinProofRuleChecker::applySubstitutionRewrite(
else if (id == PfRule::MACRO_SR_PRED_INTRO)
{
Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
- << args.size() << std::endl;
+ << args[0] << std::endl;
Assert(1 <= args.size() && args.size() <= 3);
MethodId ids, idr;
if (!getMethodIds(args, ids, idr, 1))
{
return Node::null();
}
+ Trace("builtin-pfcheck") << "Result is " << res << std::endl;
+ Trace("builtin-pfcheck") << "Witness form is "
+ << SkolemManager::getWitnessForm(res) << std::endl;
// **** NOTE: can rewrite the witness form here. This enables certain lemmas
// to be provable, e.g. (= k t) where k is a purification Skolem for t.
res = Rewriter::rewrite(SkolemManager::getWitnessForm(res));
<< "Failed to rewrite to true, res=" << res << std::endl;
return Node::null();
}
+ Trace("builtin-pfcheck") << "...success" << std::endl;
return args[0];
}
else if (id == PfRule::MACRO_SR_PRED_ELIM)
Assert(args.size() == 1);
return RemoveTermFormulas::getAxiomFor(args[0]);
}
- else if (id == PfRule::PREPROCESS || id == PfRule::THEORY_PREPROCESS
- || id == PfRule::WITNESS_AXIOM || id == PfRule::THEORY_LEMMA
- || id == PfRule::PREPROCESS_LEMMA || id == PfRule::THEORY_REWRITE
- || id == PfRule::TRUST_REWRITE || id == PfRule::TRUST_SUBS
- || id == PfRule::TRUST_SUBS_MAP)
+ else if (id == PfRule::PREPROCESS || id == PfRule::PREPROCESS_LEMMA
+ || id == PfRule::THEORY_PREPROCESS
+ || id == PfRule::THEORY_PREPROCESS_LEMMA
+ || id == PfRule::THEORY_EXPAND_DEF || id == PfRule::WITNESS_AXIOM
+ || id == PfRule::THEORY_LEMMA || id == PfRule::THEORY_REWRITE
+ || id == PfRule::TRUST_SUBS || id == PfRule::TRUST_SUBS_MAP)
{
// "trusted" rules
Assert(children.empty());
Assert(args[0].getType().isBoolean());
return args[0];
}
+
// no rule
return Node::null();
}
projects / cvc5.git / commitdiff