summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/dtype_cons.h9
-rw-r--r--src/theory/datatypes/theory_datatypes_utils.cpp151
-rw-r--r--src/theory/datatypes/theory_datatypes_utils.h23
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_norm.cpp120
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_norm.h10
-rw-r--r--src/theory/quantifiers/sygus/synth_conjecture.cpp11
-rw-r--r--test/regress/CMakeLists.txt1
-rw-r--r--test/regress/regress1/sygus/yoni-true-sol.smt220
8 files changed, 199 insertions, 146 deletions
diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h
index d5d0013de..ca4806316 100644
--- a/src/expr/dtype_cons.h
+++ b/src/expr/dtype_cons.h
@@ -87,12 +87,9 @@ class DTypeConstructor
void setSygus(Node op);
/** get sygus op
*
- * This method returns the operator or
- * term that this constructor represents
- * in the sygus encoding. This may be a
- * builtin operator, defined function, variable,
- * or constant that this constructor encodes in this
- * deep embedding.
+ * This method returns the operator or term that this constructor represents
+ * in the sygus encoding. This may be a builtin operator, defined function,
+ * variable, or constant that this constructor encodes in this deep embedding.
*/
Node getSygusOp() const;
/** is this a sygus identity function?
diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp
index 13cc8fc19..ee0fd814e 100644
--- a/src/theory/datatypes/theory_datatypes_utils.cpp
+++ b/src/theory/datatypes/theory_datatypes_utils.cpp
@@ -19,7 +19,10 @@
#include "expr/dtype.h"
#include "expr/node_algorithm.h"
#include "expr/sygus_datatype.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
#include "theory/evaluator.h"
+#include "theory/rewriter.h"
using namespace CVC4;
using namespace CVC4::kind;
@@ -117,10 +120,99 @@ Kind getOperatorKindForSygusBuiltin(Node op)
return UNDEFINED_KIND;
}
+struct SygusOpRewrittenAttributeId
+{
+};
+typedef expr::Attribute<SygusOpRewrittenAttributeId, Node>
+ SygusOpRewrittenAttribute;
+
+Kind getEliminateKind(Kind ok)
+{
+ Kind nk = ok;
+ // We also must ensure that builtin operators which are eliminated
+ // during expand definitions are replaced by the proper operator.
+ if (ok == BITVECTOR_UDIV)
+ {
+ nk = BITVECTOR_UDIV_TOTAL;
+ }
+ else if (ok == BITVECTOR_UREM)
+ {
+ nk = BITVECTOR_UREM_TOTAL;
+ }
+ else if (ok == DIVISION)
+ {
+ nk = DIVISION_TOTAL;
+ }
+ else if (ok == INTS_DIVISION)
+ {
+ nk = INTS_DIVISION_TOTAL;
+ }
+ else if (ok == INTS_MODULUS)
+ {
+ nk = INTS_MODULUS_TOTAL;
+ }
+ return nk;
+}
+
+Node eliminatePartialOperators(Node n)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+ std::unordered_map<TNode, Node, TNodeHashFunction>::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() == 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);
+ }
+ Kind ok = cur.getKind();
+ Kind nk = getEliminateKind(ok);
+ if (nk != ok || childChanged)
+ {
+ ret = nm->mkNode(nk, children);
+ }
+ visited[cur] = ret;
+ }
+ } while (!visit.empty());
+ Assert(visited.find(n) != visited.end());
+ Assert(!visited.find(n)->second.isNull());
+ return visited[n];
+}
+
Node mkSygusTerm(const DType& dt,
unsigned i,
const std::vector<Node>& children,
- bool doBetaReduction)
+ bool doBetaReduction,
+ bool isExternal)
{
Trace("dt-sygus-util") << "Make sygus term " << dt.getName() << "[" << i
<< "] with children: " << children << std::endl;
@@ -128,7 +220,49 @@ Node mkSygusTerm(const DType& dt,
Assert(dt.isSygus());
Assert(!dt[i].getSygusOp().isNull());
Node op = dt[i].getSygusOp();
- return mkSygusTerm(op, children, doBetaReduction);
+ Node opn = op;
+ if (!isExternal)
+ {
+ // Get the normalized version of the sygus operator. We do this by
+ // expanding definitions, rewriting it, and eliminating partial operators.
+ if (!op.hasAttribute(SygusOpRewrittenAttribute()))
+ {
+ if (op.isConst())
+ {
+ // If it is a builtin operator, convert to total version if necessary.
+ // First, get the kind for the operator.
+ Kind ok = NodeManager::operatorToKind(op);
+ Trace("sygus-grammar-normalize-debug")
+ << "...builtin kind is " << ok << std::endl;
+ Kind nk = getEliminateKind(ok);
+ if (nk != ok)
+ {
+ Trace("sygus-grammar-normalize-debug")
+ << "...replace by builtin operator " << nk << std::endl;
+ opn = NodeManager::currentNM()->operatorOf(nk);
+ }
+ }
+ else
+ {
+ // Only expand definitions if the operator is not constant, since
+ // calling expandDefinitions on them should be a no-op. This check
+ // ensures we don't try to expand e.g. bitvector extract operators,
+ // whose type is undefined, and thus should not be passed to
+ // expandDefinitions.
+ opn = Node::fromExpr(
+ smt::currentSmtEngine()->expandDefinitions(op.toExpr()));
+ opn = Rewriter::rewrite(opn);
+ opn = eliminatePartialOperators(opn);
+ SygusOpRewrittenAttribute sora;
+ op.setAttribute(sora, opn);
+ }
+ }
+ else
+ {
+ opn = op.getAttribute(SygusOpRewrittenAttribute());
+ }
+ }
+ return mkSygusTerm(opn, children, doBetaReduction);
}
Node mkSygusTerm(Node op,
@@ -386,7 +520,7 @@ struct SygusToBuiltinTermAttributeId
typedef expr::Attribute<SygusToBuiltinTermAttributeId, Node>
SygusToBuiltinTermAttribute;
-Node sygusToBuiltin(Node n)
+Node sygusToBuiltin(Node n, bool isExternal)
{
Assert(n.isConst());
std::unordered_map<TNode, Node, TNodeHashFunction> visited;
@@ -404,7 +538,7 @@ Node sygusToBuiltin(Node n)
{
if (cur.getKind() == APPLY_CONSTRUCTOR)
{
- if (cur.hasAttribute(SygusToBuiltinTermAttribute()))
+ if (!isExternal && cur.hasAttribute(SygusToBuiltinTermAttribute()))
{
visited[cur] = cur.getAttribute(SygusToBuiltinTermAttribute());
}
@@ -445,12 +579,15 @@ Node sygusToBuiltin(Node n)
children.push_back(it->second);
}
index = indexOf(cur.getOperator());
- ret = mkSygusTerm(dt, index, children);
+ ret = mkSygusTerm(dt, index, children, true, isExternal);
}
visited[cur] = ret;
// cache
- SygusToBuiltinTermAttribute stbt;
- cur.setAttribute(stbt, ret);
+ if (!isExternal)
+ {
+ SygusToBuiltinTermAttribute stbt;
+ cur.setAttribute(stbt, ret);
+ }
}
} while (!visit.empty());
Assert(visited.find(n) != visited.end());
diff --git a/src/theory/datatypes/theory_datatypes_utils.h b/src/theory/datatypes/theory_datatypes_utils.h
index b23302276..58f719910 100644
--- a/src/theory/datatypes/theory_datatypes_utils.h
+++ b/src/theory/datatypes/theory_datatypes_utils.h
@@ -146,17 +146,31 @@ bool checkClash(Node n1, Node n2, std::vector<Node>& rew);
* function mkSygusTerm.
*/
Kind getOperatorKindForSygusBuiltin(Node op);
+/**
+ * Returns the total version of Kind k if it is a partial operator, or
+ * otherwise k itself.
+ */
+Kind getEliminateKind(Kind k);
+/**
+ * Returns a version of n where all partial functions such as bvudiv
+ * have been replaced by their total versions like bvudiv_total.
+ */
+Node eliminatePartialOperators(Node n);
/** make sygus term
*
* This function returns a builtin term f( children[0], ..., children[n] )
* where f is the builtin op that the i^th constructor of sygus datatype dt
* encodes. If doBetaReduction is true, then lambdas are eagerly eliminated
* via beta reduction.
+ *
+ * If isExternal is true, then the returned term respects the original grammar
+ * that was provided. This includes the use of defined functions.
*/
Node mkSygusTerm(const DType& dt,
unsigned i,
const std::vector<Node>& children,
- bool doBetaReduction = true);
+ bool doBetaReduction = true,
+ bool isExternal = false);
/**
* Same as above, but we already have the sygus operator op. The above method
* is syntax sugar for calling this method on dt[i].getSygusOp().
@@ -201,8 +215,13 @@ Node applySygusArgs(const DType& dt,
* equivalent. For example, given input C_*( C_x(), C_y() ), this method returns
* x*y, assuming C_+, C_x, and C_y have sygus operators *, x, and y
* respectively.
+ *
+ * If isExternal is true, then the returned term respects the original grammar
+ * that was provided. This includes the use of defined functions. This argument
+ * should typically be false, unless we are e.g. exporting the value of the
+ * term as a final solution.
*/
-Node sygusToBuiltin(Node c);
+Node sygusToBuiltin(Node c, bool isExternal = false);
/** Sygus to builtin eval
*
* This method returns the rewritten form of (DT_SYGUS_EVAL n args). Notice that
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index f00fd0092..3b2c56974 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -81,87 +81,6 @@ SygusGrammarNorm::TypeObject::TypeObject(TypeNode src_tn, TypeNode unres_tn)
d_sdt(unres_tn.getAttribute(expr::VarNameAttr()))
{
}
-Kind SygusGrammarNorm::TypeObject::getEliminateKind(Kind ok)
-{
- Kind nk = ok;
- // We also must ensure that builtin operators which are eliminated
- // during expand definitions are replaced by the proper operator.
- if (ok == BITVECTOR_UDIV)
- {
- nk = BITVECTOR_UDIV_TOTAL;
- }
- else if (ok == BITVECTOR_UREM)
- {
- nk = BITVECTOR_UREM_TOTAL;
- }
- else if (ok == DIVISION)
- {
- nk = DIVISION_TOTAL;
- }
- else if (ok == INTS_DIVISION)
- {
- nk = INTS_DIVISION_TOTAL;
- }
- else if (ok == INTS_MODULUS)
- {
- nk = INTS_MODULUS_TOTAL;
- }
- return nk;
-}
-
-Node SygusGrammarNorm::TypeObject::eliminatePartialOperators(Node n)
-{
- NodeManager* nm = NodeManager::currentNM();
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::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() == 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);
- }
- Kind ok = cur.getKind();
- Kind nk = getEliminateKind(ok);
- if (nk != ok || childChanged)
- {
- ret = nm->mkNode(nk, children);
- }
- visited[cur] = ret;
- }
- } while (!visit.empty());
- Assert(visited.find(n) != visited.end());
- Assert(!visited.find(n)->second.isNull());
- return visited[n];
-}
void SygusGrammarNorm::TypeObject::addConsInfo(
SygusGrammarNorm* sygus_norm,
@@ -174,41 +93,6 @@ void SygusGrammarNorm::TypeObject::addConsInfo(
Node sygus_op = cons.getSygusOp();
Trace("sygus-grammar-normalize-debug")
<< ".....operator is " << sygus_op << std::endl;
- Node exp_sop_n = sygus_op;
- if (exp_sop_n.isConst())
- {
- // If it is a builtin operator, convert to total version if necessary.
- // First, get the kind for the operator.
- Kind ok = NodeManager::operatorToKind(exp_sop_n);
- Trace("sygus-grammar-normalize-debug")
- << "...builtin kind is " << ok << std::endl;
- Kind nk = getEliminateKind(ok);
- if (nk != ok)
- {
- Trace("sygus-grammar-normalize-debug")
- << "...replace by builtin operator " << nk << std::endl;
- exp_sop_n = NodeManager::currentNM()->operatorOf(nk);
- }
- }
- else
- {
- // Only expand definitions if the operator is not constant, since calling
- // expandDefinitions on them should be a no-op. This check ensures we don't
- // try to expand e.g. bitvector extract operators, whose type is undefined,
- // and thus should not be passed to expandDefinitions.
- exp_sop_n = Node::fromExpr(
- smt::currentSmtEngine()->expandDefinitions(sygus_op.toExpr()));
- exp_sop_n = Rewriter::rewrite(exp_sop_n);
- Trace("sygus-grammar-normalize-debug")
- << ".....operator (post-rewrite) is " << exp_sop_n << std::endl;
- // eliminate all partial operators from it
- exp_sop_n = eliminatePartialOperators(exp_sop_n);
- Trace("sygus-grammar-normalize-debug")
- << ".....operator (eliminate partial operators) is " << exp_sop_n
- << std::endl;
- // rewrite again
- exp_sop_n = Rewriter::rewrite(exp_sop_n);
- }
std::vector<TypeNode> consTypes;
const std::vector<std::shared_ptr<DTypeSelector> >& args = cons.getArgs();
@@ -222,10 +106,8 @@ void SygusGrammarNorm::TypeObject::addConsInfo(
consTypes.push_back(atype);
}
- Trace("sygus-type-cons-defs") << "\tOriginal op: " << cons.getSygusOp()
- << "\n\tExpanded one: " << exp_sop_n << "\n\n";
d_sdt.addConstructor(
- exp_sop_n, cons.getName(), consTypes, spc, cons.getWeight());
+ sygus_op, cons.getName(), consTypes, spc, cons.getWeight());
}
void SygusGrammarNorm::TypeObject::initializeDatatype(
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
index 360762b38..956228f38 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
@@ -200,16 +200,6 @@ class SygusGrammarNorm
void addConsInfo(SygusGrammarNorm* sygus_norm,
const DTypeConstructor& cons,
std::shared_ptr<SygusPrintCallback> spc);
- /**
- * Returns the total version of Kind k if it is a partial operator, or
- * otherwise k itself.
- */
- static Kind getEliminateKind(Kind k);
- /**
- * Returns a version of n where all partial functions such as bvudiv
- * have been replaced by their total versions like bvudiv_total.
- */
- static Node eliminatePartialOperators(Node n);
/** initializes a datatype with the information in the type object
*
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 1596c30f0..e69d746fe 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -1178,8 +1178,10 @@ bool SynthConjecture::getSynthSolutions(
NodeManager* nm = NodeManager::currentNM();
std::vector<Node> sols;
std::vector<int> statuses;
+ Trace("cegqi-debug") << "getSynthSolutions..." << std::endl;
if (!getSynthSolutionsInternal(sols, statuses))
{
+ Trace("cegqi-debug") << "...failed internal" << std::endl;
return false;
}
// we add it to the solution map, indexed by this conjecture
@@ -1188,12 +1190,16 @@ bool SynthConjecture::getSynthSolutions(
{
Node sol = sols[i];
int status = statuses[i];
+ Trace("cegqi-debug") << "...got " << i << ": " << sol
+ << ", status=" << status << std::endl;
// get the builtin solution
Node bsol = sol;
if (status != 0)
{
- // convert sygus to builtin here
- bsol = d_tds->sygusToBuiltin(sol, sol.getType());
+ // Convert sygus to builtin here.
+ // We must use the external representation to ensure bsol matches the
+ // grammar.
+ bsol = datatypes::utils::sygusToBuiltin(sol, true);
}
// convert to lambda
TypeNode tn = d_embed_quant[0][i].getType();
@@ -1214,6 +1220,7 @@ bool SynthConjecture::getSynthSolutions(
}
// store in map
smc[fvar] = bsol;
+ Trace("cegqi-debug") << "...return " << bsol << std::endl;
}
return true;
}
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8aae1890d..06dc2d87c 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1951,6 +1951,7 @@ set(regress_1_tests
regress1/sygus/unbdd_inv_gen_ex7.sy
regress1/sygus/unbdd_inv_gen_winf1.sy
regress1/sygus/univ_2-long-repeat.sy
+ regress1/sygus/yoni-true-sol.smt2
regress1/sym/q-constant.smt2
regress1/sym/q-function.smt2
regress1/sym/qf-function.smt2
diff --git a/test/regress/regress1/sygus/yoni-true-sol.smt2 b/test/regress/regress1/sygus/yoni-true-sol.smt2
new file mode 100644
index 000000000..464f7c729
--- /dev/null
+++ b/test/regress/regress1/sygus/yoni-true-sol.smt2
@@ -0,0 +1,20 @@
+; COMMAND-LINE: --produce-abducts
+; EXPECT: (define-fun A () Bool (>= j i))
+(set-logic QF_LIA)
+(set-option :produce-abducts true)
+(declare-fun n () Int)
+(declare-fun m () Int)
+(declare-fun i () Int)
+(declare-fun j () Int)
+(assert (and (>= n 0) (>= m 0)))
+(assert (< n i))
+(assert (< (+ i j) m))
+(get-abduct A
+ (<= n m)
+ ((GA Bool) (GJ Int) (GI Int))
+ (
+ (GA Bool ((>= GJ GI)))
+ (GJ Int ( j))
+ (GI Int ( i))
+ )
+)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback