diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-19 21:45:37 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-19 21:45:44 +0200 |
commit | e909e34249754bc5f021449512c9cc304802933f (patch) | |
tree | 351914fb850b4dce3d15ad8f72acde39c6770826 /src/theory/quantifiers/term_database.h | |
parent | ca72dd6bc0fdc63391b568e4cbcf289300e295dc (diff) |
Make cbqi robust to term ITE removal. Separate vts infinities for int/real.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
-rw-r--r-- | src/theory/quantifiers/term_database.h | 24 |
1 files changed, 20 insertions, 4 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 416761ce8..529207390 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -348,21 +348,37 @@ public: //for virtual term substitution private: Node d_vts_delta; - Node d_vts_inf; + std::map< TypeNode, Node > d_vts_inf; Node d_vts_delta_free; - Node d_vts_inf_free; + std::map< TypeNode, Node > d_vts_inf_free; + /** get vts infinity index */ + Node getVtsInfinityIndex( int i, bool isFree = false, bool create = true ); public: /** get vts delta */ Node getVtsDelta( bool isFree = false, bool create = true ); /** get vts infinity */ - Node getVtsInfinity( bool isFree = false, bool create = true ); + Node getVtsInfinity( TypeNode tn, bool isFree = false, bool create = true ); + /** get all vts terms */ + void getVtsTerms( std::vector< Node >& t, bool isFree = false, bool create = true, bool inc_delta = true ); /** rewrite delta */ Node rewriteVtsSymbols( Node n ); - + /** simple check for contains term */ + bool containsVtsTerm( Node n, bool isFree = false ); + /** simple check for contains term */ + bool containsVtsTerm( std::vector< Node >& n, bool isFree = false ); + /** simple check for contains term */ + bool containsVtsInfinity( Node n, bool isFree = false ); + +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 ); //general utilities public: /** simple check for contains term */ static bool containsTerm( Node n, Node t ); + /** simple check for contains term */ + static bool containsTerms( Node n, std::vector< Node >& t ); /** simple negate */ static Node simpleNegate( Node n ); /** is assoc */ |