Basic optimizations for ambqi : only normalize UF applied to variables, direct handli...

diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index 7813f2cc12b422a045e0786cb23b1bdade914e34..e3f031d1116f9ad51d63046cf320774fbe099e41 100755 (executable)
--- 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;\r
     std::vector< unsigned > entry;\r
     std::vector< bool > entry_def;\r
-    if( f ){\r
+    if( f && varChCount>0 ){\r
       AbsDef unorm;\r
       unorm.construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def );\r
       //normalize\r
@@ -570,6 +570,11 @@ bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,
     }else{\r
       construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def );\r
     }\r
+    Assert( is_normalized() );\r
+    //if( !is_normalized() ){\r
+    //  std::cout << "NON NORMALIZED DEFINITION" << std::endl;\r
+    //  exit( 10 );\r
+    //}\r
     return true;\r
   }else if( varChCount==1 && n.getKind()==EQUAL ){\r
     Trace("ambqi-check-debug2") << "Expand variable child..." << std::endl;\r
@@ -593,6 +598,17 @@ bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,
   }\r
 }\r
 \r
+void AbsDef::negate() {\r
+  for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){\r
+    it->second.negate();\r
+  }\r
+  if( d_value==0 ){\r
+    d_value = 1;\r
+  }else if( d_value==1 ){\r
+    d_value = 0;\r
+  }\r
+}\r
+\r
 Node AbsDef::getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth ) {\r
   if( depth==vars.size() ){\r
     TypeNode tn = op.getType();\r
@@ -672,6 +688,20 @@ Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< uns
   }\r
 }\r
 \r
