#define ARITH_INSTANTIATOR_USE_MINUS_DELTA
-InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) : InstStrategy( qe ){
+InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ){
}
-void InstStrategyCbqi::processResetInstantiationRound( Theory::Effort effort ) {
+bool InstStrategyCbqi::needsCheck( Theory::Effort e ) {
+ return e>=Theory::EFFORT_LAST_CALL;
+}
+
+unsigned InstStrategyCbqi::needsModel( Theory::Effort e ) {
+ for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+ if( d_quantEngine->getOwner( q )==this && d_quantEngine->getModel()->isQuantifierActive( q ) ){
+ return QuantifiersEngine::QEFFORT_STANDARD;
+ }
+ }
+ return QuantifiersEngine::QEFFORT_NONE;
+}
+
+void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
d_cbqi_set_quant_inactive = false;
//check if any cbqi lemma has not been added yet
for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
//it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
- if( d_quantEngine->hasOwnership( q, d_quantEngine->getInstantiationEngine() ) && doCbqi( q ) ){
+ if( d_quantEngine->getOwner( q )==this ){
if( !hasAddedCbqiLemma( q ) ){
- d_added_cbqi_lemma[q] = true;
+ d_added_cbqi_lemma.insert( q );
Trace("cbqi") << "Do cbqi for " << q << std::endl;
//add cbqi lemma
//get the counterexample literal
}
}
}
+ processResetInstantiationRound( effort );
+}
+
+void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) {
+ if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
+ for( int ee=0; ee<=1; ee++ ){
+ unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
+ for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+ if( d_quantEngine->getOwner( q )==this && d_quantEngine->getModel()->isQuantifierActive( q ) ){
+ process( q, e, ee );
+ }
+ }
+ if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
+ break;
+ }
+ }
+ }
+}
+
+bool InstStrategyCbqi::checkComplete() {
+ if( !options::cbqiSat() && d_cbqi_set_quant_inactive ){
+ return false;
+ }else{
+ return true;
+ }
+}
+
+void InstStrategyCbqi::preRegisterQuantifier( Node q ) {
+ if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
+ //take ownership of the quantified formula
+ d_quantEngine->setOwner( q, this );
+ }
+}
+
+void InstStrategyCbqi::registerQuantifier( Node q ) {
+
}
void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){
std::map< Node, bool >::iterator it = d_do_cbqi.find( q );
if( it==d_do_cbqi.end() ){
bool ret = false;
- Assert( options::cbqi() );
- if( options::cbqiAll() ){
- ret = true;
+ //if has an instantiation pattern, don't do it
+ if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
+ ret = false;
}else{
- //if quantifier has a non-arithmetic variable, then do not use cbqi
- //if quantifier has an APPLY_UF term, then do not use cbqi
- Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
- std::map< Node, bool > visited;
- ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( cb, visited );
+ if( options::cbqiAll() ){
+ ret = true;
+ }else{
+ //if quantifier has a non-arithmetic variable, then do not use cbqi
+ //if quantifier has an APPLY_UF term, then do not use cbqi
+ Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
+ std::map< Node, bool > visited;
+ ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( cb, visited );
+ }
}
d_do_cbqi[q] = ret;
return ret;
Debug("quant-arith-debug") << std::endl;
debugPrint( "quant-arith-debug" );
d_counter++;
- InstStrategyCbqi::processResetInstantiationRound( effort );
}
void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder<>& t ){
}
}
-int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
- if( doCbqi( f ) ){
- if( e<1 ){
- return STATUS_UNFINISHED;
- }else if( e==1 ){
- if( d_quantActive.find( f )!=d_quantActive.end() ){
- //the point instantiation
- InstMatch m_point( f );
- bool m_point_valid = true;
- int lem = 0;
- //scan over all instantiation rows
- for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
- Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
- Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl;
- for( int j=0; j<(int)d_instRows[ic].size(); j++ ){
- ArithVar x = d_instRows[ic][j];
- if( !d_ceTableaux[ic][x].empty() ){
- if( Debug.isOn("quant-arith-simplex") ){
- Debug("quant-arith-simplex") << "--- Check row " << ic << " " << x << std::endl;
- Debug("quant-arith-simplex") << " ";
- for( std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); it != d_ceTableaux[ic][x].end(); ++it ){
- if( it!=d_ceTableaux[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
- Debug("quant-arith-simplex") << it->first << " * " << it->second;
- }
- Debug("quant-arith-simplex") << " = ";
- Node v = getTableauxValue( x, false );
- Debug("quant-arith-simplex") << v << std::endl;
- Debug("quant-arith-simplex") << " term : " << d_tableaux_term[ic][x] << std::endl;
- Debug("quant-arith-simplex") << " ce-term : ";
- for( std::map< Node, Node >::iterator it = d_tableaux_ce_term[ic][x].begin(); it != d_tableaux_ce_term[ic][x].end(); it++ ){
- if( it!=d_tableaux_ce_term[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
- Debug("quant-arith-simplex") << it->first << " * " << it->second;
- }
- Debug("quant-arith-simplex") << std::endl;
+void InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
+ if( e==0 ){
+ if( d_quantActive.find( f )!=d_quantActive.end() ){
+ //the point instantiation
+ InstMatch m_point( f );
+ bool m_point_valid = true;
+ int lem = 0;
+ //scan over all instantiation rows
+ for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
+ Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
+ Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl;
+ for( int j=0; j<(int)d_instRows[ic].size(); j++ ){
+ ArithVar x = d_instRows[ic][j];
+ if( !d_ceTableaux[ic][x].empty() ){
+ if( Debug.isOn("quant-arith-simplex") ){
+ Debug("quant-arith-simplex") << "--- Check row " << ic << " " << x << std::endl;
+ Debug("quant-arith-simplex") << " ";
+ for( std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); it != d_ceTableaux[ic][x].end(); ++it ){
+ if( it!=d_ceTableaux[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
+ Debug("quant-arith-simplex") << it->first << " * " << it->second;
}
- //instantiation row will be A*e + B*t = beta,
- // where e is a vector of terms , and t is vector of ground terms.
- // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
- // We will construct the term ( beta - B*t)/coeff to use for e_i.
- InstMatch m( f );
- for( unsigned k=0; k<f[0].getNumChildren(); k++ ){
- if( f[0][k].getType().isInteger() ){
- m.setValue( k, d_zero );
- }
+ Debug("quant-arith-simplex") << " = ";
+ Node v = getTableauxValue( x, false );
+ Debug("quant-arith-simplex") << v << std::endl;
+ Debug("quant-arith-simplex") << " term : " << d_tableaux_term[ic][x] << std::endl;
+ Debug("quant-arith-simplex") << " ce-term : ";
+ for( std::map< Node, Node >::iterator it = d_tableaux_ce_term[ic][x].begin(); it != d_tableaux_ce_term[ic][x].end(); it++ ){
+ if( it!=d_tableaux_ce_term[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
+ Debug("quant-arith-simplex") << it->first << " * " << it->second;
}
- //By default, choose the first instantiation constant to be e_i.
- Node var = d_ceTableaux[ic][x].begin()->first;
- //if it is integer, we need to find variable with coefficent +/- 1
- if( var.getType().isInteger() ){
- std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin();
- while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){
- ++it;
- if( it==d_ceTableaux[ic][x].end() ){
- var = Node::null();
- }else{
- var = it->first;
- }
- }
- //Otherwise, try one that divides all ground term coefficients?
- // Might be futile, if rewrite ensures gcd of coeffs is 1.
+ Debug("quant-arith-simplex") << std::endl;
+ }
+ //instantiation row will be A*e + B*t = beta,
+ // where e is a vector of terms , and t is vector of ground terms.
+ // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
+ // We will construct the term ( beta - B*t)/coeff to use for e_i.
+ InstMatch m( f );
+ for( unsigned k=0; k<f[0].getNumChildren(); k++ ){
+ if( f[0][k].getType().isInteger() ){
+ m.setValue( k, d_zero );
}
- if( !var.isNull() ){
- //add to point instantiation if applicable
- if( d_tableaux_ce_term[ic][x].empty() && d_tableaux_term[ic][x]==d_zero ){
- Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl;
- Node v = getTableauxValue( x, false );
- if( !var.getType().isInteger() || v.getType().isInteger() ){
- m_point.setValue( i, v );
- }else{
- m_point_valid = false;
- }
+ }
+ //By default, choose the first instantiation constant to be e_i.
+ Node var = d_ceTableaux[ic][x].begin()->first;
+ //if it is integer, we need to find variable with coefficent +/- 1
+ if( var.getType().isInteger() ){
+ std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin();
+ while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){
+ ++it;
+ if( it==d_ceTableaux[ic][x].end() ){
+ var = Node::null();
+ }else{
+ var = it->first;
}
- Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
- if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){
- lem++;
+ }
+ //Otherwise, try one that divides all ground term coefficients?
+ // Might be futile, if rewrite ensures gcd of coeffs is 1.
+ }
+ if( !var.isNull() ){
+ //add to point instantiation if applicable
+ if( d_tableaux_ce_term[ic][x].empty() && d_tableaux_term[ic][x]==d_zero ){
+ Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl;
+ Node v = getTableauxValue( x, false );
+ if( !var.getType().isInteger() || v.getType().isInteger() ){
+ m_point.setValue( i, v );
+ }else{
+ m_point_valid = false;
}
- }else{
- Debug("quant-arith-simplex") << "Could not find var." << std::endl;
}
+ Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
+ if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){
+ lem++;
+ }
+ }else{
+ Debug("quant-arith-simplex") << "Could not find var." << std::endl;
}
}
}
- if( lem==0 && m_point_valid ){
- if( d_quantEngine->addInstantiation( f, m_point ) ){
- Debug("quant-arith-simplex") << "...added point instantiation." << std::endl;
- }
+ }
+ if( lem==0 && m_point_valid ){
+ if( d_quantEngine->addInstantiation( f, m_point ) ){
+ Debug("quant-arith-simplex") << "...added point instantiation." << std::endl;
}
}
}
}
- return STATUS_UNKNOWN;
}
bool InstStrategySimplex::doInstantiation( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var ){
//first try +delta
if( doInstantiation2( f, ic, term, x, m, var ) ){
- ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith);
+ ++(d_quantEngine->d_statistics.d_instantiations_cbqi_arith);
return true;
}else{
#ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA
//otherwise try -delta
if( doInstantiation2( f, ic, term, x, m, var, true ) ){
- ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith_minus);
+ ++(d_quantEngine->d_statistics.d_instantiations_cbqi_arith);
return true;
}else{
return false;
void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) {
d_check_vts_lemma_lc = true;
- InstStrategyCbqi::processResetInstantiationRound( effort );
-}
-
-int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
- //can only be called at last call, since it is model-based
- if( doCbqi( f ) && effort==Theory::EFFORT_LAST_CALL ){
- if( e<1 ){
- return STATUS_UNFINISHED;
- }else if( e==1 ){
- CegInstantiator * cinst = getInstantiator( f );
- Trace("inst-alg") << "-> Run cegqi for " << f << std::endl;
- d_curr_quant = f;
- bool addedLemma = cinst->check();
- d_curr_quant = Node::null();
- return addedLemma ? STATUS_UNKNOWN : STATUS_UNFINISHED;
- }else if( e==2 ){
- //minimize the free delta heuristically on demand
- if( d_check_vts_lemma_lc ){
- d_check_vts_lemma_lc = false;
- d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const );
- d_small_const = Rewriter::rewrite( d_small_const );
- //heuristic for now, until we know how to do nested quantification
- Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( true, false );
- if( !delta.isNull() ){
- Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl;
- Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const );
- d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
- }
- std::vector< Node > inf;
- d_quantEngine->getTermDatabase()->getVtsTerms( inf, true, false, false );
- for( unsigned i=0; i<inf.size(); i++ ){
- Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl;
- Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) );
- d_quantEngine->getOutputChannel().lemma( inf_lem_lb );
- }
+}
+
+void InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
+ if( e==0 ){
+ CegInstantiator * cinst = getInstantiator( f );
+ Trace("inst-alg") << "-> Run cegqi for " << f << std::endl;
+ d_curr_quant = f;
+ cinst->check();
+ d_curr_quant = Node::null();
+ }else if( e==1 ){
+ //minimize the free delta heuristically on demand
+ if( d_check_vts_lemma_lc ){
+ d_check_vts_lemma_lc = false;
+ d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const );
+ d_small_const = Rewriter::rewrite( d_small_const );
+ //heuristic for now, until we know how to do nested quantification
+ Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( true, false );
+ if( !delta.isNull() ){
+ Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl;
+ Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const );
+ d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
+ }
+ std::vector< Node > inf;
+ d_quantEngine->getTermDatabase()->getVtsTerms( inf, true, false, false );
+ for( unsigned i=0; i<inf.size(); i++ ){
+ Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl;
+ Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) );
+ d_quantEngine->getOutputChannel().lemma( inf_lem_lb );
}
}
}
- return STATUS_UNKNOWN;
}
bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs ) {
namespace quantifiers {
-class InstStrategyCbqi : public InstStrategy {
+class InstStrategyCbqi : public QuantifiersModule {
+ typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
protected:
bool d_cbqi_set_quant_inactive;
/** whether we have added cbqi lemma */
- std::map< Node, bool > d_added_cbqi_lemma;
+ NodeSet d_added_cbqi_lemma;
/** whether to do cbqi for this quantified formula */
std::map< Node, bool > d_do_cbqi;
/** register ce lemma */
/** helper functions */
bool hasNonCbqiVariable( Node q );
bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited );
+ /** process functions */
+ virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
+ virtual void process( Node q, Theory::Effort effort, int e ) = 0;
public:
InstStrategyCbqi( QuantifiersEngine * qe );
~InstStrategyCbqi() throw() {}
+ /** whether to do CBQI for quantifier q */
+ bool doCbqi( Node q );
/** process functions */
- void processResetInstantiationRound( Theory::Effort effort );
+ bool needsCheck( Theory::Effort e );
+ unsigned needsModel( Theory::Effort e );
+ void reset_round( Theory::Effort e );
+ void check( Theory::Effort e, unsigned quant_e );
+ bool checkComplete();
+ void preRegisterQuantifier( Node q );
+ void registerQuantifier( Node q );
/** get next decision request */
Node getNextDecisionRequest();
- //set quant inactive
- bool setQuantifierInactive() { return d_cbqi_set_quant_inactive; }
- /** whether to do CBQI for quantifier q */
- bool doCbqi( Node q );
};
Node d_negOne;
/** process functions */
void processResetInstantiationRound( Theory::Effort effort );
- int process( Node f, Theory::Effort effort, int e );
+ void process( Node f, Theory::Effort effort, int e );
public:
InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie );
~InstStrategySimplex() throw() {}
bool d_check_vts_lemma_lc;
/** process functions */
void processResetInstantiationRound( Theory::Effort effort );
- int process( Node f, Theory::Effort effort, int e );
+ void process( Node f, Theory::Effort effort, int e );
/** register ce lemma */
void registerCounterexampleLemma( Node q, Node lem );
public:
InstMatch baseMatch( f );
int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );
Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl;
- d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst;
+ d_quantEngine->d_statistics.d_instantiations_user_patterns += numInst;
if( d_user_gen[f][i]->isMultiTrigger() ){
d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
}
int numInst = tr->addInstantiations( baseMatch );
hasInst = numInst>0 || hasInst;
Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl;
- d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen += numInst;
+ d_quantEngine->d_statistics.d_instantiations_auto_gen += numInst;
if( r==1 ){
d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
}
}
if( d_quantEngine->addInstantiation( f, terms, false ) ){
Trace("inst-alg-rd") << "Success!" << std::endl;
- ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
+ ++(d_quantEngine->d_statistics.d_instantiations_guess);
return true;
}else{
index--;
d_guessed[f] = true;
InstMatch m( f );
if( d_quantEngine->addInstantiation( f, m ) ){
- ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
+ ++(d_quantEngine->d_statistics.d_instantiations_guess);
return true;
}
}
}
-void FullSaturation::assertNode( Node n ) {
-
-}
void reset_round( Theory::Effort e );
void check( Theory::Effort e, unsigned quant_e );
void registerQuantifier( Node q );
- void assertNode( Node n );
/** identify */
std::string identify() const { return std::string("FullSaturation"); }
};/* class FullSaturation */
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/inst_strategy_e_matching.h"
-#include "theory/quantifiers/inst_strategy_cbqi.h"
#include "theory/quantifiers/trigger.h"
using namespace std;
using namespace CVC4::theory::inst;
InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe ) :
-QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_splx(NULL), d_i_cegqi( NULL ){
+QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL){
}
InstantiationEngine::~InstantiationEngine() {
delete d_i_ag;
delete d_isup;
- delete d_i_splx;
- delete d_i_cegqi;
}
void InstantiationEngine::finishInit(){
if( options::eMatching() ){
//these are the instantiation strategies for E-matching
-
//user-provided patterns
if( options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
d_isup = new InstStrategyUserPatterns( d_quantEngine );
d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine );
d_instStrategies.push_back( d_i_ag );
}
-
- //counterexample-based quantifier instantiation
- if( options::cbqi() ){
- if( options::cbqiSplx() ){
- d_i_splx = new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine );
- d_instStrategies.push_back( d_i_splx );
- d_i_cbqi = d_i_splx;
- }else{
- d_i_cegqi = new InstStrategyCegqi( d_quantEngine );
- d_instStrategies.push_back( d_i_cegqi );
- d_i_cbqi = d_i_cegqi;
- }
- }else{
- d_i_cbqi = NULL;
- }
}
void InstantiationEngine::presolve() {
}
bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
- unsigned lastWaiting = d_quantEngine->d_lemmas_waiting.size();
+ unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
//iterate over an internal effort level e
int e = 0;
int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;
}
}
//do not consider another level if already added lemma at this level
- if( d_quantEngine->d_lemmas_waiting.size()>lastWaiting ){
+ if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
finished = true;
}
e++;
return d_quantEngine->getInstWhenNeedsCheck( e );
}
-unsigned InstantiationEngine::needsModel( Theory::Effort e ){
- if( options::cbqiModel() && options::cbqi() ){
- Assert( d_i_cbqi!=NULL );
- //needs model if there is at least one cbqi quantified formula that is active
- for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
- Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
- if( d_quantEngine->hasOwnership( q, this ) && d_i_cbqi->doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
- return QuantifiersEngine::QEFFORT_STANDARD;
- }
- }
- }
- return QuantifiersEngine::QEFFORT_NONE;
-}
-
void InstantiationEngine::reset_round( Theory::Effort e ){
//if not, proceed to instantiation round
//reset the instantiation strategies
clSet = double(clock())/double(CLOCKS_PER_SEC);
Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e << "---" << std::endl;
}
- ++(d_statistics.d_instantiation_rounds);
+ //collect all active quantified formulas belonging to this
bool quantActive = false;
d_quants.clear();
for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
- if( !options::cbqi() || !TermDb::hasInstConstAttr( q ) ){
- quantActive = true;
- }
+ quantActive = true;
d_quants.push_back( q );
}
}
}
bool InstantiationEngine::checkComplete() {
- if( !options::cbqiSat() && ( d_i_cbqi && d_i_cbqi->setQuantifierInactive() ) ){
- return false;
- }else{
+ if( !options::finiteModelFind() ){
for( unsigned i=0; i<d_quants.size(); i++ ){
if( isIncomplete( d_quants[i] ) ){
return false;
}
}
- return true;
}
+ return true;
}
-
-void InstantiationEngine::preRegisterQuantifier( Node q ) {
- if( options::cbqi() ){
- if( d_i_cbqi->doCbqi( q ) ){
- d_quantEngine->setOwner( q, this );
- }
- }
+bool InstantiationEngine::isIncomplete( Node q ) {
+ return true;
}
void InstantiationEngine::registerQuantifier( Node f ){
if( d_quantEngine->hasOwnership( f, this ) ){
- for( unsigned i=0; i<d_instStrategies.size(); ++i ){
- d_instStrategies[i]->registerQuantifier( f );
- }
- //Notice() << "do cbqi " << f << " ? " << std::endl;
- /*
- if( options::cbqi() ){
- Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
- if( !doCbqi( f ) ){
- d_quantEngine->addTermToDatabase( ceBody, true );
- }
- }
- */
-
+ //for( unsigned i=0; i<d_instStrategies.size(); ++i ){
+ // d_instStrategies[i]->registerQuantifier( f );
+ //}
//take into account user patterns
if( f.getNumChildren()==3 ){
Node subsPat = d_quantEngine->getTermDatabase()->getInstConstantNode( f[2], f );
}
}
-void InstantiationEngine::assertNode( Node f ){
-}
-
-bool InstantiationEngine::isIncomplete( Node q ) {
- return true;
-}
-
-Node InstantiationEngine::getNextDecisionRequest(){
- if( options::cbqi() ){
- for( unsigned i=0; i<d_instStrategies.size(); ++i ){
- InstStrategy* is = d_instStrategies[i];
- Node lit = is->getNextDecisionRequest();
- if( !lit.isNull() ){
- return lit;
- }
- }
- }
- return Node::null();
-}
-
void InstantiationEngine::addUserPattern( Node f, Node pat ){
if( d_isup ){
d_isup->addUserPattern( f, pat );
d_i_ag->addUserNoPattern( f, pat );
}
}
-
-InstantiationEngine::Statistics::Statistics():
- d_instantiations_user_patterns("InstantiationEngine::Instantiations_User_Patterns", 0),
- d_instantiations_auto_gen("InstantiationEngine::Instantiations_Auto_Gen", 0),
- d_instantiations_guess("InstantiationEngine::Instantiations_Guess", 0),
- d_instantiations_cbqi_arith("InstantiationEngine::Instantiations_Cbqi_Arith", 0),
- d_instantiations_cbqi_arith_minus("InstantiationEngine::Instantiations_Cbqi_Arith_Minus", 0),
- d_instantiations_cbqi_datatypes("InstantiationEngine::Instantiations_Cbqi_Datatypes", 0),
- d_instantiations_lte("InstantiationEngine::Instantiations_Local_T_Ext", 0),
- d_instantiation_rounds("InstantiationEngine::Rounds", 0 )
-{
- StatisticsRegistry::registerStat(&d_instantiations_user_patterns);
- StatisticsRegistry::registerStat(&d_instantiations_auto_gen);
- StatisticsRegistry::registerStat(&d_instantiations_guess);
- StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith);
- StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith_minus);
- StatisticsRegistry::registerStat(&d_instantiations_cbqi_datatypes);
- StatisticsRegistry::registerStat(&d_instantiations_lte);
- StatisticsRegistry::registerStat(&d_instantiation_rounds);
-}
-
-InstantiationEngine::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_instantiations_user_patterns);
- StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen);
- StatisticsRegistry::unregisterStat(&d_instantiations_guess);
- StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith);
- StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith_minus);
- StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_datatypes);
- StatisticsRegistry::unregisterStat(&d_instantiations_lte);
- StatisticsRegistry::unregisterStat(&d_instantiation_rounds);
-}
class InstStrategyUserPatterns;
class InstStrategyAutoGenTriggers;
class InstStrategyFreeVariable;
-class InstStrategyCbqi;
-class InstStrategySimplex;
-class InstStrategyCegqi;
/** instantiation strategy class */
class InstStrategy {
/** identify */
virtual std::string identify() const { return std::string("Unknown"); }
/** register quantifier */
- virtual void registerQuantifier( Node q ) {}
- /** get next decision request */
- virtual Node getNextDecisionRequest() { return Node::null(); }
+ //virtual void registerQuantifier( Node q ) {}
};/* class InstStrategy */
class InstantiationEngine : public QuantifiersModule
private:
/** instantiation strategies */
std::vector< InstStrategy* > d_instStrategies;
- /** instantiation strategies active */
- //std::map< InstStrategy*, bool > d_instStrategyActive;
/** user-pattern instantiation strategy */
InstStrategyUserPatterns* d_isup;
/** auto gen triggers; only kept for destructor cleanup */
InstStrategyAutoGenTriggers* d_i_ag;
- InstStrategyCbqi * d_i_cbqi;
- /** simplex (cbqi) */
- InstStrategySimplex * d_i_splx;
- /** generic cegqi */
- InstStrategyCegqi * d_i_cegqi;
private:
typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
/** current processing quantified formulas */
void finishInit();
void presolve();
bool needsCheck( Theory::Effort e );
- unsigned needsModel( Theory::Effort e );
void reset_round( Theory::Effort e );
void check( Theory::Effort e, unsigned quant_e );
bool checkComplete();
- void preRegisterQuantifier( Node q );
void registerQuantifier( Node q );
- void assertNode( Node f );
Node explain(TNode n){ return Node::null(); }
- Node getNextDecisionRequest();
/** add user pattern */
void addUserPattern( Node f, Node pat );
void addUserNoPattern( Node f, Node pat );
public:
- /** statistics class */
- class Statistics {
- public:
- IntStat d_instantiations_user_patterns;
- IntStat d_instantiations_auto_gen;
- IntStat d_instantiations_guess;
- IntStat d_instantiations_cbqi_arith;
- IntStat d_instantiations_cbqi_arith_minus;
- IntStat d_instantiations_cbqi_datatypes;
- IntStat d_instantiations_lte;
- IntStat d_instantiation_rounds;
- Statistics();
- ~Statistics();
- };
- Statistics d_statistics;
/** Identify this module */
std::string identify() const { return "InstEngine"; }
};/* class InstantiationEngine */
//for each asserted quantifier f,
// - determine selection literals
// - check which function/predicates have good and bad definitions for satisfying f
+ if( d_phase_reqs.find( f )==d_phase_reqs.end() ){
+ d_phase_reqs[f].initialize( d_qe->getTermDatabase()->getInstConstantBody( f ), true );
+ }
int selectLitScore = -1;
- QuantPhaseReq* qpr = d_qe->getPhaseRequirements( f );
- for( std::map< Node, bool >::iterator it = qpr->d_phase_reqs.begin(); it != qpr->d_phase_reqs.end(); ++it ){
+ for( std::map< Node, bool >::iterator it = d_phase_reqs[f].d_phase_reqs.begin(); it != d_phase_reqs[f].d_phase_reqs.end(); ++it ){
//the literal n is phase-required for quantifier f
Node n = it->first;
Node gn = d_qe->getTermDatabase()->getModelBasis( f, n );
int doInstGen( FirstOrderModel* fm, Node f );
//theory-specific build models
void constructModelUf( FirstOrderModel* fm, Node op );
+protected:
+ std::map< Node, QuantPhaseReq > d_phase_reqs;
public:
QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){}
~QModelBuilderDefault() throw() {}
QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){
+ initialize( n, computeEq );
+}
+
+void QuantPhaseReq::initialize( Node n, bool computeEq ){
std::map< Node, int > phaseReqs2;
computePhaseReqs( n, false, phaseReqs2 );
for( std::map< Node, int >::iterator it = phaseReqs2.begin(); it != phaseReqs2.end(); ++it ){
/** helper functions compute phase requirements */
void computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs );
public:
+ QuantPhaseReq(){}
QuantPhaseReq( Node n, bool computeEq = false );
~QuantPhaseReq(){}
+ void initialize( Node n, bool computeEq );
/** is phase required */
bool isPhaseReq( Node lit ) { return d_phase_reqs.find( lit )!=d_phase_reqs.end(); }
/** get phase requirement */
break;
}
}else{
- for( unsigned j=0; j<new_cond.size(); j++ ){
- currCond.erase( new_cond[j] );
+ if( !new_cond.empty() ){
+ for( unsigned j=0; j<new_cond.size(); j++ ){
+ currCond.erase( new_cond[j] );
+ }
+ cache.clear();
}
- cache.clear();
}
}
children.push_back( nn );
#include "theory/quantifiers/fun_def_engine.h"
#include "theory/quantifiers/quant_equality_engine.h"
#include "theory/quantifiers/inst_strategy_e_matching.h"
+#include "theory/quantifiers/inst_strategy_cbqi.h"
using namespace std;
using namespace CVC4;
d_sg_gen = NULL;
}
//maintain invariant : either InstantiationEngine or ModelEngine must be in d_modules
- if( !options::finiteModelFind() || options::fmfInstEngine() || options::cbqi() ){
+ if( !options::finiteModelFind() || options::fmfInstEngine() ){
d_inst_engine = new quantifiers::InstantiationEngine( this );
d_modules.push_back( d_inst_engine );
- if( options::cbqi() && options::cbqiModel() ){
- needsBuilder = true;
- }
}else{
d_inst_engine = NULL;
}
+ //counterexample-based instantiation (initialized during finishInit)
+ d_i_cbqi = NULL;
+ if( options::cbqi() && options::cbqiModel() ){
+ needsBuilder = true;
+ }
+ //finite model finding
if( options::finiteModelFind() ){
if( options::fmfBoundInt() ){
d_bint = new quantifiers::BoundedIntegers( c, this );
delete d_fun_def_engine;
delete d_uee;
delete d_fs;
- for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) {
- delete (*i).second;
- }
+ delete d_i_cbqi;
}
EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
void QuantifiersEngine::finishInit(){
Trace("quant-engine-debug") << "QuantifiersEngine : finishInit " << std::endl;
+ //counterexample-based quantifier instantiation
+ if( options::cbqi() ){
+ if( options::cbqiSplx() ){
+ d_i_cbqi = new quantifiers::InstStrategySimplex( (arith::TheoryArith*)getTheoryEngine()->theoryOf( THEORY_ARITH ), this );
+ d_modules.push_back( d_i_cbqi );
+ }else{
+ d_i_cbqi = new quantifiers::InstStrategyCegqi( this );
+ d_modules.push_back( d_i_cbqi );
+ }
+ }else{
+ d_i_cbqi = NULL;
+ }
for( int i=0; i<(int)d_modules.size(); i++ ){
d_modules[i]->finishInit();
}
}else if( e==Theory::EFFORT_LAST_CALL && quant_e==QEFFORT_MODEL ){
//if we have a chance not to set incomplete
if( !setIncomplete ){
- setIncomplete = true;
+ setIncomplete = false;
//check if we should set the incomplete flag
for( unsigned i=0; i<qm.size(); i++ ){
- if( qm[i]->checkComplete() ){
- Trace("quant-engine-debug") << "Do not set incomplete because " << qm[i]->identify().c_str() << " was complete." << std::endl;
- setIncomplete = false;
+ if( !qm[i]->checkComplete() ){
+ Trace("quant-engine-debug") << "Set incomplete because " << qm[i]->identify().c_str() << " was incomplete." << std::endl;
+ setIncomplete = true;
break;
}
}
}
Node ceBody = d_term_db->getInstConstantBody( f );
//generate the phase requirements
- d_phase_reqs[f] = new QuantPhaseReq( ceBody, true );
+ //d_phase_reqs[f] = new QuantPhaseReq( ceBody, true );
//also register it with the strong solver
//if( options::finiteModelFind() ){
// ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
}
}
-void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
- if( options::literalMatchMode()!=quantifiers::LITERAL_MATCH_NONE && d_phase_reqs.find( f )!=d_phase_reqs.end() ){
- // doing literal-based matching (consider polarity of literals)
- for( int i=0; i<(int)nodes.size(); i++ ){
- Node prev = nodes[i];
- if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){
- bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] );
- nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst<bool>(preq) );
- }
- //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){
- // Node req = qe->getPhaseReqEquality( f, trNodes[i] );
- // trNodes[i] = NodeManager::currentNM()->mkNode( EQUAL, trNodes[i], req );
- //}
- }
- }
-}
-
void QuantifiersEngine::printInstantiations( std::ostream& out ) {
bool printed = false;
for( BoolMap::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){
d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
- d_red_lte_partial_inst("QuantifiersEngine::Reductions_Lte_Partial_Inst", 0)
+ d_red_lte_partial_inst("QuantifiersEngine::Reductions_Lte_Partial_Inst", 0),
+ d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
+ d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
+ d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
+ d_instantiations_cbqi_arith("QuantifiersEngine::Instantiations_Cbqi_Arith", 0)
{
StatisticsRegistry::registerStat(&d_num_quant);
StatisticsRegistry::registerStat(&d_instantiation_rounds);
StatisticsRegistry::registerStat(&d_multi_triggers);
StatisticsRegistry::registerStat(&d_multi_trigger_instantiations);
StatisticsRegistry::registerStat(&d_red_alpha_equiv);
- StatisticsRegistry::registerStat(&d_red_lte_partial_inst);
+ StatisticsRegistry::registerStat(&d_red_lte_partial_inst);
+ StatisticsRegistry::registerStat(&d_instantiations_user_patterns);
+ StatisticsRegistry::registerStat(&d_instantiations_auto_gen);
+ StatisticsRegistry::registerStat(&d_instantiations_guess);
+ StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith);
}
QuantifiersEngine::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_multi_trigger_instantiations);
StatisticsRegistry::unregisterStat(&d_red_alpha_equiv);
StatisticsRegistry::unregisterStat(&d_red_lte_partial_inst);
+ StatisticsRegistry::unregisterStat(&d_instantiations_user_patterns);
+ StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen);
+ StatisticsRegistry::unregisterStat(&d_instantiations_guess);
+ StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith);
}
eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
/* Call during quantifier engine's check */
virtual void check( Theory::Effort e, unsigned quant_e ) = 0;
/* check was complete (e.g. no lemmas implies a model) */
- virtual bool checkComplete() { return false; }
+ virtual bool checkComplete() { return true; }
/* Called for new quantifiers */
virtual void preRegisterQuantifier( Node q ) {}
/* Called for new quantifiers after owners are finalized */
virtual void registerQuantifier( Node q ) = 0;
- virtual void assertNode( Node n ) = 0;
+ virtual void assertNode( Node n ) {}
virtual void propagate( Theory::Effort level ){}
virtual Node getNextDecisionRequest() { return TNode::null(); }
- virtual Node explain(TNode n) { return TNode::null(); }
/** Identify this module (for debugging, dynamic configuration, etc..) */
virtual std::string identify() const = 0;
public:
class FunDefEngine;
class QuantEqualityEngine;
class FullSaturation;
+ class InstStrategyCbqi;
}/* CVC4::theory::quantifiers */
namespace inst {
quantifiers::AlphaEquivalence * d_alpha_equiv;
/** model builder */
quantifiers::QModelBuilder* d_builder;
- /** phase requirements for each quantifier for each instantiation literal */
- std::map< Node, QuantPhaseReq* > d_phase_reqs;
/** instantiation engine */
quantifiers::InstantiationEngine* d_inst_engine;
/** model engine */
quantifiers::QuantEqualityEngine * d_uee;
/** full saturation */
quantifiers::FullSaturation * d_fs;
+ /** counterexample-based quantifier instantiation */
+ quantifiers::InstStrategyCbqi * d_i_cbqi;
public: //effort levels
enum {
QEFFORT_CONFLICT,
QuantRelevance* getQuantifierRelevance() { return d_quant_rel; }
/** get the model builder */
quantifiers::QModelBuilder* getModelBuilder() { return d_builder; }
- /** get phase requirement information */
- QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; }
- /** get phase requirement terms */
- void getPhaseReqTerms( Node f, std::vector< Node >& nodes );
public: //modules
/** get instantiation engine */
quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
quantifiers::QuantEqualityEngine * getQuantEqualityEngine() { return d_uee; }
/** get full saturation */
quantifiers::FullSaturation * getFullSaturation() { return d_fs; }
+ /** get inst strategy cbqi */
+ quantifiers::InstStrategyCbqi * getInstStrategyCbqi() { return d_i_cbqi; }
private:
/** owner of quantified formulas */
std::map< Node, QuantifiersModule * > d_owner;
/** has added lemma */
bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
/** get number of waiting lemmas */
- int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); }
+ unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
/** get needs check */
bool getInstWhenNeedsCheck( Theory::Effort e );
/** get user pat mode */
IntStat d_multi_trigger_instantiations;
IntStat d_red_alpha_equiv;
IntStat d_red_lte_partial_inst;
+ IntStat d_instantiations_user_patterns;
+ IntStat d_instantiations_auto_gen;
+ IntStat d_instantiations_guess;
+ IntStat d_instantiations_cbqi_arith;
Statistics();
~Statistics();
};/* class QuantifiersEngine::Statistics */
}
TheoryUF::~TheoryUF() {
- // destruct all ppRewrite() callbacks
- for(RegisterPpRewrites::iterator i = d_registeredPpRewrites.begin();
- i != d_registeredPpRewrites.end();
- ++i) {
- delete i->second;
- }
delete d_thss;
}
d_thss->assertDisequal(t1, t2, reason);
}
}
-
-Node TheoryUF::ppRewrite(TNode node) {
-
- if (node.getKind() != kind::APPLY_UF) {
- return node;
- }
-
- // perform the callbacks requested by TheoryUF::registerPpRewrite()
- RegisterPpRewrites::iterator c = d_registeredPpRewrites.find(node.getOperator());
- if (c == d_registeredPpRewrites.end()) {
- return node;
- } else {
- Node res = c->second->ppRewrite(node);
- if (res != node) {
- return ppRewrite(res);
- } else {
- return res;
- }
- }
-}
-
};/* class TheoryUF::NotifyClass */
- /** A callback class for ppRewrite(). See registerPpRewrite(), below. */
- class PpRewrite {
- public:
- virtual Node ppRewrite(TNode node) = 0;
- virtual ~PpRewrite() {}
- };/* class TheoryUF::PpRewrite */
-
private:
/** The notify class */
/** called when two equivalence classes are made disequal */
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
- /** a registry type for keeping Node-specific callbacks for ppRewrite() */
- typedef std::hash_map<Node, PpRewrite*, NodeHashFunction> RegisterPpRewrites;
-
- /** a collection of callbacks to issue while doing a ppRewrite() */
- RegisterPpRewrites d_registeredPpRewrites;
-
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
StrongSolverTheoryUF* getStrongSolver() {
return d_thss;
}
-
- Node ppRewrite(TNode node);
-
- /**
- * Register a ppRewrite() callback on "op." TheoryUF owns
- * the callback, and will delete it when it is destructed.
- */
- void registerPpRewrite(TNode op, PpRewrite* callback) {
- d_registeredPpRewrites.insert(std::make_pair(op, callback));
- }
};/* class TheoryUF */
}/* CVC4::theory::uf namespace */
projects / cvc5.git / commitdiff