diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-14 17:04:14 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-14 17:04:14 -0600 |
commit | 748e20967ae7698f6b545a5128633865701aeb2d (patch) | |
tree | 3413586dbdeff2ddfbb604db5c1e6045b1a749a7 /src/theory/quantifiers/term_util.h | |
parent | 376d72fd02d7f8822188055355452449b718481f (diff) |
(Refactor) Split sygus term db (#1335)
* Split explain utility, invariance tests.
* Split extended rewriter.
* Remove unused function.
* Minor
* Move generic term utilities to term_util.
* Documentation, minor.
* Make arguments private in eval invariance.
* Document
* More documentation.
* Clang format.
* Fix, improve.
* Format
* Address review.
* Address missed comment.
* Add line breaks
* Format
Diffstat (limited to 'src/theory/quantifiers/term_util.h')
-rw-r--r-- | src/theory/quantifiers/term_util.h | 104 |
1 files changed, 96 insertions, 8 deletions
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index bcdf8a2ff..d2a8a14f0 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -265,11 +265,34 @@ public: static void getRelevancyCondition( Node n, std::vector< Node >& cond ); //general utilities -private: + // TODO #1216 : promote these? + private: //helper for contains term static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited ); static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ); -public: + /** cache for getTypeValue */ + std::unordered_map<TypeNode, + std::unordered_map<int, Node>, + TypeNodeHashFunction> + d_type_value; + /** cache for getTypeMaxValue */ + std::unordered_map<TypeNode, Node, TypeNodeHashFunction> d_type_max_value; + /** cache for getTypeValueOffset */ + std::unordered_map<TypeNode, + std::unordered_map<Node, + std::unordered_map<int, Node>, + NodeHashFunction>, + TypeNodeHashFunction> + d_type_value_offset; + /** cache for status of getTypeValueOffset*/ + std::unordered_map<TypeNode, + std::unordered_map<Node, + std::unordered_map<int, int>, + NodeHashFunction>, + TypeNodeHashFunction> + d_type_value_offset_status; + + public: /** simple check for whether n contains t as subterm */ static bool containsTerm( Node n, Node t ); /** simple check for contains term, true if contains at least one term in t */ @@ -282,17 +305,82 @@ public: static Node simpleNegate( Node n ); /** is assoc */ static bool isAssoc( Kind k ); - /** is comm */ + /** is k commutative? */ static bool isComm( Kind k ); - /** ( x k ... ) k x = ( x k ... ) */ + + /** is k non-additive? + * Returns true if + * <k>( <k>( T1, x, T2 ), x ) = + * <k>( T1, x, T2 ) + * always holds, where T1 and T2 are vectors. + */ static bool isNonAdditive( Kind k ); - /** is bool connective */ + /** is k a bool connective? */ static bool isBoolConnective( Kind k ); - /** is bool connective term */ + /** is n a bool connective term? */ static bool isBoolConnectiveTerm( TNode n ); -//for higher-order -private: + /** is the kind k antisymmetric? + * If so, return true and store its inverse kind in dk. + */ + static bool isAntisymmetric(Kind k, Kind& dk); + + /** has offset arg + * Returns true if there is a Kind ok and offset + * such that + * <ik>( ... t_{arg-1}, n, t_{arg+1}... ) = + * <ok>( ... t_{arg-1}, n+offset, t_{arg+1}...) + * always holds. + * If so, this function returns true and stores + * offset and ok in the respective fields. + */ + static bool hasOffsetArg(Kind ik, int arg, int& offset, Kind& ok); + + /** is idempotent arg + * Returns true if + * <k>( ... t_{arg-1}, n, t_{arg+1}...) = + * <k>( ... t_{arg-1}, t_{arg+1}...) + * always holds. + */ + bool isIdempotentArg(Node n, Kind ik, int arg); + + /** is singular arg + * Returns true if + * <k>( ... t_{arg-1}, n, t_{arg+1}...) = n + * always holds. + */ + Node isSingularArg(Node n, Kind ik, int arg); + + /** get type value + * This gets the Node that represents value val for Type tn + * This is used to get simple values, e.g. -1,0,1, + * in a uniform way per type. + */ + Node getTypeValue(TypeNode tn, int val); + + /** get type value offset + * Returns the value of ( val + getTypeValue( tn, offset ) ), + * where + is the additive operator for the type. + * Stores the status (0: success, -1: failure) in status. + */ + Node getTypeValueOffset(TypeNode tn, Node val, int offset, int& status); + + /** get the "max" value for type tn + * For example, + * the max value for Bool is true, + * the max value for BitVector is 1..1. + */ + Node getTypeMaxValue(TypeNode tn); + + /** make value, static version of get value */ + static Node mkTypeValue(TypeNode tn, int val); + /** make value offset, static version of get value offset */ + static Node mkTypeValueOffset(TypeNode tn, Node val, int offset, int& status); + /** make max value, static version of get max value */ + static Node mkTypeMaxValue(TypeNode tn); + + // for higher-order + private: /** dummy predicate that states terms should be considered first-class members of equality engine */ std::map< TypeNode, Node > d_ho_type_match_pred; public: |