diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-09-13 20:39:13 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-09-13 20:39:13 +0000 |
commit | 01dfa806851502267e1032483fec48e8b4373634 (patch) | |
tree | 8103a5a5a763fecfc42793bf5c3c88290bff775b /src/theory/model.cpp | |
parent | dce6be13f8eb90006c7ceb8d43a8a78da23ca838 (diff) |
ensure that get-value and get-model are consistent, rewrite function value bodies, do not dag-ify model output
Diffstat (limited to 'src/theory/model.cpp')
-rw-r--r-- | src/theory/model.cpp | 79 |
1 files changed, 55 insertions, 24 deletions
diff --git a/src/theory/model.cpp b/src/theory/model.cpp index ee61c9345..62327e4dc 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -118,7 +118,7 @@ Node TheoryModel::getModelValue( TNode n ){ } //evaluate the children for( int i=0; i<(int)n.getNumChildren(); i++ ){ - Node val = getModelValue( n[i] ); + Node val = getValue( n[i] ); Debug("model-debug") << i << " : " << n[i] << " -> " << val << std::endl; Assert( !val.isNull() ); children.push_back( val ); @@ -216,6 +216,13 @@ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ } } +/** add term */ +void TheoryModel::addTerm( Node n ){ + if( !d_equalityEngine.hasTerm( n ) ){ + d_equalityEngine.addTerm( n ); + } +} + /** assert equality */ void TheoryModel::assertEquality( Node a, Node b, bool polarity ){ d_equalityEngine.assertEquality( a.eqNode(b), polarity, Node::null() ); @@ -331,6 +338,7 @@ TheoryModel( c, name ), d_enableFuncModels( enableFuncModels ){ } void DefaultModel::addTerm( Node n ){ + TheoryModel::addTerm( n ); //must collect UF terms if( d_enableFuncModels && n.getKind()==APPLY_UF ){ Node op = n.getOperator(); @@ -347,11 +355,14 @@ void DefaultModel::reset(){ } Node DefaultModel::getInterpretedValue( TNode n ){ + Trace("model") << "Get interpreted value of " << n << std::endl; TypeNode type = n.getType(); if( type.isFunction() || type.isPredicate() ){ //for function models if( d_enableFuncModels ){ + //create the function value for the model if( d_uf_models.find( n )==d_uf_models.end() ){ + Trace("model") << "Creating function value..." << std::endl; uf::UfModelTree ufmt( n ); Node default_v; for( size_t i=0; i<d_uf_terms[n].size(); i++ ){ @@ -368,42 +379,62 @@ Node DefaultModel::getInterpretedValue( TNode n ){ ufmt.simplify(); d_uf_models[n] = ufmt.getFunctionValue( "$x" ); } + Trace("model") << "Return function value." << std::endl; return d_uf_models[n]; }else{ return n; } }else{ - Trace("model") << "Get interpreted value of " << n << std::endl; + Node ret; //add term to equality engine, this will enforce a value if it exists - d_equalityEngine.addTerm( n ); - //first, see if the representative is defined + // for example, if a = b = c1, and f( a ) = c2, then adding f( b ) should force + // f( b ) to be equal to c2. + addTerm( n ); + //check if the representative is defined n = d_equalityEngine.getRepresentative( n ); - //this check is required since d_equalityEngine.hasTerm( n ) - // does not ensure that n is in an equivalence class in d_equalityEngine if( d_reps.find( n )!=d_reps.end() ){ + Trace("model") << "Return value in equality engine."<< std::endl; return d_reps[n]; } - //second, try to choose an existing term as value - Trace("model") << "Choose existing value..." << std::endl; - std::vector< Node > v_emp; - Node n2 = getDomainValue( type, v_emp ); - if( !n2.isNull() ){ - //store the equality?? this is dangerous since it may cause representatives to change - //assertEquality( n, n2, true ); - return n2; - }else{ - //otherwise, choose new value - Trace("model") << "Choose new value..." << std::endl; - n2 = getNewDomainValue( type ); - if( !n2.isNull() ){ - //store the equality?? - //assertEquality( n, n2, true ); - return n2; + //if it is APPLY_UF, we must consult the corresponding function if it exists + if( n.getKind()==APPLY_UF ){ + Node op = n.getOperator(); + if( d_uf_models.find( op )!=d_uf_models.end() ){ + std::vector< Node > lam_children; + lam_children.push_back( d_uf_models[ op ] ); + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + lam_children.push_back( n[i] ); + } + Node app_lam = NodeManager::currentNM()->mkNode( APPLY_UF, lam_children ); + ret = Rewriter::rewrite( app_lam ); + Trace("model") << "Consult UF model." << std::endl; + } + } + if( ret.isNull() ){ + //second, try to choose an existing term as value + std::vector< Node > v_emp; + ret = getDomainValue( type, v_emp ); + if( !ret.isNull() ){ + Trace("model") << "Choose existing value." << std::endl; }else{ - //otherwise, just return itself (this usually should not happen) - return n; + //otherwise, choose new value + ret = getNewDomainValue( type ); + if( !ret.isNull() ){ + Trace("model") << "Choose new value." << std::endl; + } } } + if( !ret.isNull() ){ + //store the equality + assertEquality( n, ret, true ); + //this is dangerous since it may cause representatives to change + Assert( getRepresentative( ret )==ret ); + return ret; + }else{ + //otherwise, just return itself (this usually should not happen) + Trace("model") << "Return self." << std::endl; + return n; + } } } |