From c6d2a808e4981f81e4a638d25582e8542e89b716 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 26 Sep 2012 21:44:22 +0000 Subject: [PATCH] updates to model generation : do not modify equality engine during getValue, other minor changes, still problems with constants not being specified for some eq classes --- src/theory/model.cpp | 254 +++++++++---------- src/theory/model.h | 32 +-- src/theory/quantifiers/first_order_model.cpp | 14 +- src/theory/quantifiers/first_order_model.h | 2 +- src/theory/quantifiers/model_builder.cpp | 5 +- src/theory/theory_engine.cpp | 2 +- src/theory/theory_engine.h | 2 +- src/theory/uf/theory_uf_model.cpp | 7 + src/theory/uf/theory_uf_model.h | 7 +- 9 files changed, 157 insertions(+), 168 deletions(-) diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 8aec39309..96b5d6945 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -28,8 +28,8 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; -TheoryModel::TheoryModel( context::Context* c, std::string name ) : -d_substitutions( c ), d_equalityEngine( c, name ){ +TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFuncModels ) : +d_substitutions( c ), d_equalityEngine( c, name ), d_enableFuncModels( enableFuncModels ){ d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); // The kinds we are treating as function application in congruence @@ -44,6 +44,8 @@ d_substitutions( c ), d_equalityEngine( c, name ){ void TheoryModel::reset(){ d_reps.clear(); d_rep_set.clear(); + d_uf_terms.clear(); + d_uf_models.clear(); } Node TheoryModel::getValue( TNode n ){ @@ -142,6 +144,80 @@ Node TheoryModel::getModelValue( TNode n ){ } } +Node TheoryModel::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 ){ + if( d_uf_models.find( n )!=d_uf_models.end() ){ + //pre-existing function model + Trace("model") << "Return function value." << std::endl; + return d_uf_models[n]; + }else{ + Trace("model") << "Return arbitrary function value." << std::endl; + //otherwise, choose the constant default value + uf::UfModelTree ufmt( n ); + Node default_v = getInterpretedValue( NodeManager::currentNM()->mkSkolem( "defaultValueQueryVar_$$", type.getRangeType(), + "a placeholder variable to query for a default value in model construction" ) ); + ufmt.setDefaultValue( this, default_v ); + return ufmt.getFunctionValue( "$x" ); + } + }else{ + return n; + } + }else{ + Trace("model-debug") << "check rep..." << std::endl; + Node ret; + //check if the representative is defined + n = d_equalityEngine.hasTerm( n ) ? d_equalityEngine.getRepresentative( n ) : n; + Trace("model-debug") << "rep is..." << n << std::endl; + if( d_reps.find( n )!=d_reps.end() ){ + Trace("model") << "Return value in equality engine."<< std::endl; + return d_reps[n]; + } + Trace("model-debug") << "check apply uf models..." << std::endl; + //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; + } + } + Trace("model-debug") << "check existing..." << 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; + } + } + Trace("model-debug") << "check new..." << std::endl; + if( ret.isNull() ){ + //otherwise, choose new value + ret = getNewDomainValue( type ); + if( !ret.isNull() ){ + Trace("model") << "Choose new value." << std::endl; + } + } + if( !ret.isNull() ){ + return ret; + }else{ + //otherwise, just return itself (this usually should not happen) + Trace("model") << "Return self." << std::endl; + return n; + } + } +} + Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){ if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() ){ //try to find a pre-existing arbitrary element @@ -156,7 +232,7 @@ Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){ //FIXME: need to ensure that theory enumerators exist for each sort Node TheoryModel::getNewDomainValue( TypeNode tn ){ -#if 1 +#if 0 if( tn==NodeManager::currentNM()->booleanType() ){ if( d_rep_set.d_type_reps[tn].empty() ){ return d_false; @@ -221,6 +297,14 @@ void TheoryModel::addTerm( Node n ){ if( !d_equalityEngine.hasTerm( n ) ){ d_equalityEngine.addTerm( n ); } + //must collect UF terms + if( d_enableFuncModels && n.getKind()==APPLY_UF ){ + Node op = n.getOperator(); + if( std::find( d_uf_terms[ op ].begin(), d_uf_terms[ op ].end(), n )==d_uf_terms[ op ].end() ){ + d_uf_terms[ op ].push_back( n ); + Trace("model-add-term-uf") << "Add term " << n << std::endl; + } + } } /** assert equality */ @@ -332,120 +416,6 @@ void TheoryModel::printRepresentative( std::ostream& out, Node r ){ } } -DefaultModel::DefaultModel( context::Context* c, std::string name, bool enableFuncModels ) : -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(); - if( std::find( d_uf_terms[ op ].begin(), d_uf_terms[ op ].end(), n )==d_uf_terms[ op ].end() ){ - d_uf_terms[ op ].push_back( n ); - } - } -} - -void DefaultModel::reset(){ - d_uf_terms.clear(); - d_uf_models.clear(); - TheoryModel::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; imkSkolem( "defaultValue_$$", type.getRangeType(), "a default value term from model construction" ) ); - } - ufmt.setDefaultValue( this, default_v ); - 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{ - Node ret; - //add term to equality engine, this will enforce a value if it exists - // 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 ); - if( d_reps.find( n )!=d_reps.end() ){ - Trace("model") << "Return value in equality engine."<< std::endl; - return d_reps[n]; - } - //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, choose new value - ret = getNewDomainValue( type ); - if( !ret.isNull() ){ - Trace("model") << "Choose new value." << std::endl; - } - } - } - if( !ret.isNull() ){ - Node prev = n; - //store the equality - assertEquality( n, ret, true ); - //add it to the map of representatives - n = d_equalityEngine.getRepresentative( n ); - if( d_reps.find( n )==d_reps.end() ){ - d_reps[n] = ret; - d_rep_set.add( ret ); - } - //TODO: make sure that this doesn't affect the representatives in the equality engine - // in other words, we need to be sure that all representatives of the equality engine - // are still representatives after this function, or else d_reps should be modified. - return ret; - }else{ - //otherwise, just return itself (this usually should not happen) - Trace("model") << "Return self." << std::endl; - return n; - } - } -} - TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( te ){ } @@ -502,9 +472,10 @@ void TheoryEngineModelBuilder::buildModel( Model* m, bool fullModel ){ assertedReps[ eqc ] = const_rep; }else{ if( fullModel ){ - //assertion failure? Trace("model-warn") << "No representative specified for equivalence class " << eqc << std::endl; Trace("model-warn") << " Type : " << eqc.getType() << std::endl; + //TODO: select proper representative + //Unimplemented("No representative specified for equivalence class"); } //assertedReps[ eqc ] = chooseRepresentative( tm, eqc, fullModel ); assertedReps[ eqc ] = eqc; @@ -533,6 +504,35 @@ void TheoryEngineModelBuilder::buildModel( Model* m, bool fullModel ){ processBuildModel( tm, fullModel ); } +void TheoryEngineModelBuilder::processBuildModel( TheoryModel* m, bool fullModel ){ + if( fullModel ){ + //construct function values + for( std::map< Node, std::vector< Node > >::iterator it = m->d_uf_terms.begin(); it != m->d_uf_terms.end(); ++it ){ + Trace("model-func") << "Creating function value..." << it->first << std::endl; + Node n = it->first; + if( m->d_uf_models.find( n )==m->d_uf_models.end() ){ + TypeNode type = n.getType(); + uf::UfModelTree ufmt( n ); + Node default_v; + for( size_t i=0; isecond.size(); i++ ){ + Node un = it->second[i]; + Node v = m->getRepresentative( un ); + ufmt.setValue( m, un, v ); + default_v = v; + } + if( default_v.isNull() ){ + //choose default value from model if none exists + default_v = m->getInterpretedValue( NodeManager::currentNM()->mkSkolem( "defaultValueQueryVar_$$", type.getRangeType(), + "a placeholder variable to query for a default value in model construction" ) ); + } + ufmt.setDefaultValue( m, default_v ); + ufmt.simplify(); + m->d_uf_models[n] = ufmt.getFunctionValue( "$x" ); + } + } + } +} + Node TheoryEngineModelBuilder::chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel ){ //try to get a new domain value Node rep = m->getNewDomainValue( eqc.getType() ); @@ -550,12 +550,12 @@ Node TheoryEngineModelBuilder::normalizeRepresentative( TheoryModel* m, Node r, std::map< Node, bool >& normalizing ){ Trace("temb-normalize") << r << std::endl; if( normalized.find( r )!=normalized.end() ){ - //Message() << " -> already normalized, return " << reps[r] << std::endl; + Trace("temb-normalize") << " -> already normalized, return " << reps[r] << std::endl; return reps[r]; }else if( normalizing.find( r )!=normalizing.end() && normalizing[r] ){ //this case is to handle things like when store( A, e, i ) is given // as a representative for array A. - //Message() << " -> currently normalizing, give up : " << r << std::endl; + Trace("temb-normalize") << " -> currently normalizing, give up : " << r << std::endl; return r; }else if( reps.find( r )!=reps.end() ){ normalizing[ r ] = true; @@ -563,13 +563,13 @@ Node TheoryEngineModelBuilder::normalizeRepresentative( TheoryModel* m, Node r, normalizing[ r ] = false; normalized[ r ] = true; reps[ r ] = retNode; - //Message() << " --> returned " << retNode << " for " << r << std::endl; + Trace("temb-normalize") << " --> returned " << retNode << " for " << r << std::endl; return retNode; }else if( m->d_equalityEngine.hasTerm( r ) ){ normalizing[ r ] = true; //return the normalized representative from the model r = m->d_equalityEngine.getRepresentative( r ); - //Message() << " -> it is the representative " << r << std::endl; + Trace("temb-normalize") << " -> it is the representative " << r << std::endl; Node retNode = normalizeRepresentative( m, r, reps, normalized, normalizing ); normalizing[ r ] = false; return retNode; @@ -582,7 +582,7 @@ Node TheoryEngineModelBuilder::normalizeRepresentative( TheoryModel* m, Node r, r = normalizeNode( m, r, reps, normalized, normalizing ); normalizing[ r ] = false; } - //Message() << " -> unknown, return " << r << std::endl; + Trace("temb-normalize") << " -> unknown, return " << r << std::endl; return r; } } @@ -591,7 +591,7 @@ Node TheoryEngineModelBuilder::normalizeNode( TheoryModel* m, Node r, std::map< std::map< Node, bool >& normalized, std::map< Node, bool >& normalizing ){ if( r.getNumChildren()>0 ){ - //Message() << " ---> normalize " << r << " " << r.getNumChildren() << " " << r.getKind() << std::endl; + Trace("temb-normalize") << " ---> normalize " << r << " " << r.getNumChildren() << " " << r.getKind() << std::endl; //non-leaf case: construct representative from children std::vector< Node > children; if( r.getMetaKind() == kind::metakind::PARAMETERIZED ){ @@ -603,10 +603,10 @@ Node TheoryEngineModelBuilder::normalizeNode( TheoryModel* m, Node r, std::map< } Node retNode = NodeManager::currentNM()->mkNode( r.getKind(), children ); retNode = Rewriter::rewrite( retNode ); - if( retNode!=r ){ + //if( retNode!=r ){ //assure that it is made equal in the model - m->assertEquality( r, retNode, true ); - } + //m->assertEquality( r, retNode, true ); + //} return retNode; }else{ return r; diff --git a/src/theory/model.h b/src/theory/model.h index adf97df9e..de4d57d2e 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -40,7 +40,7 @@ protected: /** substitution map for this model */ SubstitutionMap d_substitutions; public: - TheoryModel( context::Context* c, std::string name ); + TheoryModel( context::Context* c, std::string name, bool enableFuncModels ); virtual ~TheoryModel(){} /** equality engine containing all known equalities/disequalities */ eq::EqualityEngine d_equalityEngine; @@ -54,15 +54,15 @@ public: protected: /** reset the model */ virtual void reset(); - /** get interpreted value - * This function is called when the value of the node cannot be determined by the theory rewriter - * This should function should return a representative in d_reps - */ - virtual Node getInterpretedValue( TNode n ) = 0; /** * Get model value function. This function is called by getValue */ Node getModelValue( TNode n ); + /** get interpreted value + * This function is called when the value of the node cannot be determined by the theory rewriter + * This should function should return a representative in d_reps + */ + virtual Node getInterpretedValue( TNode n ); public: /** * Get value function. This should be called only after a ModelBuilder has called buildModel(...) @@ -125,28 +125,12 @@ public: void printRepresentativeDebug( const char* c, Node r ); /** print representative function */ void printRepresentative( std::ostream& out, Node r ); -}; - -/** Default model class - * The getInterpretedValue function will choose an existing value arbitrarily. - * If none are found, then it will create a new value. - */ -class DefaultModel : public TheoryModel -{ -protected: +public: /** whether function models are enabled */ bool d_enableFuncModels; - /** add term */ - void addTerm( Node n ); -public: - DefaultModel( context::Context* c, std::string name, bool enableFuncModels ); - virtual ~DefaultModel(){} //necessary information for function models std::map< Node, std::vector< Node > > d_uf_terms; std::map< Node, Node > d_uf_models; -public: - void reset(); - Node getInterpretedValue( TNode n ); }; /** TheoryEngineModelBuilder class @@ -159,7 +143,7 @@ protected: /** pointer to theory engine */ TheoryEngine* d_te; /** process build model */ - virtual void processBuildModel( TheoryModel* m, bool fullModel ){} + virtual void processBuildModel( TheoryModel* m, bool fullModel ); /** choose representative for unconstrained equivalence class */ virtual Node chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel ); /** normalize representative */ diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 6e3e27828..e0723f432 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -28,7 +28,7 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -FirstOrderModel::FirstOrderModel( context::Context* c, std::string name ) : DefaultModel( c, name, true ), +FirstOrderModel::FirstOrderModel( context::Context* c, std::string name ) : TheoryModel( c, name, true ), d_axiom_asserted( c, false ), d_forall_asserts( c ){ } @@ -41,11 +41,11 @@ void FirstOrderModel::assertQuantifier( Node n ){ } void FirstOrderModel::reset(){ - DefaultModel::reset(); + TheoryModel::reset(); } void FirstOrderModel::addTerm( Node n ){ - DefaultModel::addTerm( n ); + TheoryModel::addTerm( n ); } void FirstOrderModel::initialize( bool considerAxioms ){ @@ -94,16 +94,16 @@ void FirstOrderModel::initializeModelForTerm( Node n ){ } Node FirstOrderModel::getInterpretedValue( TNode n ){ - Trace("fo-model") << "get interpreted value " << n << std::endl; - TypeNode type = n.getType(); + //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() ){ d_uf_models[n] = d_uf_model_tree[n].getFunctionValue( "$x" ); } } - } - return DefaultModel::getInterpretedValue( n ); + }*/ + return TheoryModel::getInterpretedValue( n ); } void FirstOrderModel::toStream(std::ostream& out){ diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 1fc4fd76e..64e5fc904 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -39,7 +39,7 @@ namespace quantifiers{ class TermDb; -class FirstOrderModel : public DefaultModel +class FirstOrderModel : public TheoryModel { private: //add term function diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index c09346f35..8eac4da95 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -76,8 +76,11 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { //update models for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ it->second.update( fm ); + Trace("model-func") << "ModelEngineBuilder: Make function value from tree " << it->first << std::endl; + //construct function values + fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" ); } - + TheoryEngineModelBuilder::processBuildModel( m, fullModel ); }else{ d_curr_model = fm; //build model for relevant symbols contained in quantified formulas diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d69f43908..932f11f74 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -86,7 +86,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_quantEngine = new QuantifiersEngine(context, this); // build model information if applicable - d_curr_model = new theory::DefaultModel( context, "DefaultModel", true ); + d_curr_model = new theory::TheoryModel( context, "DefaultModel", true ); d_curr_model_builder = new theory::TheoryEngineModelBuilder( this ); Rewriter::init(); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index f2324e5d2..5ec0d9776 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -130,7 +130,7 @@ class TheoryEngine { /** * Default model object */ - theory::DefaultModel* d_curr_model; + theory::TheoryModel* d_curr_model; /** * Model builder object */ diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index 8c79f69df..424b2c117 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -262,6 +262,13 @@ void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector } } +Node UfModelTree::getFunctionValue( std::vector< Node >& args ){ + Node body = d_tree.getFunctionValue( args, 0, Node::null() ); + body = Rewriter::rewrite( body ); + Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args); + return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, body); +} + Node UfModelTree::getFunctionValue( const char* argPrefix ){ TypeNode type = d_op.getType(); std::vector< Node > vars; diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 865e7ace9..efcbbef89 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -127,12 +127,7 @@ public: /** getFunctionValue * Returns a representation of this function. */ - Node getFunctionValue( std::vector< Node >& args ){ - Node body = d_tree.getFunctionValue( args, 0, Node::null() ); - body = Rewriter::rewrite( body ); - Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args); - return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, body); - } + Node getFunctionValue( std::vector< Node >& args ); /** getFunctionValue for args with set prefix */ Node getFunctionValue( const char* argPrefix ); /** update -- 2.30.2