This removes namespace theory from proof utilities, and moves MethodId to its own file in src/proof/.
proof/lazy_proof_chain.h
proof/lazy_tree_proof_generator.cpp
proof/lazy_tree_proof_generator.h
+ proof/method_id.cpp
+ proof/method_id.h
proof/proof.cpp
proof/proof.h
proof/proof_checker.cpp
}
}
-void AssertionPipeline::pushBackTrusted(theory::TrustNode trn)
+void AssertionPipeline::pushBackTrusted(TrustNode trn)
{
- Assert(trn.getKind() == theory::TrustNodeKind::LEMMA);
+ Assert(trn.getKind() == TrustNodeKind::LEMMA);
// push back what was proven
push_back(trn.getProven(), false, false, trn.getGenerator());
}
d_nodes[i] = n;
}
-void AssertionPipeline::replaceTrusted(size_t i, theory::TrustNode trn)
+void AssertionPipeline::replaceTrusted(size_t i, TrustNode trn)
{
if (trn.isNull())
{
// null trust node denotes no change, nothing to do
return;
}
- Assert(trn.getKind() == theory::TrustNodeKind::REWRITE);
+ Assert(trn.getKind() == TrustNodeKind::REWRITE);
Assert(trn.getProven()[0] == d_nodes[i]);
replace(i, trn.getNode(), trn.getGenerator());
}
bool isInput = false,
ProofGenerator* pg = nullptr);
/** Same as above, with TrustNode */
- void pushBackTrusted(theory::TrustNode trn);
+ void pushBackTrusted(TrustNode trn);
/**
* Get the constant reference to the underlying assertions. It is only
* Same as above, with TrustNode trn, which is of kind REWRITE and proves
* d_nodes[i] = n for some n.
*/
- void replaceTrusted(size_t i, theory::TrustNode trn);
+ void replaceTrusted(size_t i, TrustNode trn);
IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
const IteSkolemMap& getIteSkolemMap() const { return d_iteSkolemMap; }
for (unsigned i = 0, size = assertions->size(); i < size; ++i)
{
Node assertion = (*assertions)[i];
- std::vector<theory::TrustNode> newAsserts;
+ std::vector<TrustNode> newAsserts;
std::vector<Node> newSkolems;
TrustNode trn = pe->removeItes(assertion, newAsserts, newSkolems);
if (!trn.isNull())
return lit;
}
-Node NonClausalSimp::processRewrittenLearnedLit(theory::TrustNode trn)
+Node NonClausalSimp::processRewrittenLearnedLit(TrustNode trn)
{
if (isProofEnabled())
{
* This tracks the proof in the learned literal preprocess proof generator
* d_llpg below and returns the rewritten learned literal.
*/
- Node processRewrittenLearnedLit(theory::TrustNode trn);
+ Node processRewrittenLearnedLit(TrustNode trn);
/** Is proof enabled? */
bool isProofEnabled() const;
/** The proof node manager */
for (unsigned i = 0, size = assertions->size(); i < size; ++i)
{
Node assertion = (*assertions)[i];
- std::vector<theory::TrustNode> newAsserts;
+ std::vector<TrustNode> newAsserts;
std::vector<Node> newSkolems;
TrustNode trn = propEngine->preprocess(assertion, newAsserts, newSkolems);
if (!trn.isNull())
return PreprocessingPassResult::NO_CONFLICT;
}
-theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n)
+TrustNode TheoryRewriteEq::rewriteAssertion(TNode n)
{
NodeManager* nm = NodeManager::currentNM();
TheoryEngine* te = d_preprocContext->getTheoryEngine();
if (ret.getKind() == kind::EQUAL && !ret[0].getType().isBoolean())
{
// For example, (= x y) ---> (and (>= x y) (<= x y))
- theory::TrustNode trn = te->ppRewriteEquality(ret);
+ TrustNode trn = te->ppRewriteEquality(ret);
// can make proof producing by using proof generator from trn
ret = trn.isNull() ? Node(ret) : trn.getNode();
}
* (= x y) ---> (and (>= x y) (<= x y))
* Returns the trust node corresponding to the rewrite.
*/
- theory::TrustNode rewriteAssertion(TNode assertion);
+ TrustNode rewriteAssertion(TNode assertion);
};
} // namespace passes
return d_pnm->mkTrans(transChildren, f);
}
-theory::TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence(
+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();
+ return TrustNode::null();
}
bool useThis = false;
ProofGenerator* pg = nullptr;
}
}
Assert(pg != nullptr);
- return theory::TrustNode::mkTrustRewrite(
- cterms[0], cterms[cterms.size() - 1], pg);
+ return TrustNode::mkTrustRewrite(cterms[0], cterms[cterms.size() - 1], pg);
}
std::string TConvSeqProofGenerator::identify() const { return d_name; }
* 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);
+ TrustNode mkTrustRewriteSequence(const std::vector<Node>& cterms);
protected:
using NodeIndexPairHashFunction =
#include "proof/proof_node_manager.h"
namespace cvc5 {
-namespace theory {
EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm,
context::Context* c,
std::string EagerProofGenerator::identify() const { return d_name; }
-} // namespace theory
} // namespace cvc5
class ProofNode;
class ProofNodeManager;
-namespace theory {
-
/**
* An eager proof generator, with explicit proof caching.
*
NodeProofNodeMap d_proofs;
};
-} // namespace theory
} // namespace cvc5
#endif /* CVC5__PROOF__PROOF_GENERATOR_H */
#include "proof/proof_node_manager.h"
namespace cvc5 {
-namespace theory {
LazyTreeProofGenerator::LazyTreeProofGenerator(ProofNodeManager* pnm,
const std::string& name)
return os;
}
-} // namespace theory
} // namespace cvc5
#include "proof/proof_node_manager.h"
namespace cvc5 {
-namespace theory {
namespace detail {
/**
* A single node in the proof tree created by the LazyTreeProofGenerator.
*/
std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg);
-} // namespace theory
} // namespace cvc5
#endif
--- /dev/null
+/******************************************************************************
+ * 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 method identifier
+ */
+
+#include "proof/method_id.h"
+
+#include "proof/proof_checker.h"
+#include "util/rational.h"
+
+namespace cvc5 {
+
+const char* toString(MethodId id)
+{
+ switch (id)
+ {
+ case MethodId::RW_REWRITE: return "RW_REWRITE";
+ case MethodId::RW_EXT_REWRITE: return "RW_EXT_REWRITE";
+ case MethodId::RW_REWRITE_EQ_EXT: return "RW_REWRITE_EQ_EXT";
+ case MethodId::RW_EVALUATE: return "RW_EVALUATE";
+ case MethodId::RW_IDENTITY: return "RW_IDENTITY";
+ case MethodId::RW_REWRITE_THEORY_PRE: return "RW_REWRITE_THEORY_PRE";
+ case MethodId::RW_REWRITE_THEORY_POST: return "RW_REWRITE_THEORY_POST";
+ case MethodId::SB_DEFAULT: return "SB_DEFAULT";
+ case MethodId::SB_LITERAL: return "SB_LITERAL";
+ case MethodId::SB_FORMULA: return "SB_FORMULA";
+ case MethodId::SBA_SEQUENTIAL: return "SBA_SEQUENTIAL";
+ case MethodId::SBA_SIMUL: return "SBA_SIMUL";
+ case MethodId::SBA_FIXPOINT: return "SBA_FIXPOINT";
+ default: return "MethodId::Unknown";
+ };
+}
+
+std::ostream& operator<<(std::ostream& out, MethodId id)
+{
+ out << toString(id);
+ return out;
+}
+
+Node mkMethodId(MethodId id)
+{
+ return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(id)));
+}
+
+bool getMethodId(TNode n, MethodId& i)
+{
+ uint32_t index;
+ if (!ProofRuleChecker::getUInt32(n, index))
+ {
+ return false;
+ }
+ i = static_cast<MethodId>(index);
+ return true;
+}
+
+bool getMethodIds(const std::vector<Node>& args,
+ MethodId& ids,
+ MethodId& ida,
+ MethodId& idr,
+ size_t index)
+{
+ ids = MethodId::SB_DEFAULT;
+ ida = MethodId::SBA_SEQUENTIAL;
+ idr = MethodId::RW_REWRITE;
+ for (size_t offset = 0; offset <= 2; offset++)
+ {
+ if (args.size() > index + offset)
+ {
+ MethodId& id = offset == 0 ? ids : (offset == 1 ? ida : idr);
+ if (!getMethodId(args[index + offset], id))
+ {
+ Trace("builtin-pfcheck")
+ << "Failed to get id from " << args[index + offset] << std::endl;
+ return false;
+ }
+ }
+ else
+ {
+ break;
+ }
+ }
+ Trace("builtin-pfcheck") << "Got MethodIds ids/ida/idr: " << ids << " / "
+ << ida << " / " << idr << "\n";
+ return true;
+}
+
+void addMethodIds(std::vector<Node>& args,
+ MethodId ids,
+ MethodId ida,
+ MethodId idr)
+{
+ bool ndefRewriter = (idr != MethodId::RW_REWRITE);
+ bool ndefApply = (ida != MethodId::SBA_SEQUENTIAL);
+ if (ids != MethodId::SB_DEFAULT || ndefRewriter || ndefApply)
+ {
+ args.push_back(mkMethodId(ids));
+ }
+ if (ndefApply || ndefRewriter)
+ {
+ args.push_back(mkMethodId(ida));
+ }
+ if (ndefRewriter)
+ {
+ args.push_back(mkMethodId(idr));
+ }
+}
+
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Method identifier enumeration
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PROOF__METHOD_ID_H
+#define CVC5__PROOF__METHOD_ID_H
+
+#include "expr/node.h"
+
+namespace cvc5 {
+
+/**
+ * Identifiers for rewriters and substitutions, which we abstractly
+ * classify as "methods". Methods have a unique identifier in the internal
+ * proof calculus implemented by the checker below.
+ *
+ * A "rewriter" is abstractly a method from Node to Node, where the output
+ * is semantically equivalent to the input. The identifiers below list
+ * various methods that have this contract. This identifier is used
+ * in a number of the builtin rules.
+ *
+ * A substitution is a method for turning a formula into a substitution.
+ */
+enum class MethodId : uint32_t
+{
+ //---------------------------- Rewriters
+ // Rewriter::rewrite(n)
+ RW_REWRITE,
+ // d_ext_rew.extendedRewrite(n);
+ RW_EXT_REWRITE,
+ // Rewriter::rewriteExtEquality(n)
+ RW_REWRITE_EQ_EXT,
+ // Evaluator::evaluate(n)
+ RW_EVALUATE,
+ // identity
+ RW_IDENTITY,
+ // theory preRewrite, note this is only intended to be used as an argument
+ // to THEORY_REWRITE in the final proof. It is not implemented in
+ // applyRewrite below, see documentation in proof_rule.h for THEORY_REWRITE.
+ RW_REWRITE_THEORY_PRE,
+ // same as above, for theory postRewrite
+ RW_REWRITE_THEORY_POST,
+ //---------------------------- Substitutions
+ // (= x y) is interpreted as x -> y, using Node::substitute
+ SB_DEFAULT,
+ // P, (not P) are interpreted as P -> true, P -> false using Node::substitute
+ SB_LITERAL,
+ // P is interpreted as P -> true using Node::substitute
+ SB_FORMULA,
+ //---------------------------- Substitution applications
+ // multiple substitutions are applied sequentially
+ SBA_SEQUENTIAL,
+ // multiple substitutions are applied simultaneously
+ SBA_SIMUL,
+ // multiple substitutions are applied to fix point
+ SBA_FIXPOINT
+ // For example, for x -> u, y -> f(z), z -> g(x), applying this substituion to
+ // y gives:
+ // - f(g(x)) for SBA_SEQUENTIAL
+ // - f(z) for SBA_SIMUL
+ // - f(g(u)) for SBA_FIXPOINT
+ // Notice that SBA_FIXPOINT should provide a terminating rewrite system
+ // as a substitution, or else non-termination will occur during proof
+ // checking.
+};
+/** Converts a rewriter id to a string. */
+const char* toString(MethodId id);
+/** Write a rewriter id to out */
+std::ostream& operator<<(std::ostream& out, MethodId id);
+/** Make a method id node */
+Node mkMethodId(MethodId id);
+
+/** get a method identifier from a node, return false if we fail */
+bool getMethodId(TNode n, MethodId& i);
+/**
+ * Get method identifiers from args starting at the given index. Store their
+ * values into ids, ida, and idr. This method returns false if args does not
+ * contain valid method identifiers at position index in args.
+ */
+bool getMethodIds(const std::vector<Node>& args,
+ MethodId& ids,
+ MethodId& ida,
+ MethodId& idr,
+ size_t index);
+/**
+ * Add method identifiers ids, ida and idr as nodes to args. This does not add
+ * ids, ida or idr if their values are the default ones.
+ */
+void addMethodIds(std::vector<Node>& args,
+ MethodId ids,
+ MethodId ida,
+ MethodId idr);
+
+} // namespace cvc5
+
+#endif /* CVC5__PROOF__METHOD_ID_H */
using namespace cvc5::kind;
namespace cvc5 {
-namespace theory {
TheoryProofStepBuffer::TheoryProofStepBuffer(ProofChecker* pc)
: ProofStepBuffer(pc)
{
std::vector<Node> args;
args.push_back(src);
- builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
+ addMethodIds(args, ids, ida, idr);
Node res = tryStep(PfRule::MACRO_SR_EQ_INTRO, exp, args);
if (res.isNull())
{
// try to prove that tgt rewrites to src
children.insert(children.end(), exp.begin(), exp.end());
args.push_back(tgt);
- builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
+ addMethodIds(args, ids, ida, idr);
Node res = tryStep(PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
if (res.isNull())
{
{
std::vector<Node> args;
args.push_back(tgt);
- builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
+ addMethodIds(args, ids, ida, idr);
Node res = tryStep(PfRule::MACRO_SR_PRED_INTRO, exp, args);
if (res.isNull())
{
children.push_back(src);
children.insert(children.end(), exp.begin(), exp.end());
std::vector<Node> args;
- builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
+ addMethodIds(args, ids, ida, idr);
Node srcRew = tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args);
if (CDProof::isSame(src, srcRew))
{
return n;
}
-} // namespace theory
} // namespace cvc5
#include "theory/builtin/proof_checker.h"
namespace cvc5 {
-namespace theory {
/**
* Class used to speculatively try and buffer a set of proof steps before
* sending them to a proof object, extended with theory-specfic proof rule
Node elimDoubleNegLit(Node n);
};
-} // namespace theory
} // namespace cvc5
#endif /* CVC5__PROOF__THEORY_PROOF_STEP_BUFFER_H */
#include "proof/proof_generator.h"
namespace cvc5 {
-namespace theory {
const char* toString(TrustNodeKind tnk)
{
return out;
}
-} // namespace theory
} // namespace cvc5
class ProofGenerator;
class ProofNode;
-namespace theory {
-
/** A kind for trust nodes */
enum class TrustNodeKind : uint32_t
{
*/
std::ostream& operator<<(std::ostream& out, TrustNode n);
-} // namespace theory
} // namespace cvc5
#endif /* CVC5__PROOF__TRUST_NODE_H */
}
}
-void ProofCnfStream::convertPropagation(theory::TrustNode trn)
+void ProofCnfStream::convertPropagation(TrustNode trn)
{
Node proven = trn.getProven();
Trace("cnf") << "ProofCnfStream::convertPropagation: proven explanation"
* clause in the SAT solver, as this is handled internally by the SAT
* solver. The clausification steps and the generator within the trust node
* are saved in d_proof if we are producing proofs in the theory engine. */
- void convertPropagation(theory::TrustNode ttn);
+ void convertPropagation(TrustNode ttn);
/**
* Ensure that the given node will have a designated SAT literal that is
* definitionally equal to it. The result of this function is that the Node
LazyCDProof d_proof;
/** An accumulator of steps that may be applied to normalize the clauses
* generated during clausification. */
- theory::TheoryProofStepBuffer d_psb;
+ TheoryProofStepBuffer d_psb;
/** Blocked proofs.
*
* These are proof nodes added to this class by external generators. */
delete d_theoryProxy;
}
-theory::TrustNode PropEngine::preprocess(
- TNode node,
- std::vector<theory::TrustNode>& newLemmas,
- std::vector<Node>& newSkolems)
+TrustNode PropEngine::preprocess(TNode node,
+ std::vector<TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems)
{
return d_theoryProxy->preprocess(node, newLemmas, newSkolems);
}
-theory::TrustNode PropEngine::removeItes(
- TNode node,
- std::vector<theory::TrustNode>& newLemmas,
- std::vector<Node>& newSkolems)
+TrustNode PropEngine::removeItes(TNode node,
+ std::vector<TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems)
{
return d_theoryProxy->removeItes(node, newLemmas, newSkolems);
}
}
}
-void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
+void PropEngine::assertLemma(TrustNode tlemma, theory::LemmaProperty p)
{
bool removable = isLemmaPropertyRemovable(p);
// call preprocessor
- std::vector<theory::TrustNode> ppLemmas;
+ std::vector<TrustNode> ppLemmas;
std::vector<Node> ppSkolems;
- theory::TrustNode tplemma =
+ TrustNode tplemma =
d_theoryProxy->preprocessLemma(tlemma, ppLemmas, ppSkolems);
Assert(ppSkolems.size() == ppLemmas.size());
assertLemmasInternal(tplemma, ppLemmas, ppSkolems, removable);
}
-void PropEngine::assertTrustedLemmaInternal(theory::TrustNode trn,
- bool removable)
+void PropEngine::assertTrustedLemmaInternal(TrustNode trn, bool removable)
{
Node node = trn.getNode();
Debug("prop::lemmas") << "assertLemma(" << node << ")" << std::endl;
- bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
+ bool negated = trn.getKind() == TrustNodeKind::CONFLICT;
Assert(
!isProofEnabled() || trn.getGenerator() != nullptr
|| options::unsatCores()
}
}
-void PropEngine::assertLemmasInternal(
- theory::TrustNode trn,
- const std::vector<theory::TrustNode>& ppLemmas,
- const std::vector<Node>& ppSkolems,
- bool removable)
+void PropEngine::assertLemmasInternal(TrustNode trn,
+ const std::vector<TrustNode>& ppLemmas,
+ const std::vector<Node>& ppSkolems,
+ bool removable)
{
if (!trn.isNull())
{
assertTrustedLemmaInternal(trn, removable);
}
- for (const theory::TrustNode& tnl : ppLemmas)
+ for (const TrustNode& tnl : ppLemmas)
{
assertTrustedLemmaInternal(tnl, removable);
}
Node PropEngine::getPreprocessedTerm(TNode n)
{
// must preprocess
- std::vector<theory::TrustNode> newLemmas;
+ std::vector<TrustNode> newLemmas;
std::vector<Node> newSkolems;
- theory::TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas, newSkolems);
+ TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas, newSkolems);
// send lemmas corresponding to the skolems introduced by preprocessing n
- theory::TrustNode trnNull;
+ TrustNode trnNull;
assertLemmasInternal(trnNull, newLemmas, newSkolems, false);
return tpn.isNull() ? Node(n) : tpn.getNode();
}
* @return The (REWRITE) trust node corresponding to rewritten node via
* preprocessing.
*/
- theory::TrustNode preprocess(TNode node,
- std::vector<theory::TrustNode>& ppLemmas,
- std::vector<Node>& ppSkolems);
+ TrustNode preprocess(TNode node,
+ std::vector<TrustNode>& ppLemmas,
+ std::vector<Node>& ppSkolems);
/**
* Remove term ITEs (and more generally, term formulas) from the given node.
* Return the REWRITE trust node corresponding to rewriting node. New lemmas
* @return The (REWRITE) trust node corresponding to rewritten node via
* preprocessing.
*/
- theory::TrustNode removeItes(TNode node,
- std::vector<theory::TrustNode>& ppLemmas,
- std::vector<Node>& ppSkolems);
+ TrustNode removeItes(TNode node,
+ std::vector<TrustNode>& ppLemmas,
+ std::vector<Node>& ppSkolems);
/**
* Converts the given formulas to CNF and assert the CNF to the SAT solver.
* @param trn the trust node storing the formula to assert
* @param p the properties of the lemma
*/
- void assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p);
+ void assertLemma(TrustNode tlemma, theory::LemmaProperty p);
/**
* If ever n is decided upon, it must be in the given phase. This
* @param removable whether this lemma can be quietly removed based
* on an activity heuristic
*/
- void assertTrustedLemmaInternal(theory::TrustNode trn, bool removable);
+ void assertTrustedLemmaInternal(TrustNode trn, bool removable);
/**
* Assert node as a formula to the CNF stream
* @param node The formula to assert
* skolem definitions and skolems obtained from preprocessing it, and
* removable is whether the lemma is removable.
*/
- void assertLemmasInternal(theory::TrustNode trn,
- const std::vector<theory::TrustNode>& ppLemmas,
+ void assertLemmasInternal(TrustNode trn,
+ const std::vector<TrustNode>& ppLemmas,
const std::vector<Node>& ppSkolems,
bool removable);
TNode lNode = d_cnfStream->getNode(l);
Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
- theory::TrustNode tte = d_theoryEngine->getExplanation(lNode);
+ TrustNode tte = d_theoryEngine->getExplanation(lNode);
Node theoryExplanation = tte.getNode();
if (options::produceProofs()
&& options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS)
CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; }
-theory::TrustNode TheoryProxy::preprocessLemma(
- theory::TrustNode trn,
- std::vector<theory::TrustNode>& newLemmas,
- std::vector<Node>& newSkolems)
+TrustNode TheoryProxy::preprocessLemma(TrustNode trn,
+ std::vector<TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems)
{
return d_tpp.preprocessLemma(trn, newLemmas, newSkolems);
}
-theory::TrustNode TheoryProxy::preprocess(
- TNode node,
- std::vector<theory::TrustNode>& newLemmas,
- std::vector<Node>& newSkolems)
+TrustNode TheoryProxy::preprocess(TNode node,
+ std::vector<TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems)
{
return d_tpp.preprocess(node, newLemmas, newSkolems);
}
-theory::TrustNode TheoryProxy::removeItes(
- TNode node,
- std::vector<theory::TrustNode>& newLemmas,
- std::vector<Node>& newSkolems)
+TrustNode TheoryProxy::removeItes(TNode node,
+ std::vector<TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems)
{
RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas();
return rtf.run(node, newLemmas, newSkolems, true);
* Call the preprocessor on node, return trust node corresponding to the
* rewrite.
*/
- theory::TrustNode preprocessLemma(theory::TrustNode trn,
- std::vector<theory::TrustNode>& newLemmas,
- std::vector<Node>& newSkolems);
+ TrustNode preprocessLemma(TrustNode trn,
+ std::vector<TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems);
/**
* Call the preprocessor on node, return trust node corresponding to the
* rewrite.
*/
- theory::TrustNode preprocess(TNode node,
- std::vector<theory::TrustNode>& newLemmas,
- std::vector<Node>& newSkolems);
+ TrustNode preprocess(TNode node,
+ std::vector<TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems);
/**
* Remove ITEs from the node.
*/
- theory::TrustNode removeItes(TNode node,
- std::vector<theory::TrustNode>& newLemmas,
- std::vector<Node>& newSkolems);
+ TrustNode removeItes(TNode node,
+ std::vector<TrustNode>& newLemmas,
+ std::vector<Node>& newSkolems);
/**
* Get the skolems within node and their corresponding definitions, store
* them in sks and skAsserts respectively. Note that this method does not
* Helper function for above, called to specify if we want proof production
* based on the optional argument tpg.
*/
- theory::TrustNode expandDefinitions(TNode n,
- std::unordered_map<Node, Node>& cache,
- TConvProofGenerator* tpg);
+ TrustNode expandDefinitions(TNode n,
+ std::unordered_map<Node, Node>& cache,
+ TConvProofGenerator* tpg);
/** Reference to the environment. */
Env& d_env;
/** Reference to the SMT stats */
{
checkEagerPedantic(d_ra);
}
- d_src[n] = theory::TrustNode::mkTrustLemma(n, pg);
+ d_src[n] = TrustNode::mkTrustLemma(n, pg);
}
else
{
}
}
-void PreprocessProofGenerator::notifyNewTrustedAssert(theory::TrustNode tn)
+void PreprocessProofGenerator::notifyNewTrustedAssert(TrustNode tn)
{
notifyNewAssert(tn.getProven(), tn.getGenerator());
}
return;
}
// call the trusted version
- notifyTrustedPreprocessed(theory::TrustNode::mkTrustRewrite(n, np, pg));
+ notifyTrustedPreprocessed(TrustNode::mkTrustRewrite(n, np, pg));
}
-void PreprocessProofGenerator::notifyTrustedPreprocessed(theory::TrustNode tnp)
+void PreprocessProofGenerator::notifyTrustedPreprocessed(TrustNode tnp)
{
if (tnp.isNull())
{
// no rewrite, nothing to do
return;
}
- Assert(tnp.getKind() == theory::TrustNodeKind::REWRITE);
+ Assert(tnp.getKind() == TrustNodeKind::REWRITE);
Node np = tnp.getNode();
Trace("smt-proof-pp-debug")
<< "PreprocessProofGenerator::notifyPreprocessed: " << tnp.getProven()
}
Trace("smt-pppg") << "...update" << std::endl;
- theory::TrustNodeKind tnk = (*it).second.getKind();
- if (tnk == theory::TrustNodeKind::REWRITE)
+ TrustNodeKind tnk = (*it).second.getKind();
+ if (tnk == TrustNodeKind::REWRITE)
{
Trace("smt-pppg") << "...rewritten from " << proven[0] << std::endl;
Assert(proven.getKind() == kind::EQUAL);
else
{
Trace("smt-pppg") << "...lemma" << std::endl;
- Assert(tnk == theory::TrustNodeKind::LEMMA);
+ Assert(tnk == TrustNodeKind::LEMMA);
}
if (!proofStepProcessed)
{
Trace("smt-pppg") << "...add missing step" << std::endl;
// add trusted step, the rule depends on the kind of trust node
- cdp.addStep(proven,
- tnk == theory::TrustNodeKind::LEMMA ? d_ra : d_rpp,
- {},
- {proven});
+ cdp.addStep(
+ proven, tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp, {}, {proven});
}
}
} while (success);
*/
class PreprocessProofGenerator : public ProofGenerator
{
- typedef context::CDHashMap<Node, theory::TrustNode> NodeTrustNodeMap;
+ typedef context::CDHashMap<Node, TrustNode> NodeTrustNodeMap;
public:
/**
*/
void notifyNewAssert(Node n, ProofGenerator* pg);
/** Notify a new assertion, trust node version. */
- void notifyNewTrustedAssert(theory::TrustNode tn);
+ void notifyNewTrustedAssert(TrustNode tn);
/**
* Notify that n was replaced by np due to preprocessing, where pg can
* provide a proof of the equality n=np.
*/
void notifyPreprocessed(Node n, Node np, ProofGenerator* pg);
/** Notify preprocessed, trust node version */
- void notifyTrustedPreprocessed(theory::TrustNode tnp);
+ void notifyTrustedPreprocessed(TrustNode tnp);
/**
* Get proof for f, which returns a proof based on proving an equality based
* on transitivity of preprocessing steps, and then using the original
MethodId ids = MethodId::SB_DEFAULT;
if (args.size() >= 2)
{
- if (builtin::BuiltinProofRuleChecker::getMethodId(args[1], ids))
+ if (getMethodId(args[1], ids))
{
sargs.push_back(args[1]);
}
MethodId ida = MethodId::SBA_SEQUENTIAL;
if (args.size() >= 3)
{
- if (builtin::BuiltinProofRuleChecker::getMethodId(args[2], ida))
+ if (getMethodId(args[2], ida))
{
sargs.push_back(args[2]);
}
MethodId idr = MethodId::RW_REWRITE;
if (args.size() >= 4)
{
- if (builtin::BuiltinProofRuleChecker::getMethodId(args[3], idr))
+ if (getMethodId(args[3], idr))
{
rargs.push_back(args[3]);
}
MethodId ids = MethodId::SB_DEFAULT;
if (args.size() >= 2)
{
- builtin::BuiltinProofRuleChecker::getMethodId(args[1], ids);
+ getMethodId(args[1], ids);
}
MethodId ida = MethodId::SBA_SEQUENTIAL;
if (args.size() >= 3)
{
- builtin::BuiltinProofRuleChecker::getMethodId(args[2], ida);
+ getMethodId(args[2], ida);
}
std::vector<std::shared_ptr<CDProof>> pfs;
std::vector<TNode> vsList;
MethodId idr = MethodId::RW_REWRITE;
if (args.size() >= 2)
{
- builtin::BuiltinProofRuleChecker::getMethodId(args[1], idr);
+ getMethodId(args[1], idr);
}
builtin::BuiltinProofRuleChecker* builtinPfC =
static_cast<builtin::BuiltinProofRuleChecker*>(
RemoveTermFormulas::~RemoveTermFormulas() {}
-theory::TrustNode RemoveTermFormulas::run(
- TNode assertion,
- std::vector<theory::TrustNode>& newAsserts,
- std::vector<Node>& newSkolems,
- bool fixedPoint)
+TrustNode RemoveTermFormulas::run(TNode assertion,
+ std::vector<TrustNode>& newAsserts,
+ std::vector<Node>& newSkolems,
+ bool fixedPoint)
{
Node itesRemoved = runInternal(assertion, newAsserts, newSkolems);
Assert(newAsserts.size() == newSkolems.size());
if (itesRemoved == assertion)
{
- return theory::TrustNode::null();
+ return TrustNode::null();
}
// if running to fixed point, we run each new assertion through the
// run lemma method
size_t i = 0;
while (i < newAsserts.size())
{
- theory::TrustNode trn = newAsserts[i];
+ TrustNode trn = newAsserts[i];
// do not run to fixed point on subcall, since we are processing all
// lemmas in this loop
newAsserts[i] = runLemma(trn, newAsserts, newSkolems, false);
}
// The rewriting of assertion can be justified by the term conversion proof
// generator d_tpg.
- return theory::TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get());
+ return TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get());
}
-theory::TrustNode RemoveTermFormulas::run(TNode assertion)
+TrustNode RemoveTermFormulas::run(TNode assertion)
{
- std::vector<theory::TrustNode> newAsserts;
+ std::vector<TrustNode> newAsserts;
std::vector<Node> newSkolems;
return run(assertion, newAsserts, newSkolems, false);
}
-theory::TrustNode RemoveTermFormulas::runLemma(
- theory::TrustNode lem,
- std::vector<theory::TrustNode>& newAsserts,
- std::vector<Node>& newSkolems,
- bool fixedPoint)
+TrustNode RemoveTermFormulas::runLemma(TrustNode lem,
+ std::vector<TrustNode>& newAsserts,
+ std::vector<Node>& newSkolems,
+ bool fixedPoint)
{
- theory::TrustNode trn =
- run(lem.getProven(), newAsserts, newSkolems, fixedPoint);
+ TrustNode trn = run(lem.getProven(), newAsserts, newSkolems, fixedPoint);
if (trn.isNull())
{
// no change
return lem;
}
- Assert(trn.getKind() == theory::TrustNodeKind::REWRITE);
+ Assert(trn.getKind() == TrustNodeKind::REWRITE);
Node newAssertion = trn.getNode();
if (!isProofEnabled())
{
// proofs not enabled, just take result
- return theory::TrustNode::mkTrustLemma(newAssertion, nullptr);
+ return TrustNode::mkTrustLemma(newAssertion, nullptr);
}
Trace("rtf-proof-debug")
<< "RemoveTermFormulas::run: setup proof for processed new lemma"
// ------------------------------------------------------- EQ_RESOLVE
// newAssertion
d_lp->addStep(newAssertion, PfRule::EQ_RESOLVE, {assertionPre, naEq}, {});
- return theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get());
+ return TrustNode::mkTrustLemma(newAssertion, d_lp.get());
}
Node RemoveTermFormulas::runInternal(TNode assertion,
- std::vector<theory::TrustNode>& output,
+ std::vector<TrustNode>& output,
std::vector<Node>& newSkolems)
{
NodeManager* nm = NodeManager::currentNM();
if (!processedChildren.back())
{
// check if we should replace the current node
- theory::TrustNode newLem;
+ TrustNode newLem;
Node currt = runCurrent(curr, newLem);
// if we replaced by a skolem, we do not recurse
if (!currt.isNull())
}
Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
- theory::TrustNode& newLem)
+ TrustNode& newLem)
{
TNode node = curr.first;
uint32_t cval = curr.second;
Trace("rtf-debug") << "*** term formula removal introduced " << skolem
<< " for " << node << std::endl;
- newLem = theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get());
+ newLem = TrustNode::mkTrustLemma(newAssertion, d_lp.get());
Trace("rtf-proof-debug") << "Checking closed..." << std::endl;
newLem.debugCheckClosed("rtf-proof-debug",
* right hand side is assertion after removing term formulas, and the proof
* generator (if provided) that can prove the equivalence.
*/
- theory::TrustNode run(TNode assertion,
- std::vector<theory::TrustNode>& newAsserts,
- std::vector<Node>& newSkolems,
- bool fixedPoint = false);
+ TrustNode run(TNode assertion,
+ std::vector<TrustNode>& newAsserts,
+ std::vector<Node>& newSkolems,
+ bool fixedPoint = false);
/**
* Same as above, but does not track lemmas, and does not run to fixed point.
* The relevant lemmas can be extracted by the caller later using getSkolems
* and getLemmaForSkolem.
*/
- theory::TrustNode run(TNode assertion);
+ TrustNode run(TNode assertion);
/**
* Same as above, but transforms a lemma, returning a LEMMA trust node that
* proves the same formula as lem with term formulas removed.
*/
- theory::TrustNode runLemma(theory::TrustNode lem,
- std::vector<theory::TrustNode>& newAsserts,
- std::vector<Node>& newSkolems,
- bool fixedPoint = false);
+ TrustNode runLemma(TrustNode lem,
+ std::vector<TrustNode>& newAsserts,
+ std::vector<Node>& newSkolems,
+ bool fixedPoint = false);
/**
* Get proof generator that is responsible for all proofs for removing term
* the version of assertion with all term formulas removed.
*/
Node runInternal(TNode assertion,
- std::vector<theory::TrustNode>& newAsserts,
+ std::vector<TrustNode>& newAsserts,
std::vector<Node>& newSkolems);
/**
* This is called on curr of the form (t, val) where t is a term and val is
* Otherwise, if t should not be replaced in the term context, this method
* returns the null node.
*/
- Node runCurrent(std::pair<Node, uint32_t>& curr, theory::TrustNode& newLem);
+ Node runCurrent(std::pair<Node, uint32_t>& curr, TrustNode& newLem);
/** Whether proofs are enabled */
bool isProofEnabled() const;
namespace cvc5 {
class ProofNodeManager;
+class EagerProofGenerator;
namespace context {
class Context;
}
namespace theory {
-
-class EagerProofGenerator;
struct EeSetupInfo;
namespace eq {
namespace cvc5 {
class ProofNodeManager;
+class EagerProofGenerator;
namespace context {
class Context;
}
namespace theory {
-class EagerProofGenerator;
-
namespace arith {
class Comparison;
#include "util/statistics_stats.h"
namespace cvc5 {
-namespace theory {
class EagerProofGenerator;
+
+namespace theory {
+
class TheoryModel;
namespace arith {
class ProofGenerator;
class ProofNode;
-
-namespace theory {
-
class EagerProofGenerator;
+namespace theory {
namespace booleans {
/**
namespace cvc5 {
namespace theory {
-
-const char* toString(MethodId id)
-{
- switch (id)
- {
- case MethodId::RW_REWRITE: return "RW_REWRITE";
- case MethodId::RW_EXT_REWRITE: return "RW_EXT_REWRITE";
- case MethodId::RW_REWRITE_EQ_EXT: return "RW_REWRITE_EQ_EXT";
- case MethodId::RW_EVALUATE: return "RW_EVALUATE";
- case MethodId::RW_IDENTITY: return "RW_IDENTITY";
- case MethodId::RW_REWRITE_THEORY_PRE: return "RW_REWRITE_THEORY_PRE";
- case MethodId::RW_REWRITE_THEORY_POST: return "RW_REWRITE_THEORY_POST";
- case MethodId::SB_DEFAULT: return "SB_DEFAULT";
- case MethodId::SB_LITERAL: return "SB_LITERAL";
- case MethodId::SB_FORMULA: return "SB_FORMULA";
- case MethodId::SBA_SEQUENTIAL: return "SBA_SEQUENTIAL";
- case MethodId::SBA_SIMUL: return "SBA_SIMUL";
- case MethodId::SBA_FIXPOINT: return "SBA_FIXPOINT";
- default: return "MethodId::Unknown";
- };
-}
-
-std::ostream& operator<<(std::ostream& out, MethodId id)
-{
- out << toString(id);
- return out;
-}
-
-Node mkMethodId(MethodId id)
-{
- return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(id)));
-}
-
namespace builtin {
void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
return ns;
}
-bool BuiltinProofRuleChecker::getMethodId(TNode n, MethodId& i)
-{
- uint32_t index;
- if (!getUInt32(n, index))
- {
- return false;
- }
- i = static_cast<MethodId>(index);
- return true;
-}
-
Node BuiltinProofRuleChecker::checkInternal(PfRule id,
const std::vector<Node>& children,
const std::vector<Node>& args)
return Node::null();
}
-bool BuiltinProofRuleChecker::getMethodIds(const std::vector<Node>& args,
- MethodId& ids,
- MethodId& ida,
- MethodId& idr,
- size_t index)
-{
- ids = MethodId::SB_DEFAULT;
- ida = MethodId::SBA_SEQUENTIAL;
- idr = MethodId::RW_REWRITE;
- for (size_t offset = 0; offset <= 2; offset++)
- {
- if (args.size() > index + offset)
- {
- MethodId& id = offset == 0 ? ids : (offset == 1 ? ida : idr);
- if (!getMethodId(args[index + offset], id))
- {
- Trace("builtin-pfcheck")
- << "Failed to get id from " << args[index + offset] << std::endl;
- return false;
- }
- }
- else
- {
- break;
- }
- }
- Trace("builtin-pfcheck") << "Got MethodIds ids/ida/idr: " << ids << " / "
- << ida << " / " << idr << "\n";
- return true;
-}
-
-void BuiltinProofRuleChecker::addMethodIds(std::vector<Node>& args,
- MethodId ids,
- MethodId ida,
- MethodId idr)
-{
- bool ndefRewriter = (idr != MethodId::RW_REWRITE);
- bool ndefApply = (ida != MethodId::SBA_SEQUENTIAL);
- if (ids != MethodId::SB_DEFAULT || ndefRewriter || ndefApply)
- {
- args.push_back(mkMethodId(ids));
- }
- if (ndefApply || ndefRewriter)
- {
- args.push_back(mkMethodId(ida));
- }
- if (ndefRewriter)
- {
- args.push_back(mkMethodId(idr));
- }
-}
-
bool BuiltinProofRuleChecker::getTheoryId(TNode n, TheoryId& tid)
{
uint32_t i;
* directory for licensing information.
* ****************************************************************************
*
- * Equality proof checker utility.
+ * Builtin proof checker utility.
*/
#include "cvc5_private.h"
#define CVC5__THEORY__BUILTIN__PROOF_CHECKER_H
#include "expr/node.h"
+#include "proof/method_id.h"
#include "proof/proof_checker.h"
#include "proof/proof_node.h"
#include "theory/quantifiers/extended_rewrite.h"
namespace cvc5 {
namespace theory {
-
-/**
- * Identifiers for rewriters and substitutions, which we abstractly
- * classify as "methods". Methods have a unique identifier in the internal
- * proof calculus implemented by the checker below.
- *
- * A "rewriter" is abstractly a method from Node to Node, where the output
- * is semantically equivalent to the input. The identifiers below list
- * various methods that have this contract. This identifier is used
- * in a number of the builtin rules.
- *
- * A substitution is a method for turning a formula into a substitution.
- */
-enum class MethodId : uint32_t
-{
- //---------------------------- Rewriters
- // Rewriter::rewrite(n)
- RW_REWRITE,
- // d_ext_rew.extendedRewrite(n);
- RW_EXT_REWRITE,
- // Rewriter::rewriteExtEquality(n)
- RW_REWRITE_EQ_EXT,
- // Evaluator::evaluate(n)
- RW_EVALUATE,
- // identity
- RW_IDENTITY,
- // theory preRewrite, note this is only intended to be used as an argument
- // to THEORY_REWRITE in the final proof. It is not implemented in
- // applyRewrite below, see documentation in proof_rule.h for THEORY_REWRITE.
- RW_REWRITE_THEORY_PRE,
- // same as above, for theory postRewrite
- RW_REWRITE_THEORY_POST,
- //---------------------------- Substitutions
- // (= x y) is interpreted as x -> y, using Node::substitute
- SB_DEFAULT,
- // P, (not P) are interpreted as P -> true, P -> false using Node::substitute
- SB_LITERAL,
- // P is interpreted as P -> true using Node::substitute
- SB_FORMULA,
- //---------------------------- Substitution applications
- // multiple substitutions are applied sequentially
- SBA_SEQUENTIAL,
- // multiple substitutions are applied simultaneously
- SBA_SIMUL,
- // multiple substitutions are applied to fix point
- SBA_FIXPOINT
- // For example, for x -> u, y -> f(z), z -> g(x), applying this substituion to
- // y gives:
- // - f(g(x)) for SBA_SEQUENTIAL
- // - f(z) for SBA_SIMUL
- // - f(g(u)) for SBA_FIXPOINT
- // Notice that SBA_FIXPOINT should provide a terminating rewrite system
- // as a substitution, or else non-termination will occur during proof
- // checking.
-};
-/** Converts a rewriter id to a string. */
-const char* toString(MethodId id);
-/** Write a rewriter id to out */
-std::ostream& operator<<(std::ostream& out, MethodId id);
-/** Make a method id node */
-Node mkMethodId(MethodId id);
-
namespace builtin {
/** A checker for builtin proofs */
MethodId ids = MethodId::SB_DEFAULT,
MethodId ida = MethodId::SBA_SEQUENTIAL,
MethodId idr = MethodId::RW_REWRITE);
- /** get a method identifier from a node, return false if we fail */
- static bool getMethodId(TNode n, MethodId& i);
- /**
- * Get method identifiers from args starting at the given index. Store their
- * values into ids, ida, and idr. This method returns false if args does not
- * contain valid method identifiers at position index in args.
- */
- bool getMethodIds(const std::vector<Node>& args,
- MethodId& ids,
- MethodId& ida,
- MethodId& idr,
- size_t index);
- /**
- * Add method identifiers ids, ida and idr as nodes to args. This does not add
- * ids, ida or idr if their values are the default ones.
- */
- static void addMethodIds(std::vector<Node>& args,
- MethodId ids,
- MethodId ida,
- MethodId idr);
/** get a TheoryId from a node, return false if we fail */
static bool getTheoryId(TNode n, TheoryId& tid);
class TheoryEngine;
class Env;
+class EagerProofGenerator;
namespace theory {
-class EagerProofGenerator;
class ModelManager;
class SharedSolver;
#include "theory/inference_manager_buffered.h"
namespace cvc5 {
-namespace theory {
class EagerProofGenerator;
+namespace theory {
namespace datatypes {
/**
class TConvProofGenerator;
class ProofNodeManager;
+class TrustNode;
namespace theory {
-class TrustNode;
-
namespace builtin {
class BuiltinProofRuleChecker;
}
}
}
-theory::TrustNode SharedTermsDatabase::explain(TNode literal) const
+TrustNode SharedTermsDatabase::explain(TNode literal) const
{
if (d_pfee != nullptr)
{
/**
* Returns an explanation of the propagation that came from the database.
*/
- theory::TrustNode explain(TNode literal) const;
+ TrustNode explain(TNode literal) const;
/**
* Add an equality to propagate.
return solveStatus;
}
-theory::TrustNode TheoryEngine::ppRewriteEquality(TNode eq)
+TrustNode TheoryEngine::ppRewriteEquality(TNode eq)
{
Assert(eq.getKind() == kind::EQUAL);
std::vector<SkolemLemma> lems;
}
}
-void TheoryEngine::lemma(theory::TrustNode tlemma,
+void TheoryEngine::lemma(TrustNode tlemma,
theory::LemmaProperty p,
theory::TheoryId atomsTo,
theory::TheoryId from)
d_lemmasAdded = true;
}
-void TheoryEngine::conflict(theory::TrustNode tconflict, TheoryId theoryId)
+void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId)
{
Assert(tconflict.getKind() == TrustNodeKind::CONFLICT);
TNode conflict = tconflict.getNode();
d_incompleteId = id;
}
-theory::TrustNode TheoryEngine::getExplanation(
+TrustNode TheoryEngine::getExplanation(
std::vector<NodeTheoryPair>& explanationVector)
{
Assert(explanationVector.size() == 1);
return trn;
}
- return theory::TrustNode::mkTrustPropExp(conclusion, expNode, nullptr);
+ return TrustNode::mkTrustPropExp(conclusion, expNode, nullptr);
}
bool TheoryEngine::isProofEnabled() const { return d_pnm != nullptr; }
* generator (if it exists),
* @param theoryId The theory that sent the conflict
*/
- void conflict(theory::TrustNode conflict, theory::TheoryId theoryId);
+ void conflict(TrustNode conflict, theory::TheoryId theoryId);
/**
* Debugging flag to ensure that shutdown() is called before the
* @param atomsTo the theory that atoms of the lemma should be sent to
* @param from the theory that sent the lemma
*/
- void lemma(theory::TrustNode node,
+ void lemma(TrustNode node,
theory::LemmaProperty p,
theory::TheoryId atomsTo = theory::THEORY_LAST,
theory::TheoryId from = theory::THEORY_LAST);
* where the node is the one to be explained, and the theory is the
* theory that sent the literal.
*/
- theory::TrustNode getExplanation(
- std::vector<NodeTheoryPair>& explanationVector);
+ TrustNode getExplanation(std::vector<NodeTheoryPair>& explanationVector);
/** Are proofs enabled? */
bool isProofEnabled() const;
* Preprocess rewrite equality, called by the preprocessor to rewrite
* equalities appearing in the input.
*/
- theory::TrustNode ppRewriteEquality(TNode eq);
+ TrustNode ppRewriteEquality(TNode eq);
/** Notify (preprocessed) assertions. */
void notifyPreprocessedAssertions(const std::vector<Node>& assertions);
* take this proof into account (when proofs are enabled).
*/
theory::Theory::PPAssertStatus solve(
- theory::TrustNode tliteral,
- theory::TrustSubstitutionMap& substitutionOut);
+ TrustNode tliteral, theory::TrustSubstitutionMap& substitutionOut);
/**
* Preregister a Theory atom with the responsible theory (or
/**
* Returns an explanation of the node propagated to the SAT solver.
*/
- theory::TrustNode getExplanation(TNode node);
+ TrustNode getExplanation(TNode node);
/**
* Get the pointer to the model object used by this theory engine.
d_false = NodeManager::currentNM()->mkConst(false);
}
-theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain(
+TrustNode TheoryEngineProofGenerator::mkTrustExplain(
TNode lit, Node exp, std::shared_ptr<LazyCDProof> lpf)
{
Node p;
- theory::TrustNode trn;
+ TrustNode trn;
if (lit == d_false)
{
// propagation of false is a conflict
- trn = theory::TrustNode::mkTrustConflict(exp, this);
+ trn = TrustNode::mkTrustConflict(exp, this);
p = trn.getProven();
Assert(p.getKind() == NOT);
}
else
{
- trn = theory::TrustNode::mkTrustPropExp(lit, exp, this);
+ trn = TrustNode::mkTrustPropExp(lit, exp, this);
p = trn.getProven();
Assert(p.getKind() == IMPLIES && p.getNumChildren() == 2);
}
* explanation already exists, then the previous explanation is taken, which
* also suffices for proving the implication.
*/
- theory::TrustNode mkTrustExplain(TNode lit,
- Node exp,
- std::shared_ptr<LazyCDProof> lpf);
+ TrustNode mkTrustExplain(TNode lit,
+ Node exp,
+ std::shared_ptr<LazyCDProof> lpf);
/**
* Get proof for, which expects implications corresponding to explained
* propagations (=> exp lit) registered by the above method. This currently
void safePoint(Resource r) override {}
void conflict(TNode n) override { push(CONFLICT, n); }
- void trustedConflict(theory::TrustNode n) override
- {
- push(CONFLICT, n.getNode());
- }
+ void trustedConflict(TrustNode n) override { push(CONFLICT, n.getNode()); }
bool propagate(TNode n) override
{
push(LEMMA, n);
}
- void trustedLemma(theory::TrustNode n, theory::LemmaProperty p) override
+ void trustedLemma(TrustNode n, theory::LemmaProperty p) override
{
push(LEMMA, n.getNode());
}
// do not assert to equality engine, since this theory does not use one
return true;
}
- theory::TrustNode explain(TNode n) override
- {
- return theory::TrustNode::null();
- }
+ TrustNode explain(TNode n) override { return TrustNode::null(); }
Node getValue(TNode n) { return Node::null(); }
std::string identify() const override { return "DummyTheory" + d_id; }
projects / cvc5.git / commitdiff