diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-22 12:56:13 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-22 12:56:13 -0600 |
commit | 047b8f69db1ab46ad68a2693565066f2a8d40b29 (patch) | |
tree | e20432814db99d98f179117bef6c6195ddc5801e /src/theory/arith/nonlinear_extension.h | |
parent | b2f4485e9d079806da4e95983dc849b1741c7823 (diff) |
Transcendental tangent planes utilities (#1288)
Diffstat (limited to 'src/theory/arith/nonlinear_extension.h')
-rw-r--r-- | src/theory/arith/nonlinear_extension.h | 525 |
1 files changed, 481 insertions, 44 deletions
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index dcaa91dc5..7c41fa096 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -23,6 +23,7 @@ #include <map> #include <queue> #include <set> +#include <unordered_map> #include <utility> #include <vector> @@ -42,25 +43,109 @@ namespace arith { typedef std::map<Node, unsigned> NodeMultiset; +// TODO : refactor/document this class (#1287) +/** Non-linear extension class + * + * This class implements model-based refinement schemes + * for non-linear arithmetic, described in: + * + * - "Invariant Checking of NRA Transition Systems + * via Incremental Reduction to LRA with EUF" by + * Cimatti et al., TACAS 2017. + * + * - Section 5 of "Desiging Theory Solvers with + * Extensions" by Reynolds et al., FroCoS 2017. + * + * - "Satisfiability Modulo Transcendental + * Functions via Incremental Linearization" by Cimatti + * et al., CADE 2017. + * + * It's main functionality is a check(...) method, + * which is called by TheoryArithPrivate either: + * (1) at full effort with no conflicts or lemmas emitted, + * or + * (2) at last call effort. + * In this method, this class calls d_out->lemma(...) + * for valid arithmetic theory lemmas, based on the current set of assertions, + * where d_out is the output channel of TheoryArith. + */ class NonlinearExtension { public: NonlinearExtension(TheoryArith& containing, eq::EqualityEngine* ee); ~NonlinearExtension(); + /** Get current substitution + * + * This function and the one below are + * used for context-dependent + * simplification, see Section 3.1 of + * "Designing Theory Solvers with Extensions" + * by Reynolds et al. FroCoS 2017. + * + * effort : an identifier indicating the stage where + * we are performing context-dependent simplification, + * vars : a set of arithmetic variables. + * + * This function populates subs and exp, such that for 0 <= i < vars.size(): + * ( exp[vars[i]] ) => vars[i] = subs[i] + * where exp[vars[i]] is a set of assertions + * that hold in the current context. We call { vars -> subs } a "derivable + * substituion" (see Reynolds et al. FroCoS 2017). + */ bool getCurrentSubstitution(int effort, const std::vector<Node>& vars, std::vector<Node>& subs, std::map<Node, std::vector<Node> >& exp); - + /** Is the term n in reduced form? + * + * Used for context-dependent simplification. + * + * effort : an identifier indicating the stage where + * we are performing context-dependent simplification, + * on : the original term that we reduced to n, + * exp : an explanation such that ( exp => on = n ). + * + * We return a pair ( b, exp' ) such that + * if b is true, then: + * n is in reduced form + * if exp' is non-null, then ( exp' => on = n ) + * The second part of the pair is used for constructing + * minimal explanations for context-dependent simplifications. + */ std::pair<bool, Node> isExtfReduced(int effort, Node n, Node on, const std::vector<Node>& exp) const; + /** Check at effort level e. + * + * This call may result in (possibly multiple) + * calls to d_out->lemma(...) where d_out + * is the output channel of TheoryArith. + */ void check(Theory::Effort e); + /** Does this class need a call to check(...) at last call effort? */ bool needsCheckLastEffort() const { return d_needsLastCall; } + /** Compare arithmetic terms i and j based an ordering. + * + * orderType = 0 : compare concrete model values + * orderType = 1 : compare abstract model values + * orderType = 2 : compare abs of concrete model values + * orderType = 3 : compare abs of abstract model values + * TODO (#1287) make this an enum? + * + * For definitions of concrete vs abstract model values, + * see computeModelValue below. + */ int compare(Node i, Node j, unsigned orderType) const; + /** Compare constant rationals i and j based an ordering. + * orderType is the same as above. + */ int compare_value(Node i, Node j, unsigned orderType) const; + private: + /** returns true if the multiset containing the + * factors of monomial a is a subset of the multiset + * containing the factors of monomial b. + */ bool isMonomialSubset(Node a, Node b) const; void registerMonomialSubset(Node a, Node b); - private: typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; // monomial information (context-independent) @@ -83,13 +168,20 @@ class NonlinearExtension { Kind d_type; }; /* struct ConstraintInfo */ - // Check assertions for consistency in the effort LAST_CALL with a subset of - // the assertions, false_asserts, evaluate to false in the current model. - // Returns the number of lemmas added on the output channel. + /** check last call + * + * Check assertions for consistency in the effort LAST_CALL with a subset of + * the assertions, false_asserts, that evaluate to false in the current model. + * + * xts : the list of (non-reduced) extended terms in the current context. + * + * This method returns the number of lemmas added on the output channel of + * TheoryArith. + */ int checkLastCall(const std::vector<Node>& assertions, const std::set<Node>& false_asserts, const std::vector<Node>& xts); - + //---------------------------------------term utilities static bool isArithKind(Kind k); static Node mkLit(Node a, Node b, int status, int orderType = 0); static Node mkAbs(Node a); @@ -99,53 +191,141 @@ class NonlinearExtension { static Kind transKinds(Kind k1, Kind k2); static bool isTranscendentalKind(Kind k); Node mkMonomialRemFactor(Node n, const NodeMultiset& n_exp_rem) const; + //---------------------------------------end term utilities - // register monomial + /** register monomial */ void registerMonomial(Node n); void setMonomialFactor(Node a, Node b, const NodeMultiset& common); void registerConstraint(Node atom); - // index = 0 : concrete, 1 : abstract + /** compute model value + * + * This computes model values for terms based on two semantics, a "concrete" + * semantics and an "abstract" semantics. + * + * index = 0 means compute the value of n based on its children recursively. + * (we call this its "concrete" value) + * index = 1 means lookup the value of n in the model. + * (we call this its "abstract" value) + * In other words, index = 1 treats multiplication terms and transcendental + * function applications as variables, whereas index = 0 computes their + * actual values. This is a key distinction used in the model-based + * refinement scheme in Cimatti et al. TACAS 2017. + * + * For example, if M( a ) = 2, M( b ) = 3, M( a * b ) = 5, then : + * + * computeModelValue( a*b, 0 ) = + * computeModelValue( a, 0 )*computeModelValue( b, 0 ) = 2*3 = 6 + * whereas: + * computeModelValue( a*b, 1 ) = 5 + */ Node computeModelValue(Node n, unsigned index = 0); - + /** returns the Node corresponding to the value of i in the + * type of order orderType, which is one of values + * described above ::compare(...). + */ Node get_compare_value(Node i, unsigned orderType) const; void assignOrderIds(std::vector<Node>& vars, NodeMultiset& d_order, unsigned orderType); - // Returns the subset of assertions that evaluate to false in the model. + /** Returns the subset of assertions whose concrete values are + * false in the model. + */ std::set<Node> getFalseInModel(const std::vector<Node>& assertions); - // status - // 0 : equal - // 1 : greater than or equal - // 2 : greater than - // -X : (less) - // in these functions we are iterating over variables of monomials - // initially : exp => ( oa = a ^ ob = b ) + /** In the following functions, status states a relationship + * between two arithmetic terms, where: + * 0 : equal + * 1 : greater than or equal + * 2 : greater than + * -X : (greater -> less) + * TODO (#1287) make this an enum? + */ + /** compute the sign of a. + * + * Calls to this function are such that : + * exp => ( oa = a ^ a <status> 0 ) + * + * This function iterates over the factors of a, + * where a_index is the index of the factor in a + * we are currently looking at. + * + * This function returns a status, which indicates + * a's relationship to 0. + * We add lemmas to lem of the form given by the + * lemma schema checkSign(...). + */ int compareSign(Node oa, Node a, unsigned a_index, int status, std::vector<Node>& exp, std::vector<Node>& lem); + /** compare monomials a and b + * + * Initially, a call to this function is such that : + * exp => ( oa = a ^ ob = b ) + * + * This function returns true if we can infer a valid + * arithmetic lemma of the form : + * P => abs( a ) >= abs( b ) + * where P is true and abs( a ) >= abs( b ) is false in the + * current model. + * + * This function is implemented by "processing" factors + * of monomials a and b until an inference of the above + * form can be made. For example, if : + * a = x*x*y and b = z*w + * Assuming we are trying to show abs( a ) >= abs( c ), + * then if abs( M( x ) ) >= abs( M( z ) ) where M is the current model, + * then we can add abs( x ) >= abs( z ) to our explanation, and + * mark one factor of x as processed in a, and + * one factor of z as processed in b. The number of processed factors of a + * and b are stored in a_exp_proc and b_exp_proc respectively. + * + * cmp_infers stores information that is helpful + * in discarding redundant inferences. For example, + * we do not want to infer abs( x ) >= abs( z ) if + * we have already inferred abs( x ) >= abs( y ) and + * abs( y ) >= abs( z ). + * It stores entries of the form (status,t1,t2)->F, + * which indicates that we constructed a lemma F that + * showed t1 <status> t2. + * + * We add lemmas to lem of the form given by the + * lemma schema checkMagnitude(...). + */ bool compareMonomial( Node oa, Node a, NodeMultiset& a_exp_proc, Node ob, Node b, NodeMultiset& b_exp_proc, std::vector<Node>& exp, std::vector<Node>& lem, std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers); + /** helper function for above + * + * The difference is the inputs a_index and b_index, which are the indices of + * children (factors) in monomials a and b which we are currently looking at. + */ bool compareMonomial( Node oa, Node a, unsigned a_index, NodeMultiset& a_exp_proc, Node ob, Node b, unsigned b_index, NodeMultiset& b_exp_proc, int status, std::vector<Node>& exp, std::vector<Node>& lem, std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers); + /** Check whether we have already inferred a relationship between monomials + * x and y based on the information in cmp_infers. This computes the + * transitive closure of the relation stored in cmp_infers. + */ bool cmp_holds(Node x, Node y, std::map<Node, std::map<Node, Node> >& cmp_infers, std::vector<Node>& exp, std::map<Node, bool>& visited); - + /** Is n entailed with polarity pol in the current context? */ bool isEntailed(Node n, bool pol); - // Potentially sends lem on the output channel if lem has not been sent on the - // output channel in this context. Returns the number of lemmas sent on the - // output channel. + /** flush lemmas + * + * Potentially sends lem on the output channel if lem has not been sent on the + * output channel in this context. Returns the number of lemmas sent on the + * output channel of TheoryArith. + */ int flushLemma(Node lem); - // Potentially sends lemmas to the output channel and clears lemmas. Returns - // the number of lemmas sent to the output channel. + /** Potentially sends lemmas to the output channel and clears lemmas. Returns + * the number of lemmas sent to the output channel. + */ int flushLemmas(std::vector<Node>& lemmas); // Returns the NodeMultiset for an existing monomial. @@ -176,12 +356,27 @@ class NonlinearExtension { // literals with Skolems (need not be satisfied by model) NodeSet d_skolem_atoms; - // utilities + /** commonly used terms */ Node d_zero; Node d_one; Node d_neg_one; Node d_true; Node d_false; + /** PI + * + * Note that PI is a (symbolic, non-constant) nullary operator. This is + * because its value cannot be computed exactly. We constraint PI to concrete + * lower and upper bounds stored in d_pi_bound below. + */ + Node d_pi; + /** PI/2 */ + Node d_pi_2; + /** -PI/2 */ + Node d_pi_neg_2; + /** -PI */ + Node d_pi_neg; + /** the concrete lower and upper bounds for PI */ + Node d_pi_bound[2]; // The theory of arithmetic containing this extension. TheoryArith& d_containing; @@ -197,7 +392,11 @@ class NonlinearExtension { std::vector<Node> d_constraints; // model values/orderings - // model values + /** cache of model values + * + * Stores the the concrete/abstract model values + * at indices 0 and 1 respectively. + */ std::map<Node, Node> d_mv[2]; // ordering, stores variables and 0,1,-1 @@ -208,11 +407,6 @@ class NonlinearExtension { 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 ); @@ -236,8 +430,14 @@ private: 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 + + /** transcendental function representative map + * + * For each transcendental function n = tf( x ), + * this stores ( n.getKind(), r ) -> n + * where r is the current representative of x + * in the equality engine assoiated with this class. + */ std::map< Kind, std::map< Node, Node > > d_tf_rep_map; // factor skolems @@ -246,29 +446,266 @@ private: // tangent plane bounds std::map< Node, std::map< Node, Node > > d_tangent_val_bound[4]; - - 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. + + /** secant points (sorted list) for transcendental functions + * + * This is used for tangent plane refinements for + * transcendental functions. This is the set + * "get-previous-secant-points" in "Satisfiability + * Modulo Transcendental Functions via Incremental + * Linearization" by Cimatti et al., CADE 2017, for + * each transcendental function application. + */ + std::unordered_map<Node, std::vector<Node>, NodeHashFunction> d_secant_points; + + /** get Taylor series of degree n for function fa centered around point fa[0]. + * + * Return value is ( P_{n,f(a)}( x ), R_{n+1,f(a)}( x ) ) where + * the first part of the pair is the Taylor series expansion : + * P_{n,f(a)}( x ) = sum_{i=0}^n (f^i( a )/i!)*(x-a)^i + * and the second part of the pair is the Taylor series remainder : + * R_{n+1,f(a),b}( x ) = (f^{n+1}( b )/(n+1)!)*(x-a)^{n+1} + * + * The above values are cached for each (f,n) for a fixed variable "a". + * To compute the Taylor series for fa, we compute the Taylor series + * for ( fa.getKind(), n ) then substitute { a -> fa[0] } if fa[0]!=0. + * We compute P_{n,f(0)}( x )/R_{n+1,f(0),b}( x ) for ( fa.getKind(), n ) + * if fa[0]=0. + * In the latter case, note we compute the exponential x^{n+1} + * instead of (x-a)^{n+1}, which can be done faster. + */ + std::pair<Node, Node> getTaylor(TNode fa, unsigned n); + + /** internal variables used for constructing (cached) versions of the Taylor + * series above. + */ + Node d_taylor_real_fv; // x above + Node d_taylor_real_fv_base; // a above + Node d_taylor_real_fv_base_rem; // b above + + /** cache of sum and remainder terms for getTaylor */ + std::unordered_map<Node, std::unordered_map<unsigned, Node>, NodeHashFunction> + d_taylor_sum; + std::unordered_map<Node, std::unordered_map<unsigned, Node>, NodeHashFunction> + d_taylor_rem; + + /** concavity region for transcendental functions + * + * This stores an integer that identifies an interval in + * which the current model value for an argument of an + * application of a transcendental function resides. + * + * For exp( x ): + * region #1 is -infty < x < infty + * For sin( x ): + * region #0 is pi < x < infty (this is an invalid region) + * region #1 is pi/2 < x <= pi + * region #2 is 0 < x <= pi/2 + * region #3 is -pi/2 < x <= 0 + * region #4 is -pi < x <= -pi/2 + * region #5 is -infty < x <= -pi (this is an invalid region) + * All regions not listed above, as well as regions 0 and 5 + * for SINE are "invalid". We only process applications + * of transcendental functions whose arguments have model + * values that reside in valid regions. + */ + std::unordered_map<Node, int, NodeHashFunction> d_tf_region; + /** get monotonicity direction + * + * Returns whether the slope is positive (+1) or negative(-1) + * in region of transcendental function with kind k. + * Returns 0 if region is invalid. + */ + int regionToMonotonicityDir(Kind k, int region); + /** get concavity + * + * Returns whether we are concave (+1) or convex (-1) + * in region of transcendental function with kind k, + * where region is defined above. + * Returns 0 if region is invalid. + */ + int regionToConcavity(Kind k, int region); + /** region to lower bound + * + * Returns the term corresponding to the lower + * bound of the region of transcendental function + * with kind k. Returns Node::null if the region + * is invalid, or there is no lower bound for the + * region. + */ + Node regionToLowerBound(Kind k, int region); + /** region to upper bound + * + * Returns the term corresponding to the upper + * bound of the region of transcendental function + * with kind k. Returns Node::null if the region + * is invalid, or there is no upper bound for the + * region. + */ + Node regionToUpperBound(Kind k, int region); + /** get derivative + * + * Returns d/dx n. Supports cases of n + * for transcendental functions applied to x, + * multiplication, addition, constants and variables. + * Returns Node::null() if derivative is an + * unhandled case. + */ + Node getDerivative(Node n, Node x); + + private: + //-------------------------------------------- lemma schemas + /** check split zero + * + * Returns a set of theory lemmas of the form + * t = 0 V t != 0 + * where t is a term that exists in the current context. + */ std::vector<Node> checkSplitZero(); - + + /** check monomial sign + * + * Returns a set of valid theory lemmas, based on a + * lemma schema which ensures that non-linear monomials + * respect sign information based on their facts. + * For more details, see Section 5 of "Design Theory + * Solvers with Extensions" by Reynolds et al., FroCoS 2017, + * Figure 5, this is the schema "Sign". + * + * Examples: + * + * x > 0 ^ y > 0 => x*y > 0 + * x < 0 => x*y*y < 0 + * x = 0 => x*y*z = 0 + */ std::vector<Node> checkMonomialSign(); - + + /** check monomial magnitude + * + * Returns a set of valid theory lemmas, based on a + * lemma schema which ensures that comparisons between + * non-linear monomials respect the magnitude of their + * factors. + * For more details, see Section 5 of "Design Theory + * Solvers with Extensions" by Reynolds et al., FroCoS 2017, + * Figure 5, this is the schema "Magnitude". + * + * Examples: + * + * |x|>|y| => |x*z|>|y*z| + * |x|>|y| ^ |z|>|w| ^ |x|>=1 => |x*x*z*u|>|y*w| + */ std::vector<Node> checkMonomialMagnitude( unsigned c ); - + + /** check monomial inferred bounds + * + * Returns a set of valid theory lemmas, based on a + * lemma schema that infers new constraints about existing + * terms based on mulitplying both sides of an existing + * constraint by a term. + * For more details, see Section 5 of "Design Theory + * Solvers with Extensions" by Reynolds et al., FroCoS 2017, + * Figure 5, this is the schema "Multiply". + * + * Examples: + * + * x > 0 ^ (y > z + w) => x*y > x*(z+w) + * x < 0 ^ (y > z + w) => x*y < x*(z+w) + * ...where (y > z + w) and x*y are a constraint and term + * that occur in the current context. + */ std::vector<Node> checkMonomialInferBounds( std::vector<Node>& nt_lemmas, const std::set<Node>& false_asserts ); - + + /** check factoring + * + * Returns a set of valid theory lemmas, based on a + * lemma schema that states a relationship betwen monomials + * with common factors that occur in the same constraint. + * + * Examples: + * + * x*z+y*z > t => ( k = x + y ^ k*z > t ) + * ...where k is fresh and x*z + y*z > t is a + * constraint that occurs in the current context. + */ std::vector<Node> checkFactoring( const std::set<Node>& false_asserts ); - + + /** check monomial infer resolution bounds + * + * Returns a set of valid theory lemmas, based on a + * lemma schema which "resolves" upper bounds + * of one inequality with lower bounds for another. + * This schema is not enabled by default, and can + * be enabled by --nl-ext-rbound. + * + * Examples: + * + * ( y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t + * ...where s <= x*z and x*y <= t are constraints + * that occur in the current context. + */ std::vector<Node> checkMonomialInferResBounds(); - + + /** check tangent planes + * + * Returns a set of valid theory lemmas, based on an + * "incremental linearization" of non-linear monomials. + * This linearization is accomplished by adding constraints + * corresponding to "tangent planes" at the current + * model value of each non-linear monomial. In particular + * consider the definition for constants a,b : + * T_{a,b}( x*y ) = b*x + a*y - a*b. + * The lemmas added by this function are of the form : + * ( ( x>a ^ y<b) ^ (x<a ^ y>b) ) => x*y < T_{a,b}( x*y ) + * ( ( x>a ^ y>b) ^ (x<a ^ y<b) ) => x*y > T_{a,b}( x*y ) + * It is inspired by "Invariant Checking of NRA Transition + * Systems via Incremental Reduction to LRA with EUF" by + * Cimatti et al., TACAS 2017. + * This schema is not terminating in general. + * It is not enabled by default, and can + * be enabled by --nl-ext-tplanes. + * + * Examples: + * + * ( ( x>2 ^ y>5) ^ (x<2 ^ y<5) ) => x*y > 5*x + 2*y - 10 + * ( ( x>2 ^ y<5) ^ (x<2 ^ y>5) ) => x*y < 5*x + 2*y - 10 + */ std::vector<Node> checkTangentPlanes(); - + + /** check transcendental initial refine + * + * Returns a set of valid theory lemmas, based on + * simple facts about transcendental functions. + * This mostly follows the initial axioms described in + * Section 4 of "Satisfiability + * Modulo Transcendental Functions via Incremental + * Linearization" by Cimatti et al., CADE 2017. + * + * Examples: + * + * sin( x ) = -sin( -x ) + * ( PI > x > 0 ) => 0 < sin( x ) < 1 + * exp( x )>0 + * x<0 => exp( x )<1 + */ std::vector<Node> checkTranscendentalInitialRefine(); + /** check transcendental monotonic + * + * Returns a set of valid theory lemmas, based on a + * lemma scheme that ensures that applications + * of transcendental functions respect monotonicity. + * + * Examples: + * + * x > y => exp( x ) > exp( y ) + * PI/2 > x > y > 0 => sin( x ) > sin( y ) + * PI > x > y > PI/2 => sin( x ) < sin( y ) + */ std::vector<Node> checkTranscendentalMonotonic(); + + //-------------------------------------------- end lemma schemas }; /* class NonlinearExtension */ } // namespace arith |