Prints both literals learned during preprocessing, and during search.
This feature was recently requested by Cetora.
prop/skolem_def_manager.h
prop/theory_proxy.cpp
prop/theory_proxy.h
+ prop/zero_level_learner.cpp
+ prop/zero_level_learner.h
smt/abduction_solver.cpp
smt/abduction_solver.h
smt/abstract_values.cpp
[[option.mode.RAW_BENCHMARK]]
name = "raw-benchmark"
help = "print the benchmark back on the output verbatim as it is processed"
- description = "With ``-o raw_benchmark``, cvc5 prints the benchmark back just as it has been parsed."
+ description = "With ``-o raw-benchmark``, cvc5 prints the benchmark back just as it has been parsed."
example-file = "regress0/datatypes/datatype-dump.cvc.smt2"
+[[option.mode.LEARNED_LITS]]
+ name = "learned-lits"
+ help = "print input literals that hold globally"
+ description = "With ``-o learned-lits``, cvc5 prints input literals that it has learned to hold globally."
+ example-file = "regress0/printer/learned-lit-output.smt2"
# Stores then enabled output tags.
[[option]]
void PropEngine::assertInputFormulas(
const std::vector<Node>& assertions,
- std::unordered_map<size_t, Node>& skolemMap)
+ std::unordered_map<size_t, Node>& skolemMap,
+ const std::vector<Node>& ppl)
{
Assert(!d_inCheckSat) << "Sat solver in solve()!";
- // notify the theory engine of preprocessed assertions
- d_theoryEngine->notifyPreprocessedAssertions(assertions);
- // Now, notify the theory proxy of the assertions and skolem definitions.
- // Notice we do this before asserting the formulas to the CNF stream below,
- // since (preregistration) lemmas may occur during calls to assertInternal.
- // These lemmas we want to be notified about after the theory proxy has
- // been notified about all input assertions.
- std::unordered_map<size_t, Node>::iterator it;
- for (size_t i = 0, asize = assertions.size(); i < asize; i++)
- {
- // is the assertion a skolem definition?
- it = skolemMap.find(i);
- Node skolem;
- if (it != skolemMap.end())
- {
- skolem = it->second;
- }
- d_theoryProxy->notifyAssertion(assertions[i], skolem, false);
- }
+ d_theoryProxy->notifyInputFormulas(assertions, skolemMap, ppl);
for (const Node& node : assertions)
{
Debug("prop") << "assertFormula(" << node << ")" << std::endl;
}
Debug("prop") << "PropEngine::checkSat() => " << result << std::endl;
- if(result == SAT_VALUE_TRUE && d_theoryEngine->isIncomplete()) {
+ if (result == SAT_VALUE_TRUE && d_theoryProxy->isIncomplete())
+ {
return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE);
}
return Result(result == SAT_VALUE_TRUE ? Result::SAT : Result::UNSAT);
return cdp.getProofFor(fnode);
}
+const std::unordered_set<Node>& PropEngine::getLearnedZeroLevelLiterals() const
+{
+ return d_theoryProxy->getLearnedZeroLevelLiterals();
+}
+
} // namespace prop
} // namespace cvc5
namespace cvc5 {
-class Env;
class ResourceManager;
class ProofNodeManager;
class TheoryEngine;
* @param skolemMap a map which says which skolem (if any) each assertion
* corresponds to. For example, if (ite C (= k a) (= k b)) is the i^th
* assertion, then skolemMap may contain the entry { i -> k }.
+ * @param ppl the list of preprocessed learned literals
*/
void assertInputFormulas(const std::vector<Node>& assertions,
- std::unordered_map<size_t, Node>& skolemMap);
+ std::unordered_map<size_t, Node>& skolemMap,
+ const std::vector<Node>& ppl);
/**
* Converts the given formula to CNF and assert the CNF to the SAT solver.
/** Return the prop engine proof for assumption-based unsat cores. */
std::shared_ptr<ProofNode> getRefutation();
+ /** Get the zero-level assertions */
+ const std::unordered_set<Node>& getLearnedZeroLevelLiterals() const;
+
private:
/** Dump out the satisfying assignment (after SAT result) */
void printSatisfyingAssignment();
#include "context/context.h"
#include "decision/decision_engine.h"
+#include "expr/node_algorithm.h"
+#include "options/base_options.h"
#include "options/decision_options.h"
#include "options/smt_options.h"
#include "prop/cnf_stream.h"
#include "prop/prop_engine.h"
#include "prop/skolem_def_manager.h"
+#include "prop/zero_level_learner.h"
#include "smt/env.h"
#include "smt/smt_statistics_registry.h"
#include "theory/rewriter.h"
d_decisionEngine(decisionEngine),
d_dmNeedsActiveDefs(d_decisionEngine->needsActiveSkolemDefs()),
d_theoryEngine(theoryEngine),
- d_queue(env.getContext()),
+ d_queue(context()),
d_tpp(env, *theoryEngine),
- d_skdm(skdm)
+ d_skdm(skdm),
+ d_zll(nullptr)
{
+ bool trackTopLevelLearned = isOutputOn(OutputTag::LEARNED_LITS);
+ if (trackTopLevelLearned)
+ {
+ d_zll = std::make_unique<ZeroLevelLearner>(env, propEngine);
+ }
}
TheoryProxy::~TheoryProxy() {
d_theoryEngine->presolve();
}
+void TheoryProxy::notifyInputFormulas(
+ const std::vector<Node>& assertions,
+ std::unordered_map<size_t, Node>& skolemMap,
+ const std::vector<Node>& ppl)
+{
+ // notify the theory engine of preprocessed assertions
+ d_theoryEngine->notifyPreprocessedAssertions(assertions);
+ // Now, notify the theory proxy of the assertions and skolem definitions.
+ // Notice we do this before asserting the formulas to the CNF stream below,
+ // since (preregistration) lemmas may occur during calls to assertInternal.
+ // These lemmas we want to be notified about after the theory proxy has
+ // been notified about all input assertions.
+ std::unordered_map<size_t, Node>::iterator it;
+ for (size_t i = 0, asize = assertions.size(); i < asize; i++)
+ {
+ // is the assertion a skolem definition?
+ it = skolemMap.find(i);
+ Node skolem;
+ if (it != skolemMap.end())
+ {
+ skolem = it->second;
+ }
+ notifyAssertion(assertions[i], skolem, false);
+ }
+
+ // the zero-level learner needs to be notified of the input assertions, to
+ // determine what is learnable
+ if (d_zll != nullptr)
+ {
+ d_zll->notifyInputFormulas(assertions, skolemMap, ppl);
+ }
+}
+
void TheoryProxy::notifyAssertion(Node a, TNode skolem, bool isLemma)
{
if (skolem.isNull())
while (!d_queue.empty()) {
TNode assertion = d_queue.front();
d_queue.pop();
+ if (d_zll != nullptr)
+ {
+ // check if this corresponds to a zero-level asserted literal
+ d_zll->notifyAsserted(assertion);
+ }
// now, assert to theory engine
d_theoryEngine->assertFact(assertion);
if (d_dmNeedsActiveDefs)
return d_theoryEngine->needCheck();
}
+bool TheoryProxy::isIncomplete() const
+{
+ return d_theoryEngine->isIncomplete();
+}
+
TNode TheoryProxy::getNode(SatLiteral lit) {
return d_cnfStream->getNode(lit);
}
void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); }
+const std::unordered_set<Node>& TheoryProxy::getLearnedZeroLevelLiterals() const
+{
+ Assert(d_zll != nullptr);
+ return d_zll->getLearnedZeroLevelLiterals();
+}
+
} // namespace prop
} // namespace cvc5
#include <unordered_set>
+#include "context/cdhashset.h"
#include "context/cdqueue.h"
#include "expr/node.h"
#include "proof/trust_node.h"
class PropEngine;
class CnfStream;
class SkolemDefManager;
+class ZeroLevelLearner;
/**
* The proxy class that allows the SatSolver to communicate with the theories
*/
class TheoryProxy : protected EnvObj, public Registrar
{
+ using NodeSet = context::CDHashSet<Node>;
+
public:
TheoryProxy(Env& env,
PropEngine* propEngine,
/** Presolve, which calls presolve for the modules managed by this class */
void presolve();
+ /**
+ * Notifies this module of the input assertions.
+ * @param assertion The preprocessed input assertions,
+ * @param skolemMap Map from indices in assertion to the Skolem they are
+ * the definition for
+ * @param ppl The preprocessed learned literals, that is, the literals that
+ * hold at top-level, as computed by the circuit propagator.
+ */
+ void notifyInputFormulas(const std::vector<Node>& assertions,
+ std::unordered_map<size_t, Node>& skolemMap,
+ const std::vector<Node>& ppl);
/**
* Notify a lemma or input assertion, possibly corresponding to a skolem
* definition.
bool theoryNeedCheck() const;
+ /** Is incomplete */
+ bool isIncomplete() const;
+
/**
* Notifies of a new variable at a decision level.
*/
/** Preregister term */
void preRegister(Node n) override;
+ /** Get the zero-level assertions */
+ const std::unordered_set<Node>& getLearnedZeroLevelLiterals() const;
+
private:
/** The prop engine we are using. */
PropEngine* d_propEngine;
/** The skolem definition manager */
SkolemDefManager* d_skdm;
+
+ /** The zero level learner */
+ std::unique_ptr<ZeroLevelLearner> d_zll;
+
}; /* class TheoryProxy */
} // namespace prop
-
} // namespace cvc5
-#endif /* CVC5__PROP__SAT_H */
+#endif
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Learner for literals asserted at level zero.
+ */
+#include "prop/zero_level_learner.h"
+
+#include "context/context.h"
+#include "expr/node_algorithm.h"
+#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/trust_substitutions.h"
+
+namespace cvc5 {
+namespace prop {
+
+ZeroLevelLearner::ZeroLevelLearner(Env& env, PropEngine* propEngine)
+ : EnvObj(env),
+ d_propEngine(propEngine),
+ d_nonZeroAssert(context(), false),
+ d_assertNoLearnCount(0)
+{
+}
+
+ZeroLevelLearner::~ZeroLevelLearner() {}
+
+void ZeroLevelLearner::getAtoms(TNode a,
+ std::unordered_set<TNode>& visited,
+ std::unordered_set<TNode>& ppLits)
+{
+ std::vector<TNode> visit;
+ TNode cur;
+ visit.push_back(a);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ if (visited.find(cur) == visited.end())
+ {
+ visited.insert(cur);
+ if (expr::isBooleanConnective(cur))
+ {
+ visit.insert(visit.end(), cur.begin(), cur.end());
+ continue;
+ }
+ ppLits.insert(cur);
+ }
+ } while (!visit.empty());
+}
+
+void ZeroLevelLearner::notifyInputFormulas(
+ const std::vector<Node>& assertions,
+ std::unordered_map<size_t, Node>& skolemMap,
+ const std::vector<Node>& ppl)
+{
+ d_assertNoLearnCount = 0;
+ d_ppnAtoms.clear();
+ // Copy the preprocessed assertions and skolem map information directly
+ // Also, compute the set of literals in the preprocessed assertions
+ std::unordered_set<TNode> visited;
+ // learned literals and d_ppnAtoms are disjoint
+ for (const Node& lit : ppl)
+ {
+ TNode atom = lit.getKind() == kind::NOT ? lit[0] : lit;
+ visited.insert(atom);
+ d_pplAtoms.insert(atom);
+ }
+ if (isOutputOn(OutputTag::LEARNED_LITS))
+ {
+ // output learned literals from preprocessing
+ for (const Node& lit : ppl)
+ {
+ output(OutputTag::LEARNED_LITS)
+ << "(learned-lit " << lit << " :preprocess)" << std::endl;
+ }
+ }
+ for (const Node& a : assertions)
+ {
+ getAtoms(a, visited, d_ppnAtoms);
+ }
+
+ Trace("level-zero") << "Preprocess status:" << std::endl;
+ Trace("level-zero") << "#Non-learned lits = " << d_ppnAtoms.size()
+ << std::endl;
+ Trace("level-zero") << "#Learned lits = " << ppl.size() << std::endl;
+ Trace("level-zero") << "#Top level subs = "
+ << d_env.getTopLevelSubstitutions().get().size()
+ << std::endl;
+}
+
+void ZeroLevelLearner::notifyAsserted(TNode assertion)
+{
+ // check if at level zero
+ if (d_nonZeroAssert.get())
+ {
+ d_assertNoLearnCount++;
+ }
+ else if (d_levelZeroAsserts.find(assertion) == d_levelZeroAsserts.end())
+ {
+ int32_t alevel = d_propEngine->getDecisionLevel(assertion);
+ if (alevel == 0)
+ {
+ 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)
+ {
+ d_assertNoLearnCount = 0;
+ d_levelZeroAssertsLearned.insert(assertion);
+ Trace("level-zero-assert")
+ << "#learned now " << d_levelZeroAssertsLearned.size() << std::endl;
+ 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(assertion)
+ << ")" << std::endl;
+ }
+ return;
+ }
+ }
+ else
+ {
+ d_nonZeroAssert = true;
+ }
+ d_assertNoLearnCount++;
+ }
+}
+
+const std::unordered_set<Node>& ZeroLevelLearner::getLearnedZeroLevelLiterals()
+ const
+{
+ return d_levelZeroAssertsLearned;
+}
+
+} // namespace prop
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Learner for literals asserted at level zero.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PROP__ZERO_LEVEL_LEARNER_H
+#define CVC5__PROP__ZERO_LEVEL_LEARNER_H
+
+#include <unordered_set>
+
+#include "context/cdhashset.h"
+#include "context/cdo.h"
+#include "expr/node.h"
+#include "smt/env_obj.h"
+
+namespace cvc5 {
+namespace prop {
+
+class PropEngine;
+
+/**
+ * The module for processing literals that are learned at decision level zero.
+ *
+ * This tracks the literals that are asserted at decision level zero. It
+ * computes which literals are "learnable", which currently is limited to those
+ * that are over atoms that appear in the input assertions.
+ *
+ * The module can be queried for the set of learned literals, and also is
+ * responsible for printing the literals it learns.
+ */
+class ZeroLevelLearner : protected EnvObj
+{
+ using NodeSet = context::CDHashSet<Node>;
+
+ public:
+ ZeroLevelLearner(Env& env, PropEngine* propEngine);
+
+ ~ZeroLevelLearner();
+
+ void notifyInputFormulas(const std::vector<Node>& assertions,
+ std::unordered_map<size_t, Node>& skolemMap,
+ const std::vector<Node>& ppl);
+ /**
+ * Notify the given literal was asserted
+ */
+ void notifyAsserted(TNode assertion);
+
+ /** Get the zero-level assertions */
+ const std::unordered_set<Node>& getLearnedZeroLevelLiterals() const;
+
+ private:
+ static void getAtoms(TNode a,
+ std::unordered_set<TNode>& visited,
+ std::unordered_set<TNode>& ppLits);
+
+ /** The prop engine we are using. */
+ PropEngine* d_propEngine;
+
+ /** Set of literals that hold at level 0 */
+ std::unordered_set<TNode> d_levelZeroAsserts;
+
+ /** Set of learnable literals that hold at level 0 */
+ std::unordered_set<Node> d_levelZeroAssertsLearned;
+
+ /** Whether we have seen an assertion level > 0 */
+ context::CDO<bool> d_nonZeroAssert;
+
+ /** Preprocessed literals that are not learned */
+ std::unordered_set<TNode> d_ppnAtoms;
+
+ /** Already learned TEMPORARY */
+ std::unordered_set<TNode> d_pplAtoms;
+
+ /** Current counter of assertions */
+ size_t d_assertNoLearnCount;
+}; /* class ZeroLevelLearner */
+
+} // namespace prop
+} // namespace cvc5
+
+#endif
d_propagator.getLearnedLiterals().clear();
}
+std::vector<Node> Preprocessor::getLearnedLiterals() const
+{
+ if (d_ppContext == nullptr)
+ {
+ return {};
+ }
+ return d_ppContext->getLearnedLiterals();
+}
+
void Preprocessor::cleanup() { d_processor.cleanup(); }
Node Preprocessor::expandDefinitions(const Node& n)
* Clear learned literals from the Boolean propagator.
*/
void clearLearnedLiterals();
+ /** Get learned literals */
+ std::vector<Node> getLearnedLiterals() const;
/**
* Cleanup, which deletes the processing passes owned by this module. This
* is required to be done explicitly so that passes are deleted before the
{
d_env.verbose(2) << "converting to CNF..." << endl;
const std::vector<Node>& assertions = ap.ref();
+ const std::vector<Node>& ppl = d_pp.getLearnedLiterals();
// It is important to distinguish the input assertions from the skolem
// definitions, as the decision justification heuristic treates the latter
// specially.
preprocessing::IteSkolemMap& ism = ap.getIteSkolemMap();
- d_propEngine->assertInputFormulas(assertions, ism);
+ d_propEngine->assertInputFormulas(assertions, ism, ppl);
}
// clear the current assertions
*/
void addSubstitutions(SubstitutionMap& subMap, bool invalidateCache = true);
+ /** Size of the substitutions */
+ size_t size() const { return d_substitutions.size(); }
/**
* Returns true iff x is in the substitution map
*/
regress0/printer/bv_consts_dec.smt2
regress0/printer/empty_sort.smt2
regress0/printer/empty_symbol_name.smt2
+ regress0/printer/learned-lit-output.smt2
regress0/printer/let_shadowing.smt2
regress0/printer/symbol_starting_w_digit.smt2
regress0/printer/tuples_and_records.cvc.smt2
--- /dev/null
+; COMMAND-LINE: -o learned-lits
+; SCRUBBER: sed -e 's/(learned-lit.*/learned-lit/'
+; EXPECT: learned-lit
+; EXPECT: learned-lit
+; EXPECT: learned-lit
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(assert (> x 10))
+(assert (or (< x 5) (> y 0)))
+(check-sat)
projects / cvc5.git / commitdiff