Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_repair_const.cpp	Lines:	299	331	90.3 %
Date:	2021-05-22	Branches:	591	1436	41.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Haniel Barbosa, Abdalrhman Mohamed
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 * ****************************************************************************
 *
 * Implementation of sygus_repair_const.
 */

#include "theory/quantifiers/sygus/sygus_repair_const.h"

#include "expr/dtype_cons.h"
#include "expr/node_algorithm.h"
#include "expr/skolem_manager.h"
#include "options/base_options.h"
#include "options/quantifiers_options.h"
#include "printer/printer.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "smt/smt_statistics_registry.h"
#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/logic_info.h"
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/smt_engine_subsolver.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

SygusRepairConst::SygusRepairConst(TermDbSygus* tds)
    : d_tds(tds), d_allow_constant_grammar(false)
{
}

void SygusRepairConst::initialize(Node base_inst,
                                  const std::vector<Node>& candidates)
{
  Trace("sygus-repair-const") << "SygusRepairConst::initialize" << std::endl;
  Trace("sygus-repair-const") << "  conjecture : " << base_inst << std::endl;
  d_base_inst = base_inst;

  // compute whether there are "allow all constant" types in the variables of q
  std::map<TypeNode, bool> tprocessed;
  for (const Node& v : candidates)
  {
    TypeNode tn = v.getType();
    // do the type traversal of the sygus type
    registerSygusType(tn, tprocessed);
  }
  Trace("sygus-repair-const")
      << "  allow constants : " << d_allow_constant_grammar << std::endl;
}

// recursion depth bounded by number of types in grammar (small)
void SygusRepairConst::registerSygusType(TypeNode tn,
                                         std::map<TypeNode, bool>& tprocessed)
{
  if (tprocessed.find(tn) == tprocessed.end())
  {
    tprocessed[tn] = true;
    if (!tn.isDatatype())
    {
      // may have recursed to a non-datatype, e.g. in the case that we have
      // "any constant" constructors
      return;
    }
    const DType& dt = tn.getDType();
    if (!dt.isSygus())
    {
      // may have recursed to a non-sygus-datatype
      return;
    }
    // check if this datatype allows all constants
    if (dt.getSygusAllowConst())
    {
      d_allow_constant_grammar = true;
    }
    for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
    {
      const DTypeConstructor& dtc = dt[i];
      // recurse on all subfields
      for (unsigned j = 0, nargs = dtc.getNumArgs(); j < nargs; j++)
      {
        TypeNode tnc = d_tds->getArgType(dtc, j);
        registerSygusType(tnc, tprocessed);
      }
    }
  }
}

bool SygusRepairConst::isActive() const
{
  return !d_base_inst.isNull() && d_allow_constant_grammar;
}

bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
                                      const std::vector<Node>& candidate_values,
                                      std::vector<Node>& repair_cv,
                                      bool useConstantsAsHoles)
{
  return repairSolution(d_base_inst,
                        candidates,
                        candidate_values,
                        repair_cv,
                        useConstantsAsHoles);
}

