Preprocessing step for finding finite runs of well-defined function definitions using FMF.

7 files changed, 206 insertions, 3 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 35566be45..a8d42a740 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1309,15 +1309,24 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
         if( ( expr.getKind()!=kind::EQUAL && expr.getKind()!=kind::IFF ) || expr[0].getKind()!=kind::APPLY_UF ){
           success = false;
         }else{
+          FunctionType t = (FunctionType)expr[0].getOperator().getType();
           for( unsigned i=0; i<expr[0].getNumChildren(); i++ ){
-            if( expr[0][i].getKind()!=kind::BOUND_VARIABLE ){
+            if( expr[0][i].getKind()!=kind::BOUND_VARIABLE || expr[0][i].getType()!=t.getArgTypes()[i] ){
               success = false;
+              break;
+            }else{
+              for( unsigned j=0; j<i; j++ ){
+                if( expr[0][j]==expr[0][i] ){
+                  success = false;
+                  break;
+                }
+              }
             }
           }
         }
         if( !success ){
           std::stringstream ss;
-          ss << "warning: Function definition should be an equality whose LHS is an uninterpreted function applied to variables.";
+          ss << "warning: Function definition should be an equality whose LHS is an uninterpreted function applied to unique variables.";
           PARSER_STATE->warning(ss.str());
         }
       }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d0a920653..577fa7413 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -83,6 +83,7 @@
 #include "util/sort_inference.h"
 #include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/quantifiers/macros.h"
+#include "theory/quantifiers/fun_def_process.h"
 #include "theory/quantifiers/first_order_reasoning.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/options.h"
@@ -1352,6 +1353,11 @@ void SmtEngine::setDefaults() {
       options::conjectureGen.set( false );
     }
   }
+  if( options::fmfFunWellDefined() ){
+    if( !options::finiteModelFind.wasSetByUser() ){
+      options::finiteModelFind.set( true );
+    }
+  }
 
   //until bugs 371,431 are fixed
   if( ! options::minisatUseElim.wasSetByUser()){
@@ -3132,6 +3138,10 @@ void SmtEnginePrivate::processAssertions() {
         success = qm.simplify( d_assertions.ref(), true );
       }while( success );
     }
