diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-24 23:23:34 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-24 23:23:34 +0000 |
commit | 80afd586eb0865efcc38aa14833d682f1b7cc27f (patch) | |
tree | aac37b28e0330bf3b72083e979ae94ee71918771 /src/theory | |
parent | 3619c784bd5dd4b91ab0a2ad429ea145636d3424 (diff) |
* disallow internal uses of mkVar() (you have to mkSkolem())
* add support for mkBoundVar() (BOUND_VAR_LISTs in quantifiers must be bound vars)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/dio_solver.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_instantiator.cpp | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_model.cpp | 2 | ||||
-rw-r--r-- | src/theory/builtin/kinds | 3 | ||||
-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 | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers_type_rules.h | 4 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 2 | ||||
-rw-r--r-- | src/theory/unconstrained_simplifier.cpp | 2 |
14 files changed, 20 insertions, 19 deletions
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index e3eae88b3..83ba49257 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->mkVar(curr->integerType()); + return curr->mkSkolem(curr->integerType()); } DioSolver::DioSolver(context::Context* ctxt) : diff --git a/src/theory/arith/theory_arith_instantiator.cpp b/src/theory/arith/theory_arith_instantiator.cpp index 1682897ae..51e3a6638 100644 --- a/src/theory/arith/theory_arith_instantiator.cpp +++ b/src/theory/arith/theory_arith_instantiator.cpp @@ -412,7 +412,7 @@ Node InstantiatorTheoryArith::getDelta( Node n ){ if( it==d_deltas.end() ){ std::ostringstream os; os << "delta_" << d_deltas.size(); - Node delta = NodeManager::currentNM()->mkVar( os.str(), n.getType() ); + Node delta = NodeManager::currentNM()->mkSkolem( os.str(), n.getType() ); d_deltas[ n.getType() ] = delta; Node gt = NodeManager::currentNM()->mkNode( GT, delta, NodeManager::currentNM()->mkConst( Rational(0) ) ); //add split diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 4f2497d2b..4beab2d61 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -694,7 +694,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->mkVar(indexType); + Node newk = nm->mkSkolem(indexType); Dump.declareVar(newk.toExpr(), "an extensional lemma index variable from the theory of arrays"); d_diseqCache[fact] = newk; diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp index 7a574fac1..5c969060d 100644 --- a/src/theory/arrays/theory_arrays_model.cpp +++ b/src/theory/arrays/theory_arrays_model.cpp @@ -29,7 +29,7 @@ using namespace CVC4::theory::arrays; ArrayModel::ArrayModel( Node arr, quantifiers::FirstOrderModel* m ) : d_model( m ), d_arr( arr ){ Assert( arr.getKind()!=STORE ); //look at ground assertions - Node sel = NodeManager::currentNM()->mkNode( SELECT, arr, NodeManager::currentNM()->mkVar( arr.getType().getArrayIndexType() ) ); + Node sel = NodeManager::currentNM()->mkNode( SELECT, arr, NodeManager::currentNM()->mkSkolem( arr.getType().getArrayIndexType() ) ); Node sel_op = sel.getOperator(); //FIXME: easier way to do this? for( size_t i=0; i<d_model->getTermDatabase()->d_op_map[ sel_op ].size(); i++ ){ Node n = d_model->getTermDatabase()->d_op_map[ sel_op ][i]; diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 285eb651f..48fe4d84a 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -293,8 +293,9 @@ parameterized APPLY FUNCTION 0: "defined function application" operator EQUAL 2 "equality" operator DISTINCT 2: "disequality" -variable SKOLEM "skolem var" variable VARIABLE "variable" +variable BOUND_VARIABLE "bound variable" +variable SKOLEM "skolem var" operator TUPLE 1: "a tuple" constant TYPE_CONSTANT \ diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index ef7078624..68d9e8702 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -152,7 +152,7 @@ public: } inline static Node mkGroundTerm(TypeNode type) { Assert(type.getKind() == kind::SORT_TYPE); - return NodeManager::currentNM()->mkVar( type ); + return NodeManager::currentNM()->mkSkolem( type ); } };/* class SortProperties */ diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index a0d418c4b..8349a1479 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->mkVar(nm->mkBitVectorType(size)); + return nm->mkSkolem(nm->mkBitVectorType(size)); } inline Node mkAnd(std::vector<TNode>& children) { diff --git a/src/theory/ite_simplifier.cpp b/src/theory/ite_simplifier.cpp index ab8f159a9..6eb777ad5 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()->mkVar(t); + Node var = NodeManager::currentNM()->mkSkolem(t); d_simpVars[t] = var; return var; } diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 2260e86d3..a194336fb 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -236,7 +236,7 @@ Node TheoryModel::getNewDomainValue( TypeNode tn ){ }while( true ); }else{ //otherwise must make a variable FIXME: how to make constants for other sorts? - //return NodeManager::currentNM()->mkVar( tn ); + //return NodeManager::currentNM()->mkSkolem( tn ); return Node::null(); } } @@ -374,7 +374,7 @@ Node DefaultModel::getInterpretedValue( TNode n ){ default_v = v; } if( default_v.isNull() ){ - default_v = getInterpretedValue( NodeManager::currentNM()->mkVar( type.getRangeType() ) ); + default_v = getInterpretedValue( NodeManager::currentNM()->mkSkolem( type.getRangeType() ) ); } ufmt.setDefaultValue( this, default_v ); ufmt.simplify(); diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 800fa910c..e928010b6 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()->mkVar( ss.str(), typ ); + Node op = NodeManager::currentNM()->mkSkolem( ss.str(), typ ); std::vector< Node > predArgs; predArgs.push_back( op ); predArgs.insert( predArgs.end(), activeArgs.begin(), activeArgs.end() ); @@ -473,7 +473,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ //if( std::find( args.begin(), args.end(), body[0][i] )!=args.end() ){ terms.push_back( body[0][i] ); - subs.push_back( NodeManager::currentNM()->mkVar( body[0][i].getType() ) ); + subs.push_back( NodeManager::currentNM()->mkSkolem( body[0][i].getType() ) ); } args.insert( args.end(), subs.begin(), subs.end() ); }else{ @@ -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()->mkVar( typ ); + Node op = NodeManager::currentNM()->mkSkolem( typ ); 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 e1cd7e42c..cc74e3e76 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()->mkVar( ss.str(), tn ); + mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn ); }else{ mbt = d_type_map[ tn ][ 0 ]; } @@ -342,7 +342,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()->mkVar( tn ); + d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( tn ); }else{ d_free_vars[tn] = d_type_map[ tn ][ 0 ]; } diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index ceec36d7b..50d5a8142 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -73,8 +73,8 @@ struct QuantifierBoundVarListTypeRule { Assert(n.getKind() == kind::BOUND_VAR_LIST ); if( check ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( n[i].getKind()!=kind::VARIABLE ){ - throw TypeCheckingExceptionPrivate(n, "argument of bound var list is not variable"); + if( n[i].getKind()!=kind::BOUND_VARIABLE ){ + throw TypeCheckingExceptionPrivate(n, "argument of bound var list is not bound variable"); } } } diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 2ee8b6c93..f0b386cae 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1048,7 +1048,7 @@ Node StrongSolverTheoryUf::ConflictFind::getCardinalityLemma(){ std::stringstream ss; ss << Expr::setlanguage(options::outputLanguage()); ss << "t_" << d_type; - d_cardinality_lemma_term = NodeManager::currentNM()->mkVar( ss.str(), d_type ); + d_cardinality_lemma_term = NodeManager::currentNM()->mkSkolem( ss.str(), d_type ); } Node lem = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, d_cardinality_lemma_term, NodeManager::currentNM()->mkConst( Rational( d_cardinality ) ) ); diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index 58254df33..c23a72c91 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -93,7 +93,7 @@ void UnconstrainedSimplifier::visitAll(TNode assertion) Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var) { - Node n = NodeManager::currentNM()->mkVar(t); + Node n = NodeManager::currentNM()->mkSkolem(t); Dump.declareVar(n.toExpr(), "a new var introduced because of unconstrained variable " + var.toString()); return n; } |