bool SygusRepairConst::repairSolution(Node sygusBody,
                                      const std::vector<Node>& candidates,
                                      const std::vector<Node>& candidate_values,
                                      std::vector<Node>& repair_cv,
                                      bool useConstantsAsHoles)
{
  Assert(candidates.size() == candidate_values.size());

  // if no grammar type allows constants, no repair is possible
  if (!isActive())
  {
    return false;
  }
  if (Trace.isOn("sygus-repair-const"))
  {
    Trace("sygus-repair-const") << "Repair candidate solutions..." << std::endl;
    for (unsigned i = 0, size = candidates.size(); i < size; i++)
    {
      std::stringstream ss;
      TermDbSygus::toStreamSygus(ss, candidate_values[i]);
      Trace("sygus-repair-const")
          << "  " << candidates[i] << " -> " << ss.str() << std::endl;
    }
    Trace("sygus-repair-const")
        << "Getting candidate skeletons : " << std::endl;
  }
  std::vector<Node> candidate_skeletons;
  std::map<TypeNode, int> free_var_count;
  std::vector<Node> sk_vars;
  std::map<Node, Node> sk_vars_to_subs;
  for (unsigned i = 0, size = candidates.size(); i < size; i++)
  {
    Node cv = candidate_values[i];
    Node skeleton = getSkeleton(
        cv, free_var_count, sk_vars, sk_vars_to_subs, useConstantsAsHoles);
    if (Trace.isOn("sygus-repair-const"))
    {
      std::stringstream ss;
      TermDbSygus::toStreamSygus(ss, cv);
      Trace("sygus-repair-const")
          << "Solution #" << i << " : " << ss.str() << std::endl;
      if (skeleton == cv)
      {
        Trace("sygus-repair-const") << "...solution unchanged" << std::endl;
      }
      else
      {
        std::stringstream sss;
        TermDbSygus::toStreamSygus(sss, skeleton);
        Trace("sygus-repair-const")
            << "...inferred skeleton : " << sss.str() << std::endl;
      }
    }
    candidate_skeletons.push_back(skeleton);
  }

  if (sk_vars.empty())
  {
    Trace("sygus-repair-const") << "...no solutions repaired." << std::endl;
    return false;
  }

  Trace("sygus-repair-const") << "Get first-order query..." << std::endl;
  Node fo_body =
      getFoQuery(sygusBody, candidates, candidate_skeletons, sk_vars);

  Trace("sygus-repair-const-debug") << "...got : " << fo_body << std::endl;

  if (d_queries.find(fo_body) != d_queries.end())
  {
    Trace("sygus-repair-const") << "...duplicate query." << std::endl;
    return false;
  }
  d_queries.insert(fo_body);

  // check whether it is not in the current logic, e.g. non-linear arithmetic.
  // if so, undo replacements until it is in the current logic.
  LogicInfo logic = smt::currentSmtEngine()->getLogicInfo();
  if (logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear())
  {
    fo_body = fitToLogic(sygusBody,
                         logic,
                         fo_body,
                         candidates,
                         candidate_skeletons,
                         sk_vars,
                         sk_vars_to_subs);
    Trace("sygus-repair-const-debug")
        << "...after fit-to-logic : " << fo_body << std::endl;
  }
  Assert(!expr::hasFreeVar(fo_body));

  if (fo_body.isNull() || sk_vars.empty())
  {
    Trace("sygus-repair-const")
        << "...all skeleton variables lead to bad logic." << std::endl;
    return false;
  }

  Trace("sygus-repair-const") << "Make satisfiabily query..." << std::endl;
  if (fo_body.getKind() == FORALL)
  {
    // must be a CBQI quantifier
    CegHandledStatus hstatus = CegInstantiator::isCbqiQuant(fo_body);
    if (hstatus < CEG_HANDLED)
    {
      // abort if less than fully handled
      Trace("sygus-repair-const") << "...first-order query is not handlable by "
                                     "counterexample-guided instantiation."
                                  << std::endl;
      return false;
    }
  }

  Trace("sygus-engine") << "Repairing previous solution..." << std::endl;
  // make the satisfiability query
  std::unique_ptr<SmtEngine> repcChecker;
  // initialize the subsolver using the standard method
  initializeSubsolver(repcChecker,
                      Options::current().wasSetByUser(options::sygusRepairConstTimeout),
                      options::sygusRepairConstTimeout());
  // renable options disabled by sygus
  repcChecker->setOption("miniscope-quant", "true");
  repcChecker->setOption("miniscope-quant-fv", "true");
  repcChecker->setOption("quant-split", "true");
  repcChecker->assertFormula(fo_body);
  // check satisfiability
  Result r = repcChecker->checkSat();
  Trace("sygus-repair-const") << "...got : " << r << std::endl;
  if (r.asSatisfiabilityResult().isSat() == Result::UNSAT
      || r.asSatisfiabilityResult().isUnknown())
  {
    Trace("sygus-engine") << "...failed" << std::endl;
    return false;
  }
  std::vector<Node> sk_sygus_m;
  for (const Node& v : sk_vars)
  {
    Assert(d_sk_to_fo.find(v) != d_sk_to_fo.end());
    Node fov = d_sk_to_fo[v];
    Node fov_m = repcChecker->getValue(fov);
    Trace("sygus-repair-const") << "  " << fov << " = " << fov_m << std::endl;
    // convert to sygus
    Node fov_m_to_sygus = d_tds->getProxyVariable(v.getType(), fov_m);
    sk_sygus_m.push_back(fov_m_to_sygus);
  }
  std::stringstream ss;
  // convert back to sygus
  for (unsigned i = 0, size = candidates.size(); i < size; i++)
  {
    Node csk = candidate_skeletons[i];
    Node scsk = csk.substitute(
        sk_vars.begin(), sk_vars.end(), sk_sygus_m.begin(), sk_sygus_m.end());
    repair_cv.push_back(scsk);
    if (Trace.isOn("sygus-repair-const") || Trace.isOn("sygus-engine"))
    {
      std::stringstream sss;
      TermDbSygus::toStreamSygus(sss, repair_cv[i]);
      ss << "  * " << candidates[i] << " -> " << sss.str() << std::endl;
    }
  }
  Trace("sygus-engine") << "...success:" << std::endl;
  Trace("sygus-engine") << ss.str();
  Trace("sygus-repair-const")
      << "Repaired constants in solution : " << std::endl;
  Trace("sygus-repair-const") << ss.str();
  return true;
}

bool SygusRepairConst::mustRepair(Node n)
{
  std::unordered_set<TNode> visited;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    if (visited.find(cur) == visited.end())
    {
      visited.insert(cur);
      Assert(cur.getKind() == APPLY_CONSTRUCTOR);
      if (isRepairable(cur, false))
      {
        return true;
      }
      for (const Node& cn : cur)
      {
        visit.push_back(cn);
      }
    }
  } while (!visit.empty());

  return false;
}

bool SygusRepairConst::isRepairable(Node n, bool useConstantsAsHoles)
{
  if (n.getKind() != APPLY_CONSTRUCTOR)
  {
    return false;
  }
  TypeNode tn = n.getType();
  Assert(tn.isDatatype());
  const DType& dt = tn.getDType();
  if (!dt.isSygus())
  {
    return false;
  }
  Node op = n.getOperator();
  unsigned cindex = datatypes::utils::indexOf(op);
  Node sygusOp = dt[cindex].getSygusOp();
  if (sygusOp.getAttribute(SygusAnyConstAttribute()))
  {
    // if it represents "any constant" then it is repairable
    return true;
  }
  if (dt[cindex].getNumArgs() > 0)
  {
    return false;
  }
  if (useConstantsAsHoles && dt.getSygusAllowConst())
  {
    if (sygusOp.isConst())
    {
      // if a constant, it is repairable
      return true;
    }
  }
  return false;
}

