src/theory/quantifiers/expr_miner_manager.cpp

   1 /*********************                                                        */
   2 /*! \file expr_miner_manager.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Implementation of expression miner manager.
  13  **/
  14
  15 #include "theory/quantifiers/expr_miner_manager.h"
  16 #include "theory/quantifiers_engine.h"
  17
  18 #include "options/quantifiers_options.h"
  19
  20 namespace CVC4 {
  21 namespace theory {
  22 namespace quantifiers {
  23
  24 ExpressionMinerManager::ExpressionMinerManager()
  25     : d_doRewSynth(false),
  26       d_doQueryGen(false),
  27       d_doFilterLogicalStrength(false),
  28       d_use_sygus_type(false),
  29       d_qe(nullptr),
  30       d_tds(nullptr),
  31       d_crd(options::sygusRewSynthCheck(), options::sygusRewSynthAccel(), false)
  32 {
  33 }
  34
  35 void ExpressionMinerManager::initialize(const std::vector<Node>& vars,
  36                                         TypeNode tn,
  37                                         unsigned nsamples,
  38                                         bool unique_type_ids)
  39 {
  40   d_doRewSynth = false;
  41   d_doQueryGen = false;
  42   d_doFilterLogicalStrength = false;
  43   d_sygus_fun = Node::null();
  44   d_use_sygus_type = false;
  45   d_qe = nullptr;
  46   d_tds = nullptr;
  47   // initialize the sampler
  48   d_sampler.initialize(tn, vars, nsamples, unique_type_ids);
  49 }
  50
  51 void ExpressionMinerManager::initializeSygus(QuantifiersEngine* qe,
  52                                              Node f,
  53                                              unsigned nsamples,
  54                                              bool useSygusType)
  55 {
  56   d_doRewSynth = false;
  57   d_doQueryGen = false;
  58   d_doFilterLogicalStrength = false;
  59   d_sygus_fun = f;
  60   d_use_sygus_type = useSygusType;
  61   d_qe = qe;
  62   d_tds = qe->getTermDatabaseSygus();
  63   // initialize the sampler
  64   d_sampler.initializeSygus(d_tds, f, nsamples, useSygusType);
  65 }
  66
  67 void ExpressionMinerManager::enableRewriteRuleSynth()
  68 {
  69   if (d_doRewSynth)
  70   {
  71     // already enabled
  72     return;
  73   }
  74   d_doRewSynth = true;
  75   std::vector<Node> vars;
  76   d_sampler.getVariables(vars);
  77   // initialize the candidate rewrite database
  78   if (!d_sygus_fun.isNull())
  79   {
  80     Assert(d_qe != nullptr);
  81     d_crd.initializeSygus(vars, d_qe, d_sygus_fun, &d_sampler);
  82   }
  83   else
  84   {
  85     d_crd.initialize(vars, &d_sampler);
  86   }
  87   d_crd.setExtendedRewriter(&d_ext_rew);
  88   d_crd.setSilent(false);
  89 }
  90
  91 void ExpressionMinerManager::enableQueryGeneration(unsigned deqThresh)
  92 {
  93   if (d_doQueryGen)
  94   {
  95     // already enabled
  96     return;
  97   }
  98   d_doQueryGen = true;
  99   std::vector<Node> vars;
 100   d_sampler.getVariables(vars);
 101   // must also enable rewrite rule synthesis
 102   if (!d_doRewSynth)
 103   {
 104     // initialize the candidate rewrite database, in silent mode
 105     enableRewriteRuleSynth();
 106     d_crd.setSilent(true);
 107   }
 108   // initialize the query generator
 109   d_qg.initialize(vars, &d_sampler);
 110   d_qg.setThreshold(deqThresh);
 111 }
 112
 113 void ExpressionMinerManager::enableFilterWeakSolutions()
 114 {
 115   d_doFilterLogicalStrength = true;
 116   std::vector<Node> vars;
 117   d_sampler.getVariables(vars);
 118   d_sols.initialize(vars, &d_sampler);
 119   d_sols.setLogicallyStrong(true);
 120 }
 121
 122 void ExpressionMinerManager::enableFilterStrongSolutions()
 123 {
 124   d_doFilterLogicalStrength = true;
 125   std::vector<Node> vars;
 126   d_sampler.getVariables(vars);
 127   d_sols.initialize(vars, &d_sampler);
 128   d_sols.setLogicallyStrong(false);
 129 }
 130
 131 bool ExpressionMinerManager::addTerm(Node sol,
 132                                      std::ostream& out,
 133                                      bool& rew_print)
 134 {
 135   // set the builtin version
 136   Node solb = sol;
 137   if (d_use_sygus_type)
 138   {
 139     solb = d_tds->sygusToBuiltin(sol);
 140   }
 141
 142   // add to the candidate rewrite rule database
 143   bool ret = true;
 144   if (d_doRewSynth)
 145   {
 146     Node rsol = d_crd.addTerm(sol, options::sygusRewSynthRec(), out, rew_print);
 147     ret = (sol == rsol);
 148   }
 149
 150   // a unique term, let's try the query generator
 151   if (ret && d_doQueryGen)
 152   {
 153     d_qg.addTerm(solb, out);
 154   }
 155
 156   // filter based on logical strength
 157   if (ret && d_doFilterLogicalStrength)
 158   {
 159     ret = d_sols.addTerm(solb, out);
 160   }
 161   return ret;
 162 }
 163
 164 bool ExpressionMinerManager::addTerm(Node sol, std::ostream& out)
 165 {
 166   bool rew_print = false;
 167   return addTerm(sol, out, rew_print);
 168 }
 169
 170 }  // namespace quantifiers
 171 }  // namespace theory
 172 }  // namespace CVC4