diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-08 15:49:14 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-08 15:50:20 -0600 |
commit | 2dd6292b73e4e19be2e261c7fe5664bd2b0149bd (patch) | |
tree | 0f4956ec068972da8c8d1c708df7c8b2f7a07f3a /src/theory/quantifiers | |
parent | 3c4c4420ebae4d27d53084453591363942eb4d2e (diff) |
Updates related to finite model finding and (co)datatypes. Bug fix enumerator and codatatype rewriter, further simplify fmc.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 24 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 125 | ||||
-rw-r--r-- | src/theory/quantifiers/full_model_check.h | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 10 |
6 files changed, 96 insertions, 84 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index cc0b18ffe..345a5eaef 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -463,9 +463,13 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { lem = Rewriter::rewrite( lem ); Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem << std::endl; Trace("cegqi-engine") << " ...refine candidate." << std::endl; - d_quantEngine->addLemma( lem ); - ++(d_statistics.d_cegqi_lemmas_refine); - conj->d_refine_count++; + bool res = d_quantEngine->addLemma( lem ); + if( res ){ + ++(d_statistics.d_cegqi_lemmas_refine); + conj->d_refine_count++; + }else{ + Trace("cegqi-engine") << " ...FAILED to add refinement!" << std::endl; + } } } conj->d_ce_sk.clear(); diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index aa2a43fbf..272f16be8 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -90,15 +90,19 @@ void FirstOrderModel::initialize() { } processInitializeQuantifier( f ); //initialize relevant models within bodies of all quantifiers - initializeModelForTerm( f[1] ); + std::map< Node, bool > visited; + initializeModelForTerm( f[1], visited ); } processInitialize( false ); } -void FirstOrderModel::initializeModelForTerm( Node n ){ - processInitializeModelForTerm( n ); - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - initializeModelForTerm( n[i] ); +void FirstOrderModel::initializeModelForTerm( Node n, std::map< Node, bool >& visited ){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + processInitializeModelForTerm( n ); + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + initializeModelForTerm( n[i], visited ); + } } } @@ -574,15 +578,6 @@ Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) { Trace("fmc-warn") << "WARNING : no representative for " << n << std::endl; } } -/* - Node r = getRepresentative(n); - if( d_model_basis_rep.find(tn)!=d_model_basis_rep.end() ){ - if (r==d_model_basis_rep[tn]) { - r = d_qe->getTermDatabase()->getModelBasisTerm(tn); - } - } - return r; -*/ return getRepresentative(n); } } @@ -609,7 +604,6 @@ void FirstOrderModelFmc::processInitialize( bool ispre ) { for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){ it->second->reset(); } - d_model_basis_rep.clear(); } } diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index a31e85d7e..d42eb61e3 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -67,7 +67,7 @@ public: //for Theory Quantifiers: /** get number to reduce quantifiers */ unsigned getNumToReduceQuantifiers() { return d_forall_to_reduce.size(); } /** initialize model for term */ - void initializeModelForTerm( Node n ); + void initializeModelForTerm( Node n, std::map< Node, bool >& visited ); virtual void processInitializeModelForTerm( Node n ) = 0; virtual void processInitializeQuantifier( Node q ) {} public: @@ -169,7 +169,6 @@ class FirstOrderModelFmc : public FirstOrderModel private: /** models for UF */ std::map<Node, Def * > d_models; - std::map<TypeNode, Node > d_model_basis_rep; std::map<TypeNode, Node > d_type_star; Node intervalOp; Node getUsedRepresentative(Node n, bool strict = false); diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index f0858f4e9..00a5241f5 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -325,11 +325,46 @@ QModelBuilder( c, qe ){ d_false = NodeManager::currentNM()->mkConst(false); } +void FullModelChecker::preProcessBuildModel(TheoryModel* m, bool fullModel) { + FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc(); + if( !fullModel ){ + Trace("fmc") << "---Full Model Check preprocess() " << std::endl; + d_preinitialized_types.clear(); + //traverse equality engine + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine ); + std::map< TypeNode, int > typ_num; + while( !eqcs_i.isFinished() ){ + TypeNode tr = (*eqcs_i).getType(); + d_preinitialized_types[tr] = true; + ++eqcs_i; + } + + //must ensure model basis terms exists in model for each relevant type + fm->initialize(); + for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { + Node op = it->first; + TypeNode tno = op.getType(); + for( unsigned i=0; i<tno.getNumChildren(); i++) { + preInitializeType( fm, tno[i] ); + } + } + //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts + if( !options::fmfEmptySorts() ){ + for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node q = fm->getAssertedQuantifier( i ); + //make sure all types are set + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + preInitializeType( fm, q[0][i].getType() ); + } + } + } + } +} + void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc(); if( !fullModel ){ Trace("fmc") << "---Full Model Check reset() " << std::endl; - fm->initialize(); d_quant_models.clear(); d_rep_ids.clear(); d_star_insts.clear(); @@ -338,50 +373,26 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ it != fm->d_rep_set.d_type_reps.end(); ++it ){ if( it->first.isSort() ){ Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; - Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first); - Node rmbt = fm->getUsedRepresentative( mbt); - int mbt_index = -1; - Trace("fmc") << " Model basis term : " << mbt << std::endl; for( size_t a=0; a<it->second.size(); a++ ){ Node r = fm->getUsedRepresentative( it->second[a] ); - std::vector< Node > eqc; - ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc ); - Trace("fmc-model-debug") << " " << (it->second[a]==r) << (r==mbt); - Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : "; - //Trace("fmc-model-debug") << r2 << " : " << ir << " : "; - Trace("fmc-model-debug") << " {"; - //find best selection for representative - for( size_t i=0; i<eqc.size(); i++ ){ - Trace("fmc-model-debug") << eqc[i] << ", "; - } - Trace("fmc-model-debug") << "}" << std::endl; - - //if this is the model basis eqc, replace with actual model basis term - if (r==rmbt || (mbt_index==-1 && a==(it->second.size()-1))) { - fm->d_model_basis_rep[it->first] = r; - r = mbt; - mbt_index = a; + if( Trace.isOn("fmc-model-debug") ){ + std::vector< Node > eqc; + ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc ); + Trace("fmc-model-debug") << " " << (it->second[a]==r); + Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : "; + //Trace("fmc-model-debug") << r2 << " : " << ir << " : "; + Trace("fmc-model-debug") << " {"; + for( size_t i=0; i<eqc.size(); i++ ){ + Trace("fmc-model-debug") << eqc[i] << ", "; + } + Trace("fmc-model-debug") << "}" << std::endl; } d_rep_ids[it->first][r] = (int)a; } Trace("fmc-model-debug") << std::endl; - - if (mbt_index==-1) { - std::cout << " WARNING: model basis term is not a representative!" << std::endl; - exit(0); - }else{ - Trace("fmc") << "Star index for " << it->first << " is " << mbt_index << std::endl; - } - } - } - //also process non-rep set sorts - for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { - Node op = it->first; - TypeNode tno = op.getType(); - for( unsigned i=0; i<tno.getNumChildren(); i++) { - initializeType( fm, tno[i] ); } } + //now, make models for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { Node op = it->first; @@ -433,24 +444,26 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ entry_children.push_back(op); bool hasNonStar = false; for( unsigned i=0; i<c.getNumChildren(); i++) { - Node ri = fm->getUsedRepresentative( c[i]); - if( !ri.getType().isSort() && !ri.isConst() ){ - Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl; - Assert( false ); - } + Node ri = fm->getUsedRepresentative( c[i] ); children.push_back(ri); + bool isStar = false; if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){ if (fm->isModelBasisTerm(ri) ) { ri = fm->getStar( ri.getType() ); + isStar = true; }else{ hasNonStar = true; } } + if( !isStar && !ri.isConst() ){ + Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl; + Assert( false ); + } entry_children.push_back(ri); } Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children ); Node nv = fm->getUsedRepresentative( v ); - if( !nv.getType().isSort() && !nv.isConst() ){ + if( !nv.isConst() ){ Trace("fmc-warn") << "Warning : model has non-constant value in model " << nv << std::endl; Assert( false ); } @@ -523,20 +536,15 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ } } -void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){ - if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){ - Trace("fmc") << "Initialize type " << tn << " hasType = " << fm->d_rep_set.hasType(tn) << std::endl; - Node mbn; - if (!fm->d_rep_set.hasType(tn)) { - mbn = fm->getSomeDomainElement(tn); - }else{ - mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn); +void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ){ + if( d_preinitialized_types.find( tn )==d_preinitialized_types.end() ){ + d_preinitialized_types[tn] = true; + Node mb = d_qe->getTermDatabase()->getModelBasisTerm(tn); + if( !mb.isConst() ){ + Trace("fmc") << "...add model basis term to EE of model " << mb << " " << tn << std::endl; + fm->d_equalityEngine->addTerm( mb ); + fm->addTerm( mb ); } - Trace("fmc") << "Get used rep for " << mbn << std::endl; - Node mbnr = fm->getUsedRepresentative( mbn ); - Trace("fmc") << "...got " << mbnr << std::endl; - fm->d_model_basis_rep[tn] = mbnr; - Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl; } } @@ -591,10 +599,6 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, Node op = NodeManager::currentNM()->mkSkolem( "qfmc", typ, "op created for full-model checking" ); d_quant_cond[f] = op; } - //make sure all types are set - for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ - initializeType( fmfmc, f[0][i].getType() ); - } if( options::mbqiMode()==MBQI_NONE ){ //just exhaustive instantiate @@ -643,6 +647,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, Node ev = d_quant_models[f].evaluate(fmfmc, inst); if (ev==d_true) { addInst = false; + Trace("fmc-debug") << "...do not instantiate, evaluation was " << ev << std::endl; } }else{ //for debugging diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 29913d98d..c7bfcd189 100644 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -92,8 +92,9 @@ protected: std::map<Node, Node > d_quant_cond; std::map< TypeNode, Node > d_array_cond; std::map< Node, Node > d_array_term_cond; - std::map<Node, std::vector< int > > d_star_insts; - void initializeType( FirstOrderModelFmc * fm, TypeNode tn ); + std::map< Node, std::vector< int > > d_star_insts; + std::map< TypeNode, bool > d_preinitialized_types; + void preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ); Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n); bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index); protected: @@ -142,7 +143,8 @@ public: Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ); - /** process build model */ + /** process build model */ + void preProcessBuildModel(TheoryModel* m, bool fullModel); void processBuildModel(TheoryModel* m, bool fullModel); /** get current model value */ Node getCurrentUfModelValue( FirstOrderModelFmc* fm, Node n, std::vector< Node > & args, bool partial ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 6dfd4c737..8bc9689bd 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -971,7 +971,7 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes } ret = NodeManager::currentNM()->mkNode( OR, nret, n_str_ind ); } - Trace("quantifiers-sk") << "mkSkolem body for " << f << " returns : " << ret << std::endl; + Trace("quantifiers-sk-debug") << "mkSkolem body for " << f << " returns : " << ret << std::endl; //if it has an instantiation level, set the skolemized body to that level if( f.hasAttribute(InstLevelAttribute()) ){ theory::QuantifiersEngine::setInstantiationLevelAttr( ret, f.getAttribute(InstLevelAttribute()) ); @@ -1002,6 +1002,14 @@ Node TermDb::getSkolemizedBody( Node f ){ d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], d_skolem_constants[f][i] ); } } + if( Trace.isOn("quantifiers-sk") ){ + Trace("quantifiers-sk") << "Skolemize : "; + for( unsigned i=0; i<d_skolem_constants[f].size(); i++ ){ + Trace("quantifiers-sk") << d_skolem_constants[f][i] << " "; + } + Trace("quantifiers-sk") << "for " << std::endl; + Trace("quantifiers-sk") << " " << f << std::endl; + } } return d_skolem_body[ f ]; } |