From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 8 May 2014 07:18:54 +0000 (-0500)
Subject: Basic optimizations for ambqi : only normalize UF applied to variables, direct handli... 
X-Git-Tag: cvc5-1.0.0~6921
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2ca4e063ca007851ebf73ccb2ac6b7c85e73133d;p=cvc5.git

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

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