diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/builtin/kinds | 1 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 5 | ||||
-rw-r--r-- | src/theory/model.cpp | 2 | ||||
-rw-r--r-- | src/theory/substitutions.cpp | 16 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 5 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 26 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_model.cpp | 4 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_model.h | 6 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 30 |
9 files changed, 62 insertions, 33 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index c4c3435a2..1218f3809 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -341,6 +341,7 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule +construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule constant SUBTYPE_TYPE \ ::CVC4::Predicate \ diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 95ede1c46..7bc1d956d 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -161,6 +161,11 @@ public: TypeNode rangeType = n[1].getType(check); return nodeManager->mkFunctionType(argTypes, rangeType); } + + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { + Assert(n.getKind() == kind::LAMBDA); + return true; + } };/* class LambdaTypeRule */ class SortProperties { diff --git a/src/theory/model.cpp b/src/theory/model.cpp index ed2d69308..ee61c9345 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -98,7 +98,7 @@ Node TheoryModel::getModelValue( TNode n ){ Trace("model") << "TheoryModel::getModelValue " << n << std::endl; //// special case: prop engine handles boolean vars - //if(metakind == kind::metakind::VARIABLE && n.getType().isBoolean()) { + //if(n.isVar() && n.getType().isBoolean()) { // Trace("model") << "-> Propositional variable." << std::endl; // return d_te->getPropEngine()->getValue( n ); //} diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index b7c9278e1..b5f846735 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -75,7 +75,7 @@ Node SubstitutionMap::internalSubstitute(TNode t) { // Children have been processed, so substitute NodeBuilder<> builder(current.getKind()); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { - builder << current.getOperator(); + builder << Node(d_substitutionCache[current.getOperator()]); } for (unsigned i = 0; i < current.getNumChildren(); ++ i) { Assert(d_substitutionCache.find(current[i]) != d_substitutionCache.end()); @@ -105,8 +105,16 @@ Node SubstitutionMap::internalSubstitute(TNode t) { toVisit.pop_back(); } else { // Mark that we have added the children if any - if (current.getNumChildren() > 0) { + if (current.getNumChildren() > 0 || current.getMetaKind() == kind::metakind::PARAMETERIZED) { stackHead.children_added = true; + // We need to add the operator, if any + if(current.getMetaKind() == kind::metakind::PARAMETERIZED) { + TNode opNode = current.getOperator(); + NodeCache::iterator opFind = d_substitutionCache.find(opNode); + if (opFind == d_substitutionCache.end()) { + toVisit.push_back(opNode); + } + } // We need to add the children for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { TNode childNode = *child_it; @@ -255,6 +263,10 @@ void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << std::endl; Assert(d_substitutions.find(x) == d_substitutions.end()); + // this causes a later assert-fail (the rhs != current one, above) anyway + // putting it here is easier to diagnose + Assert(x != t, "cannot substitute a term for itself"); + d_substitutions[x] = t; // Also invalidate the cache if necessary diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index b0a290b7d..c9fb36830 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -85,7 +85,7 @@ TheoryEngine::TheoryEngine(context::Context* context, // initialize the quantifiers engine d_quantEngine = new QuantifiersEngine(context, this); - //build model information if applicable + // build model information if applicable d_curr_model = new theory::DefaultModel( context, "DefaultModel", true ); d_curr_model_builder = new theory::TheoryEngineModelBuilder( this ); @@ -105,6 +105,9 @@ TheoryEngine::~TheoryEngine() { } } + delete d_curr_model_builder; + delete d_curr_model; + delete d_quantEngine; StatisticsRegistry::unregisterStat(&d_combineTheoriesTime); diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index a1500e084..9809b948e 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -195,31 +195,6 @@ Node TheoryUF::explain(TNode literal) { void TheoryUF::collectModelInfo( TheoryModel* m, bool fullModel ){ m->assertEqualityEngine( &d_equalityEngine ); if( fullModel ){ -#if 1 - std::map< TypeNode, int > type_count; - //must choose proper representatives - // for each equivalence class, specify the constructor as a 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_count.find( tn )==type_count.end() ){ - type_count[tn] = 0; - } - std::stringstream ss; - ss << Expr::setlanguage(options::outputLanguage()); - ss << "$t_" << tn << (type_count[tn]+1); - type_count[tn]++; - Node rep = NodeManager::currentNM()->mkSkolem( ss.str(), tn ); - Trace("mkVar") << "TheoryUF::collectModelInfo: make variable " << rep << " : " << tn << std::endl; - //specify the constant as the representative - m->assertEquality( eqc, rep, true ); - m->assertRepresentative( rep ); - } - ++eqcs_i; - } -#else std::map< TypeNode, TypeEnumerator* > type_enums; //must choose proper representatives // for each equivalence class, specify the constructor as a representative @@ -239,7 +214,6 @@ void TheoryUF::collectModelInfo( TheoryModel* m, bool fullModel ){ } ++eqcs_i; } - #endif } } diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index b8110a2aa..8c79f69df 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -268,7 +268,7 @@ Node UfModelTree::getFunctionValue( const char* argPrefix ){ for( size_t i=0; i<type.getNumChildren()-1; i++ ){ std::stringstream ss; ss << argPrefix << (i+1); - vars.push_back( NodeManager::currentNM()->mkSkolem( ss.str(), type[i] ) ); + vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) ); } return getFunctionValue( vars ); } @@ -415,4 +415,4 @@ Node UfModelPreferenceData::getBestDefaultValue( Node defaultTerm, TheoryModel* Debug("fmf-model-cons") << " # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl; Debug("fmf-model-cons") << " # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl; return defaultVal; -}
\ No newline at end of file +} diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 61c0714a3..fd346bc3c 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -127,7 +127,11 @@ public: /** getFunctionValue * Returns a representation of this function. */ - Node getFunctionValue( std::vector< Node >& args ){ return d_tree.getFunctionValue( args, 0, Node::null() ); } + Node getFunctionValue( std::vector< Node >& args ){ + Node body = d_tree.getFunctionValue( args, 0, Node::null() ); + Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args); + return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, body); + } /** getFunctionValue for args with set prefix */ Node getFunctionValue( const char* argPrefix ); /** update diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index 8ba39f372..f70d89b30 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -36,12 +36,27 @@ public: if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) { if(node[0] == node[1]) { return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); + } else if(node[0].isConst() && node[1].isConst()) { + // uninterpreted constants are all distinct + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false)); } if (node[0] > node[1]) { Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]); return RewriteResponse(REWRITE_DONE, newNode); } } + if(node.getKind() == kind::APPLY_UF && node.getOperator().getKind() == kind::LAMBDA) { + // resolve away the lambda + context::Context fakeContext; + theory::SubstitutionMap substitutions(&fakeContext); + TNode lambda = node.getOperator(); + for(TNode::iterator formal = lambda[0].begin(), arg = node.begin(); formal != lambda[0].end(); ++formal, ++arg) { + // typechecking should ensure that the APPLY_UF is well-typed, correct arity, etc. + Assert(formal != node.end()); + substitutions.addSubstitution(*formal, *arg); + } + return RewriteResponse(REWRITE_DONE, substitutions.apply(lambda[1])); + } return RewriteResponse(REWRITE_DONE, node); } @@ -49,7 +64,22 @@ public: if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) { if(node[0] == node[1]) { return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); + } else if(node[0].isConst() && node[1].isConst()) { + // uninterpreted constants are all distinct + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false)); + } + } + if(node.getKind() == kind::APPLY_UF && node.getOperator().getKind() == kind::LAMBDA) { + // resolve away the lambda + context::Context fakeContext; + theory::SubstitutionMap substitutions(&fakeContext); + TNode lambda = node.getOperator(); + for(TNode::iterator formal = lambda[0].begin(), arg = node.begin(); formal != lambda[0].end(); ++formal, ++arg) { + // typechecking should ensure that the APPLY_UF is well-typed, correct arity, etc. + Assert(formal != node.end()); + substitutions.addSubstitution(*formal, *arg); } + return RewriteResponse(REWRITE_DONE, substitutions.apply(lambda[1])); } return RewriteResponse(REWRITE_DONE, node); } |