From e909e34249754bc5f021449512c9cc304802933f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 19 Aug 2015 21:45:37 +0200 Subject: Make cbqi robust to term ITE removal. Separate vts infinities for int/real. --- src/theory/quantifiers/term_database.h | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) (limited to 'src/theory/quantifiers/term_database.h') 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 */ -- cgit v1.2.3