Towards eliminating dependencies on quantifiers engine.
theory/quantifiers/ematching/inst_match_generator_multi_linear.h
theory/quantifiers/ematching/inst_match_generator_simple.cpp
theory/quantifiers/ematching/inst_match_generator_simple.h
+ theory/quantifiers/ematching/inst_strategy.cpp
theory/quantifiers/ematching/inst_strategy.h
theory/quantifiers/ematching/inst_strategy_e_matching.cpp
theory/quantifiers/ematching/inst_strategy_e_matching.h
bool ConjectureGenerator::needsCheck( Theory::Effort e ) {
// synchonized with instantiation engine
- return d_quantEngine->getInstWhenNeedsCheck( e );
+ return d_qstate.getInstWhenNeedsCheck(e);
}
bool ConjectureGenerator::hasEnumeratedUf( Node n ) {
--- /dev/null
+/********************* */
+/*! \file inst_strategy.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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.\endverbatim
+ **
+ ** \brief Instantiation engine strategy base class
+ **/
+
+#include "theory/quantifiers/ematching/inst_strategy.h"
+
+#include "theory/quantifiers/quantifiers_state.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+InstStrategy::InstStrategy(QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ QuantifiersInferenceManager& qim)
+ : d_quantEngine(qe), d_qstate(qs), d_qim(qim)
+{
+}
+InstStrategy::~InstStrategy() {}
+void InstStrategy::presolve() {}
+std::string InstStrategy::identify() const { return std::string("Unknown"); }
+
+options::UserPatMode InstStrategy::getInstUserPatMode() const
+{
+ if (options::userPatternsQuant() == options::UserPatMode::INTERLEAVE)
+ {
+ return d_qstate.getInstRounds() % 2 == 0 ? options::UserPatMode::USE
+ : options::UserPatMode::RESORT;
+ }
+ return options::userPatternsQuant();
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
- ** \brief Instantiation Engine classes
+ ** \brief Instantiation engine strategy base class
**/
#include "cvc4_private.h"
#include <vector>
#include "expr/node.h"
+#include "options/quantifiers_options.h"
#include "theory/theory.h"
namespace CVC4 {
public:
InstStrategy(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim)
- : d_quantEngine(qe), d_qstate(qs), d_qim(qim)
- {
- }
- virtual ~InstStrategy() {}
+ QuantifiersInferenceManager& qim);
+ virtual ~InstStrategy();
/** presolve */
- virtual void presolve() {}
+ virtual void presolve();
/** reset instantiation */
virtual void processResetInstantiationRound(Theory::Effort effort) = 0;
/** process method, returns a status */
virtual InstStrategyStatus process(Node f, Theory::Effort effort, int e) = 0;
/** identify */
- virtual std::string identify() const { return std::string("Unknown"); }
+ virtual std::string identify() const;
protected:
+ /**
+ * Get the current user pat mode, which may be interleaved based on counters
+ * maintained by the quantifiers state.
+ */
+ options::UserPatMode getInstUserPatMode() const;
/** reference to the instantiation engine */
QuantifiersEngine* d_quantEngine;
/** The quantifiers state object */
Theory::Effort effort,
int e)
{
- options::UserPatMode upMode = d_quantEngine->getInstUserPatMode();
+ options::UserPatMode upMode = getInstUserPatMode();
if (hasUserPatterns(f) && upMode == options::UserPatMode::TRUST)
{
return InstStrategyStatus::STATUS_UNKNOWN;
{
return InstStrategyStatus::STATUS_UNFINISHED;
}
- options::UserPatMode upm = d_quantEngine->getInstUserPatMode();
+ options::UserPatMode upm = getInstUserPatMode();
int peffort = upm == options::UserPatMode::RESORT ? 2 : 1;
if (e < peffort)
{
}
Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl;
// check match option
- if (d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT)
+ if (getInstUserPatMode() == options::UserPatMode::RESORT)
{
d_user_gen_wait[q].push_back(nodes);
return;
#include <map>
#include "expr/node.h"
+#include "options/quantifiers_options.h"
#include "theory/quantifiers/ematching/inst_strategy.h"
#include "theory/quantifiers/ematching/trigger.h"
}
bool InstantiationEngine::needsCheck( Theory::Effort e ){
- return d_quantEngine->getInstWhenNeedsCheck( e );
+ return d_qstate.getInstWhenNeedsCheck(e);
}
void InstantiationEngine::reset_round( Theory::Effort e ){
}
if (options::fullSaturateInterleave())
{
- if (d_quantEngine->getInstWhenNeedsCheck(e))
+ // if interleaved, we run at the same time as E-matching
+ if (d_qstate.getInstWhenNeedsCheck(e))
{
return true;
}
#include "theory/quantifiers/quantifiers_state.h"
+#include "options/quantifiers_options.h"
+
namespace CVC4 {
namespace theory {
namespace quantifiers {
QuantifiersState::QuantifiersState(context::Context* c,
context::UserContext* u,
Valuation val)
- : TheoryState(c, u, val)
+ : TheoryState(c, u, val), d_ierCounterc(c)
+{
+ // allow theory combination to go first, once initially
+ d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
+ d_ierCounterc = d_ierCounter;
+ d_ierCounterLc = 0;
+ d_ierCounterLastLc = 0;
+ d_instWhenPhase =
+ 1 + (options::instWhenPhase() < 1 ? 1 : options::instWhenPhase());
+}
+
+void QuantifiersState::incrementInstRoundCounters(Theory::Effort e)
+{
+ if (e == Theory::EFFORT_FULL)
+ {
+ // increment if a last call happened, we are not strictly enforcing
+ // interleaving, or already were in phase
+ if (d_ierCounterLastLc != d_ierCounterLc
+ || !options::instWhenStrictInterleave()
+ || d_ierCounter % d_instWhenPhase != 0)
+ {
+ d_ierCounter = d_ierCounter + 1;
+ d_ierCounterLastLc = d_ierCounterLc;
+ d_ierCounterc = d_ierCounterc.get() + 1;
+ }
+ }
+ else if (e == Theory::EFFORT_LAST_CALL)
+ {
+ d_ierCounterLc = d_ierCounterLc + 1;
+ }
+}
+
+bool QuantifiersState::getInstWhenNeedsCheck(Theory::Effort e) const
+{
+ Trace("qstate-debug") << "Get inst when needs check, counts=" << d_ierCounter
+ << ", " << d_ierCounterLc << std::endl;
+ // determine if we should perform check, based on instWhenMode
+ bool performCheck = false;
+ if (options::instWhenMode() == options::InstWhenMode::FULL)
+ {
+ performCheck = (e >= Theory::EFFORT_FULL);
+ }
+ else if (options::instWhenMode() == options::InstWhenMode::FULL_DELAY)
+ {
+ performCheck = (e >= Theory::EFFORT_FULL) && !d_valuation.needCheck();
+ }
+ else if (options::instWhenMode() == options::InstWhenMode::FULL_LAST_CALL)
+ {
+ performCheck =
+ ((e == Theory::EFFORT_FULL && d_ierCounter % d_instWhenPhase != 0)
+ || e == Theory::EFFORT_LAST_CALL);
+ }
+ else if (options::instWhenMode()
+ == options::InstWhenMode::FULL_DELAY_LAST_CALL)
+ {
+ performCheck = ((e == Theory::EFFORT_FULL && !d_valuation.needCheck()
+ && d_ierCounter % d_instWhenPhase != 0)
+ || e == Theory::EFFORT_LAST_CALL);
+ }
+ else if (options::instWhenMode() == options::InstWhenMode::LAST_CALL)
+ {
+ performCheck = (e >= Theory::EFFORT_LAST_CALL);
+ }
+ else
+ {
+ performCheck = true;
+ }
+ Trace("qstate-debug") << "...returned " << performCheck << std::endl;
+ return performCheck;
+}
+
+uint64_t QuantifiersState::getInstRoundDepth() const
+{
+ return d_ierCounterc.get();
+}
+
+uint64_t QuantifiersState::getInstRounds() const { return d_ierCounter; }
+
+void QuantifiersState::debugPrintEqualityEngine(const char* c) const
{
+ bool traceEnabled = Trace.isOn(c);
+ if (!traceEnabled)
+ {
+ return;
+ }
+ eq::EqualityEngine* ee = getEqualityEngine();
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
+ std::map<TypeNode, uint64_t> tnum;
+ while (!eqcs_i.isFinished())
+ {
+ TNode r = (*eqcs_i);
+ TypeNode tr = r.getType();
+ if (tnum.find(tr) == tnum.end())
+ {
+ tnum[tr] = 0;
+ }
+ tnum[tr]++;
+ bool firstTime = true;
+ Trace(c) << " " << r;
+ Trace(c) << " : { ";
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
+ while (!eqc_i.isFinished())
+ {
+ TNode n = (*eqc_i);
+ if (r != n)
+ {
+ if (firstTime)
+ {
+ Trace(c) << std::endl;
+ firstTime = false;
+ }
+ Trace(c) << " " << n << std::endl;
+ }
+ ++eqc_i;
+ }
+ if (!firstTime)
+ {
+ Trace(c) << " ";
+ }
+ Trace(c) << "}" << std::endl;
+ ++eqcs_i;
+ }
+ Trace(c) << std::endl;
+ for (const std::pair<const TypeNode, uint64_t>& t : tnum)
+ {
+ Trace(c) << "# eqc for " << t.first << " : " << t.second << std::endl;
+ }
}
} // namespace quantifiers
#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
+#include "theory/theory.h"
#include "theory/theory_state.h"
namespace CVC4 {
public:
QuantifiersState(context::Context* c, context::UserContext* u, Valuation val);
~QuantifiersState() {}
+ /**
+ * Increment the instantiation counters, called once at the beginning of when
+ * we perform a check with quantifiers engine for the given effort.
+ */
+ void incrementInstRoundCounters(Theory::Effort e);
+ /**
+ * Get whether we need to check at effort e based on the inst-when mode. This
+ * option determines the policy of quantifier instantiation and theory
+ * combination, e.g. does it run before, after, or interleaved with theory
+ * combination. This is based on the state of the counters maintained by this
+ * class.
+ */
+ bool getInstWhenNeedsCheck(Theory::Effort e) const;
+ /** Get the number of instantiation rounds performed in this SAT context */
+ uint64_t getInstRoundDepth() const;
+ /** Get the total number of instantiation rounds performed */
+ uint64_t getInstRounds() const;
+ /** debug print equality engine on trace c */
+ void debugPrintEqualityEngine(const char* c) const;
+
+ private:
+ /** The number of instantiation rounds in this SAT context */
+ context::CDO<uint64_t> d_ierCounterc;
+ /** The number of total instantiation rounds (full effort) */
+ uint64_t d_ierCounter;
+ /** The number of total instantiation rounds (last call effort) */
+ uint64_t d_ierCounterLc;
+ /**
+ * A counter to remember the last value of d_ierCounterLc where we a
+ * full effort check. This is used for interleaving theory combination
+ * and quantifier instantiation rounds.
+ */
+ uint64_t d_ierCounterLastLc;
+ /**
+ * The number of instantiation rounds we run for each call to theory
+ * combination.
+ */
+ uint64_t d_instWhenPhase;
};
} // namespace quantifiers
d_term_enum(new quantifiers::TermEnumeration),
d_quants_prereg(qstate.getUserContext()),
d_quants_red(qstate.getUserContext()),
- d_ierCounter_c(qstate.getSatContext()),
d_presolve(qstate.getUserContext(), true),
d_presolve_in(qstate.getUserContext()),
d_presolve_cache(qstate.getUserContext())
//---- end utilities
- //allow theory combination to go first, once initially
- d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
- d_ierCounter_c = d_ierCounter;
- d_ierCounter_lc = 0;
- d_ierCounterLastLc = 0;
- d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
-
// Finite model finding requires specialized ways of building the model.
// We require constructing the model and model builder here, since it is
// required for initializing the CombinationEngine.
if( Trace.isOn("quant-engine-debug") ){
Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
- Trace("quant-engine-debug") << " depth : " << d_ierCounter_c << std::endl;
+ Trace("quant-engine-debug")
+ << " depth : " << d_qstate.getInstRoundDepth() << std::endl;
Trace("quant-engine-debug") << " modules to check : ";
for( unsigned i=0; i<qm.size(); i++ ){
Trace("quant-engine-debug") << qm[i]->identify() << " ";
}
if( Trace.isOn("quant-engine-ee-pre") ){
Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl;
- debugPrintEqualityEngine( "quant-engine-ee-pre" );
+ d_qstate.debugPrintEqualityEngine("quant-engine-ee-pre");
}
if( Trace.isOn("quant-engine-assert") ){
Trace("quant-engine-assert") << "Assertions : " << std::endl;
if( Trace.isOn("quant-engine-ee") ){
Trace("quant-engine-ee") << "Equality engine : " << std::endl;
- debugPrintEqualityEngine( "quant-engine-ee" );
+ d_qstate.debugPrintEqualityEngine("quant-engine-ee");
}
//reset the model
Assert(!d_qstate.isInConflict());
if (quant_e == QuantifiersModule::QEFFORT_CONFLICT)
{
- if( e==Theory::EFFORT_FULL ){
- //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase
- if( d_ierCounterLastLc!=d_ierCounter_lc || !options::instWhenStrictInterleave() || d_ierCounter%d_inst_when_phase!=0 ){
- d_ierCounter = d_ierCounter + 1;
- d_ierCounterLastLc = d_ierCounter_lc;
- d_ierCounter_c = d_ierCounter_c.get() + 1;
- }
- }else if( e==Theory::EFFORT_LAST_CALL ){
- d_ierCounter_lc = d_ierCounter_lc + 1;
- }
+ d_qstate.incrementInstRoundCounters(e);
}
else if (quant_e == QuantifiersModule::QEFFORT_MODEL)
{
}
void QuantifiersEngine::notifyCombineTheories() {
- //if allowing theory combination to happen at most once between instantiation rounds
- //d_ierCounter = 1;
- //d_ierCounterLastLc = -1;
+ // If allowing theory combination to happen at most once between instantiation
+ // rounds, this would reset d_ierCounter to 1 and d_ierCounterLastLc to -1
+ // in quantifiers state.
}
bool QuantifiersEngine::reduceQuantifier( Node q ) {
d_model->markRelevant( q );
}
-bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
- Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl;
- //determine if we should perform check, based on instWhenMode
- bool performCheck = false;
- if (options::instWhenMode() == options::InstWhenMode::FULL)
- {
- performCheck = ( e >= Theory::EFFORT_FULL );
- }
- else if (options::instWhenMode() == options::InstWhenMode::FULL_DELAY)
- {
- performCheck =
- (e >= Theory::EFFORT_FULL) && !d_qstate.getValuation().needCheck();
- }
- else if (options::instWhenMode() == options::InstWhenMode::FULL_LAST_CALL)
- {
- performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL );
- }
- else if (options::instWhenMode()
- == options::InstWhenMode::FULL_DELAY_LAST_CALL)
- {
- performCheck =
- ((e == Theory::EFFORT_FULL && !d_qstate.getValuation().needCheck()
- && d_ierCounter % d_inst_when_phase != 0)
- || e == Theory::EFFORT_LAST_CALL);
- }
- else if (options::instWhenMode() == options::InstWhenMode::LAST_CALL)
- {
- performCheck = ( e >= Theory::EFFORT_LAST_CALL );
- }
- else
- {
- performCheck = true;
- }
- return performCheck;
-}
-
-options::UserPatMode QuantifiersEngine::getInstUserPatMode()
-{
- if (options::userPatternsQuant() == options::UserPatMode::INTERLEAVE)
- {
- return d_ierCounter % 2 == 0 ? options::UserPatMode::USE
- : options::UserPatMode::RESORT;
- }
- else
- {
- return options::userPatternsQuant();
- }
-}
-
void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
d_instantiate->getInstantiationTermVectors(q, tvecs);
}
return d_qmodules->d_synth_e->getSynthSolutions(sol_map);
}
-void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
- eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
- std::map< TypeNode, int > typ_num;
- while( !eqcs_i.isFinished() ){
- TNode r = (*eqcs_i);
- TypeNode tr = r.getType();
- if( typ_num.find( tr )==typ_num.end() ){
- typ_num[tr] = 0;
- }
- typ_num[tr]++;
- bool firstTime = true;
- Trace(c) << " " << r;
- Trace(c) << " : { ";
- eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
- while( !eqc_i.isFinished() ){
- TNode n = (*eqc_i);
- if( r!=n ){
- if( firstTime ){
- Trace(c) << std::endl;
- firstTime = false;
- }
- Trace(c) << " " << n << std::endl;
- }
- ++eqc_i;
- }
- if( !firstTime ){ Trace(c) << " "; }
- Trace(c) << "}" << std::endl;
- ++eqcs_i;
- }
- Trace(c) << std::endl;
- for( std::map< TypeNode, int >::iterator it = typ_num.begin(); it != typ_num.end(); ++it ){
- Trace(c) << "# eqc for " << it->first << " : " << it->second << std::endl;
- }
-}
-
} // namespace theory
} // namespace CVC4
/** mark relevant quantified formula, this will indicate it should be checked
* before the others */
void markRelevant(Node q);
- /** get needs check */
- bool getInstWhenNeedsCheck(Theory::Effort e);
- /** get user pat mode */
- options::UserPatMode getInstUserPatMode();
-
-public:
/** add term to database */
void addTermToDatabase(Node n, bool withinQuant = false);
/** notification when master equality engine is updated */
void eqNotifyNewClass(TNode t);
- /** debug print equality engine */
- void debugPrintEqualityEngine(const char* c);
/** get internal representative
*
* Choose a term that is equivalent to a in the current context that is the
/** quantifiers reduced */
BoolMap d_quants_red;
std::map<Node, Node> d_quants_red_lem;
- /** inst round counters TODO: make context-dependent? */
- context::CDO<int> d_ierCounter_c;
- int d_ierCounter;
- int d_ierCounter_lc;
- int d_ierCounterLastLc;
- int d_inst_when_phase;
/** has presolve been called */
context::CDO<bool> d_presolve;
/** presolve cache */
projects / cvc5.git / commitdiff