From c3e9112157320111c18b2984052abd9cd17127dc Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Wed, 3 Oct 2012 21:28:11 +0000 Subject: [PATCH] New model code, mostly workin --- src/theory/arrays/theory_arrays.cpp | 79 +++-- src/theory/model.cpp | 530 ++++++++++++++++------------ src/theory/model.h | 128 ++++++- src/theory/theory_engine.cpp | 11 + src/theory/uf/theory_uf.cpp | 42 +-- src/theory/uf/theory_uf_model.cpp | 12 +- 6 files changed, 510 insertions(+), 292 deletions(-) diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index e1f93158f..63b61995a 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -628,47 +628,70 @@ void TheoryArrays::computeCareGraph() void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){ m->assertEqualityEngine( &d_equalityEngine ); - //must determine proper representatives for all array equivalence classes - //first, we collect all select terms and array equivalence classes - std::map< Node, std::vector< Node > > selects; - std::vector< Node > arrays; + + std::map > selects; + std::vector arrays; + + // Go through all equivalence classes eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + bool isArray, computeRep; while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); - if( eqc.getType().isArray() ){ - arrays.push_back( eqc ); - } + isArray = eqc.getType().isArray(); + computeRep = false; eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); while( !eqc_i.isFinished() ){ Node n = *eqc_i; - if( n.getKind()==kind::SELECT ){ - selects[ n[0] ].push_back( n ); + // If this EC is an array type and it contains something other than STORE nodes, we have to compute a representative explicitly + if (isArray && n.getKind() != kind::STORE) { + arrays.push_back(eqc); + computeRep = true; + } + // If this term is a select, record that the EC rep of its store parameter is being read from using this term + if (n.getKind()==kind::SELECT) { + selects[d_equalityEngine.getRepresentative(n[0])].push_back(n); } ++eqc_i; } + // If this is an array EC but it only contains STORE nodes, then the value of this EC is derived from the others - + // no need to do extra work to compute it + if (isArray && !computeRep) { + m->assertRepresentative(eqc); + } ++eqcs_i; } - //for all array equivalence classes - for( size_t i=0; i defValues; + map::iterator it; + TypeSet defaultValuesSet; + + // Loop through all array equivalence classes that need a representative computed + for (size_t i=0; imkConst(ArrayStoreAll(n.getType().toType(), rep.toExpr())); + // For each read, require that the rep stores the right value + vector& reads = selects[n]; + for (unsigned j = 0; j < reads.size(); ++j) { + rep = nm->mkNode(kind::STORE, rep, reads[j][1], reads[j]); } - //construct the representative - Node rep = am.getArrayValue(); - Assert( !rep.isNull() ); - m->assertEquality( arrays[i], rep, true ); - //communicate to the model that it is the representative - m->assertRepresentative( rep ); + m->assertEquality(n, rep, true); + m->assertRepresentative(rep); } } diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 96b5d6945..bd9e6aefa 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -29,13 +29,14 @@ using namespace CVC4::context; using namespace CVC4::theory; TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFuncModels ) : -d_substitutions( c ), d_equalityEngine( c, name ), d_enableFuncModels( 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 d_equalityEngine.addFunctionKind(kind::APPLY_UF); d_equalityEngine.addFunctionKind(kind::SELECT); - d_equalityEngine.addFunctionKind(kind::STORE); + // d_equalityEngine.addFunctionKind(kind::STORE); d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR); d_equalityEngine.addFunctionKind(kind::APPLY_TESTER); @@ -76,74 +77,76 @@ Cardinality TheoryModel::getCardinality( Type t ){ } } -void TheoryModel::toStream( std::ostream& out ){ - /*//for debugging - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - while( !eqcs_i.isFinished() ){ - Node eqc = (*eqcs_i); - Debug("get-model-debug") << eqc << " : " << eqc.getType() << " : " << std::endl; - out << " "; - //add terms to model - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); - while( !eqc_i.isFinished() ){ - out << (*eqc_i) << " "; - ++eqc_i; - } - out << std::endl; - ++eqcs_i; - } - */ +void TheoryModel::toStream( std::ostream& out ) +{ out << this; } -Node TheoryModel::getModelValue( TNode n ){ - Trace("model") << "TheoryModel::getModelValue " << n << std::endl; - - //// special case: prop engine handles boolean vars - //if(n.isVar() && n.getType().isBoolean()) { - // Trace("model") << "-> Propositional variable." << std::endl; - // return d_te->getPropEngine()->getValue( n ); - //} - - // special case: value of a constant == itself +Node TheoryModel::getModelValue( TNode n ) +{ if( n.isConst() ) { - Trace("model") << "-> Constant." << std::endl; return n; } - Node nn; - if( n.getNumChildren()>0 ){ - std::vector< Node > children; - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - Debug("model-debug") << "get operator: " << n.getOperator() << std::endl; - children.push_back( n.getOperator() ); + TypeNode t = n.getType(); + if (t.isFunction() || t.isPredicate()) { + if (d_enableFuncModels) { + if (d_uf_models.find(n) != d_uf_models.end()) { + // Existing function + return d_uf_models[n]; + } + // Unknown function symbol: return LAMBDA x. c, where c is the first constant in the enumeration of the range type + vector argTypes = t.getArgTypes(); + vector args; + NodeManager* nm = NodeManager::currentNM(); + for (unsigned i = 0; i < argTypes.size(); ++i) { + args.push_back(nm->mkBoundVar(argTypes[i])); + } + Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, args); + TypeEnumerator te(t.getRangeType()); + return nm->mkNode(kind::LAMBDA, boundVarList, *te); + } + // TODO: if func models not enabled, throw an error? + Unreachable(); + } + + if (n.getNumChildren() > 0) { + std::vector children; + if (n.getKind() == APPLY_UF) { + Node op = n.getOperator(); + if (d_uf_models.find(op) == d_uf_models.end()) { + // Unknown term - return first enumerated value for this type + TypeEnumerator te(n.getType()); + return *te; + } + // Plug in uninterpreted function model + children.push_back(d_uf_models[op]); + } + else if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { + children.push_back(n.getOperator()); } //evaluate the children - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - Node val = getValue( n[i] ); - Debug("model-debug") << i << " : " << n[i] << " -> " << val << std::endl; - Assert( !val.isNull() ); - children.push_back( val ); - } - Debug("model-debug") << "Done eval children" << std::endl; - nn = NodeManager::currentNM()->mkNode( n.getKind(), children ); - }else{ - nn = n; + for (unsigned i = 0; i < n.getNumChildren(); ++i) { + Node val = getValue(n[i]); + children.push_back(val); + } + Node val = Rewriter::rewrite(NodeManager::currentNM()->mkNode(n.getKind(), children)); + Assert(val.isConst()); + return val; } - //interpretation is the rewritten form - nn = Rewriter::rewrite( nn ); - // special case: value of a constant == itself - if( nn.isConst() ) { - Trace("model") << "-> Theory-interpreted term." << std::endl; - return nn; - }else{ - Trace("model") << "-> Model-interpreted term." << std::endl; - //otherwise, get the interpreted value in the model - return getInterpretedValue( nn ); + if (!d_equalityEngine.hasTerm(n)) { + // Unknown term - return first enumerated value for this type + TypeEnumerator te(n.getType()); + return *te; } + Node val = d_equalityEngine.getRepresentative(n); + Assert(d_reps.find(val) != d_reps.end()); + val = d_reps[val]; + return val; } + Node TheoryModel::getInterpretedValue( TNode n ){ Trace("model") << "Get interpreted value of " << n << std::endl; TypeNode type = n.getType(); @@ -166,7 +169,7 @@ Node TheoryModel::getInterpretedValue( TNode n ){ }else{ return n; } - }else{ + } else{ Trace("model-debug") << "check rep..." << std::endl; Node ret; //check if the representative is defined @@ -232,31 +235,6 @@ 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 0 - if( tn==NodeManager::currentNM()->booleanType() ){ - if( d_rep_set.d_type_reps[tn].empty() ){ - return d_false; - }else if( d_rep_set.d_type_reps[tn].size()==1 ){ - return NodeManager::currentNM()->mkConst( areEqual( d_rep_set.d_type_reps[tn][0], d_false ) ); - }else{ - return Node::null(); - } - }else if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){ - int val = 0; - do{ - Node r = NodeManager::currentNM()->mkConst( Rational(val) ); - if( std::find( d_rep_set.d_type_reps[tn].begin(), d_rep_set.d_type_reps[tn].end(), r )==d_rep_set.d_type_reps[tn].end() && - !d_equalityEngine.hasTerm( r ) ){ - return r; - } - val++; - }while( true ); - }else{ - //otherwise must make a variable FIXME: how to make constants for other sorts? - //return NodeManager::currentNM()->mkSkolem( tn ); - return Node::null(); - } -#else if( tn.isSort() ){ return Node::null(); }else{ @@ -282,7 +260,6 @@ Node TheoryModel::getNewDomainValue( TypeNode tn ){ } return Node::null(); } -#endif } /** add substitution */ @@ -298,7 +275,7 @@ void TheoryModel::addTerm( Node n ){ d_equalityEngine.addTerm( n ); } //must collect UF terms - if( d_enableFuncModels && n.getKind()==APPLY_UF ){ + if (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 ); @@ -420,119 +397,292 @@ TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( t } -void TheoryEngineModelBuilder::buildModel( Model* m, bool fullModel ){ +void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) +{ TheoryModel* tm = (TheoryModel*)m; - //reset representative information + + // Reset model tm->reset(); - //collect model info from the theory engine + + // Collect model info from the theories Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..." << std::endl; - d_te->collectModelInfo( tm, fullModel ); + d_te->collectModelInfo(tm, fullModel); + Trace("model-builder") << "Collect representatives..." << std::endl; - //store asserted representative map - std::map< Node, Node > assertedReps; - //process all terms in the equality engine, store representatives + // Process all terms in the equality engine, store representatives for each EC + std::map< Node, Node > assertedReps, constantReps; + TypeSet typeConstSet, typeRepSet, typeNoRepSet; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &tm->d_equalityEngine ); - while( !eqcs_i.isFinished() ){ + for ( ; !eqcs_i.isFinished(); ++eqcs_i) { + + // eqc is the equivalence class representative Node eqc = (*eqcs_i); - if( assertedReps.find( eqc )!=assertedReps.end() ){ - Trace("model-warn") << "Duplicate equivalence class!!!! " << eqc << std::endl; - }else{ - TypeNode eqct = eqc.getType(); - Node const_rep; - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &tm->d_equalityEngine ); - while( !eqc_i.isFinished() ){ - Node n = *eqc_i; - //if this node was specified as a representative - if( tm->d_reps.find( n )!=tm->d_reps.end() ){ - Assert( !tm->d_reps[n].isNull() ); - //if not already specified - if( assertedReps.find( eqc )==assertedReps.end() ){ - Trace("model-builder") << "Rep( " << eqc << " ) = " << tm->d_reps[n] << std::endl; - assertedReps[ eqc ] = tm->d_reps[n]; - }else{ - if( n!=assertedReps[eqc] ){ //FIXME : this should be an assertion (EqClassIterator should not give duplicates) - //duplicate representative specified - Trace("model-warn") << "Duplicate representative specified for equivalence class " << eqc << ": " << std::endl; - Trace("model-warn") << " " << assertedReps[eqc] << ", " << n << std::endl; - Trace("model-warn") << " Type : " << n.getType() << std::endl; - } + Trace("model-builder") << "Processing EC: " << eqc << endl; + Assert(tm->d_equalityEngine.getRepresentative(eqc) == eqc); + TypeNode eqct = eqc.getType(); + Assert(assertedReps.find(eqc) == assertedReps.end()); + Assert(constantReps.find(eqc) == constantReps.end()); + + // Loop through terms in this EC + Node rep, const_rep; + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &tm->d_equalityEngine); + for ( ; !eqc_i.isFinished(); ++eqc_i) { + Node n = *eqc_i; + Trace("model-builder") << " Processing Term: " << n << endl; + // Record as rep if this node was specified as a representative + if (tm->d_reps.find(n) != tm->d_reps.end()){ + Assert(rep.isNull()); + rep = tm->d_reps[n]; + Assert(!rep.isNull() ); + Trace("model-builder") << " Rep( " << eqc << " ) = " << rep << std::endl; + } + // Record as const_rep if this node is constant + if (n.isConst()) { + Assert(const_rep.isNull()); + const_rep = n; + Trace("model-builder") << " ConstRep( " << eqc << " ) = " << const_rep << std::endl; + } + //model-specific processing of the term + tm->addTerm(n); + } + + // Assign representative for this EC + if (!const_rep.isNull()) { + // Theories should not specify a rep if there is already a constant in the EC + Assert(rep.isNull() || rep == const_rep); + constantReps[eqc] = const_rep; + typeConstSet.add(eqct, const_rep); + } + else if (!rep.isNull()) { + assertedReps[eqc] = rep; + typeRepSet.add(eqct, eqc); + } + else { + typeNoRepSet.add(eqct, eqc); + } + } + + // Need to ensure that each EC has a constant representative. + + // Phase 1: For types that do not have asserted reps, assign the unassigned EC's using either evaluation or type enumeration + Trace("model-builder") << "Starting phase 1..." << std::endl; + TypeSet::iterator it; + for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) { + TypeNode t = TypeSet::getType(it); + Trace("model-builder") << " Working on type: " << t << endl; + set& noRepSet = TypeSet::getSet(it); + Assert(!noRepSet.empty()); + + set::iterator i, i2; + bool changed; + + // Find value for this EC using evaluation if possible + do { + changed = false; + d_normalizedCache.clear(); + for (i = noRepSet.begin(); i != noRepSet.end(); ) { + i2 = i; + ++i; + eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, &tm->d_equalityEngine); + for ( ; !eqc_i.isFinished(); ++eqc_i) { + Node n = *eqc_i; + Node normalized = normalize(tm, n, constantReps); + if (normalized.isConst()) { + typeConstSet.add(t, normalized); + constantReps[*i2] = normalized; + Trace("model-builder") << " Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl; + changed = true; + noRepSet.erase(i2); + break; } - }else if( n.isConst() ){ - //if this is constant, we will use it as representative (if none other specified) - const_rep = n; } - //model-specific processing of the term - tm->addTerm( n ); - ++eqc_i; } - //if a representative was not specified - if( assertedReps.find( eqc )==assertedReps.end() ){ - if( !const_rep.isNull() ){ - //use the constant representative - assertedReps[ eqc ] = const_rep; - }else{ - if( fullModel ){ - 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"); + } while (changed); + + // Skip next step if nothing to do or if fullModel is false (meaning we shouldn't choose any representatives that aren't forced) + if (noRepSet.empty() || !fullModel) { + continue; + } + + // This assertion may be too strong, but hopefully not: we expect that for every type, either all of its EC's have asserted reps (or constants) + // or none of its EC's have asserted reps. + Assert(typeRepSet.getSet(t) == NULL); + + Node n; + for (i = noRepSet.begin(); i != noRepSet.end(); ++i) { + n = typeConstSet.nextTypeEnum(t); + constantReps[*i] = n; + Trace("model-builder") << " New Const: Setting constant rep of " << (*i) << " to " << n << endl; + } + } + + // Phase 2: Substitute into asserted reps using constReps. + // Iterate until a fixed point is reached. + Trace("model-builder") << "Starting phase 2..." << std::endl; + bool changed; + do { + changed = false; + d_normalizedCache.clear(); + for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) { + set& repSet = TypeSet::getSet(it); + set::iterator i; + for (i = repSet.begin(); i != repSet.end(); ) { + Assert(assertedReps.find(*i) != assertedReps.end()); + Node rep = assertedReps[*i]; + Node normalized = normalize(tm, rep, constantReps); + Trace("model-builder") << " Normalizing rep (" << rep << "), normalized to (" << normalized << ")" << endl; + if (normalized.isConst()) { + changed = true; + constantReps[*i] = normalized; + assertedReps.erase(*i); + set::iterator i2 = i; + ++i; + repSet.erase(i2); + } + else { + if (normalized != rep) { + assertedReps[*i] = normalized; + changed = true; } - //assertedReps[ eqc ] = chooseRepresentative( tm, eqc, fullModel ); - assertedReps[ eqc ] = eqc; + ++i; } } } - ++eqcs_i; - } - Trace("model-builder") << "Normalize representatives..." << std::endl; - //now, normalize all representatives - // this will make every leaf of asserted representatives into a representative - std::map< Node, bool > normalized; - for( std::map< Node, Node >::iterator it = assertedReps.begin(); it != assertedReps.end(); ++it ){ - std::map< Node, bool > normalizing; - normalizeRepresentative( tm, it->first, assertedReps, normalized, normalizing ); + } while (changed); + + if (fullModel) { + // Assert that all representatives have been converted to constants + for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) { + set& repSet = TypeSet::getSet(it); + Assert(repSet.empty()); + } } + Trace("model-builder") << "Copy representatives to model..." << std::endl; - //assertedReps has the actual representatives we will use, now copy to model tm->d_reps.clear(); - for( std::map< Node, Node >::iterator it = assertedReps.begin(); it != assertedReps.end(); ++it ){ - tm->d_reps[ it->first ] = it->second; - tm->d_rep_set.add( it->second ); + std::map< Node, Node >::iterator itMap; + for (itMap = constantReps.begin(); itMap != constantReps.end(); ++itMap) { + tm->d_reps[itMap->first] = itMap->second; + tm->d_rep_set.add(itMap->second); + } + + if (!fullModel) { + // Make sure every EC has a rep + for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap ) { + tm->d_reps[itMap->first] = itMap->second; + tm->d_rep_set.add(itMap->second); + } + for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) { + set& noRepSet = TypeSet::getSet(it); + set::iterator i; + for (i = noRepSet.begin(); i != noRepSet.end(); ++i) { + tm->d_reps[*i] = *i; + tm->d_rep_set.add(*i); + } + } } //modelBuilder-specific initialization processBuildModel( tm, fullModel ); + + if (fullModel) { + // Check that every term evaluates to its representative in the model + for (eqcs_i = eq::EqClassesIterator(&tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) { + // eqc is the equivalence class representative + Node eqc = (*eqcs_i); + Assert(constantReps.find(eqc) != constantReps.end()); + Node rep = constantReps[eqc]; + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &tm->d_equalityEngine); + for ( ; !eqc_i.isFinished(); ++eqc_i) { + Node n = *eqc_i; + Assert(tm->getValue(*eqc_i) == rep); + } + } + } +} + + +Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node, Node >& constantReps) +{ + std::map::iterator itMap = constantReps.find(r); + if (itMap != constantReps.end()) { + return (*itMap).second; + } + NodeMap::iterator it = d_normalizedCache.find(r); + if (it != d_normalizedCache.end()) { + return (*it).second; + } + Node retNode = r; + if (r.getNumChildren() > 0) { + std::vector children; + if (r.getMetaKind() == kind::metakind::PARAMETERIZED) { + children.push_back(r.getOperator()); + } + bool childrenConst = true; + for (size_t i=0; i < r.getNumChildren(); ++i) { + Node ri = r[i]; + if (!ri.isConst()) { + if (m->d_equalityEngine.hasTerm(ri)) { + ri = m->d_equalityEngine.getRepresentative(ri); + } + ri = normalize(m, ri, constantReps); + if (!ri.isConst()) { + childrenConst = false; + } + } + children.push_back(ri); + } + retNode = NodeManager::currentNM()->mkNode( r.getKind(), children ); + if (childrenConst) { + retNode = Rewriter::rewrite(retNode); + } + } + d_normalizedCache[r] = retNode; + return retNode; } -void TheoryEngineModelBuilder::processBuildModel( TheoryModel* m, bool fullModel ){ - if( fullModel ){ + +void TheoryEngineModelBuilder::processBuildModel(TheoryModel* m, bool fullModel) +{ + if (fullModel) { + Trace("model-builder") << "Assigning function values..." << endl; //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; + Node default_v, un, simp, v; for( size_t i=0; isecond.size(); i++ ){ - Node un = it->second[i]; - Node v = m->getRepresentative( un ); - ufmt.setValue( m, un, v ); + un = it->second[i]; + vector children; + children.push_back(n); + for (size_t j = 0; j < un.getNumChildren(); ++j) { + children.push_back(m->getRepresentative(un[j])); + } + simp = NodeManager::currentNM()->mkNode(un.getKind(), children); + v = m->getRepresentative(un); + Trace("model-builder") << " Setting (" << simp << ") to (" << v << ")" << endl; + ufmt.setValue(m, simp, 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" ) ); + TypeEnumerator te(type.getRangeType()); + default_v = (*te); } ufmt.setDefaultValue( m, default_v ); ufmt.simplify(); - m->d_uf_models[n] = ufmt.getFunctionValue( "$x" ); + Node val = ufmt.getFunctionValue( "$x" ); + Trace("model-builder") << " Assigning (" << n << ") to (" << val << ")" << endl; + m->d_uf_models[n] = val; + //ufmt.debugPrint( std::cout, m ); } } } } + Node TheoryEngineModelBuilder::chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel ){ //try to get a new domain value Node rep = m->getNewDomainValue( eqc.getType() ); @@ -544,71 +694,3 @@ Node TheoryEngineModelBuilder::chooseRepresentative( TheoryModel* m, Node eqc, b return eqc; } } - -Node TheoryEngineModelBuilder::normalizeRepresentative( TheoryModel* m, Node r, std::map< Node, Node >& reps, - std::map< Node, bool >& normalized, - std::map< Node, bool >& normalizing ){ - Trace("temb-normalize") << r << std::endl; - if( normalized.find( r )!=normalized.end() ){ - 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. - Trace("temb-normalize") << " -> currently normalizing, give up : " << r << std::endl; - return r; - }else if( reps.find( r )!=reps.end() ){ - normalizing[ r ] = true; - Node retNode = normalizeNode( m, reps[r], reps, normalized, normalizing ); - normalizing[ r ] = false; - normalized[ r ] = true; - reps[ r ] = retNode; - 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 ); - Trace("temb-normalize") << " -> it is the representative " << r << std::endl; - Node retNode = normalizeRepresentative( m, r, reps, normalized, normalizing ); - normalizing[ r ] = false; - return retNode; - }else{ - if( !r.isConst() ){ - Trace("model-warn") << "Normalizing representative, unknown term: " << r << std::endl; - Trace("model-warn") << " Type : " << r.getType() << std::endl; - Trace("model-warn") << " Kind : " << r.getKind() << std::endl; - normalizing[ r ] = true; - r = normalizeNode( m, r, reps, normalized, normalizing ); - normalizing[ r ] = false; - } - Trace("temb-normalize") << " -> unknown, return " << r << std::endl; - return r; - } -} - -Node TheoryEngineModelBuilder::normalizeNode( TheoryModel* m, Node r, std::map< Node, Node >& reps, - std::map< Node, bool >& normalized, - std::map< Node, bool >& normalizing ){ - if( r.getNumChildren()>0 ){ - 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 ){ - children.push_back( r.getOperator() ); - } - for( size_t i=0; imkNode( r.getKind(), children ); - retNode = Rewriter::rewrite( retNode ); - //if( retNode!=r ){ - //assure that it is made equal in the model - //m->assertEquality( r, retNode, true ); - //} - return retNode; - }else{ - return r; - } -} diff --git a/src/theory/model.h b/src/theory/model.h index de4d57d2e..90cd1e35a 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -23,13 +23,11 @@ #include "theory/uf/equality_engine.h" #include "theory/rep_set.h" #include "theory/substitutions.h" +#include "theory/type_enumerator.h" namespace CVC4 { namespace theory { -class QuantifiersEngine; -class TheoryEngineModelBuilder; - /** Theory Model class * For Model m, should call m.initialize() before using */ @@ -133,6 +131,112 @@ public: std::map< Node, Node > d_uf_models; }; +/* + * Class that encapsulates a map from types to sets of nodes + */ +class TypeSet { +public: + typedef std::hash_map*, TypeNodeHashFunction> TypeSetMap; + typedef std::hash_map TypeToTypeEnumMap; + typedef TypeSetMap::iterator iterator; +private: + TypeSetMap d_typeSet; + TypeToTypeEnumMap d_teMap; + + public: + ~TypeSet() { + iterator it; + for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it) { + if ((*it).second != NULL) { + delete (*it).second; + } + } + TypeToTypeEnumMap::iterator it2; + for (it2 = d_teMap.begin(); it2 != d_teMap.end(); ++it2) { + if ((*it2).second != NULL) { + delete (*it2).second; + } + } + } + + void add(TypeNode t, TNode n) + { + iterator it = d_typeSet.find(t); + std::set* s; + if (it == d_typeSet.end()) { + s = new std::set; + d_typeSet[t] = s; + } + else { + s = (*it).second; + } + s->insert(n); + } + + std::set* getSet(TypeNode t) + { + iterator it = d_typeSet.find(t); + if (it == d_typeSet.end()) { + return NULL; + } + return (*it).second; + } + + Node nextTypeEnum(TypeNode t) + { + TypeEnumerator* te; + TypeToTypeEnumMap::iterator it = d_teMap.find(t); + if (it == d_teMap.end()) { + te = new TypeEnumerator(t); + d_teMap[t] = te; + } + else { + te = (*it).second; + } + Assert(!te->isFinished()); + + iterator itSet = d_typeSet.find(t); + std::set* s; + if (itSet == d_typeSet.end()) { + s = new std::set; + d_typeSet[t] = s; + } + else { + s = (*itSet).second; + } + Node n = **te; + while (s->find(n) != s->end()) { + Assert(!te->isFinished()); + ++(*te); + n = **te; + } + s->insert(n); + ++(*te); + return n; + } + + iterator begin() + { + return d_typeSet.begin(); + } + + iterator end() + { + return d_typeSet.end(); + } + + static TypeNode getType(iterator it) + { + return (*it).first; + } + + static std::set& getSet(iterator it) + { + return *(*it).second; + } + +}; + /** TheoryEngineModelBuilder class * This model builder will consult all theories in a theory engine for * collectModelInfo( ... ) when building a model. @@ -142,24 +246,22 @@ class TheoryEngineModelBuilder : public ModelBuilder protected: /** pointer to theory engine */ TheoryEngine* d_te; + typedef std::hash_map NodeMap; + NodeMap d_normalizedCache; + /** 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 ); + virtual Node chooseRepresentative(TheoryModel* m, Node eqc, bool fullModel); /** normalize representative */ - Node normalizeRepresentative( TheoryModel* m, Node r, std::map< Node, Node >& reps, - std::map< Node, bool >& normalized, - std::map< Node, bool >& normalizing ); - Node normalizeNode( TheoryModel* m, Node r, std::map< Node, Node >& reps, - std::map< Node, bool >& normalized, - std::map< Node, bool >& normalizing ); + Node normalize(TheoryModel* m, TNode r, std::map& constantReps); public: - TheoryEngineModelBuilder( TheoryEngine* te ); + TheoryEngineModelBuilder(TheoryEngine* te); virtual ~TheoryEngineModelBuilder(){} /** Build model function. * Should be called only on TheoryModels m */ - void buildModel( Model* m, bool fullModel ); + void buildModel(Model* m, bool fullModel); }; } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 0db71aba4..61b66ba3e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -590,6 +590,17 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){ d_theoryTable[theoryId]->collectModelInfo( m, fullModel ); } } + // Get the Boolean variables + vector boolVars; + d_propEngine->getBooleanVariables(boolVars); + vector::iterator it, iend = boolVars.end(); + bool hasValue, value; + for (it = boolVars.begin(); it != iend; ++it) { + TNode var = *it; + hasValue = d_propEngine->hasValue(var, value); + // TODO: Assert that hasValue is true? + m->assertPredicate(var, hasValue ? value : false); + } } /* get model */ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 67c1aa9f6..ba7890b80 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -194,27 +194,27 @@ Node TheoryUF::explain(TNode literal) { void TheoryUF::collectModelInfo( TheoryModel* m, bool fullModel ){ m->assertEqualityEngine( &d_equalityEngine ); - if( fullModel ){ - std::map< TypeNode, TypeEnumerator* > type_enums; - //must choose proper representatives - // for each equivalence class, specify fresh constant as representative - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - while( !eqcs_i.isFinished() ){ - Node eqc = (*eqcs_i); - TypeNode tn = eqc.getType(); - if( tn.isSort() ){ - if( type_enums.find( tn )==type_enums.end() ){ - type_enums[tn] = new TypeEnumerator( tn ); - } - Node rep = *(*type_enums[tn]); - ++(*type_enums[tn]); - //specify the constant as the representative - m->assertEquality( eqc, rep, true ); - m->assertRepresentative( rep ); - } - ++eqcs_i; - } - } + // if( fullModel ){ + // std::map< TypeNode, TypeEnumerator* > type_enums; + // //must choose proper representatives + // // for each equivalence class, specify fresh constant as representative + // eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + // while( !eqcs_i.isFinished() ){ + // Node eqc = (*eqcs_i); + // TypeNode tn = eqc.getType(); + // if( tn.isSort() ){ + // if( type_enums.find( tn )==type_enums.end() ){ + // type_enums[tn] = new TypeEnumerator( tn ); + // } + // Node rep = *(*type_enums[tn]); + // ++(*type_enums[tn]); + // //specify the constant as the representative + // m->assertEquality( eqc, rep, true ); + // m->assertRepresentative( rep ); + // } + // ++eqcs_i; + // } + // } } void TheoryUF::presolve() { diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index 424b2c117..5df9868f3 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -142,18 +142,18 @@ Node UfModelTreeNode::getFunctionValue( std::vector< Node >& args, int index, No if( d_data.find( Node::null() )!=d_data.end() ){ defaultValue = d_data[Node::null()].getFunctionValue( args, index+1, argDefaultValue ); } - std::vector< Node > caseValues; - std::map< Node, Node > caseArg; + std::vector< Node > caseArgs; + std::map< Node, Node > caseValues; for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ if( !it->first.isNull() ){ Node val = it->second.getFunctionValue( args, index+1, defaultValue ); - caseValues.push_back( val ); - caseArg[ val ] = it->first; + caseArgs.push_back( it->first ); + caseValues[ it->first ] = val; } } Node retNode = defaultValue; - for( int i=((int)caseValues.size()-1); i>=0; i-- ){ - retNode = NodeManager::currentNM()->mkNode( ITE, args[index].eqNode( caseArg[ caseValues[i] ] ), caseValues[i], retNode ); + for( int i=((int)caseArgs.size()-1); i>=0; i-- ){ + retNode = NodeManager::currentNM()->mkNode( ITE, args[index].eqNode( caseArgs[ i ] ), caseValues[ caseArgs[ i ] ], retNode ); } return retNode; }else{ -- 2.30.2