Node SygusRepairConst::getSkeleton(Node n,
                                   std::map<TypeNode, int>& free_var_count,
                                   std::vector<Node>& sk_vars,
                                   std::map<Node, Node>& sk_vars_to_subs,
                                   bool useConstantsAsHoles)
{
  if (isRepairable(n, useConstantsAsHoles))
  {
    Node sk_var = d_tds->getFreeVarInc(n.getType(), free_var_count);
    sk_vars.push_back(sk_var);
    sk_vars_to_subs[sk_var] = n;
    Trace("sygus-repair-const-debug")
        << "Var to subs : " << sk_var << " -> " << n << std::endl;
    return sk_var;
  }
  NodeManager* nm = NodeManager::currentNM();
  // get the most general candidate skeleton of n
  std::unordered_map<TNode, Node> visited;
  std::unordered_map<TNode, Node>::iterator it;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = visited.find(cur);

    if (it == visited.end())
    {
      visited[cur] = Node::null();
      visit.push_back(cur);
      for (const Node& cn : cur)
      {
        visit.push_back(cn);
      }
    }
    else if (it->second.isNull())
    {
      Node ret = cur;
      bool childChanged = false;
      std::vector<Node> children;
      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
      {
        children.push_back(cur.getOperator());
      }
      for (const Node& cn : cur)
      {
        Node child;
        // if it is repairable
        if (isRepairable(cn, useConstantsAsHoles))
        {
          // replace it by the next free variable
          child = d_tds->getFreeVarInc(cn.getType(), free_var_count);
          sk_vars.push_back(child);
          sk_vars_to_subs[child] = cn;
          Trace("sygus-repair-const-debug")
              << "Var to subs : " << child << " -> " << cn << std::endl;
        }
        else
        {
          it = visited.find(cn);
          Assert(it != visited.end());
          Assert(!it->second.isNull());
          child = it->second;
        }
        childChanged = childChanged || cn != child;
        children.push_back(child);
      }
      if (childChanged)
      {
        ret = nm->mkNode(cur.getKind(), children);
      }
      visited[cur] = ret;
    }
  } while (!visit.empty());
  Assert(visited.find(n) != visited.end());
  Assert(!visited.find(n)->second.isNull());
  return visited[n];
}

Node SygusRepairConst::getFoQuery(Node body,
                                  const std::vector<Node>& candidates,
                                  const std::vector<Node>& candidate_skeletons,
                                  const std::vector<Node>& sk_vars)
{
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  Trace("sygus-repair-const") << "  Substitute skeletons..." << std::endl;
  body = body.substitute(candidates.begin(),
                         candidates.end(),
                         candidate_skeletons.begin(),
                         candidate_skeletons.end());
  Trace("sygus-repair-const-debug") << "  ...got : " << body << std::endl;

  Trace("sygus-repair-const") << "  Unfold the specification..." << std::endl;
  body = d_tds->evaluateWithUnfolding(body);
  Trace("sygus-repair-const-debug") << "  ...got : " << body << std::endl;

  Trace("sygus-repair-const") << "  Introduce first-order vars..." << std::endl;
  for (const Node& v : sk_vars)
  {
    std::map<Node, Node>::iterator itf = d_sk_to_fo.find(v);
    if (itf == d_sk_to_fo.end())
    {
      TypeNode builtinType = d_tds->sygusToBuiltinType(v.getType());
      Node sk_fov = sm->mkDummySkolem("k", builtinType);
      d_sk_to_fo[v] = sk_fov;
      d_fo_to_sk[sk_fov] = v;
      Trace("sygus-repair-const-debug")
          << "Map " << v << " -> " << sk_fov << std::endl;
    }
  }
  // now, we must replace all terms of the form eval( z_i, t1...tn ) with
  // a fresh first-order variable w_i, where z_i is a variable introduced in
  // the skeleton inference step (z_i is a variable in sk_vars).
  std::unordered_map<TNode, Node> visited;
  std::unordered_map<TNode, Node>::iterator it;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(body);
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = visited.find(cur);

    if (it == visited.end())
    {
      visited[cur] = Node::null();
      if (cur.getKind() == DT_SYGUS_EVAL)
      {
        Node v = cur[0];
        if (std::find(sk_vars.begin(), sk_vars.end(), v) != sk_vars.end())
        {
          std::map<Node, Node>::iterator itf = d_sk_to_fo.find(v);
          Assert(itf != d_sk_to_fo.end());
          visited[cur] = itf->second;
        }
      }
      if (visited[cur].isNull())
      {
        visit.push_back(cur);
        for (const Node& cn : cur)
        {
          visit.push_back(cn);
        }
      }
    }
    else if (it->second.isNull())
    {
      Node ret = cur;
      bool childChanged = false;
      std::vector<Node> children;
      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
      {
        children.push_back(cur.getOperator());
      }
      for (const Node& cn : cur)
      {
        it = visited.find(cn);
        Assert(it != visited.end());
        Assert(!it->second.isNull());
        childChanged = childChanged || cn != it->second;
        children.push_back(it->second);
      }
      if (childChanged)
      {
        ret = nm->mkNode(cur.getKind(), children);
      }
      visited[cur] = ret;
    }
  } while (!visit.empty());
  Assert(visited.find(body) != visited.end());
  Assert(!visited.find(body)->second.isNull());
  Node fo_body = visited[body];
  Trace("sygus-repair-const-debug") << "  ...got : " << fo_body << std::endl;
  return fo_body;
}

