Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_repair_const.cpp	Lines:	300	332	90.4 %
Date:	2021-09-17	Branches:	588	1426	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 "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(Env& env, TermDbSygus* tds)
    : EnvObj(env), 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.
  const LogicInfo& logic = logicInfo();
  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,
      d_env.getOptions(),
      d_env.getLogicInfo(),
      Options::current().quantifiers.sygusRepairConstTimeoutWasSetByUser,
      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->rewriteNode(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,
                                  const 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(const 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 "theory/datatypes/theory_datatypes_utils.h"
25		#include "theory/logic_info.h"
26		#include "theory/quantifiers/cegqi/ceg_instantiator.h"
27		#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
28		#include "theory/quantifiers/sygus/term_database_sygus.h"
29		#include "theory/smt_engine_subsolver.h"
30
31		using namespace cvc5::kind;
32
33		namespace cvc5 {
34		namespace theory {
35		namespace quantifiers {
36
37	1233	SygusRepairConst::SygusRepairConst(Env& env, TermDbSygus* tds)
38	1233	: EnvObj(env), d_tds(tds), d_allow_constant_grammar(false)
39		{
40	1233	}
41
42	8	void SygusRepairConst::initialize(Node base_inst,
43		const std::vector<Node>& candidates)
44		{
45	8	Trace("sygus-repair-const") << "SygusRepairConst::initialize" << std::endl;
46	8	Trace("sygus-repair-const") << " conjecture : " << base_inst << std::endl;
47	8	d_base_inst = base_inst;
48
49		// compute whether there are "allow all constant" types in the variables of q
50	16	std::map<TypeNode, bool> tprocessed;
51	16	for (const Node& v : candidates)
52		{
53	16	TypeNode tn = v.getType();
54		// do the type traversal of the sygus type
55	8	registerSygusType(tn, tprocessed);
56		}
57	16	Trace("sygus-repair-const")
58	8	<< " allow constants : " << d_allow_constant_grammar << std::endl;
59	8	}
60
61		// recursion depth bounded by number of types in grammar (small)
62	105	void SygusRepairConst::registerSygusType(TypeNode tn,
63		std::map<TypeNode, bool>& tprocessed)
64		{
65	105	if (tprocessed.find(tn) == tprocessed.end())
66		{
67	30	tprocessed[tn] = true;
68	30	if (!tn.isDatatype())
69		{
70		// may have recursed to a non-datatype, e.g. in the case that we have
71		// "any constant" constructors
72	10	return;
73		}
74	20	const DType& dt = tn.getDType();
75	20	if (!dt.isSygus())
76		{
77		// may have recursed to a non-sygus-datatype
78		return;
79		}
80		// check if this datatype allows all constants
81	20	if (dt.getSygusAllowConst())
82		{
83	16	d_allow_constant_grammar = true;
84		}
85	107	for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
86		{
87	87	const DTypeConstructor& dtc = dt[i];
88		// recurse on all subfields
89	184	for (unsigned j = 0, nargs = dtc.getNumArgs(); j < nargs; j++)
90		{
91	194	TypeNode tnc = d_tds->getArgType(dtc, j);
92	97	registerSygusType(tnc, tprocessed);
93		}
94		}
95		}
96		}
97
98	171	bool SygusRepairConst::isActive() const
99		{
100	171	return !d_base_inst.isNull() && d_allow_constant_grammar;
101		}
102
103	88	bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
104		const std::vector<Node>& candidate_values,
105		std::vector<Node>& repair_cv,
106		bool useConstantsAsHoles)
107		{
108	176	return repairSolution(d_base_inst,
109		candidates,
110		candidate_values,
111		repair_cv,
112	176	useConstantsAsHoles);
113		}
114
115	171	bool SygusRepairConst::repairSolution(Node sygusBody,
116		const std::vector<Node>& candidates,
117		const std::vector<Node>& candidate_values,
118		std::vector<Node>& repair_cv,
119		bool useConstantsAsHoles)
120		{
121	171	Assert(candidates.size() == candidate_values.size());
122
123		// if no grammar type allows constants, no repair is possible
124	171	if (!isActive())
125		{
126		return false;
127		}
128	171	if (Trace.isOn("sygus-repair-const"))
129		{
130		Trace("sygus-repair-const") << "Repair candidate solutions..." << std::endl;
131		for (unsigned i = 0, size = candidates.size(); i < size; i++)
132		{
133		std::stringstream ss;
134		TermDbSygus::toStreamSygus(ss, candidate_values[i]);
135		Trace("sygus-repair-const")
136		<< " " << candidates[i] << " -> " << ss.str() << std::endl;
137		}
138		Trace("sygus-repair-const")
139		<< "Getting candidate skeletons : " << std::endl;
140		}
141	342	std::vector<Node> candidate_skeletons;
142	342	std::map<TypeNode, int> free_var_count;
143	342	std::vector<Node> sk_vars;
144	342	std::map<Node, Node> sk_vars_to_subs;
145	342	for (unsigned i = 0, size = candidates.size(); i < size; i++)
146		{
147	342	Node cv = candidate_values[i];
148		Node skeleton = getSkeleton(
149	342	cv, free_var_count, sk_vars, sk_vars_to_subs, useConstantsAsHoles);
150	171	if (Trace.isOn("sygus-repair-const"))
151		{
152		std::stringstream ss;
153		TermDbSygus::toStreamSygus(ss, cv);
154		Trace("sygus-repair-const")
155		<< "Solution #" << i << " : " << ss.str() << std::endl;
156		if (skeleton == cv)
157		{
158		Trace("sygus-repair-const") << "...solution unchanged" << std::endl;
159		}
160		else
161		{
162		std::stringstream sss;
163		TermDbSygus::toStreamSygus(sss, skeleton);
164		Trace("sygus-repair-const")
165		<< "...inferred skeleton : " << sss.str() << std::endl;
166		}
167		}
168	171	candidate_skeletons.push_back(skeleton);
169		}
170
171	171	if (sk_vars.empty())
172		{
173		Trace("sygus-repair-const") << "...no solutions repaired." << std::endl;
174		return false;
175		}
176
177	171	Trace("sygus-repair-const") << "Get first-order query..." << std::endl;
178		Node fo_body =
179	342	getFoQuery(sygusBody, candidates, candidate_skeletons, sk_vars);
180
181	171	Trace("sygus-repair-const-debug") << "...got : " << fo_body << std::endl;
182
183	171	if (d_queries.find(fo_body) != d_queries.end())
184		{
185	18	Trace("sygus-repair-const") << "...duplicate query." << std::endl;
186	18	return false;
187		}
188	153	d_queries.insert(fo_body);
189
190		// check whether it is not in the current logic, e.g. non-linear arithmetic.
191		// if so, undo replacements until it is in the current logic.
192	153	const LogicInfo& logic = logicInfo();
193	153	if (logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear())
194		{
195	111	fo_body = fitToLogic(sygusBody,
196		logic,
197		fo_body,
198		candidates,
199		candidate_skeletons,
200		sk_vars,
201		sk_vars_to_subs);
202	222	Trace("sygus-repair-const-debug")
203	111	<< "...after fit-to-logic : " << fo_body << std::endl;
204		}
205	153	Assert(!expr::hasFreeVar(fo_body));
206
207	153	if (fo_body.isNull() \|\| sk_vars.empty())
208		{
209	6	Trace("sygus-repair-const")
210	3	<< "...all skeleton variables lead to bad logic." << std::endl;
211	3	return false;
212		}
213
214	150	Trace("sygus-repair-const") << "Make satisfiabily query..." << std::endl;
215	150	if (fo_body.getKind() == FORALL)
216		{
217		// must be a CBQI quantifier
218	71	CegHandledStatus hstatus = CegInstantiator::isCbqiQuant(fo_body);
219	71	if (hstatus < CEG_HANDLED)
220		{
221		// abort if less than fully handled
222		Trace("sygus-repair-const") << "...first-order query is not handlable by "
223		"counterexample-guided instantiation."
224		<< std::endl;
225		return false;
226		}
227		}
228
229	150	Trace("sygus-engine") << "Repairing previous solution..." << std::endl;
230		// make the satisfiability query
231	300	std::unique_ptr<SmtEngine> repcChecker;
232		// initialize the subsolver using the standard method
233	600	initializeSubsolver(
234		repcChecker,
235	150	d_env.getOptions(),
236	150	d_env.getLogicInfo(),
237	150	Options::current().quantifiers.sygusRepairConstTimeoutWasSetByUser,
238		options::sygusRepairConstTimeout());
239		// renable options disabled by sygus
240	150	repcChecker->setOption("miniscope-quant", "true");
241	150	repcChecker->setOption("miniscope-quant-fv", "true");
242	150	repcChecker->setOption("quant-split", "true");
243	150	repcChecker->assertFormula(fo_body);
244		// check satisfiability
245	300	Result r = repcChecker->checkSat();
246	150	Trace("sygus-repair-const") << "...got : " << r << std::endl;
247	450	if (r.asSatisfiabilityResult().isSat() == Result::UNSAT
248	450	\|\| r.asSatisfiabilityResult().isUnknown())
249		{
250	136	Trace("sygus-engine") << "...failed" << std::endl;
251	136	return false;
252		}
253	28	std::vector<Node> sk_sygus_m;
254	34	for (const Node& v : sk_vars)
255		{
256	20	Assert(d_sk_to_fo.find(v) != d_sk_to_fo.end());
257	40	Node fov = d_sk_to_fo[v];
258	40	Node fov_m = repcChecker->getValue(fov);
259	20	Trace("sygus-repair-const") << " " << fov << " = " << fov_m << std::endl;
260		// convert to sygus
261	40	Node fov_m_to_sygus = d_tds->getProxyVariable(v.getType(), fov_m);
262	20	sk_sygus_m.push_back(fov_m_to_sygus);
263		}
264	28	std::stringstream ss;
265		// convert back to sygus
266	28	for (unsigned i = 0, size = candidates.size(); i < size; i++)
267		{
268	28	Node csk = candidate_skeletons[i];
269		Node scsk = csk.substitute(
270	28	sk_vars.begin(), sk_vars.end(), sk_sygus_m.begin(), sk_sygus_m.end());
271	14	repair_cv.push_back(scsk);
272	14	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	14	Trace("sygus-engine") << "...success:" << std::endl;
280	14	Trace("sygus-engine") << ss.str();
281	28	Trace("sygus-repair-const")
282	14	<< "Repaired constants in solution : " << std::endl;
283	14	Trace("sygus-repair-const") << ss.str();
284	14	return true;
285		}
286
287	138	bool SygusRepairConst::mustRepair(Node n)
288		{
289	276	std::unordered_set<TNode> visited;
290	276	std::vector<TNode> visit;
291	276	TNode cur;
292	138	visit.push_back(n);
293	282	do
294		{
295	420	cur = visit.back();
296	420	visit.pop_back();
297	420	if (visited.find(cur) == visited.end())
298		{
299	388	visited.insert(cur);
300	388	Assert(cur.getKind() == APPLY_CONSTRUCTOR);
301	388	if (isRepairable(cur, false))
302		{
303	88	return true;
304		}
305	713	for (const Node& cn : cur)
306		{
307	413	visit.push_back(cn);
308		}
309		}
310	332	} while (!visit.empty());
311
312	50	return false;
313		}
314
315	1398	bool SygusRepairConst::isRepairable(Node n, bool useConstantsAsHoles)
316		{
317	1398	if (n.getKind() != APPLY_CONSTRUCTOR)
318		{
319	202	return false;
320		}
321	2392	TypeNode tn = n.getType();
322	1196	Assert(tn.isDatatype());
323	1196	const DType& dt = tn.getDType();
324	1196	if (!dt.isSygus())
325		{
326		return false;
327		}
328	2392	Node op = n.getOperator();
329	1196	unsigned cindex = datatypes::utils::indexOf(op);
330	2392	Node sygusOp = dt[cindex].getSygusOp();
331	1196	if (sygusOp.getAttribute(SygusAnyConstAttribute()))
332		{
333		// if it represents "any constant" then it is repairable
334	323	return true;
335		}
336	873	if (dt[cindex].getNumArgs() > 0)
337		{
338	427	return false;
339		}
340	446	if (useConstantsAsHoles && dt.getSygusAllowConst())
341		{
342		if (sygusOp.isConst())
343		{
344		// if a constant, it is repairable
345		return true;
346		}
347		}
348	446	return false;
349		}
350
351	171	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	171	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	169	NodeManager* nm = NodeManager::currentNM();
367		// get the most general candidate skeleton of n
368	338	std::unordered_map<TNode, Node> visited;
369	169	std::unordered_map<TNode, Node>::iterator it;
370	338	std::vector<TNode> visit;
371	338	TNode cur;
372	169	visit.push_back(n);
373	1764	do
374		{
375	1933	cur = visit.back();
376	1933	visit.pop_back();
377	1933	it = visited.find(cur);
378
379	1933	if (it == visited.end())
380		{
381	925	visited[cur] = Node::null();
382	925	visit.push_back(cur);
383	1764	for (const Node& cn : cur)
384		{
385	839	visit.push_back(cn);
386		}
387		}
388	1008	else if (it->second.isNull())
389		{
390	1850	Node ret = cur;
391	925	bool childChanged = false;
392	1850	std::vector<Node> children;
393	925	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
394		{
395	723	children.push_back(cur.getOperator());
396		}
397	1764	for (const Node& cn : cur)
398		{
399	1678	Node child;
400		// if it is repairable
401	839	if (isRepairable(cn, useConstantsAsHoles))
402		{
403		// replace it by the next free variable
404	233	child = d_tds->getFreeVarInc(cn.getType(), free_var_count);
405	233	sk_vars.push_back(child);
406	233	sk_vars_to_subs[child] = cn;
407	466	Trace("sygus-repair-const-debug")
408	233	<< "Var to subs : " << child << " -> " << cn << std::endl;
409		}
410		else
411		{
412	606	it = visited.find(cn);
413	606	Assert(it != visited.end());
414	606	Assert(!it->second.isNull());
415	606	child = it->second;
416		}
417	839	childChanged = childChanged \|\| cn != child;
418	839	children.push_back(child);
419		}
420	925	if (childChanged)
421		{
422	230	ret = nm->mkNode(cur.getKind(), children);
423		}
424	925	visited[cur] = ret;
425		}
426	1933	} while (!visit.empty());
427	169	Assert(visited.find(n) != visited.end());
428	169	Assert(!visited.find(n)->second.isNull());
429	169	return visited[n];
430		}
431
432	174	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	174	NodeManager* nm = NodeManager::currentNM();
438	174	SkolemManager* sm = nm->getSkolemManager();
439	174	Trace("sygus-repair-const") << " Substitute skeletons..." << std::endl;
440	174	body = body.substitute(candidates.begin(),
441		candidates.end(),
442		candidate_skeletons.begin(),
443		candidate_skeletons.end());
444	174	Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl;
445
446	174	Trace("sygus-repair-const") << " Unfold the specification..." << std::endl;
447	174	body = d_tds->rewriteNode(body);
448	174	Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl;
449
450	174	Trace("sygus-repair-const") << " Introduce first-order vars..." << std::endl;
451	413	for (const Node& v : sk_vars)
452		{
453	239	std::map<Node, Node>::iterator itf = d_sk_to_fo.find(v);
454	239	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	348	std::unordered_map<TNode, Node> visited;
468	174	std::unordered_map<TNode, Node>::iterator it;
469	348	std::vector<TNode> visit;
470	348	TNode cur;
471	174	visit.push_back(body);
472	13809	do
473		{
474	13983	cur = visit.back();
475	13983	visit.pop_back();
476	13983	it = visited.find(cur);
477
478	13983	if (it == visited.end())
479		{
480	6274	visited[cur] = Node::null();
481	6274	if (cur.getKind() == DT_SYGUS_EVAL)
482		{
483	2100	Node v = cur[0];
484	1050	if (std::find(sk_vars.begin(), sk_vars.end(), v) != sk_vars.end())
485		{
486	1050	std::map<Node, Node>::iterator itf = d_sk_to_fo.find(v);
487	1050	Assert(itf != d_sk_to_fo.end());
488	1050	visited[cur] = itf->second;
489		}
490		}
491	6274	if (visited[cur].isNull())
492		{
493	5224	visit.push_back(cur);
494	13809	for (const Node& cn : cur)
495		{
496	8585	visit.push_back(cn);
497		}
498		}
499		}
500	7709	else if (it->second.isNull())
501		{
502	10448	Node ret = cur;
503	5224	bool childChanged = false;
504	10448	std::vector<Node> children;
505	5224	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
506		{
507	160	children.push_back(cur.getOperator());
508		}
509	13809	for (const Node& cn : cur)
510		{
511	8585	it = visited.find(cn);
512	8585	Assert(it != visited.end());
513	8585	Assert(!it->second.isNull());
514	8585	childChanged = childChanged \|\| cn != it->second;
515	8585	children.push_back(it->second);
516		}
517	5224	if (childChanged)
518		{
519	2183	ret = nm->mkNode(cur.getKind(), children);
520		}
521	5224	visited[cur] = ret;
522		}
523	13983	} while (!visit.empty());
524	174	Assert(visited.find(body) != visited.end());
525	174	Assert(!visited.find(body)->second.isNull());
526	174	Node fo_body = visited[body];
527	174	Trace("sygus-repair-const-debug") << " ...got : " << fo_body << std::endl;
528	348	return fo_body;
529		}
530
531	111	Node SygusRepairConst::fitToLogic(Node body,
532		const 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	222	std::vector<Node> rm_var;
540	222	Node exc_var;
541	117	while (getFitToLogicExcludeVar(logic, n, exc_var))
542		{
543	111	if (exc_var.isNull())
544		{
545	108	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	114	bool SygusRepairConst::getFitToLogicExcludeVar(const LogicInfo& logic,
572		Node n,
573		Node& exvar)
574		{
575	114	bool restrictLA = logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear();
576
577		// should have at least one restriction
578	114	Assert(restrictLA);
579
580	228	std::unordered_set<TNode> visited;
581	114	std::unordered_set<TNode>::iterator it;
582	228	std::vector<TNode> visit;
583	228	TNode cur;
584	114	visit.push_back(n);
585	5256	do
586		{
587	5370	cur = visit.back();
588	5370	visit.pop_back();
589	5370	it = visited.find(cur);
590
591	5370	if (it == visited.end())
592		{
593	3443	visited.insert(cur);
594	3443	Kind ck = cur.getKind();
595	6886	bool isArithDivKind = (ck == DIVISION_TOTAL \|\| ck == INTS_DIVISION_TOTAL
596	6886	\|\| ck == INTS_MODULUS_TOTAL);
597	3443	Assert(ck != DIVISION && ck != INTS_DIVISION && ck != INTS_MODULUS);
598	3443	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	8756	for (const Node& ccur : cur)
616		{
617	5319	visit.push_back(ccur);
618		}
619		}
620	5364	} while (!visit.empty());
621
622	108	return true;
623		}
624
625		} // namespace quantifiers
626		} // namespace theory
627	29577	} // namespace cvc5