diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-15 19:47:32 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-15 19:47:32 +0200 |
| commit | 520c5903a4c399b7c5beaa2d353bbf9324009ee7 (patch) | |
| tree | 22a5662b8cd9e66d99bee2ca21eccf4a6c4b1d1c /src/theory/quantifiers/trigger.cpp | |
| parent | 3ce21ef9a8b6daa1eef1dbe9af10a84e8c87e413 (diff) | |
Fixes related to cbqi + E-matching.
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
| -rw-r--r-- | src/theory/quantifiers/trigger.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index e9ce29468..c55ed27ea 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -43,7 +43,7 @@ d_quantEngine( qe ), d_f( f ){ if( isSimpleTrigger( d_nodes[0] ) ){ d_mg = new InstMatchGeneratorSimple( f, d_nodes[0] ); }else{ - d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes[0], qe ); + d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes[0], qe ); d_mg->setActiveAdd(true); } }else{ @@ -52,7 +52,7 @@ d_quantEngine( qe ), d_f( f ){ //d_mg->setActiveAdd(); } }else{ - d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe ); + d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes, qe ); d_mg->setActiveAdd(true); } if( d_nodes.size()==1 ){ @@ -553,7 +553,7 @@ Node Trigger::getInversion( Node n, Node x ) { return Node::null(); } -InstMatchGenerator* Trigger::getInstMatchGenerator( Node n ) { +InstMatchGenerator* Trigger::getInstMatchGenerator( Node q, Node n ) { if( n.getKind()==INST_CONSTANT ){ return NULL; }else{ |