Node SygusRepairConst::fitToLogic(Node body,
                                  LogicInfo& logic,
                                  Node n,
                                  const std::vector<Node>& candidates,
                                  std::vector<Node>& candidate_skeletons,
                                  std::vector<Node>& sk_vars,
                                  std::map<Node, Node>& sk_vars_to_subs)
{
  std::vector<Node> rm_var;
  Node exc_var;
  while (getFitToLogicExcludeVar(logic, n, exc_var))
  {
    if (exc_var.isNull())
    {
      return n;
    }
    Trace("sygus-repair-const") << "...exclude " << exc_var
                                << " due to logic restrictions." << std::endl;
    TNode tvar = exc_var;
    Assert(sk_vars_to_subs.find(exc_var) != sk_vars_to_subs.end());
    TNode tsubs = sk_vars_to_subs[exc_var];
    // revert the substitution
    for (unsigned i = 0, size = candidate_skeletons.size(); i < size; i++)
    {
      candidate_skeletons[i] = candidate_skeletons[i].substitute(tvar, tsubs);
    }
    // remove the variable
    sk_vars_to_subs.erase(exc_var);
    std::vector<Node>::iterator it =
        std::find(sk_vars.begin(), sk_vars.end(), exc_var);
    Assert(it != sk_vars.end());
    sk_vars.erase(it);
    // reconstruct the query
    n = getFoQuery(body, candidates, candidate_skeletons, sk_vars);
    // reset the exclusion variable
    exc_var = Node::null();
  }
  return Node::null();
}

