summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/full_model_check.cpp
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-04-12 10:13:45 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2016-04-12 10:13:45 -0500
commit4ff2946e1338d3f500b7e6bababee50fadad68d6 (patch)
tree6f1306e4476e3f7496d7a4e045e63d942802a392 /src/theory/quantifiers/full_model_check.cpp
parent1b2e6c81be2a8ab0656ff2ee3938ef4587e24e25 (diff)
Optimizations for QCF to check relevant domain of variable argument positions eagerly, global ordering mechanism for quantified formulas within check. Refactoring of term database.
Diffstat (limited to 'src/theory/quantifiers/full_model_check.cpp')
-rw-r--r--src/theory/quantifiers/full_model_check.cpp6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 0276cf7ab..6b06b9e5c 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -350,11 +350,11 @@ void FullModelChecker::preProcessBuildModel(TheoryModel* m, bool fullModel) {
}
//do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts
if( !options::fmfEmptySorts() ){
- for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node q = fm->getAssertedQuantifier( i );
//make sure all types are set
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- preInitializeType( fm, q[0][i].getType() );
+ for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
+ preInitializeType( fm, q[0][j].getType() );
}
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback