diff options
Diffstat (limited to 'src/smt/witness_form.cpp')
-rw-r--r-- | src/smt/witness_form.cpp | 128 |
1 files changed, 128 insertions, 0 deletions
diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp new file mode 100644 index 000000000..891c0f731 --- /dev/null +++ b/src/smt/witness_form.cpp @@ -0,0 +1,128 @@ +/********************* */ +/*! \file witness_form.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The module for managing witness form conversion in proofs + **/ + +#include "smt/witness_form.h" + +#include "expr/skolem_manager.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace smt { + +WitnessFormGenerator::WitnessFormGenerator(ProofNodeManager* pnm) + : d_tcpg(pnm), d_wintroPf(pnm) +{ +} + +std::shared_ptr<ProofNode> WitnessFormGenerator::getProofFor(Node eq) +{ + if (eq.getKind() != kind::EQUAL) + { + // expecting an equality + return nullptr; + } + Node lhs = eq[0]; + Node rhs = convertToWitnessForm(eq[0]); + if (rhs != eq[1]) + { + // expecting witness form + return nullptr; + } + std::shared_ptr<ProofNode> pn = d_tcpg.getProofFor(eq); + Assert(pn != nullptr); + return pn; +} + +std::string WitnessFormGenerator::identify() const +{ + return "WitnessFormGenerator"; +} + +Node WitnessFormGenerator::convertToWitnessForm(Node t) +{ + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* skm = nm->getSkolemManager(); + Node tw = SkolemManager::getWitnessForm(t); + if (t == tw) + { + // trivial case + return tw; + } + std::unordered_set<TNode, TNodeHashFunction>::iterator it; + std::vector<TNode> visit; + TNode cur; + TNode curw; + visit.push_back(t); + do + { + cur = visit.back(); + visit.pop_back(); + it = d_visited.find(cur); + if (it == d_visited.end()) + { + d_visited.insert(cur); + curw = SkolemManager::getWitnessForm(cur); + // if its witness form is different + if (cur != curw) + { + if (cur.isVar()) + { + Node eq = cur.eqNode(curw); + // equality between a variable and its witness form + d_eqs.insert(eq); + Assert(curw.getKind() == kind::WITNESS); + Node skBody = SkolemManager::getSkolemForm(curw[1]); + Node exists = nm->mkNode(kind::EXISTS, curw[0], skBody); + ProofGenerator* pg = skm->getProofGenerator(exists); + // --------------------------- from pg + // (exists ((x T)) (P x)) + // --------------------------- WITNESS_INTRO + // k = (witness ((x T)) (P x)) + d_wintroPf.addLazyStep(exists, pg, false, PfRule::WITNESS_AXIOM); + d_wintroPf.addStep(eq, PfRule::WITNESS_INTRO, {exists}, {}); + d_tcpg.addRewriteStep(cur, curw, &d_wintroPf); + } + else + { + // A term whose witness form is different from itself, recurse. + // It should be the case that cur has children, since the witness + // form of constants are themselves. + Assert(cur.getNumChildren() > 0); + visit.insert(visit.end(), cur.begin(), cur.end()); + } + } + } + } while (!visit.empty()); + return tw; +} + +bool WitnessFormGenerator::requiresWitnessFormTransform(Node t, Node s) const +{ + return theory::Rewriter::rewrite(t) != theory::Rewriter::rewrite(s); +} + +bool WitnessFormGenerator::requiresWitnessFormIntro(Node t) const +{ + Node tr = theory::Rewriter::rewrite(t); + return !tr.isConst() || !tr.getConst<bool>(); +} + +const std::unordered_set<Node, NodeHashFunction>& +WitnessFormGenerator::getWitnessFormEqs() const +{ + return d_eqs; +} + +} // namespace smt +} // namespace CVC4 |