Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_utils.cpp	Lines:	58	78	74.4 %
Date:	2021-08-06	Branches:	110	366	30.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Aina Niemetz
 *
 * 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.
 * ****************************************************************************
 *
 * Generic sygus utilities.
 */

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

#include <sstream>

#include "expr/node_algorithm.h"
#include "expr/skolem_manager.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

/**
 * Attribute for specifying a solution for a function-to-synthesize. This is
 * used for marking certain functions that we have solved for, e.g. during
 * preprocessing.
 */
struct SygusSolutionAttributeId
{
};
typedef expr::Attribute<SygusSolutionAttributeId, Node> SygusSolutionAttribute;

Node SygusUtils::mkSygusConjecture(const std::vector<Node>& fs,
                                   Node conj,
                                   const std::vector<Node>& iattrs)
{
  Assert(!fs.empty());
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  SygusAttribute ca;
  Node sygusVar = sm->mkDummySkolem("sygus", nm->booleanType());
  sygusVar.setAttribute(ca, true);
  std::vector<Node> ipls{nm->mkNode(INST_ATTRIBUTE, sygusVar)};
  // insert the remaining instantiation attributes
  ipls.insert(ipls.end(), iattrs.begin(), iattrs.end());
  Node ipl = nm->mkNode(INST_PATTERN_LIST, ipls);
  Node bvl = nm->mkNode(BOUND_VAR_LIST, fs);
  return nm->mkNode(FORALL, bvl, conj, ipl);
}

Node SygusUtils::mkSygusConjecture(const std::vector<Node>& fs, Node conj)
{
  std::vector<Node> iattrs;
  return mkSygusConjecture(fs, conj, iattrs);
}

Node SygusUtils::mkSygusConjecture(const std::vector<Node>& fs,
                                   Node conj,
                                   const Subs& solvedf)
{
  Assert(!fs.empty());
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  std::vector<Node> iattrs;
  // take existing properties, without the previous solves
  SygusSolutionAttribute ssa;
  // add the current solves, which should be a superset of the previous ones
  for (size_t i = 0, nsolved = solvedf.size(); i < nsolved; i++)
  {
    Node eq = solvedf.getEquality(i);
    Node var = sm->mkDummySkolem("solved", nm->booleanType());
    var.setAttribute(ssa, eq);
    Node ipv = nm->mkNode(INST_ATTRIBUTE, var);
    iattrs.push_back(ipv);
  }
  return mkSygusConjecture(fs, conj, iattrs);
}

void SygusUtils::decomposeSygusConjecture(Node q,
                                          std::vector<Node>& fs,
                                          std::vector<Node>& unsf,
                                          Subs& solvedf)
{
  Assert(q.getKind() == FORALL);
  Assert(q.getNumChildren() == 3);
  Node ipl = q[2];
  Assert(ipl.getKind() == INST_PATTERN_LIST);
  fs.insert(fs.end(), q[0].begin(), q[0].end());
  SygusSolutionAttribute ssa;
  for (const Node& ip : ipl)
  {
    if (ip.getKind() == INST_ATTRIBUTE)
    {
      Node ipv = ip[0];
      // does it specify a sygus solution?
      if (ipv.hasAttribute(ssa))
      {
        Node eq = ipv.getAttribute(ssa);
        Assert(std::find(fs.begin(), fs.end(), eq[0]) != fs.end());
        solvedf.addEquality(eq);
      }
    }
  }
  // add to unsolved functions
  for (const Node& f : fs)
  {
    if (!solvedf.contains(f))
    {
      unsf.push_back(f);
    }
  }
}

Node SygusUtils::decomposeSygusBody(Node conj, std::vector<Node>& vs)
{
  if (conj.getKind() == NOT && conj[0].getKind() == FORALL)
  {
    vs.insert(vs.end(), conj[0][0].begin(), conj[0][0].end());
    return conj[0][1].negate();
  }
  return conj;
}

