From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 4 Dec 2017 21:42:00 +0000 (-0600)
Subject: Eliminate expand definitions from Sygus (#1425)
X-Git-Tag: cvc5-1.0.0~5429
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3c6f227b7aa5233f785804a77f5b2daad34b5faa;p=cvc5.git

Eliminate expand definitions from Sygus (#1425)
---

diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp
index 295d7fb52..ed4e8a951 100644
--- a/src/theory/quantifiers/term_database_sygus.cpp
+++ b/src/theory/quantifiers/term_database_sygus.cpp
@@ -2,38 +2,24 @@
 /*! \file term_database_sygus.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynoldsg
+ **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Implementation of term databse class
+ ** \brief Implementation of term database sygus class
  **/
 
 #include "theory/quantifiers/term_database_sygus.h"
 
-#include "expr/datatype.h"
-#include "options/base_options.h"
-#include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
-#include "smt/smt_engine.h"
 #include "theory/arith/arith_msum.h"
-#include "theory/quantifiers/ce_guided_conjecture.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/theory_quantifiers.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
-
-//for sygus
-#include "smt/smt_engine_scope.h"
-#include "theory/bv/theory_bv_utils.h"
-#include "util/bitvector.h"
-#include "theory/datatypes/datatypes_rewriter.h"
-#include "theory/strings/theory_strings_rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -300,8 +286,9 @@ Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
       }
       ret = mkGeneric( dt, i, var_count, pre );
       Trace("sygus-db-debug") << "SygusToBuiltin : Generic is " << ret << std::endl;
-      ret = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( ret.toExpr() ) );
-      Trace("sygus-db-debug") << "SygusToBuiltin : After expand definitions " << ret << std::endl;
+      ret = Rewriter::rewrite(ret);
+      Trace("sygus-db-debug") << "SygusToBuiltin : After rewriting " << ret
+                              << std::endl;
       d_sygus_to_builtin[tn][n] = ret;
     }else{
       Assert( isFreeVar( n ) );
@@ -1535,10 +1522,11 @@ void doStrReplace(std::string& str, const std::string& oldStr, const std::string
 
 Kind TermDbSygus::getOperatorKind( Node op ) {
   Assert( op.getKind()!=BUILTIN );
-  Assert(!smt::currentSmtEngine()->isDefinedFunction(op.toExpr()));
   if (op.getKind() == LAMBDA)
   {
-    return APPLY;
+    // we use APPLY_UF instead of APPLY, since the rewriter for APPLY_UF
+    // does beta-reduction but does not for APPLY
+    return APPLY_UF;
   }else{
     TypeNode tn = op.getType();
     if( tn.isConstructor() ){
@@ -1788,9 +1776,10 @@ Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Nod
       int i = ret.getAttribute(SygusVarNumAttribute());
       Assert( Node::fromExpr( dt.getSygusVarList() )[i]==ret );
       ret = args[i];
-    }else if( ret.getKind()==APPLY ){
-      //must expand definitions to account for defined functions in sygus grammars
-      ret = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( ret.toExpr() ) );
+    }
+    else
+    {
+      ret = Rewriter::rewrite(ret);
     }
     return ret;
   }else{