diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-24 09:37:13 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-24 09:37:32 -0500 |
commit | 67ea40d24cbbcd3f490248754a6abc1989bacc7b (patch) | |
tree | f74d7a52a5046e346035b1c5b5abec1f17004033 /src/theory/quantifiers/ambqi_builder.cpp | |
parent | 2c1e5b35ba688c0df297b0510058454c54bab54d (diff) |
Refactor model building for quantifiers to be a single pass, simplification. Modify datatypes collect model info to include dt equivalence classes. Further work on sygus. Other minor fixes.
Diffstat (limited to 'src/theory/quantifiers/ambqi_builder.cpp')
-rw-r--r-- | src/theory/quantifiers/ambqi_builder.cpp | 183 |
1 files changed, 90 insertions, 93 deletions
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index 2ccc17e55..de55ecdba 100644 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -586,7 +586,7 @@ bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, // exit( 10 ); //} return true; - }else if( varChCount==1 && n.getKind()==EQUAL ){ + }else if( varChCount==1 && ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) ){ Trace("ambqi-check-debug2") << "Expand variable child..." << std::endl; //expand the variable based on its finite domain AbsDef a; @@ -598,7 +598,7 @@ bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, Trace("ambqi-check-debug2") << "Construct compose with variable..." << std::endl; construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def ); return true; - }else if( varChCount==2 && n.getKind()==EQUAL ){ + }else if( varChCount==2 && ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) ){ Trace("ambqi-check-debug2") << "Construct variable equality..." << std::endl; //efficient expansion of the equality construct_var_eq( m, q, vchildren[0], vchildren[1], val_none, val_none ); @@ -721,115 +721,112 @@ QModelBuilder( c, qe ){ //------------------------model construction---------------------------- -void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) { - Trace("ambqi-debug") << "process build model " << fullModel << std::endl; +bool AbsMbqiBuilder::processBuildModel(TheoryModel* m) { + Trace("ambqi-debug") << "process build model " << std::endl; FirstOrderModel* f = (FirstOrderModel*)m; FirstOrderModelAbs* fm = f->asFirstOrderModelAbs(); - if( fullModel ){ - Trace("ambqi-model") << "Construct model representation..." << std::endl; - //make function values - for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { - if( it->first.getType().getNumChildren()>1 ){ - Trace("ambqi-model") << "Construct for " << it->first << "..." << std::endl; - m->d_uf_models[ it->first ] = fm->getFunctionValue( it->first, "$x" ); - } - } - TheoryEngineModelBuilder::processBuildModel( m, fullModel ); - //mark that the model has been set - fm->markModelSet(); - //debug the model - debugModel( fm ); - }else{ - fm->initialize(); - //process representatives - fm->d_rep_id.clear(); - fm->d_domain.clear(); - - //initialize boolean sort - TypeNode b = d_true.getType(); - fm->d_rep_set.d_type_reps[b].clear(); - fm->d_rep_set.d_type_reps[b].push_back( d_false ); - fm->d_rep_set.d_type_reps[b].push_back( d_true ); - fm->d_rep_id[d_false] = 0; - fm->d_rep_id[d_true] = 1; - - //initialize unintpreted sorts - Trace("ambqi-model") << std::endl << "Making representatives..." << std::endl; - for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); - it != fm->d_rep_set.d_type_reps.end(); ++it ){ - if( it->first.isSort() ){ - Assert( !it->second.empty() ); - //set the domain - fm->d_domain[it->first] = 0; - Trace("ambqi-model") << "Representatives for " << it->first << " : " << std::endl; - for( unsigned i=0; i<it->second.size(); i++ ){ - if( i<32 ){ - fm->d_domain[it->first] |= ( 1 << i ); - } - Trace("ambqi-model") << i << " : " << it->second[i] << std::endl; - fm->d_rep_id[it->second[i]] = i; - } - if( it->second.size()>=32 ){ - fm->d_domain.erase( it->first ); + fm->initialize(); + //process representatives + fm->d_rep_id.clear(); + fm->d_domain.clear(); + + //initialize boolean sort + TypeNode b = d_true.getType(); + fm->d_rep_set.d_type_reps[b].clear(); + fm->d_rep_set.d_type_reps[b].push_back( d_false ); + fm->d_rep_set.d_type_reps[b].push_back( d_true ); + fm->d_rep_id[d_false] = 0; + fm->d_rep_id[d_true] = 1; + + //initialize unintpreted sorts + Trace("ambqi-model") << std::endl << "Making representatives..." << std::endl; + for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); + it != fm->d_rep_set.d_type_reps.end(); ++it ){ + if( it->first.isSort() ){ + Assert( !it->second.empty() ); + //set the domain + fm->d_domain[it->first] = 0; + Trace("ambqi-model") << "Representatives for " << it->first << " : " << std::endl; + for( unsigned i=0; i<it->second.size(); i++ ){ + if( i<32 ){ + fm->d_domain[it->first] |= ( 1 << i ); } + Trace("ambqi-model") << i << " : " << it->second[i] << std::endl; + fm->d_rep_id[it->second[i]] = i; + } + if( it->second.size()>=32 ){ + fm->d_domain.erase( it->first ); } } + } - Trace("ambqi-model") << std::endl << "Making function definitions..." << std::endl; - //construct the models for functions - for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { - Node f = it->first; - Trace("ambqi-model-debug") << "Building Model for " << f << std::endl; - //reset the model - it->second->clear(); - //get all (non-redundant) f-applications - std::vector< TNode > fapps; - Trace("ambqi-model-debug") << "Initial terms: " << std::endl; - for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){ - Node n = fm->d_uf_terms[f][i]; + Trace("ambqi-model") << std::endl << "Making function definitions..." << std::endl; + //construct the models for functions + for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { + Node f = it->first; + Trace("ambqi-model-debug") << "Building Model for " << f << std::endl; + //reset the model + it->second->clear(); + //get all (non-redundant) f-applications + std::vector< TNode > fapps; + Trace("ambqi-model-debug") << "Initial terms: " << std::endl; + std::map< Node, std::vector< Node > >::iterator itut = fm->d_uf_terms.find( f ); + if( itut!=fm->d_uf_terms.end() ){ + for( size_t i=0; i<itut->second.size(); i++ ){ + Node n = itut->second[i]; if( d_qe->getTermDatabase()->isTermActive( n ) ){ Trace("ambqi-model-debug") << " " << n << " -> " << fm->getRepresentativeId( n ) << std::endl; fapps.push_back( n ); } } - if( fapps.empty() ){ - //choose arbitrary value - Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f); - Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl; - fapps.push_back( mbt ); - } - bool fValid = true; - for( unsigned i=0; i<fapps[0].getNumChildren(); i++ ){ - if( fm->d_domain.find( fapps[0][i].getType() )==fm->d_domain.end() ){ - Trace("ambqi-model") << "Interpretation of " << f << " is not valid."; - Trace("ambqi-model") << " (domain for " << fapps[0][i].getType() << " is too large)." << std::endl; - fValid = false; - break; - } + } + if( fapps.empty() ){ + //choose arbitrary value + Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f); + Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl; + fapps.push_back( mbt ); + } + bool fValid = true; + for( unsigned i=0; i<fapps[0].getNumChildren(); i++ ){ + if( fm->d_domain.find( fapps[0][i].getType() )==fm->d_domain.end() ){ + Trace("ambqi-model") << "Interpretation of " << f << " is not valid."; + Trace("ambqi-model") << " (domain for " << fapps[0][i].getType() << " is too large)." << std::endl; + fValid = false; + break; } - fm->d_models_valid[f] = fValid; - if( fValid ){ - //construct the ambqi model - it->second->construct_func( fm, fapps ); - Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl; - it->second->debugPrint("ambqi-model-debug", fm, fapps[0] ); - Trace("ambqi-model-debug") << "Simplifying " << f << "..." << std::endl; - it->second->simplify( fm, TNode::null(), fapps[0] ); - Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl; - it->second->debugPrint("ambqi-model", fm, fapps[0] ); + } + fm->d_models_valid[f] = fValid; + if( fValid ){ + //construct the ambqi model + it->second->construct_func( fm, fapps ); + Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl; + it->second->debugPrint("ambqi-model-debug", fm, fapps[0] ); + Trace("ambqi-model-debug") << "Simplifying " << f << "..." << std::endl; + it->second->simplify( fm, TNode::null(), fapps[0] ); + Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl; + it->second->debugPrint("ambqi-model", fm, fapps[0] ); /* - if( Debug.isOn("ambqi-model-debug") ){ - for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){ - Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] ); - Debug("ambqi-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl; - Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) ); - } + if( Debug.isOn("ambqi-model-debug") ){ + for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){ + Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] ); + Debug("ambqi-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl; + Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) ); } -*/ } +*/ + } + } + Trace("ambqi-model") << "Construct model representation..." << std::endl; + //make function values + for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { + if( it->first.getType().getNumChildren()>1 ){ + Trace("ambqi-model") << "Construct for " << it->first << "..." << std::endl; + m->d_uf_models[ it->first ] = fm->getFunctionValue( it->first, "$x" ); } } + Assert( d_addedLemmas==0 ); + return TheoryEngineModelBuilder::processBuildModel( m ); } |