From e179e62b57eb207d41647a6bbd50ef0f8c723e96 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 27 Jan 2014 08:34:52 -0600 Subject: More optimization of QCF and instantiation caching. Fix CDInstMatchTrie. --- src/theory/quantifiers/quant_conflict_find.h | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src/theory/quantifiers/quant_conflict_find.h') diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 5ba7684ef..29ddceb40 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -110,9 +110,11 @@ public: std::map< int, MatchGen * > d_var_mg; void reset_round( QuantConflictFind * p ); public: + //initialize + void initialize( Node q ); //current constraints - std::map< int, TNode > d_match; - std::map< int, TNode > d_match_term; + std::vector< TNode > d_match; + std::vector< TNode > d_match_term; std::map< int, std::map< TNode, int > > d_curr_var_deq; int getCurrentRepVar( int v ); TNode getCurrentValue( TNode n ); -- cgit v1.2.3