diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-18 10:01:17 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-18 10:01:17 -0600 |
| commit | 7d4c7be8cbe1ac3b68c3bb5e2b08143f8324b5a1 (patch) | |
| tree | cf80f5c45a6dc4b13256009d883e4407a718acb5 /src/api/cvc4cpp.cpp | |
| parent | 879bc5c29cbfc8ebcfe69fcc9316dfdb1361ff1f (diff) | |
Simplify internal API for sygus (#5687)
This makes simplifications to the internal sygus API now that the SmtEngine interface is independent of parsing.
Diffstat (limited to 'src/api/cvc4cpp.cpp')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 8044508c7..b11a01628 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -5615,7 +5615,7 @@ Term Solver::mkSygusVar(Sort sort, const std::string& symbol) const Node res = getNodeManager()->mkBoundVar(symbol, *sort.d_type); (void)res.getType(true); /* kick off type checking */ - d_smtEngine->declareSygusVar(symbol, res, *sort.d_type); + d_smtEngine->declareSygusVar(res); return Term(this, res); @@ -5740,7 +5740,7 @@ Term Solver::synthFunHelper(const std::string& symbol, std::vector<Node> bvns = termVectorToNodes(boundVars); d_smtEngine->declareSynthFun( - symbol, fun, g == nullptr ? funType : *g->resolve().d_type, isInv, bvns); + fun, g == nullptr ? funType : *g->resolve().d_type, isInv, bvns); return Term(this, fun); |