+    if( options::fmfFunWellDefined() ){
+      quantifiers::FunDefFmf fdf;
+      fdf.simplify( d_assertions.ref() );
+    }
 
     Trace("fo-rsn-enable") << std::endl;
     if( options::foPropQuant() ){
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index c9dbb8d4b..c375d68f2 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -18,6 +18,8 @@
 
 #include "theory/quantifiers/fun_def_process.h"
 #include "theory/rewriter.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/quant_util.h"
 
 using namespace CVC4;
 using namespace std;
@@ -27,5 +29,160 @@ using namespace CVC4::kind;
 
 
 void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
+  std::vector< int > fd_assertions;
+  //first pass : find defined functions, transform quantifiers
+  for( unsigned i=0; i<assertions.size(); i++ ){
+    if( assertions[i].getKind()==FORALL ){
+      if( quantifiers::TermDb::isFunDef( assertions[i] ) ){
+        Assert( assertions[i][1].getKind()==EQUAL || assertions[i][1].getKind()==IFF );
+        Node n = assertions[i][1][0];
+        Assert( n.getKind()==APPLY_UF );
+        Node f = n.getOperator();
+        
+        //create a sort S that represents the inputs of the function
+        std::stringstream ss;
+        ss << "I_" << f;
+        TypeNode iType = NodeManager::currentNM()->mkSort( ss.str() );
+        d_sorts[f] = iType;
+        
+        //create functions f1...fn mapping from this sort to concrete elements
+        for( unsigned j=0; j<n.getNumChildren(); j++ ){
+          TypeNode typ = NodeManager::currentNM()->mkFunctionType( iType, n[j].getType() );
+          std::stringstream ss;
+          ss << f << "_arg_" << j;
+          d_input_arg_inj[f].push_back( NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during fun def fmf" ) );
+        }
+        
+        //construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn]
+        std::vector< Node > children;
+        Node bv = NodeManager::currentNM()->mkBoundVar("?i", iType );
+        Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bv );
+        std::vector< Node > subs;
+        std::vector< Node > vars;
+        for( unsigned j=0; j<n.getNumChildren(); j++ ){
+          vars.push_back( n[j] );
+          subs.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], bv ) );
+        }
+        Node bd = assertions[i][1].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+        
+        Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << " to ";
+        assertions[i] = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
+        Trace("fmf-fun-def") << assertions[i] << std::endl;
+        fd_assertions.push_back( i );
+      }
+    }
+  }
+  //second pass : rewrite assertions
+  for( unsigned i=0; i<assertions.size(); i++ ){
+    bool is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end();
+    std::vector< Node > constraints;
+    Node n = simplify( assertions[i], true, true, constraints, is_fd );
+    Assert( constraints.empty() );
+    if( n!=assertions[i] ){
+      n = Rewriter::rewrite( n );
+      Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i] << " to " << n << std::endl;
+      assertions[i] = n;
+    }
+  }
+}
+
+Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, bool is_fun_def ) {
+  Trace("fmf-fun-def-debug") << "Simplify " << n << " " << pol << " " << hasPol << " " << is_fun_def << std::endl;
+  if( n.getKind()==FORALL ){
+    Node c = simplify( n[1], pol, hasPol, constraints, is_fun_def );
+    if( c!=n[1] ){
+      return NodeManager::currentNM()->mkNode( FORALL, n[0], c );
+    }else{
+      return n;
+    }
+  }else if( n.getType().isBoolean() && n.getKind()!=APPLY_UF ){
+    std::vector< Node > children;
+    bool childChanged = false;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      Node c = n[i];
+      //do not process LHS of definition
+      if( !is_fun_def || i!=0 ){
+        bool newHasPol;
+        bool newPol;
+        QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
+        //get child constraints
+        std::vector< Node > cconstraints;
+        c = simplify( n[i], newPol, newHasPol, cconstraints );
+        constraints.insert( constraints.end(), cconstraints.begin(), cconstraints.end() );
+      }
+      children.push_back( c );
+      childChanged = c!=n[i] || childChanged;
+    }
+    if( !constraints.empty() || childChanged ){
+      std::vector< Node > c;
+      if( childChanged ){
+        c.push_back( NodeManager::currentNM()->mkNode( n.getKind(), children ) );
+      }else{
+        c.push_back( n );
+      }
+      if( hasPol ){
+        //conjoin with current
+        for( unsigned i=0; i<constraints.size(); i++ ){
+          if( pol ){
+            c.push_back( constraints[i] );
+          }else{
+            c.push_back( constraints[i].negate() );
+          }
+        }
+        constraints.clear();
+      }else{
+        //must add at higher level
+      }
+      return c.size()==1 ? c[0] : NodeManager::currentNM()->mkNode( AND, c );
+    }
+  }else{
+    //simplify term
+    simplifyTerm( n, constraints );
+  }
+  return n;
+}
 
