diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 16:22:19 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 16:22:26 -0500 |
commit | 2c0482cfb9b8164670cf56187e127d38c5d05bcf (patch) | |
tree | 804f7806944b9175fdaea8cc919566ca302ddf09 /src/theory/arith/nonlinear_extension.h | |
parent | 0e513c05b2e0ae3b8e2d08514ccb8007258f963b (diff) |
Merge ntExt branch. Adds support for transcendental functions. Refactoring of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.
Diffstat (limited to 'src/theory/arith/nonlinear_extension.h')
-rw-r--r-- | src/theory/arith/nonlinear_extension.h | 78 |
1 files changed, 72 insertions, 6 deletions
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index dc93046c0..1a19eb67a 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -86,17 +86,17 @@ class NonlinearExtension { // Check assertions for consistency in the effort LAST_CALL with a subset of // the assertions, false_asserts, evaluate to false in the current model. void checkLastCall(const std::vector<Node>& assertions, - const std::set<Node>& false_asserts); - - // Returns a vector containing a split on whether each term is 0 or not for - // those terms that have not been split on in the current context. - std::vector<Node> splitOnZeros(const std::vector<Node>& terms); + const std::set<Node>& false_asserts, + const std::vector<Node>& xts); static bool isArithKind(Kind k); static Node mkLit(Node a, Node b, int status, int orderType = 0); static Node mkAbs(Node a); + static Node mkValidPhase(Node a, Node pi); + static Node mkBounded( Node l, Node a, Node u ); static Kind joinKinds(Kind k1, Kind k2); static Kind transKinds(Kind k1, Kind k2); + static bool isTranscendentalKind(Kind k); Node mkMonomialRemFactor(Node n, const NodeMultiset& n_exp_rem) const; // register monomial @@ -171,6 +171,9 @@ class NonlinearExtension { // cache of all lemmas sent NodeSet d_lemmas; NodeSet d_zero_split; + + // literals with Skolems (need not be satisfied by model) + NodeSet d_skolem_atoms; // utilities Node d_zero; @@ -197,8 +200,71 @@ class NonlinearExtension { std::map<Node, Node> d_mv[2]; // ordering, stores variables and 0,1,-1 - std::map<unsigned, NodeMultiset> d_order_vars; + std::map<Node, unsigned> d_order_vars; std::vector<Node> d_order_points; + + //transcendent functions + std::map<Node, Node> d_trig_base; + std::map<Node, bool> d_trig_is_base; + std::map< Node, bool > d_tf_initial_refine; + Node d_pi; + Node d_pi_2; + Node d_pi_neg_2; + Node d_pi_neg; + Node d_pi_bound[2]; + + void mkPi(); + void getCurrentPiBounds( std::vector< Node >& lemmas ); +private: + //per last-call effort check + + //information about monomials + std::vector< Node > d_ms; + std::vector< Node > d_ms_vars; + std::map<Node, bool> d_ms_proc; + std::vector<Node> d_mterms; + //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; + // term -> coeff -> rhs -> ( status, exp, b ), + // where we have that : exp => ( coeff * term <status> rhs ) + // b is true if degree( term ) >= degree( rhs ) + std::map<Node, std::map<Node, std::map<Node, Kind> > > d_ci; + std::map<Node, std::map<Node, std::map<Node, Node> > > d_ci_exp; + std::map<Node, std::map<Node, std::map<Node, bool> > > d_ci_max; + + //information about transcendental functions + std::map< Kind, std::map< Node, Node > > d_tf_rep_map; + + // factor skolems + std::map< Node, Node > d_factor_skolem; + Node getFactorSkolem( Node n, std::vector< Node >& lemmas ); + + Node getTaylor( Node tf, Node x, unsigned n, std::vector< Node >& lemmas ); +private: + // Returns a vector containing a split on whether each term is 0 or not for + // those terms that have not been split on in the current context. + std::vector<Node> checkSplitZero(); + + std::vector<Node> checkMonomialSign(); + + std::vector<Node> checkMonomialMagnitude( unsigned c ); + + std::vector<Node> checkMonomialInferBounds( std::vector<Node>& nt_lemmas, + const std::set<Node>& false_asserts ); + + std::vector<Node> checkFactoring( const std::set<Node>& false_asserts ); + + std::vector<Node> checkMonomialInferResBounds(); + + std::vector<Node> checkTangentPlanes(); + + std::vector<Node> checkTranscendentalInitialRefine(); + + std::vector<Node> checkTranscendentalMonotonic(); }; /* class NonlinearExtension */ } // namespace arith |