*/
CONSTANT_PROP,
/** Any internal literal that does not fall into the above categories. */
- INTERNAL
+ INTERNAL,
+ /** Special case for when produce-learned-literals is not set. */
+ UNKNOWN
};
/** Writes a learned literal type to a stream. */
std::ostream& operator<<(std::ostream& out, LearnedLitType ltype);
default = "1"
help = "number of standard or full effort checks until partitioning"
+[[option]]
+ name = "checksBetweenPartitions"
+ category = "expert"
+ long = "checks-between-partitions=N"
+ type = "uint64_t"
+ default = "1"
+ help = "number of checks between partitions"
+
[[option]]
name = "partitionConflictSize"
category = "expert"
[[option.mode.DECISION_TRAIL]]
name = "decision-trail"
help = "Creates mutually exclusive cubes from the decisions in the SAT solver."
+[[option.mode.HEAP_TRAIL]]
+ name = "heap-trail"
+ help = "Creates mutually exclusive cubes from the order heap in the SAT solver."
[[option]]
name = "partitionCheck"
default = "ManagedOut()"
includes = ["<iostream>", "options/managed_streams.h"]
help = "set the output channel for writing partitions"
+
+[[option]]
+ name = "appendLearnedLiteralsToCubes"
+ category = "expert"
+ long = "append-learned-literals-to-cubes"
+ type = "bool"
+ default = "false"
+ help = "emit learned literals with the cubes"
+
&& options().base.incrementalSolving;
}
+const std::vector<Node> Solver::getMiniSatOrderHeap()
+{
+ std::vector<Node> heapList;
+ for (size_t i = 0, hsize = order_heap.size(); i < hsize; ++i)
+ {
+ Node n = d_proxy->getNode(order_heap[i]);
+ heapList.push_back(n);
+ }
+ return heapList;
+}
+
} // namespace Minisat
} // namespace cvc5::internal
bool b); // Declare if a variable should be eligible for
// selection in the decision heuristic.
+ // Return the decision trail
const vec<Lit>& getMiniSatDecisions() { return trail; }
+ // Return the order_heap, which is a priority queue of variables ordered with
+ // respect to the variable activity. The order heap is made available here
+ // in order to make partitions based on the literals contained in the heap.
+
+ const std::vector<Node> getMiniSatOrderHeap();
+
// Read state:
//
lbool value(Var x) const; // The current value of a variable.
return decisions;
}
+std::vector<Node> MinisatSatSolver::getOrderHeap() const
+{
+ return d_minisat->getMiniSatOrderHeap();
+}
+
int32_t MinisatSatSolver::getDecisionLevel(SatVariable v) const
{
return d_minisat->level(v) + d_minisat->user_level(v);
*/
std::vector<SatLiteral> getDecisions() const override;
+ /** Return the order heap.
+ */
+ std::vector<Node> getOrderHeap() const override;
+
/** Return decision level at which `lit` was decided on. */
int32_t getDecisionLevel(SatVariable v) const override;
return decisions;
}
+std::vector<Node> PropEngine::getPropOrderHeap() const
+{
+ return d_satSolver->getOrderHeap();
+}
+
int32_t PropEngine::getDecisionLevel(Node lit) const
{
Assert(isSatLiteral(lit));
return d_theoryProxy->getLearnedZeroLevelLiteralsForRestart();
}
+modes::LearnedLitType PropEngine::getLiteralType(const Node& lit) const
+{
+ return d_theoryProxy->getLiteralType(lit);
+}
+
} // namespace prop
} // namespace cvc5::internal
*/
std::vector<Node> getPropDecisions() const;
+ /**
+ * Get the order heap from the SAT solver.
+ * order_heap is a priority queue of variables ordered with
+ * respect to the variable activity. The order heap is made available here
+ * in order to make partitions based on the literals contained in the heap.
+ *
+ * @return List of Nodes from the SAT variables order heap.
+ */
+ std::vector<Node> getPropOrderHeap() const;
+
/**
* Return SAT context level at which `lit` was decided on.
*
/** Get the zero-level assertions that should be used on deep restart */
std::vector<Node> getLearnedZeroLevelLiteralsForRestart() const;
+ /** Get the literal type through the ZLL utilities */
+ modes::LearnedLitType getLiteralType(const Node& lit) const;
+
private:
/** Dump out the satisfying assignment (after SAT result) */
void printSatisfyingAssignment();
*/
virtual std::vector<SatLiteral> getDecisions() const = 0;
+ /**
+ * Return the order heap of the SAT solver, which is a priority queueue
+ * of literals ordered with respect to variable activity.
+ */
+ virtual std::vector<Node> getOrderHeap() const = 0;
+
/**
* Return the current decision level of `lit`.
*/
#include "expr/node_algorithm.h"
#include "options/base_options.h"
#include "options/decision_options.h"
+#include "options/parallel_options.h"
#include "options/smt_options.h"
#include "prop/cnf_stream.h"
#include "prop/prop_engine.h"
bool trackZeroLevel =
options().smt.deepRestartMode != options::DeepRestartMode::NONE
|| isOutputOn(OutputTag::LEARNED_LITS)
- || options().smt.produceLearnedLiterals;
+ || options().smt.produceLearnedLiterals
+ || options().parallel.computePartitions > 0;
if (trackZeroLevel)
{
d_zll = std::make_unique<ZeroLevelLearner>(env, theoryEngine);
return {};
}
+modes::LearnedLitType TheoryProxy::getLiteralType(const Node& lit) const
+{
+ if (d_zll != nullptr)
+ {
+ return d_zll->computeLearnedLiteralType(lit);
+ }
+ return modes::LearnedLitType::UNKNOWN;
+}
+
std::vector<Node> TheoryProxy::getLearnedZeroLevelLiteralsForRestart() const
{
if (d_zll != nullptr)
modes::LearnedLitType ltype) const;
/** Get the zero-level assertions that should be used on deep restart */
std::vector<Node> getLearnedZeroLevelLiteralsForRestart() const;
+ /** Get literal type using ZLL utility */
+ modes::LearnedLitType getLiteralType(const Node& lit) const;
private:
/** The prop engine we are using. */
modes::LearnedLitType ltype) const;
/** Get the zero-level assertions that should be used on deep restart */
std::vector<Node> getLearnedZeroLevelLiteralsForRestart() const;
+ /** compute type for learned literal */
+ modes::LearnedLitType computeLearnedLiteralType(const Node& lit);
private:
static void getAtoms(TNode a,
std::unordered_set<Node>& atoms);
/** Process learned literal */
void processLearnedLiteral(const Node& lit, modes::LearnedLitType ltype);
- /** compute type for learned literal */
- modes::LearnedLitType computeLearnedLiteralType(const Node& lit);
/** is learnable based on the value of options */
bool isLearnable(modes::LearnedLitType ltype) const;
/** get solved */
: EnvObj(env),
d_numPartitions(options().parallel.computePartitions),
d_numChecks(0),
+ d_betweenChecks(0),
d_numPartitionsSoFar(0)
{
d_valuation = std::make_unique<Valuation>(theoryEngine);
}
}
-std::vector<TNode> PartitionGenerator::collectDecisionLiterals()
+std::vector<Node> PartitionGenerator::collectLiterals(LiteralListType litType)
{
- std::vector<TNode> literals;
- std::vector<Node> decisionNodes = d_propEngine->getPropDecisions();
+ std::vector<Node> filteredLiterals;
+ std::vector<Node> unfilteredLiterals;
+
+ // Filter out the types of literals we don't want.
// Make sure the literal does not have a boolean term or skolem in it.
const std::unordered_set<Kind, kind::KindHashFunction> kinds = {
kind::SKOLEM, kind::BOOLEAN_TERM_VARIABLE};
- for (const Node& n : decisionNodes)
+ switch (litType)
{
- Node originalN = SkolemManager::getOriginalForm(n);
-
- // If the literal is the not of some node, do the checks for the child
- // of the not instead of the not itself.
- Node original = originalN.getKind() == kind::NOT ? originalN[0] : originalN;
- if (expr::hasSubtermKinds(kinds, original)
- || !d_valuation->isSatLiteral(original)
- || !d_valuation->isDecision(original)
- || Theory::theoryOf(original) == THEORY_BOOL
- || n.isConst())
+ case DECISION:
{
- continue;
+ unfilteredLiterals = d_propEngine->getPropDecisions();
+ break;
}
+ case HEAP:
+ {
+ unfilteredLiterals = d_propEngine->getPropOrderHeap();
+ break;
+ }
+ case ZLL:
+ {
+ unfilteredLiterals = d_propEngine->getLearnedZeroLevelLiterals(
+ modes::LearnedLitType::INPUT);
+ break;
+ }
+ default: return filteredLiterals;
+ }
- literals.push_back(originalN);
+ if (litType == HEAP || litType == DECISION)
+ {
+ for (const Node& n : unfilteredLiterals)
+ {
+ Node originalN = SkolemManager::getOriginalForm(n);
+ modes::LearnedLitType nType = d_propEngine->getLiteralType(n);
+
+ // If the literal is the not of some node, do the checks for the child
+ // of the not instead of the not itself.
+ Node original = originalN.getKind() == kind::NOT ? originalN[0] : originalN;
+
+ if (expr::hasSubtermKinds(kinds, original)
+ || !d_valuation->isSatLiteral(original)
+ || Theory::theoryOf(original) == THEORY_BOOL
+ || n.isConst()
+ || nType != modes::LearnedLitType::INPUT
+ || !d_valuation->isDecision(original))
+ {
+ continue;
+ }
+ filteredLiterals.push_back(originalN);
+ }
}
- return literals;
+ // else it must be zll
+ else
+ {
+ for (const Node& n : unfilteredLiterals)
+ {
+ Node originalN = SkolemManager::getOriginalForm(n);
+
+ // If the literal is the not of some node, do the checks for the child
+ // of the not instead of the not itself.
+ Node original = originalN.getKind() == kind::NOT ? originalN[0] : originalN;
+
+ if (expr::hasSubtermKinds(kinds, original)
+ || !d_valuation->isSatLiteral(original)
+ || Theory::theoryOf(original) == THEORY_BOOL
+ || n.isConst())
+ {
+ continue;
+ }
+ filteredLiterals.push_back(originalN);
+ }
+ }
+
+ return filteredLiterals;
}
void PartitionGenerator::emitCube(Node toEmit)
// C2 = l2_{1} & .... & l2_{d_conflictSize}
// C3 = l3_{1} & .... & l3_{d_conflictSize}
// C4 = !C1 & !C2 & !C3
-TrustNode PartitionGenerator::makeRevisedPartitions(bool strict)
+TrustNode PartitionGenerator::makeRevisedPartitions(bool strict, bool emitZLL)
{
// If we're not at the last cube
if (d_numPartitionsSoFar < d_numPartitions - 1)
{
- std::vector<TNode> literals = collectDecisionLiterals();
+ std::vector<Node> literals = collectLiterals(DECISION);
// Make sure we have enough literals.
// Conflict size can be set through options, but the default is log base 2
toEmit.push_back(c.notNode());
}
toEmit.push_back(conj);
- Node cube = NodeManager::currentNM()->mkAnd(toEmit);
+ Node strict_cube = NodeManager::currentNM()->mkAnd(toEmit);
+ d_strict_cubes.push_back(strict_cube);
- emitCube(cube);
+ if (emitZLL)
+ {
+ // just increment and don't actually output the cube yet
+ d_numPartitionsSoFar++;
+ }
+ else
+ {
+ emitCube(strict_cube);
+ }
}
- else
- {
- emitCube(conj);
+ else {
+ if (emitZLL)
+ {
+ // just increment and don't actually output the cube yet
+ d_numPartitionsSoFar++;
+ }
+ else
+ {
+ emitCube(conj);
+ }
}
// Add to the list of cubes.
d_cubes.push_back(conj);
// At the last cube
else
{
+ if (emitZLL)
+ {
+ std::vector<Node> zllLiterals = d_propEngine->getLearnedZeroLevelLiterals(
+ modes::LearnedLitType::INPUT);
+ std::vector<Node>* cubes = strict ? &d_strict_cubes : &d_cubes;
+
+ for (const auto& c : *cubes)
+ {
+ zllLiterals.push_back(c);
+ Node lemma = NodeManager::currentNM()->mkAnd(zllLiterals);
+ emitCube(lemma);
+ zllLiterals.pop_back();
+ }
+ }
+
vector<Node> nots;
for (const Node& c : d_cubes)
{
}
Node lemma = NodeManager::currentNM()->mkAnd(nots);
// Emit not(cube_one) and not(cube_two) and ... and not(cube_n-1)
- emitCube(lemma);
+ if (emitZLL)
+ {
+ std::vector<Node> zllLiterals = d_propEngine->getLearnedZeroLevelLiterals(
+ modes::LearnedLitType::INPUT);
+ zllLiterals.push_back(lemma);
+ Node zllLemma = NodeManager::currentNM()->mkAnd(zllLiterals);
+ emitCube(zllLemma);
+ }
+ else {
+ emitCube(lemma);
+ }
return stopPartitioning();
}
}
-
-TrustNode PartitionGenerator::makeFullTrailPartitions()
+TrustNode PartitionGenerator::makeFullTrailPartitions(LiteralListType litType, bool emitZLL)
{
- std::vector<TNode> literals = collectDecisionLiterals();
+ std::vector<Node> literals = collectLiterals(litType);
uint64_t numVar = static_cast<uint64_t>(log2(d_numPartitions));
if (literals.size() >= numVar)
{
size_t total = pow(2, numVar);
// resultNodeLists is built column by column.
- std::vector<std::vector<TNode> > resultNodeLists(total);
+ std::vector<std::vector<Node> > resultNodeLists(total);
// t is used to determine whether to push the node or its not_node.
bool t = false;
numConsecutiveTF = numConsecutiveTF / 2;
}
- for (const std::vector<TNode>& row : resultNodeLists)
+ for (const std::vector<Node>& row : resultNodeLists)
{
Node conj = NodeManager::currentNM()->mkAnd(row);
- emitCube(conj);
+ if (emitZLL)
+ {
+ std::vector<Node> zllLiterals = collectLiterals(ZLL);
+ zllLiterals.push_back(conj);
+ Node zllConj = NodeManager::currentNM()->mkAnd(zllLiterals);
+ emitCube(zllConj);
+ }
+ else {
+ emitCube(conj);
+ }
}
return stopPartitioning();
}
}
d_numChecks = d_numChecks + 1;
+ d_betweenChecks = d_betweenChecks + 1;
- if (d_numChecks < options().parallel.checksBeforePartitioning)
+ if (d_numChecks < options().parallel.checksBeforePartitioning ||
+ d_betweenChecks < options().parallel.checksBetweenPartitions)
{
return TrustNode::null();
}
+ // Reset betweenChecks
+ d_betweenChecks = 0;
+
+ bool emitZLL = options().parallel.appendLearnedLiteralsToCubes;
switch (options().parallel.partitionStrategy)
{
- case options::PartitionMode::DECISION_TRAIL: return makeFullTrailPartitions();
- case options::PartitionMode::STRICT_CUBE: return makeRevisedPartitions(true);
- case options::PartitionMode::REVISED: return makeRevisedPartitions(false);
+ case options::PartitionMode::HEAP_TRAIL:
+ return makeFullTrailPartitions(/*litType=*/HEAP, emitZLL);
+ case options::PartitionMode::DECISION_TRAIL:
+ return makeFullTrailPartitions(/*litType=*/DECISION, emitZLL);
+ case options::PartitionMode::STRICT_CUBE:
+ return makeRevisedPartitions(/*strict=*/true, emitZLL);
+ case options::PartitionMode::REVISED:
+ return makeRevisedPartitions(/*strict=*/false, emitZLL);
default: return TrustNode::null();
}
}
TrustNode check(Theory::Effort e);
private:
+ /* LiteralListType is used to specify where to pull literals from when calling
+ * collectLiterals. HEAP for the order_heap in the SAT solver, DECISION for
+ * the decision trail in the SAT solver, and ZLL for the zero-level learned
+ * literals.
+ */
+ enum LiteralListType
+ {
+ HEAP,
+ DECISION,
+ ZLL
+ };
/**
- * Print the cube to the specified output.
+ * Increment d_numPartitionsSoFar and print the cube to
+ * the output file specified by --write-partitions-to.
*/
void emitCube(Node toEmit);
/**
* Partition using the "revised" strategy, which emits cubes such as C1, C2,
- * C3, !C1 & !C2 & !C3. If strict is set to true, a modified version of this emits
- * "strict cubes:" C1, !C1 & C2, !C1 & !C2 & C3, !C1 & !C2 & !C3.
+ * C3, !C1 & !C2 & !C3. If strict is set to true, a modified version of this
+ * emits "strict cubes:" C1, !C1 & C2, !C1 & !C2 & C3, !C1 & !C2 & !C3. If
+ * emitZLL is set to true, then zero-level learned literals will be appended
+ * to the cubes.
*/
- TrustNode makeRevisedPartitions(bool strict);
+ TrustNode makeRevisedPartitions(bool strict, bool emitZLL);
/**
- * Partition by taking a list of literals and emitting mutually exclusive cubes
- * that resemble entries in a truth table:
+ * Partition by taking a list of literals and emitting mutually exclusive
+ * cubes that resemble entries in a truth table:
* C1: { l1, !l2}
- * C2: { l1, l2}
- * C3: {!l1, !l2}
- * C4: {!l1, l2}
+ * C2: { l1, l2}
+ * C3: {!l1, !l2}
+ * C4: {!l1, l2}
+ * If emitZLL is set to true, then zero-level learned literals will be
+ * appended to the cubes.
*/
- TrustNode makeFullTrailPartitions();
-
+ TrustNode makeFullTrailPartitions(LiteralListType litType, bool emitZLL);
/**
* Generate a lemma that is the negation of toBlock which ultimately blocks
TrustNode stopPartitioning() const;
/**
- * Get the list of decisions from the SAT solver
+ * Get a list of literals.
+ * litType specifies whether to pull from the decision trail in the sat solver,
+ * from the order heap in the sat solver, or from the zero level learned literals.
*/
- std::vector<TNode> collectDecisionLiterals();
+ std::vector<Node> collectLiterals(LiteralListType litType);
/**
* Returns the d_cubes, the cubes that have been created for partitioning the
* original problem.
*/
+
std::vector<Node> getPartitions() const { return d_cubes; }
/**
*/
uint64_t d_numChecks;
+/**
+ * Number of standard checks that have occured since the last partition that was emitted.
+ */
+uint64_t d_betweenChecks;
+
/**
* The number of partitions that have been created.
*/
*/
std::vector<Node> d_cubes;
+/**
+ * List of the strict cubes that have been created.
+ */
+std::vector<Node> d_strict_cubes;
+
/**
* Minimum number of literals required in the list of decisions for cubes to
* be made.
projects / cvc5.git / commitdiff