diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-27 15:03:31 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-27 15:03:31 -0500 |
| commit | a1d554d9e401ff0cc860b88c2f082ab08a46542f (patch) | |
| tree | 232c4ceaa038a4b7b173a930383cea2bd00f787e /src/theory/arith/nonlinear_extension.h | |
| parent | 79296a59e00efe5b00496a251005d01dbeddcd48 (diff) | |
Simplify tangent plane direction (#1824)
Diffstat (limited to 'src/theory/arith/nonlinear_extension.h')
| -rw-r--r-- | src/theory/arith/nonlinear_extension.h | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index 1264a0fb8..c7e6b2b2a 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -487,9 +487,8 @@ private: //list of monomials with factors whose model value is non-constant in model // e.g. y*cos( x ) std::map<Node, bool> d_m_nconst_factor; - // If ( m, p1, true ), then it would help satisfiability if m were ( > - // if p1=true, < if p1=false ) - std::map<Node, std::map<bool, bool> > d_tplane_refine_dir; + /** the set of monomials we should apply tangent planes to */ + std::unordered_set<Node, NodeHashFunction> d_tplane_refine; // term -> coeff -> rhs -> ( status, exp, b ), // where we have that : exp => ( coeff * term <status> rhs ) // b is true if degree( term ) >= degree( rhs ) |