Node SygusUtils::getSygusArgumentListForSynthFun(Node f)
{
  Node sfvl = f.getAttribute(SygusSynthFunVarListAttribute());
  if (sfvl.isNull() && f.getType().isFunction())
  {
    NodeManager* nm = NodeManager::currentNM();
    std::vector<TypeNode> argTypes = f.getType().getArgTypes();
    // make default variable list if none was specified by input
    std::vector<Node> bvs;
    for (unsigned j = 0, size = argTypes.size(); j < size; j++)
    {
      std::stringstream ss;
      ss << "arg" << j;
      bvs.push_back(nm->mkBoundVar(ss.str(), argTypes[j]));
    }
    sfvl = nm->mkNode(BOUND_VAR_LIST, bvs);
    f.setAttribute(SygusSynthFunVarListAttribute(), sfvl);
  }
  return sfvl;
}

void SygusUtils::getSygusArgumentListForSynthFun(Node f,
                                                 std::vector<Node>& formals)
{
  Node sfvl = getSygusArgumentListForSynthFun(f);
  if (!sfvl.isNull())
  {
    formals.insert(formals.end(), sfvl.begin(), sfvl.end());
  }
}

Node SygusUtils::wrapSolutionForSynthFun(Node f, Node sol)
{
  Node al = getSygusArgumentListForSynthFun(f);
  if (!al.isNull())
  {
    sol = NodeManager::currentNM()->mkNode(LAMBDA, al, sol);
  }
  Assert(!expr::hasFreeVar(sol));
  return sol;
}

