diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-07-22 17:59:47 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-08-13 16:23:11 -0500 |
| commit | fc34e25ce2df4c0fb41b7521cc033afd688e0295 (patch) | |
| tree | 537c4ac5ae261045b1aa5619db45e58c51d814ab /src/theory/quantifiers/inst_strategy_cbqi.h | |
| parent | 753807683ee6e52d1859aaa6277fe65e74b1c0bc (diff) | |
initial modifications for per-ic cbqi
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: |