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/smt | |
parent | 46857bda6c6bb6db3481514c8cdee3ecbadb3301 (diff) |
Minor fixes, always expand applications of lambdas at preprocess.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 68 |
1 files changed, 40 insertions, 28 deletions
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; |