TypeNode SygusUtils::getSygusTypeForSynthFun(Node f)
{
  Node gv = f.getAttribute(SygusSynthGrammarAttribute());
  if (!gv.isNull())
  {
    return gv.getType();
  }
  return TypeNode::null();
}

}  // 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, Aina Niemetz
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		* Generic sygus utilities.
14		*/
15
16		#include "theory/quantifiers/sygus/sygus_utils.h"
17
18		#include <sstream>
19
20		#include "expr/node_algorithm.h"
21		#include "expr/skolem_manager.h"
22		#include "theory/quantifiers/quantifiers_attributes.h"
23		#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
24
25		using namespace cvc5::kind;
26
27		namespace cvc5 {
28		namespace theory {
29		namespace quantifiers {
30
31		/**
32		* Attribute for specifying a solution for a function-to-synthesize. This is
33		* used for marking certain functions that we have solved for, e.g. during
34		* preprocessing.
35		*/
36		struct SygusSolutionAttributeId
37		{
38		};
39		typedef expr::Attribute<SygusSolutionAttributeId, Node> SygusSolutionAttribute;
40
41	274	Node SygusUtils::mkSygusConjecture(const std::vector<Node>& fs,
42		Node conj,
43		const std::vector<Node>& iattrs)
44		{
45	274	Assert(!fs.empty());
46	274	NodeManager* nm = NodeManager::currentNM();
47	274	SkolemManager* sm = nm->getSkolemManager();
48		SygusAttribute ca;
49	548	Node sygusVar = sm->mkDummySkolem("sygus", nm->booleanType());
50	274	sygusVar.setAttribute(ca, true);
51	548	std::vector<Node> ipls{nm->mkNode(INST_ATTRIBUTE, sygusVar)};
52		// insert the remaining instantiation attributes
53	274	ipls.insert(ipls.end(), iattrs.begin(), iattrs.end());
54	548	Node ipl = nm->mkNode(INST_PATTERN_LIST, ipls);
55	548	Node bvl = nm->mkNode(BOUND_VAR_LIST, fs);
56	548	return nm->mkNode(FORALL, bvl, conj, ipl);
57		}
58
59	258	Node SygusUtils::mkSygusConjecture(const std::vector<Node>& fs, Node conj)
60		{
61	516	std::vector<Node> iattrs;
62	516	return mkSygusConjecture(fs, conj, iattrs);
63		}
64
65		Node SygusUtils::mkSygusConjecture(const std::vector<Node>& fs,
66		Node conj,
67		const Subs& solvedf)
68		{
69		Assert(!fs.empty());
70		NodeManager* nm = NodeManager::currentNM();
71		SkolemManager* sm = nm->getSkolemManager();
72		std::vector<Node> iattrs;
73		// take existing properties, without the previous solves
74		SygusSolutionAttribute ssa;
75		// add the current solves, which should be a superset of the previous ones
76		for (size_t i = 0, nsolved = solvedf.size(); i < nsolved; i++)
77		{
78		Node eq = solvedf.getEquality(i);
79		Node var = sm->mkDummySkolem("solved", nm->booleanType());
80		var.setAttribute(ssa, eq);
81		Node ipv = nm->mkNode(INST_ATTRIBUTE, var);
82		iattrs.push_back(ipv);
83		}
84		return mkSygusConjecture(fs, conj, iattrs);
85		}
86
87	331	void SygusUtils::decomposeSygusConjecture(Node q,
88		std::vector<Node>& fs,
89		std::vector<Node>& unsf,
90		Subs& solvedf)
91		{
92	331	Assert(q.getKind() == FORALL);
93	331	Assert(q.getNumChildren() == 3);
94	662	Node ipl = q[2];
95	331	Assert(ipl.getKind() == INST_PATTERN_LIST);
96	331	fs.insert(fs.end(), q[0].begin(), q[0].end());
97		SygusSolutionAttribute ssa;
98	678	for (const Node& ip : ipl)
99		{
100	347	if (ip.getKind() == INST_ATTRIBUTE)
101		{
102	694	Node ipv = ip[0];
103		// does it specify a sygus solution?
104	347	if (ipv.hasAttribute(ssa))
105		{
106		Node eq = ipv.getAttribute(ssa);
107		Assert(std::find(fs.begin(), fs.end(), eq[0]) != fs.end());
108		solvedf.addEquality(eq);
109		}
110		}
111		}
112		// add to unsolved functions
113	836	for (const Node& f : fs)
114		{
115	505	if (!solvedf.contains(f))
116		{
117	505	unsf.push_back(f);
118		}
119		}
120	331	}
121
122		Node SygusUtils::decomposeSygusBody(Node conj, std::vector<Node>& vs)
123		{
124		if (conj.getKind() == NOT && conj[0].getKind() == FORALL)
125		{
126		vs.insert(vs.end(), conj[0][0].begin(), conj[0][0].end());
127		return conj[0][1].negate();
128		}
129		return conj;
130		}
131
132	1495	Node SygusUtils::getSygusArgumentListForSynthFun(Node f)
133		{
134	1495	Node sfvl = f.getAttribute(SygusSynthFunVarListAttribute());
135	1495	if (sfvl.isNull() && f.getType().isFunction())
136		{
137	26	NodeManager* nm = NodeManager::currentNM();
138	52	std::vector<TypeNode> argTypes = f.getType().getArgTypes();
139		// make default variable list if none was specified by input
140	52	std::vector<Node> bvs;
141	56	for (unsigned j = 0, size = argTypes.size(); j < size; j++)
142		{
143	60	std::stringstream ss;
144	30	ss << "arg" << j;
145	30	bvs.push_back(nm->mkBoundVar(ss.str(), argTypes[j]));
146		}
147	26	sfvl = nm->mkNode(BOUND_VAR_LIST, bvs);
148	26	f.setAttribute(SygusSynthFunVarListAttribute(), sfvl);
149		}
150	1495	return sfvl;
151		}
152
153	505	void SygusUtils::getSygusArgumentListForSynthFun(Node f,
154		std::vector<Node>& formals)
155		{
156	1010	Node sfvl = getSygusArgumentListForSynthFun(f);
157	505	if (!sfvl.isNull())
158		{
159	371	formals.insert(formals.end(), sfvl.begin(), sfvl.end());
160		}
161	505	}
162
163	154	Node SygusUtils::wrapSolutionForSynthFun(Node f, Node sol)
164		{
165	308	Node al = getSygusArgumentListForSynthFun(f);
166	154	if (!al.isNull())
167		{
168	115	sol = NodeManager::currentNM()->mkNode(LAMBDA, al, sol);
169		}
170	154	Assert(!expr::hasFreeVar(sol));
171	308	return sol;
172		}
173
174	80	TypeNode SygusUtils::getSygusTypeForSynthFun(Node f)
175		{
176	160	Node gv = f.getAttribute(SygusSynthGrammarAttribute());
177	80	if (!gv.isNull())
178		{
179	43	return gv.getType();
180		}
181	37	return TypeNode::null();
182		}
183
184		} // namespace quantifiers
185		} // namespace theory
186	29322	} // namespace cvc5