summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r--src/theory/quantifiers_engine.cpp408
1 files changed, 60 insertions, 348 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 2d1ae7983..0e10dfe54 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -26,6 +26,7 @@
#include "theory/quantifiers/ce_guided_instantiation.h"
#include "theory/quantifiers/ceg_t_instantiator.h"
#include "theory/quantifiers/conjecture_generator.h"
+#include "theory/quantifiers/equality_query.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/full_model_check.h"
#include "theory/quantifiers/fun_def_engine.h"
@@ -34,12 +35,15 @@
#include "theory/quantifiers/instantiation_engine.h"
#include "theory/quantifiers/local_theory_ext.h"
#include "theory/quantifiers/model_engine.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/quant_conflict_find.h"
#include "theory/quantifiers/quant_equality_engine.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/relevant_domain.h"
#include "theory/quantifiers/rewrite_engine.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers/trigger.h"
#include "theory/quantifiers/quant_split.h"
#include "theory/quantifiers/anti_skolem.h"
@@ -74,11 +78,21 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
d_presolve_cache_wq(u),
d_presolve_cache_wic(u){
//utilities
- d_eq_query = new EqualityQueryQuantifiersEngine( c, this );
+ d_eq_query = new quantifiers::EqualityQueryQuantifiersEngine( c, this );
d_util.push_back( d_eq_query );
d_term_db = new quantifiers::TermDb( c, u, this );
d_util.push_back( d_term_db );
+
+ d_term_util = new quantifiers::TermUtil( this );
+
+ if (options::ceGuidedInst()) {
+ d_sygus_tdb = new quantifiers::TermDbSygus(c, this);
+ }else{
+ d_sygus_tdb = NULL;
+ }
+
+ d_quant_attr = new quantifiers::QuantAttributes( this );
if( options::instPropagate() ){
// notice that this option is incompatible with options::qcfAllConflict()
@@ -88,6 +102,12 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
}else{
d_inst_prop = NULL;
}
+
+ if( options::inferArithTriggerEq() ){
+ d_eq_inference = new quantifiers::EqualityInference( c, options::inferArithTriggerEqExp() );
+ }else{
+ d_eq_inference = NULL;
+ }
d_tr_trie = new inst::TriggerTrie;
d_curr_effort_level = QEFFORT_NONE;
@@ -95,7 +115,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
d_hasAddedLemma = false;
d_useModelEe = false;
//don't add true lemma
- d_lemmas_produced_c[d_term_db->d_true] = true;
+ d_lemmas_produced_c[d_term_util->d_true] = true;
Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
@@ -166,6 +186,9 @@ QuantifiersEngine::~QuantifiersEngine(){
delete d_model;
delete d_tr_trie;
delete d_term_db;
+ delete d_sygus_tdb;
+ delete d_term_util;
+ delete d_eq_inference;
delete d_eq_query;
delete d_sg_gen;
delete d_ceg_inst;
@@ -179,7 +202,7 @@ QuantifiersEngine::~QuantifiersEngine(){
delete d_inst_prop;
}
-EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
+EqualityQuery* QuantifiersEngine::getEqualityQuery() {
return d_eq_query;
}
@@ -337,7 +360,7 @@ bool QuantifiersEngine::isFiniteBound( Node q, Node v ) {
TypeNode tn = v.getType();
if( tn.isSort() && options::finiteModelFind() ){
return true;
- }else if( getTermDatabase()->mayComplete( tn ) ){
+ }else if( getTermUtil()->mayComplete( tn ) ){
return true;
}
}
@@ -717,9 +740,16 @@ bool QuantifiersEngine::registerQuantifier( Node f ){
d_quants[f] = false;
return false;
}else{
- //make instantiation constants for f
- d_term_db->makeInstantiationConstantsFor( f );
- d_term_db->computeAttributes( f );
+ // register with utilities : TODO (#1163) make this a standard call
+
+ d_term_util->registerQuantifier( f );
+ d_term_db->registerQuantifier( f );
+ d_quant_attr->computeAttributes( f );
+ //register with quantifier relevance
+ if( d_quant_rel ){
+ d_quant_rel->registerQuantifier( f );
+ }
+
for( unsigned i=0; i<d_modules.size(); i++ ){
Trace("quant-debug") << "pre-register with " << d_modules[i]->identify() << "..." << std::endl;
d_modules[i]->preRegisterQuantifier( f );
@@ -728,17 +758,13 @@ bool QuantifiersEngine::registerQuantifier( Node f ){
if( qm!=NULL ){
Trace("quant") << " Owner : " << qm->identify() << std::endl;
}
- //register with quantifier relevance
- if( d_quant_rel ){
- d_quant_rel->registerQuantifier( f );
- }
//register with each module
for( unsigned i=0; i<d_modules.size(); i++ ){
Trace("quant-debug") << "register with " << d_modules[i]->identify() << "..." << std::endl;
d_modules[i]->registerQuantifier( f );
}
//TODO: remove this
- Node ceBody = d_term_db->getInstConstantBody( f );
+ Node ceBody = d_term_util->getInstConstantBody( f );
//also register it with the strong solver
//if( options::finiteModelFind() ){
// ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
@@ -767,7 +793,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
if( !reduceQuantifier( f ) ){
//do skolemization
if( d_skolemized.find( f )==d_skolemized.end() ){
- Node body = d_term_db->getSkolemizedBody( f );
+ Node body = d_term_util->getSkolemizedBody( f );
NodeBuilder<> nb(kind::OR);
nb << f << body.notNode();
Node lem = nb;
@@ -787,7 +813,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
for( unsigned i=0; i<d_modules.size(); i++ ){
d_modules[i]->assertNode( f );
}
- addTermToDatabase( d_term_db->getInstConstantBody( f ), true );
+ addTermToDatabase( d_term_util->getInstConstantBody( f ), true );
}
}
}
@@ -813,10 +839,6 @@ Node QuantifiersEngine::getNextDecisionRequest( unsigned& priority ){
return dec;
}
-quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() {
- return getTermDatabase()->getTermDatabaseSygus();
-}
-
void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
if( options::incrementalSolving() ){
if( d_presolve_in.find( n )==d_presolve_in.end() ){
@@ -844,14 +866,14 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within
void QuantifiersEngine::eqNotifyNewClass(TNode t) {
addTermToDatabase( t );
- if( d_eq_query->getEqualityInference() ){
- d_eq_query->getEqualityInference()->eqNotifyNewClass( t );
+ if( d_eq_inference ){
+ d_eq_inference->eqNotifyNewClass( t );
}
}
void QuantifiersEngine::eqNotifyPreMerge(TNode t1, TNode t2) {
- if( d_eq_query->getEqualityInference() ){
- d_eq_query->getEqualityInference()->eqNotifyMerge( t1, t2 );
+ if( d_eq_inference ){
+ d_eq_inference->eqNotifyMerge( t1, t2 );
}
}
@@ -947,7 +969,7 @@ Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms, std::
Debug("check-inst") << "Substitute inst constant : " << n << std::endl;
ret = terms[n.getAttribute(InstVarNumAttribute())];
}else{
- //if( !quantifiers::TermDb::hasInstConstAttr( n ) ){
+ //if( !quantifiers::TermUtil::hasInstConstAttr( n ) ){
//Debug("check-inst") << "No inst const attr : " << n << std::endl;
//return n;
//}else{
@@ -998,7 +1020,7 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std
body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
}else{
//do optimized version
- Node icb = d_term_db->getInstConstantBody( q );
+ Node icb = d_term_util->getInstConstantBody( q );
std::map< Node, Node > visited;
body = getSubstitute( icb, terms, visited );
if( Debug.isOn("check-inst") ){
@@ -1013,7 +1035,7 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std
//do virtual term substitution
body = Rewriter::rewrite( body );
Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl;
- Node body_r = d_term_db->rewriteVtsSymbols( body );
+ Node body_r = d_term_util->rewriteVtsSymbols( body );
Trace("quant-vts-debug") << " ...result: " << body_r << std::endl;
body = body_r;
}
@@ -1028,8 +1050,8 @@ Node QuantifiersEngine::getInstantiation( Node q, InstMatch& m, bool doVts ){
}
Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms, bool doVts ) {
- Assert( d_term_db->d_vars.find( q )!=d_term_db->d_vars.end() );
- return getInstantiation( q, d_term_db->d_vars[q], terms, doVts );
+ Assert( d_term_util->d_vars.find( q )!=d_term_util->d_vars.end() );
+ return getInstantiation( q, d_term_util->d_vars[q], terms, doVts );
}
/*
@@ -1114,7 +1136,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
terms[i] = getInternalRepresentative( terms[i], q, i );
}else{
//ensure the type is correct
- terms[i] = quantifiers::TermDb::ensureType( terms[i], q[0][i].getType() );
+ terms[i] = quantifiers::TermUtil::ensureType( terms[i], q[0][i].getType() );
}
Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
if( terms[i].isNull() ){
@@ -1123,24 +1145,24 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
}else{
//get relevancy conditions
if( options::instRelevantCond() ){
- quantifiers::TermDb::getRelevancyCondition( terms[i], rlv_cond );
+ quantifiers::TermUtil::getRelevancyCondition( terms[i], rlv_cond );
}
}
#ifdef CVC4_ASSERTIONS
bool bad_inst = false;
- if( quantifiers::TermDb::containsUninterpretedConstant( terms[i] ) ){
+ if( quantifiers::TermUtil::containsUninterpretedConstant( terms[i] ) ){
Trace("inst") << "***& inst contains uninterpreted constant : " << terms[i] << std::endl;
bad_inst = true;
}else if( !terms[i].getType().isSubtypeOf( q[0][i].getType() ) ){
Trace("inst") << "***& inst bad type : " << terms[i] << " " << terms[i].getType() << "/" << q[0][i].getType() << std::endl;
bad_inst = true;
}else if( options::cbqi() ){
- Node icf = quantifiers::TermDb::getInstConstAttr(terms[i]);
+ Node icf = quantifiers::TermUtil::getInstConstAttr(terms[i]);
if( !icf.isNull() ){
if( icf==q ){
Trace("inst") << "***& inst contains inst constant attr : " << terms[i] << std::endl;
bad_inst = true;
- }else if( quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] ) ){
+ }else if( quantifiers::TermUtil::containsTerms( terms[i], d_term_util->d_inst_constants[q] ) ){
Trace("inst") << "***& inst contains inst constants : " << terms[i] << std::endl;
bad_inst = true;
}
@@ -1193,8 +1215,8 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
//construct the instantiation
Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
- Assert( d_term_db->d_vars[q].size()==terms.size() );
- Node body = getInstantiation( q, d_term_db->d_vars[q], terms, doVts ); //do virtual term substitution
+ Assert( d_term_util->d_vars[q].size()==terms.size() );
+ Node body = getInstantiation( q, d_term_util->d_vars[q], terms, doVts ); //do virtual term substitution
Node orig_body = body;
if( options::cbqiNestedQE() && d_i_cbqi ){
body = d_i_cbqi->doNestedQE( q, terms, body, doVts );
@@ -1208,7 +1230,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
if( d_useModelEe && options::instNoModelTrue() ){
Node val_body = d_model->getValue( body );
- if( val_body==d_term_db->d_true ){
+ if( val_body==d_term_util->d_true ){
Trace("inst-add-debug") << " --> True in model." << std::endl;
++(d_statistics.d_inst_duplicate_model_true);
return false;
@@ -1495,9 +1517,9 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) {
printed = true;
out << "(skolem " << q << std::endl;
out << " ( ";
- for( unsigned i=0; i<d_term_db->d_skolem_constants[q].size(); i++ ){
+ for( unsigned i=0; i<d_term_util->d_skolem_constants[q].size(); i++ ){
if( i>0 ){ out << " "; }
- out << d_term_db->d_skolem_constants[q][i];
+ out << d_term_util->d_skolem_constants[q][i];
}
out << " )" << std::endl;
out << ")" << std::endl;
@@ -1595,7 +1617,7 @@ Node QuantifiersEngine::getInstantiatedConjunction( Node q ) {
}
//have to remove q, TODO: avoid this in a better way
TNode tq = q;
- TNode tt = d_term_db->d_true;
+ TNode tt = d_term_util->d_true;
ret = ret.substitute( tq, tt );
return ret;
}
@@ -1739,313 +1761,3 @@ void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
}
}
-
-EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ) : d_qe( qe ), d_eqi_counter( c ), d_reset_count( 0 ){
- if( options::inferArithTriggerEq() ){
- d_eq_inference = new quantifiers::EqualityInference( c, options::inferArithTriggerEqExp() );
- }else{
- d_eq_inference = NULL;
- }
-}
-
-EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){
- delete d_eq_inference;
-}
-
-bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){
- d_int_rep.clear();
- d_reset_count++;
- return processInferences( e );
-}
-
-bool EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) {
- if( options::inferArithTriggerEq() ){
- eq::EqualityEngine* ee = getEngine();
- //updated implementation
- while( d_eqi_counter.get()<d_eq_inference->getNumPendingMerges() ){
- Node eq = d_eq_inference->getPendingMerge( d_eqi_counter.get() );
- Node eq_exp = d_eq_inference->getPendingMergeExplanation( d_eqi_counter.get() );
- Trace("quant-engine-ee-proc") << "processInferences : Infer : " << eq << std::endl;
- Trace("quant-engine-ee-proc") << " explanation : " << eq_exp << std::endl;
- Assert( ee->hasTerm( eq[0] ) );
- Assert( ee->hasTerm( eq[1] ) );
- if( areDisequal( eq[0], eq[1] ) ){
- Trace("quant-engine-ee-proc") << "processInferences : Conflict : " << eq << std::endl;
- if( Trace.isOn("term-db-lemma") ){
- Trace("term-db-lemma") << "Disequal terms, equal by normalization : " << eq[0] << " " << eq[1] << "!!!!" << std::endl;
- if( !d_qe->getTheoryEngine()->needCheck() ){
- Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl;
- //this should really never happen (implies arithmetic is incomplete when sharing is enabled)
- Assert( false );
- }
- Trace("term-db-lemma") << " add split on : " << eq << std::endl;
- }
- d_qe->addSplit( eq );
- return false;
- }else{
- ee->assertEquality( eq, true, eq_exp );
- d_eqi_counter = d_eqi_counter.get() + 1;
- }
- }
- Assert( ee->consistent() );
- }
- return true;
-}
-
-bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){
- return getEngine()->hasTerm( a );
-}
-
-Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){
- eq::EqualityEngine* ee = getEngine();
- if( ee->hasTerm( a ) ){
- return ee->getRepresentative( a );
- }else{
- return a;
- }
-}
-
-bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
- if( a==b ){
- return true;
- }else{
- eq::EqualityEngine* ee = getEngine();
- if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
- return ee->areEqual( a, b );
- }else{
- return false;
- }
- }
-}
-
-bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
- if( a==b ){
- return false;
- }else{
- eq::EqualityEngine* ee = getEngine();
- if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
- return ee->areDisequal( a, b, false );
- }else{
- return a.isConst() && b.isConst();
- }
- }
-}
-
-Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){
- Assert( f.isNull() || f.getKind()==FORALL );
- Node r = getRepresentative( a );
- if( options::finiteModelFind() ){
- if( r.isConst() && quantifiers::TermDb::containsUninterpretedConstant( r ) ){
- //map back from values assigned by model, if any
- if( d_qe->getModel() ){
- std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r );
- if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){
- r = it->second;
- r = getRepresentative( r );
- }else{
- if( r.getType().isSort() ){
- Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
- //should never happen : UF constants should never escape model
- Assert( false );
- }
- }
- }
- }
- }
- if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_EE ){
- return r;
- }else{
- TypeNode v_tn = f.isNull() ? a.getType() : f[0][index].getType();
- std::map< Node, Node >::iterator itir = d_int_rep[v_tn].find( r );
- if( itir==d_int_rep[v_tn].end() ){
- //find best selection for representative
- Node r_best;
- //if( options::fmfRelevantDomain() && !f.isNull() ){
- // Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl;
- // r_best = d_qe->getRelevantDomain()->getRelevantTerm( f, index, r );
- // Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl;
- //}
- std::vector< Node > eqc;
- getEquivalenceClass( r, eqc );
- Trace("internal-rep-select") << "Choose representative for equivalence class : { ";
- for( unsigned i=0; i<eqc.size(); i++ ){
- if( i>0 ) Trace("internal-rep-select") << ", ";
- Trace("internal-rep-select") << eqc[i];
- }
- Trace("internal-rep-select") << " }, type = " << v_tn << std::endl;
- int r_best_score = -1;
- for( size_t i=0; i<eqc.size(); i++ ){
- int score = getRepScore( eqc[i], f, index, v_tn );
- if( score!=-2 ){
- if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
- r_best = eqc[i];
- r_best_score = score;
- }
- }
- }
- if( r_best.isNull() ){
- Trace("internal-rep-warn") << "No valid choice for representative in eqc class." << std::endl;
- r_best = r;
- }
- //now, make sure that no other member of the class is an instance
- std::unordered_map<TNode, Node, TNodeHashFunction> cache;
- r_best = getInstance( r_best, eqc, cache );
- //store that this representative was chosen at this point
- if( d_rep_score.find( r_best )==d_rep_score.end() ){
- d_rep_score[ r_best ] = d_reset_count;
- }
- Trace("internal-rep-select") << "...Choose " << r_best << " with score " << r_best_score << std::endl;
- Assert( r_best.getType().isSubtypeOf( v_tn ) );
- d_int_rep[v_tn][r] = r_best;
- if( r_best!=a ){
- Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
- Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
- }
- return r_best;
- }else{
- return itir->second;
- }
- }
-}
-
-void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ) {
- //make sure internal representatives currently exist
- for( std::map< TypeNode, std::vector< Node > >::iterator it = reps.begin(); it != reps.end(); ++it ){
- if( it->first.isSort() ){
- for( unsigned i=0; i<it->second.size(); i++ ){
- Node r = getInternalRepresentative( it->second[i], Node::null(), 0 );
- }
- }
- }
- Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl;
- for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
- for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
- Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
- }
- }
- //store representatives for newly created terms
- std::map< Node, Node > temp_rep_map;
-
- bool success;
- do {
- success = false;
- for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
- for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
- if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){
- Node ni = it->second;
- std::vector< Node > cc;
- cc.push_back( it->second.getOperator() );
- bool changed = false;
- for( unsigned j=0; j<ni.getNumChildren(); j++ ){
- if( ni[j].getType().isSort() ){
- Node r = getRepresentative( ni[j] );
- if( itt->second.find( r )==itt->second.end() ){
- Assert( temp_rep_map.find( r )!=temp_rep_map.end() );
- r = temp_rep_map[r];
- }
- if( r==ni ){
- //found sub-term as instance
- Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl;
- itt->second[it->first] = ni[j];
- changed = false;
- success = true;
- break;
- }else{
- Node ir = itt->second[r];
- cc.push_back( ir );
- if( ni[j]!=ir ){
- changed = true;
- }
- }
- }else{
- changed = false;
- break;
- }
- }
- if( changed ){
- Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc );
- Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl;
- success = true;
- itt->second[it->first] = n;
- temp_rep_map[n] = it->first;
- }
- }
- }
- }
- }while( success );
- Trace("internal-rep-flatten") << "---After flattening : " << std::endl;
- for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
- for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
- Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
- }
- }
-}
-
-eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
- return d_qe->getActiveEqualityEngine();
-}
-
-void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
- eq::EqualityEngine* ee = getEngine();
- if( ee->hasTerm( a ) ){
- Node rep = ee->getRepresentative( a );
- eq::EqClassIterator eqc_iter( rep, ee );
- while( !eqc_iter.isFinished() ){
- eqc.push_back( *eqc_iter );
- eqc_iter++;
- }
- }else{
- eqc.push_back( a );
- }
- //a should be in its equivalence class
- Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() );
-}
-
-TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNode >& args ) {
- return d_qe->getTermDatabase()->getCongruentTerm( f, args );
-}
-
-//helper functions
-
-Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ){
- if(cache.find(n) != cache.end()) {
- return cache[n];
- }
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- Node nn = getInstance( n[i], eqc, cache );
- if( !nn.isNull() ){
- return cache[n] = nn;
- }
- }
- if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){
- return cache[n] = n;
- }else{
- return cache[n] = Node::null();
- }
-}
-
-//-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
-int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, TypeNode v_tn ){
- if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){ //reject
- return -2;
- }else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type
- return -2;
- }else if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){
- return -1;
- }else if( options::instMaxLevel()!=-1 ){
- //score prefer lowest instantiation level
- if( n.hasAttribute(InstLevelAttribute()) ){
- return n.getAttribute(InstLevelAttribute());
- }else{
- return options::instLevelInputOnly() ? -1 : 0;
- }
- }else{
- if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_FIRST ){
- //score prefers earliest use of this term as a representative
- return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
- }else{
- Assert( options::quantRepMode()==quantifiers::QUANT_REP_MODE_DEPTH );
- return quantifiers::TermDb::getTermDepth( n );
- }
- }
-}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback