summaryrefslogtreecommitdiff
path: root/src/parser/parser.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/parser.h')
-rw-r--r--src/parser/parser.h12
1 files changed, 7 insertions, 5 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 7941cfdd5..b5dc83902 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -808,7 +808,7 @@ public:
inline SymbolTable* getSymbolTable() const {
return d_symtab;
}
-
+
//------------------------ operator overloading
/** is this function overloaded? */
bool isOverloadedFunction(api::Term fun)
@@ -822,7 +822,8 @@ public:
*/
api::Term getOverloadedConstantForType(const std::string& name, api::Sort t)
{
- return d_symtab->getOverloadedConstantForType(name, t.getType());
+ return api::Term(d_solver,
+ d_symtab->getOverloadedConstantForType(name, t.getType()));
}
/**
@@ -833,8 +834,9 @@ public:
api::Term getOverloadedFunctionForTypes(const std::string& name,
std::vector<api::Sort>& argTypes)
{
- return d_symtab->getOverloadedFunctionForTypes(
- name, api::sortVectorToTypes(argTypes));
+ return api::Term(d_solver,
+ d_symtab->getOverloadedFunctionForTypes(
+ name, api::sortVectorToTypes(argTypes)));
}
//------------------------ end operator overloading
/**
@@ -845,7 +847,7 @@ public:
* SMT-LIB 2.6 or higher), or otherwise calling the solver to construct
* the string.
*/
- Expr mkStringConstant(const std::string& s);
+ api::Term mkStringConstant(const std::string& s);
private:
/** ad-hoc string escaping
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback