From 2ca4e063ca007851ebf73ccb2ac6b7c85e73133d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 8 May 2014 02:18:54 -0500 Subject: [PATCH] Basic optimizations for ambqi : only normalize UF applied to variables, direct handling of NOT --- src/theory/quantifiers/ambqi_builder.cpp | 126 +++++++++++++++-------- src/theory/quantifiers/ambqi_builder.h | 3 + 2 files changed, 84 insertions(+), 45 deletions(-) diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index 7813f2cc1..e3f031d11 100755 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -560,7 +560,7 @@ bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, Trace("ambqi-check-debug2") << "Construct compose..." << std::endl; std::vector< unsigned > entry; std::vector< bool > entry_def; - if( f ){ + if( f && varChCount>0 ){ AbsDef unorm; unorm.construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def ); //normalize @@ -570,6 +570,11 @@ bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, }else{ construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def ); } + Assert( is_normalized() ); + //if( !is_normalized() ){ + // std::cout << "NON NORMALIZED DEFINITION" << std::endl; + // exit( 10 ); + //} return true; }else if( varChCount==1 && n.getKind()==EQUAL ){ Trace("ambqi-check-debug2") << "Expand variable child..." << std::endl; @@ -593,6 +598,17 @@ bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, } } +void AbsDef::negate() { + for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ + it->second.negate(); + } + if( d_value==0 ){ + d_value = 1; + }else if( d_value==1 ){ + d_value = 0; + } +} + Node AbsDef::getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth ) { if( depth==vars.size() ){ TypeNode tn = op.getType(); @@ -672,6 +688,20 @@ Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< uns } } +bool AbsDef::is_normalized() { + for( std::map< unsigned, AbsDef >::iterator it1 = d_def.begin(); it1 != d_def.end(); ++it1 ){ + if( !it1->second.is_normalized() ){ + return false; + } + for( std::map< unsigned, AbsDef >::iterator it2 = d_def.begin(); it2 != d_def.end(); ++it2 ){ + if( it1->first!=it2->first && (( it1->first & it2->first )!=0) ){ + return false; + } + } + } + return true; +} + AbsMbqiBuilder::AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe ) : QModelBuilder( c, qe ){ d_true = NodeManager::currentNM()->mkConst( true ); @@ -833,55 +863,61 @@ bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, in bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ) { Assert( n.getKind()!=FORALL ); - std::map< unsigned, AbsDef > children; - std::map< unsigned, int > bchildren; - std::map< unsigned, int > vchildren; - int varChCount = 0; - for( unsigned i=0; igetVariableId( q, n[i] ); - }else if( m->hasTerm( n[i] ) ){ - bchildren[i] = m->getRepresentativeId( n[i] ); - }else{ - if( !doCheck( m, q, children[i], n[i] ) ){ + if( n.getKind()==NOT ){ + doCheck( m, q, ad, n[0] ); + ad.negate(); + return true; + }else{ + std::map< unsigned, AbsDef > children; + std::map< unsigned, int > bchildren; + std::map< unsigned, int > vchildren; + int varChCount = 0; + for( unsigned i=0; igetVariableId( q, n[i] ); + }else if( m->hasTerm( n[i] ) ){ + bchildren[i] = m->getRepresentativeId( n[i] ); + }else{ + if( !doCheck( m, q, children[i], n[i] ) ){ + bchildren[i] = AbsDef::val_unk; + children.erase( i ); + } } } - } - //convert to pointers - std::map< unsigned, AbsDef * > pchildren; - for( std::map< unsigned, AbsDef >::iterator it = children.begin(); it != children.end(); ++it ){ - pchildren[it->first] = &it->second; - } - //construct the interpretation - Trace("ambqi-check-debug") << "Compute Interpretation of " << n << " " << n.getKind() << std::endl; - if( n.getKind() == APPLY_UF || n.getKind() == VARIABLE || n.getKind() == SKOLEM ){ - Node op; - if( n.getKind() == APPLY_UF ){ - op = n.getOperator(); - }else{ - op = n; + //convert to pointers + std::map< unsigned, AbsDef * > pchildren; + for( std::map< unsigned, AbsDef >::iterator it = children.begin(); it != children.end(); ++it ){ + pchildren[it->first] = &it->second; } - //uninterpreted compose - if( m->d_models_valid[op] ){ - ad.construct( m, q, n, m->d_models[op], pchildren, bchildren, vchildren, varChCount ); - }else{ - Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (no function model)" << std::endl; + //construct the interpretation + Trace("ambqi-check-debug") << "Compute Interpretation of " << n << " " << n.getKind() << std::endl; + if( n.getKind() == APPLY_UF || n.getKind() == VARIABLE || n.getKind() == SKOLEM ){ + Node op; + if( n.getKind() == APPLY_UF ){ + op = n.getOperator(); + }else{ + op = n; + } + //uninterpreted compose + if( m->d_models_valid[op] ){ + ad.construct( m, q, n, m->d_models[op], pchildren, bchildren, vchildren, varChCount ); + }else{ + Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (no function model)" << std::endl; + return false; + } + }else if( !ad.construct( m, q, n, NULL, pchildren, bchildren, vchildren, varChCount ) ){ + Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (variables are children of interpreted symbol)" << std::endl; return false; } - }else if( !ad.construct( m, q, n, NULL, pchildren, bchildren, vchildren, varChCount ) ){ - Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (variables are children of interpreted symbol)" << std::endl; - return false; + Trace("ambqi-check-try") << "Interpretation for " << n << " is : " << std::endl; + ad.debugPrint("ambqi-check-try", m, q[0] ); + ad.simplify( m, q[0] ); + Trace("ambqi-check-debug") << "(Simplified) Interpretation for " << n << " is : " << std::endl; + ad.debugPrint("ambqi-check-debug", m, q[0] ); + Trace("ambqi-check-debug") << std::endl; + return true; } - Trace("ambqi-check-try") << "Interpretation for " << n << " is : " << std::endl; - ad.debugPrint("ambqi-check-try", m, q[0] ); - ad.simplify( m, q[0] ); - Trace("ambqi-check-debug") << "(Simplified) Interpretation for " << n << " is : " << std::endl; - ad.debugPrint("ambqi-check-debug", m, q[0] ); - Trace("ambqi-check-debug") << std::endl; - return true; } diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h index 29cee448b..def074177 100755 --- a/src/theory/quantifiers/ambqi_builder.h +++ b/src/theory/quantifiers/ambqi_builder.h @@ -69,11 +69,14 @@ public: std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren, int varChCount ); + void negate(); Node getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth = 0 ); static bool isSimple( unsigned n ); static unsigned getId( unsigned n, unsigned start=0 ); Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< Node >& args ); Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< unsigned >& iargs, unsigned depth = 0 ); + //for debugging + bool is_normalized(); }; class AbsMbqiBuilder : public QModelBuilder -- 2.30.2