+bool AbsDef::is_normalized() {\r
+  for( std::map< unsigned, AbsDef >::iterator it1 = d_def.begin(); it1 != d_def.end(); ++it1 ){\r
+    if( !it1->second.is_normalized() ){\r
+      return false;\r
+    }\r
+    for( std::map< unsigned, AbsDef >::iterator it2 = d_def.begin(); it2 != d_def.end(); ++it2 ){\r
+      if( it1->first!=it2->first && (( it1->first & it2->first )!=0) ){\r
+        return false;\r
+      }\r
+    }\r
+  }\r
+  return true;\r
+}\r
+\r
 AbsMbqiBuilder::AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe ) :\r
 QModelBuilder( c, qe ){\r
   d_true = NodeManager::currentNM()->mkConst( true );\r
@@ -833,55 +863,61 @@ bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, in
 \r
 bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ) {\r
   Assert( n.getKind()!=FORALL );\r
-  std::map< unsigned, AbsDef > children;\r
-  std::map< unsigned, int > bchildren;\r
-  std::map< unsigned, int > vchildren;\r
-  int varChCount = 0;\r
-  for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
-    if( n[i].getKind()==FORALL ){\r
-      bchildren[i] = AbsDef::val_unk;\r
-    }else if( n[i].getKind() == BOUND_VARIABLE ){\r
-      varChCount++;\r
-      vchildren[i] = m->getVariableId( q, n[i] );\r
-    }else if( m->hasTerm( n[i] ) ){\r
-      bchildren[i] = m->getRepresentativeId( n[i] );\r
-    }else{\r
-      if( !doCheck( m, q, children[i], n[i] ) ){\r
+  if( n.getKind()==NOT ){\r
+    doCheck( m, q, ad, n[0] );\r
+    ad.negate();\r
+    return true;\r
+  }else{\r
+    std::map< unsigned, AbsDef > children;\r
+    std::map< unsigned, int > bchildren;\r
+    std::map< unsigned, int > vchildren;\r
+    int varChCount = 0;\r
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+      if( n[i].getKind()==FORALL ){\r
         bchildren[i] = AbsDef::val_unk;\r
-        children.erase( i );\r
+      }else if( n[i].getKind() == BOUND_VARIABLE ){\r
+        varChCount++;\r
+        vchildren[i] = m->getVariableId( q, n[i] );\r
+      }else if( m->hasTerm( n[i] ) ){\r
+        bchildren[i] = m->getRepresentativeId( n[i] );\r
+      }else{\r
+        if( !doCheck( m, q, children[i], n[i] ) ){\r
+          bchildren[i] = AbsDef::val_unk;\r
+          children.erase( i );\r
+        }\r
       }\r
     }\r
-  }\r
-  //convert to pointers\r
-  std::map< unsigned, AbsDef * > pchildren;\r
-  for( std::map< unsigned, AbsDef >::iterator it = children.begin(); it != children.end(); ++it ){\r
-    pchildren[it->first] = &it->second;\r
-  }\r
-  //construct the interpretation\r
-  Trace("ambqi-check-debug") << "Compute Interpretation of " << n << " " << n.getKind() << std::endl;\r
-  if( n.getKind() == APPLY_UF || n.getKind() == VARIABLE || n.getKind() == SKOLEM ){\r
-    Node op;\r
-    if( n.getKind() == APPLY_UF ){\r
-      op = n.getOperator();\r
-    }else{\r
-      op = n;\r
+    //convert to pointers\r
+    std::map< unsigned, AbsDef * > pchildren;\r
+    for( std::map< unsigned, AbsDef >::iterator it = children.begin(); it != children.end(); ++it ){\r
+      pchildren[it->first] = &it->second;\r
     }\r
-    //uninterpreted compose\r
-    if( m->d_models_valid[op] ){\r
-      ad.construct( m, q, n, m->d_models[op], pchildren, bchildren, vchildren, varChCount );\r
-    }else{\r
-      Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (no function model)" << std::endl;\r
+    //construct the interpretation\r
+    Trace("ambqi-check-debug") << "Compute Interpretation of " << n << " " << n.getKind() << std::endl;\r
+    if( n.getKind() == APPLY_UF || n.getKind() == VARIABLE || n.getKind() == SKOLEM ){\r
+      Node op;\r
+      if( n.getKind() == APPLY_UF ){\r
+        op = n.getOperator();\r
+      }else{\r
+        op = n;\r
+      }\r
+      //uninterpreted compose\r
+      if( m->d_models_valid[op] ){\r
+        ad.construct( m, q, n, m->d_models[op], pchildren, bchildren, vchildren, varChCount );\r
+      }else{\r
+        Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (no function model)" << std::endl;\r
+        return false;\r
+      }\r
+    }else if( !ad.construct( m, q, n, NULL, pchildren, bchildren, vchildren, varChCount ) ){\r
+      Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (variables are children of interpreted symbol)" << std::endl;\r
       return false;\r
     }\r
-  }else if( !ad.construct( m, q, n, NULL, pchildren, bchildren, vchildren, varChCount ) ){\r
-    Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (variables are children of interpreted symbol)" << std::endl;\r
-    return false;\r
+    Trace("ambqi-check-try") << "Interpretation for " << n << " is : " << std::endl;\r
+    ad.debugPrint("ambqi-check-try", m, q[0] );\r
+    ad.simplify( m, q[0] );\r
+    Trace("ambqi-check-debug") << "(Simplified) Interpretation for " << n << " is : " << std::endl;\r
+    ad.debugPrint("ambqi-check-debug", m, q[0] );\r
+    Trace("ambqi-check-debug") << std::endl;\r
+    return true;\r
   }\r
-  Trace("ambqi-check-try") << "Interpretation for " << n << " is : " << std::endl;\r
-  ad.debugPrint("ambqi-check-try", m, q[0] );\r
-  ad.simplify( m, q[0] );\r
-  Trace("ambqi-check-debug") << "(Simplified) Interpretation for " << n << " is : " << std::endl;\r
-  ad.debugPrint("ambqi-check-debug", m, q[0] );\r
-  Trace("ambqi-check-debug") << std::endl;\r
-  return true;\r
 }\r

diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h
index 29cee448b367ccdc2811e60bd7e0b5424b84eea0..def0741775b9887e37215ff72490dd41bbe99730 100755 (executable)
--- a/src/theory/quantifiers/ambqi_builder.h
+++ b/src/theory/quantifiers/ambqi_builder.h
@@ -69,11 +69,14 @@ public:
                   std::map< unsigned, int >& bchildren,\r
                   std::map< unsigned, int >& vchildren,\r
                   int varChCount );\r
+  void negate();\r
   Node getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth = 0 );\r
   static bool isSimple( unsigned n );\r
   static unsigned getId( unsigned n, unsigned start=0 );\r
   Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< Node >& args );\r
   Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< unsigned >& iargs, unsigned depth = 0 );\r
+  //for debugging\r
+  bool is_normalized();\r
 };\r
 \r
 class AbsMbqiBuilder : public QModelBuilder\r