diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-16 12:38:08 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-16 12:38:08 +0100 |
commit | cb54542531904204fc147015469d54c6750ab73b (patch) | |
tree | fa29a40d7a2761101bf2ce415e9682a9c238db6e /src/parser/smt2/smt2.h | |
parent | 338ec2ee86e16423b265ba9bfc036606223f846f (diff) |
Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding declare-var vs synth-fun arguments. Handle ground properties in sythesis conjectures.
Diffstat (limited to 'src/parser/smt2/smt2.h')
-rw-r--r-- | src/parser/smt2/smt2.h | 30 |
1 files changed, 22 insertions, 8 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 50edc3311..35842f308 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -187,41 +187,55 @@ public: while(d_nextSygusFun < d_sygusFuns.size()) { std::pair<std::string, Expr> p = d_sygusFuns[d_nextSygusFun]; std::string fun = p.first; + Debug("parser-sygus") << "Sygus : define fun " << fun << std::endl; Expr eval = p.second; FunctionType evalType = eval.getType(); std::vector<Type> argTypes = evalType.getArgTypes(); Type rangeType = evalType.getRangeType(); + Debug("parser-sygus") << "...eval type : " << evalType << ", #args=" << argTypes.size() << std::endl; // first make the function type + std::vector<Expr> sygusVars; std::vector<Type> funType; for(size_t j = 1; j < argTypes.size(); ++j) { funType.push_back(argTypes[j]); + std::stringstream ss; + ss << fun << "_v_" << j; + sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), argTypes[j])); } Type funt = getExprManager()->mkFunctionType(funType, rangeType); + Debug("parser-sygus") << "...eval function type : " << funt << std::endl; // copy the bound vars + /* std::vector<Expr> sygusVars; - std::vector<Type> types; + //std::vector<Type> types; for(size_t i = 0; i < d_sygusVars.size(); ++i) { std::stringstream ss; ss << d_sygusVars[i]; Type type = d_sygusVars[i].getType(); sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type)); - types.push_back(type); + //types.push_back(type); } - - Type t = getExprManager()->mkFunctionType(types, rangeType); - Expr lambda = mkFunction(fun, t, ExprManager::VAR_FLAG_DEFINED); + Debug("parser-sygus") << "...made vars, #vars=" << sygusVars.size() << std::endl; + */ + + //Type t = getExprManager()->mkFunctionType(types, rangeType); + //Debug("parser-sygus") << "...function type : " << t << std::endl; + + Expr lambda = mkFunction(fun, funt, ExprManager::VAR_FLAG_DEFINED); + Debug("parser-sygus") << "...made function : " << lambda << std::endl; std::vector<Expr> applyv; Expr funbv = getExprManager()->mkBoundVar(std::string("f") + fun, argTypes[0]); d_sygusFunSymbols.push_back(funbv); applyv.push_back(eval); applyv.push_back(funbv); - for(size_t i = 0; i < d_sygusVars.size(); ++i) { - applyv.push_back(d_sygusVars[i]); + for(size_t i = 0; i < sygusVars.size(); ++i) { + applyv.push_back(sygusVars[i]); } Expr apply = getExprManager()->mkExpr(kind::APPLY_UF, applyv); - Command* cmd = new DefineFunctionCommand(fun, lambda, d_sygusVars, apply); + Debug("parser-sygus") << "...made apply " << apply << std::endl; + Command* cmd = new DefineFunctionCommand(fun, lambda, sygusVars, apply); preemptCommand(cmd); ++d_nextSygusFun; |