It was not robust to cases where a function-to-synthesize occurred in a higher-order context.
Also does general clean up of the single invocation utility.
+void Subs::clear()
+{
+ d_vars.clear();
+ d_subs.clear();
+}
+
std::ostream& operator<<(std::ostream& out, const Subs& s)
{
out << s.toString();
std::ostream& operator<<(std::ostream& out, const Subs& s)
{
out << s.toString();
std::map<Node, Node> toMap() const;
/** Get string for this substitution */
std::string toString() const;
std::map<Node, Node> toMap() const;
/** Get string for this substitution */
std::string toString() const;
+ /** clear the substitution */
+ void clear();
/** The data */
std::vector<Node> d_vars;
std::vector<Node> d_subs;
/** The data */
std::vector<Node> d_vars;
std::vector<Node> d_subs;
std::map<Node, bool> visited;
// functions to arguments
std::vector<Node> args;
std::map<Node, bool> visited;
// functions to arguments
std::vector<Node> args;
- std::vector<Node> terms;
- std::vector<Node> subs;
bool singleInvocation = true;
bool ngroundSingleInvocation = false;
bool singleInvocation = true;
bool ngroundSingleInvocation = false;
- if (processConjunct(cr, visited, args, terms, subs))
+ if (processConjunct(cr, visited, args, sb))
- for (unsigned j = 0; j < terms.size(); j++)
+ for (size_t j = 0, vsize = sb.d_vars.size(); j < vsize; j++)
- si_terms.push_back(subs[j]);
- Node op = subs[j].hasOperator() ? subs[j].getOperator() : subs[j];
+ Node s = sb.d_subs[j];
+ si_terms.push_back(s);
+ Node op = s.hasOperator() ? s.getOperator() : s;
Assert(d_func_fo_var.find(op) != d_func_fo_var.end());
si_subs.push_back(d_func_fo_var[op]);
}
std::map<Node, Node> subs_map;
std::map<Node, Node> subs_map_rev;
// normalize the invocations
Assert(d_func_fo_var.find(op) != d_func_fo_var.end());
si_subs.push_back(d_func_fo_var[op]);
}
std::map<Node, Node> subs_map;
std::map<Node, Node> subs_map_rev;
// normalize the invocations
- Assert(terms.size() == subs.size());
- cr = cr.substitute(
- terms.begin(), terms.end(), subs.begin(), subs.end());
}
std::vector<Node> children;
children.push_back(cr);
}
std::vector<Node> children;
children.push_back(cr);
- terms.clear();
- subs.clear();
Trace("si-prt") << "...single invocation, with arguments: "
<< std::endl;
for (unsigned j = 0; j < args.size(); j++)
{
Trace("si-prt") << args[j] << " ";
Trace("si-prt") << "...single invocation, with arguments: "
<< std::endl;
for (unsigned j = 0; j < args.size(); j++)
{
Trace("si-prt") << args[j] << " ";
- if (args[j].getKind() == BOUND_VARIABLE
- && std::find(terms.begin(), terms.end(), args[j]) == terms.end())
+ if (args[j].getKind() == BOUND_VARIABLE && !sb.contains(args[j]))
- terms.push_back(args[j]);
- subs.push_back(d_si_vars[j]);
+ sb.add(args[j], d_si_vars[j]);
}
}
Trace("si-prt") << std::endl;
}
}
Trace("si-prt") << std::endl;
- cr = children.size() == 1
- ? children[0]
- : NodeManager::currentNM()->mkNode(OR, children);
- Assert(terms.size() == subs.size());
- cr =
- cr.substitute(terms.begin(), terms.end(), subs.begin(), subs.end());
+ cr = nm->mkOr(children);
+ cr = sb.apply(cr);
Trace("si-prt-debug") << "...normalized invocations to " << cr
<< std::endl;
// now must check if it has other bound variables
Trace("si-prt-debug") << "...normalized invocations to " << cr
<< std::endl;
// now must check if it has other bound variables
bool SingleInvocationPartition::processConjunct(Node n,
std::map<Node, bool>& visited,
std::vector<Node>& args,
bool SingleInvocationPartition::processConjunct(Node n,
std::map<Node, bool>& visited,
std::vector<Node>& args,
- std::vector<Node>& terms,
- std::vector<Node>& subs)
{
std::map<Node, bool>::iterator it = visited.find(n);
if (it != visited.end())
{
std::map<Node, bool>::iterator it = visited.find(n);
if (it != visited.end())
bool ret = true;
for (unsigned i = 0; i < n.getNumChildren(); i++)
{
bool ret = true;
for (unsigned i = 0; i < n.getNumChildren(); i++)
{
- if (!processConjunct(n[i], visited, args, terms, subs))
+ if (!processConjunct(n[i], visited, args, sb))
if (std::find(d_input_funcs.begin(), d_input_funcs.end(), f)
!= d_input_funcs.end())
{
if (std::find(d_input_funcs.begin(), d_input_funcs.end(), f)
!= d_input_funcs.end())
{
+ // If n is an application of a function-to-synthesize f, or is
+ // itself a function-to-synthesize, then n must be fully applied.
+ // This catches cases where n is a function-to-synthesize that occurs
+ // in a higher-order context.
+ // If the type of n is functional, then it is not fully applied.
+ if (n.getType().isFunction())
+ {
+ ret = false;
+ success = false;
+ }
+ else
+ {
+ success = true;
+ }
- if (std::find(terms.begin(), terms.end(), n) == terms.end())
+ Trace("si-prt-debug") << "Process " << n << std::endl;
+ if (!sb.contains(n))
{
// check if it matches the type requirement
if (isAntiSkolemizableType(f))
{
// check if it matches the type requirement
if (isAntiSkolemizableType(f))
- terms.push_back(n);
- subs.push_back(d_func_inv[f]);
+ sb.add(n, d_func_inv[f]);
visited[n] = ret;
return ret;
}
visited[n] = ret;
return ret;
}
#include <vector>
#include "expr/node.h"
#include <vector>
#include "expr/node.h"
#include "expr/type_node.h"
namespace cvc5 {
#include "expr/type_node.h"
namespace cvc5 {
bool processConjunct(Node n,
std::map<Node, bool>& visited,
std::vector<Node>& args,
bool processConjunct(Node n,
std::map<Node, bool>& visited,
std::vector<Node>& args,
- std::vector<Node>& terms,
- std::vector<Node>& subs);
/** get the and node corresponding to d_conjuncts[index] */
Node getConjunct(int index);
/** get the and node corresponding to d_conjuncts[index] */
Node getConjunct(int index);
regress0/sygus/dt-sel-parse1.sy
regress0/sygus/General_plus10.sy
regress0/sygus/hd-05-d1-prog-nogrammar.sy
regress0/sygus/dt-sel-parse1.sy
regress0/sygus/General_plus10.sy
regress0/sygus/hd-05-d1-prog-nogrammar.sy
+ regress0/sygus/ho-occ-synth-fun.sy
regress0/sygus/inv-different-var-order.sy
regress0/sygus/issue3356-syg-inf-usort.smt2
regress0/sygus/issue3624.sy
regress0/sygus/inv-different-var-order.sy
regress0/sygus/issue3356-syg-inf-usort.smt2
regress0/sygus/issue3624.sy
--- /dev/null
+; COMMAND-LINE: --sygus-out=status
+; EXPECT: unsat
+(set-logic HO_ALL)
+(synth-fun f ((x Int)) Int)
+(synth-fun g ((x Int)) Int)
+(declare-var P (-> (-> Int Int) Bool))
+(constraint (=> (P f) (P g)))
+; a trivial class of solutions is where f = g.
+(check-synth)