diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-16 14:05:23 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-16 14:05:23 -0500 |
commit | 00785f2b65eb9dfdfbfcd8b58b0cc57255919c31 (patch) | |
tree | 3e737a65502c2633d525b4d7344a3ae6f9a3c2ed /src | |
parent | 46857bda6c6bb6db3481514c8cdee3ecbadb3301 (diff) |
Minor fixes, always expand applications of lambdas at preprocess.
Diffstat (limited to 'src')
-rw-r--r-- | src/parser/smt2/Smt2.g | 7 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 68 |
2 files changed, 43 insertions, 32 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index bb7ac9fb8..c52f2ad51 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2074,10 +2074,9 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] if( !type.isConstructor() ){ PARSER_STATE->parseError("Pattern must be application of a constructor or a variable."); } - //TODO - //if( Datatype::datatypeOf(f).isParametric() ){ - // type = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getSpecializedConstructorType(expr.getType()); - //} + if( Datatype::datatypeOf(f).isParametric() ){ + type = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getSpecializedConstructorType(expr.getType()); + } match_ptypes = ((ConstructorType)type).getArgTypes(); } //arguments diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 306843c81..998967c5e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2305,7 +2305,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF } // otherwise expand it - bool doExpand = ( k == kind::APPLY && n.getOperator().getKind() != kind::LAMBDA ); + bool doExpand = k == kind::APPLY; if( !doExpand ){ if( options::macrosQuant() ){ //expand if we have inferred an operator corresponds to a defined function @@ -2313,35 +2313,47 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF } } if (doExpand) { - // application of a user-defined symbol - TNode func = n.getOperator(); - SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(func); - if(i == d_smt.d_definedFunctions->end()) { - throw TypeCheckingException(n.toExpr(), string("Undefined function: `") + func.toString() + "'"); - } - DefinedFunction def = (*i).second; - vector<Node> formals = def.getFormals(); - - if(Debug.isOn("expand")) { - Debug("expand") << "found: " << n << endl; - Debug("expand") << " func: " << func << endl; - string name = func.getAttribute(expr::VarNameAttr()); - Debug("expand") << " : \"" << name << "\"" << endl; - } - if(Debug.isOn("expand")) { - Debug("expand") << " defn: " << def.getFunction() << endl - << " ["; - if(formals.size() > 0) { - copy( formals.begin(), formals.end() - 1, - ostream_iterator<Node>(Debug("expand"), ", ") ); - Debug("expand") << formals.back(); + vector<Node> formals; + TNode fm; + if( n.getOperator().getKind() == kind::LAMBDA ){ + TNode op = n.getOperator(); + // lambda + for( unsigned i=0; i<op[0].getNumChildren(); i++ ){ + formals.push_back( op[0][i] ); + } + fm = op[1]; + }else{ + // application of a user-defined symbol + TNode func = n.getOperator(); + SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(func); + if(i == d_smt.d_definedFunctions->end()) { + throw TypeCheckingException(n.toExpr(), string("Undefined function: `") + func.toString() + "'"); + } + DefinedFunction def = (*i).second; + formals = def.getFormals(); + + if(Debug.isOn("expand")) { + Debug("expand") << "found: " << n << endl; + Debug("expand") << " func: " << func << endl; + string name = func.getAttribute(expr::VarNameAttr()); + Debug("expand") << " : \"" << name << "\"" << endl; + } + if(Debug.isOn("expand")) { + Debug("expand") << " defn: " << def.getFunction() << endl + << " ["; + if(formals.size() > 0) { + copy( formals.begin(), formals.end() - 1, + ostream_iterator<Node>(Debug("expand"), ", ") ); + Debug("expand") << formals.back(); + } + Debug("expand") << "]" << endl + << " " << def.getFunction().getType() << endl + << " " << def.getFormula() << endl; } - Debug("expand") << "]" << endl - << " " << def.getFunction().getType() << endl - << " " << def.getFormula() << endl; - } - TNode fm = def.getFormula(); + fm = def.getFormula(); + } + Node instance = fm.substitute(formals.begin(), formals.end(), n.begin(), n.end()); Debug("expand") << "made : " << instance << endl; |