diff options
Diffstat (limited to 'src/theory/arith/nl/nl_model.h')
| -rw-r--r-- | src/theory/arith/nl/nl_model.h | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index 1e6f6c8f3..dcbd9cce7 100644 --- a/src/theory/arith/nl/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -166,22 +166,6 @@ class NlModel void setUsedApproximate(); /** Did we use an approximation during this check? */ bool usedApproximate() const; - /** - * This states that formula n is a tautology (satisfied in all models). - * We call this on internally generated lemmas. This method computes a - * set of literals that are implied by n, that are hence tautological - * as well, such as: - * l_pi <= real.pi <= u_pi (pi approximations) - * sin(x) = -1*sin(-x) - * where these literals are internally generated for the purposes - * of guiding the models of the linear solver. - * - * TODO (cvc4-projects #113: would be helpful if we could do this even - * more aggressively by ignoring all internally generated literals. - * - * Tautological literals do not need be checked during checkModel. - */ - void addTautology(Node n); //------------------------------ end recording model substitutions and bounds /** @@ -334,8 +318,6 @@ class NlModel std::unordered_map<Node, Node, NodeHashFunction> d_check_model_solved; /** did we use an approximation on this call to last-call effort? */ bool d_used_approx; - /** the set of all tautological literals */ - std::unordered_set<Node, NodeHashFunction> d_tautology; }; /* class NlModel */ } // namespace nl |