diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-24 13:51:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-24 15:51:09 -0300 |
commit | bd33d20609999f6f847aeb63a42350aeb3041406 (patch) | |
tree | 8b4a3ccb0ab48b65bd70222dbfd572de8743bcd9 /src/expr | |
parent | 1516e3b5d9436be86841a52002fc728fcd52dd34 (diff) |
Move proof utilities to src/proof/ (#6611)
This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/.
It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term").
Diffstat (limited to 'src/expr')
34 files changed, 0 insertions, 7650 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 9bf63dcfc..094c7bcbd 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -24,8 +24,6 @@ libcvc5_add_sources( attribute_unique_id.h bound_var_manager.cpp bound_var_manager.h - buffered_proof_generator.cpp - buffered_proof_generator.h emptyset.cpp emptyset.h emptybag.cpp @@ -33,10 +31,6 @@ libcvc5_add_sources( expr_iomanip.cpp expr_iomanip.h kind_map.h - lazy_proof.cpp - lazy_proof.h - lazy_proof_chain.cpp - lazy_proof_chain.h match_trie.cpp match_trie.h node.cpp @@ -58,37 +52,12 @@ libcvc5_add_sources( sequence.cpp sequence.h node_visitor.h - proof.cpp - proof.h - proof_checker.cpp - proof_checker.h - proof_ensure_closed.cpp - proof_ensure_closed.h - proof_generator.cpp - proof_generator.h - proof_node.cpp - proof_node.h - proof_node_algorithm.cpp - proof_node_algorithm.h - proof_node_to_sexpr.cpp - proof_node_to_sexpr.h - proof_node_manager.cpp - proof_node_manager.h - proof_node_updater.cpp - proof_node_updater.h - proof_rule.cpp - proof_rule.h - proof_set.h - proof_step_buffer.cpp - proof_step_buffer.h skolem_manager.cpp skolem_manager.h symbol_manager.cpp symbol_manager.h symbol_table.cpp symbol_table.h - tconv_seq_proof_generator.cpp - tconv_seq_proof_generator.h term_canonize.cpp term_canonize.h term_context.cpp @@ -97,8 +66,6 @@ libcvc5_add_sources( term_context_node.h term_context_stack.cpp term_context_stack.h - term_conversion_proof_generator.cpp - term_conversion_proof_generator.h type_checker.h type_matcher.cpp type_matcher.h diff --git a/src/expr/buffered_proof_generator.cpp b/src/expr/buffered_proof_generator.cpp deleted file mode 100644 index 2cbbd7e91..000000000 --- a/src/expr/buffered_proof_generator.cpp +++ /dev/null @@ -1,103 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Haniel Barbosa - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of a proof generator for buffered proof steps. - */ - -#include "expr/buffered_proof_generator.h" - -#include "expr/proof.h" -#include "expr/proof_node_manager.h" - -namespace cvc5 { - -BufferedProofGenerator::BufferedProofGenerator(context::Context* c, - ProofNodeManager* pnm) - : ProofGenerator(), d_facts(c), d_pnm(pnm) -{ -} - -bool BufferedProofGenerator::addStep(Node fact, - ProofStep ps, - CDPOverwrite opolicy) -{ - // check duplicates if we are not always overwriting - if (opolicy != CDPOverwrite::ALWAYS) - { - if (d_facts.find(fact) != d_facts.end()) - { - // duplicate - return false; - } - Node symFact = CDProof::getSymmFact(fact); - if (!symFact.isNull()) - { - if (d_facts.find(symFact) != d_facts.end()) - { - // duplicate due to symmetry - return false; - } - } - } - // note that this replaces the value fact is mapped to if there is already one - d_facts.insert(fact, std::make_shared<ProofStep>(ps)); - return true; -} - -std::shared_ptr<ProofNode> BufferedProofGenerator::getProofFor(Node fact) -{ - Trace("pfee-fact-gen") << "BufferedProofGenerator::getProofFor: " << fact - << std::endl; - NodeProofStepMap::iterator it = d_facts.find(fact); - if (it == d_facts.end()) - { - Node symFact = CDProof::getSymmFact(fact); - if (symFact.isNull()) - { - Trace("pfee-fact-gen") << "...cannot find step" << std::endl; - Assert(false); - return nullptr; - } - it = d_facts.find(symFact); - if (it == d_facts.end()) - { - Assert(false); - Trace("pfee-fact-gen") << "...cannot find step (no sym)" << std::endl; - return nullptr; - } - } - Trace("pfee-fact-gen") << "...return via step " << *(*it).second << std::endl; - CDProof cdp(d_pnm); - cdp.addStep(fact, *(*it).second); - return cdp.getProofFor(fact); -} - -bool BufferedProofGenerator::hasProofFor(Node f) -{ - NodeProofStepMap::iterator it = d_facts.find(f); - if (it == d_facts.end()) - { - Node symFact = CDProof::getSymmFact(f); - if (symFact.isNull()) - { - return false; - } - it = d_facts.find(symFact); - if (it == d_facts.end()) - { - return false; - } - } - return true; -} - -} // namespace cvc5 diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h deleted file mode 100644 index 2e1ef6c53..000000000 --- a/src/expr/buffered_proof_generator.h +++ /dev/null @@ -1,64 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Haniel Barbosa, Andrew Reynolds, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * A proof generator for buffered proof steps. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H -#define CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H - -#include "context/cdhashmap.h" -#include "expr/proof_generator.h" - -namespace cvc5 { - -class ProofNodeManager; -class ProofStep; - -/** - * The proof generator for buffered steps. This class is a context-dependent - * mapping from formulas to proof steps. It does not generate ProofNodes until it - * is asked to provide a proof for a given fact. - */ -class BufferedProofGenerator : public ProofGenerator -{ - typedef context::CDHashMap<Node, std::shared_ptr<ProofStep>> NodeProofStepMap; - - public: - BufferedProofGenerator(context::Context* c, ProofNodeManager* pnm); - ~BufferedProofGenerator() {} - /** add step - * Unless the overwrite policy is ALWAYS it does not replace previously - * registered steps (modulo (dis)equality symmetry). - */ - bool addStep(Node fact, - ProofStep ps, - CDPOverwrite opolicy = CDPOverwrite::NEVER); - /** Get proof for. It is robust to (dis)equality symmetry. */ - std::shared_ptr<ProofNode> getProofFor(Node f) override; - /** Whether a step has been registered for f. */ - bool hasProofFor(Node f) override; - /** identify */ - std::string identify() const override { return "BufferedProofGenerator"; } - - private: - /** maps expected to ProofStep */ - NodeProofStepMap d_facts; - /** the proof node manager */ - ProofNodeManager* d_pnm; -}; - -} // namespace cvc5 - -#endif /* CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H */ diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp deleted file mode 100644 index 8a54637fa..000000000 --- a/src/expr/lazy_proof.cpp +++ /dev/null @@ -1,232 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Aina Niemetz - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of lazy proof utility. - */ - -#include "expr/lazy_proof.h" - -#include "expr/proof_ensure_closed.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" - -using namespace cvc5::kind; - -namespace cvc5 { - -LazyCDProof::LazyCDProof(ProofNodeManager* pnm, - ProofGenerator* dpg, - context::Context* c, - std::string name) - : CDProof(pnm, c, name), d_gens(c ? c : &d_context), d_defaultGen(dpg) -{ -} - -LazyCDProof::~LazyCDProof() {} - -std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact) -{ - Trace("lazy-cdproof") << "LazyCDProof::mkLazyProof " << fact << std::endl; - // make the proof, which should always be non-null, since we construct an - // assumption in the worst case. - std::shared_ptr<ProofNode> opf = CDProof::getProofFor(fact); - Assert(opf != nullptr); - if (!hasGenerators()) - { - Trace("lazy-cdproof") << "...no generators, finished" << std::endl; - // optimization: no generators, we are done - return opf; - } - // otherwise, we traverse the proof opf and fill in the ASSUME leafs that - // have generators - std::unordered_set<ProofNode*> visited; - std::unordered_set<ProofNode*>::iterator it; - std::vector<ProofNode*> visit; - ProofNode* cur; - visit.push_back(opf.get()); - do - { - cur = visit.back(); - visit.pop_back(); - it = visited.find(cur); - - if (it == visited.end()) - { - visited.insert(cur); - Node cfact = cur->getResult(); - if (getProof(cfact).get() != cur) - { - // We don't own this proof, skip it. This is to ensure that this method - // is idempotent, since it may be the case that a previous call to - // getProofFor connected a proof from a proof generator as a child of - // a ProofNode in the range of the map in CDProof. Thus, this ensures - // we don't touch such proofs. - Trace("lazy-cdproof") << "...skip unowned proof" << std::endl; - } - else if (cur->getRule() == PfRule::ASSUME) - { - bool isSym = false; - ProofGenerator* pg = getGeneratorFor(cfact, isSym); - if (pg != nullptr) - { - Trace("lazy-cdproof") - << "LazyCDProof: Call generator " << pg->identify() - << " for assumption " << cfact << std::endl; - Node cfactGen = isSym ? CDProof::getSymmFact(cfact) : cfact; - Assert(!cfactGen.isNull()); - // Do not use the addProofTo interface, instead use the update node - // interface, since this ensures that we don't take ownership for - // the current proof. Instead, it is only linked, and ignored on - // future calls to getProofFor due to the check above. - std::shared_ptr<ProofNode> pgc = pg->getProofFor(cfactGen); - // If the proof was null, then the update is not performed. This is - // not considered an error, since this behavior is equivalent to - // if pg had provided the proof (ASSUME cfactGen). Ensuring the - // proper behavior wrt closed proofs should be done outside this - // method. - if (pgc != nullptr) - { - Trace("lazy-cdproof-gen") - << "LazyCDProof: stored proof: " << *pgc.get() << std::endl; - - if (isSym) - { - d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {}); - } - else - { - d_manager->updateNode(cur, pgc.get()); - } - Trace("lazy-cdproof") << "LazyCDProof: Successfully added fact for " - << cfactGen << std::endl; - } - } - else - { - Trace("lazy-cdproof") << "LazyCDProof: " << identify() - << " : No generator for " << cfact << std::endl; - } - // Notice that we do not traverse the proofs that have been generated - // lazily by the proof generators here. In other words, we assume that - // the proofs from provided proof generators are final and need - // no further modification by this class. - } - else - { - const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren(); - for (const std::shared_ptr<ProofNode>& cp : cc) - { - visit.push_back(cp.get()); - } - } - } - } while (!visit.empty()); - // we have now updated the ASSUME leafs of opf, return it - Trace("lazy-cdproof") << "...finished" << std::endl; - Assert(opf->getResult() == fact); - return opf; -} - -void LazyCDProof::addLazyStep(Node expected, - ProofGenerator* pg, - PfRule idNull, - bool isClosed, - const char* ctx, - bool forceOverwrite) -{ - if (pg == nullptr) - { - // null generator, should have given a proof rule - if (idNull == PfRule::ASSUME) - { - Unreachable() << "LazyCDProof::addLazyStep: " << identify() - << ": failed to provide proof generator for " << expected; - return; - } - Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected - << " set (trusted) step " << idNull << "\n"; - addStep(expected, idNull, {}, {expected}); - return; - } - Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected - << " set to generator " << pg->identify() << "\n"; - if (!forceOverwrite) - { - NodeProofGeneratorMap::const_iterator it = d_gens.find(expected); - if (it != d_gens.end()) - { - // don't overwrite something that is already there - return; - } - } - // just store now - d_gens.insert(expected, pg); - // debug checking - if (isClosed) - { - Trace("lazy-cdproof-debug") << "Checking closed..." << std::endl; - pfgEnsureClosed(expected, pg, "lazy-cdproof-debug", ctx); - } -} - -ProofGenerator* LazyCDProof::getGeneratorFor(Node fact, - bool& isSym) -{ - isSym = false; - NodeProofGeneratorMap::const_iterator it = d_gens.find(fact); - if (it != d_gens.end()) - { - return (*it).second; - } - Node factSym = CDProof::getSymmFact(fact); - // could be symmetry - if (factSym.isNull()) - { - // can't be symmetry, return the default generator - return d_defaultGen; - } - it = d_gens.find(factSym); - if (it != d_gens.end()) - { - isSym = true; - return (*it).second; - } - // return the default generator - return d_defaultGen; -} - -bool LazyCDProof::hasGenerators() const -{ - return !d_gens.empty() || d_defaultGen != nullptr; -} - -bool LazyCDProof::hasGenerator(Node fact) const -{ - if (d_defaultGen != nullptr) - { - return true; - } - NodeProofGeneratorMap::const_iterator it = d_gens.find(fact); - if (it != d_gens.end()) - { - return true; - } - // maybe there is a symmetric fact? - Node factSym = CDProof::getSymmFact(fact); - if (!factSym.isNull()) - { - it = d_gens.find(factSym); - } - return it != d_gens.end(); -} - -} // namespace cvc5 diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h deleted file mode 100644 index efcda94bd..000000000 --- a/src/expr/lazy_proof.h +++ /dev/null @@ -1,110 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Lazy proof utility. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__EXPR__LAZY_PROOF_H -#define CVC5__EXPR__LAZY_PROOF_H - -#include "expr/proof.h" - -namespace cvc5 { - -class ProofGenerator; -class ProofNodeManager; - -/** - * A (context-dependent) lazy proof. This class is an extension of CDProof - * that additionally maps facts to proof generators in a context-dependent - * manner. It extends CDProof with an additional method, addLazyStep for adding - * steps to a proof via a given proof generator. - */ -class LazyCDProof : public CDProof -{ - public: - /** Constructor - * - * @param pnm The proof node manager for constructing ProofNode objects. - * @param dpg The (optional) default proof generator, which is called - * for facts that have no explicitly provided generator. - * @param c The context that this class depends on. If none is provided, - * this class is context-independent. - */ - LazyCDProof(ProofNodeManager* pnm, - ProofGenerator* dpg = nullptr, - context::Context* c = nullptr, - std::string name = "LazyCDProof"); - ~LazyCDProof(); - /** - * Get lazy proof for fact, or nullptr if it does not exist. This may - * additionally call proof generators to generate proofs for ASSUME nodes that - * don't yet have a concrete proof. - */ - std::shared_ptr<ProofNode> getProofFor(Node fact) override; - /** Add step by generator - * - * This method stores that expected can be proven by proof generator pg if - * it is required to do so. This mapping is maintained in the remainder of - * the current context (according to the context c provided to this class). - * - * It is important to note that pg is asked to provide a proof for expected - * only when no other call for the fact expected is provided via the addStep - * method of this class. In particular, pg is asked to prove expected when it - * appears as the conclusion of an ASSUME leaf within CDProof::getProofFor. - * - * @param expected The fact that can be proven. - * @param pg The generator that can proof expected. - * @param trustId If a null proof generator is provided, we add a step to - * the proof that has trustId as the rule and expected as the sole argument. - * We do this only if trustId is not PfRule::ASSUME. This is primarily used - * for identifying the kind of hole when a proof generator is not given. - * @param isClosed Whether to expect that pg can provide a closed proof for - * this fact. - * @param ctx The context we are in (for debugging). - * @param forceOverwrite If this flag is true, then this call overwrites - * an existing proof generator provided for expected, if one was provided - * via a previous call to addLazyStep in the current context. - */ - void addLazyStep(Node expected, - ProofGenerator* pg, - PfRule trustId = PfRule::ASSUME, - bool isClosed = false, - const char* ctx = "LazyCDProof::addLazyStep", - bool forceOverwrite = false); - /** - * Does this have any proof generators? This method always returns true - * if the default is non-null. - */ - bool hasGenerators() const; - /** Does the given fact have an explicitly provided generator? */ - bool hasGenerator(Node fact) const; - - protected: - typedef context::CDHashMap<Node, ProofGenerator*> NodeProofGeneratorMap; - /** Maps facts that can be proven to generators */ - NodeProofGeneratorMap d_gens; - /** The default proof generator */ - ProofGenerator* d_defaultGen; - /** - * Get generator for fact, or nullptr if it doesnt exist. This method is - * robust to symmetry of (dis)equality. It updates isSym to true if a - * proof generator for the symmetric form of fact was provided. - */ - ProofGenerator* getGeneratorFor(Node fact, bool& isSym); -}; - -} // namespace cvc5 - -#endif /* CVC5__EXPR__LAZY_PROOF_H */ diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp deleted file mode 100644 index 3ce2212be..000000000 --- a/src/expr/lazy_proof_chain.cpp +++ /dev/null @@ -1,327 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Haniel Barbosa, Andrew Reynolds, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of lazy proof utility. - */ - -#include "expr/lazy_proof_chain.h" - -#include "expr/proof.h" -#include "expr/proof_ensure_closed.h" -#include "expr/proof_node.h" -#include "expr/proof_node_algorithm.h" -#include "expr/proof_node_manager.h" -#include "options/proof_options.h" - -namespace cvc5 { - -LazyCDProofChain::LazyCDProofChain(ProofNodeManager* pnm, - bool cyclic, - context::Context* c, - ProofGenerator* defGen, - bool defRec) - : d_manager(pnm), - d_cyclic(cyclic), - d_defRec(defRec), - d_context(), - d_gens(c ? c : &d_context), - d_defGen(defGen) -{ -} - -LazyCDProofChain::~LazyCDProofChain() {} - -const std::map<Node, std::shared_ptr<ProofNode>> LazyCDProofChain::getLinks() - const -{ - std::map<Node, std::shared_ptr<ProofNode>> links; - for (const std::pair<const Node, ProofGenerator* const>& link : d_gens) - { - Assert(link.second); - std::shared_ptr<ProofNode> pfn = link.second->getProofFor(link.first); - Assert(pfn); - links[link.first] = pfn; - } - return links; -} - -std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact) -{ - Trace("lazy-cdproofchain") - << "LazyCDProofChain::getProofFor " << fact << "\n"; - // which facts have had proofs retrieved for. This is maintained to avoid - // cycles. It also saves the proof node of the fact - std::unordered_map<Node, std::shared_ptr<ProofNode>> toConnect; - // leaves of proof node links in the chain, i.e. assumptions, yet to be - // expanded - std::unordered_map<Node, std::vector<std::shared_ptr<ProofNode>>> - assumptionsToExpand; - // invariant of the loop below, the first iteration notwithstanding: - // visit = domain(assumptionsToExpand) \ domain(toConnect) - std::vector<Node> visit{fact}; - std::unordered_map<Node, bool> visited; - Node cur; - do - { - cur = visit.back(); - visit.pop_back(); - auto itVisited = visited.find(cur); - // pre-traversal - if (itVisited == visited.end()) - { - Trace("lazy-cdproofchain") - << "LazyCDProofChain::getProofFor: check " << cur << "\n"; - Assert(toConnect.find(cur) == toConnect.end()); - bool rec = true; - ProofGenerator* pg = getGeneratorForInternal(cur, rec); - if (!pg) - { - Trace("lazy-cdproofchain") - << "LazyCDProofChain::getProofFor: nothing to do\n"; - // nothing to do for this fact, it'll be a leaf in the final proof - // node, don't post-traverse. - visited[cur] = true; - continue; - } - Trace("lazy-cdproofchain") - << "LazyCDProofChain::getProofFor: Call generator " << pg->identify() - << " for chain link " << cur << "\n"; - std::shared_ptr<ProofNode> curPfn = pg->getProofFor(cur); - if (curPfn == nullptr) - { - Trace("lazy-cdproofchain") - << "LazyCDProofChain::getProofFor: No proof found, skip\n"; - visited[cur] = true; - continue; - } - // map node whose proof node must be expanded to the respective poof node - toConnect[cur] = curPfn; - if (!rec) - { - // we don't want to recursively connect this proof - visited[cur] = true; - continue; - } - Trace("lazy-cdproofchain-debug") - << "LazyCDProofChain::getProofFor: stored proof: " << *curPfn.get() - << "\n"; - // retrieve free assumptions and their respective proof nodes - std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap; - expr::getFreeAssumptionsMap(curPfn, famap); - if (Trace.isOn("lazy-cdproofchain")) - { - unsigned alreadyToVisit = 0; - Trace("lazy-cdproofchain") - << "LazyCDProofChain::getProofFor: " << famap.size() - << " free assumptions:\n"; - for (auto fap : famap) - { - Trace("lazy-cdproofchain") - << "LazyCDProofChain::getProofFor: - " << fap.first << "\n"; - alreadyToVisit += - std::find(visit.begin(), visit.end(), fap.first) != visit.end() - ? 1 - : 0; - } - Trace("lazy-cdproofchain") - << "LazyCDProofChain::getProofFor: " << alreadyToVisit - << " already to visit\n"; - } - // mark for post-traversal if we are controlling cycles - if (d_cyclic) - { - Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: marking " - << cur << " for cycle check\n"; - visit.push_back(cur); - visited[cur] = false; - } - else - { - visited[cur] = true; - } - // enqueue free assumptions to process - for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& - fap : famap) - { - // check cycles - if (d_cyclic) - { - // cycles are assumptions being *currently* expanded and seen again, - // i.e. in toConnect and not yet post-visited - auto itToConnect = toConnect.find(fap.first); - if (itToConnect != toConnect.end() && !visited[fap.first]) - { - // Since we have a cycle with an assumption, this fact will be an - // assumption in the final proof node produced by this - // method. Thus we erase it as something to be connected, which - // will keep it as an assumption. - Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: " - "removing cyclic assumption " - << fap.first << " from expansion\n"; - continue; - } - } - // We always add assumptions to visit so that their last seen occurrence - // is expanded (rather than the first seen occurrence, if we were not - // adding assumptions, say, in assumptionsToExpand). This is so because - // in the case where we are checking cycles this is necessary (and - // harmless when we are not). For example the cycle - // - // a2 - // ... - // ---- - // a1 - // ... - // -------- - // a0 a1 a2 - // ... - // --------------- - // n - // - // in which a2 has a1 as an assumption, which has a2 an assumption, - // would not be captured if we did not revisit a1, which is an - // assumption of n and this already occur in assumptionsToExpand when - // it shows up again as an assumption of a2. - visit.push_back(fap.first); - // add assumption proof nodes to be updated - assumptionsToExpand[fap.first].insert( - assumptionsToExpand[fap.first].end(), - fap.second.begin(), - fap.second.end()); - } - if (d_cyclic) - { - Trace("lazy-cdproofchain") << push; - Trace("lazy-cdproofchain-debug") << push; - } - } - else if (!itVisited->second) - { - visited[cur] = true; - Trace("lazy-cdproofchain") << pop; - Trace("lazy-cdproofchain-debug") << pop; - Trace("lazy-cdproofchain") - << "LazyCDProofChain::getProofFor: post-visited " << cur << "\n"; - } - else - { - Trace("lazy-cdproofchain") - << "LazyCDProofChain::getProofFor: already fully processed " << cur - << "\n"; - } - } while (!visit.empty()); - // expand all assumptions marked to be connected - for (const std::pair<const Node, std::shared_ptr<ProofNode>>& npfn : - toConnect) - { - auto it = assumptionsToExpand.find(npfn.first); - if (it == assumptionsToExpand.end()) - { - Assert(npfn.first == fact); - continue; - } - Assert(npfn.second); - Trace("lazy-cdproofchain") - << "LazyCDProofChain::getProofFor: expand assumption " << npfn.first - << "\n"; - Trace("lazy-cdproofchain-debug") - << "LazyCDProofChain::getProofFor: ...expand to " << *npfn.second.get() - << "\n"; - // update each assumption proof node - for (std::shared_ptr<ProofNode> pfn : it->second) - { - d_manager->updateNode(pfn.get(), npfn.second.get()); - } - } - // final proof of fact - auto it = toConnect.find(fact); - if (it == toConnect.end()) - { - return nullptr; - } - return it->second; -} - -void LazyCDProofChain::addLazyStep(Node expected, ProofGenerator* pg) -{ - Assert(pg != nullptr); - Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected - << " set to generator " << pg->identify() << "\n"; - // note this will replace the generator for expected, if any - d_gens.insert(expected, pg); -} - -void LazyCDProofChain::addLazyStep(Node expected, - ProofGenerator* pg, - const std::vector<Node>& assumptions, - const char* ctx) -{ - Assert(pg != nullptr); - Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected - << " set to generator " << pg->identify() << "\n"; - // note this will rewrite the generator for expected, if any - d_gens.insert(expected, pg); - // check if chain is closed if options::proofEagerChecking() is on - if (options::proofEagerChecking()) - { - Trace("lazy-cdproofchain") - << "LazyCDProofChain::addLazyStep: Checking closed proof...\n"; - std::shared_ptr<ProofNode> pfn = pg->getProofFor(expected); - std::vector<Node> allowedLeaves{assumptions.begin(), assumptions.end()}; - // add all current links in the chain - for (const std::pair<const Node, ProofGenerator* const>& link : d_gens) - { - allowedLeaves.push_back(link.first); - } - if (Trace.isOn("lazy-cdproofchain")) - { - Trace("lazy-cdproofchain") << "Checking relative to leaves...\n"; - for (const Node& n : allowedLeaves) - { - Trace("lazy-cdproofchain") << " - " << n << "\n"; - } - Trace("lazy-cdproofchain") << "\n"; - } - pfnEnsureClosedWrt(pfn.get(), allowedLeaves, "lazy-cdproofchain", ctx); - } -} - -bool LazyCDProofChain::hasGenerator(Node fact) const -{ - return d_gens.find(fact) != d_gens.end(); -} - -ProofGenerator* LazyCDProofChain::getGeneratorFor(Node fact) -{ - bool rec = true; - return getGeneratorForInternal(fact, rec); -} - -ProofGenerator* LazyCDProofChain::getGeneratorForInternal(Node fact, bool& rec) -{ - auto it = d_gens.find(fact); - if (it != d_gens.end()) - { - return (*it).second; - } - // otherwise, if no explicit generators, we use the default one - if (d_defGen != nullptr) - { - rec = d_defRec; - return d_defGen; - } - return nullptr; -} - -std::string LazyCDProofChain::identify() const { return "LazyCDProofChain"; } - -} // namespace cvc5 diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h deleted file mode 100644 index 1abb3f84e..000000000 --- a/src/expr/lazy_proof_chain.h +++ /dev/null @@ -1,154 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Haniel Barbosa, Andrew Reynolds, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Lazy proof chain utility. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__EXPR__LAZY_PROOF_CHAIN_H -#define CVC5__EXPR__LAZY_PROOF_CHAIN_H - -#include <vector> - -#include "context/cdhashmap.h" -#include "expr/proof_generator.h" - -namespace cvc5 { - -class ProofNodeManager; - -/** - * A (context-dependent) lazy generator for proof chains. This class is an - * extension of ProofGenerator that additionally that maps facts to proof - * generators in a context-dependent manner. The map is built with the addition - * of lazy steps mapping facts to proof generators. More importantly, its - * getProofFor method expands the proof generators registered to this class by - * connecting, for the proof generated to one fact, assumptions to the proofs - * generated for those assumptinos that are registered in the chain. - */ -class LazyCDProofChain : public ProofGenerator -{ - public: - /** Constructor - * - * @param pnm The proof node manager for constructing ProofNode objects. - * @param cyclic Whether this instance is robust to cycles in the chain. - * @param c The context that this class depends on. If none is provided, - * this class is context-independent. - * @param defGen The default generator to be used if no generator exists - * for a step. - * @param defRec Whether this instance expands proofs from defGen recursively. - */ - LazyCDProofChain(ProofNodeManager* pnm, - bool cyclic = true, - context::Context* c = nullptr, - ProofGenerator* defGen = nullptr, - bool defRec = true); - ~LazyCDProofChain(); - /** - * Get lazy proof for fact, or nullptr if it does not exist, by connecting the - * proof nodes generated for each intermediate relevant fact registered in the - * chain (i.e., in the domain of d_gens). - * - * For example, if d_gens consists of the following pairs - * - * --- (A, PG1) - * --- (B, PG2) - * --- (C, PG3) - * - * and getProofFor(A) is called, with PG1 generating a proof with assumptions - * B and D, then B is expanded, with its assumption proof node being updated - * to the expanded proof node, while D is not. Assuming PG2 provides a proof - * with assumptions C and E, then C is expanded and E is not. Suppose PG3 - * gives a closed proof, thus the call getProofFor(A) produces a proof node - * - * A : ( ... B : ( ... C : (...), ... ASSUME( E ) ), ... ASSUME( D ) ) - * - * Note that the expansions are done directly on the proof nodes produced by - * the generators. - * - * If this instance has been set to be robust to cyclic proofs (i.e., d_cyclic - * is true), then the construction of the proof chain checks that there are no - * cycles, i.e., a given fact would have itself as an assumption when - * connecting the chain links. If such a cycle were to be detected then the - * fact will be marked as an assumption and not expanded in the final proof - * node. The method does not fail. - */ - std::shared_ptr<ProofNode> getProofFor(Node fact) override; - /** Add step by generator - * - * This method stores that expected can be proven by proof generator pg if - * it is required to do so. This mapping is maintained in the remainder of - * the current context (according to the context c provided to this class). - * - * Moreover the lazy steps of this class are expected to fulfill the - * requirement that pg.getProofFor(expected) generates a proof node closed - * with relation to - * (1) a fixed set F1, ..., Fn, - * (2) formulas in the current domain of d_gens. - * - * This is so that we only add links to the chain that depend on a fixed set - * of assumptions or in other links. - * - * @param expected The fact that can be proven. - * @param pg The generator that can proof expected. - * @param assumptions The fixed set of assumptions with relation to which the - * chain, now augmented with expect, must be closed. - * @param ctx The context we are in (for debugging). - */ - void addLazyStep(Node expected, - ProofGenerator* pg, - const std::vector<Node>& assumptions, - const char* ctx = "LazyCDProofChain::addLazyStep"); - - /** As above but does not do the closedness check. */ - void addLazyStep(Node expected, ProofGenerator* pg); - - /** Does the given fact have an explicitly provided generator? */ - bool hasGenerator(Node fact) const; - - /** - * Get generator for fact, or nullptr if it doesnt exist. - */ - ProofGenerator* getGeneratorFor(Node fact); - - /** identify */ - std::string identify() const override; - - /** Retrieve, for each fact in d_gens, it mapped to the proof node generated - * by its generator in d_gens. */ - const std::map<Node, std::shared_ptr<ProofNode>> getLinks() const; - - private: - /** - * Get generator for fact, or nullptr if it doesnt exist. Updates rec to - * true if we should recurse on its proof. - */ - ProofGenerator* getGeneratorForInternal(Node fact, bool& rec); - /** The proof manager, used for allocating new ProofNode objects */ - ProofNodeManager* d_manager; - /** Whether this instance is robust to cycles in the chain. */ - bool d_cyclic; - /** Whether we expand recursively (for the default generator) */ - bool d_defRec; - /** A dummy context used by this class if none is provided */ - context::Context d_context; - /** Maps facts that can be proven to generators */ - context::CDHashMap<Node, ProofGenerator*> d_gens; - /** The default proof generator (if one exists) */ - ProofGenerator* d_defGen; -}; - -} // namespace cvc5 - -#endif /* CVC5__EXPR__LAZY_PROOF_CHAIN_H */ diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp deleted file mode 100644 index 289a5be5b..000000000 --- a/src/expr/proof.cpp +++ /dev/null @@ -1,459 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Aina Niemetz - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of proof. - */ - -#include "expr/proof.h" - -#include "expr/proof_checker.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" - -using namespace cvc5::kind; - -namespace cvc5 { - -CDProof::CDProof(ProofNodeManager* pnm, - context::Context* c, - std::string name, - bool autoSymm) - : d_manager(pnm), - d_context(), - d_nodes(c ? c : &d_context), - d_name(name), - d_autoSymm(autoSymm) -{ -} - -CDProof::~CDProof() {} - -std::shared_ptr<ProofNode> CDProof::getProofFor(Node fact) -{ - std::shared_ptr<ProofNode> pf = getProofSymm(fact); - if (pf != nullptr) - { - return pf; - } - // add as assumption - std::vector<Node> pargs = {fact}; - std::vector<std::shared_ptr<ProofNode>> passume; - std::shared_ptr<ProofNode> pfa = - d_manager->mkNode(PfRule::ASSUME, passume, pargs, fact); - d_nodes.insert(fact, pfa); - return pfa; -} - -std::shared_ptr<ProofNode> CDProof::getProof(Node fact) const -{ - NodeProofNodeMap::iterator it = d_nodes.find(fact); - if (it != d_nodes.end()) - { - return (*it).second; - } - return nullptr; -} - -std::shared_ptr<ProofNode> CDProof::getProofSymm(Node fact) -{ - Trace("cdproof") << "CDProof::getProofSymm: " << fact << std::endl; - std::shared_ptr<ProofNode> pf = getProof(fact); - if (pf != nullptr && !isAssumption(pf.get())) - { - Trace("cdproof") << "...existing non-assume " << pf->getRule() << std::endl; - return pf; - } - else if (!d_autoSymm) - { - Trace("cdproof") << "...not auto considering symmetry" << std::endl; - return pf; - } - Node symFact = getSymmFact(fact); - if (symFact.isNull()) - { - Trace("cdproof") << "...no possible symm" << std::endl; - // no symmetry possible, return original proof (possibly assumption) - return pf; - } - // See if a proof exists for the opposite direction, if so, add the step. - // Notice that SYMM is also disallowed. - std::shared_ptr<ProofNode> pfs = getProof(symFact); - if (pfs != nullptr) - { - // The symmetric fact exists, and the current one either does not, or is - // an assumption. We make a new proof that applies SYMM to pfs. - std::vector<std::shared_ptr<ProofNode>> pschild; - pschild.push_back(pfs); - std::vector<Node> args; - if (pf == nullptr) - { - Trace("cdproof") << "...fresh make symm" << std::endl; - std::shared_ptr<ProofNode> psym = - d_manager->mkNode(PfRule::SYMM, pschild, args, fact); - Assert(psym != nullptr); - d_nodes.insert(fact, psym); - return psym; - } - else if (!isAssumption(pfs.get())) - { - // if its not an assumption, make the connection - Trace("cdproof") << "...update symm" << std::endl; - // update pf - bool sret = d_manager->updateNode(pf.get(), PfRule::SYMM, pschild, args); - AlwaysAssert(sret); - } - } - else - { - Trace("cdproof") << "...no symm, return " - << (pf == nullptr ? "null" : "non-null") << std::endl; - } - // return original proof (possibly assumption) - return pf; -} - -bool CDProof::addStep(Node expected, - PfRule id, - const std::vector<Node>& children, - const std::vector<Node>& args, - bool ensureChildren, - CDPOverwrite opolicy) -{ - Trace("cdproof") << "CDProof::addStep: " << identify() << " : " << id << " " - << expected << ", ensureChildren = " << ensureChildren - << ", overwrite policy = " << opolicy << std::endl; - Trace("cdproof-debug") << "CDProof::addStep: " << identify() - << " : children: " << children << "\n"; - Trace("cdproof-debug") << "CDProof::addStep: " << identify() - << " : args: " << args << "\n"; - // We must always provide expected to this method - Assert(!expected.isNull()); - - std::shared_ptr<ProofNode> pprev = getProofSymm(expected); - if (pprev != nullptr) - { - if (!shouldOverwrite(pprev.get(), id, opolicy)) - { - // we should not overwrite the current step - Trace("cdproof") << "...success, no overwrite" << std::endl; - return true; - } - Trace("cdproof") << "existing proof " << pprev->getRule() - << ", overwrite..." << std::endl; - // we will overwrite the existing proof node by updating its contents below - } - // collect the child proofs, for each premise - std::vector<std::shared_ptr<ProofNode>> pchildren; - for (const Node& c : children) - { - Trace("cdproof") << "- get child " << c << std::endl; - std::shared_ptr<ProofNode> pc = getProofSymm(c); - if (pc == nullptr) - { - if (ensureChildren) - { - // failed to get a proof for a child, fail - Trace("cdproof") << "...fail, no child" << std::endl; - return false; - } - Trace("cdproof") << "--- add assume" << std::endl; - // otherwise, we initialize it as an assumption - std::vector<Node> pcargs = {c}; - std::vector<std::shared_ptr<ProofNode>> pcassume; - pc = d_manager->mkNode(PfRule::ASSUME, pcassume, pcargs, c); - // assumptions never fail to check - Assert(pc != nullptr); - d_nodes.insert(c, pc); - } - pchildren.push_back(pc); - } - - // the user may have provided SYMM of an assumption - if (id == PfRule::SYMM) - { - Assert(pchildren.size() == 1); - if (isAssumption(pchildren[0].get())) - { - // the step we are constructing is a (symmetric fact of an) assumption, so - // there is no use adding it to the proof. - return true; - } - } - - bool ret = true; - // create or update it - std::shared_ptr<ProofNode> pthis; - if (pprev == nullptr) - { - Trace("cdproof") << " new node " << expected << "..." << std::endl; - pthis = d_manager->mkNode(id, pchildren, args, expected); - if (pthis == nullptr) - { - // failed to construct the node, perhaps due to a proof checking failure - Trace("cdproof") << "...fail, proof checking" << std::endl; - return false; - } - d_nodes.insert(expected, pthis); - } - else - { - Trace("cdproof") << " update node " << expected << "..." << std::endl; - // update its value - pthis = pprev; - // We return the value of updateNode here. This means this method may return - // false if this call failed, regardless of whether we already have a proof - // step for expected. - ret = d_manager->updateNode(pthis.get(), id, pchildren, args); - } - if (ret) - { - // the result of the proof node should be expected - Assert(pthis->getResult() == expected); - - // notify new proof - notifyNewProof(expected); - } - - Trace("cdproof") << "...return " << ret << std::endl; - return ret; -} - -void CDProof::notifyNewProof(Node expected) -{ - if (!d_autoSymm) - { - return; - } - // ensure SYMM proof is also linked to an existing proof, if it is an - // assumption. - Node symExpected = getSymmFact(expected); - if (!symExpected.isNull()) - { - Trace("cdproof") << " check connect symmetry " << symExpected << std::endl; - // if it exists, we may need to update it - std::shared_ptr<ProofNode> pfs = getProof(symExpected); - if (pfs != nullptr) - { - Trace("cdproof") << " connect via getProofSymm method..." << std::endl; - // call the get function with symmetry, which will do the update - std::shared_ptr<ProofNode> pfss = getProofSymm(symExpected); - } - else - { - Trace("cdproof") << " no connect" << std::endl; - } - } -} - -bool CDProof::addStep(Node expected, - const ProofStep& step, - bool ensureChildren, - CDPOverwrite opolicy) -{ - return addStep(expected, - step.d_rule, - step.d_children, - step.d_args, - ensureChildren, - opolicy); -} - -bool CDProof::addSteps(const ProofStepBuffer& psb, - bool ensureChildren, - CDPOverwrite opolicy) -{ - const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps(); - for (const std::pair<Node, ProofStep>& ps : steps) - { - if (!addStep(ps.first, ps.second, ensureChildren, opolicy)) - { - return false; - } - } - return true; -} - -bool CDProof::addProof(std::shared_ptr<ProofNode> pn, - CDPOverwrite opolicy, - bool doCopy) -{ - if (!doCopy) - { - // If we aren't doing a deep copy, we either store pn or link its top - // node into the existing pointer - Node curFact = pn->getResult(); - std::shared_ptr<ProofNode> cur = getProofSymm(curFact); - if (cur == nullptr) - { - // Assert that the checker of this class agrees with (the externally - // provided) pn. This ensures that if pn was checked by a different - // checker than the one of the manager in this class, then it is double - // checked here, so that this class maintains the invariant that all of - // its nodes in d_nodes have been checked by the underlying checker. - Assert(d_manager->getChecker() == nullptr - || d_manager->getChecker()->check(pn.get(), curFact) == curFact); - // just store the proof for fact - d_nodes.insert(curFact, pn); - } - else if (shouldOverwrite(cur.get(), pn->getRule(), opolicy)) - { - // We update cur to have the structure of the top node of pn. Notice that - // the interface to update this node will ensure that the proof apf is a - // proof of the assumption. If it does not, then pn was wrong. - if (!d_manager->updateNode( - cur.get(), pn->getRule(), pn->getChildren(), pn->getArguments())) - { - return false; - } - } - // also need to connect via SYMM if necessary - notifyNewProof(curFact); - return true; - } - std::unordered_map<ProofNode*, bool> visited; - std::unordered_map<ProofNode*, bool>::iterator it; - std::vector<ProofNode*> visit; - ProofNode* cur; - Node curFact; - visit.push_back(pn.get()); - bool retValue = true; - do - { - cur = visit.back(); - curFact = cur->getResult(); - visit.pop_back(); - it = visited.find(cur); - if (it == visited.end()) - { - // visit the children - visited[cur] = false; - visit.push_back(cur); - const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren(); - for (const std::shared_ptr<ProofNode>& c : cs) - { - visit.push_back(c.get()); - } - } - else if (!it->second) - { - // we always call addStep, which may or may not overwrite the - // current step - std::vector<Node> pexp; - const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren(); - for (const std::shared_ptr<ProofNode>& c : cs) - { - Assert(!c->getResult().isNull()); - pexp.push_back(c->getResult()); - } - // can ensure children at this point - bool res = addStep( - curFact, cur->getRule(), pexp, cur->getArguments(), true, opolicy); - // should always succeed - Assert(res); - retValue = retValue && res; - visited[cur] = true; - } - } while (!visit.empty()); - - return retValue; -} - -bool CDProof::hasStep(Node fact) -{ - std::shared_ptr<ProofNode> pf = getProof(fact); - if (pf != nullptr && !isAssumption(pf.get())) - { - return true; - } - else if (!d_autoSymm) - { - return false; - } - Node symFact = getSymmFact(fact); - if (symFact.isNull()) - { - return false; - } - pf = getProof(symFact); - if (pf != nullptr && !isAssumption(pf.get())) - { - return true; - } - return false; -} - -ProofNodeManager* CDProof::getManager() const { return d_manager; } - -bool CDProof::shouldOverwrite(ProofNode* pn, PfRule newId, CDPOverwrite opol) -{ - Assert(pn != nullptr); - // we overwrite only if opol is CDPOverwrite::ALWAYS, or if - // opol is CDPOverwrite::ASSUME_ONLY and the previously - // provided proof pn was an assumption and the currently provided step is not - return opol == CDPOverwrite::ALWAYS - || (opol == CDPOverwrite::ASSUME_ONLY && isAssumption(pn) - && newId != PfRule::ASSUME); -} - -bool CDProof::isAssumption(ProofNode* pn) -{ - PfRule rule = pn->getRule(); - if (rule == PfRule::ASSUME) - { - return true; - } - else if (rule == PfRule::SYMM) - { - const std::vector<std::shared_ptr<ProofNode>>& pc = pn->getChildren(); - Assert(pc.size() == 1); - return pc[0]->getRule() == PfRule::ASSUME; - } - return false; -} - -bool CDProof::isSame(TNode f, TNode g) -{ - if (f == g) - { - return true; - } - Kind fk = f.getKind(); - Kind gk = g.getKind(); - if (fk == EQUAL && gk == EQUAL && f[0] == g[1] && f[1] == g[0]) - { - // symmetric equality - return true; - } - if (fk == NOT && gk == NOT && f[0].getKind() == EQUAL - && g[0].getKind() == EQUAL && f[0][0] == g[0][1] && f[0][1] == g[0][0]) - { - // symmetric disequality - return true; - } - return false; -} - -Node CDProof::getSymmFact(TNode f) -{ - bool polarity = f.getKind() != NOT; - TNode fatom = polarity ? f : f[0]; - if (fatom.getKind() != EQUAL || fatom[0] == fatom[1]) - { - return Node::null(); - } - Node symFact = fatom[1].eqNode(fatom[0]); - return polarity ? symFact : symFact.notNode(); -} - -std::string CDProof::identify() const { return d_name; } - -} // namespace cvc5 diff --git a/src/expr/proof.h b/src/expr/proof.h deleted file mode 100644 index 496815938..000000000 --- a/src/expr/proof.h +++ /dev/null @@ -1,278 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Proof utility. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__EXPR__PROOF_H -#define CVC5__EXPR__PROOF_H - -#include <vector> - -#include "context/cdhashmap.h" -#include "expr/node.h" -#include "expr/proof_generator.h" -#include "expr/proof_step_buffer.h" - -namespace cvc5 { - -class ProofNode; -class ProofNodeManager; - -/** - * A (context-dependent) proof. - * - * This maintains a context-dependent map from formulas to ProofNode shared - * pointers. When a step is added, it internally uses mutable ProofNode pointers - * to link the steps in the proof together. - * - * It is important to note that the premises of proof steps given to this class - * are *Node* not *ProofNode*. In other words, the user of this class does - * not have to manage ProofNode pointers while using this class. Instead, - * ProofNode is the final product of this class, via the getProof interface, - * which returns a ProofNode object that has linked together the proof steps - * added to this object. - * - * Its main interface is the function addStep, which registers a single - * step in the proof. Its interface is: - * addStep( <conclusion>, <rule>, <premises>, <args>, ...<options>... ) - * where conclusion is what to be proven, rule is an identifier, premises - * are the formulas that imply conclusion, and args are additional arguments to - * the proof rule application. The options include whether we ensure children - * proofs already exist for the premises and our policty for overwriting - * existing steps. - * - * As an example, let A, B, C, D be formulas represented by Nodes. If we - * call: - * - addStep( A, ID_A, { B, C }, {} ) - * - addStep( B, ID_B, { D }, {} ) - * - addStep( E, ID_E, {}, {} ) - * with default options, then getProof( A ) returns the ProofNode of the form: - * ID_A( ID_B( ASSUME( D ) ), ASSUME( C ) ) - * Notice that the above calls to addStep can be made in either order. The - * proof step for E was not involved in the proof of A. - * - * If the user wants to combine proofs, then a addProof interface is - * available. The method addProof can be seen as syntax sugar for making - * multiple calls to addStep. Continuing the above example, if we call: - * - addProof( F, ID_F( ASSUME( A ), ASSUME( E ) ) ) - * is the same as calling steps corresponding the steps in the provided proof - * bottom-up, starting from the leaves. - * --- addStep( A, ASSUME, {}, {}, true ) - * --- addStep( E, ASSUME, {}, {}, true ) - * --- addStep( F, ID_F, { A, E }, {}, true ) - * The fifth argument provided indicates that we want to ensure child proofs - * are already available for the step (see ensureChildren in addStep below). - * This will result in getProof( F ) returning: - * ID_F( ID_A( ID_B( ASSUME( D ) ), ASSUME( C ) ), ID_E() ) - * Notice that the proof of A by ID_A was not overwritten by ASSUME in the - * addStep call above. - * - * The default policy for overwriting proof steps (CDPOverwrite::ASSUME_ONLY) - * gives ASSUME a special status. An ASSUME step can be seen as a step whose - * justification has not yet been provided. Thus, it is always overwritten. - * Other proof rules are never overwritten, unless the argument opolicy is - * CDPOverwrite::ALWAYS. - * - * As an another example, say that we call: - * - addStep( B, ID_B1 {}, {} ) - * - addStep( A, ID_A1, {B, C}, {} ) - * At this point, getProof( A ) returns: - * ID_A1( ID_B1(), ASSUME(C) ) - * Now, assume an additional call is made to addProof, where notice - * the overwrite policy is CDPOverwrite::ASSUME_ONLY by default: - * - addProof( D, ID_D( ID_A2( ID_B2(), ID_C() ) ) ) - * where assume ID_B2() and ID_C() prove B and C respectively. This call is - * equivalent to calling: - * --- addStep( B, ID_B2, {}, {}, true ) - * --- addStep( C, ID_C, {}, {}, true ) - * --- addStep( A, ID_A2, {B, C}, {}, true ) - * --- addStep( D, ID_D, {A}, {}, true ) - * Afterwards, getProof( D ) returns: - * ID_D( ID_A1( ID_B1(), ID_C() ) ) - * Notice that the steps with ID_A1 and ID_B1 were not overwritten by this call, - * whereas the assumption of C was overwritten by the proof ID_C(). Notice that - * the proof of D was completely traversed in addProof, despite encountering - * formulas, A and B, that were already given proof steps. - * - * This class requires a ProofNodeManager object, which is a trusted way of - * allocating ProofNode pointers. This manager may have an underlying checker, - * although this is not required. It also (optionally) takes a context c. - * If no context is provided, then this proof is context-independent. This - * is implemented internally by using a dummy context that is never pushed - * or popped. The map from Nodes to ProofNodes is context-dependent and is - * backtracked when its context backtracks. - * - * An important invariant of this object is that there exists (at most) one - * proof step for each Node. Thus, the ProofNode objects returned by this - * class share proofs for common subformulas, as guaranteed by the fact that - * Node objects have perfect sharing. - * - * Notice that this class is agnostic to symmetry of equality. In other - * words, adding a step that concludes (= x y) is effectively the same as - * providing a step that concludes (= y x) from the point of view of a user - * of this class. This is accomplished by adding SYMM steps on demand when - * a formula is looked up. For example say we call: - * - addStep( (= x y), ID_1 {}, {} ) - * - addStep( P, ID_2, {(= y x)}, {} ) - * Afterwards, getProof( P ) returns: - * ID_2( SYMM( ID_1() ) ) - * where notice SYMM was added so that (= y x) is a premise of the application - * of ID_2. More generally, CDProof::isSame(F,G) returns true if F and G are - * essentially the same formula according to this class. - */ -class CDProof : public ProofGenerator -{ - public: - /** - * @param pnm The proof node manager responsible for constructor ProofNode - * @param c The context this proof depends on - * @param name The name of this proof (for debugging) - * @param autoSymm Whether this proof automatically adds symmetry steps based - * on policy documented above. - */ - CDProof(ProofNodeManager* pnm, - context::Context* c = nullptr, - std::string name = "CDProof", - bool autoSymm = true); - virtual ~CDProof(); - /** - * Make proof for fact. - * - * This method always returns a non-null ProofNode. It may generate new - * steps so that a ProofNode can be constructed for fact. In particular, - * if no step exists for fact, then we may construct and return ASSUME(fact). - * If fact is of the form (= t s), no step exists for fact, but a proof - * P for (= s t) exists, then this method returns SYMM(P). - * - * Notice that this call does *not* clone the ProofNode object. Hence, the - * returned proof may be updated by further calls to this class. The caller - * should call ProofNode::clone if they want to own it. - */ - std::shared_ptr<ProofNode> getProofFor(Node fact) override; - /** Add step - * - * @param expected The intended conclusion of this proof step. This must be - * non-null. - * @param id The identifier for the proof step. - * @param children The antecendants of the proof step. Each children[i] should - * be a fact previously added as a conclusion of an addStep call when - * ensureChildren is true. - * @param args The arguments of the proof step. - * @param ensureChildren Whether we wish to ensure steps have been added - * for all nodes in children - * @param opolicy Policy for whether to overwrite if a step for - * expected was already provided (via a previous call to addStep) - * @return The true if indeed the proof step proves expected, or - * false otherwise. The latter can happen if the proof has a different (or - * invalid) conclusion, or if one of the children does not have a proof and - * ensureChildren is true. - * - * This method may create proofs justified by ASSUME of the facts in - * children that have not already been proven when ensureChildren is false. - * Notice that ensureChildren should be true if the proof is being - * constructed is a strictly eager fashion (bottom up from its leaves), while - * ensureChildren should be false if the steps are added lazily or out - * of order. - * - * This method only overwrites proofs for facts that were added as - * steps with id ASSUME when opolicy is CDPOverwrite::ASSUME_ONLY, and always - * (resp. never) overwrites an existing step if one was provided when opolicy - * is CDPOverwrite::ALWAYS (resp. CDPOverwrite::NEVER). - */ - bool addStep(Node expected, - PfRule id, - const std::vector<Node>& children, - const std::vector<Node>& args, - bool ensureChildren = false, - CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY); - /** Version with ProofStep */ - bool addStep(Node expected, - const ProofStep& step, - bool ensureChildren = false, - CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY); - /** Version with ProofStepBuffer */ - bool addSteps(const ProofStepBuffer& psb, - bool ensureChildren = false, - CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY); - /** Add proof - * - * @param pn The proof of the given fact. - * @param opolicy Policy for whether to force overwriting if a step - * was already provided. This is used for each node in the proof if doCopy - * is true. - * @param doCopy Whether we make a deep copy of the pn. - * @return true if all steps were successfully added to this class. If it - * returns true, it registers a copy of all of the subnodes of pn to this - * proof class. - * - * If doCopy is true, this method is implemented by calling addStep above for - * all subnodes of pn, traversed as a dag. This means that fresh ProofNode - * objects may be generated by this call, and further modifications to pn do - * not impact the internal data of this class. - */ - bool addProof(std::shared_ptr<ProofNode> pn, - CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY, - bool doCopy = false); - /** Return true if fact already has a proof step */ - bool hasStep(Node fact); - /** Get the proof manager for this proof */ - ProofNodeManager* getManager() const; - /** - * Is same? Returns true if f and g are the same formula, or if they are - * symmetric equalities. If two nodes f and g are the same, then a proof for - * f suffices as a proof for g according to this class. - */ - static bool isSame(TNode f, TNode g); - /** Get proof for fact, or nullptr if it does not exist. */ - std::shared_ptr<ProofNode> getProof(Node fact) const; - /** - * Get symmetric fact (a g such that isSame returns true for isSame(f,g)), or - * null if none exist. - */ - static Node getSymmFact(TNode f); - /** identify */ - std::string identify() const override; - - protected: - typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofNodeMap; - /** The proof manager, used for allocating new ProofNode objects */ - ProofNodeManager* d_manager; - /** A dummy context used by this class if none is provided */ - context::Context d_context; - /** The nodes of the proof */ - NodeProofNodeMap d_nodes; - /** Name identifier */ - std::string d_name; - /** Whether we automatically add symmetry steps */ - bool d_autoSymm; - /** Ensure fact sym */ - std::shared_ptr<ProofNode> getProofSymm(Node fact); - /** - * Returns true if we should overwrite proof node pn with a step having id - * newId, based on policy opol. - */ - static bool shouldOverwrite(ProofNode* pn, PfRule newId, CDPOverwrite opol); - /** Returns true if pn is an assumption. */ - static bool isAssumption(ProofNode* pn); - /** - * Notify new proof, called when a new proof of expected is provided. This is - * used internally to connect proofs of symmetric facts, when necessary. - */ - void notifyNewProof(Node expected); -}; - -} // namespace cvc5 - -#endif /* CVC5__EXPR__PROOF_MANAGER_H */ diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp deleted file mode 100644 index 69f880ed5..000000000 --- a/src/expr/proof_checker.cpp +++ /dev/null @@ -1,345 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Aina Niemetz - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of proof checker. - */ - -#include "expr/proof_checker.h" - -#include "expr/proof_node.h" -#include "expr/skolem_manager.h" -#include "options/proof_options.h" -#include "smt/smt_statistics_registry.h" - -using namespace cvc5::kind; - -namespace cvc5 { - -Node ProofRuleChecker::check(PfRule id, - const std::vector<Node>& children, - const std::vector<Node>& args) -{ - // call instance-specific checkInternal method - return checkInternal(id, children, args); -} - -bool ProofRuleChecker::getUInt32(TNode n, uint32_t& i) -{ - // must be a non-negative integer constant that fits an unsigned int - if (n.isConst() && n.getType().isInteger() - && n.getConst<Rational>().sgn() >= 0 - && n.getConst<Rational>().getNumerator().fitsUnsignedInt()) - { - i = n.getConst<Rational>().getNumerator().toUnsignedInt(); - return true; - } - return false; -} - -bool ProofRuleChecker::getBool(TNode n, bool& b) -{ - if (n.isConst() && n.getType().isBoolean()) - { - b = n.getConst<bool>(); - return true; - } - return false; -} - -bool ProofRuleChecker::getKind(TNode n, Kind& k) -{ - uint32_t i; - if (!getUInt32(n, i)) - { - return false; - } - k = static_cast<Kind>(i); - return true; -} - -Node ProofRuleChecker::mkKindNode(Kind k) -{ - if (k == UNDEFINED_KIND) - { - // UNDEFINED_KIND is negative, hence return null to avoid cast - return Node::null(); - } - return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(k))); -} - -ProofCheckerStatistics::ProofCheckerStatistics() - : d_ruleChecks(smtStatisticsRegistry().registerHistogram<PfRule>( - "ProofCheckerStatistics::ruleChecks")), - d_totalRuleChecks(smtStatisticsRegistry().registerInt( - "ProofCheckerStatistics::totalRuleChecks")) -{ -} - -Node ProofChecker::check(ProofNode* pn, Node expected) -{ - return check(pn->getRule(), pn->getChildren(), pn->getArguments(), expected); -} - -Node ProofChecker::check( - PfRule id, - const std::vector<std::shared_ptr<ProofNode>>& children, - const std::vector<Node>& args, - Node expected) -{ - // optimization: immediately return for ASSUME - if (id == PfRule::ASSUME) - { - Assert(children.empty()); - Assert(args.size() == 1 && args[0].getType().isBoolean()); - Assert(expected.isNull() || expected == args[0]); - return expected; - } - // record stat - d_stats.d_ruleChecks << id; - ++d_stats.d_totalRuleChecks; - Trace("pfcheck") << "ProofChecker::check: " << id << std::endl; - std::vector<Node> cchildren; - for (const std::shared_ptr<ProofNode>& pc : children) - { - Assert(pc != nullptr); - Node cres = pc->getResult(); - if (cres.isNull()) - { - Trace("pfcheck") << "ProofChecker::check: failed child" << std::endl; - Unreachable() - << "ProofChecker::check: child proof was invalid (null conclusion)" - << std::endl; - // should not have been able to create such a proof node - return Node::null(); - } - cchildren.push_back(cres); - if (Trace.isOn("pfcheck")) - { - std::stringstream ssc; - pc->printDebug(ssc); - Trace("pfcheck") << " child: " << ssc.str() << " : " << cres - << std::endl; - } - } - Trace("pfcheck") << " args: " << args << std::endl; - Trace("pfcheck") << " expected: " << expected << std::endl; - std::stringstream out; - // we use trusted (null) checkers here, since we want the proof generation to - // proceed without failing here. We always enable output since a failure - // implies that we will exit with the error message below. - Node res = checkInternal(id, cchildren, args, expected, out, true, true); - if (res.isNull()) - { - Trace("pfcheck") << "ProofChecker::check: failed" << std::endl; - Unreachable() << "ProofChecker::check: failed, " << out.str() << std::endl; - // it did not match the given expectation, fail - return Node::null(); - } - Trace("pfcheck") << "ProofChecker::check: success!" << std::endl; - return res; -} - -Node ProofChecker::checkDebug(PfRule id, - const std::vector<Node>& cchildren, - const std::vector<Node>& args, - Node expected, - const char* traceTag) -{ - std::stringstream out; - bool traceEnabled = Trace.isOn(traceTag); - // Since we are debugging, we want to treat trusted (null) checkers as - // a failure. We only enable output if the trace is enabled for efficiency. - Node res = - checkInternal(id, cchildren, args, expected, out, false, traceEnabled); - if (traceEnabled) - { - Trace(traceTag) << "ProofChecker::checkDebug: " << id; - if (res.isNull()) - { - Trace(traceTag) << " failed, " << out.str() << std::endl; - } - else - { - Trace(traceTag) << " success" << std::endl; - } - Trace(traceTag) << "cchildren: " << cchildren << std::endl; - Trace(traceTag) << " args: " << args << std::endl; - } - return res; -} - -Node ProofChecker::checkInternal(PfRule id, - const std::vector<Node>& cchildren, - const std::vector<Node>& args, - Node expected, - std::stringstream& out, - bool useTrustedChecker, - bool enableOutput) -{ - std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id); - if (it == d_checker.end()) - { - // no checker for the rule - if (enableOutput) - { - out << "no checker for rule " << id << std::endl; - } - return Node::null(); - } - else if (it->second == nullptr) - { - if (useTrustedChecker) - { - Notice() << "ProofChecker::check: trusting PfRule " << id << std::endl; - // trusted checker - return expected; - } - else - { - if (enableOutput) - { - out << "trusted checker for rule " << id << std::endl; - } - return Node::null(); - } - } - // check it with the corresponding checker - Node res = it->second->check(id, cchildren, args); - if (!expected.isNull()) - { - Node expectedw = expected; - if (res != expectedw) - { - if (enableOutput) - { - out << "result does not match expected value." << std::endl - << " PfRule: " << id << std::endl; - for (const Node& c : cchildren) - { - out << " child: " << c << std::endl; - } - for (const Node& a : args) - { - out << " arg: " << a << std::endl; - } - out << " result: " << res << std::endl - << " expected: " << expected << std::endl; - } - // it did not match the given expectation, fail - return Node::null(); - } - } - // fails if pedantic level is not met - if (options::proofEagerChecking()) - { - std::stringstream serr; - if (isPedanticFailure(id, serr, enableOutput)) - { - if (enableOutput) - { - out << serr.str() << std::endl; - if (Trace.isOn("proof-pedantic")) - { - Trace("proof-pedantic") - << "Failed pedantic check for " << id << std::endl; - Trace("proof-pedantic") << "Expected: " << expected << std::endl; - out << "Expected: " << expected << std::endl; - } - } - return Node::null(); - } - } - return res; -} - -void ProofChecker::registerChecker(PfRule id, ProofRuleChecker* psc) -{ - std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id); - if (it != d_checker.end()) - { - // checker is already provided - Notice() << "ProofChecker::registerChecker: checker already exists for " - << id << std::endl; - return; - } - d_checker[id] = psc; -} - -void ProofChecker::registerTrustedChecker(PfRule id, - ProofRuleChecker* psc, - uint32_t plevel) -{ - AlwaysAssert(plevel <= 10) << "ProofChecker::registerTrustedChecker: " - "pedantic level must be 0-10, got " - << plevel << " for " << id; - registerChecker(id, psc); - // overwrites if already there - if (d_plevel.find(id) != d_plevel.end()) - { - Notice() << "ProofChecker::registerTrustedRule: already provided pedantic " - "level for " - << id << std::endl; - } - d_plevel[id] = plevel; -} - -ProofRuleChecker* ProofChecker::getCheckerFor(PfRule id) -{ - std::map<PfRule, ProofRuleChecker*>::const_iterator it = d_checker.find(id); - if (it == d_checker.end()) - { - return nullptr; - } - return it->second; -} - -uint32_t ProofChecker::getPedanticLevel(PfRule id) const -{ - std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id); - if (itp != d_plevel.end()) - { - return itp->second; - } - return 0; -} - -bool ProofChecker::isPedanticFailure(PfRule id, - std::ostream& out, - bool enableOutput) const -{ - if (d_pclevel == 0) - { - return false; - } - std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id); - if (itp != d_plevel.end()) - { - if (itp->second <= d_pclevel) - { - if (enableOutput) - { - out << "pedantic level for " << id << " not met (rule level is " - << itp->second << " which is at or below the pedantic level " - << d_pclevel << ")"; - bool pedanticTraceEnabled = Trace.isOn("proof-pedantic"); - if (!pedanticTraceEnabled) - { - out << ", use -t proof-pedantic for details"; - } - } - return true; - } - } - return false; -} - -} // namespace cvc5 diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h deleted file mode 100644 index e778f687e..000000000 --- a/src/expr/proof_checker.h +++ /dev/null @@ -1,206 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Proof checker utility. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__EXPR__PROOF_CHECKER_H -#define CVC5__EXPR__PROOF_CHECKER_H - -#include <map> - -#include "expr/node.h" -#include "expr/proof_rule.h" -#include "util/statistics_stats.h" - -namespace cvc5 { - -class ProofChecker; -class ProofNode; - -/** A virtual base class for checking a proof rule */ -class ProofRuleChecker -{ - public: - ProofRuleChecker() {} - virtual ~ProofRuleChecker() {} - /** - * This checks a single step in a proof. - * - * Return the formula that is proven by a proof node with the given id, - * premises and arguments, or null if such a proof node is not well-formed. - * - * Note that the input/output of this method expects to be terms in *Skolem - * form*, which is passed to checkInternal below. Rule checkers may - * convert premises to witness form when necessary. - * - * @param id The id of the proof node to check - * @param children The premises of the proof node to check. These are nodes - * corresponding to the conclusion (ProofNode::getResult) of the children - * of the proof node we are checking in Skolem form. - * @param args The arguments of the proof node to check - * @return The conclusion of the proof node, in Skolem form, if successful or - * null if such a proof node is malformed. - */ - Node check(PfRule id, - const std::vector<Node>& children, - const std::vector<Node>& args); - - /** get an index from a node, return false if we fail */ - static bool getUInt32(TNode n, uint32_t& i); - /** get a Boolean from a node, return false if we fail */ - static bool getBool(TNode n, bool& b); - /** get a Kind from a node, return false if we fail */ - static bool getKind(TNode n, Kind& k); - /** Make a Kind into a node */ - static Node mkKindNode(Kind k); - - /** Register all rules owned by this rule checker into pc. */ - virtual void registerTo(ProofChecker* pc) {} - - protected: - /** - * This checks a single step in a proof. - * - * @param id The id of the proof node to check - * @param children The premises of the proof node to check. These are nodes - * corresponding to the conclusion (ProofNode::getResult) of the children - * of the proof node we are checking. - * @param args The arguments of the proof node to check - * @return The conclusion of the proof node if successful or null if such a - * proof node is malformed. - */ - virtual Node checkInternal(PfRule id, - const std::vector<Node>& children, - const std::vector<Node>& args) = 0; -}; - -/** Statistics class */ -class ProofCheckerStatistics -{ - public: - ProofCheckerStatistics(); - /** Counts the number of checks for each kind of proof rule */ - HistogramStat<PfRule> d_ruleChecks; - /** Total number of rule checks */ - IntStat d_totalRuleChecks; -}; - -/** A class for checking proofs */ -class ProofChecker -{ - public: - ProofChecker(uint32_t pclevel = 0) : d_pclevel(pclevel) {} - ~ProofChecker() {} - /** - * Return the formula that is proven by proof node pn, or null if pn is not - * well-formed. If expected is non-null, then we return null if pn does not - * prove expected. - * - * @param pn The proof node to check - * @param expected The (optional) formula that is the expected conclusion of - * the proof node. - * @return The conclusion of the proof node if successful or null if the - * proof is malformed, or if no checker is available for id. - */ - Node check(ProofNode* pn, Node expected = Node::null()); - /** Same as above, with explicit arguments - * - * @param id The id of the proof node to check - * @param children The children of the proof node to check - * @param args The arguments of the proof node to check - * @param expected The (optional) formula that is the expected conclusion of - * the proof node. - * @return The conclusion of the proof node if successful or null if the - * proof is malformed, or if no checker is available for id. - */ - Node check(PfRule id, - const std::vector<std::shared_ptr<ProofNode>>& children, - const std::vector<Node>& args, - Node expected = Node::null()); - /** - * Same as above, without conclusions instead of proof node children. This - * is used for debugging. In particular, this function does not throw an - * assertion failure when a proof step is malformed and can be used without - * constructing proof nodes. - * - * @param id The id of the proof node to check - * @param children The conclusions of the children of the proof node to check - * @param args The arguments of the proof node to check - * @param expected The (optional) formula that is the expected conclusion of - * the proof node. - * @param traceTag The trace tag to print debug information to - * @return The conclusion of the proof node if successful or null if the - * proof is malformed, or if no checker is available for id. - */ - Node checkDebug(PfRule id, - const std::vector<Node>& cchildren, - const std::vector<Node>& args, - Node expected = Node::null(), - const char* traceTag = ""); - /** Indicate that psc is the checker for proof rule id */ - void registerChecker(PfRule id, ProofRuleChecker* psc); - /** - * Indicate that id is a trusted rule with the given pedantic level, e.g.: - * 0: (mandatory) always a failure to use the given id - * 1: (major) failure on all (non-zero) pedantic levels - * 10: (minor) failure only on pedantic levels >= 10. - */ - void registerTrustedChecker(PfRule id, - ProofRuleChecker* psc, - uint32_t plevel = 10); - /** get checker for */ - ProofRuleChecker* getCheckerFor(PfRule id); - - /** - * Get the pedantic level for id if it has been assigned a pedantic - * level via registerTrustedChecker above, or zero otherwise. - */ - uint32_t getPedanticLevel(PfRule id) const; - - /** - * Is pedantic failure? If so, we return true and write a debug message on the - * output stream out if enableOutput is true. - */ - bool isPedanticFailure(PfRule id, - std::ostream& out, - bool enableOutput = true) const; - - private: - /** statistics class */ - ProofCheckerStatistics d_stats; - /** Maps proof rules to their checker */ - std::map<PfRule, ProofRuleChecker*> d_checker; - /** Maps proof trusted rules to their pedantic level */ - std::map<PfRule, uint32_t> d_plevel; - /** The pedantic level of this checker */ - uint32_t d_pclevel; - /** - * Check internal. This is used by check and checkDebug above. It writes - * checking errors on out when enableOutput is true. We treat trusted checkers - * (nullptr in the range of the map d_checker) as failures if - * useTrustedChecker = false. - */ - Node checkInternal(PfRule id, - const std::vector<Node>& cchildren, - const std::vector<Node>& args, - Node expected, - std::stringstream& out, - bool useTrustedChecker, - bool enableOutput); -}; - -} // namespace cvc5 - -#endif /* CVC5__EXPR__PROOF_CHECKER_H */ diff --git a/src/expr/proof_ensure_closed.cpp b/src/expr/proof_ensure_closed.cpp deleted file mode 100644 index e89bd6692..000000000 --- a/src/expr/proof_ensure_closed.cpp +++ /dev/null @@ -1,183 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Haniel Barbosa - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of debug checks for ensuring proofs are closed. - */ - -#include "expr/proof_ensure_closed.h" - -#include <sstream> - -#include "expr/proof_generator.h" -#include "expr/proof_node.h" -#include "expr/proof_node_algorithm.h" -#include "options/proof_options.h" -#include "options/smt_options.h" - -namespace cvc5 { - -/** - * Ensure closed with respect to assumptions, internal version, which - * generalizes the check for a proof generator or a proof node. - */ -void ensureClosedWrtInternal(Node proven, - ProofGenerator* pg, - ProofNode* pnp, - const std::vector<Node>& assumps, - const char* c, - const char* ctx, - bool reqGen) -{ - if (!options::produceProofs()) - { - // proofs not enabled, do not do check - return; - } - bool isTraceDebug = Trace.isOn(c); - if (!options::proofEagerChecking() && !isTraceDebug) - { - // trace is off and proof new eager checking is off, do not do check - return; - } - std::stringstream sdiag; - bool isTraceOn = Trace.isOn(c); - if (!isTraceOn) - { - sdiag << ", use -t " << c << " for details"; - } - bool dumpProofTraceOn = Trace.isOn("dump-proof-error"); - if (!dumpProofTraceOn) - { - sdiag << ", use -t dump-proof-error for details on proof"; - } - // get the proof node in question, which is either provided or built by the - // proof generator - std::shared_ptr<ProofNode> pn; - std::stringstream ss; - if (pnp != nullptr) - { - Assert(pg == nullptr); - ss << "ProofNode in context " << ctx; - } - else - { - ss << "ProofGenerator: " << (pg == nullptr ? "null" : pg->identify()) - << " in context " << ctx; - if (pg == nullptr) - { - // only failure if flag is true - if (reqGen) - { - Unreachable() << "...ensureClosed: no generator in context " << ctx - << sdiag.str(); - } - } - else - { - Assert(!proven.isNull()); - pn = pg->getProofFor(proven); - pnp = pn.get(); - } - } - Trace(c) << "=== ensureClosed: " << ss.str() << std::endl; - Trace(c) << "Proven: " << proven << std::endl; - if (pnp == nullptr) - { - if (pg == nullptr) - { - // did not require generator - Assert(!reqGen); - Trace(c) << "...ensureClosed: no generator in context " << ctx - << std::endl; - return; - } - } - // if we don't have a proof node, a generator failed - if (pnp == nullptr) - { - Assert(pg != nullptr); - AlwaysAssert(false) << "...ensureClosed: null proof from " << ss.str() - << sdiag.str(); - } - std::vector<Node> fassumps; - expr::getFreeAssumptions(pnp, fassumps); - bool isClosed = true; - std::stringstream ssf; - for (const Node& fa : fassumps) - { - if (std::find(assumps.begin(), assumps.end(), fa) == assumps.end()) - { - isClosed = false; - ssf << "- " << fa << std::endl; - } - } - if (!isClosed) - { - Trace(c) << "Free assumptions:" << std::endl; - Trace(c) << ssf.str(); - if (!assumps.empty()) - { - Trace(c) << "Expected assumptions:" << std::endl; - for (const Node& a : assumps) - { - Trace(c) << "- " << a << std::endl; - } - } - if (dumpProofTraceOn) - { - Trace("dump-proof-error") << " Proof: " << *pnp << std::endl; - } - } - AlwaysAssert(isClosed) << "...ensureClosed: open proof from " << ss.str() - << sdiag.str(); - Trace(c) << "...ensureClosed: success" << std::endl; - Trace(c) << "====" << std::endl; -} - -void pfgEnsureClosed(Node proven, - ProofGenerator* pg, - const char* c, - const char* ctx, - bool reqGen) -{ - Assert(!proven.isNull()); - // proof generator may be null - std::vector<Node> assumps; - ensureClosedWrtInternal(proven, pg, nullptr, assumps, c, ctx, reqGen); -} - -void pfgEnsureClosedWrt(Node proven, - ProofGenerator* pg, - const std::vector<Node>& assumps, - const char* c, - const char* ctx, - bool reqGen) -{ - Assert(!proven.isNull()); - // proof generator may be null - ensureClosedWrtInternal(proven, pg, nullptr, assumps, c, ctx, reqGen); -} - -void pfnEnsureClosed(ProofNode* pn, const char* c, const char* ctx) -{ - ensureClosedWrtInternal(Node::null(), nullptr, pn, {}, c, ctx, false); -} - -void pfnEnsureClosedWrt(ProofNode* pn, - const std::vector<Node>& assumps, - const char* c, - const char* ctx) -{ - ensureClosedWrtInternal(Node::null(), nullptr, pn, assumps, c, ctx, false); -} - -} // namespace cvc5 diff --git a/src/expr/proof_ensure_closed.h b/src/expr/proof_ensure_closed.h deleted file mode 100644 index 3d126a4a1..000000000 --- a/src/expr/proof_ensure_closed.h +++ /dev/null @@ -1,73 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Debug checks for ensuring proofs are closed. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__EXPR__PROOF_ENSURE_CLOSED_H -#define CVC5__EXPR__PROOF_ENSURE_CLOSED_H - -#include "expr/node.h" - -namespace cvc5 { - -class ProofGenerator; -class ProofNode; - -/** - * Debug check closed on Trace c. Context ctx is string for debugging. - * This method throws an assertion failure if pg cannot provide a closed - * proof for fact proven. This is checked only if --proof-eager-checking - * is enabled or the Trace c is enabled. - * - * @param reqGen Whether we consider a null generator to be a failure. - */ -void pfgEnsureClosed(Node proven, - ProofGenerator* pg, - const char* c, - const char* ctx, - bool reqGen = true); - -/** - * Debug check closed with Trace c. Context ctx is string for debugging and - * assumps is the set of allowed open assertions. This method throws an - * assertion failure if pg cannot provide a proof for fact proven whose - * free assumptions are contained in assumps. - * - * @param reqGen Whether we consider a null generator to be a failure. - */ -void pfgEnsureClosedWrt(Node proven, - ProofGenerator* pg, - const std::vector<Node>& assumps, - const char* c, - const char* ctx, - bool reqGen = true); - -/** - * Debug check closed with Trace c, proof node versions. This gives an - * assertion failure if pn is not closed. Detailed information is printed - * on trace c. Context ctx is a string used for debugging. - */ -void pfnEnsureClosed(ProofNode* pn, const char* c, const char* ctx); -/** - * Same as above, but throws an assertion failure only if the free assumptions - * of pn are not contained in assumps. - */ -void pfnEnsureClosedWrt(ProofNode* pn, - const std::vector<Node>& assumps, - const char* c, - const char* ctx); -} // namespace cvc5 - -#endif /* CVC5__EXPR__PROOF_ENSURE_CLOSED_H */ diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp deleted file mode 100644 index 7c034c10d..000000000 --- a/src/expr/proof_generator.cpp +++ /dev/null @@ -1,77 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of proof generator utility. - */ - -#include "expr/proof_generator.h" - -#include <sstream> - -#include "expr/proof.h" -#include "expr/proof_node.h" -#include "expr/proof_node_algorithm.h" -#include "options/smt_options.h" - -namespace cvc5 { - -std::ostream& operator<<(std::ostream& out, CDPOverwrite opol) -{ - switch (opol) - { - case CDPOverwrite::ALWAYS: out << "ALWAYS"; break; - case CDPOverwrite::ASSUME_ONLY: out << "ASSUME_ONLY"; break; - case CDPOverwrite::NEVER: out << "NEVER"; break; - default: out << "CDPOverwrite:unknown"; break; - } - return out; -} - -ProofGenerator::ProofGenerator() {} - -ProofGenerator::~ProofGenerator() {} - -std::shared_ptr<ProofNode> ProofGenerator::getProofFor(Node f) -{ - Unreachable() << "ProofGenerator::getProofFor: " << identify() - << " has no implementation" << std::endl; - return nullptr; -} - -bool ProofGenerator::addProofTo(Node f, - CDProof* pf, - CDPOverwrite opolicy, - bool doCopy) -{ - Trace("pfgen") << "ProofGenerator::addProofTo: " << f << "..." << std::endl; - Assert(pf != nullptr); - // plug in the proof provided by the generator, if it exists - std::shared_ptr<ProofNode> apf = getProofFor(f); - if (apf != nullptr) - { - Trace("pfgen") << "...got proof " << *apf.get() << std::endl; - if (pf->addProof(apf, opolicy, doCopy)) - { - Trace("pfgen") << "...success!" << std::endl; - return true; - } - Trace("pfgen") << "...failed to add proof" << std::endl; - } - else - { - Trace("pfgen") << "...failed, no proof" << std::endl; - Assert(false) << "Failed to get proof from generator for fact " << f; - } - return false; -} - -} // namespace cvc5 diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h deleted file mode 100644 index 2e87ab756..000000000 --- a/src/expr/proof_generator.h +++ /dev/null @@ -1,113 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * The abstract proof generator class. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__EXPR__PROOF_GENERATOR_H -#define CVC5__EXPR__PROOF_GENERATOR_H - -#include "expr/node.h" - -namespace cvc5 { - -class CDProof; -class ProofNode; - -/** An overwrite policy for CDProof */ -enum class CDPOverwrite : uint32_t -{ - // always overwrite an existing step. - ALWAYS, - // overwrite ASSUME with non-ASSUME steps. - ASSUME_ONLY, - // never overwrite an existing step. - NEVER, -}; -/** Writes a overwrite policy name to a stream. */ -std::ostream& operator<<(std::ostream& out, CDPOverwrite opol); - -/** - * An abstract proof generator class. - * - * A proof generator is intended to be used as a utility e.g. in theory - * solvers for constructing and storing proofs internally. A theory may have - * multiple instances of ProofGenerator objects, e.g. if it has more than one - * way of justifying lemmas or conflicts. - * - * A proof generator has two main interfaces for generating proofs: - * (1) getProofFor, and (2) addProofTo. The latter is optional. - * - * The addProofTo method can be used as an optimization for avoiding - * the construction of the ProofNode for a given fact. - * - * If no implementation of addProofTo is provided, then addProofTo(f, pf) - * calls getProofFor(f) and links the topmost ProofNode of the returned proof - * into pf. Note this top-most ProofNode can be avoided in the addProofTo - * method. - */ -class ProofGenerator -{ - public: - ProofGenerator(); - virtual ~ProofGenerator(); - /** Get the proof for formula f - * - * This forces the proof generator to construct a proof for formula f and - * return it. If this is an "eager" proof generator, this function is expected - * to be implemented as a map lookup. If this is a "lazy" proof generator, - * this function is expected to invoke a proof producing procedure of the - * generator. - * - * It should be the case that hasProofFor(f) is true. - * - * @param f The fact to get the proof for. - * @return The proof for f. - */ - virtual std::shared_ptr<ProofNode> getProofFor(Node f); - /** - * Add the proof for formula f to proof pf. The proof of f is overwritten in - * pf based on the policy opolicy. - * - * @param f The fact to get the proof for. - * @param pf The CDProof object to add the proof to. - * @param opolicy The overwrite policy for adding to pf. - * @param doCopy Whether to do a deep copy of the proof steps into pf. - * @return True if this call was sucessful. - */ - virtual bool addProofTo(Node f, - CDProof* pf, - CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY, - bool doCopy = false); - /** - * Can we give the proof for formula f? This is used for debugging. This - * returns false if the generator cannot provide a proof of formula f. - * - * Also notice that this function does not require the proof for f to be - * constructed at the time of this call. Thus, if this is a "lazy" proof - * generator, it is expected that this call is implemented as a map lookup - * into the bookkeeping maintained by the generator only. - * - * Notice the default return value is true. In other words, a proof generator - * may choose to override this function to verify the construction, although - * we do not insist this is the case. - */ - virtual bool hasProofFor(Node f) { return true; } - /** Identify this generator (for debugging, etc..) */ - virtual std::string identify() const = 0; -}; - -} // namespace cvc5 - -#endif /* CVC5__EXPR__PROOF_GENERATOR_H */ diff --git a/src/expr/proof_node.cpp b/src/expr/proof_node.cpp deleted file mode 100644 index 92daad8ed..000000000 --- a/src/expr/proof_node.cpp +++ /dev/null @@ -1,72 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of proof node utility. - */ - -#include "expr/proof_node.h" - -#include "expr/proof_node_algorithm.h" -#include "expr/proof_node_to_sexpr.h" - -namespace cvc5 { - -ProofNode::ProofNode(PfRule id, - const std::vector<std::shared_ptr<ProofNode>>& children, - const std::vector<Node>& args) -{ - setValue(id, children, args); -} - -PfRule ProofNode::getRule() const { return d_rule; } - -const std::vector<std::shared_ptr<ProofNode>>& ProofNode::getChildren() const -{ - return d_children; -} - -const std::vector<Node>& ProofNode::getArguments() const { return d_args; } - -Node ProofNode::getResult() const { return d_proven; } - -bool ProofNode::isClosed() -{ - std::vector<Node> assumps; - expr::getFreeAssumptions(this, assumps); - return assumps.empty(); -} - -void ProofNode::setValue( - PfRule id, - const std::vector<std::shared_ptr<ProofNode>>& children, - const std::vector<Node>& args) -{ - d_rule = id; - d_children = children; - d_args = args; -} - -void ProofNode::printDebug(std::ostream& os) const -{ - // convert to sexpr and print - ProofNodeToSExpr pnts; - Node ps = pnts.convertToSExpr(this); - os << ps; -} - -std::ostream& operator<<(std::ostream& out, const ProofNode& pn) -{ - pn.printDebug(out); - return out; -} - -} // namespace cvc5 diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h deleted file mode 100644 index f8d71f703..000000000 --- a/src/expr/proof_node.h +++ /dev/null @@ -1,145 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Haniel Barbosa, Alex Ozdemir - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Proof node utility. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__EXPR__PROOF_NODE_H -#define CVC5__EXPR__PROOF_NODE_H - -#include <vector> - -#include "expr/node.h" -#include "expr/proof_rule.h" - -namespace cvc5 { - -class ProofNodeManager; -class ProofNode; - -// Alias for shared pointer to a proof node -using Pf = std::shared_ptr<ProofNode>; - -struct ProofNodeHashFunction -{ - inline size_t operator()(std::shared_ptr<ProofNode> pfn) const; -}; /* struct ProofNodeHashFunction */ - -/** A node in a proof - * - * A ProofNode represents a single step in a proof. It contains: - * (1) d_id, an identifier indicating the kind of inference, - * (2) d_children, the child ProofNode objects indicating its premises, - * (3) d_args, additional arguments used to determine the conclusion, - * (4) d_proven, cache of the formula that this ProofNode proves. - * - * Overall, a ProofNode and its children form a directed acyclic graph. - * - * A ProofNode is partially mutable in that (1), (2) and (3) can be - * modified. A motivating example of when this is useful is when a ProofNode - * is established to be a "hole" for something to be proven later. On the other - * hand, (4) is intended to be immutable. - * - * The method setValue is private and can be called by objects that manage - * ProofNode objects in trusted ways that ensure that the node maintains - * the invariant above. Furthermore, notice that this class is not responsible - * for setting d_proven; this is done externally by a ProofNodeManager class. - * - * Notice that all fields of ProofNode are stored in ***Skolem form***. Their - * correctness is checked in ***witness form*** (for details on this - * terminology, see expr/skolem_manager.h). As a simple example, say a - * theory solver has a term t, and wants to introduce a unit lemma (= k t) - * where k is a fresh Skolem variable. It creates this variable via: - * k = SkolemManager::mkPurifySkolem(t,"k"); - * A checked ProofNode for the fact (= k t) then may have fields: - * d_rule := MACRO_SR_PRED_INTRO, - * d_children := {}, - * d_args := {(= k t)} - * d_proven := (= k t). - * Its justification via the rule MACRO_SR_PRED_INTRO (see documentation - * in theory/builtin/proof_kinds) is in terms of the witness form of the - * argument: - * (= (witness ((z T)) (= z t)) t) - * which, by that rule's side condition, is such that: - * Rewriter::rewrite((= (witness ((z T)) (= z t)) t)) = true. - * Notice that the correctness of the rule is justified here by rewriting - * the witness form of (= k t). The conversion to/from witness form is - * managed by ProofRuleChecker::check. - * - * An external proof checker is expected to formalize the ProofNode only in - * terms of *witness* forms. - * - * However, the rest of cvc5 sees only the *Skolem* form of arguments and - * conclusions in ProofNode, since this is what is used throughout cvc5. - */ -class ProofNode -{ - friend class ProofNodeManager; - - public: - ProofNode(PfRule id, - const std::vector<std::shared_ptr<ProofNode>>& children, - const std::vector<Node>& args); - ~ProofNode() {} - /** get the rule of this proof node */ - PfRule getRule() const; - /** Get children */ - const std::vector<std::shared_ptr<ProofNode>>& getChildren() const; - /** Get arguments */ - const std::vector<Node>& getArguments() const; - /** get what this node proves, or the null node if this is an invalid proof */ - Node getResult() const; - /** - * Returns true if this is a closed proof (i.e. it has no free assumptions). - */ - bool isClosed(); - /** Print debug on output strem os */ - void printDebug(std::ostream& os) const; - - private: - /** - * Set value, called to overwrite the contents of this ProofNode with the - * given arguments. - */ - void setValue(PfRule id, - const std::vector<std::shared_ptr<ProofNode>>& children, - const std::vector<Node>& args); - /** The proof rule */ - PfRule d_rule; - /** The children of this proof node */ - std::vector<std::shared_ptr<ProofNode>> d_children; - /** arguments of this node */ - std::vector<Node> d_args; - /** The cache of the fact that has been proven, modifiable by ProofChecker */ - Node d_proven; -}; - -inline size_t ProofNodeHashFunction::operator()( - std::shared_ptr<ProofNode> pfn) const -{ - return pfn->getResult().getId() + static_cast<unsigned>(pfn->getRule()); -} - -/** - * Serializes a given proof node to the given stream. - * - * @param out the output stream to use - * @param pn the proof node to output to the stream - * @return the stream - */ -std::ostream& operator<<(std::ostream& out, const ProofNode& pn); - -} // namespace cvc5 - -#endif /* CVC5__EXPR__PROOF_NODE_H */ diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp deleted file mode 100644 index 4bb35b5dc..000000000 --- a/src/expr/proof_node_algorithm.cpp +++ /dev/null @@ -1,176 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Haniel Barbosa - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of proof node algorithm utilities. - */ - -#include "expr/proof_node_algorithm.h" - -#include "expr/proof_node.h" - -namespace cvc5 { -namespace expr { - -void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump) -{ - std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amap; - std::shared_ptr<ProofNode> spn = std::make_shared<ProofNode>( - pn->getRule(), pn->getChildren(), pn->getArguments()); - getFreeAssumptionsMap(spn, amap); - for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& p : - amap) - { - assump.push_back(p.first); - } -} - -void getFreeAssumptionsMap( - std::shared_ptr<ProofNode> pn, - std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap) -{ - // proof should not be cyclic - // visited set false after preorder traversal, true after postorder traversal - std::unordered_map<ProofNode*, bool> visited; - std::unordered_map<ProofNode*, bool>::iterator it; - std::vector<std::shared_ptr<ProofNode>> visit; - std::vector<std::shared_ptr<ProofNode>> traversing; - // Maps a bound assumption to the number of bindings it is under - // e.g. in (SCOPE (SCOPE (ASSUME x) (x y)) (y)), y would be mapped to 2 at - // (ASSUME x), and x would be mapped to 1. - // - // This map is used to track which nodes are in scope while traversing the - // DAG. The in-scope assumptions are keys in the map. They're removed when - // their binding count drops to zero. Let's annotate the above example to - // serve as an illustration: - // - // (SCOPE0 (SCOPE1 (ASSUME x) (x y)) (y)) - // - // This is how the map changes during the traversal: - // after previsiting SCOPE0: { y: 1 } - // after previsiting SCOPE1: { y: 2, x: 1 } - // at ASSUME: { y: 2, x: 1 } (so x is in scope!) - // after postvisiting SCOPE1: { y: 1 } - // after postvisiting SCOPE2: {} - // - std::unordered_map<Node, uint32_t> scopeDepth; - std::shared_ptr<ProofNode> cur; - visit.push_back(pn); - do - { - cur = visit.back(); - visit.pop_back(); - it = visited.find(cur.get()); - const std::vector<Node>& cargs = cur->getArguments(); - if (it == visited.end()) - { - PfRule id = cur->getRule(); - if (id == PfRule::ASSUME) - { - visited[cur.get()] = true; - Assert(cargs.size() == 1); - Node f = cargs[0]; - if (!scopeDepth.count(f)) - { - amap[f].push_back(cur); - } - } - else - { - if (id == PfRule::SCOPE) - { - // mark that its arguments are bound in the current scope - for (const Node& a : cargs) - { - scopeDepth[a] += 1; - } - // will need to unbind the variables below - } - // The following loop cannot be merged with the loop above because the - // same subproof - visited[cur.get()] = false; - visit.push_back(cur); - traversing.push_back(cur); - const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren(); - for (const std::shared_ptr<ProofNode>& cp : cs) - { - if (std::find(traversing.begin(), traversing.end(), cp) - != traversing.end()) - { - Unhandled() << "getFreeAssumptionsMap: cyclic proof! (use " - "--proof-eager-checking)" - << std::endl; - } - visit.push_back(cp); - } - } - } - else if (!it->second) - { - Assert(!traversing.empty()); - traversing.pop_back(); - visited[cur.get()] = true; - if (cur->getRule() == PfRule::SCOPE) - { - // unbind its assumptions - for (const Node& a : cargs) - { - auto scopeCt = scopeDepth.find(a); - Assert(scopeCt != scopeDepth.end()); - scopeCt->second -= 1; - if (scopeCt->second == 0) - { - scopeDepth.erase(scopeCt); - } - } - } - } - } while (!visit.empty()); -} - -bool containsSubproof(ProofNode* pn, ProofNode* pnc) -{ - std::unordered_set<const ProofNode*> visited; - return containsSubproof(pn, pnc, visited); -} - -bool containsSubproof(ProofNode* pn, - ProofNode* pnc, - std::unordered_set<const ProofNode*>& visited) -{ - std::unordered_map<const ProofNode*, bool>::iterator it; - std::vector<const ProofNode*> visit; - visit.push_back(pn); - const ProofNode* cur; - while (!visit.empty()) - { - cur = visit.back(); - visit.pop_back(); - if (visited.find(cur) == visited.end()) - { - visited.insert(cur); - if (cur == pnc) - { - return true; - } - const std::vector<std::shared_ptr<ProofNode>>& children = - cur->getChildren(); - for (const std::shared_ptr<ProofNode>& cp : children) - { - visit.push_back(cp.get()); - } - } - } - return false; -} - -} // namespace expr -} // namespace cvc5 diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h deleted file mode 100644 index 4c89dd4bc..000000000 --- a/src/expr/proof_node_algorithm.h +++ /dev/null @@ -1,76 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Haniel Barbosa, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Proof node algorithm utilities. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__EXPR__PROOF_NODE_ALGORITHM_H -#define CVC5__EXPR__PROOF_NODE_ALGORITHM_H - -#include <vector> - -#include "expr/node.h" - -namespace cvc5 { - -class ProofNode; - -namespace expr { - -/** - * This adds to the vector assump all formulas that are "free assumptions" of - * the proof whose root is ProofNode pn. A free assumption is a formula F - * that is an argument (in d_args) of a ProofNode whose kind is ASSUME, and - * that proof node is not beneath an application of SCOPE containing F as an - * argument. - * - * This traverses the structure of the dag represented by this ProofNode. - * Its implementation is analogous to expr::getFreeVariables. - * - * @param pn The proof node. - * @param assump The vector to add the free asumptions of pn to. - */ -void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump); -/** - * Same as above, but maps assumptions to the proof pointer(s) for that - * assumption. Notice that depending on how pn is constructed, there may be - * multiple ProofNode that are ASSUME proofs of the same assumption, which - * are each added to the range of the assumption. - * - * @param pn The proof node. - * @param amap The mapping to add the free asumptions of pn and their - * corresponding proof nodes to. - */ -void getFreeAssumptionsMap( - std::shared_ptr<ProofNode> pn, - std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap); - -/** - * @return true if pn contains pnc. - */ -bool containsSubproof(ProofNode* pn, ProofNode* pnc); - -/** - * Same as above, with a visited cache. - * - * @return true if pn contains pnc. - */ -bool containsSubproof(ProofNode* pn, - ProofNode* pnc, - std::unordered_set<const ProofNode*>& visited); - -} // namespace expr -} // namespace cvc5 - -#endif /* CVC5__EXPR__PROOF_NODE_ALGORITHM_H */ diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp deleted file mode 100644 index c2c72f35d..000000000 --- a/src/expr/proof_node_manager.cpp +++ /dev/null @@ -1,408 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Haniel Barbosa, Aina Niemetz - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of proof node manager. - */ - -#include "expr/proof_node_manager.h" - -#include <sstream> - -#include "expr/proof.h" -#include "expr/proof_checker.h" -#include "expr/proof_node.h" -#include "expr/proof_node_algorithm.h" -#include "options/proof_options.h" -#include "theory/rewriter.h" - -using namespace cvc5::kind; - -namespace cvc5 { - -ProofNodeManager::ProofNodeManager(ProofChecker* pc) - : d_checker(pc) -{ - d_true = NodeManager::currentNM()->mkConst(true); -} - -std::shared_ptr<ProofNode> ProofNodeManager::mkNode( - PfRule id, - const std::vector<std::shared_ptr<ProofNode>>& children, - const std::vector<Node>& args, - Node expected) -{ - Trace("pnm") << "ProofNodeManager::mkNode " << id << " {" << expected.getId() - << "} " << expected << "\n"; - Node res = checkInternal(id, children, args, expected); - if (res.isNull()) - { - // if it was invalid, then we return the null node - return nullptr; - } - // otherwise construct the proof node and set its proven field - std::shared_ptr<ProofNode> pn = - std::make_shared<ProofNode>(id, children, args); - pn->d_proven = res; - return pn; -} - -std::shared_ptr<ProofNode> ProofNodeManager::mkAssume(Node fact) -{ - Assert(!fact.isNull()); - Assert(fact.getType().isBoolean()); - return mkNode(PfRule::ASSUME, {}, {fact}, fact); -} - -std::shared_ptr<ProofNode> ProofNodeManager::mkTrans( - const std::vector<std::shared_ptr<ProofNode>>& children, Node expected) -{ - Assert(!children.empty()); - if (children.size() == 1) - { - Assert(expected.isNull() || children[0]->getResult() == expected); - return children[0]; - } - return mkNode(PfRule::TRANS, children, {}, expected); -} - -std::shared_ptr<ProofNode> ProofNodeManager::mkScope( - std::shared_ptr<ProofNode> pf, - std::vector<Node>& assumps, - bool ensureClosed, - bool doMinimize, - Node expected) -{ - if (!ensureClosed) - { - return mkNode(PfRule::SCOPE, {pf}, assumps, expected); - } - Trace("pnm-scope") << "ProofNodeManager::mkScope " << assumps << std::endl; - // we first ensure the assumptions are flattened - std::unordered_set<Node> ac{assumps.begin(), assumps.end()}; - // map from the rewritten form of assumptions to the original. This is only - // computed in the rare case when we need rewriting to match the - // assumptions. An example of this is for Boolean constant equalities in - // scoped proofs from the proof equality engine. - std::unordered_map<Node, Node> acr; - // whether we have compute the map above - bool computedAcr = false; - - // The free assumptions of the proof - std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap; - expr::getFreeAssumptionsMap(pf, famap); - std::unordered_set<Node> acu; - for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& - fa : famap) - { - Node a = fa.first; - if (ac.find(a) != ac.end()) - { - // already covered by an assumption - acu.insert(a); - continue; - } - // trivial assumption - if (a == d_true) - { - Trace("pnm-scope") << "- justify trivial True assumption\n"; - for (std::shared_ptr<ProofNode> pfs : fa.second) - { - Assert(pfs->getResult() == a); - updateNode(pfs.get(), PfRule::MACRO_SR_PRED_INTRO, {}, {a}); - } - Trace("pnm-scope") << "...finished" << std::endl; - acu.insert(a); - continue; - } - Trace("pnm-scope") << "- try matching free assumption " << a << "\n"; - // otherwise it may be due to symmetry? - Node aeqSym = CDProof::getSymmFact(a); - Trace("pnm-scope") << " - try sym " << aeqSym << "\n"; - Node aMatch; - if (!aeqSym.isNull() && ac.count(aeqSym)) - { - Trace("pnm-scope") << "- reorient assumption " << aeqSym << " via " << a - << " for " << fa.second.size() << " proof nodes" - << std::endl; - aMatch = aeqSym; - } - else - { - // Otherwise, may be derivable by rewriting. Note this is used in - // ensuring that proofs from the proof equality engine that involve - // equality with Boolean constants are closed. - if (!computedAcr) - { - computedAcr = true; - for (const Node& acc : ac) - { - Node accr = theory::Rewriter::rewrite(acc); - if (accr != acc) - { - acr[accr] = acc; - } - } - } - Node ar = theory::Rewriter::rewrite(a); - std::unordered_map<Node, Node>::iterator itr = acr.find(ar); - if (itr != acr.end()) - { - aMatch = itr->second; - } - } - - // if we found a match either by symmetry or rewriting, then we connect - // the assumption here. - if (!aMatch.isNull()) - { - std::shared_ptr<ProofNode> pfaa = mkAssume(aMatch); - // must correct the orientation on this leaf - std::vector<std::shared_ptr<ProofNode>> children; - children.push_back(pfaa); - for (std::shared_ptr<ProofNode> pfs : fa.second) - { - Assert(pfs->getResult() == a); - // use SYMM if possible - if (aMatch == aeqSym) - { - updateNode(pfs.get(), PfRule::SYMM, children, {}); - } - else - { - updateNode(pfs.get(), PfRule::MACRO_SR_PRED_TRANSFORM, children, {a}); - } - } - Trace("pnm-scope") << "...finished" << std::endl; - acu.insert(aMatch); - continue; - } - // If we did not find a match, it is an error, since all free assumptions - // should be arguments to SCOPE. - std::stringstream ss; - - bool dumpProofTraceOn = Trace.isOn("dump-proof-error"); - if (dumpProofTraceOn) - { - ss << "The proof : " << *pf << std::endl; - } - ss << std::endl << "Free assumption: " << a << std::endl; - for (const Node& aprint : ac) - { - ss << "- assumption: " << aprint << std::endl; - } - if (!dumpProofTraceOn) - { - ss << "Use -t dump-proof-error for details on proof" << std::endl; - } - Unreachable() << "Generated a proof that is not closed by the scope: " - << ss.str() << std::endl; - } - if (acu.size() < ac.size()) - { - // All assumptions should match a free assumption; if one does not, then - // the explanation could have been smaller. - for (const Node& a : ac) - { - if (acu.find(a) == acu.end()) - { - Notice() << "ProofNodeManager::mkScope: assumption " << a - << " does not match a free assumption in proof" << std::endl; - } - } - } - if (doMinimize && acu.size() < ac.size()) - { - assumps.clear(); - assumps.insert(assumps.end(), acu.begin(), acu.end()); - } - else if (ac.size() < assumps.size()) - { - // remove duplicates to avoid redundant literals in clauses - assumps.clear(); - assumps.insert(assumps.end(), ac.begin(), ac.end()); - } - Node minExpected; - NodeManager* nm = NodeManager::currentNM(); - Node exp; - if (assumps.empty()) - { - // SCOPE with no arguments is a no-op, just return original - return pf; - } - Node conc = pf->getResult(); - exp = assumps.size() == 1 ? assumps[0] : nm->mkNode(AND, assumps); - if (conc.isConst() && !conc.getConst<bool>()) - { - minExpected = exp.notNode(); - } - else - { - minExpected = nm->mkNode(IMPLIES, exp, conc); - } - return mkNode(PfRule::SCOPE, {pf}, assumps, minExpected); -} - -bool ProofNodeManager::updateNode( - ProofNode* pn, - PfRule id, - const std::vector<std::shared_ptr<ProofNode>>& children, - const std::vector<Node>& args) -{ - return updateNodeInternal(pn, id, children, args, true); -} - -bool ProofNodeManager::updateNode(ProofNode* pn, ProofNode* pnr) -{ - Assert(pn != nullptr); - Assert(pnr != nullptr); - if (pn->getResult() != pnr->getResult()) - { - return false; - } - // can shortcut re-check of rule - return updateNodeInternal( - pn, pnr->getRule(), pnr->getChildren(), pnr->getArguments(), false); -} - -Node ProofNodeManager::checkInternal( - PfRule id, - const std::vector<std::shared_ptr<ProofNode>>& children, - const std::vector<Node>& args, - Node expected) -{ - Node res; - if (d_checker) - { - // check with the checker, which takes expected as argument - res = d_checker->check(id, children, args, expected); - Assert(!res.isNull()) - << "ProofNodeManager::checkInternal: failed to check proof"; - } - else - { - // otherwise we trust the expected value, if it exists - Assert(!expected.isNull()) << "ProofNodeManager::checkInternal: no checker " - "or expected value provided"; - res = expected; - } - return res; -} - -ProofChecker* ProofNodeManager::getChecker() const { return d_checker; } - -std::shared_ptr<ProofNode> ProofNodeManager::clone( - std::shared_ptr<ProofNode> pn) -{ - const ProofNode* orig = pn.get(); - std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>> visited; - std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>>::iterator it; - std::vector<const ProofNode*> visit; - std::shared_ptr<ProofNode> cloned; - visit.push_back(orig); - const ProofNode* cur; - while (!visit.empty()) - { - cur = visit.back(); - it = visited.find(cur); - if (it == visited.end()) - { - visited[cur] = nullptr; - const std::vector<std::shared_ptr<ProofNode>>& children = - cur->getChildren(); - for (const std::shared_ptr<ProofNode>& cp : children) - { - visit.push_back(cp.get()); - } - continue; - } - visit.pop_back(); - if (it->second.get() == nullptr) - { - std::vector<std::shared_ptr<ProofNode>> cchildren; - const std::vector<std::shared_ptr<ProofNode>>& children = - cur->getChildren(); - for (const std::shared_ptr<ProofNode>& cp : children) - { - it = visited.find(cp.get()); - Assert(it != visited.end()); - Assert(it->second != nullptr); - cchildren.push_back(it->second); - } - cloned = std::make_shared<ProofNode>( - cur->getRule(), cchildren, cur->getArguments()); - visited[cur] = cloned; - // we trust the above cloning does not change what is proven - cloned->d_proven = cur->d_proven; - } - } - Assert(visited.find(orig) != visited.end()); - return visited[orig]; -} - -bool ProofNodeManager::updateNodeInternal( - ProofNode* pn, - PfRule id, - const std::vector<std::shared_ptr<ProofNode>>& children, - const std::vector<Node>& args, - bool needsCheck) -{ - Assert(pn != nullptr); - // ---------------- check for cyclic - if (options::proofEagerChecking()) - { - std::unordered_set<const ProofNode*> visited; - for (const std::shared_ptr<ProofNode>& cpc : children) - { - if (expr::containsSubproof(cpc.get(), pn, visited)) - { - std::stringstream ss; - ss << "ProofNodeManager::updateNode: attempting to make cyclic proof! " - << id << " " << pn->getResult() << ", children = " << std::endl; - for (const std::shared_ptr<ProofNode>& cp : children) - { - ss << " " << cp->getRule() << " " << cp->getResult() << std::endl; - } - ss << "Full children:" << std::endl; - for (const std::shared_ptr<ProofNode>& cp : children) - { - ss << " - "; - cp->printDebug(ss); - ss << std::endl; - } - Unreachable() << ss.str(); - } - } - } - // ---------------- end check for cyclic - - // should have already computed what is proven - Assert(!pn->d_proven.isNull()) - << "ProofNodeManager::updateProofNode: invalid proof provided"; - if (needsCheck) - { - // We expect to prove the same thing as before - Node res = checkInternal(id, children, args, pn->d_proven); - if (res.isNull()) - { - // if it was invalid, then we do not update - return false; - } - // proven field should already be the same as the result - Assert(res == pn->d_proven); - } - - // we update its value - pn->setValue(id, children, args); - return true; -} - -} // namespace cvc5 diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h deleted file mode 100644 index 853d22de7..000000000 --- a/src/expr/proof_node_manager.h +++ /dev/null @@ -1,206 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Haniel Barbosa, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Proof node manager utility. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__EXPR__PROOF_NODE_MANAGER_H -#define CVC5__EXPR__PROOF_NODE_MANAGER_H - -#include <vector> - -#include "expr/node.h" -#include "expr/proof_rule.h" - -namespace cvc5 { - -class ProofChecker; -class ProofNode; - -/** - * A manager for proof node objects. This is a trusted interface for creating - * and updating ProofNode objects. - * - * In more detail, we say a ProofNode is "well-formed (with respect to checker - * X)" if its d_proven field is non-null, and corresponds to the formula that - * the ProofNode proves according to X. The ProofNodeManager class constructs - * and update nodes that are well-formed with respect to its underlying checker. - * - * If no checker is provided, then the ProofNodeManager assigns the d_proven - * field of ProofNode based on the provided "expected" argument in mkNode below, - * which must be provided in this case. - * - * The ProofNodeManager is used as a trusted way of updating ProofNode objects - * via updateNode below. In particular, this method leaves the d_proven field - * unchanged and updates (if possible) the remaining content of a given proof - * node. - * - * Notice that ProofNode objects are mutable, and hence this class does not - * cache the results of mkNode. A version of this class that caches - * immutable version of ProofNode objects could be built as an extension - * or layer on top of this class. - */ -class ProofNodeManager -{ - public: - ProofNodeManager(ProofChecker* pc = nullptr); - ~ProofNodeManager() {} - /** - * This constructs a ProofNode with the given arguments. The expected - * argument, when provided, indicates the formula that the returned node - * is expected to prove. If we find that it does not, based on the underlying - * checker, this method returns nullptr. - * - * @param id The id of the proof node. - * @param children The children of the proof node. - * @param args The arguments of the proof node. - * @param expected (Optional) the expected conclusion of the proof node. - * @return the proof node, or nullptr if the given arguments do not - * consistute a proof of the expected conclusion according to the underlying - * checker, if both are provided. It also returns nullptr if neither the - * checker nor the expected field is provided, since in this case the - * conclusion is unknown. - */ - std::shared_ptr<ProofNode> mkNode( - PfRule id, - const std::vector<std::shared_ptr<ProofNode>>& children, - const std::vector<Node>& args, - Node expected = Node::null()); - /** - * Make the proof node corresponding to the assumption of fact. - * - * @param fact The fact to assume. - * @return The ASSUME proof of fact. - */ - std::shared_ptr<ProofNode> mkAssume(Node fact); - /** - * Make transitivity proof, where children contains one or more proofs of - * equalities that form an ordered chain. In other words, the vector children - * is a legal set of children for an application of TRANS. - */ - std::shared_ptr<ProofNode> mkTrans( - const std::vector<std::shared_ptr<ProofNode>>& children, - Node expected = Node::null()); - - /** - * Make scope having body pf and arguments (assumptions-to-close) assumps. - * If ensureClosed is true, then this method throws an assertion failure if - * the returned proof is not closed. This is the case if a free assumption - * of pf is missing from the vector assumps. - * - * For conveinence, the proof pf may be modified to ensure that the overall - * result is closed. For instance, given input: - * pf = TRANS( ASSUME( x=y ), ASSUME( y=z ) ) - * assumps = { y=x, y=z } - * This method will modify pf to be: - * pf = TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) ) - * so that y=x matches the free assumption. The returned proof is: - * SCOPE(TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) ) :args { y=x, y=z }) - * - * When ensureClosed is true, duplicates are eliminated from assumps. The - * reason for this is due to performance, since in this method, assumps is - * converted to an unordered_set to do the above check and hence it is a - * convienient time to eliminate duplicate literals. - * - * Additionally, if both ensureClosed and doMinimize are true, assumps is - * updated to contain exactly the free asumptions of pf. This also includes - * having no duplicates. Furthermore, if assumps is empty after minimization, - * this method is a no-op. - * - * In each case, the update vector assumps is passed as arguments to SCOPE. - * - * @param pf The body of the proof, - * @param assumps The assumptions-to-close of the scope, - * @param ensureClosed Whether to ensure that the proof is closed, - * @param doMinimize Whether to minimize assumptions. - * @param expected the node that the scope should prove. - * @return The scoped proof. - */ - std::shared_ptr<ProofNode> mkScope(std::shared_ptr<ProofNode> pf, - std::vector<Node>& assumps, - bool ensureClosed = true, - bool doMinimize = false, - Node expected = Node::null()); - /** - * This method updates pn to be a proof of the form <id>( children, args ), - * while maintaining its d_proven field. This method returns false if this - * proof manager is using a checker, and we compute that the above proof - * is not a proof of the fact that pn previously proved. - * - * @param pn The proof node to update. - * @param id The updated id of the proof node. - * @param children The updated children of the proof node. - * @param args The updated arguments of the proof node. - * @return true if the update was successful. - * - * Notice that updateNode always returns true if there is no underlying - * checker. - */ - bool updateNode(ProofNode* pn, - PfRule id, - const std::vector<std::shared_ptr<ProofNode>>& children, - const std::vector<Node>& args); - /** - * Update node pn to have the contents of pnr. It should be the case that - * pn and pnr prove the same fact, otherwise false is returned and pn is - * unchanged. - */ - bool updateNode(ProofNode* pn, ProofNode* pnr); - /** Get the underlying proof checker */ - ProofChecker* getChecker() const; - /** - * Clone a proof node, which creates a deep copy of pn and returns it. The - * dag structure of pn is the same as that in the returned proof node. - * - * @param pn The proof node to clone - * @return the cloned proof node. - */ - std::shared_ptr<ProofNode> clone(std::shared_ptr<ProofNode> pn); - - private: - /** The (optional) proof checker */ - ProofChecker* d_checker; - /** the true node */ - Node d_true; - /** Check internal - * - * This returns the result of proof checking a ProofNode with the provided - * arguments with an expected conclusion, which may not null if there is - * no expected conclusion. - * - * This throws an assertion error if we fail to check such a proof node, or - * if expected is provided (non-null) and is different what is proven by the - * other arguments. - */ - Node checkInternal(PfRule id, - const std::vector<std::shared_ptr<ProofNode>>& children, - const std::vector<Node>& args, - Node expected); - /** - * Update node internal, return true if successful. This is called by - * the update node methods above. The argument needsCheck is whether we - * need to check the correctness of the rule application. This is false - * for the updateNode routine where pnr is an (already checked) proof node. - */ - bool updateNodeInternal( - ProofNode* pn, - PfRule id, - const std::vector<std::shared_ptr<ProofNode>>& children, - const std::vector<Node>& args, - bool needsCheck); -}; - -} // namespace cvc5 - -#endif /* CVC5__EXPR__PROOF_NODE_H */ diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp deleted file mode 100644 index 033232959..000000000 --- a/src/expr/proof_node_to_sexpr.cpp +++ /dev/null @@ -1,148 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Haniel Barbosa, Aina Niemetz - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of proof node to s-expression. - */ - -#include "expr/proof_node_to_sexpr.h" - -#include <iostream> -#include <sstream> - -#include "expr/proof_node.h" -#include "options/proof_options.h" - -using namespace cvc5::kind; - -namespace cvc5 { - -ProofNodeToSExpr::ProofNodeToSExpr() -{ - NodeManager* nm = NodeManager::currentNM(); - d_conclusionMarker = nm->mkBoundVar(":conclusion", nm->sExprType()); - d_argsMarker = nm->mkBoundVar(":args", nm->sExprType()); -} - -Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn) -{ - NodeManager* nm = NodeManager::currentNM(); - std::map<const ProofNode*, Node>::iterator it; - std::vector<const ProofNode*> visit; - std::vector<const ProofNode*> traversing; - const ProofNode* cur; - visit.push_back(pn); - do - { - cur = visit.back(); - visit.pop_back(); - it = d_pnMap.find(cur); - - if (it == d_pnMap.end()) - { - d_pnMap[cur] = Node::null(); - traversing.push_back(cur); - visit.push_back(cur); - const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren(); - for (const std::shared_ptr<ProofNode>& cp : pc) - { - if (std::find(traversing.begin(), traversing.end(), cp.get()) - != traversing.end()) - { - Unhandled() << "ProofNodeToSExpr::convertToSExpr: cyclic proof! (use " - "--proof-eager-checking)" - << std::endl; - return Node::null(); - } - visit.push_back(cp.get()); - } - } - else if (it->second.isNull()) - { - Assert(!traversing.empty()); - traversing.pop_back(); - std::vector<Node> children; - // add proof rule - children.push_back(getOrMkPfRuleVariable(cur->getRule())); - if (options::proofPrintConclusion()) - { - children.push_back(d_conclusionMarker); - children.push_back(cur->getResult()); - } - const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren(); - for (const std::shared_ptr<ProofNode>& cp : pc) - { - it = d_pnMap.find(cp.get()); - Assert(it != d_pnMap.end()); - Assert(!it->second.isNull()); - children.push_back(it->second); - } - // add arguments - const std::vector<Node>& args = cur->getArguments(); - if (!args.empty()) - { - children.push_back(d_argsMarker); - // needed to ensure builtin operators are not treated as operators - // this can be the case for CONG where d_args may contain a builtin - // operator - std::vector<Node> argsSafe; - for (const Node& a : args) - { - Node av = a; - if (a.getNumChildren() == 0 - && NodeManager::operatorToKind(a) != UNDEFINED_KIND) - { - av = getOrMkNodeVariable(a); - } - argsSafe.push_back(av); - } - Node argsC = nm->mkNode(SEXPR, argsSafe); - children.push_back(argsC); - } - d_pnMap[cur] = nm->mkNode(SEXPR, children); - } - } while (!visit.empty()); - Assert(d_pnMap.find(pn) != d_pnMap.end()); - Assert(!d_pnMap.find(pn)->second.isNull()); - return d_pnMap[pn]; -} - -Node ProofNodeToSExpr::getOrMkPfRuleVariable(PfRule r) -{ - std::map<PfRule, Node>::iterator it = d_pfrMap.find(r); - if (it != d_pfrMap.end()) - { - return it->second; - } - std::stringstream ss; - ss << r; - NodeManager* nm = NodeManager::currentNM(); - Node var = nm->mkBoundVar(ss.str(), nm->sExprType()); - d_pfrMap[r] = var; - return var; -} - -Node ProofNodeToSExpr::getOrMkNodeVariable(Node n) -{ - std::map<Node, Node>::iterator it = d_nodeMap.find(n); - if (it != d_nodeMap.end()) - { - return it->second; - } - std::stringstream ss; - ss << n; - NodeManager* nm = NodeManager::currentNM(); - Node var = nm->mkBoundVar(ss.str(), nm->sExprType()); - d_nodeMap[n] = var; - return var; -} - -} // namespace cvc5 diff --git a/src/expr/proof_node_to_sexpr.h b/src/expr/proof_node_to_sexpr.h deleted file mode 100644 index d4cca8eae..000000000 --- a/src/expr/proof_node_to_sexpr.h +++ /dev/null @@ -1,70 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Haniel Barbosa, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Conversion from ProofNode to s-expressions. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__EXPR__PROOF_NODE_TO_SEXPR_H -#define CVC5__EXPR__PROOF_NODE_TO_SEXPR_H - -#include <map> - -#include "expr/node.h" -#include "expr/proof_rule.h" - -namespace cvc5 { - -class ProofNode; - -/** A class to convert ProofNode objects to s-expressions */ -class ProofNodeToSExpr -{ - public: - ProofNodeToSExpr(); - ~ProofNodeToSExpr() {} - /** Convert the given proof node to an s-expression - * - * This is useful for operations where it is useful to view a ProofNode as - * a Node. Printing is one such example, where a ProofNode can be printed - * as a dag after this conversion. - * - * The s-expression for a ProofNode has the form: - * (SEXPR (VAR "<d_rule>") S1 ... Sn (VAR ":args") (SEXPR <d_args>)) - * where S1, ..., Sn are the s-expressions for its <d_children>. - */ - Node convertToSExpr(const ProofNode* pn); - - private: - /** map proof rules to a variable */ - std::map<PfRule, Node> d_pfrMap; - /** Dummy ":args" marker */ - Node d_argsMarker; - /** Dummy ":conclusion" marker */ - Node d_conclusionMarker; - /** map proof nodes to their s-expression */ - std::map<const ProofNode*, Node> d_pnMap; - /** - * map nodes to a bound variable, used for nodes that have special AST status - * like builtin operators - */ - std::map<Node, Node> d_nodeMap; - /** get or make pf rule variable */ - Node getOrMkPfRuleVariable(PfRule r); - /** get or make node variable */ - Node getOrMkNodeVariable(Node n); -}; - -} // namespace cvc5 - -#endif /* CVC5__EXPR__PROOF_RULE_H */ diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp deleted file mode 100644 index e2fd0c566..000000000 --- a/src/expr/proof_node_updater.cpp +++ /dev/null @@ -1,258 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Haniel Barbosa - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of a utility for updating proof nodes. - */ - -#include "expr/proof_node_updater.h" - -#include "expr/lazy_proof.h" -#include "expr/proof_ensure_closed.h" -#include "expr/proof_node_algorithm.h" -#include "expr/proof_node_manager.h" - -namespace cvc5 { - -ProofNodeUpdaterCallback::ProofNodeUpdaterCallback() {} -ProofNodeUpdaterCallback::~ProofNodeUpdaterCallback() {} - -bool ProofNodeUpdaterCallback::update(Node res, - PfRule id, - const std::vector<Node>& children, - const std::vector<Node>& args, - CDProof* cdp, - bool& continueUpdate) -{ - return false; -} - -ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm, - ProofNodeUpdaterCallback& cb, - bool mergeSubproofs, - bool autoSym) - : d_pnm(pnm), - d_cb(cb), - d_debugFreeAssumps(false), - d_mergeSubproofs(mergeSubproofs), - d_autoSym(autoSym) -{ -} - -void ProofNodeUpdater::process(std::shared_ptr<ProofNode> pf) -{ - if (d_debugFreeAssumps) - { - if (Trace.isOn("pfnu-debug")) - { - Trace("pfnu-debug2") << "Initial proof: " << *pf.get() << std::endl; - Trace("pfnu-debug") << "ProofNodeUpdater::process" << std::endl; - Trace("pfnu-debug") << "Expected free assumptions: " << std::endl; - for (const Node& fa : d_freeAssumps) - { - Trace("pfnu-debug") << "- " << fa << std::endl; - } - std::vector<Node> assump; - expr::getFreeAssumptions(pf.get(), assump); - Trace("pfnu-debug") << "Current free assumptions: " << std::endl; - for (const Node& fa : assump) - { - Trace("pfnu-debug") << "- " << fa << std::endl; - } - } - } - std::vector<std::shared_ptr<ProofNode>> traversing; - processInternal(pf, d_freeAssumps, traversing); -} - -void ProofNodeUpdater::processInternal( - std::shared_ptr<ProofNode> pf, - const std::vector<Node>& fa, - std::vector<std::shared_ptr<ProofNode>>& traversing) -{ - Trace("pf-process") << "ProofNodeUpdater::process" << std::endl; - std::unordered_map<std::shared_ptr<ProofNode>, bool> visited; - std::unordered_map<std::shared_ptr<ProofNode>, bool>::iterator it; - std::vector<std::shared_ptr<ProofNode>> visit; - std::shared_ptr<ProofNode> cur; - visit.push_back(pf); - std::map<Node, std::shared_ptr<ProofNode>>::iterator itc; - // A cache from formulas to proof nodes that are in the current scope. - // Notice that we make a fresh recursive call to process if the current - // rule is SCOPE below. - std::map<Node, std::shared_ptr<ProofNode>> resCache; - Node res; - do - { - cur = visit.back(); - visit.pop_back(); - it = visited.find(cur); - res = cur->getResult(); - if (it == visited.end()) - { - if (d_mergeSubproofs) - { - itc = resCache.find(res); - if (itc != resCache.end()) - { - // already have a proof, merge it into this one - visited[cur] = true; - d_pnm->updateNode(cur.get(), itc->second.get()); - continue; - } - } - // run update to a fixed point - bool continueUpdate = true; - while (runUpdate(cur, fa, continueUpdate) && continueUpdate) - { - Trace("pf-process-debug") << "...updated proof." << std::endl; - } - visited[cur] = !continueUpdate; - if (!continueUpdate) - { - // no further changes should be made to cur according to the callback - Trace("pf-process-debug") - << "...marked to not continue update." << std::endl; - runFinalize(cur, fa, resCache); - continue; - } - traversing.push_back(cur); - visit.push_back(cur); - // If we are not the top-level proof, we were a scope, or became a scope - // after updating, we do a separate recursive call to this method. This - // allows us to properly track the assumptions in scope, which is - // important for example to merge or to determine updates based on free - // assumptions. - if (cur->getRule() == PfRule::SCOPE && cur != pf) - { - std::vector<Node> nfa; - nfa.insert(nfa.end(), fa.begin(), fa.end()); - const std::vector<Node>& args = cur->getArguments(); - nfa.insert(nfa.end(), args.begin(), args.end()); - Trace("pfnu-debug2") << "Process new scope with " << args << std::endl; - // Process in new call separately - processInternal(cur, nfa, traversing); - continue; - } - const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren(); - // now, process children - for (const std::shared_ptr<ProofNode>& cp : ccp) - { - if (std::find(traversing.begin(), traversing.end(), cp) - != traversing.end()) - { - Unhandled() - << "ProofNodeUpdater::processInternal: cyclic proof! (use " - "--proof-eager-checking)" - << std::endl; - } - visit.push_back(cp); - } - } - else if (!it->second) - { - Assert(!traversing.empty()); - traversing.pop_back(); - visited[cur] = true; - // finalize the node - runFinalize(cur, fa, resCache); - } - } while (!visit.empty()); - Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl; -} - -bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur, - const std::vector<Node>& fa, - bool& continueUpdate) -{ - // should it be updated? - if (!d_cb.shouldUpdate(cur, fa, continueUpdate)) - { - return false; - } - PfRule id = cur->getRule(); - // use CDProof to open a scope for which the callback updates - CDProof cpf(d_pnm, nullptr, "ProofNodeUpdater::CDProof", d_autoSym); - const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren(); - std::vector<Node> ccn; - for (const std::shared_ptr<ProofNode>& cp : cc) - { - Node cpres = cp->getResult(); - ccn.push_back(cpres); - // store in the proof - cpf.addProof(cp); - } - Node res = cur->getResult(); - Trace("pf-process-debug") - << "Updating (" << cur->getRule() << "): " << res << std::endl; - // only if the callback updated the node - if (d_cb.update(res, id, ccn, cur->getArguments(), &cpf, continueUpdate)) - { - std::shared_ptr<ProofNode> npn = cpf.getProofFor(res); - std::vector<Node> fullFa; - if (d_debugFreeAssumps) - { - expr::getFreeAssumptions(cur.get(), fullFa); - Trace("pfnu-debug") << "Original proof : " << *cur << std::endl; - } - // then, update the original proof node based on this one - Trace("pf-process-debug") << "Update node..." << std::endl; - d_pnm->updateNode(cur.get(), npn.get()); - Trace("pf-process-debug") << "...update node finished." << std::endl; - if (d_debugFreeAssumps) - { - fullFa.insert(fullFa.end(), fa.begin(), fa.end()); - // We have that npn is a node we occurring the final updated version of - // the proof. We can now debug based on the expected set of free - // assumptions. - Trace("pfnu-debug") << "Ensure update closed..." << std::endl; - pfnEnsureClosedWrt( - npn.get(), fullFa, "pfnu-debug", "ProofNodeUpdater:postupdate"); - } - Trace("pf-process-debug") << "..finished" << std::endl; - return true; - } - Trace("pf-process-debug") << "..finished" << std::endl; - return false; -} - -void ProofNodeUpdater::runFinalize( - std::shared_ptr<ProofNode> cur, - const std::vector<Node>& fa, - std::map<Node, std::shared_ptr<ProofNode>>& resCache) -{ - if (d_mergeSubproofs) - { - Node res = cur->getResult(); - // cache result if we are merging subproofs - resCache[res] = cur; - } - if (d_debugFreeAssumps) - { - // We have that npn is a node we occurring the final updated version of - // the proof. We can now debug based on the expected set of free - // assumptions. - Trace("pfnu-debug") << "Ensure update closed..." << std::endl; - pfnEnsureClosedWrt( - cur.get(), fa, "pfnu-debug", "ProofNodeUpdater:finalize"); - } -} - -void ProofNodeUpdater::setDebugFreeAssumptions( - const std::vector<Node>& freeAssumps) -{ - d_freeAssumps.clear(); - d_freeAssumps.insert( - d_freeAssumps.end(), freeAssumps.begin(), freeAssumps.end()); - d_debugFreeAssumps = true; -} - -} // namespace cvc5 diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h deleted file mode 100644 index 215c61210..000000000 --- a/src/expr/proof_node_updater.h +++ /dev/null @@ -1,164 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Haniel Barbosa, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * A utility for updating proof nodes. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__EXPR__PROOF_NODE_UPDATER_H -#define CVC5__EXPR__PROOF_NODE_UPDATER_H - -#include <map> -#include <memory> - -#include "expr/node.h" -#include "expr/proof_node.h" - -namespace cvc5 { - -class CDProof; -class ProofNode; -class ProofNodeManager; - -/** - * A virtual callback class for updating ProofNode. An example use case of this - * class is to eliminate a proof rule by expansion. - */ -class ProofNodeUpdaterCallback -{ - public: - ProofNodeUpdaterCallback(); - virtual ~ProofNodeUpdaterCallback(); - /** Should proof pn be updated? - * - * @param pn the proof node that maybe should be updated - * @param fa the assumptions in scope - * @param continueUpdate whether we should continue recursively updating pn - * @return whether we should run the update method on pn - */ - virtual bool shouldUpdate(std::shared_ptr<ProofNode> pn, - const std::vector<Node>& fa, - bool& continueUpdate) = 0; - /** - * Update the proof rule application, store steps in cdp. Return true if - * the proof changed. It can be assumed that cdp contains proofs of each - * fact in children. - * - * If continueUpdate is set to false in this method, then the resulting - * proof (the proof of res in cdp) is *not* called back to update by the - * proof node updater, nor are its children recursed. Otherwise, by default, - * the proof node updater will continue updating the resulting proof and will - * recursively update its children. This is analogous to marking REWRITE_DONE - * in a rewrite response. - */ - virtual bool update(Node res, - PfRule id, - const std::vector<Node>& children, - const std::vector<Node>& args, - CDProof* cdp, - bool& continueUpdate); -}; - -/** - * A generic class for updating ProofNode. It is parameterized by a callback - * class. Its process method runs this callback on all subproofs of a provided - * ProofNode application that meet some criteria - * (ProofNodeUpdaterCallback::shouldUpdate) - * and overwrites them based on the update procedure of the callback - * (ProofNodeUpdaterCallback::update), which uses local CDProof objects that - * should be filled in the callback for each ProofNode to update. This update - * process is applied in a *pre-order* traversal. - */ -class ProofNodeUpdater -{ - public: - /** - * @param pnm The proof node manager we are using - * @param cb The callback to apply to each node - * @param mergeSubproofs Whether to automatically merge subproofs within - * the same SCOPE that prove the same fact. - * @param autoSym Whether intermediate CDProof objects passed to updater - * callbacks automatically introduce SYMM steps. - */ - ProofNodeUpdater(ProofNodeManager* pnm, - ProofNodeUpdaterCallback& cb, - bool mergeSubproofs = false, - bool autoSym = true); - /** - * Post-process, which performs the main post-processing technique described - * above. - */ - void process(std::shared_ptr<ProofNode> pf); - - /** - * Set free assumptions to freeAssumps. This indicates that we expect - * the proof we are processing to have free assumptions that are in - * freeAssumps. This enables checking when this is violated, which is - * expensive in general. It is not recommended that this method is called - * by default. - */ - void setDebugFreeAssumptions(const std::vector<Node>& freeAssumps); - - private: - /** The proof node manager */ - ProofNodeManager* d_pnm; - /** The callback */ - ProofNodeUpdaterCallback& d_cb; - /** - * Post-process, which performs the main post-processing technique described - * above. - * - * @param pf The proof to process - * @param fa The assumptions of the scope that fa is a subproof of with - * respect to the original proof. For example, if (SCOPE P :args (A B)), we - * may call this method on P with fa = { A, B }. - * @param traversing The list of proof nodes we are currently traversing - * beneath. This is used for checking for cycles in the overall proof. - */ - void processInternal(std::shared_ptr<ProofNode> pf, - const std::vector<Node>& fa, - std::vector<std::shared_ptr<ProofNode>>& traversing); - /** - * Update proof node cur based on the callback. This modifies curr using - * ProofNodeManager::updateNode based on the proof node constructed to - * replace it by the callback. Return true if cur was updated. If - * continueUpdate is updated to false, then cur is not updated further - * and its children are not traversed. - */ - bool runUpdate(std::shared_ptr<ProofNode> cur, - const std::vector<Node>& fa, - bool& continueUpdate); - /** - * Finalize the node cur. This is called at the moment that it is established - * that cur will appear in the final proof. We do any final debug checking - * and add it to the results cache resCache if we are merging subproofs. - */ - void runFinalize(std::shared_ptr<ProofNode> cur, - const std::vector<Node>& fa, - std::map<Node, std::shared_ptr<ProofNode>>& resCache); - /** Are we debugging free assumptions? */ - bool d_debugFreeAssumps; - /** The initial free assumptions */ - std::vector<Node> d_freeAssumps; - /** Whether we are merging subproofs */ - bool d_mergeSubproofs; - /** - * Whether intermediate CDProof objects passed to updater callbacks - * automatically introduce SYMM steps. - */ - bool d_autoSym; -}; - -} // namespace cvc5 - -#endif diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp deleted file mode 100644 index f4e8078dc..000000000 --- a/src/expr/proof_rule.cpp +++ /dev/null @@ -1,258 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Haniel Barbosa, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of proof rule. - */ - -#include "expr/proof_rule.h" - -#include <iostream> - -namespace cvc5 { - -const char* toString(PfRule id) -{ - switch (id) - { - //================================================= Core rules - case PfRule::ASSUME: return "ASSUME"; - case PfRule::SCOPE: return "SCOPE"; - case PfRule::SUBS: return "SUBS"; - case PfRule::REWRITE: return "REWRITE"; - case PfRule::EVALUATE: return "EVALUATE"; - case PfRule::MACRO_SR_EQ_INTRO: return "MACRO_SR_EQ_INTRO"; - case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO"; - case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM"; - case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM"; - case PfRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM"; - //================================================= Trusted rules - case PfRule::THEORY_LEMMA: return "THEORY_LEMMA"; - case PfRule::THEORY_REWRITE: return "THEORY_REWRITE"; - case PfRule::PREPROCESS: return "PREPROCESS"; - case PfRule::PREPROCESS_LEMMA: return "PREPROCESS_LEMMA"; - case PfRule::THEORY_PREPROCESS: return "THEORY_PREPROCESS"; - case PfRule::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA"; - case PfRule::THEORY_EXPAND_DEF: return "THEORY_EXPAND_DEF"; - case PfRule::WITNESS_AXIOM: return "WITNESS_AXIOM"; - case PfRule::TRUST_REWRITE: return "TRUST_REWRITE"; - case PfRule::TRUST_SUBS: return "TRUST_SUBS"; - case PfRule::TRUST_SUBS_MAP: return "TRUST_SUBS_MAP"; - //================================================= Boolean rules - case PfRule::RESOLUTION: return "RESOLUTION"; - case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION"; - case PfRule::FACTORING: return "FACTORING"; - case PfRule::REORDERING: return "REORDERING"; - case PfRule::MACRO_RESOLUTION: return "MACRO_RESOLUTION"; - case PfRule::MACRO_RESOLUTION_TRUST: return "MACRO_RESOLUTION_TRUST"; - case PfRule::SPLIT: return "SPLIT"; - case PfRule::EQ_RESOLVE: return "EQ_RESOLVE"; - case PfRule::MODUS_PONENS: return "MODUS_PONENS"; - case PfRule::NOT_NOT_ELIM: return "NOT_NOT_ELIM"; - case PfRule::CONTRA: return "CONTRA"; - case PfRule::AND_ELIM: return "AND_ELIM"; - case PfRule::AND_INTRO: return "AND_INTRO"; - case PfRule::NOT_OR_ELIM: return "NOT_OR_ELIM"; - case PfRule::IMPLIES_ELIM: return "IMPLIES_ELIM"; - case PfRule::NOT_IMPLIES_ELIM1: return "NOT_IMPLIES_ELIM1"; - case PfRule::NOT_IMPLIES_ELIM2: return "NOT_IMPLIES_ELIM2"; - case PfRule::EQUIV_ELIM1: return "EQUIV_ELIM1"; - case PfRule::EQUIV_ELIM2: return "EQUIV_ELIM2"; - case PfRule::NOT_EQUIV_ELIM1: return "NOT_EQUIV_ELIM1"; - case PfRule::NOT_EQUIV_ELIM2: return "NOT_EQUIV_ELIM2"; - case PfRule::XOR_ELIM1: return "XOR_ELIM1"; - case PfRule::XOR_ELIM2: return "XOR_ELIM2"; - case PfRule::NOT_XOR_ELIM1: return "NOT_XOR_ELIM1"; - case PfRule::NOT_XOR_ELIM2: return "NOT_XOR_ELIM2"; - case PfRule::ITE_ELIM1: return "ITE_ELIM1"; - case PfRule::ITE_ELIM2: return "ITE_ELIM2"; - case PfRule::NOT_ITE_ELIM1: return "NOT_ITE_ELIM1"; - case PfRule::NOT_ITE_ELIM2: return "NOT_ITE_ELIM2"; - //================================================= De Morgan rules - case PfRule::NOT_AND: return "NOT_AND"; - //================================================= CNF rules - case PfRule::CNF_AND_POS: return "CNF_AND_POS"; - case PfRule::CNF_AND_NEG: return "CNF_AND_NEG"; - case PfRule::CNF_OR_POS: return "CNF_OR_POS"; - case PfRule::CNF_OR_NEG: return "CNF_OR_NEG"; - case PfRule::CNF_IMPLIES_POS: return "CNF_IMPLIES_POS"; - case PfRule::CNF_IMPLIES_NEG1: return "CNF_IMPLIES_NEG1"; - case PfRule::CNF_IMPLIES_NEG2: return "CNF_IMPLIES_NEG2"; - case PfRule::CNF_EQUIV_POS1: return "CNF_EQUIV_POS1"; - case PfRule::CNF_EQUIV_POS2: return "CNF_EQUIV_POS2"; - case PfRule::CNF_EQUIV_NEG1: return "CNF_EQUIV_NEG1"; - case PfRule::CNF_EQUIV_NEG2: return "CNF_EQUIV_NEG2"; - case PfRule::CNF_XOR_POS1: return "CNF_XOR_POS1"; - case PfRule::CNF_XOR_POS2: return "CNF_XOR_POS2"; - case PfRule::CNF_XOR_NEG1: return "CNF_XOR_NEG1"; - case PfRule::CNF_XOR_NEG2: return "CNF_XOR_NEG2"; - case PfRule::CNF_ITE_POS1: return "CNF_ITE_POS1"; - case PfRule::CNF_ITE_POS2: return "CNF_ITE_POS2"; - case PfRule::CNF_ITE_POS3: return "CNF_ITE_POS3"; - case PfRule::CNF_ITE_NEG1: return "CNF_ITE_NEG1"; - case PfRule::CNF_ITE_NEG2: return "CNF_ITE_NEG2"; - case PfRule::CNF_ITE_NEG3: return "CNF_ITE_NEG3"; - //================================================= Equality rules - case PfRule::REFL: return "REFL"; - case PfRule::SYMM: return "SYMM"; - case PfRule::TRANS: return "TRANS"; - case PfRule::CONG: return "CONG"; - case PfRule::TRUE_INTRO: return "TRUE_INTRO"; - case PfRule::TRUE_ELIM: return "TRUE_ELIM"; - case PfRule::FALSE_INTRO: return "FALSE_INTRO"; - case PfRule::FALSE_ELIM: return "FALSE_ELIM"; - case PfRule::HO_APP_ENCODE: return "HO_APP_ENCODE"; - case PfRule::HO_CONG: return "HO_CONG"; - //================================================= Array rules - case PfRule::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE"; - case PfRule::ARRAYS_READ_OVER_WRITE_CONTRA: - return "ARRAYS_READ_OVER_WRITE_CONTRA"; - case PfRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1"; - case PfRule::ARRAYS_EXT: return "ARRAYS_EXT"; - case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST"; - //================================================= Bit-Vector rules - case PfRule::BV_BITBLAST: return "BV_BITBLAST"; - case PfRule::BV_BITBLAST_CONST: return "BV_BITBLAST_CONST"; - case PfRule::BV_BITBLAST_VAR: return "BV_BITBLAST_VAR"; - case PfRule::BV_BITBLAST_EQUAL: return "BV_BITBLAST_EQUAL"; - case PfRule::BV_BITBLAST_ULT: return "BV_BITBLAST_ULT"; - case PfRule::BV_BITBLAST_ULE: return "BV_BITBLAST_ULE"; - case PfRule::BV_BITBLAST_UGT: return "BV_BITBLAST_UGT"; - case PfRule::BV_BITBLAST_UGE: return "BV_BITBLAST_UGE"; - case PfRule::BV_BITBLAST_SLT: return "BV_BITBLAST_SLT"; - case PfRule::BV_BITBLAST_SLE: return "BV_BITBLAST_SLE"; - case PfRule::BV_BITBLAST_SGT: return "BV_BITBLAST_SGT"; - case PfRule::BV_BITBLAST_SGE: return "BV_BITBLAST_SGE"; - case PfRule::BV_BITBLAST_NOT: return "BV_BITBLAST_NOT"; - case PfRule::BV_BITBLAST_CONCAT: return "BV_BITBLAST_CONCAT"; - case PfRule::BV_BITBLAST_AND: return "BV_BITBLAST_AND"; - case PfRule::BV_BITBLAST_OR: return "BV_BITBLAST_OR"; - case PfRule::BV_BITBLAST_XOR: return "BV_BITBLAST_XOR"; - case PfRule::BV_BITBLAST_XNOR: return "BV_BITBLAST_XNOR"; - case PfRule::BV_BITBLAST_NAND: return "BV_BITBLAST_NAND"; - case PfRule::BV_BITBLAST_NOR: return "BV_BITBLAST_NOR"; - case PfRule::BV_BITBLAST_COMP: return "BV_BITBLAST_COMP"; - case PfRule::BV_BITBLAST_MULT: return "BV_BITBLAST_MULT"; - case PfRule::BV_BITBLAST_ADD: return "BV_BITBLAST_ADD"; - case PfRule::BV_BITBLAST_SUB: return "BV_BITBLAST_SUB"; - case PfRule::BV_BITBLAST_NEG: return "BV_BITBLAST_NEG"; - case PfRule::BV_BITBLAST_UDIV: return "BV_BITBLAST_UDIV"; - case PfRule::BV_BITBLAST_UREM: return "BV_BITBLAST_UREM"; - case PfRule::BV_BITBLAST_SDIV: return "BV_BITBLAST_SDIV"; - case PfRule::BV_BITBLAST_SREM: return "BV_BITBLAST_SREM"; - case PfRule::BV_BITBLAST_SMOD: return "BV_BITBLAST_SMOD"; - case PfRule::BV_BITBLAST_SHL: return "BV_BITBLAST_SHL"; - case PfRule::BV_BITBLAST_LSHR: return "BV_BITBLAST_LSHR"; - case PfRule::BV_BITBLAST_ASHR: return "BV_BITBLAST_ASHR"; - case PfRule::BV_BITBLAST_ULTBV: return "BV_BITBLAST_ULTBV"; - case PfRule::BV_BITBLAST_SLTBV: return "BV_BITBLAST_SLTBV"; - case PfRule::BV_BITBLAST_ITE: return "BV_BITBLAST_ITE"; - case PfRule::BV_BITBLAST_EXTRACT: return "BV_BITBLAST_EXTRACT"; - case PfRule::BV_BITBLAST_REPEAT: return "BV_BITBLAST_REPEAT"; - case PfRule::BV_BITBLAST_ZERO_EXTEND: return "BV_BITBLAST_ZERO_EXTEND"; - case PfRule::BV_BITBLAST_SIGN_EXTEND: return "BV_BITBLAST_SIGN_EXTEND"; - case PfRule::BV_BITBLAST_ROTATE_RIGHT: return "BV_BITBLAST_ROTATE_RIGHT"; - case PfRule::BV_BITBLAST_ROTATE_LEFT: return "BV_BITBLAST_ROTATE_LEFT"; - case PfRule::BV_EAGER_ATOM: return "BV_EAGER_ATOM"; - //================================================= Datatype rules - case PfRule::DT_UNIF: return "DT_UNIF"; - case PfRule::DT_INST: return "DT_INST"; - case PfRule::DT_COLLAPSE: return "DT_COLLAPSE"; - case PfRule::DT_SPLIT: return "DT_SPLIT"; - case PfRule::DT_CLASH: return "DT_CLASH"; - case PfRule::DT_TRUST: return "DT_TRUST"; - //================================================= Quantifiers rules - case PfRule::SKOLEM_INTRO: return "SKOLEM_INTRO"; - case PfRule::EXISTS_INTRO: return "EXISTS_INTRO"; - case PfRule::SKOLEMIZE: return "SKOLEMIZE"; - case PfRule::INSTANTIATE: return "INSTANTIATE"; - //================================================= String rules - case PfRule::CONCAT_EQ: return "CONCAT_EQ"; - case PfRule::CONCAT_UNIFY: return "CONCAT_UNIFY"; - case PfRule::CONCAT_CONFLICT: return "CONCAT_CONFLICT"; - case PfRule::CONCAT_SPLIT: return "CONCAT_SPLIT"; - case PfRule::CONCAT_CSPLIT: return "CONCAT_CSPLIT"; - case PfRule::CONCAT_LPROP: return "CONCAT_LPROP"; - case PfRule::CONCAT_CPROP: return "CONCAT_CPROP"; - case PfRule::STRING_DECOMPOSE: return "STRING_DECOMPOSE"; - case PfRule::STRING_LENGTH_POS: return "STRING_LENGTH_POS"; - case PfRule::STRING_LENGTH_NON_EMPTY: return "STRING_LENGTH_NON_EMPTY"; - case PfRule::STRING_REDUCTION: return "STRING_REDUCTION"; - case PfRule::STRING_EAGER_REDUCTION: return "STRING_EAGER_REDUCTION"; - case PfRule::RE_INTER: return "RE_INTER"; - case PfRule::RE_UNFOLD_POS: return "RE_UNFOLD_POS"; - case PfRule::RE_UNFOLD_NEG: return "RE_UNFOLD_NEG"; - case PfRule::RE_UNFOLD_NEG_CONCAT_FIXED: - return "RE_UNFOLD_NEG_CONCAT_FIXED"; - case PfRule::RE_ELIM: return "RE_ELIM"; - case PfRule::STRING_CODE_INJ: return "STRING_CODE_INJ"; - case PfRule::STRING_SEQ_UNIT_INJ: return "STRING_SEQ_UNIT_INJ"; - case PfRule::STRING_TRUST: return "STRING_TRUST"; - //================================================= Arith rules - case PfRule::MACRO_ARITH_SCALE_SUM_UB: - return "ARITH_SCALE_SUM_UPPER_BOUNDS"; - case PfRule::ARITH_SUM_UB: return "ARITH_SUM_UB"; - case PfRule::ARITH_TRICHOTOMY: return "ARITH_TRICHOTOMY"; - case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB"; - case PfRule::INT_TIGHT_UB: return "INT_TIGHT_UB"; - case PfRule::INT_TRUST: return "INT_TRUST"; - case PfRule::ARITH_MULT_SIGN: return "ARITH_MULT_SIGN"; - case PfRule::ARITH_MULT_POS: return "ARITH_MULT_POS"; - case PfRule::ARITH_MULT_NEG: return "ARITH_MULT_NEG"; - case PfRule::ARITH_MULT_TANGENT: return "ARITH_MULT_TANGENT"; - case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM"; - case PfRule::ARITH_TRANS_PI: return "ARITH_TRANS_PI"; - case PfRule::ARITH_TRANS_EXP_NEG: return "ARITH_TRANS_EXP_NEG"; - case PfRule::ARITH_TRANS_EXP_POSITIVITY: - return "ARITH_TRANS_EXP_POSITIVITY"; - case PfRule::ARITH_TRANS_EXP_SUPER_LIN: return "ARITH_TRANS_EXP_SUPER_LIN"; - case PfRule::ARITH_TRANS_EXP_ZERO: return "ARITH_TRANS_EXP_ZERO"; - case PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG: - return "ARITH_TRANS_EXP_APPROX_ABOVE_NEG"; - case PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS: - return "ARITH_TRANS_EXP_APPROX_ABOVE_POS"; - case PfRule::ARITH_TRANS_EXP_APPROX_BELOW: - return "ARITH_TRANS_EXP_APPROX_BELOW"; - case PfRule::ARITH_TRANS_SINE_BOUNDS: return "ARITH_TRANS_SINE_BOUNDS"; - case PfRule::ARITH_TRANS_SINE_SHIFT: return "ARITH_TRANS_SINE_SHIFT"; - case PfRule::ARITH_TRANS_SINE_SYMMETRY: return "ARITH_TRANS_SINE_SYMMETRY"; - case PfRule::ARITH_TRANS_SINE_TANGENT_ZERO: - return "ARITH_TRANS_SINE_TANGENT_ZERO"; - case PfRule::ARITH_TRANS_SINE_TANGENT_PI: - return "ARITH_TRANS_SINE_TANGENT_PI"; - case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG: - return "ARITH_TRANS_SINE_APPROX_ABOVE_NEG"; - case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS: - return "ARITH_TRANS_SINE_APPROX_ABOVE_POS"; - case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG: - return "ARITH_TRANS_SINE_APPROX_BELOW_NEG"; - case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS: - return "ARITH_TRANS_SINE_APPROX_BELOW_POS"; - case PfRule::ARITH_NL_CAD_DIRECT: return "ARITH_NL_CAD_DIRECT"; - case PfRule::ARITH_NL_CAD_RECURSIVE: return "ARITH_NL_CAD_RECURSIVE"; - //================================================= Unknown rule - case PfRule::UNKNOWN: return "UNKNOWN"; - default: return "?"; - } -} - -std::ostream& operator<<(std::ostream& out, PfRule id) -{ - out << toString(id); - return out; -} - -size_t PfRuleHashFunction::operator()(PfRule id) const -{ - return static_cast<size_t>(id); -} - -} // namespace cvc5 diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h deleted file mode 100644 index 9771dda31..000000000 --- a/src/expr/proof_rule.h +++ /dev/null @@ -1,1453 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Haniel Barbosa, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Proof rule enumeration. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__EXPR__PROOF_RULE_H -#define CVC5__EXPR__PROOF_RULE_H - -#include <iosfwd> - -namespace cvc5 { - -/** - * An enumeration for proof rules. This enumeration is analogous to Kind for - * Node objects. In the documentation below, P:F denotes a ProofNode that - * proves formula F. - * - * Conceptually, the following proof rules form a calculus whose target - * user is the Node-level theory solvers. This means that the rules below - * are designed to reason about, among other things, common operations on Node - * objects like Rewriter::rewrite or Node::substitute. It is intended to be - * translated or printed in other formats. - * - * The following PfRule values include core rules and those categorized by - * theory, including the theory of equality. - * - * The "core rules" include two distinguished rules which have special status: - * (1) ASSUME, which represents an open leaf in a proof. - * (2) SCOPE, which closes the scope of assumptions. - * The core rules additionally correspond to generic operations that are done - * internally on nodes, e.g. calling Rewriter::rewrite. - * - * Rules with prefix MACRO_ are those that can be defined in terms of other - * rules. These exist for convienience. We provide their definition in the line - * "Macro:". - */ -enum class PfRule : uint32_t -{ - //================================================= Core rules - //======================== Assume and Scope - // ======== Assumption (a leaf) - // Children: none - // Arguments: (F) - // -------------- - // Conclusion: F - // - // This rule has special status, in that an application of assume is an - // open leaf in a proof that is not (yet) justified. An assume leaf is - // analogous to a free variable in a term, where we say "F is a free - // assumption in proof P" if it contains an application of F that is not - // bound by SCOPE (see below). - ASSUME, - // ======== Scope (a binder for assumptions) - // Children: (P:F) - // Arguments: (F1, ..., Fn) - // -------------- - // Conclusion: (=> (and F1 ... Fn) F) or (not (and F1 ... Fn)) if F is false - // - // This rule has a dual purpose with ASSUME. It is a way to close - // assumptions in a proof. We require that F1 ... Fn are free assumptions in - // P and say that F1, ..., Fn are not free in (SCOPE P). In other words, they - // are bound by this application. For example, the proof node: - // (SCOPE (ASSUME F) :args F) - // has the conclusion (=> F F) and has no free assumptions. More generally, a - // proof with no free assumptions always concludes a valid formula. - SCOPE, - - //======================== Builtin theory (common node operations) - // ======== Substitution - // Children: (P1:F1, ..., Pn:Fn) - // Arguments: (t, (ids)?) - // --------------------------------------------------------------- - // Conclusion: (= t t*sigma{ids}(Fn)*...*sigma{ids}(F1)) - // where sigma{ids}(Fi) are substitutions, which notice are applied in - // reverse order. - // Notice that ids is a MethodId identifier, which determines how to convert - // the formulas F1, ..., Fn into substitutions. - SUBS, - // ======== Rewrite - // Children: none - // Arguments: (t, (idr)?) - // ---------------------------------------- - // Conclusion: (= t Rewriter{idr}(t)) - // where idr is a MethodId identifier, which determines the kind of rewriter - // to apply, e.g. Rewriter::rewrite. - REWRITE, - // ======== Evaluate - // Children: none - // Arguments: (t) - // ---------------------------------------- - // Conclusion: (= t Evaluator::evaluate(t)) - // Note this is equivalent to: - // (REWRITE t MethodId::RW_EVALUATE) - EVALUATE, - // ======== Substitution + Rewriting equality introduction - // - // In this rule, we provide a term t and conclude that it is equal to its - // rewritten form under a (proven) substitution. - // - // Children: (P1:F1, ..., Pn:Fn) - // Arguments: (t, (ids (ida (idr)?)?)?) - // --------------------------------------------------------------- - // Conclusion: (= t t') - // where - // t' is - // Rewriter{idr}(t*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)) - // - // In other words, from the point of view of Skolem forms, this rule - // transforms t to t' by standard substitution + rewriting. - // - // The arguments ids, ida and idr are optional and specify the identifier of - // the substitution, the substitution application and rewriter respectively to - // be used. For details, see theory/builtin/proof_checker.h. - MACRO_SR_EQ_INTRO, - // ======== Substitution + Rewriting predicate introduction - // - // In this rule, we provide a formula F and conclude it, under the condition - // that it rewrites to true under a proven substitution. - // - // Children: (P1:F1, ..., Pn:Fn) - // Arguments: (F, (ids (ida (idr)?)?)?) - // --------------------------------------------------------------- - // Conclusion: F - // where - // Rewriter{idr}(F*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)) == true - // where ids and idr are method identifiers. - // - // More generally, this rule also holds when: - // Rewriter::rewrite(toOriginal(F')) == true - // where F' is the result of the left hand side of the equality above. Here, - // notice that we apply rewriting on the original form of F', meaning that - // this rule may conclude an F whose Skolem form is justified by the - // definition of its (fresh) Skolem variables. For example, this rule may - // justify the conclusion (= k t) where k is the purification Skolem for t, - // e.g. where the original form of k is t. - // - // Furthermore, notice that the rewriting and substitution is applied only - // within the side condition, meaning the rewritten form of the original form - // of F does not escape this rule. - MACRO_SR_PRED_INTRO, - // ======== Substitution + Rewriting predicate elimination - // - // In this rule, if we have proven a formula F, then we may conclude its - // rewritten form under a proven substitution. - // - // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn) - // Arguments: ((ids (ida (idr)?)?)?) - // ---------------------------------------- - // Conclusion: F' - // where - // F' is - // Rewriter{idr}(F*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)). - // where ids and idr are method identifiers. - // - // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO. - MACRO_SR_PRED_ELIM, - // ======== Substitution + Rewriting predicate transform - // - // In this rule, if we have proven a formula F, then we may provide a formula - // G and conclude it if F and G are equivalent after rewriting under a proven - // substitution. - // - // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn) - // Arguments: (G, (ids (ida (idr)?)?)?) - // ---------------------------------------- - // Conclusion: G - // where - // Rewriter{idr}(F*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)) == - // Rewriter{idr}(G*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)) - // - // More generally, this rule also holds when: - // Rewriter::rewrite(toOriginal(F')) == Rewriter::rewrite(toOriginal(G')) - // where F' and G' are the result of each side of the equation above. Here, - // original forms are used in a similar manner to MACRO_SR_PRED_INTRO above. - MACRO_SR_PRED_TRANSFORM, - //================================================= Processing rules - // ======== Remove Term Formulas Axiom - // Children: none - // Arguments: (t) - // --------------------------------------------------------------- - // Conclusion: RemoveTermFormulas::getAxiomFor(t). - REMOVE_TERM_FORMULA_AXIOM, - - //================================================= Trusted rules - // ======== Theory lemma - // Children: none - // Arguments: (F, tid) - // --------------------------------------------------------------- - // Conclusion: F - // where F is a (T-valid) theory lemma generated by theory with TheoryId tid. - // This is a "coarse-grained" rule that is used as a placeholder if a theory - // did not provide a proof for a lemma or conflict. - THEORY_LEMMA, - // ======== Theory Rewrite - // Children: none - // Arguments: (F, tid, rid) - // ---------------------------------------- - // Conclusion: F - // where F is an equality of the form (= t t') where t' is obtained by - // applying the kind of rewriting given by the method identifier rid, which - // is one of: - // { RW_REWRITE_THEORY_PRE, RW_REWRITE_THEORY_POST, RW_REWRITE_EQ_EXT } - // Notice that the checker for this rule does not replay the rewrite to ensure - // correctness, since theory rewriter methods are not static. For example, - // the quantifiers rewriter involves constructing new bound variables that are - // not guaranteed to be consistent on each call. - THEORY_REWRITE, - // The remaining rules in this section have the signature of a "trusted rule": - // - // Children: none - // Arguments: (F) - // --------------------------------------------------------------- - // Conclusion: F - // - // where F is an equality of the form t = t' where t was replaced by t' - // based on some preprocessing pass, or otherwise F was added as a new - // assertion by some preprocessing pass. - PREPROCESS, - // where F was added as a new assertion by some preprocessing pass. - PREPROCESS_LEMMA, - // where F is an equality of the form t = Theory::ppRewrite(t) for some - // theory. Notice this is a "trusted" rule. - THEORY_PREPROCESS, - // where F was added as a new assertion by theory preprocessing. - THEORY_PREPROCESS_LEMMA, - // where F is an equality of the form t = t' where t was replaced by t' - // based on theory expand definitions. - THEORY_EXPAND_DEF, - // where F is an existential (exists ((x T)) (P x)) used for introducing - // a witness term (witness ((x T)) (P x)). - WITNESS_AXIOM, - // where F is an equality (= t t') that holds by a form of rewriting that - // could not be replayed during proof postprocessing. - TRUST_REWRITE, - // where F is an equality (= t t') that holds by a form of substitution that - // could not be replayed during proof postprocessing. - TRUST_SUBS, - // where F is an equality (= t t') that holds by a form of substitution that - // could not be determined by the TrustSubstitutionMap. - TRUST_SUBS_MAP, - // ========= SAT Refutation for assumption-based unsat cores - // Children: (P1, ..., Pn) - // Arguments: none - // --------------------- - // Conclusion: false - // Note: P1, ..., Pn correspond to the unsat core determined by the SAT - // solver. - SAT_REFUTATION, - - //================================================= Boolean rules - // ======== Resolution - // Children: - // (P1:C1, P2:C2) - // Arguments: (pol, L) - // --------------------- - // Conclusion: C - // where - // - C1 and C2 are nodes viewed as clauses, i.e., either an OR node with - // each children viewed as a literal or a node viewed as a literal. Note - // that an OR node could also be a literal. - // - pol is either true or false, representing the polarity of the pivot on - // the first clause - // - L is the pivot of the resolution, which occurs as is (resp. under a - // NOT) in C1 and negatively (as is) in C2 if pol = true (pol = false). - // C is a clause resulting from collecting all the literals in C1, minus the - // first occurrence of the pivot or its negation, and C2, minus the first - // occurrence of the pivot or its negation, according to the policy above. - // If the resulting clause has a single literal, that literal itself is the - // result; if it has no literals, then the result is false; otherwise it's - // an OR node of the resulting literals. - // - // Note that it may be the case that the pivot does not occur in the - // clauses. In this case the rule is not unsound, but it does not correspond - // to resolution but rather to a weakening of the clause that did not have a - // literal eliminated. - RESOLUTION, - // ======== N-ary Resolution - // Children: (P1:C_1, ..., Pm:C_n) - // Arguments: (pol_1, L_1, ..., pol_{n-1}, L_{n-1}) - // --------------------- - // Conclusion: C - // where - // - let C_1 ... C_n be nodes viewed as clauses, as defined above - // - let "C_1 <>_{L,pol} C_2" represent the resolution of C_1 with C_2 with - // pivot L and polarity pol, as defined above - // - let C_1' = C_1 (from P1), - // - for each i > 1, let C_i' = C_{i-1} <>_{L_{i-1}, pol_{i-1}} C_i' - // The result of the chain resolution is C = C_n' - CHAIN_RESOLUTION, - // ======== Factoring - // Children: (P:C1) - // Arguments: () - // --------------------- - // Conclusion: C2 - // where - // Set representations of C1 and C2 is the same and the number of literals in - // C2 is smaller than that of C1 - FACTORING, - // ======== Reordering - // Children: (P:C1) - // Arguments: (C2) - // --------------------- - // Conclusion: C2 - // where - // Set representations of C1 and C2 are the same and the number of literals - // in C2 is the same of that of C1 - REORDERING, - // ======== N-ary Resolution + Factoring + Reordering - // Children: (P1:C_1, ..., Pm:C_n) - // Arguments: (C, pol_1, L_1, ..., pol_{n-1}, L_{n-1}) - // --------------------- - // Conclusion: C - // where - // - let C_1 ... C_n be nodes viewed as clauses, as defined in RESOLUTION - // - let "C_1 <>_{L,pol} C_2" represent the resolution of C_1 with C_2 with - // pivot L and polarity pol, as defined in RESOLUTION - // - let C_1' be equal, in its set representation, to C_1 (from P1), - // - for each i > 1, let C_i' be equal, it its set representation, to - // C_{i-1} <>_{L_{i-1}, pol_{i-1}} C_i' - // The result of the chain resolution is C, which is equal, in its set - // representation, to C_n' - MACRO_RESOLUTION, - // As above but not checked - MACRO_RESOLUTION_TRUST, - - // ======== Split - // Children: none - // Arguments: (F) - // --------------------- - // Conclusion: (or F (not F)) - SPLIT, - // ======== Equality resolution - // Children: (P1:F1, P2:(= F1 F2)) - // Arguments: none - // --------------------- - // Conclusion: (F2) - // Note this can optionally be seen as a macro for EQUIV_ELIM1+RESOLUTION. - EQ_RESOLVE, - // ======== Modus ponens - // Children: (P1:F1, P2:(=> F1 F2)) - // Arguments: none - // --------------------- - // Conclusion: (F2) - // Note this can optionally be seen as a macro for IMPLIES_ELIM+RESOLUTION. - MODUS_PONENS, - // ======== Double negation elimination - // Children: (P:(not (not F))) - // Arguments: none - // --------------------- - // Conclusion: (F) - NOT_NOT_ELIM, - // ======== Contradiction - // Children: (P1:F P2:(not F)) - // Arguments: () - // --------------------- - // Conclusion: false - CONTRA, - // ======== And elimination - // Children: (P:(and F1 ... Fn)) - // Arguments: (i) - // --------------------- - // Conclusion: (Fi) - AND_ELIM, - // ======== And introduction - // Children: (P1:F1 ... Pn:Fn)) - // Arguments: () - // --------------------- - // Conclusion: (and P1 ... Pn) - AND_INTRO, - // ======== Not Or elimination - // Children: (P:(not (or F1 ... Fn))) - // Arguments: (i) - // --------------------- - // Conclusion: (not Fi) - NOT_OR_ELIM, - // ======== Implication elimination - // Children: (P:(=> F1 F2)) - // Arguments: () - // --------------------- - // Conclusion: (or (not F1) F2) - IMPLIES_ELIM, - // ======== Not Implication elimination version 1 - // Children: (P:(not (=> F1 F2))) - // Arguments: () - // --------------------- - // Conclusion: (F1) - NOT_IMPLIES_ELIM1, - // ======== Not Implication elimination version 2 - // Children: (P:(not (=> F1 F2))) - // Arguments: () - // --------------------- - // Conclusion: (not F2) - NOT_IMPLIES_ELIM2, - // ======== Equivalence elimination version 1 - // Children: (P:(= F1 F2)) - // Arguments: () - // --------------------- - // Conclusion: (or (not F1) F2) - EQUIV_ELIM1, - // ======== Equivalence elimination version 2 - // Children: (P:(= F1 F2)) - // Arguments: () - // --------------------- - // Conclusion: (or F1 (not F2)) - EQUIV_ELIM2, - // ======== Not Equivalence elimination version 1 - // Children: (P:(not (= F1 F2))) - // Arguments: () - // --------------------- - // Conclusion: (or F1 F2) - NOT_EQUIV_ELIM1, - // ======== Not Equivalence elimination version 2 - // Children: (P:(not (= F1 F2))) - // Arguments: () - // --------------------- - // Conclusion: (or (not F1) (not F2)) - NOT_EQUIV_ELIM2, - // ======== XOR elimination version 1 - // Children: (P:(xor F1 F2))) - // Arguments: () - // --------------------- - // Conclusion: (or F1 F2) - XOR_ELIM1, - // ======== XOR elimination version 2 - // Children: (P:(xor F1 F2))) - // Arguments: () - // --------------------- - // Conclusion: (or (not F1) (not F2)) - XOR_ELIM2, - // ======== Not XOR elimination version 1 - // Children: (P:(not (xor F1 F2))) - // Arguments: () - // --------------------- - // Conclusion: (or F1 (not F2)) - NOT_XOR_ELIM1, - // ======== Not XOR elimination version 2 - // Children: (P:(not (xor F1 F2))) - // Arguments: () - // --------------------- - // Conclusion: (or (not F1) F2) - NOT_XOR_ELIM2, - // ======== ITE elimination version 1 - // Children: (P:(ite C F1 F2)) - // Arguments: () - // --------------------- - // Conclusion: (or (not C) F1) - ITE_ELIM1, - // ======== ITE elimination version 2 - // Children: (P:(ite C F1 F2)) - // Arguments: () - // --------------------- - // Conclusion: (or C F2) - ITE_ELIM2, - // ======== Not ITE elimination version 1 - // Children: (P:(not (ite C F1 F2))) - // Arguments: () - // --------------------- - // Conclusion: (or (not C) (not F1)) - NOT_ITE_ELIM1, - // ======== Not ITE elimination version 1 - // Children: (P:(not (ite C F1 F2))) - // Arguments: () - // --------------------- - // Conclusion: (or C (not F2)) - NOT_ITE_ELIM2, - - //================================================= De Morgan rules - // ======== Not And - // Children: (P:(not (and F1 ... Fn)) - // Arguments: () - // --------------------- - // Conclusion: (or (not F1) ... (not Fn)) - NOT_AND, - //================================================= CNF rules - // ======== CNF And Pos - // Children: () - // Arguments: ((and F1 ... Fn), i) - // --------------------- - // Conclusion: (or (not (and F1 ... Fn)) Fi) - CNF_AND_POS, - // ======== CNF And Neg - // Children: () - // Arguments: ((and F1 ... Fn)) - // --------------------- - // Conclusion: (or (and F1 ... Fn) (not F1) ... (not Fn)) - CNF_AND_NEG, - // ======== CNF Or Pos - // Children: () - // Arguments: ((or F1 ... Fn)) - // --------------------- - // Conclusion: (or (not (or F1 ... Fn)) F1 ... Fn) - CNF_OR_POS, - // ======== CNF Or Neg - // Children: () - // Arguments: ((or F1 ... Fn), i) - // --------------------- - // Conclusion: (or (or F1 ... Fn) (not Fi)) - CNF_OR_NEG, - // ======== CNF Implies Pos - // Children: () - // Arguments: ((implies F1 F2)) - // --------------------- - // Conclusion: (or (not (implies F1 F2)) (not F1) F2) - CNF_IMPLIES_POS, - // ======== CNF Implies Neg version 1 - // Children: () - // Arguments: ((implies F1 F2)) - // --------------------- - // Conclusion: (or (implies F1 F2) F1) - CNF_IMPLIES_NEG1, - // ======== CNF Implies Neg version 2 - // Children: () - // Arguments: ((implies F1 F2)) - // --------------------- - // Conclusion: (or (implies F1 F2) (not F2)) - CNF_IMPLIES_NEG2, - // ======== CNF Equiv Pos version 1 - // Children: () - // Arguments: ((= F1 F2)) - // --------------------- - // Conclusion: (or (not (= F1 F2)) (not F1) F2) - CNF_EQUIV_POS1, - // ======== CNF Equiv Pos version 2 - // Children: () - // Arguments: ((= F1 F2)) - // --------------------- - // Conclusion: (or (not (= F1 F2)) F1 (not F2)) - CNF_EQUIV_POS2, - // ======== CNF Equiv Neg version 1 - // Children: () - // Arguments: ((= F1 F2)) - // --------------------- - // Conclusion: (or (= F1 F2) F1 F2) - CNF_EQUIV_NEG1, - // ======== CNF Equiv Neg version 2 - // Children: () - // Arguments: ((= F1 F2)) - // --------------------- - // Conclusion: (or (= F1 F2) (not F1) (not F2)) - CNF_EQUIV_NEG2, - // ======== CNF Xor Pos version 1 - // Children: () - // Arguments: ((xor F1 F2)) - // --------------------- - // Conclusion: (or (not (xor F1 F2)) F1 F2) - CNF_XOR_POS1, - // ======== CNF Xor Pos version 2 - // Children: () - // Arguments: ((xor F1 F2)) - // --------------------- - // Conclusion: (or (not (xor F1 F2)) (not F1) (not F2)) - CNF_XOR_POS2, - // ======== CNF Xor Neg version 1 - // Children: () - // Arguments: ((xor F1 F2)) - // --------------------- - // Conclusion: (or (xor F1 F2) (not F1) F2) - CNF_XOR_NEG1, - // ======== CNF Xor Neg version 2 - // Children: () - // Arguments: ((xor F1 F2)) - // --------------------- - // Conclusion: (or (xor F1 F2) F1 (not F2)) - CNF_XOR_NEG2, - // ======== CNF ITE Pos version 1 - // Children: () - // Arguments: ((ite C F1 F2)) - // --------------------- - // Conclusion: (or (not (ite C F1 F2)) (not C) F1) - CNF_ITE_POS1, - // ======== CNF ITE Pos version 2 - // Children: () - // Arguments: ((ite C F1 F2)) - // --------------------- - // Conclusion: (or (not (ite C F1 F2)) C F2) - CNF_ITE_POS2, - // ======== CNF ITE Pos version 3 - // Children: () - // Arguments: ((ite C F1 F2)) - // --------------------- - // Conclusion: (or (not (ite C F1 F2)) F1 F2) - CNF_ITE_POS3, - // ======== CNF ITE Neg version 1 - // Children: () - // Arguments: ((ite C F1 F2)) - // --------------------- - // Conclusion: (or (ite C F1 F2) (not C) (not F1)) - CNF_ITE_NEG1, - // ======== CNF ITE Neg version 2 - // Children: () - // Arguments: ((ite C F1 F2)) - // --------------------- - // Conclusion: (or (ite C F1 F2) C (not F2)) - CNF_ITE_NEG2, - // ======== CNF ITE Neg version 3 - // Children: () - // Arguments: ((ite C F1 F2)) - // --------------------- - // Conclusion: (or (ite C F1 F2) (not F1) (not F2)) - CNF_ITE_NEG3, - - //================================================= Equality rules - // ======== Reflexive - // Children: none - // Arguments: (t) - // --------------------- - // Conclusion: (= t t) - REFL, - // ======== Symmetric - // Children: (P:(= t1 t2)) or (P:(not (= t1 t2))) - // Arguments: none - // ----------------------- - // Conclusion: (= t2 t1) or (not (= t2 t1)) - SYMM, - // ======== Transitivity - // Children: (P1:(= t1 t2), ..., Pn:(= t{n-1} tn)) - // Arguments: none - // ----------------------- - // Conclusion: (= t1 tn) - TRANS, - // ======== Congruence - // Children: (P1:(= t1 s1), ..., Pn:(= tn sn)) - // Arguments: (<kind> f?) - // --------------------------------------------- - // Conclusion: (= (<kind> f? t1 ... tn) (<kind> f? s1 ... sn)) - // Notice that f must be provided iff <kind> is a parameterized kind, e.g. - // APPLY_UF. The actual node for <kind> is constructible via - // ProofRuleChecker::mkKindNode. - CONG, - // ======== True intro - // Children: (P:F) - // Arguments: none - // ---------------------------------------- - // Conclusion: (= F true) - TRUE_INTRO, - // ======== True elim - // Children: (P:(= F true)) - // Arguments: none - // ---------------------------------------- - // Conclusion: F - TRUE_ELIM, - // ======== False intro - // Children: (P:(not F)) - // Arguments: none - // ---------------------------------------- - // Conclusion: (= F false) - FALSE_INTRO, - // ======== False elim - // Children: (P:(= F false)) - // Arguments: none - // ---------------------------------------- - // Conclusion: (not F) - FALSE_ELIM, - // ======== HO trust - // Children: none - // Arguments: (t) - // --------------------- - // Conclusion: (= t TheoryUfRewriter::getHoApplyForApplyUf(t)) - // For example, this rule concludes (f x y) = (HO_APPLY (HO_APPLY f x) y) - HO_APP_ENCODE, - // ======== Congruence - // Children: (P1:(= f g), P2:(= t1 s1), ..., Pn+1:(= tn sn)) - // Arguments: () - // --------------------------------------------- - // Conclusion: (= (f t1 ... tn) (g s1 ... sn)) - // Notice that this rule is only used when the application kinds are APPLY_UF. - HO_CONG, - - //================================================= Array rules - // ======== Read over write - // Children: (P:(not (= i1 i2))) - // Arguments: ((select (store a i2 e) i1)) - // ---------------------------------------- - // Conclusion: (= (select (store a i2 e) i1) (select a i1)) - ARRAYS_READ_OVER_WRITE, - // ======== Read over write, contrapositive - // Children: (P:(not (= (select (store a i2 e) i1) (select a i1))) - // Arguments: none - // ---------------------------------------- - // Conclusion: (= i1 i2) - ARRAYS_READ_OVER_WRITE_CONTRA, - // ======== Read over write 1 - // Children: none - // Arguments: ((select (store a i e) i)) - // ---------------------------------------- - // Conclusion: (= (select (store a i e) i) e) - ARRAYS_READ_OVER_WRITE_1, - // ======== Extensionality - // Children: (P:(not (= a b))) - // Arguments: none - // ---------------------------------------- - // Conclusion: (not (= (select a k) (select b k))) - // where k is arrays::SkolemCache::getExtIndexSkolem((not (= a b))). - ARRAYS_EXT, - // ======== Array Trust - // Children: (P1 ... Pn) - // Arguments: (F) - // --------------------- - // Conclusion: F - ARRAYS_TRUST, - - //================================================= Bit-Vector rules - // Note: bitblast() represents the result of the bit-blasted term as a - // bit-vector consisting of the output bits of the bit-blasted circuit - // representation of the term. Terms are bit-blasted according to the - // strategies defined in - // theory/bv/bitblast/bitblast_strategies_template.h. - // ======== Bitblast - // Children: none - // Arguments: (t) - // --------------------- - // Conclusion: (= t bitblast(t)) - BV_BITBLAST, - // ======== Bitblast Bit-Vector Constant - // Children: none - // Arguments: (= t bitblast(t)) - // --------------------- - // Conclusion: (= t bitblast(t)) - BV_BITBLAST_CONST, - // ======== Bitblast Bit-Vector Variable - // Children: none - // Arguments: (= t bitblast(t)) - // --------------------- - // Conclusion: (= t bitblast(t)) - BV_BITBLAST_VAR, - // ======== Bitblast Bit-Vector Terms - // TODO cvc4-projects issue #275 - // Children: none - // Arguments: (= (KIND bitblast(child_1) ... bitblast(child_n)) bitblast(t)) - // --------------------- - // Conclusion: (= (KIND bitblast(child_1) ... bitblast(child_n)) bitblast(t)) - BV_BITBLAST_EQUAL, - BV_BITBLAST_ULT, - BV_BITBLAST_ULE, - BV_BITBLAST_UGT, - BV_BITBLAST_UGE, - BV_BITBLAST_SLT, - BV_BITBLAST_SLE, - BV_BITBLAST_SGT, - BV_BITBLAST_SGE, - BV_BITBLAST_NOT, - BV_BITBLAST_CONCAT, - BV_BITBLAST_AND, - BV_BITBLAST_OR, - BV_BITBLAST_XOR, - BV_BITBLAST_XNOR, - BV_BITBLAST_NAND, - BV_BITBLAST_NOR, - BV_BITBLAST_COMP, - BV_BITBLAST_MULT, - BV_BITBLAST_ADD, - BV_BITBLAST_SUB, - BV_BITBLAST_NEG, - BV_BITBLAST_UDIV, - BV_BITBLAST_UREM, - BV_BITBLAST_SDIV, - BV_BITBLAST_SREM, - BV_BITBLAST_SMOD, - BV_BITBLAST_SHL, - BV_BITBLAST_LSHR, - BV_BITBLAST_ASHR, - BV_BITBLAST_ULTBV, - BV_BITBLAST_SLTBV, - BV_BITBLAST_ITE, - BV_BITBLAST_EXTRACT, - BV_BITBLAST_REPEAT, - BV_BITBLAST_ZERO_EXTEND, - BV_BITBLAST_SIGN_EXTEND, - BV_BITBLAST_ROTATE_RIGHT, - BV_BITBLAST_ROTATE_LEFT, - // ======== Eager Atom - // Children: none - // Arguments: (F) - // --------------------- - // Conclusion: (= F F[0]) - // where F is of kind BITVECTOR_EAGER_ATOM - BV_EAGER_ATOM, - - //================================================= Datatype rules - // ======== Unification - // Children: (P:(= (C t1 ... tn) (C s1 ... sn))) - // Arguments: (i) - // ---------------------------------------- - // Conclusion: (= ti si) - // where C is a constructor. - DT_UNIF, - // ======== Instantiate - // Children: none - // Arguments: (t, n) - // ---------------------------------------- - // Conclusion: (= ((_ is C) t) (= t (C (sel_1 t) ... (sel_n t)))) - // where C is the n^th constructor of the type of T, and (_ is C) is the - // discriminator (tester) for C. - DT_INST, - // ======== Collapse - // Children: none - // Arguments: ((sel_i (C_j t_1 ... t_n))) - // ---------------------------------------- - // Conclusion: (= (sel_i (C_j t_1 ... t_n)) r) - // where C_j is a constructor, r is t_i if sel_i is a correctly applied - // selector, or TypeNode::mkGroundTerm() of the proper type otherwise. Notice - // that the use of mkGroundTerm differs from the rewriter which uses - // mkGroundValue in this case. - DT_COLLAPSE, - // ======== Split - // Children: none - // Arguments: (t) - // ---------------------------------------- - // Conclusion: (or ((_ is C1) t) ... ((_ is Cn) t)) - DT_SPLIT, - // ======== Clash - // Children: (P1:((_ is Ci) t), P2: ((_ is Cj) t)) - // Arguments: none - // ---------------------------------------- - // Conclusion: false - // for i != j. - DT_CLASH, - // ======== Datatype Trust - // Children: (P1 ... Pn) - // Arguments: (F) - // --------------------- - // Conclusion: F - DT_TRUST, - - //================================================= Quantifiers rules - // ======== Skolem intro - // Children: none - // Arguments: (k) - // ---------------------------------------- - // Conclusion: (= k t) - // where t is the original form of skolem k. - SKOLEM_INTRO, - // ======== Exists intro - // Children: (P:F[t]) - // Arguments: ((exists ((x T)) F[x])) - // ---------------------------------------- - // Conclusion: (exists ((x T)) F[x]) - // This rule verifies that F[x] indeed matches F[t] with a substitution - // over x. - EXISTS_INTRO, - // ======== Skolemize - // Children: (P:(exists ((x1 T1) ... (xn Tn)) F)) - // Arguments: none - // ---------------------------------------- - // Conclusion: F*sigma - // sigma maps x1 ... xn to their representative skolems obtained by - // SkolemManager::mkSkolemize, returned in the skolems argument of that - // method. Alternatively, can use negated forall as a premise. The witness - // terms for the returned skolems can be obtained by - // SkolemManager::getWitnessForm. - SKOLEMIZE, - // ======== Instantiate - // Children: (P:(forall ((x1 T1) ... (xn Tn)) F)) - // Arguments: (t1 ... tn) - // ---------------------------------------- - // Conclusion: F*sigma - // sigma maps x1 ... xn to t1 ... tn. - INSTANTIATE, - - //================================================= String rules - //======================== Core solver - // ======== Concat eq - // Children: (P1:(= (str.++ t1 ... tn t) (str.++ t1 ... tn s))) - // Arguments: (b), indicating if reverse direction - // --------------------- - // Conclusion: (= t s) - // - // Notice that t or s may be empty, in which case they are implicit in the - // concatenation above. For example, if - // P1 concludes (= x (str.++ x z)), then - // (CONCAT_EQ P1 :args false) concludes (= "" z) - // - // Also note that constants are split, such that if - // P1 concludes (= (str.++ "abc" x) (str.++ "a" y)), then - // (CONCAT_EQ P1 :args false) concludes (= (str.++ "bc" x) y) - // This splitting is done only for constants such that Word::splitConstant - // returns non-null. - CONCAT_EQ, - // ======== Concat unify - // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)), - // P2:(= (str.len t1) (str.len s1))) - // Arguments: (b), indicating if reverse direction - // --------------------- - // Conclusion: (= t1 s1) - CONCAT_UNIFY, - // ======== Concat conflict - // Children: (P1:(= (str.++ c1 t) (str.++ c2 s))) - // Arguments: (b), indicating if reverse direction - // --------------------- - // Conclusion: false - // Where c1, c2 are constants such that Word::splitConstant(c1,c2,index,b) - // is null, in other words, neither is a prefix of the other. - CONCAT_CONFLICT, - // ======== Concat split - // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)), - // P2:(not (= (str.len t1) (str.len s1)))) - // Arguments: (false) - // --------------------- - // Conclusion: (or (= t1 (str.++ s1 r_t)) (= s1 (str.++ t1 r_s))) - // where - // r_t = (skolem (suf t1 (str.len s1)))), - // r_s = (skolem (suf s1 (str.len t1)))). - // - // or the reverse form of the above: - // - // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)), - // P2:(not (= (str.len t2) (str.len s2)))) - // Arguments: (true) - // --------------------- - // Conclusion: (or (= t2 (str.++ r_t s2)) (= s2 (str.++ r_s t2))) - // where - // r_t = (skolem (pre t2 (- (str.len t2) (str.len s2))))), - // r_s = (skolem (pre s2 (- (str.len s2) (str.len t2))))). - // - // Above, (suf x n) is shorthand for (str.substr x n (- (str.len x) n)) and - // (pre x n) is shorthand for (str.substr x 0 n). - CONCAT_SPLIT, - // ======== Concat constant split - // Children: (P1:(= (str.++ t1 t2) (str.++ c s2)), - // P2:(not (= (str.len t1) 0))) - // Arguments: (false) - // --------------------- - // Conclusion: (= t1 (str.++ c r)) - // where - // r = (skolem (suf t1 1)). - // - // or the reverse form of the above: - // - // Children: (P1:(= (str.++ t1 t2) (str.++ s1 c)), - // P2:(not (= (str.len t2) 0))) - // Arguments: (true) - // --------------------- - // Conclusion: (= t2 (str.++ r c)) - // where - // r = (skolem (pre t2 (- (str.len t2) 1))). - CONCAT_CSPLIT, - // ======== Concat length propagate - // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)), - // P2:(> (str.len t1) (str.len s1))) - // Arguments: (false) - // --------------------- - // Conclusion: (= t1 (str.++ s1 r_t)) - // where - // r_t = (skolem (suf t1 (str.len s1))) - // - // or the reverse form of the above: - // - // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)), - // P2:(> (str.len t2) (str.len s2))) - // Arguments: (false) - // --------------------- - // Conclusion: (= t2 (str.++ r_t s2)) - // where - // r_t = (skolem (pre t2 (- (str.len t2) (str.len s2)))). - CONCAT_LPROP, - // ======== Concat constant propagate - // Children: (P1:(= (str.++ t1 w1 t2) (str.++ w2 s)), - // P2:(not (= (str.len t1) 0))) - // Arguments: (false) - // --------------------- - // Conclusion: (= t1 (str.++ w3 r)) - // where - // w1, w2, w3, w4 are words, - // w3 is (pre w2 p), - // w4 is (suf w2 p), - // p = Word::overlap((suf w2 1), w1), - // r = (skolem (suf t1 (str.len w3))). - // In other words, w4 is the largest suffix of (suf w2 1) that can contain a - // prefix of w1; since t1 is non-empty, w3 must therefore be contained in t1. - // - // or the reverse form of the above: - // - // Children: (P1:(= (str.++ t1 w1 t2) (str.++ s w2)), - // P2:(not (= (str.len t2) 0))) - // Arguments: (true) - // --------------------- - // Conclusion: (= t2 (str.++ r w3)) - // where - // w1, w2, w3, w4 are words, - // w3 is (suf w2 (- (str.len w2) p)), - // w4 is (pre w2 (- (str.len w2) p)), - // p = Word::roverlap((pre w2 (- (str.len w2) 1)), w1), - // r = (skolem (pre t2 (- (str.len t2) (str.len w3)))). - // In other words, w4 is the largest prefix of (pre w2 (- (str.len w2) 1)) - // that can contain a suffix of w1; since t2 is non-empty, w3 must therefore - // be contained in t2. - CONCAT_CPROP, - // ======== String decompose - // Children: (P1: (>= (str.len t) n) - // Arguments: (false) - // --------------------- - // Conclusion: (and (= t (str.++ w1 w2)) (= (str.len w1) n)) - // or - // Children: (P1: (>= (str.len t) n) - // Arguments: (true) - // --------------------- - // Conclusion: (and (= t (str.++ w1 w2)) (= (str.len w2) n)) - // where - // w1 is (skolem (pre t n)) - // w2 is (skolem (suf t n)) - STRING_DECOMPOSE, - // ======== Length positive - // Children: none - // Arguments: (t) - // --------------------- - // Conclusion: (or (and (= (str.len t) 0) (= t "")) (> (str.len t) 0)) - STRING_LENGTH_POS, - // ======== Length non-empty - // Children: (P1:(not (= t ""))) - // Arguments: none - // --------------------- - // Conclusion: (not (= (str.len t) 0)) - STRING_LENGTH_NON_EMPTY, - //======================== Extended functions - // ======== Reduction - // Children: none - // Arguments: (t) - // --------------------- - // Conclusion: (and R (= t w)) - // where w = strings::StringsPreprocess::reduce(t, R, ...). - // In other words, R is the reduction predicate for extended term t, and w is - // (skolem t) - // Notice that the free variables of R are w and the free variables of t. - STRING_REDUCTION, - // ======== Eager Reduction - // Children: none - // Arguments: (t) - // --------------------- - // Conclusion: R - // where R = strings::TermRegistry::eagerReduce(t). - STRING_EAGER_REDUCTION, - //======================== Regular expressions - // ======== Regular expression intersection - // Children: (P:(str.in.re t R1), P:(str.in.re t R2)) - // Arguments: none - // --------------------- - // Conclusion: (str.in.re t (re.inter R1 R2)). - RE_INTER, - // ======== Regular expression unfold positive - // Children: (P:(str.in.re t R)) - // Arguments: none - // --------------------- - // Conclusion:(RegExpOpr::reduceRegExpPos((str.in.re t R))), - // corresponding to the one-step unfolding of the premise. - RE_UNFOLD_POS, - // ======== Regular expression unfold negative - // Children: (P:(not (str.in.re t R))) - // Arguments: none - // --------------------- - // Conclusion:(RegExpOpr::reduceRegExpNeg((not (str.in.re t R)))), - // corresponding to the one-step unfolding of the premise. - RE_UNFOLD_NEG, - // ======== Regular expression unfold negative concat fixed - // Children: (P:(not (str.in.re t R))) - // Arguments: none - // --------------------- - // Conclusion:(RegExpOpr::reduceRegExpNegConcatFixed((not (str.in.re t - // R)),L,i)) where RegExpOpr::getRegExpConcatFixed((not (str.in.re t R)), i) = - // L. corresponding to the one-step unfolding of the premise, optimized for - // fixed length of component i of the regular expression concatenation R. - RE_UNFOLD_NEG_CONCAT_FIXED, - // ======== Regular expression elimination - // Children: none - // Arguments: (F, b) - // --------------------- - // Conclusion: (= F strings::RegExpElimination::eliminate(F, b)) - // where b is a Boolean indicating whether we are using aggressive - // eliminations. Notice this rule concludes (= F F) if no eliminations - // are performed for F. - RE_ELIM, - //======================== Code points - // Children: none - // Arguments: (t, s) - // --------------------- - // Conclusion:(or (= (str.code t) (- 1)) - // (not (= (str.code t) (str.code s))) - // (not (= t s))) - STRING_CODE_INJ, - //======================== Sequence unit - // Children: (P:(= (seq.unit x) (seq.unit y))) - // Arguments: none - // --------------------- - // Conclusion:(= x y) - // Also applies to the case where (seq.unit y) is a constant sequence - // of length one. - STRING_SEQ_UNIT_INJ, - // ======== String Trust - // Children: none - // Arguments: (Q) - // --------------------- - // Conclusion: (Q) - STRING_TRUST, - - //================================================= Arithmetic rules - // ======== Adding Inequalities - // Note: an ArithLiteral is a term of the form (>< poly const) - // where - // >< is >=, >, ==, <, <=, or not(== ...). - // poly is a polynomial - // const is a rational constant - - // Children: (P1:l1, ..., Pn:ln) - // where each li is an ArithLiteral - // not(= ...) is dis-allowed! - // - // Arguments: (k1, ..., kn), non-zero reals - // --------------------- - // Conclusion: (>< t1 t2) - // where >< is the fusion of the combination of the ><i, (flipping each it - // its ki is negative). >< is always one of <, <= - // NB: this implies that lower bounds must have negative ki, - // and upper bounds must have positive ki. - // t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n * - // poly_n) t2 is the sum of the scaled constants (k_1 * const_1 + ... + k_n - // * const_n) - MACRO_ARITH_SCALE_SUM_UB, - // ======== Sum Upper Bounds - // Children: (P1, ... , Pn) - // where each Pi has form (><i, Li, Ri) - // for ><i in {<, <=, ==} - // Conclusion: (>< L R) - // where >< is < if any ><i is <, and <= otherwise. - // L is (+ L1 ... Ln) - // R is (+ R1 ... Rn) - ARITH_SUM_UB, - // ======== Tightening Strict Integer Upper Bounds - // Children: (P:(< i c)) - // where i has integer type. - // Arguments: none - // --------------------- - // Conclusion: (<= i greatestIntLessThan(c)}) - INT_TIGHT_UB, - // ======== Tightening Strict Integer Lower Bounds - // Children: (P:(> i c)) - // where i has integer type. - // Arguments: none - // --------------------- - // Conclusion: (>= i leastIntGreaterThan(c)}) - INT_TIGHT_LB, - // ======== Trichotomy of the reals - // Children: (A B) - // Arguments: (C) - // --------------------- - // Conclusion: (C), - // where (not A) (not B) and C - // are (> x c) (< x c) and (= x c) - // in some order - // note that "not" here denotes arithmetic negation, flipping - // >= to <, etc. - ARITH_TRICHOTOMY, - // ======== Arithmetic operator elimination - // Children: none - // Arguments: (t) - // --------------------- - // Conclusion: arith::OperatorElim::getAxiomFor(t) - ARITH_OP_ELIM_AXIOM, - // ======== Int Trust - // Children: (P1 ... Pn) - // Arguments: (Q) - // --------------------- - // Conclusion: (Q) - INT_TRUST, - - //======== Multiplication sign inference - // Children: none - // Arguments: (f1, ..., fk, m) - // --------------------- - // Conclusion: (=> (and f1 ... fk) (~ m 0)) - // Where f1, ..., fk are variables compared to zero (less, greater or not - // equal), m is a monomial from these variables, and ~ is the comparison (less - // or greater) that results from the signs of the variables. All variables - // with even exponent in m should be given as not equal to zero while all - // variables with odd exponent in m should be given as less or greater than - // zero. - ARITH_MULT_SIGN, - //======== Multiplication with positive factor - // Children: none - // Arguments: (m, (rel lhs rhs)) - // --------------------- - // Conclusion: (=> (and (> m 0) (rel lhs rhs)) (rel (* m lhs) (* m rhs))) - // Where rel is a relation symbol. - ARITH_MULT_POS, - //======== Multiplication with negative factor - // Children: none - // Arguments: (m, (rel lhs rhs)) - // --------------------- - // Conclusion: (=> (and (< m 0) (rel lhs rhs)) (rel_inv (* m lhs) (* m rhs))) - // Where rel is a relation symbol and rel_inv the inverted relation symbol. - ARITH_MULT_NEG, - //======== Multiplication tangent plane - // Children: none - // Arguments: (t, x, y, a, b, sgn) - // --------------------- - // Conclusion: - // sgn=-1: (= (<= t tplane) (or (and (<= x a) (>= y b)) (and (>= x a) (<= y - // b))) sgn= 1: (= (>= t tplane) (or (and (<= x a) (<= y b)) (and (>= x a) - // (>= y b))) - // Where x,y are real terms (variables or extended terms), t = (* x y) - // (possibly under rewriting), a,b are real constants, and sgn is either -1 - // or 1. tplane is the tangent plane of x*y at (a,b): b*x + a*y - a*b - ARITH_MULT_TANGENT, - - // ================ Lemmas for transcendentals - //======== Assert bounds on PI - // Children: none - // Arguments: (l, u) - // --------------------- - // Conclusion: (and (>= real.pi l) (<= real.pi u)) - // Where l (u) is a valid lower (upper) bound on pi. - ARITH_TRANS_PI, - //======== Exp at negative values - // Children: none - // Arguments: (t) - // --------------------- - // Conclusion: (= (< t 0) (< (exp t) 1)) - ARITH_TRANS_EXP_NEG, - //======== Exp is always positive - // Children: none - // Arguments: (t) - // --------------------- - // Conclusion: (> (exp t) 0) - ARITH_TRANS_EXP_POSITIVITY, - //======== Exp grows super-linearly for positive values - // Children: none - // Arguments: (t) - // --------------------- - // Conclusion: (or (<= t 0) (> exp(t) (+ t 1))) - ARITH_TRANS_EXP_SUPER_LIN, - //======== Exp at zero - // Children: none - // Arguments: (t) - // --------------------- - // Conclusion: (= (= t 0) (= (exp t) 1)) - ARITH_TRANS_EXP_ZERO, - //======== Exp is approximated from above for negative values - // Children: none - // Arguments: (d, t, l, u) - // --------------------- - // Conclusion: (=> (and (>= t l) (<= t u)) (<= (exp t) (secant exp l u t)) - // Where d is an even positive number, t an arithmetic term and l (u) a lower - // (upper) bound on t. Let p be the d'th taylor polynomial at zero (also - // called the Maclaurin series) of the exponential function. (secant exp l u - // t) denotes the secant of p from (l, exp(l)) to (u, exp(u)) evaluated at t, - // calculated as follows: - // (p(l) - p(u)) / (l - u) * (t - l) + p(l) - // The lemma states that if t is between l and u, then (exp t) is below the - // secant of p from l to u. - ARITH_TRANS_EXP_APPROX_ABOVE_NEG, - //======== Exp is approximated from above for positive values - // Children: none - // Arguments: (d, t, l, u) - // --------------------- - // Conclusion: (=> (and (>= t l) (<= t u)) (<= (exp t) (secant-pos exp l u t)) - // Where d is an even positive number, t an arithmetic term and l (u) a lower - // (upper) bound on t. Let p* be a modification of the d'th taylor polynomial - // at zero (also called the Maclaurin series) of the exponential function as - // follows where p(d-1) is the regular Maclaurin series of degree d-1: - // p* = p(d-1) * (1 + t^n / n!) - // (secant-pos exp l u t) denotes the secant of p from (l, exp(l)) to (u, - // exp(u)) evaluated at t, calculated as follows: - // (p(l) - p(u)) / (l - u) * (t - l) + p(l) - // The lemma states that if t is between l and u, then (exp t) is below the - // secant of p from l to u. - ARITH_TRANS_EXP_APPROX_ABOVE_POS, - //======== Exp is approximated from below - // Children: none - // Arguments: (d, t) - // --------------------- - // Conclusion: (>= (exp t) (maclaurin exp d t)) - // Where d is an odd positive number and (maclaurin exp d t) is the d'th - // taylor polynomial at zero (also called the Maclaurin series) of the - // exponential function evaluated at t. The Maclaurin series for the - // exponential function is the following: - // e^x = \sum_{n=0}^{\infty} x^n / n! - ARITH_TRANS_EXP_APPROX_BELOW, - //======== Sine is always between -1 and 1 - // Children: none - // Arguments: (t) - // --------------------- - // Conclusion: (and (<= (sin t) 1) (>= (sin t) (- 1))) - ARITH_TRANS_SINE_BOUNDS, - //======== Sine arg shifted to -pi..pi - // Children: none - // Arguments: (x, y, s) - // --------------------- - // Conclusion: (and - // (<= -pi y pi) - // (= (sin y) (sin x)) - // (ite (<= -pi x pi) (= x y) (= x (+ y (* 2 pi s)))) - // ) - // Where x is the argument to sine, y is a new real skolem that is x shifted - // into -pi..pi and s is a new integer skolem that is the number of phases y - // is shifted. - ARITH_TRANS_SINE_SHIFT, - //======== Sine is symmetric with respect to negation of the argument - // Children: none - // Arguments: (t) - // --------------------- - // Conclusion: (= (- (sin t) (sin (- t))) 0) - ARITH_TRANS_SINE_SYMMETRY, - //======== Sine is bounded by the tangent at zero - // Children: none - // Arguments: (t) - // --------------------- - // Conclusion: (and - // (=> (> t 0) (< (sin t) t)) - // (=> (< t 0) (> (sin t) t)) - // ) - ARITH_TRANS_SINE_TANGENT_ZERO, - //======== Sine is bounded by the tangents at -pi and pi - // Children: none - // Arguments: (t) - // --------------------- - // Conclusion: (and - // (=> (> t -pi) (> (sin t) (- -pi t))) - // (=> (< t pi) (< (sin t) (- pi t))) - // ) - ARITH_TRANS_SINE_TANGENT_PI, - //======== Sine is approximated from above for negative values - // Children: none - // Arguments: (d, t, lb, ub, l, u) - // --------------------- - // Conclusion: (=> (and (>= t lb) (<= t ub)) (<= (sin t) (secant sin l u t)) - // Where d is an even positive number, t an arithmetic term, lb (ub) a - // symbolic lower (upper) bound on t (possibly containing pi) and l (u) the - // evaluated lower (upper) bound on t. Let p be the d'th taylor polynomial at - // zero (also called the Maclaurin series) of the sine function. (secant sin l - // u t) denotes the secant of p from (l, sin(l)) to (u, sin(u)) evaluated at - // t, calculated as follows: - // (p(l) - p(u)) / (l - u) * (t - l) + p(l) - // The lemma states that if t is between l and u, then (sin t) is below the - // secant of p from l to u. - ARITH_TRANS_SINE_APPROX_ABOVE_NEG, - //======== Sine is approximated from above for positive values - // Children: none - // Arguments: (d, t, c, lb, ub) - // --------------------- - // Conclusion: (=> (and (>= t lb) (<= t ub)) (<= (sin t) (upper sin c)) - // Where d is an even positive number, t an arithmetic term, c an arithmetic - // constant, and lb (ub) a symbolic lower (upper) bound on t (possibly - // containing pi). Let p be the d'th taylor polynomial at zero (also called - // the Maclaurin series) of the sine function. (upper sin c) denotes the upper - // bound on sin(c) given by p and lb,ub are such that sin(t) is the maximum of - // the sine function on (lb,ub). - ARITH_TRANS_SINE_APPROX_ABOVE_POS, - //======== Sine is approximated from below for negative values - // Children: none - // Arguments: (d, t, c, lb, ub) - // --------------------- - // Conclusion: (=> (and (>= t lb) (<= t ub)) (>= (sin t) (lower sin c)) - // Where d is an even positive number, t an arithmetic term, c an arithmetic - // constant, and lb (ub) a symbolic lower (upper) bound on t (possibly - // containing pi). Let p be the d'th taylor polynomial at zero (also called - // the Maclaurin series) of the sine function. (lower sin c) denotes the lower - // bound on sin(c) given by p and lb,ub are such that sin(t) is the minimum of - // the sine function on (lb,ub). - ARITH_TRANS_SINE_APPROX_BELOW_NEG, - //======== Sine is approximated from below for positive values - // Children: none - // Arguments: (d, t, lb, ub, l, u) - // --------------------- - // Conclusion: (=> (and (>= t lb) (<= t ub)) (>= (sin t) (secant sin l u t)) - // Where d is an even positive number, t an arithmetic term, lb (ub) a - // symbolic lower (upper) bound on t (possibly containing pi) and l (u) the - // evaluated lower (upper) bound on t. Let p be the d'th taylor polynomial at - // zero (also called the Maclaurin series) of the sine function. (secant sin l - // u t) denotes the secant of p from (l, sin(l)) to (u, sin(u)) evaluated at - // t, calculated as follows: - // (p(l) - p(u)) / (l - u) * (t - l) + p(l) - // The lemma states that if t is between l and u, then (sin t) is above the - // secant of p from l to u. - ARITH_TRANS_SINE_APPROX_BELOW_POS, - - // ================ CAD Lemmas - // We use IRP for IndexedRootPredicate. - // - // A formula "Interval" describes that a variable (xn is none is given) is - // within a particular interval whose bounds are given as IRPs. It is either - // an open interval or a point interval: - // (IRP k poly) < xn < (IRP k poly) - // xn == (IRP k poly) - // - // A formula "Cell" describes a portion - // of the real space in the following form: - // Interval(x1) and Interval(x2) and ... - // We implicitly assume a Cell to go up to n-1 (and can be empty). - // - // A formula "Covering" is a set of Intervals, implying that xn can be in - // neither of these intervals. To be a covering (of the real line), the union - // of these intervals should be the real numbers. - // ======== CAD direct conflict - // Children (Cell, A) - // --------------------- - // Conclusion: (false) - // A direct interval is generated from an assumption A (in variables x1...xn) - // over a Cell (in variables x1...xn). It derives that A evaluates to false - // over the Cell. In the actual algorithm, it means that xn can not be in the - // topmost interval of the Cell. - ARITH_NL_CAD_DIRECT, - // ======== CAD recursive interval - // Children (Cell, Covering) - // --------------------- - // Conclusion: (false) - // A recursive interval is generated from a Covering (for xn) over a Cell - // (in variables x1...xn-1). It generates the conclusion that no xn exists - // that extends the Cell and satisfies all assumptions. - ARITH_NL_CAD_RECURSIVE, - - //================================================= Unknown rule - UNKNOWN, -}; - -/** - * Converts a proof rule to a string. Note: This function is also used in - * `safe_print()`. Changing this function name or signature will result in - * `safe_print()` printing "<unsupported>" instead of the proper strings for - * the enum values. - * - * @param id The proof rule - * @return The name of the proof rule - */ -const char* toString(PfRule id); - -/** - * Writes a proof rule name to a stream. - * - * @param out The stream to write to - * @param id The proof rule to write to the stream - * @return The stream - */ -std::ostream& operator<<(std::ostream& out, PfRule id); - -/** Hash function for proof rules */ -struct PfRuleHashFunction -{ - size_t operator()(PfRule id) const; -}; /* struct PfRuleHashFunction */ - -} // namespace cvc5 - -#endif /* CVC5__EXPR__PROOF_RULE_H */ diff --git a/src/expr/proof_set.h b/src/expr/proof_set.h deleted file mode 100644 index 5ea9c1021..000000000 --- a/src/expr/proof_set.h +++ /dev/null @@ -1,76 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Gereon Kremer, Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Proof set utility. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__EXPR__PROOF_SET_H -#define CVC5__EXPR__PROOF_SET_H - -#include <memory> - -#include "context/cdlist.h" -#include "context/context.h" -#include "expr/proof_node_manager.h" - -namespace cvc5 { - -/** - * A (context-dependent) set of proofs, which is used for memory - * management purposes. - */ -template <typename T> -class CDProofSet -{ - public: - CDProofSet(ProofNodeManager* pnm, - context::Context* c, - std::string namePrefix = "Proof") - : d_pnm(pnm), d_proofs(c), d_namePrefix(namePrefix) - { - } - /** - * Allocate a new proof. - * - * This returns a fresh proof object that remains alive in the context given - * to this class. Internally, this adds a new proof of type T to a - * context-dependent list of proofs and passes the following arguments to the - * T constructor: - * pnm, args..., name - * where pnm is the proof node manager - * provided to this proof set upon construction, args... are the arguments to - * allocateProof() and name is the namePrefix with an appended index. - */ - template <typename... Args> - T* allocateProof(Args&&... args) - { - d_proofs.push_back(std::make_shared<T>( - d_pnm, - std::forward<Args>(args)..., - d_namePrefix + "_" + std::to_string(d_proofs.size()))); - return d_proofs.back().get(); - } - - protected: - /** The proof node manager */ - ProofNodeManager* d_pnm; - /** A context-dependent list of lazy proofs. */ - context::CDList<std::shared_ptr<T>> d_proofs; - /** The name prefix of the lazy proofs */ - std::string d_namePrefix; -}; - -} // namespace cvc5 - -#endif /* CVC5__EXPR__LAZY_PROOF_SET_H */ diff --git a/src/expr/proof_step_buffer.cpp b/src/expr/proof_step_buffer.cpp deleted file mode 100644 index 84cfc040c..000000000 --- a/src/expr/proof_step_buffer.cpp +++ /dev/null @@ -1,112 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Aina Niemetz - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of proof step and proof step buffer utilities. - */ - -#include "expr/proof_step_buffer.h" - -#include "expr/proof_checker.h" - -using namespace cvc5::kind; - -namespace cvc5 { - -ProofStep::ProofStep() : d_rule(PfRule::UNKNOWN) {} -ProofStep::ProofStep(PfRule r, - const std::vector<Node>& children, - const std::vector<Node>& args) - : d_rule(r), d_children(children), d_args(args) -{ -} -std::ostream& operator<<(std::ostream& out, ProofStep step) -{ - out << "(step " << step.d_rule; - for (const Node& c : step.d_children) - { - out << " " << c; - } - if (!step.d_args.empty()) - { - out << " :args"; - for (const Node& a : step.d_args) - { - out << " " << a; - } - } - out << ")"; - return out; -} - -ProofStepBuffer::ProofStepBuffer(ProofChecker* pc) : d_checker(pc) {} - -Node ProofStepBuffer::tryStep(PfRule id, - const std::vector<Node>& children, - const std::vector<Node>& args, - Node expected) -{ - if (d_checker == nullptr) - { - Assert(false) << "ProofStepBuffer::ProofStepBuffer: no proof checker."; - return Node::null(); - } - Node res = - d_checker->checkDebug(id, children, args, expected, "pf-step-buffer"); - if (!res.isNull()) - { - // add proof step - d_steps.push_back( - std::pair<Node, ProofStep>(res, ProofStep(id, children, args))); - } - return res; -} - -void ProofStepBuffer::addStep(PfRule id, - const std::vector<Node>& children, - const std::vector<Node>& args, - Node expected) -{ - d_steps.push_back( - std::pair<Node, ProofStep>(expected, ProofStep(id, children, args))); -} - -void ProofStepBuffer::addSteps(ProofStepBuffer& psb) -{ - const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps(); - for (const std::pair<Node, ProofStep>& step : steps) - { - addStep(step.second.d_rule, - step.second.d_children, - step.second.d_args, - step.first); - } -} - -void ProofStepBuffer::popStep() -{ - Assert(!d_steps.empty()); - if (!d_steps.empty()) - { - d_steps.pop_back(); - } -} - -size_t ProofStepBuffer::getNumSteps() const { return d_steps.size(); } - -const std::vector<std::pair<Node, ProofStep>>& ProofStepBuffer::getSteps() const -{ - return d_steps; -} - -void ProofStepBuffer::clear() { d_steps.clear(); } - -} // namespace cvc5 diff --git a/src/expr/proof_step_buffer.h b/src/expr/proof_step_buffer.h deleted file mode 100644 index b9350cf45..000000000 --- a/src/expr/proof_step_buffer.h +++ /dev/null @@ -1,98 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Proof step and proof step buffer utilities. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__EXPR__PROOF_STEP_BUFFER_H -#define CVC5__EXPR__PROOF_STEP_BUFFER_H - -#include <vector> - -#include "expr/node.h" -#include "expr/proof_rule.h" - -namespace cvc5 { - -class ProofChecker; - -/** - * Information for constructing a step in a CDProof. Notice that the conclusion - * of the proof step is intentionally not included in this data structure. - * Instead, it is intended that conclusions may be associated with proof steps - * based on e.g. the result of proof checking. - */ -class ProofStep -{ - public: - ProofStep(); - ProofStep(PfRule r, - const std::vector<Node>& children, - const std::vector<Node>& args); - /** The proof rule */ - PfRule d_rule; - /** The proof children */ - std::vector<Node> d_children; - /** The proof arguments */ - std::vector<Node> d_args; -}; -std::ostream& operator<<(std::ostream& out, ProofStep step); - -/** - * Class used to speculatively try and buffer a set of proof steps before - * sending them to a proof object. - */ -class ProofStepBuffer -{ - public: - ProofStepBuffer(ProofChecker* pc = nullptr); - ~ProofStepBuffer() {} - /** - * Returns the conclusion of the proof step, as determined by the proof - * checker of the given proof. If this is non-null, then the given step - * is added to the buffer maintained by this class. - * - * If expected is non-null, then this method returns null if the result of - * checking is not equal to expected. - */ - Node tryStep(PfRule id, - const std::vector<Node>& children, - const std::vector<Node>& args, - Node expected = Node::null()); - /** Same as above, without checking */ - void addStep(PfRule id, - const std::vector<Node>& children, - const std::vector<Node>& args, - Node expected); - /** Multi-step version */ - void addSteps(ProofStepBuffer& psb); - /** pop step */ - void popStep(); - /** Get num steps */ - size_t getNumSteps() const; - /** Get steps */ - const std::vector<std::pair<Node, ProofStep>>& getSteps() const; - /** Clear */ - void clear(); - - private: - /** The proof checker*/ - ProofChecker* d_checker; - /** the queued proof steps */ - std::vector<std::pair<Node, ProofStep>> d_steps; -}; - -} // namespace cvc5 - -#endif /* CVC5__EXPR__PROOF_STEP_BUFFER_H */ diff --git a/src/expr/tconv_seq_proof_generator.cpp b/src/expr/tconv_seq_proof_generator.cpp deleted file mode 100644 index 00e961628..000000000 --- a/src/expr/tconv_seq_proof_generator.cpp +++ /dev/null @@ -1,172 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Term conversion sequence proof generator utility. - */ - -#include "expr/tconv_seq_proof_generator.h" - -#include <sstream> - -#include "expr/proof_node_manager.h" - -namespace cvc5 { - -TConvSeqProofGenerator::TConvSeqProofGenerator( - ProofNodeManager* pnm, - const std::vector<ProofGenerator*>& ts, - context::Context* c, - std::string name) - : d_pnm(pnm), d_converted(c), d_name(name) -{ - d_tconvs.insert(d_tconvs.end(), ts.begin(), ts.end()); - AlwaysAssert(!d_tconvs.empty()) - << "TConvSeqProofGenerator::TConvSeqProofGenerator: expecting non-empty " - "sequence"; -} - -TConvSeqProofGenerator::~TConvSeqProofGenerator() {} - -void TConvSeqProofGenerator::registerConvertedTerm(Node t, Node s, size_t index) -{ - if (t == s) - { - // no need - return; - } - std::pair<Node, size_t> key = std::pair<Node, size_t>(t, index); - d_converted[key] = s; -} - -std::shared_ptr<ProofNode> TConvSeqProofGenerator::getProofFor(Node f) -{ - Trace("tconv-seq-pf-gen") - << "TConvSeqProofGenerator::getProofFor: " << identify() << ": " << f - << std::endl; - return getSubsequenceProofFor(f, 0, d_tconvs.size() - 1); -} - -std::shared_ptr<ProofNode> TConvSeqProofGenerator::getSubsequenceProofFor( - Node f, size_t start, size_t end) -{ - Assert(end < d_tconvs.size()); - if (f.getKind() != kind::EQUAL) - { - std::stringstream serr; - serr << "TConvSeqProofGenerator::getProofFor: " << identify() - << ": fail, non-equality " << f; - Unhandled() << serr.str(); - Trace("tconv-seq-pf-gen") << serr.str() << std::endl; - return nullptr; - } - // start with the left hand side of the equality - Node curr = f[0]; - // proofs forming transitivity chain - std::vector<std::shared_ptr<ProofNode>> transChildren; - std::pair<Node, size_t> currKey; - NodeIndexNodeMap::iterator itc; - // convert the term in sequence - for (size_t i = start; i <= end; i++) - { - currKey = std::pair<Node, size_t>(curr, i); - itc = d_converted.find(currKey); - // if we provided a conversion at this index via registerConvertedTerm - if (itc != d_converted.end()) - { - Node next = (*itc).second; - Trace("tconv-seq-pf-gen") << "...convert to " << next << std::endl; - Node eq = curr.eqNode(next); - std::shared_ptr<ProofNode> pf = d_tconvs[i]->getProofFor(eq); - transChildren.push_back(pf); - curr = next; - } - } - // should end up with the right hand side of the equality - if (curr != f[1]) - { - // unexpected - std::stringstream serr; - serr << "TConvSeqProofGenerator::getProofFor: " << identify() - << ": failed, mismatch (see -t tconv-seq-pf-gen-debug for details)" - << std::endl; - serr << " source: " << f[0] << std::endl; - serr << "expected after conversions: " << f[1] << std::endl; - serr << " actual after conversions: " << curr << std::endl; - - if (Trace.isOn("tconv-seq-pf-gen-debug")) - { - Trace("tconv-pf-gen-debug") - << "Printing conversion steps..." << std::endl; - serr << "Conversions: " << std::endl; - for (NodeIndexNodeMap::const_iterator it = d_converted.begin(); - it != d_converted.end(); - ++it) - { - serr << "(" << (*it).first.first << ", " << (*it).first.second - << ") -> " << (*it).second << std::endl; - } - } - Unhandled() << serr.str(); - return nullptr; - } - // otherwise, make transitivity - return d_pnm->mkTrans(transChildren, f); -} - -theory::TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence( - const std::vector<Node>& cterms) -{ - Assert(cterms.size() == d_tconvs.size() + 1); - if (cterms[0] == cterms[cterms.size() - 1]) - { - return theory::TrustNode::null(); - } - bool useThis = false; - ProofGenerator* pg = nullptr; - for (size_t i = 0, nconvs = d_tconvs.size(); i < nconvs; i++) - { - if (cterms[i] == cterms[i + 1]) - { - continue; - } - else if (pg == nullptr) - { - // Maybe the i^th generator can explain it alone, which must be the case - // if there is only one position in the sequence where the term changes. - // We may overwrite pg with this class if another step is encountered in - // this loop. - pg = d_tconvs[i]; - } - else - { - // need more than a single generator, use this class - useThis = true; - break; - } - } - if (useThis) - { - pg = this; - // if more than two steps, we must register each conversion step - for (size_t i = 0, nconvs = d_tconvs.size(); i < nconvs; i++) - { - registerConvertedTerm(cterms[i], cterms[i + 1], i); - } - } - Assert(pg != nullptr); - return theory::TrustNode::mkTrustRewrite( - cterms[0], cterms[cterms.size() - 1], pg); -} - -std::string TConvSeqProofGenerator::identify() const { return d_name; } - -} // namespace cvc5 diff --git a/src/expr/tconv_seq_proof_generator.h b/src/expr/tconv_seq_proof_generator.h deleted file mode 100644 index bc067f60a..000000000 --- a/src/expr/tconv_seq_proof_generator.h +++ /dev/null @@ -1,121 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Term conversion sequence proof generator utility. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H -#define CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H - -#include "context/cdhashmap.h" -#include "expr/node.h" -#include "expr/proof_generator.h" -#include "theory/trust_node.h" - -namespace cvc5 { - -class ProofNodeManager; - -/** - * The term conversion sequence proof generator. This is used for maintaining - * a fixed sequence of proof generators that provide proofs for rewrites - * (equalities). We call these the "component generators" of this sequence, - * which are typically TConvProofGenerator. - */ -class TConvSeqProofGenerator : public ProofGenerator -{ - public: - /** - * @param pnm The proof node manager for constructing ProofNode objects. - * @param ts The list of component term conversion generators that are - * applied in sequence - * @param c The context that this class depends on. If none is provided, - * this class is context-independent. - * @param name The name of this generator (for debugging). - */ - TConvSeqProofGenerator(ProofNodeManager* pnm, - const std::vector<ProofGenerator*>& ts, - context::Context* c = nullptr, - std::string name = "TConvSeqProofGenerator"); - ~TConvSeqProofGenerator(); - /** - * Indicate that the index^th proof generator converts term t to s. This - * should be called for a unique s for each (t, index). It must be the - * case that d_tconv[index] can provide a proof for t = s in the remainder - * of the context maintained by this class. - */ - void registerConvertedTerm(Node t, Node s, size_t index); - /** - * Get the proof for formula f. It should be the case that f is of the form - * t_0 = t_n, where it must be the case that t_n is obtained by the following: - * For each i=0, ... n, let t_{i+1} be the term such that - * registerConvertedTerm(t_i, t_{i+1}, i) - * was called. Otherwise t_{i+1} = t_i. - * In other words, t_n is obtained by converting t_0, in order, based on the - * calls to registerConvertedTerm. - * - * @param f The equality fact to get the proof for. - * @return The proof for f. - */ - std::shared_ptr<ProofNode> getProofFor(Node f) override; - /** - * Get subsequence proof for f, with given start and end steps (inclusive). - */ - std::shared_ptr<ProofNode> getSubsequenceProofFor(Node f, - size_t start, - size_t end); - /** Identify this generator (for debugging, etc..) */ - std::string identify() const override; - - /** - * Make trust node from a sequence of converted terms. The number of - * terms in cterms should be 1 + the number of component proof generators - * maintained by this class. This selects a proof generator that is capable - * of proving cterms[0] = cterms[cterms.size()-1], which is either this - * generator, or one of the component proof generators, if only one step - * rewrote. In the former case, all steps are registered to this class. - * Using a component generator is an optimization that saves having to - * save the conversion steps or use this class. For example, if we have 2 - * term conversion components, and call this method on: - * { a, b, c } - * then this method calls: - * registerConvertedTerm( a, b, 0 ) - * registerConvertedTerm( b, c, 1 ) - * and returns a trust node proving (= a c) with this class as the proof - * generator. On the other hand, if we call this method on: - * { d, d, e } - * then we return a trust node proving (= d e) with the 2nd component proof - * generator, as it alone is capable of proving this equality. - */ - theory::TrustNode mkTrustRewriteSequence(const std::vector<Node>& cterms); - - protected: - using NodeIndexPairHashFunction = - PairHashFunction<Node, size_t, std::hash<Node>>; - typedef context:: - CDHashMap<std::pair<Node, size_t>, Node, NodeIndexPairHashFunction> - NodeIndexNodeMap; - /** The proof node manager */ - ProofNodeManager* d_pnm; - /** The term conversion generators */ - std::vector<ProofGenerator*> d_tconvs; - /** the set of converted terms */ - NodeIndexNodeMap d_converted; - /** Name identifier */ - std::string d_name; -}; - -} // namespace cvc5 - -#endif /* CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H */ diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp deleted file mode 100644 index 0e0ed3165..000000000 --- a/src/expr/term_conversion_proof_generator.cpp +++ /dev/null @@ -1,624 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Aina Niemetz - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of term conversion proof generator utility. - */ - -#include "expr/term_conversion_proof_generator.h" - -#include <sstream> - -#include "expr/proof_checker.h" -#include "expr/proof_node.h" -#include "expr/proof_node_algorithm.h" -#include "expr/term_context.h" -#include "expr/term_context_stack.h" - -using namespace cvc5::kind; - -namespace cvc5 { - -std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol) -{ - switch (tcpol) - { - case TConvPolicy::FIXPOINT: out << "FIXPOINT"; break; - case TConvPolicy::ONCE: out << "ONCE"; break; - default: out << "TConvPolicy:unknown"; break; - } - return out; -} - -std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol) -{ - switch (tcpol) - { - case TConvCachePolicy::STATIC: out << "STATIC"; break; - case TConvCachePolicy::DYNAMIC: out << "DYNAMIC"; break; - case TConvCachePolicy::NEVER: out << "NEVER"; break; - default: out << "TConvCachePolicy:unknown"; break; - } - return out; -} - -TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm, - context::Context* c, - TConvPolicy pol, - TConvCachePolicy cpol, - std::string name, - TermContext* tccb, - bool rewriteOps) - : d_proof(pnm, nullptr, c, name + "::LazyCDProof"), - d_preRewriteMap(c ? c : &d_context), - d_postRewriteMap(c ? c : &d_context), - d_policy(pol), - d_cpolicy(cpol), - d_name(name), - d_tcontext(tccb), - d_rewriteOps(rewriteOps) -{ -} - -TConvProofGenerator::~TConvProofGenerator() {} - -void TConvProofGenerator::addRewriteStep(Node t, - Node s, - ProofGenerator* pg, - bool isPre, - PfRule trustId, - bool isClosed, - uint32_t tctx) -{ - Node eq = registerRewriteStep(t, s, tctx, isPre); - if (!eq.isNull()) - { - d_proof.addLazyStep(eq, pg, trustId, isClosed); - } -} - -void TConvProofGenerator::addRewriteStep( - Node t, Node s, ProofStep ps, bool isPre, uint32_t tctx) -{ - Node eq = registerRewriteStep(t, s, tctx, isPre); - if (!eq.isNull()) - { - d_proof.addStep(eq, ps); - } -} - -void TConvProofGenerator::addRewriteStep(Node t, - Node s, - PfRule id, - const std::vector<Node>& children, - const std::vector<Node>& args, - bool isPre, - uint32_t tctx) -{ - Node eq = registerRewriteStep(t, s, tctx, isPre); - if (!eq.isNull()) - { - d_proof.addStep(eq, id, children, args); - } -} - -bool TConvProofGenerator::hasRewriteStep(Node t, - uint32_t tctx, - bool isPre) const -{ - return !getRewriteStep(t, tctx, isPre).isNull(); -} - -Node TConvProofGenerator::getRewriteStep(Node t, - uint32_t tctx, - bool isPre) const -{ - Node thash = t; - if (d_tcontext != nullptr) - { - thash = TCtxNode::computeNodeHash(t, tctx); - } - return getRewriteStepInternal(thash, isPre); -} - -Node TConvProofGenerator::registerRewriteStep(Node t, - Node s, - uint32_t tctx, - bool isPre) -{ - Assert(!t.isNull()); - Assert(!s.isNull()); - - if (t == s) - { - return Node::null(); - } - Node thash = t; - if (d_tcontext != nullptr) - { - thash = TCtxNode::computeNodeHash(t, tctx); - } - else - { - // don't use term context ids if not using term context - Assert(tctx == 0); - } - // should not rewrite term to two different things - if (!getRewriteStepInternal(thash, isPre).isNull()) - { - Assert(getRewriteStepInternal(thash, isPre) == s) - << identify() << " rewriting " << t << " to both " << s << " and " - << getRewriteStepInternal(thash, isPre); - return Node::null(); - } - NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap; - rm[thash] = s; - if (d_cpolicy == TConvCachePolicy::DYNAMIC) - { - // clear the cache - d_cache.clear(); - } - return t.eqNode(s); -} - -std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f) -{ - Trace("tconv-pf-gen") << "TConvProofGenerator::getProofFor: " << identify() - << ": " << f << std::endl; - if (f.getKind() != EQUAL) - { - std::stringstream serr; - serr << "TConvProofGenerator::getProofFor: " << identify() - << ": fail, non-equality " << f; - Unhandled() << serr.str(); - Trace("tconv-pf-gen") << serr.str() << std::endl; - return nullptr; - } - // we use the existing proofs - LazyCDProof lpf( - d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProof"); - if (f[0] == f[1]) - { - // assertion failure in debug - Assert(false) << "TConvProofGenerator::getProofFor: " << identify() - << ": don't ask for trivial proofs"; - lpf.addStep(f, PfRule::REFL, {}, {f[0]}); - } - else - { - Node conc = getProofForRewriting(f[0], lpf, d_tcontext); - if (conc != f) - { - bool debugTraceEnabled = Trace.isOn("tconv-pf-gen-debug"); - Assert(conc.getKind() == EQUAL && conc[0] == f[0]); - std::stringstream serr; - serr << "TConvProofGenerator::getProofFor: " << toStringDebug() - << ": failed, mismatch"; - if (!debugTraceEnabled) - { - serr << " (see -t tconv-pf-gen-debug for details)"; - } - serr << std::endl; - serr << " source: " << f[0] << std::endl; - serr << " requested conclusion: " << f[1] << std::endl; - serr << "conclusion from generator: " << conc[1] << std::endl; - - if (debugTraceEnabled) - { - Trace("tconv-pf-gen-debug") << "Printing rewrite steps..." << std::endl; - for (size_t r = 0; r < 2; r++) - { - const NodeNodeMap& rm = r == 0 ? d_preRewriteMap : d_postRewriteMap; - serr << "Rewrite steps (" << (r == 0 ? "pre" : "post") - << "):" << std::endl; - for (NodeNodeMap::const_iterator it = rm.begin(); it != rm.end(); - ++it) - { - serr << (*it).first << " -> " << (*it).second << std::endl; - } - } - } - Unhandled() << serr.str(); - return nullptr; - } - } - std::shared_ptr<ProofNode> pfn = lpf.getProofFor(f); - Trace("tconv-pf-gen") << "... success" << std::endl; - Assert (pfn!=nullptr); - Trace("tconv-pf-gen-debug") << "... proof is " << *pfn << std::endl; - return pfn; -} - -std::shared_ptr<ProofNode> TConvProofGenerator::getProofForRewriting(Node n) -{ - LazyCDProof lpf( - d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProofRew"); - Node conc = getProofForRewriting(n, lpf, d_tcontext); - if (conc[1] == n) - { - // assertion failure in debug - Assert(false) << "TConvProofGenerator::getProofForRewriting: " << identify() - << ": don't ask for trivial proofs"; - lpf.addStep(conc, PfRule::REFL, {}, {n}); - } - std::shared_ptr<ProofNode> pfn = lpf.getProofFor(conc); - Assert(pfn != nullptr); - Trace("tconv-pf-gen-debug") << "... proof is " << *pfn << std::endl; - return pfn; -} - -Node TConvProofGenerator::getProofForRewriting(Node t, - LazyCDProof& pf, - TermContext* tctx) -{ - NodeManager* nm = NodeManager::currentNM(); - // Invariant: if visited[hash(t)] = s or rewritten[hash(t)] = s and t,s are - // distinct, then pf is able to generate a proof of t=s. We must - // Node in the domains of the maps below due to hashing creating new (SEXPR) - // nodes. - - // the final rewritten form of terms - std::unordered_map<Node, Node> visited; - // the rewritten form of terms we have processed so far - std::unordered_map<Node, Node> rewritten; - std::unordered_map<Node, Node>::iterator it; - std::unordered_map<Node, Node>::iterator itr; - std::map<Node, std::shared_ptr<ProofNode> >::iterator itc; - Trace("tconv-pf-gen-rewrite") - << "TConvProofGenerator::getProofForRewriting: " << toStringDebug() - << std::endl; - Trace("tconv-pf-gen-rewrite") << "Input: " << t << std::endl; - // if provided, we use term context for cache - std::shared_ptr<TCtxStack> visitctx; - // otherwise, visit is used if we don't have a term context - std::vector<TNode> visit; - Node tinitialHash; - if (tctx != nullptr) - { - visitctx = std::make_shared<TCtxStack>(tctx); - visitctx->pushInitial(t); - tinitialHash = TCtxNode::computeNodeHash(t, tctx->initialValue()); - } - else - { - visit.push_back(t); - tinitialHash = t; - } - Node cur; - uint32_t curCVal = 0; - Node curHash; - do - { - // pop the top element - if (tctx != nullptr) - { - std::pair<Node, uint32_t> curPair = visitctx->getCurrent(); - cur = curPair.first; - curCVal = curPair.second; - curHash = TCtxNode::computeNodeHash(cur, curCVal); - visitctx->pop(); - } - else - { - cur = visit.back(); - curHash = cur; - visit.pop_back(); - } - Trace("tconv-pf-gen-rewrite") << "* visit : " << curHash << std::endl; - // has the proof for cur been cached? - itc = d_cache.find(curHash); - if (itc != d_cache.end()) - { - Node res = itc->second->getResult(); - Assert(res.getKind() == EQUAL); - Assert(!res[1].isNull()); - visited[curHash] = res[1]; - pf.addProof(itc->second); - continue; - } - it = visited.find(curHash); - if (it == visited.end()) - { - Trace("tconv-pf-gen-rewrite") << "- previsit" << std::endl; - visited[curHash] = Node::null(); - // did we rewrite the current node (at pre-rewrite)? - Node rcur = getRewriteStepInternal(curHash, true); - if (!rcur.isNull()) - { - Trace("tconv-pf-gen-rewrite") - << "*** " << curHash << " prerewrites to " << rcur << std::endl; - // d_proof has a proof of cur = rcur. Hence there is nothing - // to do here, as pf will reference d_proof to get its proof. - if (d_policy == TConvPolicy::FIXPOINT) - { - // It may be the case that rcur also rewrites, thus we cannot assign - // the final rewritten form for cur yet. Instead we revisit cur after - // finishing visiting rcur. - rewritten[curHash] = rcur; - if (tctx != nullptr) - { - visitctx->push(cur, curCVal); - visitctx->push(rcur, curCVal); - } - else - { - visit.push_back(cur); - visit.push_back(rcur); - } - } - else - { - Assert(d_policy == TConvPolicy::ONCE); - Trace("tconv-pf-gen-rewrite") << "-> (once, prewrite) " << curHash - << " = " << rcur << std::endl; - // not rewriting again, rcur is final - Assert(!rcur.isNull()); - visited[curHash] = rcur; - doCache(curHash, cur, rcur, pf); - } - } - else if (tctx != nullptr) - { - visitctx->push(cur, curCVal); - // visit operator if apply uf - if (d_rewriteOps && cur.getKind() == APPLY_UF) - { - visitctx->pushOp(cur, curCVal); - } - visitctx->pushChildren(cur, curCVal); - } - else - { - visit.push_back(cur); - // visit operator if apply uf - if (d_rewriteOps && cur.getKind() == APPLY_UF) - { - visit.push_back(cur.getOperator()); - } - visit.insert(visit.end(), cur.begin(), cur.end()); - } - } - else if (it->second.isNull()) - { - itr = rewritten.find(curHash); - if (itr != rewritten.end()) - { - // only can generate partially rewritten nodes when rewrite again is - // true. - Assert(d_policy != TConvPolicy::ONCE); - // if it was rewritten, check the status of the rewritten node, - // which should be finished now - Node rcur = itr->second; - Trace("tconv-pf-gen-rewrite") - << "- postvisit, previously rewritten to " << rcur << std::endl; - Node rcurHash = rcur; - if (tctx != nullptr) - { - rcurHash = TCtxNode::computeNodeHash(rcur, curCVal); - } - Assert(cur != rcur); - // the final rewritten form of cur is the final form of rcur - Node rcurFinal = visited[rcurHash]; - Assert(!rcurFinal.isNull()); - if (rcurFinal != rcur) - { - // must connect via TRANS - std::vector<Node> pfChildren; - pfChildren.push_back(cur.eqNode(rcur)); - pfChildren.push_back(rcur.eqNode(rcurFinal)); - Node result = cur.eqNode(rcurFinal); - pf.addStep(result, PfRule::TRANS, pfChildren, {}); - } - Trace("tconv-pf-gen-rewrite") - << "-> (rewritten postrewrite) " << curHash << " = " << rcurFinal - << std::endl; - visited[curHash] = rcurFinal; - doCache(curHash, cur, rcurFinal, pf); - } - else - { - Trace("tconv-pf-gen-rewrite") << "- postvisit" << std::endl; - Node ret = cur; - Node retHash = curHash; - bool childChanged = false; - std::vector<Node> children; - Kind ck = cur.getKind(); - if (d_rewriteOps && ck == APPLY_UF) - { - // the operator of APPLY_UF is visited - Node cop = cur.getOperator(); - if (tctx != nullptr) - { - uint32_t coval = tctx->computeValueOp(cur, curCVal); - Node coHash = TCtxNode::computeNodeHash(cop, coval); - it = visited.find(coHash); - } - else - { - it = visited.find(cop); - } - Assert(it != visited.end()); - Assert(!it->second.isNull()); - childChanged = childChanged || cop != it->second; - children.push_back(it->second); - } - else if (cur.getMetaKind() == metakind::PARAMETERIZED) - { - // all other parametrized operators are unchanged - children.push_back(cur.getOperator()); - } - // get the results of the children - if (tctx != nullptr) - { - for (size_t i = 0, nchild = cur.getNumChildren(); i < nchild; i++) - { - Node cn = cur[i]; - uint32_t cnval = tctx->computeValue(cur, curCVal, i); - Node cnHash = TCtxNode::computeNodeHash(cn, cnval); - it = visited.find(cnHash); - Assert(it != visited.end()); - Assert(!it->second.isNull()); - childChanged = childChanged || cn != it->second; - children.push_back(it->second); - } - } - else - { - // can use simple loop if not term-context-sensitive - for (const Node& cn : cur) - { - it = visited.find(cn); - Assert(it != visited.end()); - Assert(!it->second.isNull()); - childChanged = childChanged || cn != it->second; - children.push_back(it->second); - } - } - if (childChanged) - { - ret = nm->mkNode(ck, children); - rewritten[curHash] = ret; - // congruence to show (cur = ret) - PfRule congRule = PfRule::CONG; - std::vector<Node> pfChildren; - std::vector<Node> pfArgs; - pfArgs.push_back(ProofRuleChecker::mkKindNode(ck)); - if (ck == APPLY_UF && children[0] != cur.getOperator()) - { - // use HO_CONG if the operator changed - congRule = PfRule::HO_CONG; - pfChildren.push_back(cur.getOperator().eqNode(children[0])); - } - else if (kind::metaKindOf(ck) == kind::metakind::PARAMETERIZED) - { - pfArgs.push_back(cur.getOperator()); - } - for (size_t i = 0, size = cur.getNumChildren(); i < size; i++) - { - if (cur[i] == ret[i]) - { - // ensure REFL proof for unchanged children - pf.addStep(cur[i].eqNode(cur[i]), PfRule::REFL, {}, {cur[i]}); - } - pfChildren.push_back(cur[i].eqNode(ret[i])); - } - Node result = cur.eqNode(ret); - pf.addStep(result, congRule, pfChildren, pfArgs); - // must update the hash - retHash = ret; - if (tctx != nullptr) - { - retHash = TCtxNode::computeNodeHash(ret, curCVal); - } - } - else if (tctx != nullptr) - { - // now we need the hash - retHash = TCtxNode::computeNodeHash(cur, curCVal); - } - // did we rewrite ret (at post-rewrite)? - Node rret = getRewriteStepInternal(retHash, false); - if (!rret.isNull() && d_policy == TConvPolicy::FIXPOINT) - { - Trace("tconv-pf-gen-rewrite") - << "*** " << retHash << " postrewrites to " << rret << std::endl; - // d_proof should have a proof of ret = rret, hence nothing to do - // here, for the same reasons as above. It also may be the case that - // rret rewrites, hence we must revisit ret. - rewritten[retHash] = rret; - if (tctx != nullptr) - { - if (cur != ret) - { - visitctx->push(cur, curCVal); - } - visitctx->push(ret, curCVal); - visitctx->push(rret, curCVal); - } - else - { - if (cur != ret) - { - visit.push_back(cur); - } - visit.push_back(ret); - visit.push_back(rret); - } - } - else - { - // If we changed due to congruence, and then rewrote, then we - // require a trans step to connect here - if (!rret.isNull() && childChanged) - { - std::vector<Node> pfChildren; - pfChildren.push_back(cur.eqNode(ret)); - pfChildren.push_back(ret.eqNode(rret)); - Node result = cur.eqNode(rret); - pf.addStep(result, PfRule::TRANS, pfChildren, {}); - } - // take its rewrite if it rewrote and we have ONCE rewriting policy - ret = rret.isNull() ? ret : rret; - Trace("tconv-pf-gen-rewrite") - << "-> (postrewrite) " << curHash << " = " << ret << std::endl; - // it is final - Assert(!ret.isNull()); - visited[curHash] = ret; - doCache(curHash, cur, ret, pf); - } - } - } - else - { - Trace("tconv-pf-gen-rewrite") << "- already visited" << std::endl; - } - } while (!(tctx != nullptr ? visitctx->empty() : visit.empty())); - Assert(visited.find(tinitialHash) != visited.end()); - Assert(!visited.find(tinitialHash)->second.isNull()); - Trace("tconv-pf-gen-rewrite") - << "...finished, return " << visited[tinitialHash] << std::endl; - // return the conclusion of the overall proof - return t.eqNode(visited[tinitialHash]); -} - -void TConvProofGenerator::doCache(Node curHash, - Node cur, - Node r, - LazyCDProof& pf) -{ - if (d_cpolicy != TConvCachePolicy::NEVER) - { - Node eq = cur.eqNode(r); - d_cache[curHash] = pf.getProofFor(eq); - } -} - -Node TConvProofGenerator::getRewriteStepInternal(Node t, bool isPre) const -{ - const NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap; - NodeNodeMap::const_iterator it = rm.find(t); - if (it == rm.end()) - { - return Node::null(); - } - return (*it).second; -} -std::string TConvProofGenerator::identify() const { return d_name; } - -std::string TConvProofGenerator::toStringDebug() const -{ - std::stringstream ss; - ss << identify() << " (policy=" << d_policy << ", cache policy=" << d_cpolicy - << (d_tcontext != nullptr ? ", term-context-sensitive" : "") << ")"; - return ss.str(); -} - -} // namespace cvc5 diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h deleted file mode 100644 index 70e606db4..000000000 --- a/src/expr/term_conversion_proof_generator.h +++ /dev/null @@ -1,256 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Term conversion proof generator utility. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H -#define CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H - -#include "context/cdhashmap.h" -#include "expr/lazy_proof.h" -#include "expr/proof_generator.h" - -namespace cvc5 { - -class ProofNodeManager; -class TermContext; - -/** A policy for how rewrite steps are applied in TConvProofGenerator */ -enum class TConvPolicy : uint32_t -{ - // steps are applied to fix-point, common use case is PfRule::REWRITE - FIXPOINT, - // steps are applied once at pre-rewrite, common use case is PfRule::SUBS - ONCE, -}; -/** Writes a term conversion policy name to a stream. */ -std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol); - -/** A policy for how proofs are cached in TConvProofGenerator */ -enum class TConvCachePolicy : uint32_t -{ - // proofs are statically cached - STATIC, - // proofs are dynamically cached, cleared when a new rewrite is added - DYNAMIC, - // proofs are never cached - NEVER, -}; -/** Writes a term conversion cache policy name to a stream. */ -std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol); - -/** - * The term conversion proof generator. - * - * This class is used for proofs of t = t', where t' is obtained from t by - * applying (context-free) small step rewrites on subterms of t. Its main - * interface functions are: - * (1) addRewriteStep(t,s,<justification>) which notifies this class that t - * rewrites to s, where justification is either a proof generator or proof - * step, - * (2) getProofFor(f) where f is any equality that can be justified by the - * rewrite steps given above. - * - * For example, say we make the following calls: - * addRewriteStep(a,b,P1) - * addRewriteStep(f(a),c,P2) - * addRewriteStep(c,d,P3) - * where P1 and P2 are proof steps. Afterwards, this class may justify any - * equality t = s where s is obtained by applying the rewrites a->b, f(a)->c, - * c->d, based on the strategy outlined below [***]. For example, the call to: - * getProofFor(g(f(a),h(a),f(e)) = g(d,h(b),f(e))) - * will return the proof: - * CONG( - * TRANS(P2,P3), ; f(a)=d - * CONG(P1 :args h), ; h(a)=h(b) - * REFL(:args f(e)) ; f(e)=f(e) - * :args g) - * - * [***] This class traverses the left hand side of a given equality-to-prove - * (the term g(f(a),h(a),e) in the above example) and "replays" the rewrite - * steps to obtain its rewritten form. To do so, it applies any available - * rewrite step at pre-rewrite (pre-order traversal) and post-rewrite - * (post-order traversal) based on whether the user specified pre-rewrite or a - * post-rewrite during addRewriteStep. - * - * This class may additionally be used for term-context-sensitive rewrite - * systems. An example is the term formula removal pass which rewrites - * terms dependending on whether they occur in a "term position", for details - * see RtfTermContext in expr/term_context.h. To use this class in a way - * that takes into account term contexts, the user of the term conversion - * proof generator should: - * (1) Provide a term context callback to the constructor of this class (tccb), - * (2) Register rewrite steps that indicate the term context identifier of - * the rewrite, which is a uint32_t. - * - * For example, RtfTermContext uses hash value 2 to indicate we are in a "term - * position". Say the user of this class calls: - * addRewriteStep( (and A B), BOOLEAN_TERM_VARIABLE_1, pg, true, 2) - * This indicates that (and A B) should rewrite to BOOLEAN_TERM_VARIABLE_1 if - * (and A B) occurs in a term position, where pg is a proof generator that can - * provide a closed proof of: - * (= (and A B) BOOLEAN_TERM_VARIABLE_1) - * Subsequently, this class may respond to a call to getProofFor on: - * (= - * (or (and A B) (P (and A B))) - * (or (and A B) (P BOOLEAN_TERM_VARIABLE_1))) - * where P is a predicate Bool -> Bool. The proof returned by this class - * involves congruence and pg's proof of the equivalence above. In particular, - * assuming its proof of the equivalence is P1, this proof is: - * (CONG{=} (CONG{or} (REFL (and A B)) (CONG{P} P1))) - * Notice the callback provided to this class ensures that the rewrite is - * replayed in the expected way, e.g. the occurrence of (and A B) that is not - * in term position is not rewritten. - */ -class TConvProofGenerator : public ProofGenerator -{ - public: - /** - * Constructor, which notice does fixpoint rewriting (since this is the - * most common use case) and never caches. - * - * @param pnm The proof node manager for constructing ProofNode objects. - * @param c The context that this class depends on. If none is provided, - * this class is context-independent. - * @param tpol The policy for applying rewrite steps of this class. For - * details, see d_policy. - * @param cpol The caching policy for this generator. - * @param name The name of this generator (for debugging). - * @param tccb The term context callback that this class depends on. If this - * is non-null, then this class stores a term-context-sensitive rewrite - * system. The rewrite steps should be given term context identifiers. - */ - TConvProofGenerator(ProofNodeManager* pnm, - context::Context* c = nullptr, - TConvPolicy pol = TConvPolicy::FIXPOINT, - TConvCachePolicy cpol = TConvCachePolicy::NEVER, - std::string name = "TConvProofGenerator", - TermContext* tccb = nullptr, - bool rewriteOps = false); - ~TConvProofGenerator(); - /** - * Add rewrite step t --> s based on proof generator. - * - * @param isPre Whether the rewrite is applied at prerewrite (pre-order - * traversal). - * @param trustId If a null proof generator is provided, we add a step to - * the proof that has trustId as the rule and expected as the sole argument. - * @param isClosed whether to expect that pg can provide a closed proof for - * this fact. - * @param tctx The term context identifier for the rewrite step. This - * value should correspond to one generated by the term context callback - * class provided in the argument tccb provided to the constructor of this - * class. - */ - void addRewriteStep(Node t, - Node s, - ProofGenerator* pg, - bool isPre = false, - PfRule trustId = PfRule::ASSUME, - bool isClosed = false, - uint32_t tctx = 0); - /** Same as above, for a single step */ - void addRewriteStep( - Node t, Node s, ProofStep ps, bool isPre = false, uint32_t tctx = 0); - /** Same as above, with explicit arguments */ - void addRewriteStep(Node t, - Node s, - PfRule id, - const std::vector<Node>& children, - const std::vector<Node>& args, - bool isPre = false, - uint32_t tctx = 0); - /** Has rewrite step for term t */ - bool hasRewriteStep(Node t, uint32_t tctx = 0, bool isPre = false) const; - /** - * Get rewrite step for term t, returns the s provided in a call to - * addRewriteStep if one exists, or null otherwise. - */ - Node getRewriteStep(Node t, uint32_t tctx = 0, bool isPre = false) const; - /** - * Get the proof for formula f. It should be the case that f is of the form - * t = t', where t' is the result of rewriting t based on the rewrite steps - * registered to this class. - * - * @param f The equality fact to get the proof for. - * @return The proof for f. - */ - std::shared_ptr<ProofNode> getProofFor(Node f) override; - /** Identify this generator (for debugging, etc..) */ - std::string identify() const override; - /** - * Get the proof for how term n would rewrite. This is in contrast to the - * above method where the user provides an equality (= n n'). The motivation - * for this method is when it may be expensive to compute n', and hence it - * is preferred that the proof checker computes the rewritten form of - * n, instead of verifying that n has rewritten form n'. - */ - std::shared_ptr<ProofNode> getProofForRewriting(Node n); - - protected: - typedef context::CDHashMap<Node, Node> NodeNodeMap; - /** A dummy context used by this class if none is provided */ - context::Context d_context; - /** The (lazy) context dependent proof object. */ - LazyCDProof d_proof; - /** map to rewritten forms */ - NodeNodeMap d_preRewriteMap; - NodeNodeMap d_postRewriteMap; - /** - * Policy for how rewrites are applied to terms. As a simple example, say we - * have registered the rewrite steps: - * addRewriteStep( a, f(c), p1 ) - * addRewriteStep( c, d, p2 ) - * Then getProofForRewriting(f(a,c),pf) returns a proof of: - * f(a,c) = f(f(d),d) if d_policy is FIXPOINT, - * f(a,c) = f(f(c),d) if d_policy is ONCE. - */ - TConvPolicy d_policy; - /** The cache policy */ - TConvCachePolicy d_cpolicy; - /** Name identifier */ - std::string d_name; - /** The cache for terms */ - std::map<Node, std::shared_ptr<ProofNode> > d_cache; - /** An (optional) term context object */ - TermContext* d_tcontext; - /** - * Whether we rewrite operators. If this flag is true, then the main - * traversal algorithm of this proof generator traverses operators of - * APPLY_UF and uses HO_CONG to justify rewriting of subterms when necessary. - */ - bool d_rewriteOps; - /** Get rewrite step for (hash value of) term. */ - Node getRewriteStepInternal(Node thash, bool isPre) const; - /** - * Adds a proof of t = t' to the proof pf where t' is the result of rewriting - * t based on the rewrite steps registered to this class. This method then - * returns the proved equality t = t'. - */ - Node getProofForRewriting(Node t, LazyCDProof& pf, TermContext* tc = nullptr); - /** - * Register rewrite step, returns the equality t=s if t is distinct from s - * and a rewrite step has not already been registered for t. - */ - Node registerRewriteStep(Node t, Node s, uint32_t tctx, bool isPre); - /** cache that r is the rewritten form of cur, pf can provide a proof */ - void doCache(Node curHash, Node cur, Node r, LazyCDProof& pf); - /** get debug information on this generator */ - std::string toStringDebug() const; -}; - -} // namespace cvc5 - -#endif /* CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */ |