This adds the "revised" partitioning algorithm to the splitter and adds support for collecting literals from the sat solver. There is only one partitioning strategy in this PR, but the others will be added in subsequent PRs.
theory/smt_engine_subsolver.h
theory/sort_inference.cpp
theory/sort_inference.h
+ theory/partition_generator.cpp
+ theory/partition_generator.h
theory/strings/array_solver.cpp
theory/strings/array_solver.h
theory/strings/array_core_solver.cpp
options/expr_options.toml
options/fp_options.toml
options/main_options.toml
+ options/parallel_options.toml
options/parser_options.toml
options/printer_options.toml
options/proof_options.toml
--- /dev/null
+id = "PARALLEL"
+name = "Parallel"
+
+[[option]]
+ name = "computePartitions"
+ category = "expert"
+ long = "compute-partitions=N"
+ type = "uint64_t"
+ default = "0"
+ help = "make n partitions. n <2 disables computing partitions entirely"
+
+[[option]]
+ name = "checksBeforePartitioning"
+ category = "expert"
+ long = "checks-before-partition=N"
+ type = "uint64_t"
+ default = "1"
+ help = "number of standard or full effort checks until partitioning"
+
+[[option]]
+ name = "partitionConflictSize"
+ category = "expert"
+ long = "partition-conflict-size=N"
+ type = "uint64_t"
+ default = "0"
+ help = "number of literals in a cube; if no partition size is set, then the partition conflict size is chosen to be log2(number of requested partitions)"
+
+[[option]]
+ name = "partitionStrategy"
+ alias = ["partition"]
+ category = "expert"
+ long = "partition-strategy=MODE"
+ type = "PartitionMode"
+ default = "REVISED"
+ help = "choose partition strategy mode"
+ help_mode = "Partition strategy modes."
+[[option.mode.REVISED]]
+ name = "revised"
+ help = "For 4 partitions, creates cubes C1, C2, C3, !C1 & !C2 & !C3"
+
+[[option]]
+ name = "partitionCheck"
+ alias = ["check"]
+ category = "expert"
+ long = "partition-check=MODE"
+ type = "CheckMode"
+ default = "STANDARD"
+ help = "select whether partitioning happens at full or standard check"
+ help_mode = "Partition check modes."
+[[option.mode.STANDARD]]
+ name = "standard"
+ help = "create partitions at standard checks"
+[[option.mode.FULL]]
+ name = "full"
+ help = "create partitions at full checks"
+
+[[option]]
+ name = "partitionsOut"
+ alias = ["partitions-out"]
+ category = "expert"
+ long = "write-partitions-to=output"
+ type = "ManagedOut"
+ default = "ManagedOut()"
+ includes = ["<iostream>", "options/managed_streams.h"]
+ help = "set the output channel for writing partitions"
bool b); // Declare if a variable should be eligible for
// selection in the decision heuristic.
+ const vec<Lit>& getMiniSatDecisions() { return trail; }
+
// Read state:
//
lbool value(Var x) const; // The current value of a variable.
return d_minisat->isDecision( decn );
}
+std::vector<SatLiteral> MinisatSatSolver::getDecisions() const
+{
+ std::vector<SatLiteral> decisions;
+ const Minisat::vec<Minisat::Lit>& miniDecisions =
+ d_minisat->getMiniSatDecisions();
+ for (size_t i = 0, ndec = miniDecisions.size(); i < ndec; ++i)
+ {
+ decisions.push_back(toSatLiteral(miniDecisions[i]));
+ }
+ return decisions;
+}
+
int32_t MinisatSatSolver::getDecisionLevel(SatVariable v) const
{
return d_minisat->level(v) + d_minisat->user_level(v);
bool isDecision(SatVariable decn) const override;
+ /** Return the list of current list of decisions that have been made by the
+ * solver at the point when this function is called.
+ */
+ std::vector<SatLiteral> getDecisions() const override;
+
/** Return decision level at which `lit` was decided on. */
int32_t getDecisionLevel(SatVariable v) const override;
return d_satSolver->isDecision(d_cnfStream->getLiteral(lit).getSatVariable());
}
+std::vector<Node> PropEngine::getPropDecisions() const
+{
+ std::vector<Node> decisions;
+ std::vector<SatLiteral> miniDecisions = d_satSolver->getDecisions();
+ for (SatLiteral d : miniDecisions)
+ {
+ decisions.push_back(d_cnfStream->getNode(d));
+ }
+ return decisions;
+}
+
int32_t PropEngine::getDecisionLevel(Node lit) const
{
Assert(isSatLiteral(lit));
*/
bool isDecision(Node lit) const;
+ /**
+ * Get the current list of decisions made by the SAT solver at the moment in
+ * time that getPropDecisions() is called.
+ *
+ * @return List of decisions made by the SAT solver.
+ */
+ std::vector<Node> getPropDecisions() const;
+
/**
* Return SAT context level at which `lit` was decided on.
*
virtual bool isDecision(SatVariable decn) const = 0;
+ /**
+ * Return the current list of decisions made by the SAT solver.
+ */
+ virtual std::vector<SatLiteral> getDecisions() const = 0;
+
/**
* Return the current decision level of `lit`.
*/
#include "options/language.h"
#include "options/main_options.h"
#include "options/option_exception.h"
+#include "options/parallel_options.h"
#include "options/printer_options.h"
#include "options/proof_options.h"
#include "options/prop_options.h"
reason << "solveIntAsBV";
return true;
}
+ if (opts.parallel.computePartitions > 1)
+ {
+ reason << "compute partitions";
+ return true;
+ }
// disable modes not supported by incremental
notifyModifyOption("sortInference", "false", "incremental solving");
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Amalee Wilson, Andrew Wu
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * PartitionGenerator for creating partitions.
+ */
+
+#include "theory/partition_generator.h"
+
+#include <math.h>
+
+#include "expr/node_algorithm.h"
+#include "expr/node_builder.h"
+#include "options/parallel_options.h"
+#include "prop/prop_engine.h"
+#include "prop/theory_proxy.h"
+#include "prop/zero_level_learner.h"
+#include "theory/theory_engine.h"
+#include "theory/theory_id.h"
+#include "theory/theory_traits.h"
+
+using namespace std;
+
+namespace cvc5::internal {
+
+namespace theory {
+PartitionGenerator::PartitionGenerator(Env& env,
+ TheoryEngine* theoryEngine,
+ prop::PropEngine* propEngine)
+ : EnvObj(env),
+ d_numPartitions(options().parallel.computePartitions),
+ d_numChecks(0),
+ d_numPartitionsSoFar(0)
+{
+ d_valuation = std::make_unique<Valuation>(theoryEngine);
+ d_propEngine = propEngine;
+
+ d_conflictSize = options().parallel.partitionConflictSize;
+ if (!d_conflictSize)
+ {
+ d_conflictSize = static_cast<uint64_t>(log2(d_numPartitions));
+ }
+}
+
+std::vector<TNode> PartitionGenerator::collectDecisionLiterals()
+{
+ std::vector<TNode> literals;
+ std::vector<Node> decisionNodes = d_propEngine->getPropDecisions();
+ // 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)
+ {
+ 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())
+ {
+ continue;
+ }
+
+ literals.push_back(originalN);
+ }
+ return literals;
+}
+
+void PartitionGenerator::emitCube(Node toEmit)
+{
+ *options().parallel.partitionsOut << toEmit << std::endl;
+ ++d_numPartitionsSoFar;
+}
+
+TrustNode PartitionGenerator::blockPath(TNode toBlock)
+{
+ // Now block the path in the search.
+ Node lemma = toBlock.notNode();
+ d_assertedLemmas.push_back(lemma);
+ TrustNode trustedLemma = TrustNode::mkTrustLemma(lemma);
+ return trustedLemma;
+}
+
+// Send lemma that is the negation of all previously asserted lemmas.
+TrustNode PartitionGenerator::stopPartitioning() const
+{
+ return TrustNode::mkTrustLemma(NodeManager::currentNM()->mkConst(false));
+}
+
+// This is the revised version of the old splitting strategy.
+// Cubes look like the following:
+// C1 = l1_{1} & .... & l1_{d_conflictSize}
+// C2 = l2_{1} & .... & l2_{d_conflictSize}
+// C3 = l3_{1} & .... & l3_{d_conflictSize}
+// C4 = !C1 & !C2 & !C3
+TrustNode PartitionGenerator::makeRevisedPartitions()
+{
+ // If we're not at the last cube
+ if (d_numPartitionsSoFar < d_numPartitions - 1)
+ {
+ std::vector<TNode> literals = collectDecisionLiterals();
+
+ // Make sure we have enough literals.
+ // Conflict size can be set through options, but the default is log base 2
+ // of the requested number of partitions.
+ if (literals.size() < d_conflictSize)
+ {
+ return TrustNode::null();
+ }
+
+ literals.resize(d_conflictSize);
+ // Make first cube and emit it.
+ Node conj = NodeManager::currentNM()->mkAnd(literals);
+ emitCube(conj);
+ // Add to the list of cubes.
+ d_cubes.push_back(conj);
+ return blockPath(conj);
+ }
+ // At the last cube
+ else
+ {
+ vector<Node> nots;
+ for (auto c : d_cubes) nots.push_back(c.notNode());
+ Node lemma = NodeManager::currentNM()->mkAnd(nots);
+ // Emit not(cube_one) and not(cube_two) and ... and not(cube_n-1)
+ emitCube(lemma);
+ return stopPartitioning();
+ }
+}
+
+TrustNode PartitionGenerator::check(Theory::Effort e)
+{
+ if ((options().parallel.partitionCheck == options::CheckMode::FULL
+ && !Theory::fullEffort(e))
+ || (options().parallel.partitionCheck == options::CheckMode::STANDARD
+ && Theory::fullEffort(e))
+ || (options().parallel.computePartitions < 2))
+ {
+ return TrustNode::null();
+ }
+
+ d_numChecks = d_numChecks + 1;
+
+ if (d_numChecks < options().parallel.checksBeforePartitioning)
+ {
+ return TrustNode::null();
+ }
+
+ switch (options().parallel.partitionStrategy)
+ {
+ case options::PartitionMode::REVISED: return makeRevisedPartitions();
+ default: return TrustNode::null();
+ }
+}
+
+} // namespace theory
+} // namespace cvc5::internal
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Amalee Wilson, Andrew Wu
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * PartitionGenerator for creating partitions.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__SPLITTER_H
+#define CVC5__THEORY__SPLITTER_H
+
+#include <vector>
+
+#include "proof/trust_node.h"
+#include "smt/env_obj.h"
+#include "theory/theory.h"
+#include "theory/valuation.h"
+
+namespace cvc5::internal {
+
+class TheoryEngine;
+
+namespace prop {
+class PropEngine;
+}
+
+namespace theory {
+
+class PartitionGenerator : protected EnvObj
+{
+ public:
+ PartitionGenerator(Env& env,
+ TheoryEngine* theoryEngine,
+ prop::PropEngine* propEngine);
+
+ /**
+ * Make partitions for parallel solving. e communicates the effort at which
+ * check was called. Returns a lemma blocking off the emitted cube from the
+ * search.
+ */
+ TrustNode check(Theory::Effort e);
+
+ private:
+ /**
+ * Print the cube to the specified output.
+ */
+ void emitCube(Node toEmit);
+
+ /**
+ * Partition using the "revised" strategy, which emits cubes such as C1, C2,
+ * C3, !C1 & !C2 & !C3
+ */
+ TrustNode makeRevisedPartitions();
+
+ /**
+ * Generate a lemma that is the negation of toBlock which ultimately blocks
+ * that path in the search.
+ */
+ TrustNode blockPath(TNode toBlock);
+
+ /**
+ * Stop partitioning and return unsat.
+ */
+ TrustNode stopPartitioning() const;
+
+ /**
+ * Get the list of decisions from the SAT solver
+ */
+ std::vector<TNode> collectDecisionLiterals();
+
+/**
+ * Returns the d_cubes, the cubes that have been created for partitioning the
+ * original problem.
+ */
+std::vector<Node> getPartitions() const { return d_cubes; }
+
+/**
+ * Current propEngine.
+ */
+prop::PropEngine* d_propEngine;
+
+/**
+ * Valuation of the theory engine.
+ */
+std::unique_ptr<Valuation> d_valuation;
+
+/**
+ * The number of partitions requested through the compute-partitions option.
+ */
+const uint64_t d_numPartitions;
+
+/**
+ * Number of standard or full (depending on partition check mode) checks that
+ * have occured.
+ */
+uint64_t d_numChecks;
+
+/**
+ * The number of partitions that have been created.
+ */
+uint64_t d_numPartitionsSoFar;
+
+/**
+ * Lemmas that have been sent to the SAT solver.
+ */
+std::vector<Node> d_assertedLemmas;
+
+/**
+ * List of the cubes that have been created.
+ */
+std::vector<Node> d_cubes;
+
+/**
+ * Minimum number of literals required in the list of decisions for cubes to
+ * be made.
+ */
+uint64_t d_conflictSize;
+};
+} // namespace theory
+} // namespace cvc5::internal
+
+#endif /* CVC5__PARTITION__GENERATOR_H */
#include "expr/attribute.h"
#include "expr/node_builder.h"
#include "expr/node_visitor.h"
+#include "options/parallel_options.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "options/theory_options.h"
#include "smt/logic_exception.h"
#include "theory/combination_care_graph.h"
#include "theory/decision_manager.h"
+#include "theory/partition_generator.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers_engine.h"
#include "theory/relevance_manager.h"
// finish initializing the theory
t->finishInit();
}
+
+ if (options().parallel.computePartitions > 1)
+ {
+ d_partitionGen =
+ std::make_unique<PartitionGenerator>(d_env, this, getPropEngine());
+ }
Trace("theory") << "End TheoryEngine::finishInit" << std::endl;
}
d_tc->resetRound();
}
+ if (d_partitionGen != nullptr)
+ {
+ TrustNode tl = d_partitionGen->check(effort);
+ if (!tl.isNull())
+ {
+ lemma(tl, LemmaProperty::NONE, THEORY_LAST);
+ }
+ }
+
// Check until done
while (d_factsAsserted && !d_inConflict && !d_lemmasAdded) {
#include "theory/atom_requests.h"
#include "theory/engine_output_channel.h"
#include "theory/interrupted.h"
+#include "theory/partition_generator.h"
#include "theory/rewriter.h"
#include "theory/sort_inference.h"
#include "theory/theory.h"
*/
context::CDO<bool> d_factsAsserted;
+ /**
+ * The splitter produces partitions when the compute-partitions option is
+ * used.
+ */
+ std::unique_ptr<theory::PartitionGenerator> d_partitionGen;
+
}; /* class TheoryEngine */
} // namespace cvc5::internal
projects / cvc5.git / commitdiff