From: Amalee Wilson Date: Thu, 14 Apr 2022 15:26:49 +0000 (-0700) Subject: Revised partitioning (#8143) X-Git-Tag: cvc5-1.0.1~261 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=74a46ddc8efe114b4823865d08c370ca518f1cbd;p=cvc5.git Revised partitioning (#8143) 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. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index eec6ba2b1..8cf8d516e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1044,6 +1044,8 @@ libcvc5_add_sources( 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 @@ -1209,6 +1211,7 @@ set(options_toml_files 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 diff --git a/src/options/parallel_options.toml b/src/options/parallel_options.toml new file mode 100644 index 000000000..9d5c288b9 --- /dev/null +++ b/src/options/parallel_options.toml @@ -0,0 +1,65 @@ +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 = ["", "options/managed_streams.h"] + help = "set the output channel for writing partitions" diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 5704133f4..39369a78a 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -288,6 +288,8 @@ public: bool b); // Declare if a variable should be eligible for // selection in the decision heuristic. + const vec& getMiniSatDecisions() { return trail; } + // Read state: // lbool value(Var x) const; // The current value of a variable. diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index f82bd59f3..2d0680cc3 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -266,6 +266,18 @@ bool MinisatSatSolver::isDecision(SatVariable decn) const { return d_minisat->isDecision( decn ); } +std::vector MinisatSatSolver::getDecisions() const +{ + std::vector decisions; + const Minisat::vec& 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); diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index ac5abf8fe..cf37582f4 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -94,6 +94,11 @@ class MinisatSatSolver : public CDCLTSatSolverInterface, protected EnvObj 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 getDecisions() const override; + /** Return decision level at which `lit` was decided on. */ int32_t getDecisionLevel(SatVariable v) const override; diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index c843387f5..53f6877fe 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -317,6 +317,17 @@ bool PropEngine::isDecision(Node lit) const { return d_satSolver->isDecision(d_cnfStream->getLiteral(lit).getSatVariable()); } +std::vector PropEngine::getPropDecisions() const +{ + std::vector decisions; + std::vector 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)); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 6a144f20a..f69da4387 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -141,6 +141,14 @@ class PropEngine : protected EnvObj */ 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 getPropDecisions() const; + /** * Return SAT context level at which `lit` was decided on. * diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 61606ad98..e9f509a80 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -143,6 +143,11 @@ class CDCLTSatSolverInterface : public SatSolver virtual bool isDecision(SatVariable decn) const = 0; + /** + * Return the current list of decisions made by the SAT solver. + */ + virtual std::vector getDecisions() const = 0; + /** * Return the current decision level of `lit`. */ diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 4e71b2311..fb402863d 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -28,6 +28,7 @@ #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" @@ -1041,6 +1042,11 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, 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"); diff --git a/src/theory/partition_generator.cpp b/src/theory/partition_generator.cpp new file mode 100644 index 000000000..8b5ee94e1 --- /dev/null +++ b/src/theory/partition_generator.cpp @@ -0,0 +1,170 @@ +/****************************************************************************** + * 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 + +#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(theoryEngine); + d_propEngine = propEngine; + + d_conflictSize = options().parallel.partitionConflictSize; + if (!d_conflictSize) + { + d_conflictSize = static_cast(log2(d_numPartitions)); + } +} + +std::vector PartitionGenerator::collectDecisionLiterals() +{ + std::vector literals; + std::vector decisionNodes = d_propEngine->getPropDecisions(); + // Make sure the literal does not have a boolean term or skolem in it. + const std::unordered_set 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 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 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 diff --git a/src/theory/partition_generator.h b/src/theory/partition_generator.h new file mode 100644 index 000000000..dfe8533bc --- /dev/null +++ b/src/theory/partition_generator.h @@ -0,0 +1,131 @@ +/****************************************************************************** + * 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 + +#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 collectDecisionLiterals(); + +/** + * Returns the d_cubes, the cubes that have been created for partitioning the + * original problem. + */ +std::vector getPartitions() const { return d_cubes; } + +/** + * Current propEngine. + */ +prop::PropEngine* d_propEngine; + +/** + * Valuation of the theory engine. + */ +std::unique_ptr 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 d_assertedLemmas; + +/** + * List of the cubes that have been created. + */ +std::vector 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 */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 0e88ebaa7..f250b053e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -22,6 +22,7 @@ #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" @@ -34,6 +35,7 @@ #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" @@ -200,6 +202,12 @@ void TheoryEngine::finishInit() // finish initializing the theory t->finishInit(); } + + if (options().parallel.computePartitions > 1) + { + d_partitionGen = + std::make_unique(d_env, this, getPropEngine()); + } Trace("theory") << "End TheoryEngine::finishInit" << std::endl; } @@ -396,6 +404,15 @@ void TheoryEngine::check(Theory::Effort effort) { 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) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index f31008ea5..a177a7bc0 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -30,6 +30,7 @@ #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" @@ -642,6 +643,12 @@ class TheoryEngine : protected EnvObj */ context::CDO d_factsAsserted; + /** + * The splitter produces partitions when the compute-partitions option is + * used. + */ + std::unique_ptr d_partitionGen; + }; /* class TheoryEngine */ } // namespace cvc5::internal