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-2019 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 {
  32 }
  33
  34 void ExpressionMinerManager::initialize(const std::vector<Node>& vars,
  35                                         TypeNode tn,
  36                                         unsigned nsamples,
  37                                         bool unique_type_ids)
  38 {
  39   d_doRewSynth = false;
  40   d_doQueryGen = false;
  41   d_doFilterLogicalStrength = false;
  42   d_sygus_fun = Node::null();
  43   d_use_sygus_type = false;
  44   d_qe = nullptr;
  45   d_tds = nullptr;
  46   // initialize the sampler
  47   d_sampler.initialize(tn, vars, nsamples, unique_type_ids);
  48 }
  49
  50 void ExpressionMinerManager::initializeSygus(QuantifiersEngine* qe,
  51                                              Node f,
  52                                              unsigned nsamples,
  53                                              bool useSygusType)
  54 {
  55   d_doRewSynth = false;
  56   d_doQueryGen = false;
  57   d_doFilterLogicalStrength = false;
  58   d_sygus_fun = f;
  59   d_use_sygus_type = useSygusType;
  60   d_qe = qe;
  61   d_tds = qe->getTermDatabaseSygus();
  62   // initialize the sampler
  63   d_sampler.initializeSygus(d_tds, f, nsamples, useSygusType);
  64 }
  65
  66 void ExpressionMinerManager::enableRewriteRuleSynth()
  67 {
  68   if (d_doRewSynth)
  69   {
  70     // already enabled
  71     return;
  72   }
  73   d_doRewSynth = true;
  74   std::vector<Node> vars;
  75   d_sampler.getVariables(vars);
  76   // initialize the candidate rewrite database
  77   if (!d_sygus_fun.isNull())
  78   {
  79     Assert(d_qe != nullptr);
  80     d_crd.initializeSygus(vars, d_qe, d_sygus_fun, &d_sampler);
  81   }
  82   else
  83   {
  84     d_crd.initialize(vars, &d_sampler);
  85   }
  86   d_crd.setExtendedRewriter(&d_ext_rew);
  87   d_crd.setSilent(false);
  88 }
  89
  90 void ExpressionMinerManager::enableQueryGeneration(unsigned deqThresh)
  91 {
  92   if (d_doQueryGen)
  93   {
  94     // already enabled
  95     return;
  96   }
  97   d_doQueryGen = true;
  98   std::vector<Node> vars;
  99   d_sampler.getVariables(vars);
 100   // must also enable rewrite rule synthesis
 101   if (!d_doRewSynth)
 102   {
 103     // initialize the candidate rewrite database, in silent mode
 104     enableRewriteRuleSynth();
 105     d_crd.setSilent(true);
 106   }
 107   // initialize the query generator
 108   d_qg.initialize(vars, &d_sampler);
 109   d_qg.setThreshold(deqThresh);
 110 }
 111
 112 void ExpressionMinerManager::enableFilterWeakSolutions()
 113 {
 114   d_doFilterLogicalStrength = true;
 115   std::vector<Node> vars;
 116   d_sampler.getVariables(vars);
 117   d_sols.initialize(vars, &d_sampler);
 118   d_sols.setLogicallyStrong(true);
 119 }
 120
 121 void ExpressionMinerManager::enableFilterStrongSolutions()
 122 {
 123   d_doFilterLogicalStrength = true;
 124   std::vector<Node> vars;
 125   d_sampler.getVariables(vars);
 126   d_sols.initialize(vars, &d_sampler);
 127   d_sols.setLogicallyStrong(false);
 128 }
 129
 130 bool ExpressionMinerManager::addTerm(Node sol,
 131                                      std::ostream& out,
 132                                      bool& rew_print)
 133 {
 134   // set the builtin version
 135   Node solb = sol;
 136   if (d_use_sygus_type)
 137   {
 138     solb = d_tds->sygusToBuiltin(sol);
 139   }
 140
 141   // add to the candidate rewrite rule database
 142   bool ret = true;
 143   if (d_doRewSynth)
 144   {
 145     ret = d_crd.addTerm(sol, options::sygusRewSynthRec(), out, rew_print);
 146   }
 147
 148   // a unique term, let's try the query generator
 149   if (ret && d_doQueryGen)
 150   {
 151     d_qg.addTerm(solb, out);
 152   }
 153
 154   // filter based on logical strength
 155   if (ret && d_doFilterLogicalStrength)
 156   {
 157     ret = d_sols.addTerm(solb, out);
 158   }
 159   return ret;
 160 }
 161
 162 bool ExpressionMinerManager::addTerm(Node sol, std::ostream& out)
 163 {
 164   bool rew_print = false;
 165   return addTerm(sol, out, rew_print);
 166 }
 167
 168 }  // namespace quantifiers
 169 }  // namespace theory
 170 }  // namespace CVC4