+void FunDefFmf::simplifyTerm( Node n, std::vector< Node >& constraints ) {
+  Trace("fmf-fun-def-debug") << "Simplify term " << n << std::endl;
+  if( n.getKind()==ITE ){
+    simplifyTerm( n[0], constraints );
+    std::vector< Node > ccons1;
+    std::vector< Node > ccons2;
+    simplifyTerm( n[1], ccons1 );
+    simplifyTerm( n[2], ccons2 );
+    if( !ccons1.empty() || !ccons2.empty() ){
+      Node n1 = ccons1.empty() ? NodeManager::currentNM()->mkConst( true ) : ( ccons1.size()==1 ? ccons1[0] : NodeManager::currentNM()->mkNode( AND, ccons1 ) );
+      Node n2 = ccons2.empty() ? NodeManager::currentNM()->mkConst( true ) : ( ccons2.size()==1 ? ccons2[0] : NodeManager::currentNM()->mkNode( AND, ccons2 ) );
+      constraints.push_back( NodeManager::currentNM()->mkNode( ITE, n[0], n1, n2 ) );
+    }
+  }else{
+    if( n.getKind()==APPLY_UF ){
+      //check if f is defined, if so, we must enforce domain constraints for this f-application
+      Node f = n.getOperator();
+      std::map< Node, TypeNode >::iterator it = d_sorts.find( f );
+      if( it!=d_sorts.end() ){
+        //create existential
+        Node z = NodeManager::currentNM()->mkBoundVar("?z", it->second );
+        Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, z );
+        std::vector< Node > children;
+        for( unsigned j=0; j<n.getNumChildren(); j++ ){
+          Node uz = NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], z );
+          if( !n[j].getType().isBoolean() ){
+            children.push_back( uz.eqNode( n[j] ) );
+          }else{
+            children.push_back( uz.iffNode( n[j] ) );
+          }
+        }
+        Node bd = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children );
+        bd = bd.negate();
+        Node ex = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
+        ex = ex.negate();
+        constraints.push_back( ex );
+        Trace("fmf-fun-def-debug") << "---> add constraint " << ex << std::endl;
+      }
+    }
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      simplifyTerm( n[i], constraints );
+    }
+  }
 }
diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h
index c2d8aeb65..22adf427d 100644
--- a/src/theory/quantifiers/fun_def_process.h
+++ b/src/theory/quantifiers/fun_def_process.h
@@ -30,6 +30,17 @@ namespace quantifiers {
 
 //find finite models for well-defined functions
 class FunDefFmf {
+private:
+  //defined functions to input sort
+  std::map< Node, TypeNode > d_sorts;
+  //defined functions to injections input -> argument elements
+  std::map< Node, std::vector< Node > > d_input_arg_inj;
+  //flatten ITE
+  void flattenITE( Node lhs, Node n, std::vector< std::vector< Node > >& conds, std::vector< Node >& terms );
+  //simplify
+  Node simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, bool is_fun_def = false );
+  //simplify term
+  void simplifyTerm( Node n, std::vector< Node >& constraints );
 public:
   FunDefFmf(){}
   ~FunDefFmf(){}
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 730da8839..8cb693117 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -74,6 +74,8 @@ option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :d
 
 option quantFunWellDefined --quant-fun-wd bool :default false
  assume that function defined by quantifiers are well defined
+option fmfFunWellDefined --fmf-fun bool :default false
+ find models for finite runs of defined functions, assumes functions are well-defined
  
 # Whether to consider terms in the bodies of quantifiers for matching
 option registerQuantBodyTerms --register-quant-body-terms bool :default false
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 3a9353de9..0b606ecf0 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1000,6 +1000,19 @@ Node TermDb::getRewriteRule( Node q ) {
   }
 }
 
+bool TermDb::isFunDef( Node q ) {
+  if( q.getKind()==FORALL && ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF ){
+    for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
+      if( q[2][i].getKind()==INST_ATTRIBUTE ){
+        if( q[2][i][0].getAttribute(FunDefAttribute()) ){
+          return true;
+        }
+      }
+    }
+  }
+  return false;
+}
+
 
 void TermDb::computeAttributes( Node q ) {
   if( q.getNumChildren()==3 ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 13dfa657c..dbd12f8f0 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -316,7 +316,8 @@ public: //general queries concerning quantified formulas wrt modules
   static bool isRewriteRule( Node q );
   /** get the rewrite rule associated with the quanfied formula */
   static Node getRewriteRule( Node q );
-  
+  /** is fun def */
+  static bool isFunDef( Node q );
 //attributes
 private:
   std::map< Node, bool > d_qattr_conjecture;