This PR activates the use of the relevance manager in TheoryEngine and makes use of it (via Valuation) in the non-linear extension in arith. It removes a deprecated hack (addTautology) for doing this.
This addresses CVC4/cvc4-projects#113.
Note that the best method for relevance is interleaving, where roughly you gain on SMT-LIB:
QF_NIA: +484-53 unsat +792-440 sat
QF_NRA: +32-19 unsat +57-23 sat
However, this PR does not (yet) enable this method by default.
Note that more work is necessary to determine which lemmas require NEEDS_JUSTIFY, this PR identifies 2 cases of lemmas that need justification (skolemization and strings reductions). Regardless, the use of the relevance manager is limited to non-linear arithmetic for now, which is only able to answer "sat" when only arithmetic is present in assertions.
read_only = true
help = "whether to increment the precision for irrational function constraints"
+[[option]]
+ name = "nlRlvMode"
+ category = "regular"
+ long = "nl-rlv=MODE"
+ type = "NlRlvMode"
+ default = "NONE"
+ help = "choose mode for using relevance of assertoins in non-linear arithmetic"
+ help_mode = "Modes for using relevance of assertoins in non-linear arithmetic."
+[[option.mode.NONE]]
+ name = "none"
+ help = "Do not use relevance."
+[[option.mode.INTERLEAVE]]
+ name = "interleave"
+ help = "Alternate rounds using relevance."
+[[option.mode.ALWAYS]]
+ name = "always"
+ help = "Always use relevance."
+
[[option]]
name = "brabTest"
category = "regular"
default = "true"
read_only = true
help = "condense values for functions in models rather than explicitly representing them"
+
+[[option]]
+ name = "relevanceFilter"
+ category = "regular"
+ long = "relevance-filter"
+ type = "bool"
+ default = "false"
+ help = "enable analysis of relevance of asserted literals with respect to the input formula"
}
}
+ if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
+ && options::nlRlvMode() != options::NlRlvMode::NONE)
+ {
+ if (!options::relevanceFilter())
+ {
+ if (options::relevanceFilter.wasSetByUser())
+ {
+ Warning() << "SmtEngine: turning on relevance filtering to support "
+ "--nl-ext-rlv="
+ << options::nlRlvMode() << std::endl;
+ }
+ // must use relevance filtering techniques
+ options::relevanceFilter.set(true);
+ }
+ }
+
// For now, these array theory optimizations do not support model-building
if (options::produceModels() || options::produceAssignments()
|| options::checkModels())
#include "expr/node_algorithm.h"
#include "options/arith_options.h"
+#include "options/theory_options.h"
#include "theory/arith/arith_msum.h"
#include "theory/arith/arith_utilities.h"
#include "theory/rewriter.h"
std::vector<Node> check_assertions;
for (const Node& a : assertions)
{
- // don't have to check tautological literals
- if (d_tautology.find(a) != d_tautology.end())
- {
- continue;
- }
if (d_check_model_solved.find(a) == d_check_model_solved.end())
{
Node av = a;
bool NlModel::usedApproximate() const { return d_used_approx; }
-void NlModel::addTautology(Node n)
-{
- // ensure rewritten
- n = Rewriter::rewrite(n);
- std::unordered_set<TNode, TNodeHashFunction> visited;
- std::vector<TNode> visit;
- TNode cur;
- visit.push_back(n);
- do
- {
- cur = visit.back();
- visit.pop_back();
- if (visited.find(cur) == visited.end())
- {
- visited.insert(cur);
- if (cur.getKind() == AND)
- {
- // children of AND are also implied
- for (const Node& cn : cur)
- {
- visit.push_back(cn);
- }
- }
- else
- {
- // is this an arithmetic literal?
- Node atom = cur.getKind() == NOT ? cur[0] : cur;
- if ((atom.getKind() == EQUAL && atom[0].getType().isReal())
- || atom.getKind() == LEQ)
- {
- // Add to tautological literals if it does not contain
- // non-linear multiplication. We cannot consider literals
- // with non-linear multiplication to be tautological since this
- // model object is responsible for checking whether they hold.
- // (TODO, cvc4-projects #113: revisit this).
- if (!expr::hasSubtermKind(NONLINEAR_MULT, atom))
- {
- Trace("nl-taut") << "Tautological literal: " << atom << std::endl;
- d_tautology.insert(cur);
- }
- }
- }
- }
- } while (!visit.empty());
-}
-
bool NlModel::solveEqualitySimple(Node eq,
unsigned d,
std::vector<NlLemma>& lemmas)
void setUsedApproximate();
/** Did we use an approximation during this check? */
bool usedApproximate() const;
- /**
- * This states that formula n is a tautology (satisfied in all models).
- * We call this on internally generated lemmas. This method computes a
- * set of literals that are implied by n, that are hence tautological
- * as well, such as:
- * l_pi <= real.pi <= u_pi (pi approximations)
- * sin(x) = -1*sin(-x)
- * where these literals are internally generated for the purposes
- * of guiding the models of the linear solver.
- *
- * TODO (cvc4-projects #113: would be helpful if we could do this even
- * more aggressively by ignoring all internally generated literals.
- *
- * Tautological literals do not need be checked during checkModel.
- */
- void addTautology(Node n);
//------------------------------ end recording model substitutions and bounds
/**
std::unordered_map<Node, Node, NodeHashFunction> d_check_model_solved;
/** did we use an approximation on this call to last-call effort? */
bool d_used_approx;
- /** the set of all tautological literals */
- std::unordered_set<Node, NodeHashFunction> d_tautology;
}; /* class NlModel */
} // namespace nl
d_containing(containing),
d_ee(ee),
d_needsLastCall(false),
+ d_checkCounter(0),
d_extTheory(&containing),
d_model(containing.getSatContext()),
d_trSlv(d_model),
d_lemmas.insert(lem);
}
d_stats.d_inferences << nlem.d_id;
- // also indicate this is a tautology
- d_model.addTautology(lem);
}
}
d_trSlv.processSideEffect(se);
}
+void NonlinearExtension::computeRelevantAssertions(
+ const std::vector<Node>& assertions, std::vector<Node>& keep)
+{
+ Trace("nl-ext-rlv") << "Compute relevant assertions..." << std::endl;
+ Valuation v = d_containing.getValuation();
+ for (const Node& a : assertions)
+ {
+ if (v.isRelevant(a))
+ {
+ keep.push_back(a);
+ }
+ }
+ Trace("nl-ext-rlv") << "...keep " << keep.size() << "/" << assertions.size()
+ << " assertions" << std::endl;
+}
+
unsigned NonlinearExtension::filterLemma(NlLemma lem, std::vector<NlLemma>& out)
{
Trace("nl-ext-lemma-debug")
void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
{
Trace("nl-ext") << "Getting assertions..." << std::endl;
+ bool useRelevance = false;
+ if (options::nlRlvMode() == options::NlRlvMode::INTERLEAVE)
+ {
+ useRelevance = (d_checkCounter % 2);
+ }
+ else if (options::nlRlvMode() == options::NlRlvMode::ALWAYS)
+ {
+ useRelevance = true;
+ }
+ Valuation v = d_containing.getValuation();
NodeManager* nm = NodeManager::currentNM();
// get the assertions
std::map<Node, Rational> init_bounds[2];
nassertions++;
const Assertion& assertion = *it;
Node lit = assertion.d_assertion;
+ if (useRelevance && !v.isRelevant(lit))
+ {
+ // not relevant, skip
+ continue;
+ }
init_assertions.insert(lit);
// check for concrete bounds
bool pol = lit.getKind() != NOT;
}
bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
- const std::vector<Node>& false_asserts,
std::vector<NlLemma>& lemmas,
std::vector<Node>& gs)
{
// get the presubstitution
Trace("nl-ext-cm-debug") << " apply pre-substitution..." << std::endl;
- std::vector<Node> passertions = assertions;
+ std::vector<Node> passertions;
+ if (options::nlRlvMode() != options::NlRlvMode::NONE)
+ {
+ // only keep the relevant assertions (those required for showing input
+ // is satisfied)
+ computeRelevantAssertions(assertions, passertions);
+ }
+ else
+ {
+ passertions = assertions;
+ }
if (options::nlExt())
{
// preprocess the assertions with the trancendental solver
bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
{
++(d_stats.d_mbrRuns);
+ d_checkCounter++;
// get the assertions
std::vector<Node> assertions;
// error bounds on the Taylor approximation of transcendental functions.
std::vector<NlLemma> lemmas;
std::vector<Node> gs;
- if (checkModel(assertions, false_asserts, lemmas, gs))
+ if (checkModel(assertions, lemmas, gs))
{
complete_status = 1;
}
* ensureLiteral respectively.
*/
bool checkModel(const std::vector<Node>& assertions,
- const std::vector<Node>& false_asserts,
std::vector<NlLemma>& lemmas,
std::vector<Node>& gs);
//---------------------------end check model
-
+ /** compute relevant assertions */
+ void computeRelevantAssertions(const std::vector<Node>& assertions,
+ std::vector<Node>& keep);
/**
* Potentially adds lemmas to the set out and clears lemmas. Returns
* the number of lemmas added to out. We do not add lemmas that have already
NlStats d_stats;
// needs last call effort
bool d_needsLastCall;
+ /**
+ * The number of times we have the called main check method
+ * (modelBasedRefinement). This counter is used for interleaving strategies.
+ */
+ unsigned d_checkCounter;
/** Extended theory, responsible for context-dependent simplification. */
ExtTheory d_extTheory;
/** The non-linear model object
{
return (p & LemmaProperty::SEND_ATOMS) != LemmaProperty::NONE;
}
+bool isLemmaPropertyNeedsJustify(LemmaProperty p)
+{
+ return (p & LemmaProperty::NEEDS_JUSTIFY) != LemmaProperty::NONE;
+}
std::ostream& operator<<(std::ostream& out, LemmaProperty p)
{
{
out << " SEND_ATOMS";
}
+ if (isLemmaPropertyNeedsJustify(p))
+ {
+ out << " NEEDS_JUSTIFY";
+ }
out << " }";
}
return out;
// whether the lemma needs preprocessing
PREPROCESS = 2,
// whether the processing of the lemma should send atoms to the caller
- SEND_ATOMS = 4
+ SEND_ATOMS = 4,
+ // whether the lemma is part of the justification for answering "sat"
+ NEEDS_JUSTIFY = 8
};
/** Define operator lhs | rhs */
LemmaProperty operator|(LemmaProperty lhs, LemmaProperty rhs);
bool isLemmaPropertyPreprocess(LemmaProperty p);
/** is the send atoms bit set on p? */
bool isLemmaPropertySendAtoms(LemmaProperty p);
+/** is the needs justify bit set on p? */
+bool isLemmaPropertyNeedsJustify(LemmaProperty p);
/**
* Writes an lemma property name to a stream.
Trace("quantifiers-sk-debug")
<< "Skolemize lemma : " << slem << std::endl;
}
- getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS);
+ getOutputChannel().lemma(
+ lem, LemmaProperty::PREPROCESS | LemmaProperty::NEEDS_JUSTIFY);
}
return;
}
d_termReg.registerTermAtomic(n, sks.first);
}
}
-
- d_out.lemma(lem);
+ LemmaProperty p = LemmaProperty::NONE;
+ if (ii.d_id == Inference::REDUCTION)
+ {
+ p |= LemmaProperty::NEEDS_JUSTIFY;
+ }
+ d_out.lemma(lem, p);
}
// process the pending require phase calls
for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
#include "theory/quantifiers/fmf/model_engine.h"
#include "theory/quantifiers/theory_quantifiers.h"
#include "theory/quantifiers_engine.h"
+#include "theory/relevance_manager.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
#include "theory/theory_model.h"
d_userContext, "DefaultModel", options::assignFunctionValues());
d_aloc_curr_model = true;
}
+ // create the relevance filter if any option requires it
+ if (options::relevanceFilter())
+ {
+ d_relManager.reset(
+ new RelevanceManager(d_userContext, theory::Valuation(this)));
+ }
//make the default builder, e.g. in the case that the quantifiers engine does not have a model builder
if( d_curr_model_builder==NULL ){
d_eeDistributed(nullptr),
d_quantEngine(nullptr),
d_decManager(new DecisionManager(userContext)),
+ d_relManager(nullptr),
d_curr_model(nullptr),
d_aloc_curr_model(false),
d_curr_model_builder(nullptr),
// If in full effort, we have a fake new assertion just to jumpstart the checking
if (Theory::fullEffort(effort)) {
d_factsAsserted = true;
+ // Reset round for the relevance manager, which notice only sets a flag
+ // to indicate that its information must be recomputed.
+ if (d_relManager != nullptr)
+ {
+ d_relManager->resetRound();
+ }
}
// Check until done
CVC4_FOR_EACH_THEORY;
}
+bool TheoryEngine::isRelevant(Node lit) const
+{
+ if (d_relManager != nullptr)
+ {
+ return d_relManager->isRelevant(lit);
+ }
+ // otherwise must assume its relevant
+ return true;
+}
+
void TheoryEngine::shutdown() {
// Set this first; if a Theory shutdown() throws an exception,
// at least the destruction of the TheoryEngine won't confound
theoryOf(theoryId)->ppNotifyAssertions(assertions);
}
}
+ if (d_relManager != nullptr)
+ {
+ d_relManager->notifyPreprocessedAssertions(assertions);
+ }
}
bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
lemmas.push_back(newLemmas[i].getNode());
}
+ // If specified, we must add this lemma to the set of those that need to be
+ // justified, where note we pass all auxiliary lemmas in lemmas, since these
+ // by extension must be justified as well.
+ if (d_relManager != nullptr && isLemmaPropertyNeedsJustify(p))
+ {
+ d_relManager->notifyPreprocessedAssertions(lemmas.ref());
+ }
+
// assert lemmas to prop engine
for (size_t i = 0, lsize = lemmas.size(); i < lsize; ++i)
{
it != it_end;
++it) {
Node assertion = (*it).d_assertion;
+ if (!isRelevant(assertion))
+ {
+ // not relevant, skip
+ continue;
+ }
Node val = getModel()->getValue(assertion);
if (val != d_true)
{
#include "prop/prop_engine.h"
#include "smt/command.h"
#include "theory/atom_requests.h"
-#include "theory/decision_manager.h"
#include "theory/engine_output_channel.h"
#include "theory/interrupted.h"
#include "theory/rewriter.h"
class TheoryEngineModelBuilder;
class EqEngineManagerDistributed;
+ class DecisionManager;
+ class RelevanceManager;
+
namespace eq {
class EqualityEngine;
}/* CVC4::theory::eq namespace */
* The decision manager
*/
std::unique_ptr<theory::DecisionManager> d_decManager;
+ /** The relevance manager */
+ std::unique_ptr<theory::RelevanceManager> d_relManager;
/**
* Default model object
inline bool needCheck() const {
return d_outputChannelUsed || d_lemmasAdded;
}
+ /**
+ * Is the literal lit (possibly) critical for satisfying the input formula in
+ * the current context? This call is applicable only during collectModelInfo
+ * or during LAST_CALL effort.
+ */
+ bool isRelevant(Node lit) const;
/**
* This is called at shutdown time by the SmtEngine, just before
return d_engine->needCheck();
}
+bool Valuation::isRelevant(Node lit) const { return d_engine->isRelevant(lit); }
+
}/* CVC4::theory namespace */
}/* CVC4 namespace */
/** need check ? */
bool needCheck() const;
-
+
+ /**
+ * Is the literal lit (possibly) critical for satisfying the input formula in
+ * the current context? This call is applicable only during collectModelInfo
+ * or during LAST_CALL effort.
+ */
+ bool isRelevant(Node lit) const;
};/* class Valuation */
}/* CVC4::theory namespace */
+% COMMAND-LINE: --nl-rlv=none
% EXPECT: entailed
QUERY FORALL (x:INT) : EXISTS (y:INT) : (x*y=x) ;
-; COMMAND-LINE: --no-check-models --produce-models --decision=internal
+; COMMAND-LINE: --no-check-models --produce-models --decision=internal --nl-rlv=always
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
-; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models
+; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models --nl-rlv=always
; EXPECT: sat
(set-logic QF_NRAT)
(set-info :status sat)
-; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models
+; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models --nl-rlv=always
; EXPECT: sat
(set-logic QF_NRAT)
(set-info :status sat)
; EXPECT: sat
-; COMMAND-LINE: --sygus-inference --no-check-models
+; COMMAND-LINE: --sygus-inference --no-check-models --nl-rlv=always
(set-logic ALL)
(declare-fun a () Real)
(assert (> a 0.000001))
projects / cvc5.git / commitdiff