Now tracks learned literals for all types. Unifies the output of `-o learned-literals`.
Followup PRs will add the deep restart feature, which configures which kind of learned literals can be used when restarting.
#include "preprocessing/preprocessing_pass_context.h"
#include "expr/node_algorithm.h"
-#include "expr/skolem_manager.h"
#include "options/base_options.h"
+#include "prop/prop_engine.h"
#include "smt/env.h"
#include "theory/theory_engine.h"
#include "theory/theory_model.h"
return d_llm.getLearnedLiterals();
}
-void PreprocessingPassContext::printSubstitution(const Node& lhs,
- const Node& rhs) const
-{
- Node eq = SkolemManager::getOriginalForm(lhs.eqNode(rhs));
- output(OutputTag::LEARNED_LITS)
- << "(learned-lit " << eq << " :preprocess-subs)" << std::endl;
- output(OutputTag::SUBS) << "(substitution " << eq << ")" << std::endl;
-}
-
void PreprocessingPassContext::addSubstitution(const Node& lhs,
const Node& rhs,
ProofGenerator* pg)
{
- if (isOutputOn(OutputTag::LEARNED_LITS) || isOutputOn(OutputTag::SUBS))
- {
- printSubstitution(lhs, rhs);
- }
+ d_propEngine->notifyTopLevelSubstitution(lhs, rhs);
d_env.getTopLevelSubstitutions().addSubstitution(lhs, rhs, pg);
}
PfRule id,
const std::vector<Node>& args)
{
- if (isOutputOn(OutputTag::LEARNED_LITS) || isOutputOn(OutputTag::SUBS))
- {
- printSubstitution(lhs, rhs);
- }
+ d_propEngine->notifyTopLevelSubstitution(lhs, rhs);
d_env.getTopLevelSubstitutions().addSubstitution(lhs, rhs, id, {}, args);
}
void PreprocessingPassContext::addSubstitutions(
theory::TrustSubstitutionMap& tm)
{
- if (isOutputOn(OutputTag::LEARNED_LITS) || isOutputOn(OutputTag::SUBS))
+ std::unordered_map<Node, Node> subs = tm.get().getSubstitutions();
+ for (const std::pair<const Node, Node>& s : subs)
{
- std::unordered_map<Node, Node> subs = tm.get().getSubstitutions();
- for (const std::pair<const Node, Node>& s : subs)
- {
- printSubstitution(s.first, s.second);
- }
+ d_propEngine->notifyTopLevelSubstitution(s.first, s.second);
}
d_env.getTopLevelSubstitutions().addSubstitutions(tm);
}
#include "base/check.h"
#include "base/output.h"
#include "decision/justification_strategy.h"
+#include "expr/skolem_manager.h"
#include "options/base_options.h"
#include "options/decision_options.h"
#include "options/main_options.h"
return d_theoryProxy->removeItes(node, newLemmas);
}
+void PropEngine::notifyTopLevelSubstitution(const Node& lhs,
+ const Node& rhs) const
+{
+ d_theoryProxy->notifyTopLevelSubstitution(lhs, rhs);
+ if (isOutputOn(OutputTag::SUBS))
+ {
+ Node eq = SkolemManager::getOriginalForm(lhs.eqNode(rhs));
+ output(OutputTag::SUBS) << "(substitution " << eq << ")" << std::endl;
+ }
+}
+
void PropEngine::assertInputFormulas(
const std::vector<Node>& assertions,
std::unordered_map<size_t, Node>& skolemMap)
return cdp.getProofFor(fnode);
}
-std::vector<Node> PropEngine::getLearnedZeroLevelLiterals() const
+std::vector<Node> PropEngine::getLearnedZeroLevelLiterals(
+ modes::LearnedLitType ltype) const
{
- return d_theoryProxy->getLearnedZeroLevelLiterals();
+ return d_theoryProxy->getLearnedZeroLevelLiterals(ltype);
}
} // namespace prop
#ifndef CVC5__PROP_ENGINE_H
#define CVC5__PROP_ENGINE_H
+#include "api/cpp/cvc5_types.h"
#include "context/cdlist.h"
#include "expr/node.h"
#include "proof/proof.h"
*/
TrustNode removeItes(TNode node, std::vector<theory::SkolemLemma>& ppLemmas);
+ /**
+ * Notify that lhs was substituted by rhs during preprocessing. This impacts
+ * the tracked learned literals and output traces.
+ * @param lhs The left-hand side of the substitution
+ * @param rhs The right-hand side of the substitution
+ */
+ void notifyTopLevelSubstitution(const Node& lhs, const Node& rhs) const;
/**
* Converts the given formulas to CNF and assert the CNF to the SAT solver.
* These formulas are asserted permanently for the current context.
/** Return the prop engine proof for assumption-based unsat cores. */
std::shared_ptr<ProofNode> getRefutation();
- /** Get the zero-level assertions */
- std::vector<Node> getLearnedZeroLevelLiterals() const;
+ /** Get the zero-level assertions of the given type */
+ std::vector<Node> getLearnedZeroLevelLiterals(
+ modes::LearnedLitType ltype) const;
private:
/** Dump out the satisfying assignment (after SAT result) */
d_skdm(skdm),
d_zll(nullptr)
{
- bool trackTopLevelLearned = isOutputOn(OutputTag::LEARNED_LITS)
- || options().smt.produceLearnedLiterals;
- if (trackTopLevelLearned)
+ bool trackZeroLevel = isOutputOn(OutputTag::LEARNED_LITS)
+ || options().smt.produceLearnedLiterals;
+ if (trackZeroLevel)
{
- d_zll = std::make_unique<ZeroLevelLearner>(env, propEngine);
+ d_zll = std::make_unique<ZeroLevelLearner>(env, theoryEngine);
}
}
d_theoryEngine->presolve();
}
+void TheoryProxy::notifyTopLevelSubstitution(const Node& lhs,
+ const Node& rhs) const
+{
+ if (d_zll != nullptr)
+ {
+ d_zll->notifyTopLevelSubstitution(lhs, rhs);
+ }
+}
+
void TheoryProxy::notifyInputFormulas(
const std::vector<Node>& assertions,
std::unordered_map<size_t, Node>& skolemMap)
// determine what is learnable
if (d_zll != nullptr)
{
- d_zll->notifyInputFormulas(assertions, skolemMap);
+ d_zll->notifyInputFormulas(assertions);
}
}
d_queue.pop();
if (d_zll != nullptr)
{
- // check if this corresponds to a zero-level asserted literal
- d_zll->notifyAsserted(assertion);
+ int32_t alevel = d_propEngine->getDecisionLevel(assertion);
+ d_zll->notifyAsserted(assertion, alevel);
}
// now, assert to theory engine
d_theoryEngine->assertFact(assertion);
void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); }
-std::vector<Node> TheoryProxy::getLearnedZeroLevelLiterals() const
+std::vector<Node> TheoryProxy::getLearnedZeroLevelLiterals(
+ modes::LearnedLitType ltype) const
{
if (d_zll != nullptr)
{
- return d_zll->getLearnedZeroLevelLiterals();
+ return d_zll->getLearnedZeroLevelLiterals(ltype);
}
return {};
}
#include "context/cdqueue.h"
#include "expr/node.h"
#include "proof/trust_node.h"
+#include "prop/learned_db.h"
#include "prop/registrar.h"
#include "prop/sat_solver_types.h"
#include "smt/env_obj.h"
/** Presolve, which calls presolve for the modules managed by this class */
void presolve();
+ /**
+ * Notify that lhs was substituted by rhs during preprocessing. This impacts
+ * the tracked learned literals and output traces.
+ * @param lhs The left-hand side of the substitution
+ * @param rhs The right-hand side of the substitution
+ */
+ void notifyTopLevelSubstitution(const Node& lhs, const Node& rhs) const;
/**
* Notifies this module of the input assertions.
* @param assertion The preprocessed input assertions,
void preRegister(Node n) override;
/** Get the zero-level assertions */
- std::vector<Node> getLearnedZeroLevelLiterals() const;
+ std::vector<Node> getLearnedZeroLevelLiterals(
+ modes::LearnedLitType ltype) const;
private:
/** The prop engine we are using. */
#include "expr/skolem_manager.h"
#include "options/base_options.h"
#include "options/smt_options.h"
-#include "prop/prop_engine.h"
#include "smt/env.h"
#include "smt/smt_statistics_registry.h"
+#include "theory/theory_engine.h"
#include "theory/trust_substitutions.h"
namespace cvc5::internal {
namespace prop {
-ZeroLevelLearner::ZeroLevelLearner(Env& env, PropEngine* propEngine)
+ZeroLevelLearner::ZeroLevelLearner(Env& env, TheoryEngine* theoryEngine)
: EnvObj(env),
- d_propEngine(propEngine),
+ d_theoryEngine(theoryEngine),
d_levelZeroAsserts(userContext()),
- d_levelZeroAssertsLearned(userContext()),
+ d_ldb(userContext()),
d_nonZeroAssert(context(), false),
d_ppnAtoms(userContext()),
- d_pplAtoms(userContext()),
+ d_ppnTerms(userContext()),
+ d_ppnSyms(userContext()),
d_assertNoLearnCount(0)
{
+ // get the learned types
+ d_learnedTypes.insert(modes::LearnedLitType::INPUT);
}
ZeroLevelLearner::~ZeroLevelLearner() {}
void ZeroLevelLearner::getAtoms(TNode a,
std::unordered_set<TNode>& visited,
- NodeSet& ppLits)
+ std::unordered_set<Node>& atoms)
{
std::vector<TNode> visit;
TNode cur;
visit.insert(visit.end(), cur.begin(), cur.end());
continue;
}
- ppLits.insert(cur);
+ atoms.insert(cur);
}
} while (!visit.empty());
}
-void ZeroLevelLearner::notifyInputFormulas(
- const std::vector<Node>& assertions,
- const std::unordered_map<size_t, Node>& skolemMap)
+void ZeroLevelLearner::notifyTopLevelSubstitution(const Node& lhs,
+ const Node& rhs)
+{
+ // process as a preprocess solved learned literal.
+ Node eq = lhs.eqNode(rhs);
+ processLearnedLiteral(eq, modes::LearnedLitType::PREPROCESS_SOLVED);
+}
+
+void ZeroLevelLearner::notifyInputFormulas(const std::vector<Node>& assertions)
{
- d_assertNoLearnCount = 0;
std::unordered_set<TNode> visited;
+ std::unordered_set<TNode> visitedWithinAtom;
+ std::unordered_set<Node> inputSymbols;
// We consider top level literals of assertions, including those occurring
// as children of AND to be the preprocessed learned literals only, and not
// the literals tracked by the preprocessor
{
continue;
}
+ // we mark that we visited this
visited.insert(atom);
- d_pplAtoms.insert(atom);
- }
- if (isOutputOn(OutputTag::LEARNED_LITS))
- {
// output learned literals from preprocessing
- for (const Node& lit : d_pplAtoms)
- {
- output(OutputTag::LEARNED_LITS)
- << "(learned-lit " << SkolemManager::getOriginalForm(lit)
- << " :preprocess)" << std::endl;
- }
+ processLearnedLiteral(lit, modes::LearnedLitType::PREPROCESS);
+ // also get its symbols
+ expr::getSymbols(atom, inputSymbols, visitedWithinAtom);
+ // remember we've seen it
+ d_levelZeroAsserts.insert(lit);
}
// Compute the set of literals in the preprocessed assertions
+ std::unordered_set<Node> inputAtoms;
for (const Node& a : assertions)
{
- getAtoms(a, visited, d_ppnAtoms);
+ getAtoms(a, visited, inputAtoms);
+ }
+ for (const Node& a : inputAtoms)
+ {
+ d_ppnAtoms.insert(a);
+ // also get its symbols
+ expr::getSymbols(a, inputSymbols, visitedWithinAtom);
+ }
+ for (const TNode& t : visitedWithinAtom)
+ {
+ d_ppnTerms.insert(t);
+ }
+ for (const Node& s : inputSymbols)
+ {
+ d_ppnSyms.insert(s);
}
Trace("level-zero") << "Preprocess status:" << std::endl;
Trace("level-zero") << "#Non-learned lits = " << d_ppnAtoms.size()
<< std::endl;
- Trace("level-zero") << "#Learned lits = " << d_pplAtoms.size() << std::endl;
- Trace("level-zero") << "#Top level subs = "
+ Trace("level-zero") << "#Symbols = " << d_ppnSyms.size() << std::endl;
+ Trace("level-zero") << "#Subterms = " << d_ppnTerms.size() << std::endl;
+ Trace("level-zero") << "#Current top level subs = "
<< d_env.getTopLevelSubstitutions().get().size()
<< std::endl;
+ Trace("level-zero") << d_ldb.toStringDebug();
}
-void ZeroLevelLearner::notifyAsserted(TNode assertion)
+bool ZeroLevelLearner::notifyAsserted(TNode assertion, int32_t alevel)
{
// check if at level zero
if (d_nonZeroAssert.get())
{
+ // already not at level zero, skip
+ d_assertNoLearnCount++;
+ }
+ else if (alevel != 0)
+ {
+ Trace("level-zero-dec") << "First non-zero: " << assertion << std::endl;
+ d_nonZeroAssert = true;
d_assertNoLearnCount++;
}
else if (d_levelZeroAsserts.find(assertion) == d_levelZeroAsserts.end())
{
- int32_t alevel = d_propEngine->getDecisionLevel(assertion);
- if (alevel == 0)
+ // remember we've processed this
+ d_levelZeroAsserts.insert(assertion);
+ // process what we should do with the learned literal
+ modes::LearnedLitType ltype = computeLearnedLiteralType(assertion);
+ processLearnedLiteral(assertion, ltype);
+ return true;
+ }
+ return true;
+}
+
+modes::LearnedLitType ZeroLevelLearner::computeLearnedLiteralType(
+ const Node& lit)
+{
+ // literal was learned, determine its type
+ TNode aatom = lit.getKind() == kind::NOT ? lit[0] : lit;
+ bool internal = d_ppnAtoms.find(aatom) == d_ppnAtoms.end();
+ modes::LearnedLitType ltype =
+ internal ? modes::LearnedLitType::INTERNAL : modes::LearnedLitType::INPUT;
+ // compute if solvable
+ if (internal)
+ {
+ Subs ss;
+ if (getSolved(lit, ss))
{
- TNode aatom = assertion.getKind() == kind::NOT ? assertion[0] : assertion;
- bool learnable = d_ppnAtoms.find(aatom) != d_ppnAtoms.end();
- Trace("level-zero-assert")
- << "Level zero assert: " << assertion << ", learnable=" << learnable
- << ", already learned="
- << (d_pplAtoms.find(aatom) != d_pplAtoms.end()) << std::endl;
- d_levelZeroAsserts.insert(assertion);
- if (learnable)
+ // if we solved for any variable from input, we are SOLVABLE.
+ for (const Node& v : ss.d_vars)
{
- d_assertNoLearnCount = 0;
- d_levelZeroAssertsLearned.insert(assertion);
- Trace("level-zero-assert")
- << "#learned now " << d_levelZeroAssertsLearned.size() << std::endl;
- if (isOutputOn(OutputTag::LEARNED_LITS))
+ if (d_ppnSyms.find(v) == d_ppnSyms.end())
{
- // get the original form so that internally generated variables
- // are mapped back to their original form
- output(OutputTag::LEARNED_LITS)
- << "(learned-lit " << SkolemManager::getOriginalForm(assertion)
- << ")" << std::endl;
+ Trace("level-zero-assert") << "...solvable due to " << v << std::endl;
+ ltype = modes::LearnedLitType::SOLVABLE;
+ break;
}
- return;
}
}
- else
+ if (ltype != modes::LearnedLitType::SOLVABLE)
{
- d_nonZeroAssert = true;
+ // maybe a constant prop?
+ if (lit.getKind() == kind::EQUAL)
+ {
+ for (size_t i = 0; i < 2; i++)
+ {
+ if (lit[i].isConst()
+ && d_ppnTerms.find(lit[1 - i]) != d_ppnTerms.end())
+ {
+ ltype = modes::LearnedLitType::CONSTANT_PROP;
+ break;
+ }
+ }
+ }
}
- d_assertNoLearnCount++;
+ }
+ Trace("level-zero-assert")
+ << "Level zero assert: " << lit << ", type=" << ltype << std::endl;
+ return ltype;
+}
+
+void ZeroLevelLearner::processLearnedLiteral(const Node& lit,
+ modes::LearnedLitType ltype)
+{
+ // add to the database
+ d_ldb.addLearnedLiteral(lit, ltype);
+ // reset the counter for deep restart if the literal was learnable
+ if (isLearnable(ltype))
+ {
+ d_assertNoLearnCount = 0;
+ }
+ // print to stream
+ if (isOutputOn(OutputTag::LEARNED_LITS))
+ {
+ // get the original form so that internally generated variables
+ // are mapped back to their original form
+ output(OutputTag::LEARNED_LITS)
+ << "(learned-lit " << SkolemManager::getOriginalForm(lit);
+ if (ltype != modes::LearnedLitType::INPUT)
+ {
+ std::stringstream tss;
+ tss << ltype;
+ std::string ltstr = tss.str();
+ std::transform(
+ ltstr.begin(), ltstr.end(), ltstr.begin(), [](unsigned char c) {
+ return std::tolower(c);
+ });
+ output(OutputTag::LEARNED_LITS) << " :" << ltstr;
+ }
+ output(OutputTag::LEARNED_LITS) << ")" << std::endl;
}
}
-std::vector<Node> ZeroLevelLearner::getLearnedZeroLevelLiterals() const
+std::vector<Node> ZeroLevelLearner::getLearnedZeroLevelLiterals(
+ modes::LearnedLitType ltype) const
{
- std::vector<Node> ret;
- for (const Node& n : d_levelZeroAssertsLearned)
+ std::vector<Node> ret = d_ldb.getLearnedLiterals(ltype);
+ if (TraceIsOn("level-zero"))
{
- ret.push_back(n);
+ if (!ret.empty())
+ {
+ Trace("level-zero") << "...learned #literals (" << ltype
+ << ") = " << ret.size() << std::endl;
+ }
}
return ret;
}
+bool ZeroLevelLearner::isLearnable(modes::LearnedLitType ltype) const
+{
+ return d_learnedTypes.find(ltype) != d_learnedTypes.end();
+}
+
+bool ZeroLevelLearner::getSolved(const Node& lit, Subs& subs)
+{
+ context::Context dummyContext;
+ theory::TrustSubstitutionMap subsOut(&dummyContext);
+ TrustNode tlit = TrustNode::mkTrustLemma(lit);
+ theory::Theory::PPAssertStatus status = d_theoryEngine->solve(tlit, subsOut);
+ if (status == theory::Theory::PP_ASSERT_STATUS_SOLVED)
+ {
+ Trace("level-zero-debug") << lit << " is solvable" << std::endl;
+ // extract the substitution
+ std::unordered_map<Node, Node> ss = subsOut.get().getSubstitutions();
+ for (const std::pair<const Node, Node>& s : ss)
+ {
+ subs.add(s.first, s.second);
+ Trace("level-zero-debug")
+ << " subs: " << s.first << " -> " << s.second << std::endl;
+ }
+ return true;
+ }
+ Trace("level-zero-debug") << lit << " is not solvable" << std::endl;
+ return false;
+}
+
} // namespace prop
} // namespace cvc5::internal
#include "context/cdhashset.h"
#include "context/cdo.h"
#include "expr/node.h"
+#include "expr/subs.h"
+#include "prop/learned_db.h"
#include "smt/env_obj.h"
namespace cvc5::internal {
-namespace prop {
-class PropEngine;
+class TheoryEngine;
+
+namespace prop {
/**
* The module for processing literals that are learned at decision level zero.
using NodeSet = context::CDHashSet<Node>;
public:
- ZeroLevelLearner(Env& env, PropEngine* propEngine);
+ ZeroLevelLearner(Env& env, TheoryEngine* theoryEngine);
~ZeroLevelLearner();
- void notifyInputFormulas(const std::vector<Node>& assertions,
- const std::unordered_map<size_t, Node>& skolemMap);
+ void notifyTopLevelSubstitution(const Node& lhs, const Node& rhs);
+ /** Notify the input formulas and the skolem map */
+ void notifyInputFormulas(const std::vector<Node>& assertions);
/**
- * Notify the given literal was asserted
+ * Notify the given literal was asserted at the given assertion level.
+ * Return false if a deep restart is requested.
*/
- void notifyAsserted(TNode assertion);
+ bool notifyAsserted(TNode assertion, int32_t alevel);
/** Get the zero-level assertions */
- std::vector<Node> getLearnedZeroLevelLiterals() const;
+ std::vector<Node> getLearnedZeroLevelLiterals(
+ modes::LearnedLitType ltype) const;
private:
static void getAtoms(TNode a,
std::unordered_set<TNode>& visited,
- NodeSet& ppLits);
-
- /** The prop engine we are using. */
- PropEngine* d_propEngine;
+ 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 */
+ bool getSolved(const Node& lit, Subs& subs);
+
+ /** The theory engine we are using */
+ TheoryEngine* d_theoryEngine;
/** Set of literals that hold at level 0 */
NodeSet d_levelZeroAsserts;
- /** Set of learnable literals that hold at level 0 */
- NodeSet d_levelZeroAssertsLearned;
+ /** What we have learned */
+ LearnedDb d_ldb;
/** Whether we have seen an assertion level > 0 */
context::CDO<bool> d_nonZeroAssert;
- /** Preprocessed literals that are not learned */
+ /**
+ * Atoms of literals from the input formula that were not learned at
+ * preprocess.
+ */
NodeSet d_ppnAtoms;
-
- /** Already learned TEMPORARY */
- NodeSet d_pplAtoms;
-
+ /** Subterms of the above atoms. */
+ NodeSet d_ppnTerms;
+ /** Symbols in the above atoms. */
+ NodeSet d_ppnSyms;
/** Current counter of assertions */
size_t d_assertNoLearnCount;
+ /** learnable learned literal types (for deep restart), based on option */
+ std::unordered_set<modes::LearnedLitType> d_learnedTypes;
}; /* class ZeroLevelLearner */
} // namespace prop
// although other modes could use the preprocessor
PropEngine* pe = getPropEngine();
Assert(pe != nullptr);
- return pe->getLearnedZeroLevelLiterals();
+ return pe->getLearnedZeroLevelLiterals(modes::LearnedLitType::INPUT);
}
void SolverEngine::checkProof()
projects / cvc5.git / commitdiff