diff options
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.h')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index a45318489..821beeae0 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -49,19 +49,19 @@ private: /** for each quantifier, simplex rows */ std::map< Node, std::vector< arith::ArithVar > > d_instRows; /** tableaux */ - std::map< arith::ArithVar, Node > d_tableaux_term; - std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux_ce_term; - std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux; + std::map< Node, std::map< arith::ArithVar, Node > > d_tableaux_term; + std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_tableaux_ce_term; + std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_tableaux; /** ce tableaux */ - std::map< arith::ArithVar, std::map< Node, Node > > d_ceTableaux; + std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_ceTableaux; /** get value */ Node getTableauxValue( Node n, bool minus_delta = false ); Node getTableauxValue( arith::ArithVar v, bool minus_delta = false ); /** do instantiation */ - bool doInstantiation( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var ); - bool doInstantiation2( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false ); + bool doInstantiation( Node f, Node ic, Node term, arith::ArithVar x, InstMatch& m, Node var ); + bool doInstantiation2( Node f, Node ic, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false ); /** add term to row */ - void addTermToRow( arith::ArithVar x, Node n, Node& f, NodeBuilder<>& t ); + void addTermToRow( Node ic, arith::ArithVar x, Node n, NodeBuilder<>& t ); /** print debug */ void debugPrint( const char* c ); private: |