Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_repair_const.cpp	Lines:	298	330	90.3 %
Date:	2021-08-14	Branches:	587	1424	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,
      nullptr,
      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->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	1151	SygusRepairConst::SygusRepairConst(TermDbSygus* tds)
41	1151	: d_tds(tds), d_allow_constant_grammar(false)
42		{
43	1151	}
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	135	bool SygusRepairConst::isActive() const
102		{
103	135	return !d_base_inst.isNull() && d_allow_constant_grammar;
104		}
105
106	70	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	140	return repairSolution(d_base_inst,
112		candidates,
113		candidate_values,
114		repair_cv,
115	140	useConstantsAsHoles);
116		}
117
118	135	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	135	Assert(candidates.size() == candidate_values.size());
125
126		// if no grammar type allows constants, no repair is possible
127	135	if (!isActive())
128		{
129		return false;
130		}
131	135	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	270	std::vector<Node> candidate_skeletons;
145	270	std::map<TypeNode, int> free_var_count;
146	270	std::vector<Node> sk_vars;
147	270	std::map<Node, Node> sk_vars_to_subs;
148	270	for (unsigned i = 0, size = candidates.size(); i < size; i++)
149		{
150	270	Node cv = candidate_values[i];
151		Node skeleton = getSkeleton(
152	270	cv, free_var_count, sk_vars, sk_vars_to_subs, useConstantsAsHoles);
153	135	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	135	candidate_skeletons.push_back(skeleton);
172		}
173
174	135	if (sk_vars.empty())
175		{
176		Trace("sygus-repair-const") << "...no solutions repaired." << std::endl;
177		return false;
178		}
179
180	135	Trace("sygus-repair-const") << "Get first-order query..." << std::endl;
181		Node fo_body =
182	270	getFoQuery(sygusBody, candidates, candidate_skeletons, sk_vars);
183
184	135	Trace("sygus-repair-const-debug") << "...got : " << fo_body << std::endl;
185
186	135	if (d_queries.find(fo_body) != d_queries.end())
187		{
188	18	Trace("sygus-repair-const") << "...duplicate query." << std::endl;
189	18	return false;
190		}
191	117	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	234	LogicInfo logic = smt::currentSmtEngine()->getLogicInfo();
196	117	if (logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear())
197		{
198	75	fo_body = fitToLogic(sygusBody,
199		logic,
200		fo_body,
201		candidates,
202		candidate_skeletons,
203		sk_vars,
204		sk_vars_to_subs);
205	150	Trace("sygus-repair-const-debug")
206	75	<< "...after fit-to-logic : " << fo_body << std::endl;
207		}
208	117	Assert(!expr::hasFreeVar(fo_body));
209
210	117	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	114	Trace("sygus-repair-const") << "Make satisfiabily query..." << std::endl;
218	114	if (fo_body.getKind() == FORALL)
219		{
220		// must be a CBQI quantifier
221	53	CegHandledStatus hstatus = CegInstantiator::isCbqiQuant(fo_body);
222	53	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	114	Trace("sygus-engine") << "Repairing previous solution..." << std::endl;
233		// make the satisfiability query
234	228	std::unique_ptr<SmtEngine> repcChecker;
235		// initialize the subsolver using the standard method
236	228	initializeSubsolver(
237		repcChecker,
238		nullptr,
239	114	Options::current().quantifiers.sygusRepairConstTimeoutWasSetByUser,
240		options::sygusRepairConstTimeout());
241		// renable options disabled by sygus
242	114	repcChecker->setOption("miniscope-quant", "true");
243	114	repcChecker->setOption("miniscope-quant-fv", "true");
244	114	repcChecker->setOption("quant-split", "true");
245	114	repcChecker->assertFormula(fo_body);
246		// check satisfiability
247	228	Result r = repcChecker->checkSat();
248	114	Trace("sygus-repair-const") << "...got : " << r << std::endl;
249	342	if (r.asSatisfiabilityResult().isSat() == Result::UNSAT
250	342	\|\| r.asSatisfiabilityResult().isUnknown())
251		{
252	100	Trace("sygus-engine") << "...failed" << std::endl;
253	100	return false;
254		}
255	28	std::vector<Node> sk_sygus_m;
256	35	for (const Node& v : sk_vars)
257		{
258	21	Assert(d_sk_to_fo.find(v) != d_sk_to_fo.end());
259	42	Node fov = d_sk_to_fo[v];
260	42	Node fov_m = repcChecker->getValue(fov);
261	21	Trace("sygus-repair-const") << " " << fov << " = " << fov_m << std::endl;
262		// convert to sygus
263	42	Node fov_m_to_sygus = d_tds->getProxyVariable(v.getType(), fov_m);
264	21	sk_sygus_m.push_back(fov_m_to_sygus);
265		}
266	28	std::stringstream ss;
267		// convert back to sygus
268	28	for (unsigned i = 0, size = candidates.size(); i < size; i++)
269		{
270	28	Node csk = candidate_skeletons[i];
271		Node scsk = csk.substitute(
272	28	sk_vars.begin(), sk_vars.end(), sk_sygus_m.begin(), sk_sygus_m.end());
273	14	repair_cv.push_back(scsk);
274	14	if (Trace.isOn("sygus-repair-const") \|\| Trace.isOn("sygus-engine"))
275		{
276		std::stringstream sss;
277		TermDbSygus::toStreamSygus(sss, repair_cv[i]);
278		ss << " * " << candidates[i] << " -> " << sss.str() << std::endl;
279		}
280		}
281	14	Trace("sygus-engine") << "...success:" << std::endl;
282	14	Trace("sygus-engine") << ss.str();
283	28	Trace("sygus-repair-const")
284	14	<< "Repaired constants in solution : " << std::endl;
285	14	Trace("sygus-repair-const") << ss.str();
286	14	return true;
287		}
288
289	110	bool SygusRepairConst::mustRepair(Node n)
290		{
291	220	std::unordered_set<TNode> visited;
292	220	std::vector<TNode> visit;
293	220	TNode cur;
294	110	visit.push_back(n);
295	195	do
296		{
297	305	cur = visit.back();
298	305	visit.pop_back();
299	305	if (visited.find(cur) == visited.end())
300		{
301	284	visited.insert(cur);
302	284	Assert(cur.getKind() == APPLY_CONSTRUCTOR);
303	284	if (isRepairable(cur, false))
304		{
305	70	return true;
306		}
307	521	for (const Node& cn : cur)
308		{
309	307	visit.push_back(cn);
310		}
311		}
312	235	} while (!visit.empty());
313
314	40	return false;
315		}
316
317	1070	bool SygusRepairConst::isRepairable(Node n, bool useConstantsAsHoles)
318		{
319	1070	if (n.getKind() != APPLY_CONSTRUCTOR)
320		{
321	158	return false;
322		}
323	1824	TypeNode tn = n.getType();
324	912	Assert(tn.isDatatype());
325	912	const DType& dt = tn.getDType();
326	912	if (!dt.isSygus())
327		{
328		return false;
329		}
330	1824	Node op = n.getOperator();
331	912	unsigned cindex = datatypes::utils::indexOf(op);
332	1824	Node sygusOp = dt[cindex].getSygusOp();
333	912	if (sygusOp.getAttribute(SygusAnyConstAttribute()))
334		{
335		// if it represents "any constant" then it is repairable
336	261	return true;
337		}
338	651	if (dt[cindex].getNumArgs() > 0)
339		{
340	302	return false;
341		}
342	349	if (useConstantsAsHoles && dt.getSygusAllowConst())
343		{
344		if (sygusOp.isConst())
345		{
346		// if a constant, it is repairable
347		return true;
348		}
349		}
350	349	return false;
351		}
352
353	135	Node SygusRepairConst::getSkeleton(Node n,
354		std::map<TypeNode, int>& free_var_count,
355		std::vector<Node>& sk_vars,
356		std::map<Node, Node>& sk_vars_to_subs,
357		bool useConstantsAsHoles)
358		{
359	135	if (isRepairable(n, useConstantsAsHoles))
360		{
361	4	Node sk_var = d_tds->getFreeVarInc(n.getType(), free_var_count);
362	2	sk_vars.push_back(sk_var);
363	2	sk_vars_to_subs[sk_var] = n;
364	4	Trace("sygus-repair-const-debug")
365	2	<< "Var to subs : " << sk_var << " -> " << n << std::endl;
366	2	return sk_var;
367		}
368	133	NodeManager* nm = NodeManager::currentNM();
369		// get the most general candidate skeleton of n
370	266	std::unordered_map<TNode, Node> visited;
371	133	std::unordered_map<TNode, Node>::iterator it;
372	266	std::vector<TNode> visit;
373	266	TNode cur;
374	133	visit.push_back(n);
375	1360	do
376		{
377	1493	cur = visit.back();
378	1493	visit.pop_back();
379	1493	it = visited.find(cur);
380
381	1493	if (it == visited.end())
382		{
383	709	visited[cur] = Node::null();
384	709	visit.push_back(cur);
385	1360	for (const Node& cn : cur)
386		{
387	651	visit.push_back(cn);
388		}
389		}
390	784	else if (it->second.isNull())
391		{
392	1418	Node ret = cur;
393	709	bool childChanged = false;
394	1418	std::vector<Node> children;
395	709	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
396		{
397	551	children.push_back(cur.getOperator());
398		}
399	1360	for (const Node& cn : cur)
400		{
401	1302	Node child;
402		// if it is repairable
403	651	if (isRepairable(cn, useConstantsAsHoles))
404		{
405		// replace it by the next free variable
406	189	child = d_tds->getFreeVarInc(cn.getType(), free_var_count);
407	189	sk_vars.push_back(child);
408	189	sk_vars_to_subs[child] = cn;
409	378	Trace("sygus-repair-const-debug")
410	189	<< "Var to subs : " << child << " -> " << cn << std::endl;
411		}
412		else
413		{
414	462	it = visited.find(cn);
415	462	Assert(it != visited.end());
416	462	Assert(!it->second.isNull());
417	462	child = it->second;
418		}
419	651	childChanged = childChanged \|\| cn != child;
420	651	children.push_back(child);
421		}
422	709	if (childChanged)
423		{
424	172	ret = nm->mkNode(cur.getKind(), children);
425		}
426	709	visited[cur] = ret;
427		}
428	1493	} while (!visit.empty());
429	133	Assert(visited.find(n) != visited.end());
430	133	Assert(!visited.find(n)->second.isNull());
431	133	return visited[n];
432		}
433
434	138	Node SygusRepairConst::getFoQuery(Node body,
435		const std::vector<Node>& candidates,
436		const std::vector<Node>& candidate_skeletons,
437		const std::vector<Node>& sk_vars)
438		{
439	138	NodeManager* nm = NodeManager::currentNM();
440	138	SkolemManager* sm = nm->getSkolemManager();
441	138	Trace("sygus-repair-const") << " Substitute skeletons..." << std::endl;
442	138	body = body.substitute(candidates.begin(),
443		candidates.end(),
444		candidate_skeletons.begin(),
445		candidate_skeletons.end());
446	138	Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl;
447
448	138	Trace("sygus-repair-const") << " Unfold the specification..." << std::endl;
449	138	body = d_tds->evaluateWithUnfolding(body);
450	138	Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl;
451
452	138	Trace("sygus-repair-const") << " Introduce first-order vars..." << std::endl;
453	333	for (const Node& v : sk_vars)
454		{
455	195	std::map<Node, Node>::iterator itf = d_sk_to_fo.find(v);
456	195	if (itf == d_sk_to_fo.end())
457		{
458	32	TypeNode builtinType = d_tds->sygusToBuiltinType(v.getType());
459	32	Node sk_fov = sm->mkDummySkolem("k", builtinType);
460	16	d_sk_to_fo[v] = sk_fov;
461	16	d_fo_to_sk[sk_fov] = v;
462	32	Trace("sygus-repair-const-debug")
463	16	<< "Map " << v << " -> " << sk_fov << std::endl;
464		}
465		}
466		// now, we must replace all terms of the form eval( z_i, t1...tn ) with
467		// a fresh first-order variable w_i, where z_i is a variable introduced in
468		// the skeleton inference step (z_i is a variable in sk_vars).
469	276	std::unordered_map<TNode, Node> visited;
470	138	std::unordered_map<TNode, Node>::iterator it;
471	276	std::vector<TNode> visit;
472	276	TNode cur;
473	138	visit.push_back(body);
474	10583	do
475		{
476	10721	cur = visit.back();
477	10721	visit.pop_back();
478	10721	it = visited.find(cur);
479
480	10721	if (it == visited.end())
481		{
482	4883	visited[cur] = Node::null();
483	4883	if (cur.getKind() == DT_SYGUS_EVAL)
484		{
485	1762	Node v = cur[0];
486	881	if (std::find(sk_vars.begin(), sk_vars.end(), v) != sk_vars.end())
487		{
488	881	std::map<Node, Node>::iterator itf = d_sk_to_fo.find(v);
489	881	Assert(itf != d_sk_to_fo.end());
490	881	visited[cur] = itf->second;
491		}
492		}
493	4883	if (visited[cur].isNull())
494		{
495	4002	visit.push_back(cur);
496	10583	for (const Node& cn : cur)
497		{
498	6581	visit.push_back(cn);
499		}
500		}
501		}
502	5838	else if (it->second.isNull())
503		{
504	8004	Node ret = cur;
505	4002	bool childChanged = false;
506	8004	std::vector<Node> children;
507	4002	if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
508		{
509	160	children.push_back(cur.getOperator());
510		}
511	10583	for (const Node& cn : cur)
512		{
513	6581	it = visited.find(cn);
514	6581	Assert(it != visited.end());
515	6581	Assert(!it->second.isNull());
516	6581	childChanged = childChanged \|\| cn != it->second;
517	6581	children.push_back(it->second);
518		}
519	4002	if (childChanged)
520		{
521	1794	ret = nm->mkNode(cur.getKind(), children);
522		}
523	4002	visited[cur] = ret;
524		}
525	10721	} while (!visit.empty());
526	138	Assert(visited.find(body) != visited.end());
527	138	Assert(!visited.find(body)->second.isNull());
528	138	Node fo_body = visited[body];
529	138	Trace("sygus-repair-const-debug") << " ...got : " << fo_body << std::endl;
530	276	return fo_body;
531		}
532
533	75	Node SygusRepairConst::fitToLogic(Node body,
534		LogicInfo& logic,
535		Node n,
536		const std::vector<Node>& candidates,
537		std::vector<Node>& candidate_skeletons,
538		std::vector<Node>& sk_vars,
539		std::map<Node, Node>& sk_vars_to_subs)
540		{
541	150	std::vector<Node> rm_var;
542	150	Node exc_var;
543	81	while (getFitToLogicExcludeVar(logic, n, exc_var))
544		{
545	75	if (exc_var.isNull())
546		{
547	72	return n;
548		}
549	6	Trace("sygus-repair-const") << "...exclude " << exc_var
550	3	<< " due to logic restrictions." << std::endl;
551	6	TNode tvar = exc_var;
552	3	Assert(sk_vars_to_subs.find(exc_var) != sk_vars_to_subs.end());
553	6	TNode tsubs = sk_vars_to_subs[exc_var];
554		// revert the substitution
555	6	for (unsigned i = 0, size = candidate_skeletons.size(); i < size; i++)
556		{
557	3	candidate_skeletons[i] = candidate_skeletons[i].substitute(tvar, tsubs);
558		}
559		// remove the variable
560	3	sk_vars_to_subs.erase(exc_var);
561		std::vector<Node>::iterator it =
562	3	std::find(sk_vars.begin(), sk_vars.end(), exc_var);
563	3	Assert(it != sk_vars.end());
564	3	sk_vars.erase(it);
565		// reconstruct the query
566	3	n = getFoQuery(body, candidates, candidate_skeletons, sk_vars);
567		// reset the exclusion variable
568	3	exc_var = Node::null();
569		}
570	3	return Node::null();
571		}
572
573	78	bool SygusRepairConst::getFitToLogicExcludeVar(LogicInfo& logic,
574		Node n,
575		Node& exvar)
576		{
577	78	bool restrictLA = logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear();
578
579		// should have at least one restriction
580	78	Assert(restrictLA);
581
582	156	std::unordered_set<TNode> visited;
583	78	std::unordered_set<TNode>::iterator it;
584	156	std::vector<TNode> visit;
585	156	TNode cur;
586	78	visit.push_back(n);
587	3381	do
588		{
589	3459	cur = visit.back();
590	3459	visit.pop_back();
591	3459	it = visited.find(cur);
592
593	3459	if (it == visited.end())
594		{
595	2246	visited.insert(cur);
596	2246	Kind ck = cur.getKind();
597	4492	bool isArithDivKind = (ck == DIVISION_TOTAL \|\| ck == INTS_DIVISION_TOTAL
598	4492	\|\| ck == INTS_MODULUS_TOTAL);
599	2246	Assert(ck != DIVISION && ck != INTS_DIVISION && ck != INTS_MODULUS);
600	2246	if (restrictLA && (ck == NONLINEAR_MULT \|\| isArithDivKind))
601		{
602	15	for (unsigned j = 0, size = cur.getNumChildren(); j < size; j++)
603		{
604	21	Node ccur = cur[j];
605	12	std::map<Node, Node>::iterator itf = d_fo_to_sk.find(ccur);
606	12	if (itf != d_fo_to_sk.end())
607		{
608	3	if (ck == NONLINEAR_MULT \|\| (isArithDivKind && j == 1))
609		{
610	3	exvar = itf->second;
611	3	return true;
612		}
613		}
614		}
615	3	return false;
616		}
617	5684	for (const Node& ccur : cur)
618		{
619	3444	visit.push_back(ccur);
620		}
621		}
622	3453	} while (!visit.empty());
623
624	72	return true;
625		}
626
627		} // namespace quantifiers
628		} // namespace theory
629	29340	} // namespace cvc5