summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/builtin/kinds1
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h5
-rw-r--r--src/theory/model.cpp2
-rw-r--r--src/theory/substitutions.cpp16
-rw-r--r--src/theory/theory_engine.cpp5
-rw-r--r--src/theory/uf/theory_uf.cpp26
-rw-r--r--src/theory/uf/theory_uf_model.cpp4
-rw-r--r--src/theory/uf/theory_uf_model.h6
-rw-r--r--src/theory/uf/theory_uf_rewriter.h30
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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback