/*! \file circuit_propagator.h
** \verbatim
** Top contributors (to current version):
- ** Aina Niemetz, Morgan Deters, Dejan Jovanovic
+ ** Morgan Deters, Aina Niemetz, Gereon Kremer
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
#define CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
#include <functional>
+#include <memory>
#include <unordered_map>
#include <vector>
#include "context/cdhashset.h"
#include "context/cdo.h"
#include "context/context.h"
+#include "expr/lazy_proof_chain.h"
#include "expr/node.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node.h"
+#include "theory/eager_proof_generator.h"
#include "theory/theory.h"
+#include "theory/trust_node.h"
#include "util/hash.h"
namespace CVC4 {
/**
* Construct a new CircuitPropagator.
*/
- CircuitPropagator(bool enableForward = true, bool enableBackward = true)
- : d_context(),
- d_propagationQueue(),
- d_propagationQueueClearer(&d_context, d_propagationQueue),
- d_conflict(&d_context, false),
- d_learnedLiterals(),
- d_learnedLiteralClearer(&d_context, d_learnedLiterals),
- d_backEdges(),
- d_backEdgesClearer(&d_context, d_backEdges),
- d_seen(&d_context),
- d_state(&d_context),
- d_forwardPropagation(enableForward),
- d_backwardPropagation(enableBackward),
- d_needsFinish(false)
- {
- }
+ CircuitPropagator(bool enableForward = true, bool enableBackward = true);
/** Get Node assignment in circuit. Assert-fails if Node is unassigned. */
bool getAssignment(TNode n) const
bool getNeedsFinish() { return d_needsFinish; }
- std::vector<Node>& getLearnedLiterals() { return d_learnedLiterals; }
+ std::vector<TrustNode>& getLearnedLiterals() { return d_learnedLiterals; }
- void finish() { d_context.pop(); }
+ /** Finish the computation and pop the internal context */
+ void finish();
/** Assert for propagation */
void assertTrue(TNode assertion);
* discovered by the propagator are put in the substitutions vector used in
* construction.
*
- * @return true iff conflict found
+ * @return a trust node encapsulating the proof for a conflict as a lemma that
+ * proves false, or the null trust node otherwise
*/
- bool propagate() CVC4_WARN_UNUSED_RESULT;
+ TrustNode propagate() CVC4_WARN_UNUSED_RESULT;
/**
* Get the back edges of this circuit.
if (!value && ((*i).second == ASSIGNED_TO_FALSE)) return true;
return false;
}
+ /**
+ * Set proof node manager, context and parent proof generator.
+ *
+ * If parent is non-null, then it is responsible for the proofs provided
+ * to this class.
+ */
+ void setProof(ProofNodeManager* pnm,
+ context::Context* ctx,
+ ProofGenerator* defParent);
private:
/** A context-notify object that clears out stale data. */
* Assign Node in circuit with the value and add it to the queue; note
* conflicts.
*/
- void assignAndEnqueue(TNode n, bool value)
- {
- Trace("circuit-prop") << "CircuitPropagator::assign(" << n << ", "
- << (value ? "true" : "false") << ")" << std::endl;
-
- if (n.getKind() == kind::CONST_BOOLEAN)
- {
- // Assigning a constant to the opposite value is dumb
- if (value != n.getConst<bool>())
- {
- d_conflict = true;
- return;
- }
- }
-
- // Get the current assignment
- AssignmentStatus state = d_state[n];
+ void assignAndEnqueue(TNode n,
+ bool value,
+ std::shared_ptr<ProofNode> proof = nullptr);
- if (state != UNASSIGNED)
- {
- // If the node is already assigned we might have a conflict
- if (value != (state == ASSIGNED_TO_TRUE))
- {
- d_conflict = true;
- }
- }
- else
- {
- // If unassigned, mark it as assigned
- d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE;
- // Add for further propagation
- d_propagationQueue.push_back(n);
- }
- }
+ /**
+ * Store a conflict for the case that we have derived both n and n.negate()
+ * to be true.
+ */
+ void makeConflict(Node n);
/**
* Compute the map from nodes to the nodes that use it.
*/
void propagateBackward(TNode parent, bool assignment);
+ /** Are proofs enabled? */
+ bool isProofEnabled() const;
+
context::Context d_context;
/** The propagation queue */
* but this keeps us safe in case there's still some rubbish around
* on the queue.
*/
- DataClearer<std::vector<TNode> > d_propagationQueueClearer;
+ DataClearer<std::vector<TNode>> d_propagationQueueClearer;
/** Are we in conflict? */
- context::CDO<bool> d_conflict;
+ context::CDO<TrustNode> d_conflict;
/** Map of substitutions */
- std::vector<Node> d_learnedLiterals;
+ std::vector<TrustNode> d_learnedLiterals;
/**
* Similar data clearer for learned literals.
*/
- DataClearer<std::vector<Node>> d_learnedLiteralClearer;
+ DataClearer<std::vector<TrustNode>> d_learnedLiteralClearer;
/**
* Back edges from nodes to where they are used.
/* Does the current state require a call to finish()? */
bool d_needsFinish;
+ /** Adds a new proof for f, or drops it if we already have a proof */
+ void addProof(TNode f, std::shared_ptr<ProofNode> pf);
+
+ /** A pointer to the proof manager */
+ ProofNodeManager* d_pnm;
+ /** Eager proof generator that actually stores the proofs */
+ std::unique_ptr<EagerProofGenerator> d_epg;
+ /** Connects the proofs to subproofs internally */
+ std::unique_ptr<LazyCDProofChain> d_proofInternal;
+ /** Connects the proofs to assumptions externally */
+ std::unique_ptr<LazyCDProofChain> d_proofExternal;
}; /* class CircuitPropagator */
} // namespace booleans
projects / cvc5.git / blobdiff