diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/dio_solver.cpp | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 4 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 2 | ||||
-rw-r--r-- | src/theory/ite_simplifier.cpp | 2 | ||||
-rw-r--r-- | src/theory/model.cpp | 6 | ||||
-rw-r--r-- | src/theory/model.h | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 6 | ||||
-rw-r--r-- | src/theory/rep_set.cpp | 2 | ||||
-rw-r--r-- | src/theory/rewriterules/theory_rewriterules.cpp | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 6 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 2 | ||||
-rw-r--r-- | src/theory/unconstrained_simplifier.cpp | 3 |
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; } |