Basic optimizations for ambqi : only normalize UF applied to variables, direct handling of NOT

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; i<n.getNumChildren(); i++ ){

-    if( n[i].getKind()==FORALL ){

-      bchildren[i] = AbsDef::val_unk;

-    }else if( n[i].getKind() == BOUND_VARIABLE ){

-      varChCount++;

-      vchildren[i] = m->getVariableId( 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; i<n.getNumChildren(); i++ ){

+      if( n[i].getKind()==FORALL ){

         bchildren[i] = AbsDef::val_unk;

-        children.erase( i );

+      }else if( n[i].getKind() == BOUND_VARIABLE ){

+        varChCount++;

+        vchildren[i] = m->getVariableId( 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