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-11-07	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<SolverEngine> 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	1900	SygusRepairConst::SygusRepairConst(Env& env, TermDbSygus* tds)
38	1900	: EnvObj(env), d_tds(tds), d_allow_constant_grammar(false)
39		{
40	1900	}
41
42	13	void SygusRepairConst::initialize(Node base_inst,
43		const std::vector<Node>& candidates)
44		{
45	13	Trace("sygus-repair-const") << "SygusRepairConst::initialize" << std::endl;
46	13	Trace("sygus-repair-const") << " conjecture : " << base_inst << std::endl;
47	13	d_base_inst = base_inst;
48
49		// compute whether there are "allow all constant" types in the variables of q
50	26	std::map<TypeNode, bool> tprocessed;
51	26	for (const Node& v : candidates)
52		{
53	26	TypeNode tn = v.getType();
54		// do the type traversal of the sygus type
55	13	registerSygusType(tn, tprocessed);
56		}
57	26	Trace("sygus-repair-const")
58	13	<< " allow constants : " << d_allow_constant_grammar << std::endl;
59	13	}
60
61		// recursion depth bounded by number of types in grammar (small)
62	165	void SygusRepairConst::registerSygusType(TypeNode tn,
63		std::map<TypeNode, bool>& tprocessed)
64		{
65	165	if (tprocessed.find(tn) == tprocessed.end())
66		{
67	48	tprocessed[tn] = true;
68	48	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	16	return;
73		}
74	32	const DType& dt = tn.getDType();
75	32	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	32	if (dt.getSygusAllowConst())
82		{
83	25	d_allow_constant_grammar = true;
84		}
85	169	for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
86		{
87	137	const DTypeConstructor& dtc = dt[i];
88		// recurse on all subfields
89	289	for (unsigned j = 0, nargs = dtc.getNumArgs(); j < nargs; j++)
90		{
91	304	TypeNode tnc = d_tds->getArgType(dtc, j);
92	152	registerSygusType(tnc, tprocessed);
93		}
94		}
95		}
96		}
97
98	293	bool SygusRepairConst::isActive() const
99		{
100	293	return !d_base_inst.isNull() && d_allow_constant_grammar;
101		}
102
103	151	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	302	return repairSolution(d_base_inst,
109		candidates,
110		candidate_values,
111		repair_cv,
112	302	useConstantsAsHoles);
113		}
114
115	293	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	293	Assert(candidates.size() == candidate_values.size());
122
123		// if no grammar type allows constants, no repair is possible
124	293	if (!isActive())
125		{
126		return false;
127		}
128	293	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	586	std::vector<Node> candidate_skeletons;
142	586	std::map<TypeNode, int> free_var_count;
143	586	std::vector<Node> sk_vars;
144	586	std::map<Node, Node> sk_vars_to_subs;
145	586	for (unsigned i = 0, size = candidates.size(); i < size; i++)
146		{
147	586	Node cv = candidate_values[i];
148		Node skeleton = getSkeleton(
149	586	cv, free_var_count, sk_vars, sk_vars_to_subs, useConstantsAsHoles);
150	293	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	293	candidate_skeletons.push_back(skeleton);
169		}
170
171	293	if (sk_vars.empty())
172		{
173		Trace("sygus-repair-const") << "...no solutions repaired." << std::endl;
174		return false;
175		}
176
177	293	Trace("sygus-repair-const") << "Get first-order query..." << std::endl;
178		Node fo_body =
179	586	getFoQuery(sygusBody, candidates, candidate_skeletons, sk_vars);
180
181	293	Trace("sygus-repair-const-debug") << "...got : " << fo_body << std::endl;
182
183	293	if (d_queries.find(fo_body) != d_queries.end())
184		{
185	28	Trace("sygus-repair-const") << "...duplicate query." << std::endl;
186	28	return false;
187		}
188	265	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	265	const LogicInfo& logic = logicInfo();
193	265	if (logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear())
194		{
195	202	fo_body = fitToLogic(sygusBody,
196		logic,
197		fo_body,
198		candidates,
199		candidate_skeletons,
200		sk_vars,
201		sk_vars_to_subs);
202	404	Trace("sygus-repair-const-debug")
203	202	<< "...after fit-to-logic : " << fo_body << std::endl;
204		}
205	265	Assert(!expr::hasFreeVar(fo_body));
206
207	265	if (fo_body.isNull() \|\| sk_vars.empty())
208		{
209	12	Trace("sygus-repair-const")
210	6	<< "...all skeleton variables lead to bad logic." << std::endl;
211	6	return false;
212		}
213
214	259	Trace("sygus-repair-const") << "Make satisfiabily query..." << std::endl;
215	259	if (fo_body.getKind() == FORALL)
216		{
217		// must be a CBQI quantifier
218	123	CegHandledStatus hstatus = CegInstantiator::isCbqiQuant(fo_body);
219	123	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	259	Trace("sygus-engine") << "Repairing previous solution..." << std::endl;
230		// make the satisfiability query
231	518	std::unique_ptr<SolverEngine> repcChecker;
232		// initialize the subsolver using the standard method
233	1036	initializeSubsolver(
234		repcChecker,
235	259	d_env.getOptions(),
236	259	d_env.getLogicInfo(),
237	259	Options::current().quantifiers.sygusRepairConstTimeoutWasSetByUser,
238		options::sygusRepairConstTimeout());
239		// renable options disabled by sygus
240	259	repcChecker->setOption("miniscope-quant", "true");
241	259	repcChecker->setOption("miniscope-quant-fv", "true");
242	259	repcChecker->setOption("quant-split", "true");
243	259	repcChecker->assertFormula(fo_body);
244		// check satisfiability
245	518	Result r = repcChecker->checkSat();
246	259	Trace("sygus-repair-const") << "...got : " << r << std::endl;
247	777	if (r.asSatisfiabilityResult().isSat() == Result::UNSAT
248	777	\|\| r.asSatisfiabilityResult().isUnknown())
249		{
250	226	Trace("sygus-engine") << "...failed" << std::endl;
251	226	return false;
252		}
253	66	std::vector<Node> sk_sygus_m;
254	79	for (const Node& v : sk_vars)
255		{
256	46	Assert(d_sk_to_fo.find(v) != d_sk_to_fo.end());
257	92	Node fov = d_sk_to_fo[v];
258	92	Node fov_m = repcChecker->getValue(fov);
259	46	Trace("sygus-repair-const") << " " << fov << " = " << fov_m << std::endl;
260		// convert to sygus
261	92	Node fov_m_to_sygus = d_tds->getProxyVariable(v.getType(), fov_m);
262	46	sk_sygus_m.push_back(fov_m_to_sygus);
263		}
264	66	std::stringstream ss;
265		// convert back to sygus
266	66	for (unsigned i = 0, size = candidates.size(); i < size; i++)
267		{
268	66	Node csk = candidate_skeletons[i];
269		Node scsk = csk.substitute(
270	66	sk_vars.begin(), sk_vars.end(), sk_sygus_m.begin(), sk_sygus_m.end());
271	33	repair_cv.push_back(scsk);
272	33	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	33	Trace("sygus-engine") << "...success:" << std::endl;
280	33	Trace("sygus-engine") << ss.str();
281	66	Trace("sygus-repair-const")
282	33	<< "Repaired constants in solution : " << std::endl;
283	33	Trace("sygus-repair-const") << ss.str();
284	33	return true;
285		}
286
287	241	bool SygusRepairConst::mustRepair(Node n)
288		{
289	482	std::unordered_set<TNode> visited;
290	482	std::vector<TNode> visit;
291	482	TNode cur;
292	241	visit.push_back(n);
293	453	do
294		{
295	694	cur = visit.back();
296	694	visit.pop_back();
297	694	if (visited.find(cur) == visited.end())
298		{
299	640	visited.insert(cur);
300	640	Assert(cur.getKind() == APPLY_CONSTRUCTOR);
301	640	if (isRepairable(cur, false))
302		{
303	151	return true;
304		}
305	1142	for (const Node& cn : cur)
306		{
307	653	visit.push_back(cn);
308		}
309		}
310	543	} while (!visit.empty());
311
312	90	return false;
313		}
314
315	2323	bool SygusRepairConst::isRepairable(Node n, bool useConstantsAsHoles)
316		{
317	2323	if (n.getKind() != APPLY_CONSTRUCTOR)
318		{
319	341	return false;
320		}
321	3964	TypeNode tn = n.getType();
322	1982	Assert(tn.isDatatype());
323	1982	const DType& dt = tn.getDType();
324	1982	if (!dt.isSygus())
325		{
326		return false;
327		}
328	3964	Node op = n.getOperator();
329	1982	unsigned cindex = datatypes::utils::indexOf(op);
330	3964	Node sygusOp = dt[cindex].getSygusOp();
331	1982	if (sygusOp.getAttribute(SygusAnyConstAttribute()))
332		{
333		// if it represents "any constant" then it is repairable
334	541	return true;
335		}
336	1441	if (dt[cindex].getNumArgs() > 0)
337		{
338	706	return false;
339		}
340	735	if (useConstantsAsHoles && dt.getSygusAllowConst())
341		{
342		if (sygusOp.isConst())
343		{
344		// if a constant, it is repairable
345		return true;
346		}
347		}
348	735	return false;
349		}
350
351	293	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	293	if (isRepairable(n, useConstantsAsHoles))
358		{
359	8	Node sk_var = d_tds->getFreeVarInc(n.getType(), free_var_count);
360	4	sk_vars.push_back(sk_var);
361	4	sk_vars_to_subs[sk_var] = n;
362	8	Trace("sygus-repair-const-debug")
363	4	<< "Var to subs : " << sk_var << " -> " << n << std::endl;
364	4	return sk_var;
365		}
366	289	NodeManager* nm = NodeManager::currentNM();
367		// get the most general candidate skeleton of n
368	578	std::unordered_map<TNode, Node> visited;
369	289	std::unordered_map<TNode, Node>::iterator it;
370	578	std::vector<TNode> visit;
371	578	TNode cur;
372	289	visit.push_back(n);
373	2931	do
374		{
375	3220	cur = visit.back();
376	3220	visit.pop_back();
377	3220	it = visited.find(cur);
378
379	3220	if (it == visited.end())
380		{
381	1541	visited[cur] = Node::null();
382	1541	visit.push_back(cur);
383	2931	for (const Node& cn : cur)
384		{
385	1390	visit.push_back(cn);
386		}
387		}
388	1679	else if (it->second.isNull())
389		{
390	3082	Node ret = cur;
391	1541	bool childChanged = false;
392	3082	std::vector<Node> children;
393	1541	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
394		{
395	1200	children.push_back(cur.getOperator());
396		}
397	2931	for (const Node& cn : cur)
398		{
399	2780	Node child;
400		// if it is repairable
401	1390	if (isRepairable(cn, useConstantsAsHoles))
402		{
403		// replace it by the next free variable
404	386	child = d_tds->getFreeVarInc(cn.getType(), free_var_count);
405	386	sk_vars.push_back(child);
406	386	sk_vars_to_subs[child] = cn;
407	772	Trace("sygus-repair-const-debug")
408	386	<< "Var to subs : " << child << " -> " << cn << std::endl;
409		}
410		else
411		{
412	1004	it = visited.find(cn);
413	1004	Assert(it != visited.end());
414	1004	Assert(!it->second.isNull());
415	1004	child = it->second;
416		}
417	1390	childChanged = childChanged \|\| cn != child;
418	1390	children.push_back(child);
419		}
420	1541	if (childChanged)
421		{
422	367	ret = nm->mkNode(cur.getKind(), children);
423		}
424	1541	visited[cur] = ret;
425		}
426	3220	} while (!visit.empty());
427	289	Assert(visited.find(n) != visited.end());
428	289	Assert(!visited.find(n)->second.isNull());
429	289	return visited[n];
430		}
431
432	299	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	299	NodeManager* nm = NodeManager::currentNM();
438	299	SkolemManager* sm = nm->getSkolemManager();
439	299	Trace("sygus-repair-const") << " Substitute skeletons..." << std::endl;
440	299	body = body.substitute(candidates.begin(),
441		candidates.end(),
442		candidate_skeletons.begin(),
443		candidate_skeletons.end());
444	299	Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl;
445
446	299	Trace("sygus-repair-const") << " Unfold the specification..." << std::endl;
447	299	body = d_tds->rewriteNode(body);
448	299	Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl;
449
450	299	Trace("sygus-repair-const") << " Introduce first-order vars..." << std::endl;
451	697	for (const Node& v : sk_vars)
452		{
453	398	std::map<Node, Node>::iterator itf = d_sk_to_fo.find(v);
454	398	if (itf == d_sk_to_fo.end())
455		{
456	58	TypeNode builtinType = d_tds->sygusToBuiltinType(v.getType());
457	58	Node sk_fov = sm->mkDummySkolem("k", builtinType);
458	29	d_sk_to_fo[v] = sk_fov;
459	29	d_fo_to_sk[sk_fov] = v;
460	58	Trace("sygus-repair-const-debug")
461	29	<< "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	598	std::unordered_map<TNode, Node> visited;
468	299	std::unordered_map<TNode, Node>::iterator it;
469	598	std::vector<TNode> visit;
470	598	TNode cur;
471	299	visit.push_back(body);
472	23399	do
473		{
474	23698	cur = visit.back();
475	23698	visit.pop_back();
476	23698	it = visited.find(cur);
477
478	23698	if (it == visited.end())
479		{
480	10624	visited[cur] = Node::null();
481	10624	if (cur.getKind() == DT_SYGUS_EVAL)
482		{
483	3304	Node v = cur[0];
484	1652	if (std::find(sk_vars.begin(), sk_vars.end(), v) != sk_vars.end())
485		{
486	1652	std::map<Node, Node>::iterator itf = d_sk_to_fo.find(v);
487	1652	Assert(itf != d_sk_to_fo.end());
488	1652	visited[cur] = itf->second;
489		}
490		}
491	10624	if (visited[cur].isNull())
492		{
493	8972	visit.push_back(cur);
494	23399	for (const Node& cn : cur)
495		{
496	14427	visit.push_back(cn);
497		}
498		}
499		}
500	13074	else if (it->second.isNull())
501		{
502	17944	Node ret = cur;
503	8972	bool childChanged = false;
504	17944	std::vector<Node> children;
505	8972	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
506		{
507	240	children.push_back(cur.getOperator());
508		}
509	23399	for (const Node& cn : cur)
510		{
511	14427	it = visited.find(cn);
512	14427	Assert(it != visited.end());
513	14427	Assert(!it->second.isNull());
514	14427	childChanged = childChanged \|\| cn != it->second;
515	14427	children.push_back(it->second);
516		}
517	8972	if (childChanged)
518		{
519	3780	ret = nm->mkNode(cur.getKind(), children);
520		}
521	8972	visited[cur] = ret;
522		}
523	23698	} while (!visit.empty());
524	299	Assert(visited.find(body) != visited.end());
525	299	Assert(!visited.find(body)->second.isNull());
526	299	Node fo_body = visited[body];
527	299	Trace("sygus-repair-const-debug") << " ...got : " << fo_body << std::endl;
528	598	return fo_body;
529		}
530
531	202	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	404	std::vector<Node> rm_var;
540	404	Node exc_var;
541	214	while (getFitToLogicExcludeVar(logic, n, exc_var))
542		{
543	202	if (exc_var.isNull())
544		{
545	196	return n;
546		}
547	12	Trace("sygus-repair-const") << "...exclude " << exc_var
548	6	<< " due to logic restrictions." << std::endl;
549	12	TNode tvar = exc_var;
550	6	Assert(sk_vars_to_subs.find(exc_var) != sk_vars_to_subs.end());
551	12	TNode tsubs = sk_vars_to_subs[exc_var];
552		// revert the substitution
553	12	for (unsigned i = 0, size = candidate_skeletons.size(); i < size; i++)
554		{
555	6	candidate_skeletons[i] = candidate_skeletons[i].substitute(tvar, tsubs);
556		}
557		// remove the variable
558	6	sk_vars_to_subs.erase(exc_var);
559		std::vector<Node>::iterator it =
560	6	std::find(sk_vars.begin(), sk_vars.end(), exc_var);
561	6	Assert(it != sk_vars.end());
562	6	sk_vars.erase(it);
563		// reconstruct the query
564	6	n = getFoQuery(body, candidates, candidate_skeletons, sk_vars);
565		// reset the exclusion variable
566	6	exc_var = Node::null();
567		}
568	6	return Node::null();
569		}
570
571	208	bool SygusRepairConst::getFitToLogicExcludeVar(const LogicInfo& logic,
572		Node n,
573		Node& exvar)
574		{
575	208	bool restrictLA = logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear();
576
577		// should have at least one restriction
578	208	Assert(restrictLA);
579
580	416	std::unordered_set<TNode> visited;
581	208	std::unordered_set<TNode>::iterator it;
582	416	std::vector<TNode> visit;
583	416	TNode cur;
584	208	visit.push_back(n);
585	9344	do
586		{
587	9552	cur = visit.back();
588	9552	visit.pop_back();
589	9552	it = visited.find(cur);
590
591	9552	if (it == visited.end())
592		{
593	6186	visited.insert(cur);
594	6186	Kind ck = cur.getKind();
595	12372	bool isArithDivKind = (ck == DIVISION_TOTAL \|\| ck == INTS_DIVISION_TOTAL
596	12372	\|\| ck == INTS_MODULUS_TOTAL);
597	6186	Assert(ck != DIVISION && ck != INTS_DIVISION && ck != INTS_MODULUS);
598	6186	if (restrictLA && (ck == NONLINEAR_MULT \|\| isArithDivKind))
599		{
600	30	for (unsigned j = 0, size = cur.getNumChildren(); j < size; j++)
601		{
602	42	Node ccur = cur[j];
603	24	std::map<Node, Node>::iterator itf = d_fo_to_sk.find(ccur);
604	24	if (itf != d_fo_to_sk.end())
605		{
606	6	if (ck == NONLINEAR_MULT \|\| (isArithDivKind && j == 1))
607		{
608	6	exvar = itf->second;
609	6	return true;
610		}
611		}
612		}
613	6	return false;
614		}
615	15644	for (const Node& ccur : cur)
616		{
617	9470	visit.push_back(ccur);
618		}
619		}
620	9540	} while (!visit.empty());
621
622	196	return true;
623		}
624
625		} // namespace quantifiers
626		} // namespace theory
627	31137	} // namespace cvc5