bool SygusRepairConst::getFitToLogicExcludeVar(LogicInfo& logic,
                                               Node n,
                                               Node& exvar)
{
  bool restrictLA = logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear();

  // should have at least one restriction
  Assert(restrictLA);

  std::unordered_set<TNode> visited;
  std::unordered_set<TNode>::iterator it;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = visited.find(cur);

    if (it == visited.end())
    {
      visited.insert(cur);
      Kind ck = cur.getKind();
      bool isArithDivKind = (ck == DIVISION_TOTAL || ck == INTS_DIVISION_TOTAL
                             || ck == INTS_MODULUS_TOTAL);
      Assert(ck != DIVISION && ck != INTS_DIVISION && ck != INTS_MODULUS);
      if (restrictLA && (ck == NONLINEAR_MULT || isArithDivKind))
      {
        for (unsigned j = 0, size = cur.getNumChildren(); j < size; j++)
        {
          Node ccur = cur[j];
          std::map<Node, Node>::iterator itf = d_fo_to_sk.find(ccur);
          if (itf != d_fo_to_sk.end())
          {
            if (ck == NONLINEAR_MULT || (isArithDivKind && j == 1))
            {
              exvar = itf->second;
              return true;
            }
          }
        }
        return false;
      }
      for (const Node& ccur : cur)
      {
        visit.push_back(ccur);
      }
    }
  } while (!visit.empty());

  return true;
}

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Haniel Barbosa, Abdalrhman Mohamed
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 sygus_repair_const.
14		*/
15
16		#include "theory/quantifiers/sygus/sygus_repair_const.h"
17
18		#include "expr/dtype_cons.h"
19		#include "expr/node_algorithm.h"
20		#include "expr/skolem_manager.h"
21		#include "options/base_options.h"
22		#include "options/quantifiers_options.h"
23		#include "printer/printer.h"
24		#include "smt/smt_engine.h"
25		#include "smt/smt_engine_scope.h"
26		#include "smt/smt_statistics_registry.h"
27		#include "theory/datatypes/theory_datatypes_utils.h"
28		#include "theory/logic_info.h"
29		#include "theory/quantifiers/cegqi/ceg_instantiator.h"
30		#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
31		#include "theory/quantifiers/sygus/term_database_sygus.h"
32		#include "theory/smt_engine_subsolver.h"
33
34		using namespace cvc5::kind;
35
36		namespace cvc5 {
37		namespace theory {
38		namespace quantifiers {
39
40	1529	SygusRepairConst::SygusRepairConst(TermDbSygus* tds)
41	1529	: d_tds(tds), d_allow_constant_grammar(false)
42		{
43	1529	}
44
45	8	void SygusRepairConst::initialize(Node base_inst,
46		const std::vector<Node>& candidates)
47		{
48	8	Trace("sygus-repair-const") << "SygusRepairConst::initialize" << std::endl;
49	8	Trace("sygus-repair-const") << " conjecture : " << base_inst << std::endl;
50	8	d_base_inst = base_inst;
51
52		// compute whether there are "allow all constant" types in the variables of q
53	16	std::map<TypeNode, bool> tprocessed;
54	16	for (const Node& v : candidates)
55		{
56	16	TypeNode tn = v.getType();
57		// do the type traversal of the sygus type
58	8	registerSygusType(tn, tprocessed);
59		}
60	16	Trace("sygus-repair-const")
61	8	<< " allow constants : " << d_allow_constant_grammar << std::endl;
62	8	}
63
64		// recursion depth bounded by number of types in grammar (small)
65	105	void SygusRepairConst::registerSygusType(TypeNode tn,
66		std::map<TypeNode, bool>& tprocessed)
67		{
68	105	if (tprocessed.find(tn) == tprocessed.end())
69		{
70	30	tprocessed[tn] = true;
71	30	if (!tn.isDatatype())
72		{
73		// may have recursed to a non-datatype, e.g. in the case that we have
74		// "any constant" constructors
75	10	return;
76		}
77	20	const DType& dt = tn.getDType();
78	20	if (!dt.isSygus())
79		{
80		// may have recursed to a non-sygus-datatype
81		return;
82		}
83		// check if this datatype allows all constants
84	20	if (dt.getSygusAllowConst())
85		{
86	16	d_allow_constant_grammar = true;
87		}
88	107	for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
89		{
90	87	const DTypeConstructor& dtc = dt[i];
91		// recurse on all subfields
92	184	for (unsigned j = 0, nargs = dtc.getNumArgs(); j < nargs; j++)
93		{
94	194	TypeNode tnc = d_tds->getArgType(dtc, j);
95	97	registerSygusType(tnc, tprocessed);
96		}
97		}
98		}
99		}
100
101	149	bool SygusRepairConst::isActive() const
102		{
103	149	return !d_base_inst.isNull() && d_allow_constant_grammar;
104		}
105
106	77	bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
107		const std::vector<Node>& candidate_values,
108		std::vector<Node>& repair_cv,
109		bool useConstantsAsHoles)
110		{
111	154	return repairSolution(d_base_inst,
112		candidates,
113		candidate_values,
114		repair_cv,
115	154	useConstantsAsHoles);
116		}
117
118	149	bool SygusRepairConst::repairSolution(Node sygusBody,
119		const std::vector<Node>& candidates,
120		const std::vector<Node>& candidate_values,
121		std::vector<Node>& repair_cv,
122		bool useConstantsAsHoles)
123		{
124	149	Assert(candidates.size() == candidate_values.size());
125
126		// if no grammar type allows constants, no repair is possible
127	149	if (!isActive())
128		{
129		return false;
130		}
131	149	if (Trace.isOn("sygus-repair-const"))
132		{
133		Trace("sygus-repair-const") << "Repair candidate solutions..." << std::endl;
134		for (unsigned i = 0, size = candidates.size(); i < size; i++)
135		{
136		std::stringstream ss;
137		TermDbSygus::toStreamSygus(ss, candidate_values[i]);
138		Trace("sygus-repair-const")
139		<< " " << candidates[i] << " -> " << ss.str() << std::endl;
140		}
141		Trace("sygus-repair-const")
142		<< "Getting candidate skeletons : " << std::endl;
143		}
144	298	std::vector<Node> candidate_skeletons;
145	298	std::map<TypeNode, int> free_var_count;
146	298	std::vector<Node> sk_vars;
147	298	std::map<Node, Node> sk_vars_to_subs;
148	298	for (unsigned i = 0, size = candidates.size(); i < size; i++)
149		{
150	298	Node cv = candidate_values[i];
151		Node skeleton = getSkeleton(
152	298	cv, free_var_count, sk_vars, sk_vars_to_subs, useConstantsAsHoles);
153	149	if (Trace.isOn("sygus-repair-const"))
154		{
155		std::stringstream ss;
156		TermDbSygus::toStreamSygus(ss, cv);
157		Trace("sygus-repair-const")
158		<< "Solution #" << i << " : " << ss.str() << std::endl;
159		if (skeleton == cv)
160		{
161		Trace("sygus-repair-const") << "...solution unchanged" << std::endl;
162		}
163		else
164		{
165		std::stringstream sss;
166		TermDbSygus::toStreamSygus(sss, skeleton);
167		Trace("sygus-repair-const")
168		<< "...inferred skeleton : " << sss.str() << std::endl;
169		}
170		}
171	149	candidate_skeletons.push_back(skeleton);
172		}
173
174	149	if (sk_vars.empty())
175		{
176		Trace("sygus-repair-const") << "...no solutions repaired." << std::endl;
177		return false;
178		}
179
180	149	Trace("sygus-repair-const") << "Get first-order query..." << std::endl;
181		Node fo_body =
182	298	getFoQuery(sygusBody, candidates, candidate_skeletons, sk_vars);
183
184	149	Trace("sygus-repair-const-debug") << "...got : " << fo_body << std::endl;
185
186	149	if (d_queries.find(fo_body) != d_queries.end())
187		{
188	20	Trace("sygus-repair-const") << "...duplicate query." << std::endl;
189	20	return false;
190		}
191	129	d_queries.insert(fo_body);
192
193		// check whether it is not in the current logic, e.g. non-linear arithmetic.
194		// if so, undo replacements until it is in the current logic.
195	258	LogicInfo logic = smt::currentSmtEngine()->getLogicInfo();
196	129	if (logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear())
197		{
198	85	fo_body = fitToLogic(sygusBody,
199		logic,
200		fo_body,
201		candidates,
202		candidate_skeletons,
203		sk_vars,
204		sk_vars_to_subs);
205	170	Trace("sygus-repair-const-debug")
206	85	<< "...after fit-to-logic : " << fo_body << std::endl;
207		}
208	129	Assert(!expr::hasFreeVar(fo_body));
209
210	129	if (fo_body.isNull() \|\| sk_vars.empty())
211		{
212	6	Trace("sygus-repair-const")
213	3	<< "...all skeleton variables lead to bad logic." << std::endl;
214	3	return false;
215		}
216
217	126	Trace("sygus-repair-const") << "Make satisfiabily query..." << std::endl;
218	126	if (fo_body.getKind() == FORALL)
219		{
220		// must be a CBQI quantifier
221	58	CegHandledStatus hstatus = CegInstantiator::isCbqiQuant(fo_body);
222	58	if (hstatus < CEG_HANDLED)
223		{
224		// abort if less than fully handled
225		Trace("sygus-repair-const") << "...first-order query is not handlable by "
226		"counterexample-guided instantiation."
227		<< std::endl;
228		return false;
229		}
230		}
231
232	126	Trace("sygus-engine") << "Repairing previous solution..." << std::endl;
233		// make the satisfiability query
234	252	std::unique_ptr<SmtEngine> repcChecker;
235		// initialize the subsolver using the standard method
236	252	initializeSubsolver(repcChecker,
237	378	Options::current().wasSetByUser(options::sygusRepairConstTimeout),
238	126	options::sygusRepairConstTimeout());
239		// renable options disabled by sygus
240	126	repcChecker->setOption("miniscope-quant", "true");
241	126	repcChecker->setOption("miniscope-quant-fv", "true");
242	126	repcChecker->setOption("quant-split", "true");
243	126	repcChecker->assertFormula(fo_body);
244		// check satisfiability
245	252	Result r = repcChecker->checkSat();
246	126	Trace("sygus-repair-const") << "...got : " << r << std::endl;
247	378	if (r.asSatisfiabilityResult().isSat() == Result::UNSAT
248	378	\|\| r.asSatisfiabilityResult().isUnknown())
249		{
250	115	Trace("sygus-engine") << "...failed" << std::endl;
251	115	return false;
252		}
253	22	std::vector<Node> sk_sygus_m;
254	28	for (const Node& v : sk_vars)
255		{
256	17	Assert(d_sk_to_fo.find(v) != d_sk_to_fo.end());
257	34	Node fov = d_sk_to_fo[v];
258	34	Node fov_m = repcChecker->getValue(fov);
259	17	Trace("sygus-repair-const") << " " << fov << " = " << fov_m << std::endl;
260		// convert to sygus
261	34	Node fov_m_to_sygus = d_tds->getProxyVariable(v.getType(), fov_m);
262	17	sk_sygus_m.push_back(fov_m_to_sygus);
263		}
264	22	std::stringstream ss;
265		// convert back to sygus
266	22	for (unsigned i = 0, size = candidates.size(); i < size; i++)
267		{
268	22	Node csk = candidate_skeletons[i];
269		Node scsk = csk.substitute(
270	22	sk_vars.begin(), sk_vars.end(), sk_sygus_m.begin(), sk_sygus_m.end());
271	11	repair_cv.push_back(scsk);
272	11	if (Trace.isOn("sygus-repair-const") \|\| Trace.isOn("sygus-engine"))
273		{
274		std::stringstream sss;
275		TermDbSygus::toStreamSygus(sss, repair_cv[i]);
276		ss << " * " << candidates[i] << " -> " << sss.str() << std::endl;
277		}
278		}
279	11	Trace("sygus-engine") << "...success:" << std::endl;
280	11	Trace("sygus-engine") << ss.str();
281	22	Trace("sygus-repair-const")
282	11	<< "Repaired constants in solution : " << std::endl;
283	11	Trace("sygus-repair-const") << ss.str();
284	11	return true;
285		}
286
287	125	bool SygusRepairConst::mustRepair(Node n)
288		{
289	250	std::unordered_set<TNode> visited;
290	250	std::vector<TNode> visit;
291	250	TNode cur;
292	125	visit.push_back(n);
293	263	do
294		{
295	388	cur = visit.back();
296	388	visit.pop_back();
297	388	if (visited.find(cur) == visited.end())
298		{
299	352	visited.insert(cur);
300	352	Assert(cur.getKind() == APPLY_CONSTRUCTOR);
301	352	if (isRepairable(cur, false))
302		{
303	77	return true;
304		}
305	652	for (const Node& cn : cur)
306		{
307	377	visit.push_back(cn);
308		}
309		}
310	311	} while (!visit.empty());
311
312	48	return false;
313		}
314
315	1226	bool SygusRepairConst::isRepairable(Node n, bool useConstantsAsHoles)
316		{
317	1226	if (n.getKind() != APPLY_CONSTRUCTOR)
318		{
319	172	return false;
320		}
321	2108	TypeNode tn = n.getType();
322	1054	Assert(tn.isDatatype());
323	1054	const DType& dt = tn.getDType();
324	1054	if (!dt.isSygus())
325		{
326		return false;
327		}
328	2108	Node op = n.getOperator();
329	1054	unsigned cindex = datatypes::utils::indexOf(op);
330	2108	Node sygusOp = dt[cindex].getSygusOp();
331	1054	if (sygusOp.getAttribute(SygusAnyConstAttribute()))
332		{
333		// if it represents "any constant" then it is repairable
334	288	return true;
335		}
336	766	if (dt[cindex].getNumArgs() > 0)
337		{
338	364	return false;
339		}
340	402	if (useConstantsAsHoles && dt.getSygusAllowConst())
341		{
342		if (sygusOp.isConst())
343		{
344		// if a constant, it is repairable
345		return true;
346		}
347		}
348	402	return false;
349		}
350
351	149	Node SygusRepairConst::getSkeleton(Node n,
352		std::map<TypeNode, int>& free_var_count,
353		std::vector<Node>& sk_vars,
354		std::map<Node, Node>& sk_vars_to_subs,
355		bool useConstantsAsHoles)
356		{
357	149	if (isRepairable(n, useConstantsAsHoles))
358		{
359	4	Node sk_var = d_tds->getFreeVarInc(n.getType(), free_var_count);
360	2	sk_vars.push_back(sk_var);
361	2	sk_vars_to_subs[sk_var] = n;
362	4	Trace("sygus-repair-const-debug")
363	2	<< "Var to subs : " << sk_var << " -> " << n << std::endl;
364	2	return sk_var;
365		}
366	147	NodeManager* nm = NodeManager::currentNM();
367		// get the most general candidate skeleton of n
368	294	std::unordered_map<TNode, Node> visited;
369	147	std::unordered_map<TNode, Node>::iterator it;
370	294	std::vector<TNode> visit;
371	294	TNode cur;
372	147	visit.push_back(n);
373	1506	do
374		{
375	1653	cur = visit.back();
376	1653	visit.pop_back();
377	1653	it = visited.find(cur);
378
379	1653	if (it == visited.end())
380		{
381	781	visited[cur] = Node::null();
382	781	visit.push_back(cur);
383	1506	for (const Node& cn : cur)
384		{
385	725	visit.push_back(cn);
386		}
387		}
388	872	else if (it->second.isNull())
389		{
390	1562	Node ret = cur;
391	781	bool childChanged = false;
392	1562	std::vector<Node> children;
393	781	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
394		{
395	609	children.push_back(cur.getOperator());
396		}
397	1506	for (const Node& cn : cur)
398		{
399	1450	Node child;
400		// if it is repairable
401	725	if (isRepairable(cn, useConstantsAsHoles))
402		{
403		// replace it by the next free variable
404	209	child = d_tds->getFreeVarInc(cn.getType(), free_var_count);
405	209	sk_vars.push_back(child);
406	209	sk_vars_to_subs[child] = cn;
407	418	Trace("sygus-repair-const-debug")
408	209	<< "Var to subs : " << child << " -> " << cn << std::endl;
409		}
410		else
411		{
412	516	it = visited.find(cn);
413	516	Assert(it != visited.end());
414	516	Assert(!it->second.isNull());
415	516	child = it->second;
416		}
417	725	childChanged = childChanged \|\| cn != child;
418	725	children.push_back(child);
419		}
420	781	if (childChanged)
421		{
422	200	ret = nm->mkNode(cur.getKind(), children);
423		}
424	781	visited[cur] = ret;
425		}
426	1653	} while (!visit.empty());
427	147	Assert(visited.find(n) != visited.end());
428	147	Assert(!visited.find(n)->second.isNull());
429	147	return visited[n];
430		}
431
432	152	Node SygusRepairConst::getFoQuery(Node body,
433		const std::vector<Node>& candidates,
434		const std::vector<Node>& candidate_skeletons,
435		const std::vector<Node>& sk_vars)
436		{
437	152	NodeManager* nm = NodeManager::currentNM();
438	152	SkolemManager* sm = nm->getSkolemManager();
439	152	Trace("sygus-repair-const") << " Substitute skeletons..." << std::endl;
440	152	body = body.substitute(candidates.begin(),
441		candidates.end(),
442		candidate_skeletons.begin(),
443		candidate_skeletons.end());
444	152	Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl;
445
446	152	Trace("sygus-repair-const") << " Unfold the specification..." << std::endl;
447	152	body = d_tds->evaluateWithUnfolding(body);
448	152	Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl;
449
450	152	Trace("sygus-repair-const") << " Introduce first-order vars..." << std::endl;
451	367	for (const Node& v : sk_vars)
452		{
453	215	std::map<Node, Node>::iterator itf = d_sk_to_fo.find(v);
454	215	if (itf == d_sk_to_fo.end())
455		{
456	32	TypeNode builtinType = d_tds->sygusToBuiltinType(v.getType());
457	32	Node sk_fov = sm->mkDummySkolem("k", builtinType);
458	16	d_sk_to_fo[v] = sk_fov;
459	16	d_fo_to_sk[sk_fov] = v;
460	32	Trace("sygus-repair-const-debug")
461	16	<< "Map " << v << " -> " << sk_fov << std::endl;
462		}
463		}
464		// now, we must replace all terms of the form eval( z_i, t1...tn ) with
465		// a fresh first-order variable w_i, where z_i is a variable introduced in
466		// the skeleton inference step (z_i is a variable in sk_vars).
467	304	std::unordered_map<TNode, Node> visited;
468	152	std::unordered_map<TNode, Node>::iterator it;
469	304	std::vector<TNode> visit;
470	304	TNode cur;
471	152	visit.push_back(body);
472	11250	do
473		{
474	11402	cur = visit.back();
475	11402	visit.pop_back();
476	11402	it = visited.find(cur);
477
478	11402	if (it == visited.end())
479		{
480	5249	visited[cur] = Node::null();
481	5249	if (cur.getKind() == DT_SYGUS_EVAL)
482		{
483	1954	Node v = cur[0];
484	977	if (std::find(sk_vars.begin(), sk_vars.end(), v) != sk_vars.end())
485		{
486	977	std::map<Node, Node>::iterator itf = d_sk_to_fo.find(v);
487	977	Assert(itf != d_sk_to_fo.end());
488	977	visited[cur] = itf->second;
489		}
490		}
491	5249	if (visited[cur].isNull())
492		{
493	4272	visit.push_back(cur);
494	11250	for (const Node& cn : cur)
495		{
496	6978	visit.push_back(cn);
497		}
498		}
499		}
500	6153	else if (it->second.isNull())
501		{
502	8544	Node ret = cur;
503	4272	bool childChanged = false;
504	8544	std::vector<Node> children;
505	4272	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
506		{
507	160	children.push_back(cur.getOperator());
508		}
509	11250	for (const Node& cn : cur)
510		{
511	6978	it = visited.find(cn);
512	6978	Assert(it != visited.end());
513	6978	Assert(!it->second.isNull());
514	6978	childChanged = childChanged \|\| cn != it->second;
515	6978	children.push_back(it->second);
516		}
517	4272	if (childChanged)
518		{
519	1932	ret = nm->mkNode(cur.getKind(), children);
520		}
521	4272	visited[cur] = ret;
522		}
523	11402	} while (!visit.empty());
524	152	Assert(visited.find(body) != visited.end());
525	152	Assert(!visited.find(body)->second.isNull());
526	152	Node fo_body = visited[body];
527	152	Trace("sygus-repair-const-debug") << " ...got : " << fo_body << std::endl;
528	304	return fo_body;
529		}
530
531	85	Node SygusRepairConst::fitToLogic(Node body,
532		LogicInfo& logic,
533		Node n,
534		const std::vector<Node>& candidates,
535		std::vector<Node>& candidate_skeletons,
536		std::vector<Node>& sk_vars,
537		std::map<Node, Node>& sk_vars_to_subs)
538		{
539	170	std::vector<Node> rm_var;
540	170	Node exc_var;
541	91	while (getFitToLogicExcludeVar(logic, n, exc_var))
542		{
543	85	if (exc_var.isNull())
544		{
545	82	return n;
546		}
547	6	Trace("sygus-repair-const") << "...exclude " << exc_var
548	3	<< " due to logic restrictions." << std::endl;
549	6	TNode tvar = exc_var;
550	3	Assert(sk_vars_to_subs.find(exc_var) != sk_vars_to_subs.end());
551	6	TNode tsubs = sk_vars_to_subs[exc_var];
552		// revert the substitution
553	6	for (unsigned i = 0, size = candidate_skeletons.size(); i < size; i++)
554		{
555	3	candidate_skeletons[i] = candidate_skeletons[i].substitute(tvar, tsubs);
556		}
557		// remove the variable
558	3	sk_vars_to_subs.erase(exc_var);
559		std::vector<Node>::iterator it =
560	3	std::find(sk_vars.begin(), sk_vars.end(), exc_var);
561	3	Assert(it != sk_vars.end());
562	3	sk_vars.erase(it);
563		// reconstruct the query
564	3	n = getFoQuery(body, candidates, candidate_skeletons, sk_vars);
565		// reset the exclusion variable
566	3	exc_var = Node::null();
567		}
568	3	return Node::null();
569		}
570
571	88	bool SygusRepairConst::getFitToLogicExcludeVar(LogicInfo& logic,
572		Node n,
573		Node& exvar)
574		{
575	88	bool restrictLA = logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear();
576
577		// should have at least one restriction
578	88	Assert(restrictLA);
579
580	176	std::unordered_set<TNode> visited;
581	88	std::unordered_set<TNode>::iterator it;
582	176	std::vector<TNode> visit;
583	176	TNode cur;
584	88	visit.push_back(n);
585	3614	do
586		{
587	3702	cur = visit.back();
588	3702	visit.pop_back();
589	3702	it = visited.find(cur);
590
591	3702	if (it == visited.end())
592		{
593	2417	visited.insert(cur);
594	2417	Kind ck = cur.getKind();
595	4834	bool isArithDivKind = (ck == DIVISION_TOTAL \|\| ck == INTS_DIVISION_TOTAL
596	4834	\|\| ck == INTS_MODULUS_TOTAL);
597	2417	Assert(ck != DIVISION && ck != INTS_DIVISION && ck != INTS_MODULUS);
598	2417	if (restrictLA && (ck == NONLINEAR_MULT \|\| isArithDivKind))
599		{
600	15	for (unsigned j = 0, size = cur.getNumChildren(); j < size; j++)
601		{
602	21	Node ccur = cur[j];
603	12	std::map<Node, Node>::iterator itf = d_fo_to_sk.find(ccur);
604	12	if (itf != d_fo_to_sk.end())
605		{
606	3	if (ck == NONLINEAR_MULT \|\| (isArithDivKind && j == 1))
607		{
608	3	exvar = itf->second;
609	3	return true;
610		}
611		}
612		}
613	3	return false;
614		}
615	6088	for (const Node& ccur : cur)
616		{
617	3677	visit.push_back(ccur);
618		}
619		}
620	3696	} while (!visit.empty());
621
622	82	return true;
623		}
624
625		} // namespace quantifiers
626		} // namespace theory
627	28446	} // namespace cvc5