diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-03-12 14:25:25 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-03-12 14:25:25 -0500 |
| commit | 8b41e8d8128752eba75f32f751ec9c095a6b1d87 (patch) | |
| tree | 68559af9be49966dedfa877b124f76d3af152b7b /src/theory/quantifiers/model_builder.cpp | |
| parent | 15d36d99363b4ee20754498b566bd315150953fc (diff) | |
Work on array pf signature, add working example. Add quantifiers proof signature. Ignore terms not in current master EE for QCF. Minor refactoring. Make --rewrite-rules true by default.
Diffstat (limited to 'src/theory/quantifiers/model_builder.cpp')
| -rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 50a0084fc..a12fc7ca2 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -1039,7 +1039,7 @@ int QModelBuilderInstGen::getSelectionFormulaScore( Node fn ){ if( fn.getKind()==APPLY_UF ){ Node op = fn.getOperator(); //return total number of terms - return d_qe->getTermDatabase()->d_op_count[op]; + return d_qe->getTermDatabase()->d_op_nonred_count[op]; }else{ int score = 0; for( size_t i=0; i<fn.getNumChildren(); i++ ){ |