summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/dio_solver.cpp2
-rw-r--r--src/theory/arrays/theory_arrays.cpp4
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h2
-rw-r--r--src/theory/bv/theory_bv_utils.h2
-rw-r--r--src/theory/ite_simplifier.cpp2
-rw-r--r--src/theory/model.cpp6
-rw-r--r--src/theory/model.h4
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp4
-rw-r--r--src/theory/quantifiers/term_database.cpp6
-rw-r--r--src/theory/rep_set.cpp2
-rw-r--r--src/theory/rewriterules/theory_rewriterules.cpp2
-rw-r--r--src/theory/theory_engine.cpp6
-rw-r--r--src/theory/uf/theory_uf_strong_solver.cpp2
-rw-r--r--src/theory/unconstrained_simplifier.cpp3
14 files changed, 22 insertions, 25 deletions
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 83ba49257..c70bc911b 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -28,7 +28,7 @@ namespace arith {
inline Node makeIntegerVariable(){
NodeManager* curr = NodeManager::currentNM();
- return curr->mkSkolem(curr->integerType());
+ return curr->mkSkolem("intvar", curr->integerType(), "is an integer variable created by the dio solver");
}
DioSolver::DioSolver(context::Context* ctxt) :
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 0ec8e1384..e1f93158f 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -737,9 +737,7 @@ void TheoryArrays::check(Effort e) {
TNode k;
std::hash_map<TNode, Node, TNodeHashFunction>::iterator it = d_diseqCache.find(fact);
if (it == d_diseqCache.end()) {
- Node newk = nm->mkSkolem(indexType);
- Dump.declareVar(newk.toExpr(),
- "an extensional lemma index variable from the theory of arrays");
+ Node newk = nm->mkSkolem("array_ext_index_$$", indexType, "an extensional lemma index variable from the theory of arrays");
d_diseqCache[fact] = newk;
k = newk;
}
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 7bc1d956d..b7fd3c351 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -175,7 +175,7 @@ public:
}
inline static Node mkGroundTerm(TypeNode type) {
Assert(type.getKind() == kind::SORT_TYPE);
- return NodeManager::currentNM()->mkSkolem( type );
+ return NodeManager::currentNM()->mkSkolem("groundTerm_$$", type, "a ground term created for type " + type.toString());
}
};/* class SortProperties */
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 8349a1479..d20107958 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -68,7 +68,7 @@ inline Node mkFalse() {
inline Node mkVar(unsigned size) {
NodeManager* nm = NodeManager::currentNM();
- return nm->mkSkolem(nm->mkBitVectorType(size));
+ return nm->mkSkolem("bv_$$", nm->mkBitVectorType(size), "is a variable created by the theory of bitvectors");
}
inline Node mkAnd(std::vector<TNode>& children) {
diff --git a/src/theory/ite_simplifier.cpp b/src/theory/ite_simplifier.cpp
index 6eb777ad5..dd87557f2 100644
--- a/src/theory/ite_simplifier.cpp
+++ b/src/theory/ite_simplifier.cpp
@@ -148,7 +148,7 @@ Node ITESimplifier::getSimpVar(TypeNode t)
return (*it).second;
}
else {
- Node var = NodeManager::currentNM()->mkSkolem(t);
+ Node var = NodeManager::currentNM()->mkSkolem("iteSimp_$$", t, "is a variable resulting from ITE simplification");
d_simpVars[t] = var;
return var;
}
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 42654b74c..8aec39309 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -53,14 +53,14 @@ Node TheoryModel::getValue( TNode n ){
return getModelValue( nn );
}
-Expr TheoryModel::getValue( const Expr& expr ){
+Expr TheoryModel::getValue( Expr expr ){
Node n = Node::fromExpr( expr );
Node ret = getValue( n );
return ret.toExpr();
}
/** get cardinality for sort */
-Cardinality TheoryModel::getCardinality( const Type& t ){
+Cardinality TheoryModel::getCardinality( Type t ){
TypeNode tn = TypeNode::fromType( t );
//for now, we only handle cardinalities for uninterpreted sorts
if( tn.isSort() ){
@@ -373,7 +373,7 @@ Node DefaultModel::getInterpretedValue( TNode n ){
}
if( default_v.isNull() ){
//choose default value from model if none exists
- default_v = getInterpretedValue( NodeManager::currentNM()->mkSkolem( type.getRangeType() ) );
+ default_v = getInterpretedValue( NodeManager::currentNM()->mkSkolem( "defaultValue_$$", type.getRangeType(), "a default value term from model construction" ) );
}
ufmt.setDefaultValue( this, default_v );
ufmt.simplify();
diff --git a/src/theory/model.h b/src/theory/model.h
index 85f5dd31b..adf97df9e 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -115,9 +115,9 @@ public:
bool areDisequal( Node a, Node b );
public:
/** get value function for Exprs. */
- Expr getValue( const Expr& expr );
+ Expr getValue( Expr expr );
/** get cardinality for sort */
- Cardinality getCardinality( const Type& t );
+ Cardinality getCardinality( Type t );
/** to stream function */
void toStream( std::ostream& out );
public:
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index b0728de29..c6987a85a 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -384,7 +384,7 @@ Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBui
TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->booleanType() );
std::stringstream ss;
ss << "cnf_" << n.getKind() << "_" << n.getId();
- Node op = NodeManager::currentNM()->mkSkolem( ss.str(), typ );
+ Node op = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "was created by the quantifiers rewriter" );
std::vector< Node > predArgs;
predArgs.push_back( op );
predArgs.insert( predArgs.end(), activeArgs.begin(), activeArgs.end() );
@@ -486,7 +486,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
terms.push_back( body[0][i] );
//make the new function symbol
TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, body[0][i].getType() );
- Node op = NodeManager::currentNM()->mkSkolem( typ );
+ Node op = NodeManager::currentNM()->mkSkolem( "op_$$", typ, "was created by the quantifiers rewriter" );
std::vector< Node > funcArgs;
funcArgs.push_back( op );
funcArgs.insert( funcArgs.end(), args.begin(), args.end() );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index bd6b03a78..7b5d9e6e2 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -198,7 +198,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
std::stringstream ss;
ss << Expr::setlanguage(options::outputLanguage());
ss << "e_" << tn;
- mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn );
+ mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" );
Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl;
}else{
mbt = d_type_map[ tn ][ 0 ];
@@ -307,7 +307,7 @@ Node TermDb::getSkolemizedBody( Node f ){
if( d_skolem_body.find( f )==d_skolem_body.end() ){
std::vector< Node > vars;
for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
- Node skv = NodeManager::currentNM()->mkSkolem( f[0][i].getType() );
+ Node skv = NodeManager::currentNM()->mkSkolem( "skv_$$", f[0][i].getType(), "is a termdb-created skolemized body" );
d_skolem_constants[ f ].push_back( skv );
vars.push_back( f[0][i] );
}
@@ -343,7 +343,7 @@ Node TermDb::getFreeVariableForInstConstant( Node n ){
d_free_vars[tn] = NodeManager::currentNM()->mkConst( z );
}else{
if( d_type_map[ tn ].empty() ){
- d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( tn );
+ d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( "freevar_$$", tn, "is a free variable created by termdb" );
Trace("mkVar") << "FreeVar:: Make variable " << d_free_vars[tn] << " : " << tn << std::endl;
}else{
d_free_vars[tn] = d_type_map[ tn ][ 0 ];
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index aaca53464..4a5bb2247 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -112,7 +112,7 @@ void RepSetIterator::initialize(){
TypeNode tn = d_types[i];
if( tn.isSort() ){
if( !d_rep_set->hasType( tn ) ){
- Node var = NodeManager::currentNM()->mkSkolem( tn );
+ Node var = NodeManager::currentNM()->mkSkolem( "repSet_$$", tn, "is a variable created by the RepSetIterator" );
Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
d_rep_set->add( var );
}
diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp
index 5ffd4ac4a..f94a373d7 100644
--- a/src/theory/rewriterules/theory_rewriterules.cpp
+++ b/src/theory/rewriterules/theory_rewriterules.cpp
@@ -434,7 +434,7 @@ Node skolemizeBody( Node f ){
std::vector< Node > vars;
std::vector< Node > csts;
for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
- csts.push_back( NodeManager::currentNM()->mkSkolem( f[0][i].getType()) );
+ csts.push_back( NodeManager::currentNM()->mkSkolem( "skolem_$$", f[0][i].getType(), "is from skolemizing the body of a rewrite rule" ) );
vars.push_back( f[0][i] );
}
return f[ 1 ].substitute( vars.begin(), vars.end(),
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index c9fb36830..d69f43908 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -580,12 +580,12 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){
}
/* get model */
-TheoryModel* TheoryEngine::getModel(){
+TheoryModel* TheoryEngine::getModel() {
Debug("model") << "TheoryEngine::getModel()" << std::endl;
- if( d_logicInfo.isQuantified() ){
+ if( d_logicInfo.isQuantified() ) {
Debug("model") << "Get model from quantifiers engine." << std::endl;
return d_quantEngine->getModel();
- }else{
+ } else {
Debug("model") << "Get default model." << std::endl;
return d_curr_model;
}
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index de7061022..3f82a6948 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -921,7 +921,7 @@ void StrongSolverTheoryUf::SortRepModel::allocateCardinality( OutputChannel* out
//must generate new cardinality lemma term
std::stringstream ss;
ss << "_c_" << d_aloc_cardinality;
- Node var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type );
+ Node var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "is a cardinality lemma term" );
d_totality_terms[0].push_back( var );
Trace("mkVar") << "allocateCardinality, mkVar : " << var << " : " << d_type << std::endl;
//must be distinct from all other cardinality terms
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index c23a72c91..636e61a6d 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -93,8 +93,7 @@ void UnconstrainedSimplifier::visitAll(TNode assertion)
Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var)
{
- Node n = NodeManager::currentNM()->mkSkolem(t);
- Dump.declareVar(n.toExpr(), "a new var introduced because of unconstrained variable " + var.toString());
+ Node n = NodeManager::currentNM()->mkSkolem("unconstrained_$$", t, "a new var introduced because of unconstrained variable " + var.toString());
return n;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback