}
//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 );
}
}
+/** 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() );
}
void DefaultModel::addTerm( Node n ){
+ TheoryModel::addTerm( n );
//must collect UF terms
if( d_enableFuncModels && n.getKind()==APPLY_UF ){
Node op = n.getOperator();
}
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++ ){
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;
+ }
}
}
{
friend class TheoryEngineModelBuilder;
protected:
- /** add term function
- * This should be called on all terms that exist in the model.
- * addTerm( n ) will do any model-specific processing necessary for n,
- * such as contraining the interpretation of uninterpretted functions.
- */
- virtual void addTerm( Node n ) {}
/** substitution map for this model */
SubstitutionMap d_substitutions;
public:
public:
/** Adds a substitution from x to t. */
void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
+ /** add term function
+ * addTerm( n ) will do any model-specific processing necessary for n,
+ * such as contraining the interpretation of uninterpretted functions,
+ * and adding n to the equality engine of this model
+ */
+ virtual void addTerm( Node n );
/** assert equality holds in the model */
void assertEquality( Node a, Node b, bool polarity );
/** assert predicate holds in the model */
}
Node FirstOrderModel::getInterpretedValue( TNode n ){
- Debug("fo-model") << "get interpreted value " << n << std::endl;
+ Trace("fo-model") << "get interpreted value " << n << std::endl;
TypeNode type = n.getType();
if( type.isFunction() || type.isPredicate() ){
if( d_uf_model_tree.find( n )!=d_uf_model_tree.end() ){
if( d_uf_models.find( n )==d_uf_models.end() ){
- //use the model tree to generate the model
d_uf_models[n] = d_uf_model_tree[n].getFunctionValue( "$x" );
}
- return d_uf_models[n];
}
- /*
- }else if( type.isArray() ){
- if( d_array_model.find( n )!=d_array_model.end() ){
- return d_array_model[n].getArrayValue();
- }else{
- //std::cout << "no array model generated for " << n << std::endl;
- }
- */
- }else if( n.getKind()==APPLY_UF ){
- Node op = n.getOperator();
- if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){
- //consult the uf model
- int depIndex;
- return d_uf_model_tree[ op ].getValue( this, n, depIndex );
- }
- }else if( n.getKind()==SELECT ){
-
}
return DefaultModel::getInterpretedValue( n );
}
if( !n.hasAttribute(InstConstantAttribute()) ){
//if evaluating a ground term, just consult the standard getValue functionality
depIndex = -1;
- return getModelValue( n );
+ return getValue( n );
}else{
Node val;
depIndex = ri->getNumTerms()-1;
projects / cvc5.git / commitdiff