mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 09:55:19 +00:00
update comment
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
9d82c1d8a9
commit
09ee60ccce
|
@ -307,13 +307,13 @@ namespace smt {
|
|||
|
||||
/**
|
||||
\brief Return a reference to smt::context.
|
||||
This is a temporary hack to support user theories.
|
||||
TODO: remove this hack.
|
||||
We need to revamp user theories too.
|
||||
This breaks abstractions.
|
||||
|
||||
It is currently used by the opt-solver
|
||||
to access optimization services from arithmetic solvers
|
||||
and to ensure that the solver has registered PB theory solver.
|
||||
|
||||
This method breaks the abstraction barrier.
|
||||
|
||||
\warning We should not use this method
|
||||
\warning This method should not be used in new code.
|
||||
*/
|
||||
context & get_context();
|
||||
};
|
||||
|
|
Loading…
Reference in a new issue