From 65c2e1688d83dfeb913b689c10d9b43c5dc89cc0 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 27 Jun 2015 09:30:06 +0200 Subject: [PATCH] Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by default on pure quantified arithmetic. Fix bug in sort inference related to mixed real/int, add regression. --- src/smt/smt_engine.cpp | 6 + src/theory/datatypes/datatypes_sygus.cpp | 2 +- .../quantifiers/instantiation_engine.cpp | 5 +- src/theory/quantifiers/model_builder.cpp | 12 +- src/theory/quantifiers/model_builder.h | 4 - src/theory/quantifiers/model_engine.cpp | 68 +++++---- src/theory/quantifiers/options | 4 +- src/theory/quantifiers/quant_util.h | 2 - src/theory/quantifiers/term_database.cpp | 6 +- src/theory/quantifiers/term_database.h | 2 +- src/theory/quantifiers_engine.cpp | 136 +++++++++--------- src/theory/quantifiers_engine.h | 10 +- src/theory/rep_set.cpp | 14 +- src/theory/theory_model.cpp | 20 +-- src/theory/theory_model.h | 2 +- src/util/sort_inference.cpp | 29 +++- test/regress/regress0/fmf/Makefile.am | 3 +- .../regress0/fmf/syn002-si-real-int.smt2 | 11 ++ 18 files changed, 190 insertions(+), 146 deletions(-) create mode 100755 test/regress/regress0/fmf/syn002-si-real-int.smt2 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1ab4ee62a..55e83ee14 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1426,6 +1426,12 @@ void SmtEngine::setDefaults() { } //cbqi options + // enable if pure arithmetic quantifiers + if( d_logic.isQuantified() && d_logic.isPure(THEORY_ARITH) ){ + if( !options::cbqi.wasSetByUser() && !options::cbqi2.wasSetByUser() ){ + options::cbqi2.set( true ); + } + } if( options::recurseCbqi() || options::cbqi2() ){ options::cbqi.set( true ); } diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index d08c92dd9..851f97624 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -820,7 +820,7 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node Node progr = d_tds->getNormalized( at, prog ); Node rep_prog; std::map< Node, Node >::iterator itnp = d_normalized_to_orig[at].find( progr ); - int tsize = d_tds->getTermSize( prog ); + int tsize = d_tds->getSygusTermSize( prog ); if( itnp==d_normalized_to_orig[at].end() ){ d_normalized_to_orig[at][progr] = prog; if( progr.getKind()==SKOLEM && d_tds->getSygusType( progr )==at ){ diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 4fbf298f4..631216507 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -66,11 +66,10 @@ void InstantiationEngine::finishInit(){ //counterexample-based quantifier instantiation if( options::cbqi() ){ - if( !options::cbqi2() || options::cbqi.wasSetByUser() ){ + if( !options::cbqi2() ){ d_i_splx = new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine ); d_instStrategies.push_back( d_i_splx ); - } - if( options::cbqi2() ){ + }else{ d_i_cegqi = new InstStrategyCegqi( d_quantEngine ); d_instStrategies.push_back( d_i_cegqi ); } diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 53f55e70b..e297e138c 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -176,7 +176,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { } //if applicable, find exceptions to model via inst-gen - if( optInstGen() ){ + if( options::fmfInstGen() ){ d_didInstGen = true; d_instGenMatches = 0; d_numQuantSat = 0; @@ -201,7 +201,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { }else{ d_numQuantNoSelForm++; } - if( optOneQuantPerRoundInstGen() && lems>0 ){ + if( options::fmfInstGenOneQuantPerRound() && lems>0 ){ break; } }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){ @@ -341,14 +341,6 @@ bool QModelBuilderIG::hasConstantDefinition( Node n ){ return false; } -bool QModelBuilderIG::optInstGen(){ - return options::fmfInstGen(); -} - -bool QModelBuilderIG::optOneQuantPerRoundInstGen(){ - return options::fmfInstGenOneQuantPerRound(); -} - QModelBuilderIG::Statistics::Statistics(): d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0), d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0), diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index d9ed3f092..8e84f15e2 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -123,10 +123,6 @@ public: QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ); virtual ~QModelBuilderIG() throw() {} public: - //whether to add inst-gen lemmas - virtual bool optInstGen(); - //whether to only consider only quantifier per round of inst-gen - virtual bool optOneQuantPerRoundInstGen(); /** statistics class */ class Statistics { public: diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index ce780a29b..2ad8be3a1 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -157,15 +157,19 @@ int ModelEngine::checkModel(){ if( it->first.isSort() ){ Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; if( Trace.isOn("model-engine-debug") ){ - Trace("model-engine-debug") << " "; - Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); + Trace("model-engine-debug") << " Reps : "; + for( size_t i=0; isecond.size(); i++ ){ + Trace("model-engine-debug") << it->second[i] << " "; + } + Trace("model-engine-debug") << std::endl; + Trace("model-engine-debug") << " Term reps : "; for( size_t i=0; isecond.size(); i++ ){ - //Trace("model-engine-debug") << it->second[i] << " "; Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 ); Trace("model-engine-debug") << r << " "; } Trace("model-engine-debug") << std::endl; - Trace("model-engine-debug") << " Model basis term : " << mbt << std::endl; + Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); + Trace("model-engine-debug") << " Basis term : " << mbt << std::endl; } } } @@ -200,6 +204,7 @@ int ModelEngine::checkModel(){ for( int i=0; igetNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); bool isAx = getTermDatabase()->isQAttrAxiom( f ); + Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl; //determine if we should check this quantifier if( ( ( effort==1 && ( options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT || isAx ) ) || ( effort==0 && !isAx ) ) && mb->isQuantifierActive( f ) ){ exhaustiveInstantiate( f, e ); @@ -214,7 +219,7 @@ int ModelEngine::checkModel(){ break; } }else{ - Trace("inst-fmf-ei") << "-> Inactive : " << f << std::endl; + Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl; } } } @@ -240,43 +245,46 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ mb->d_addedLemmas = 0; mb->d_incomplete_check = false; if( mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){ - Trace("inst-fmf-ei") << "-> Builder determined instantiation(s)." << std::endl; + Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl; d_triedLemmas += mb->d_triedLemmas; d_addedLemmas += mb->d_addedLemmas; d_incomplete_check = d_incomplete_check || mb->d_incomplete_check; d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas; }else{ - Trace("inst-fmf-ei") << "-> Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl; - Debug("inst-fmf-ei") << " Instantiation Constants: "; + Trace("fmf-exh-inst-debug") << " Instantiation Constants: "; for( size_t i=0; igetTermDatabase()->getInstantiationConstant( f, i ) << " "; + Trace("fmf-exh-inst-debug") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " "; } - Debug("inst-fmf-ei") << std::endl; + Trace("fmf-exh-inst-debug") << std::endl; //create a rep set iterator and iterate over the (relevant) domain of the quantifier RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) ); if( riter.setQuantifier( f ) ){ - Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl; - int triedLemmas = 0; - int addedLemmas = 0; - while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ - //instantiation was not shown to be true, construct the match - InstMatch m( f ); - for( int i=0; iaddInstantiation( f, m ) ){ - addedLemmas++; - }else{ - Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl; + Trace("fmf-exh-inst") << "...exhaustive instantiation incomplete=" << riter.d_incomplete << "..." << std::endl; + if( !riter.d_incomplete || options::fmfFullSaturate() ){ + int triedLemmas = 0; + int addedLemmas = 0; + while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ + //instantiation was not shown to be true, construct the match + InstMatch m( f ); + for( int i=0; iaddInstantiation( f, m ) ){ + addedLemmas++; + }else{ + Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl; + } + riter.increment(); } - riter.increment(); + d_addedLemmas += addedLemmas; + d_triedLemmas += triedLemmas; + d_statistics.d_exh_inst_lemmas += addedLemmas; } - d_addedLemmas += addedLemmas; - d_triedLemmas += triedLemmas; - d_statistics.d_exh_inst_lemmas += addedLemmas; + }else{ + Assert( riter.d_incomplete ); } //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round d_incomplete_check = d_incomplete_check || riter.d_incomplete; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index fe81df7f8..2af66e60a 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -137,8 +137,10 @@ option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false option fmfInstEngine --fmf-inst-engine bool :default false use instantiation engine in conjunction with finite model finding +option fmfFullSaturate --fmf-full-saturate bool :default false + instantiate with all known ground terms for infinite domain quantifiers when finite model finding option fmfInstGen --fmf-inst-gen bool :default true - disable Inst-Gen instantiation techniques for finite model finding + disable Inst-Gen instantiation techniques for finite model finding option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false only perform Inst-Gen instantiation techniques on one quantifier per round option fmfFreshDistConst --fmf-fresh-dc bool :default false diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index ca24de5f7..5e0f511e0 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -110,8 +110,6 @@ public: virtual eq::EqualityEngine* getEngine() = 0; /** get the equivalence class of a */ virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0; - - virtual void setLiberal( bool l ) = 0; };/* class EqualityQuery */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 2671f616b..20d622122 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -409,7 +409,7 @@ bool TermDb::isInstClosure( Node r ) { return d_iclosure_processed.find( r )!=d_iclosure_processed.end(); } -//checks whether a type is reasonably small enough such that all of its domain elements can be enumerated +//checks whether a type is not Array and is reasonably small enough (<1000) such that all of its domain elements can be enumerated bool TermDb::mayComplete( TypeNode tn ) { std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn ); if( it==d_may_complete.end() ){ @@ -1756,13 +1756,13 @@ Node TermDbSygus::getNormalized( TypeNode t, Node prog, bool do_pre_norm, bool d } } -int TermDbSygus::getTermSize( Node n ){ +int TermDbSygus::getSygusTermSize( Node n ){ if( isVar( n ) ){ return 0; }else{ int sum = 0; for( unsigned i=0; i& var_count, std::map< Node, Node >& subs ); Node getNormalized( TypeNode t, Node prog, bool do_pre_norm = false, bool do_post_norm = true ); - int getTermSize( Node n ); + int getSygusTermSize( Node n ); /** given a term, construct an equivalent smaller one that respects syntax */ Node minimizeBuiltinTerm( Node n ); /** given a term, expand it into more basic components */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index e654a689d..2d9ba5713 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -99,7 +99,7 @@ d_lemmas_produced_c(u){ }else{ d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" ); } - if( !options::finiteModelFind() ){ + if( options::fullSaturateQuant() ){ d_rel_dom = new quantifiers::RelevantDomain( this, d_model ); }else{ d_rel_dom = NULL; @@ -783,12 +783,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo //make it representative, this is helpful for recognizing duplication if( mkRep ){ //pick the best possible representative for instantiation, based on past use and simplicity of term - Node ti = d_eq_query->getInternalRepresentative( terms[i], f, i ); - //check if it is a subtype (can be violated in mixed int/real) FIXME : do this check inside getInternalRepresentative - if( ti.getType().isSubtypeOf( f[0][i].getType() ) ){ - terms[i] = ti; - Trace("inst-add-debug2") << " (" << terms[i] << ")"; - } + terms[i] = d_eq_query->getInternalRepresentative( terms[i], f, i ); } } Trace("inst-add-debug") << std::endl; @@ -1070,16 +1065,12 @@ bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){ return true; }else{ eq::EqualityEngine* ee = getEngine(); - if( d_liberal ){ - return true;//!areDisequal( a, b ); - }else{ - if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ - if( ee->areEqual( a, b ) ){ - return true; - } + if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ + if( ee->areEqual( a, b ) ){ + return true; } - return false; } + return false; } } @@ -1094,6 +1085,7 @@ bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){ } Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){ + Assert( f.isNull() || f.getKind()==FORALL ); Node r = getRepresentative( a ); if( !options::internalReps() ){ return r; @@ -1108,16 +1100,17 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, r = getRepresentative( r ); }else{ if( r.getType().isSort() ){ - //TODO : this can happen in rare cases - // say x:(Array Int U), select( x, 0 ), x assigned (const @u1). Trace("internal-rep-warn") << "No representative for UF constant." << std::endl; + //should never happen : UF constants should never escape model + Assert( false ); } } } } } - std::map< Node, Node >::iterator itir = d_int_rep.find( r ); - if( itir==d_int_rep.end() ){ + 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() ){ @@ -1134,8 +1127,9 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, } Trace("internal-rep-select") << " } " << std::endl; int r_best_score = -1; + TypeNode v_tn = f[0][index].getType(); for( size_t i=0; i=0 && ( r_best_score<0 || scoregetTermDatabase()->getInstantiationConstant( f, index ); - r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); - }else{ - r_best = a; - } + 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::hash_map cache; @@ -1159,7 +1149,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, d_rep_score[ r_best ] = d_reset_count; } Trace("internal-rep-select") << "...Choose " << r_best << std::endl; - d_int_rep[r] = r_best; + 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; @@ -1181,8 +1171,10 @@ void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, } } Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl; - for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){ - Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << 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; @@ -1190,51 +1182,55 @@ void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, bool success; do { success = false; - for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.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; jsecond << " to subterm " << ni[j] << std::endl; - d_int_rep[it->first] = ni[j]; + 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; jsecond.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; - success = true; break; - }else{ - Node ir = d_int_rep[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; - d_int_rep[it->first] = n; - temp_rep_map[n] = it->first; + 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< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){ - Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << 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; + } } } @@ -1277,6 +1273,7 @@ Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Nod } } +/* int getDepth( Node n ){ if( n.getNumChildren()==0 ){ return 0; @@ -1291,10 +1288,13 @@ int getDepth( Node n ){ return maxDepth; } } +*/ -//smaller the score, the better -int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){ - if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){ +//-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; diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index d5887f907..c9f14b2c4 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -337,20 +337,18 @@ private: /** pointer to theory engine */ QuantifiersEngine* d_qe; /** internal representatives */ - std::map< Node, Node > d_int_rep; + std::map< TypeNode, std::map< Node, Node > > d_int_rep; /** rep score */ std::map< Node, int > d_rep_score; /** reset count */ int d_reset_count; - - bool d_liberal; private: /** node contains */ Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map& cache ); /** get score */ - int getRepScore( Node n, Node f, int index ); + int getRepScore( Node n, Node f, int index, TypeNode v_tn ); public: - EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ), d_liberal( false ){} + EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ){} ~EqualityQueryQuantifiersEngine(){} /** reset */ void reset(); @@ -368,8 +366,6 @@ public: Node getInternalRepresentative( Node a, Node f, int index ); /** flatten representatives */ void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ); - - void setLiberal( bool l ) { d_liberal = l; } }; /* EqualityQueryQuantifiersEngine */ }/* CVC4::theory namespace */ diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index eb05564e5..6a64f762e 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -16,6 +16,7 @@ #include "theory/type_enumerator.h" #include "theory/quantifiers/bounded_integers.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/first_order_model.h" using namespace std; using namespace CVC4; @@ -187,8 +188,14 @@ bool RepSetIterator::initialize(){ TypeNode tn = d_types[i]; Trace("rsi") << "Var #" << i << " is type " << tn << "..." << std::endl; if( tn.isSort() ){ + //must ensure uninterpreted type is non-empty. if( !d_rep_set->hasType( tn ) ){ - Node var = NodeManager::currentNM()->mkSkolem( "repSet", tn, "is a variable created by the RepSetIterator" ); + //FIXME: + // terms in rep_set are now constants which mapped to terms through TheoryModel + // thus, should introduce a constant and a term. for now, just a term. + + //Node c = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 ); + Node var = d_qe->getModel()->getSomeDomainElement( tn ); Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl; d_rep_set->add( tn, var ); } @@ -216,15 +223,18 @@ bool RepSetIterator::initialize(){ d_incomplete = true; } } - //enumerate if the sort is reasonably small, not an Array, the upper bound of 1000 is chosen arbitrarily for now + //enumerate if the sort is reasonably small }else if( d_qe->getTermDatabase()->mayComplete( tn ) ){ Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl; d_rep_set->complete( tn ); + //must have succeeded + Assert( d_rep_set->hasType( tn ) ); }else{ Trace("rsi") << " variable cannot be bounded." << std::endl; Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl; d_incomplete = true; } + //if we have yet to determine the type of enumeration if( d_enum_type.size()<=i ){ d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS ); if( d_rep_set->hasType( tn ) ){ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 52b018234..05d0c896a 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -478,6 +478,14 @@ void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cac cache.insert(n); } +void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, std::map& constantReps, Node eqc, Node const_rep, bool fullModel ) { + constantReps[eqc] = const_rep; + Trace("model-builder") << " Assign: Setting constant rep of " << eqc << " to " << const_rep << endl; + if( !fullModel ){ + tm->d_rep_set.d_values_to_terms[const_rep] = eqc; + } +} + void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) { @@ -551,7 +559,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) if (!const_rep.isNull()) { // Theories should not specify a rep if there is already a constant in the EC Assert(rep.isNull() || rep == const_rep); - constantReps[eqc] = const_rep; + assignConstantRep( tm, constantReps, eqc, const_rep, fullModel ); typeConstSet.add(eqct.getBaseType(), const_rep); } else if (!rep.isNull()) { @@ -615,7 +623,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) Node normalized = normalize(tm, n, constantReps, true); if (normalized.isConst()) { typeConstSet.add(tb, normalized); - constantReps[*i2] = normalized; + assignConstantRep( tm, constantReps, *i2, normalized, fullModel ); Trace("model-builder") << " Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl; changed = true; evaluated = true; @@ -648,7 +656,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) if (normalized.isConst()) { changed = true; typeConstSet.add(tb, normalized); - constantReps[*i] = normalized; + assignConstantRep( tm, constantReps, *i, normalized, fullModel ); assertedReps.erase(*i); i2 = i; ++i; @@ -727,11 +735,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) n = *te; } Assert(!n.isNull()); - constantReps[*i2] = n; - Trace("model-builder") << " Assign: Setting constant rep of " << (*i2) << " to " << n << endl; - if( !fullModel ){ - tm->d_rep_set.d_values_to_terms[n] = (*i2); - } + assignConstantRep( tm, constantReps, *i2, n, fullModel ); changed = true; noRepSet.erase(i2); if (assignOne) { diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index be202fb69..a161f02f4 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -261,7 +261,7 @@ protected: Node normalize(TheoryModel* m, TNode r, std::map& constantReps, bool evalOnly); bool isAssignable(TNode n); void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache); - + void assignConstantRep( TheoryModel* tm, std::map& constantReps, Node eqc, Node const_rep, bool fullModel ); public: TheoryEngineModelBuilder(TheoryEngine* te); virtual ~TheoryEngineModelBuilder(){} diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index 9aef059bd..c88d9adff 100644 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -296,7 +296,7 @@ void SortInference::setEqual( int t1, int t2 ){ d_type_types[rt2] = it1->second; d_type_types.erase( rt1 ); }else{ - //may happen for mixed int/real + Trace("sort-inference-debug") << "...fail : associated with types " << d_type_types[rt1] << " and " << d_type_types[rt2] << std::endl; return; } } @@ -361,14 +361,25 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){ int retType; if( n.getKind()==kind::EQUAL ){ - //we only require that the left and right hand side must be equal - setEqual( child_types[0], child_types[1] ); + Trace("sort-inference-debug") << "For equality " << n << ", set equal types from : " << n[0].getType() << " " << n[1].getType() << std::endl; + //if original types are mixed (e.g. Int/Real), don't commit type equality in either direction + if( n[0].getType()!=n[1].getType() ){ + //for now, assume the original types + for( unsigned i=0; i<2; i++ ){ + int ct = getIdForType( n[i].getType() ); + setEqual( child_types[i], ct ); + } + }else{ + //we only require that the left and right hand side must be equal + setEqual( child_types[0], child_types[1] ); + } //int eqType = getIdForType( n[0].getType() ); //setEqual( child_types[0], eqType ); //setEqual( child_types[1], eqType ); retType = getIdForType( n.getType() ); }else if( n.getKind()==kind::APPLY_UF ){ Node op = n.getOperator(); + TypeNode tn_op = op.getType(); if( d_op_return_types.find( op )==d_op_return_types.end() ){ if( n.getType().isBoolean() ){ //use booleans @@ -387,7 +398,17 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){ } for( size_t i=0; i