diff options
author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-11-05 17:13:44 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-05 17:13:44 -0600 |
commit | ac8b2593bed81125cb1a494e4b8311e517d0e3d9 (patch) | |
tree | eadc038a8e3700fdf96f52f41ac6a99f3090bf9b /src/theory/arith/nl/nonlinear_extension.cpp | |
parent | d301b5175e39f82df9c179be1da7eaea892f7795 (diff) |
Remove mkSingleton from the API (#5366)
This PR removes mkSingleton from the API after removing subtyping from set theory and introducing mkInteger to the API.
Instead the user needs to use Solver::mkTerm(api::SINGLETON, element) where element has the right type.
Internally NodeManager::mkSingleton(type, element) is still needed to determine the type of the set.
Other changes:
Renamed Solver::mkTerm(Op op, .. functions to Solver::mkTermFromOp(Op op, ...
Added mkTermFromOp to the python API
Diffstat (limited to 'src/theory/arith/nl/nonlinear_extension.cpp')
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index f5e83c8f0..5bd02cf19 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -179,7 +179,6 @@ void NonlinearExtension::getAssertions(std::vector<Node>& assertions) useRelevance = true; } Valuation v = d_containing.getValuation(); - NodeManager* nm = NodeManager::currentNM(); BoundInference bounds; |