src/theory/quantifiers/expr_miner_manager.cpp

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