theory/datatypes/theory_datatypes_type_rules.h \
theory/datatypes/type_enumerator.cpp \
theory/datatypes/type_enumerator.h \
+ theory/datatypes/sygus_simple_sym.cpp \
+ theory/datatypes/sygus_simple_sym.h \
theory/ext_theory.cpp \
theory/ext_theory.h \
theory/fp/theory_fp.cpp \
using namespace CVC4::theory::datatypes;
SygusSymBreakNew::SygusSymBreakNew(TheoryDatatypes* td,
- quantifiers::TermDbSygus* tds,
+ QuantifiersEngine* qe,
context::Context* c)
: d_td(td),
- d_tds(tds),
+ d_tds(qe->getTermDatabaseSygus()),
+ d_ssb(qe),
d_testers(c),
d_testers_exp(c),
d_active_terms(c),
- d_currTermSize(c) {
+ d_currTermSize(c)
+{
d_zero = NodeManager::currentNM()->mkConst(Rational(0));
d_true = NodeManager::currentNM()->mkConst(true);
}
std::map<unsigned, unsigned> children_solved;
for (unsigned j = 0; j < dt_index_nargs; j++)
{
- int i = d_tds->solveForArgument(tn, tindex, j);
+ int i = d_ssb.solveForArgument(tn, tindex, j);
if (i >= 0)
{
children_solved[j] = i;
{
Trace("sygus-sb-simple-debug") << " argument " << j << " " << k
<< " is : " << nck << std::endl;
- red = !d_tds->considerArgKind(tnc, tn, nck, nk, j);
+ red = !d_ssb.considerArgKind(tnc, tn, nck, nk, j);
}
else
{
Trace("sygus-sb-simple-debug")
<< " argument " << j << " " << k << " is constant : " << cc
<< std::endl;
- red = !d_tds->considerConst(tnc, tn, cc, nk, j);
+ red = !d_ssb.considerConst(tnc, tn, cc, nk, j);
if (usingAnyConstCons)
{
// we only consider concrete constant constructors
#include "context/context.h"
#include "expr/datatype.h"
#include "expr/node.h"
+#include "theory/datatypes/sygus_simple_sym.h"
#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
#include "theory/quantifiers/sygus/sygus_explain.h"
#include "theory/quantifiers/sygus_sampler.h"
public:
SygusSymBreakNew(TheoryDatatypes* td,
- quantifiers::TermDbSygus* tds,
+ QuantifiersEngine* qe,
context::Context* c);
~SygusSymBreakNew();
/**
TheoryDatatypes* d_td;
/** Pointer to the sygus term database */
quantifiers::TermDbSygus* d_tds;
+ /** the simple symmetry breaking utility */
+ SygusSimpleSymBreak d_ssb;
/**
* Map from terms to the index of the tester that is asserted for them in
* the current SAT context. In other words, if d_testers[n] = 2, then the
--- /dev/null
+/********************* */
+/*! \file sygus_simple_sym.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief Implementation of simple symmetry breaking for sygus
+ **/
+
+#include "theory/datatypes/sygus_simple_sym.h"
+
+#include "theory/quantifiers_engine.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+
+SygusSimpleSymBreak::SygusSimpleSymBreak(QuantifiersEngine* qe)
+ : d_tds(qe->getTermDatabaseSygus()), d_tutil(qe->getTermUtil())
+{
+}
+
+/** Requirement trie
+ *
+ * This class is used to make queries about sygus grammars, including what
+ * constructors they contain, and their types.
+ *
+ * As a simple example, consider the trie:
+ * root:
+ * d_req_kind = PLUS
+ * d_children[0]:
+ * d_req_type = A
+ * d_children[1]:
+ * d_req_type = A
+ * This trie is satisfied by sygus types that have a constructor whose builtin
+ * kind is PLUS and whose argument types are both A.
+ */
+class ReqTrie
+{
+ public:
+ ReqTrie() : d_req_kind(UNDEFINED_KIND) {}
+ /** the children of this node */
+ std::map<unsigned, ReqTrie> d_children;
+ /** the (builtin) kind required by this node */
+ Kind d_req_kind;
+ /** the type that this node is required to be */
+ TypeNode d_req_type;
+ /** the constant required by this node */
+ Node d_req_const;
+ /** print this trie */
+ void print(const char* c, int indent = 0)
+ {
+ if (d_req_kind != UNDEFINED_KIND)
+ {
+ Trace(c) << d_req_kind << " ";
+ }
+ else if (!d_req_type.isNull())
+ {
+ Trace(c) << d_req_type;
+ }
+ else if (!d_req_const.isNull())
+ {
+ Trace(c) << d_req_const;
+ }
+ else
+ {
+ Trace(c) << "_";
+ }
+ Trace(c) << std::endl;
+ for (std::map<unsigned, ReqTrie>::iterator it = d_children.begin();
+ it != d_children.end();
+ ++it)
+ {
+ for (int i = 0; i <= indent; i++)
+ {
+ Trace(c) << " ";
+ }
+ Trace(c) << it->first << " : ";
+ it->second.print(c, indent + 1);
+ }
+ }
+ /**
+ * Are the requirements of this trie satisfied by sygus type tn?
+ * tdb is a reference to the sygus term database.
+ */
+ bool satisfiedBy(quantifiers::TermDbSygus* tdb, TypeNode tn)
+ {
+ if (!d_req_const.isNull())
+ {
+ if (!tdb->hasConst(tn, d_req_const))
+ {
+ return false;
+ }
+ }
+ if (!d_req_type.isNull())
+ {
+ Trace("sygus-sb-debug")
+ << "- check if " << tn << " is type " << d_req_type << std::endl;
+ if (tn != d_req_type)
+ {
+ return false;
+ }
+ }
+ if (d_req_kind != UNDEFINED_KIND)
+ {
+ Trace("sygus-sb-debug")
+ << "- check if " << tn << " has " << d_req_kind << std::endl;
+ std::vector<TypeNode> argts;
+ if (tdb->canConstructKind(tn, d_req_kind, argts))
+ {
+ bool ret = true;
+ for (std::map<unsigned, ReqTrie>::iterator it = d_children.begin();
+ it != d_children.end();
+ ++it)
+ {
+ if (it->first < argts.size())
+ {
+ TypeNode tnc = argts[it->first];
+ if (!it->second.satisfiedBy(tdb, tnc))
+ {
+ return false;
+ }
+ }
+ else
+ {
+ return false;
+ }
+ }
+ if (!ret)
+ {
+ return false;
+ }
+ }
+ else
+ {
+ return false;
+ }
+ }
+ return true;
+ }
+ /** is this the empty (trivially satisfied) trie? */
+ bool empty()
+ {
+ return d_req_kind == UNDEFINED_KIND && d_req_const.isNull()
+ && d_req_type.isNull() && d_children.empty();
+ }
+};
+
+bool SygusSimpleSymBreak::considerArgKind(
+ TypeNode tn, TypeNode tnp, Kind k, Kind pk, int arg)
+{
+ const Datatype& pdt = ((DatatypeType)(tnp).toType()).getDatatype();
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ Assert(d_tds->hasKind(tn, k));
+ Assert(d_tds->hasKind(tnp, pk));
+ Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk
+ << ", arg = " << arg << " in " << tnp << "?"
+ << std::endl;
+ int c = d_tds->getKindConsNum(tn, k);
+ int pc = d_tds->getKindConsNum(tnp, pk);
+ // check for associativity
+ if (k == pk && quantifiers::TermUtil::isAssoc(k))
+ {
+ // if the operator is associative, then a repeated occurrence should only
+ // occur in the leftmost argument position
+ int firstArg = getFirstArgOccurrence(pdt[pc], tn);
+ Assert(firstArg != -1);
+ if (arg == firstArg)
+ {
+ return true;
+ }
+ // the argument types of the child must be the parent's type
+ for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
+ {
+ TypeNode tn = TypeNode::fromType(dt[c].getArgType(i));
+ if (tn != tnp)
+ {
+ return true;
+ }
+ }
+ Trace("sygus-sb-simple")
+ << " sb-simple : do not consider " << k << " at child arg " << arg
+ << " of " << k
+ << " since it is associative, with first arg = " << firstArg
+ << std::endl;
+ return false;
+ }
+ // describes the shape of an alternate term to construct
+ // we check whether this term is in the sygus grammar below
+ ReqTrie rt;
+ Assert(rt.empty());
+
+ // construct rt by cases
+ if (pk == NOT || pk == BITVECTOR_NOT || pk == UMINUS || pk == BITVECTOR_NEG)
+ {
+ // negation normal form
+ if (pk == k)
+ {
+ rt.d_req_type = TypeNode::fromType(dt[c].getArgType(0));
+ }
+ else
+ {
+ Kind reqk = UNDEFINED_KIND; // required kind for all children
+ std::map<unsigned, Kind> reqkc; // required kind for some children
+ if (pk == NOT)
+ {
+ if (k == AND)
+ {
+ rt.d_req_kind = OR;
+ reqk = NOT;
+ }
+ else if (k == OR)
+ {
+ rt.d_req_kind = AND;
+ reqk = NOT;
+ }
+ else if (k == EQUAL)
+ {
+ rt.d_req_kind = XOR;
+ }
+ else if (k == XOR)
+ {
+ rt.d_req_kind = EQUAL;
+ }
+ else if (k == ITE)
+ {
+ rt.d_req_kind = ITE;
+ reqkc[1] = NOT;
+ reqkc[2] = NOT;
+ rt.d_children[0].d_req_type = TypeNode::fromType(dt[c].getArgType(0));
+ }
+ else if (k == LEQ || k == GT)
+ {
+ // (not (~ x y)) -----> (~ (+ y 1) x)
+ rt.d_req_kind = k;
+ rt.d_children[0].d_req_kind = PLUS;
+ rt.d_children[0].d_children[0].d_req_type =
+ TypeNode::fromType(dt[c].getArgType(1));
+ rt.d_children[0].d_children[1].d_req_const =
+ NodeManager::currentNM()->mkConst(Rational(1));
+ rt.d_children[1].d_req_type = TypeNode::fromType(dt[c].getArgType(0));
+ }
+ else if (k == LT || k == GEQ)
+ {
+ // (not (~ x y)) -----> (~ y (+ x 1))
+ rt.d_req_kind = k;
+ rt.d_children[0].d_req_type = TypeNode::fromType(dt[c].getArgType(1));
+ rt.d_children[1].d_req_kind = PLUS;
+ rt.d_children[1].d_children[0].d_req_type =
+ TypeNode::fromType(dt[c].getArgType(0));
+ rt.d_children[1].d_children[1].d_req_const =
+ NodeManager::currentNM()->mkConst(Rational(1));
+ }
+ }
+ else if (pk == BITVECTOR_NOT)
+ {
+ if (k == BITVECTOR_AND)
+ {
+ rt.d_req_kind = BITVECTOR_OR;
+ reqk = BITVECTOR_NOT;
+ }
+ else if (k == BITVECTOR_OR)
+ {
+ rt.d_req_kind = BITVECTOR_AND;
+ reqk = BITVECTOR_NOT;
+ }
+ else if (k == BITVECTOR_XNOR)
+ {
+ rt.d_req_kind = BITVECTOR_XOR;
+ }
+ else if (k == BITVECTOR_XOR)
+ {
+ rt.d_req_kind = BITVECTOR_XNOR;
+ }
+ }
+ else if (pk == UMINUS)
+ {
+ if (k == PLUS)
+ {
+ rt.d_req_kind = PLUS;
+ reqk = UMINUS;
+ }
+ }
+ else if (pk == BITVECTOR_NEG)
+ {
+ if (k == PLUS)
+ {
+ rt.d_req_kind = PLUS;
+ reqk = BITVECTOR_NEG;
+ }
+ }
+ if (!rt.empty() && (reqk != UNDEFINED_KIND || !reqkc.empty()))
+ {
+ int pcr = d_tds->getKindConsNum(tnp, rt.d_req_kind);
+ if (pcr != -1)
+ {
+ Assert(pcr < static_cast<int>(pdt.getNumConstructors()));
+ // must have same number of arguments
+ if (pdt[pcr].getNumArgs() == dt[c].getNumArgs())
+ {
+ for (unsigned i = 0, nargs = pdt[pcr].getNumArgs(); i < nargs; i++)
+ {
+ Kind rk = reqk;
+ if (reqk == UNDEFINED_KIND)
+ {
+ std::map<unsigned, Kind>::iterator itr = reqkc.find(i);
+ if (itr != reqkc.end())
+ {
+ rk = itr->second;
+ }
+ }
+ if (rk != UNDEFINED_KIND)
+ {
+ rt.d_children[i].d_req_kind = rk;
+ rt.d_children[i].d_children[0].d_req_type =
+ TypeNode::fromType(dt[c].getArgType(i));
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ else if (k == MINUS || k == BITVECTOR_SUB)
+ {
+ if (pk == EQUAL || pk == MINUS || pk == BITVECTOR_SUB || pk == LEQ
+ || pk == LT || pk == GEQ || pk == GT)
+ {
+ int oarg = arg == 0 ? 1 : 0;
+ // (~ x (- y z)) ----> (~ (+ x z) y)
+ // (~ (- y z) x) ----> (~ y (+ x z))
+ rt.d_req_kind = pk;
+ rt.d_children[arg].d_req_type = TypeNode::fromType(dt[c].getArgType(0));
+ rt.d_children[oarg].d_req_kind = k == MINUS ? PLUS : BITVECTOR_PLUS;
+ rt.d_children[oarg].d_children[0].d_req_type =
+ TypeNode::fromType(pdt[pc].getArgType(oarg));
+ rt.d_children[oarg].d_children[1].d_req_type =
+ TypeNode::fromType(dt[c].getArgType(1));
+ }
+ else if (pk == PLUS || pk == BITVECTOR_PLUS)
+ {
+ // (+ x (- y z)) -----> (- (+ x y) z)
+ // (+ (- y z) x) -----> (- (+ x y) z)
+ rt.d_req_kind = pk == PLUS ? MINUS : BITVECTOR_SUB;
+ int oarg = arg == 0 ? 1 : 0;
+ rt.d_children[0].d_req_kind = pk;
+ rt.d_children[0].d_children[0].d_req_type =
+ TypeNode::fromType(pdt[pc].getArgType(oarg));
+ rt.d_children[0].d_children[1].d_req_type =
+ TypeNode::fromType(dt[c].getArgType(0));
+ rt.d_children[1].d_req_type = TypeNode::fromType(dt[c].getArgType(1));
+ }
+ }
+ else if (k == ITE)
+ {
+ if (pk != ITE)
+ {
+ // (o X (ite y z w) X') -----> (ite y (o X z X') (o X w X'))
+ rt.d_req_kind = ITE;
+ rt.d_children[0].d_req_type = TypeNode::fromType(dt[c].getArgType(0));
+ unsigned n_args = pdt[pc].getNumArgs();
+ for (unsigned r = 1; r <= 2; r++)
+ {
+ rt.d_children[r].d_req_kind = pk;
+ for (unsigned q = 0; q < n_args; q++)
+ {
+ if ((int)q == arg)
+ {
+ rt.d_children[r].d_children[q].d_req_type =
+ TypeNode::fromType(dt[c].getArgType(r));
+ }
+ else
+ {
+ rt.d_children[r].d_children[q].d_req_type =
+ TypeNode::fromType(pdt[pc].getArgType(q));
+ }
+ }
+ }
+ // this increases term size but is probably a good idea
+ }
+ }
+ else if (k == NOT)
+ {
+ if (pk == ITE)
+ {
+ // (ite (not y) z w) -----> (ite y w z)
+ rt.d_req_kind = ITE;
+ rt.d_children[0].d_req_type = TypeNode::fromType(dt[c].getArgType(0));
+ rt.d_children[1].d_req_type = TypeNode::fromType(pdt[pc].getArgType(2));
+ rt.d_children[2].d_req_type = TypeNode::fromType(pdt[pc].getArgType(1));
+ }
+ }
+ Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk
+ << ", arg = " << arg << "?" << std::endl;
+ if (!rt.empty())
+ {
+ rt.print("sygus-sb-debug");
+ // check if it meets the requirements
+ if (rt.satisfiedBy(d_tds, tnp))
+ {
+ Trace("sygus-sb-debug") << "...success!" << std::endl;
+ Trace("sygus-sb-simple")
+ << " sb-simple : do not consider " << k << " as arg " << arg
+ << " of " << pk << std::endl;
+ // do not need to consider the kind in the search since there are ways to
+ // construct equivalent terms
+ return false;
+ }
+ else
+ {
+ Trace("sygus-sb-debug") << "...failed." << std::endl;
+ }
+ Trace("sygus-sb-debug") << std::endl;
+ }
+ // must consider this kind in the search
+ return true;
+}
+
+bool SygusSimpleSymBreak::considerConst(
+ TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg)
+{
+ const Datatype& pdt = static_cast<DatatypeType>(tnp.toType()).getDatatype();
+ // child grammar-independent
+ if (!considerConst(pdt, tnp, c, pk, arg))
+ {
+ return false;
+ }
+ // this can probably be made child grammar independent
+ int pc = d_tds->getKindConsNum(tnp, pk);
+ if (pdt[pc].getNumArgs() == 2)
+ {
+ Kind ok;
+ int offset;
+ if (d_tutil->hasOffsetArg(pk, arg, offset, ok))
+ {
+ Trace("sygus-sb-simple-debug")
+ << pk << " has offset arg " << ok << " " << offset << std::endl;
+ int ok_arg = d_tds->getKindConsNum(tnp, ok);
+ if (ok_arg != -1)
+ {
+ Trace("sygus-sb-simple-debug")
+ << "...at argument " << ok_arg << std::endl;
+ // other operator be the same type
+ if (d_tds->isTypeMatch(pdt[ok_arg], pdt[arg]))
+ {
+ int status;
+ Node co = d_tutil->getTypeValueOffset(c.getType(), c, offset, status);
+ Trace("sygus-sb-simple-debug")
+ << c << " with offset " << offset << " is " << co
+ << ", status=" << status << std::endl;
+ if (status == 0 && !co.isNull())
+ {
+ if (d_tds->hasConst(tn, co))
+ {
+ Trace("sygus-sb-simple")
+ << " sb-simple : by offset reasoning, do not consider const "
+ << c;
+ Trace("sygus-sb-simple")
+ << " as arg " << arg << " of " << pk << " since we can use "
+ << co << " under " << ok << " " << std::endl;
+ return false;
+ }
+ }
+ }
+ }
+ }
+ }
+ return true;
+}
+
+bool SygusSimpleSymBreak::considerConst(
+ const Datatype& pdt, TypeNode tnp, Node c, Kind pk, int arg)
+{
+ Assert(d_tds->hasKind(tnp, pk));
+ int pc = d_tds->getKindConsNum(tnp, pk);
+ bool ret = true;
+ Trace("sygus-sb-debug") << "Consider sygus const " << c << ", parent = " << pk
+ << ", arg = " << arg << "?" << std::endl;
+ if (d_tutil->isIdempotentArg(c, pk, arg))
+ {
+ if (pdt[pc].getNumArgs() == 2)
+ {
+ int oarg = arg == 0 ? 1 : 0;
+ TypeNode otn = TypeNode::fromType(pdt[pc].getArgType(oarg));
+ if (otn == tnp)
+ {
+ Trace("sygus-sb-simple")
+ << " sb-simple : " << c << " is idempotent arg " << arg << " of "
+ << pk << "..." << std::endl;
+ ret = false;
+ }
+ }
+ }
+ else
+ {
+ Node sc = d_tutil->isSingularArg(c, pk, arg);
+ if (!sc.isNull())
+ {
+ if (d_tds->hasConst(tnp, sc))
+ {
+ Trace("sygus-sb-simple")
+ << " sb-simple : " << c << " is singular arg " << arg << " of "
+ << pk << ", evaluating to " << sc << "..." << std::endl;
+ ret = false;
+ }
+ }
+ }
+ if (ret)
+ {
+ ReqTrie rt;
+ Assert(rt.empty());
+ Node max_c = d_tutil->getTypeMaxValue(c.getType());
+ Node zero_c = d_tutil->getTypeValue(c.getType(), 0);
+ Node one_c = d_tutil->getTypeValue(c.getType(), 1);
+ if (pk == XOR || pk == BITVECTOR_XOR)
+ {
+ if (c == max_c)
+ {
+ rt.d_req_kind = pk == XOR ? NOT : BITVECTOR_NOT;
+ }
+ }
+ else if (pk == ITE)
+ {
+ if (arg == 0)
+ {
+ if (c == max_c)
+ {
+ rt.d_children[1].d_req_type = tnp;
+ }
+ else if (c == zero_c)
+ {
+ rt.d_children[2].d_req_type = tnp;
+ }
+ }
+ }
+ else if (pk == STRING_SUBSTR)
+ {
+ if (c == one_c && arg == 2)
+ {
+ rt.d_req_kind = STRING_CHARAT;
+ rt.d_children[0].d_req_type = TypeNode::fromType(pdt[pc].getArgType(0));
+ rt.d_children[1].d_req_type = TypeNode::fromType(pdt[pc].getArgType(1));
+ }
+ }
+ if (!rt.empty())
+ {
+ // check if satisfied
+ if (rt.satisfiedBy(d_tds, tnp))
+ {
+ Trace("sygus-sb-simple") << " sb-simple : do not consider const " << c
+ << " as arg " << arg << " of " << pk;
+ Trace("sygus-sb-simple") << " in " << pdt.getName() << std::endl;
+ // do not need to consider the constant in the search since there are
+ // ways to construct equivalent terms
+ ret = false;
+ }
+ }
+ }
+ return ret;
+}
+
+int SygusSimpleSymBreak::solveForArgument(TypeNode tn,
+ unsigned cindex,
+ unsigned arg)
+{
+ // we currently do not solve for arguments
+ return -1;
+}
+
+int SygusSimpleSymBreak::getFirstArgOccurrence(const DatatypeConstructor& c,
+ TypeNode tn)
+{
+ for (unsigned i = 0, nargs = c.getNumArgs(); i < nargs; i++)
+ {
+ TypeNode tni = TypeNode::fromType(c.getArgType(i));
+ if (tni == tn)
+ {
+ return i;
+ }
+ }
+ return -1;
+}
+
+} // namespace datatypes
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file sygus_simple_sym.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief Simple symmetry breaking for sygus.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
+#define __CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
+
+#include <map>
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
+
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+
+/** SygusSimpleSymBreak
+ *
+ * This class implements queries that can be queried statically about sygus
+ * grammars, for example, concerning which constructors need not appear at
+ * argument positions of others. This is used by the sygus extension of the
+ * quantifier-free datatypes procedure for adding symmetry breaking lemmas.
+ * We call this class of techniques "simple static symmetry breaking". These
+ * techniques have the advantage over "dynamic symmetry breaking" (blocking
+ * redundant solutions on demand in datatypes_sygus.h) in that we can design
+ * efficient encodings of symmetry breaking constraints, whereas dynamic
+ * symmetry breaking may in the worst case block solutions one by one.
+ */
+class SygusSimpleSymBreak
+{
+ public:
+ SygusSimpleSymBreak(QuantifiersEngine* qe);
+ ~SygusSimpleSymBreak() {}
+ /** consider argument kind
+ *
+ * This method returns false if the arg^th argument of terms of parent kind
+ * pk need not be of kind k. The type tnp is the sygus type of type
+ * containing pk, and tn is the sygus type of the arg^th argument of the
+ * constructor whose builtin kind is pk.
+ *
+ * For example, given grammar:
+ * A -> A + A | 0 | 1 | x | -A
+ * This method will return false for inputs such as:
+ * A, A, -, -, 0 (due to cancelling of double unary minus)
+ * A, A, +, +, 1 (due to commutativity of addition, we can assume all
+ * nested + occurs in the 0^th argument)
+ */
+ bool considerArgKind(TypeNode tn, TypeNode tnp, Kind k, Kind pk, int arg);
+ /** consider constant
+ *
+ * Similar to the above function, this method returns false if the arg^th
+ * argument of terms of parent kind pk need not be the constant c. The type
+ * tnp is the sygus type of type containing pk, and tn is the sygus type of
+ * the arg^th argument of the constructor whose builtin kind is pk.
+ *
+ * For example, given grammar:
+ * A -> B * B | A + A | 0 | 1 | x | -A
+ * B -> 0 | x
+ * This method will return false for inputs such as:
+ * A, A, 0, +, 0 (due to identity of addition with zero)
+ * B, A, 0, *, 0 (due to simplification 0*x --> 0, and 0 is generated by A)
+ */
+ bool considerConst(TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg);
+ /** solve for argument
+ *
+ * If this method returns a non-negative integer n, then all terms at
+ * the arg^th position of the cindex^th constructor of sygus type tnp need
+ * only be of the n^th constructor of that argument.
+ *
+ * For example, given grammar:
+ * A -> A - A | A + A | 0 | 1 | x | y
+ * Say solveForArgument(A, 0, 0)=2. This indicates that all terms of the form
+ * x1-x2 need only be such that x1 is 0.
+ */
+ int solveForArgument(TypeNode tnp, unsigned cindex, unsigned arg);
+
+ private:
+ /** Pointer to the sygus term database */
+ quantifiers::TermDbSygus* d_tds;
+ /** Pointer to the quantifiers term utility */
+ quantifiers::TermUtil* d_tutil;
+ /** return the index of the first argument position of c that has type tn */
+ int getFirstArgOccurrence(const DatatypeConstructor& c, TypeNode tn);
+ /**
+ * Helper function for consider const above, pdt is the datatype of the type
+ * of tnp.
+ */
+ bool considerConst(
+ const Datatype& pdt, TypeNode tnp, Node c, Kind pk, int arg);
+};
+
+} // namespace datatypes
+} // namespace theory
+} // namespace CVC4
+
+#endif /* __CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H */
void TheoryDatatypes::finishInit() {
if( getQuantifiersEngine() && options::ceGuidedInst() ){
- quantifiers::TermDbSygus * tds = getQuantifiersEngine()->getTermDatabaseSygus();
- Assert( tds!=NULL );
- d_sygus_sym_break = new SygusSymBreakNew( this, tds, getSatContext() );
+ d_sygus_sym_break =
+ new SygusSymBreakNew(this, getQuantifiersEngine(), getSatContext());
// do congruence on evaluation functions
d_equalityEngine.addFunctionKind(kind::DT_SYGUS_EVAL);
}
return weight + sum;
}
-class ReqTrie {
-public:
- ReqTrie() : d_req_kind( UNDEFINED_KIND ){}
- std::map< unsigned, ReqTrie > d_children;
- Kind d_req_kind;
- TypeNode d_req_type;
- Node d_req_const;
- void print( const char * c, int indent = 0 ){
- if( d_req_kind!=UNDEFINED_KIND ){
- Trace(c) << d_req_kind << " ";
- }else if( !d_req_type.isNull() ){
- Trace(c) << d_req_type;
- }else if( !d_req_const.isNull() ){
- Trace(c) << d_req_const;
- }else{
- Trace(c) << "_";
- }
- Trace(c) << std::endl;
- for( std::map< unsigned, ReqTrie >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
- for( int i=0; i<=indent; i++ ) { Trace(c) << " "; }
- Trace(c) << it->first << " : ";
- it->second.print( c, indent+1 );
- }
- }
- bool satisfiedBy( quantifiers::TermDbSygus * tdb, TypeNode tn ){
- if( !d_req_const.isNull() ){
- if( !tdb->hasConst( tn, d_req_const ) ){
- return false;
- }
- }
- if( !d_req_type.isNull() ){
- Trace("sygus-sb-debug") << "- check if " << tn << " is type "
- << d_req_type << std::endl;
- if( tn!=d_req_type ){
- return false;
- }
- }
- if( d_req_kind!=UNDEFINED_KIND ){
- Trace("sygus-sb-debug") << "- check if " << tn << " has " << d_req_kind
- << std::endl;
- std::vector<TypeNode> argts;
- if (tdb->canConstructKind(tn, d_req_kind, argts))
- {
- bool ret = true;
- for( std::map< unsigned, ReqTrie >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
- if (it->first < argts.size())
- {
- TypeNode tnc = argts[it->first];
- if( !it->second.satisfiedBy( tdb, tnc ) ){
- return false;
- }
- }else{
- return false;
- }
- }
- if( !ret ){
- return false;
- }
- }else{
- return false;
- }
- }
- return true;
- }
- bool empty()
- {
- return d_req_kind == UNDEFINED_KIND && d_req_const.isNull()
- && d_req_type.isNull() && d_children.empty();
- }
-};
-
-//this function gets all easy redundant cases, before consulting rewriters
-bool TermDbSygus::considerArgKind( TypeNode tn, TypeNode tnp, Kind k, Kind pk, int arg ) {
- const Datatype& pdt = ((DatatypeType)(tnp).toType()).getDatatype();
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- Assert( hasKind( tn, k ) );
- Assert( hasKind( tnp, pk ) );
- Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk
- << ", arg = " << arg << " in " << tnp << "?"
- << std::endl;
- int c = getKindConsNum( tn, k );
- int pc = getKindConsNum( tnp, pk );
- //check for associativity
- if (k == pk && quantifiers::TermUtil::isAssoc(k))
- {
- // if the operator is associative, then a repeated occurrence should only
- // occur in the leftmost argument position
- int firstArg = getFirstArgOccurrence(pdt[pc], tn);
- Assert(firstArg != -1);
- if (arg == firstArg)
- {
- return true;
- }
- // the argument types of the child must be the parent's type
- for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
- {
- TypeNode tn = TypeNode::fromType(dt[c].getArgType(i));
- if (tn != tnp)
- {
- return true;
- }
- }
- Trace("sygus-sb-simple")
- << " sb-simple : do not consider " << k << " at child arg " << arg
- << " of " << k
- << " since it is associative, with first arg = " << firstArg
- << std::endl;
- return false;
- }
- //describes the shape of an alternate term to construct
- // we check whether this term is in the sygus grammar below
- ReqTrie rt;
- Assert( rt.empty() );
-
- //construct rt by cases
- if( pk==NOT || pk==BITVECTOR_NOT || pk==UMINUS || pk==BITVECTOR_NEG ){
- //negation normal form
- if( pk==k ){
- rt.d_req_type = getArgType( dt[c], 0 );
- }else{
- Kind reqk = UNDEFINED_KIND; //required kind for all children
- std::map< unsigned, Kind > reqkc; //required kind for some children
- if( pk==NOT ){
- if( k==AND ) {
- rt.d_req_kind = OR;reqk = NOT;
- }else if( k==OR ){
- rt.d_req_kind = AND;reqk = NOT;
- //AJR : eliminate this if we eliminate xor
- }else if( k==EQUAL ) {
- rt.d_req_kind = XOR;
- }else if( k==XOR ) {
- rt.d_req_kind = EQUAL;
- }else if( k==ITE ){
- rt.d_req_kind = ITE;reqkc[1] = NOT;reqkc[2] = NOT;
- rt.d_children[0].d_req_type = getArgType( dt[c], 0 );
- }else if( k==LEQ || k==GT ){
- // (not (~ x y)) -----> (~ (+ y 1) x)
- rt.d_req_kind = k;
- rt.d_children[0].d_req_kind = PLUS;
- rt.d_children[0].d_children[0].d_req_type = getArgType( dt[c], 1 );
- rt.d_children[0].d_children[1].d_req_const = NodeManager::currentNM()->mkConst( Rational( 1 ) );
- rt.d_children[1].d_req_type = getArgType( dt[c], 0 );
- //TODO: other possibilities?
- }else if( k==LT || k==GEQ ){
- // (not (~ x y)) -----> (~ y (+ x 1))
- rt.d_req_kind = k;
- rt.d_children[0].d_req_type = getArgType( dt[c], 1 );
- rt.d_children[1].d_req_kind = PLUS;
- rt.d_children[1].d_children[0].d_req_type = getArgType( dt[c], 0 );
- rt.d_children[1].d_children[1].d_req_const = NodeManager::currentNM()->mkConst( Rational( 1 ) );
- }
- }else if( pk==BITVECTOR_NOT ){
- if( k==BITVECTOR_AND ) {
- rt.d_req_kind = BITVECTOR_OR;reqk = BITVECTOR_NOT;
- }else if( k==BITVECTOR_OR ){
- rt.d_req_kind = BITVECTOR_AND;reqk = BITVECTOR_NOT;
- }else if( k==BITVECTOR_XNOR ) {
- rt.d_req_kind = BITVECTOR_XOR;
- }else if( k==BITVECTOR_XOR ) {
- rt.d_req_kind = BITVECTOR_XNOR;
- }
- }else if( pk==UMINUS ){
- if( k==PLUS ){
- rt.d_req_kind = PLUS;reqk = UMINUS;
- }
- }else if( pk==BITVECTOR_NEG ){
- if( k==PLUS ){
- rt.d_req_kind = PLUS;reqk = BITVECTOR_NEG;
- }
- }
- if( !rt.empty() && ( reqk!=UNDEFINED_KIND || !reqkc.empty() ) ){
- int pcr = getKindConsNum( tnp, rt.d_req_kind );
- if( pcr!=-1 ){
- Assert( pcr<(int)pdt.getNumConstructors() );
- //must have same number of arguments
- if( pdt[pcr].getNumArgs()==dt[c].getNumArgs() ){
- for( unsigned i=0; i<pdt[pcr].getNumArgs(); i++ ){
- Kind rk = reqk;
- if( reqk==UNDEFINED_KIND ){
- std::map< unsigned, Kind >::iterator itr = reqkc.find( i );
- if( itr!=reqkc.end() ){
- rk = itr->second;
- }
- }
- if( rk!=UNDEFINED_KIND ){
- rt.d_children[i].d_req_kind = rk;
- rt.d_children[i].d_children[0].d_req_type = getArgType( dt[c], i );
- }
- }
- }
- }
- }
- }
- }else if( k==MINUS || k==BITVECTOR_SUB ){
- if( pk==EQUAL ||
- pk==MINUS || pk==BITVECTOR_SUB ||
- pk==LEQ || pk==LT || pk==GEQ || pk==GT ){
- int oarg = arg==0 ? 1 : 0;
- // (~ x (- y z)) ----> (~ (+ x z) y)
- // (~ (- y z) x) ----> (~ y (+ x z))
- rt.d_req_kind = pk;
- rt.d_children[arg].d_req_type = getArgType( dt[c], 0 );
- rt.d_children[oarg].d_req_kind = k==MINUS ? PLUS : BITVECTOR_PLUS;
- rt.d_children[oarg].d_children[0].d_req_type = getArgType( pdt[pc], oarg );
- rt.d_children[oarg].d_children[1].d_req_type = getArgType( dt[c], 1 );
- }else if( pk==PLUS || pk==BITVECTOR_PLUS ){
- // (+ x (- y z)) -----> (- (+ x y) z)
- // (+ (- y z) x) -----> (- (+ x y) z)
- rt.d_req_kind = pk==PLUS ? MINUS : BITVECTOR_SUB;
- int oarg = arg==0 ? 1 : 0;
- rt.d_children[0].d_req_kind = pk;
- rt.d_children[0].d_children[0].d_req_type = getArgType( pdt[pc], oarg );
- rt.d_children[0].d_children[1].d_req_type = getArgType( dt[c], 0 );
- rt.d_children[1].d_req_type = getArgType( dt[c], 1 );
- // TODO : this is subsumbed by solving for MINUS
- }
- }else if( k==ITE ){
- if( pk!=ITE ){
- // (o X (ite y z w) X') -----> (ite y (o X z X') (o X w X'))
- rt.d_req_kind = ITE;
- rt.d_children[0].d_req_type = getArgType( dt[c], 0 );
- unsigned n_args = pdt[pc].getNumArgs();
- for( unsigned r=1; r<=2; r++ ){
- rt.d_children[r].d_req_kind = pk;
- for( unsigned q=0; q<n_args; q++ ){
- if( (int)q==arg ){
- rt.d_children[r].d_children[q].d_req_type = getArgType( dt[c], r );
- }else{
- rt.d_children[r].d_children[q].d_req_type = getArgType( pdt[pc], q );
- }
- }
- }
- //TODO: this increases term size but is probably a good idea
- }
- }else if( k==NOT ){
- if( pk==ITE ){
- // (ite (not y) z w) -----> (ite y w z)
- rt.d_req_kind = ITE;
- rt.d_children[0].d_req_type = getArgType( dt[c], 0 );
- rt.d_children[1].d_req_type = getArgType( pdt[pc], 2 );
- rt.d_children[2].d_req_type = getArgType( pdt[pc], 1 );
- }
- }
- Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk << ", arg = " << arg << "?" << std::endl;
- if( !rt.empty() ){
- rt.print("sygus-sb-debug");
- //check if it meets the requirements
- if( rt.satisfiedBy( this, tnp ) ){
- Trace("sygus-sb-debug") << "...success!" << std::endl;
- Trace("sygus-sb-simple") << " sb-simple : do not consider " << k << " as arg " << arg << " of " << pk << std::endl;
- //do not need to consider the kind in the search since there are ways to construct equivalent terms
- return false;
- }else{
- Trace("sygus-sb-debug") << "...failed." << std::endl;
- }
- Trace("sygus-sb-debug") << std::endl;
- }
- //must consider this kind in the search
- return true;
-}
-
-bool TermDbSygus::considerConst( TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg ) {
- const Datatype& pdt = ((DatatypeType)(tnp).toType()).getDatatype();
- // child grammar-independent
- if( !considerConst( pdt, tnp, c, pk, arg ) ){
- return false;
- }
- // TODO : this can probably be made child grammar independent
- int pc = getKindConsNum( tnp, pk );
- if( pdt[pc].getNumArgs()==2 ){
- Kind ok;
- int offset;
- if (d_quantEngine->getTermUtil()->hasOffsetArg(pk, arg, offset, ok))
- {
- Trace("sygus-sb-simple-debug") << pk << " has offset arg " << ok << " " << offset << std::endl;
- int ok_arg = getKindConsNum( tnp, ok );
- if( ok_arg!=-1 ){
- Trace("sygus-sb-simple-debug") << "...at argument " << ok_arg << std::endl;
- //other operator be the same type
- if( isTypeMatch( pdt[ok_arg], pdt[arg] ) ){
- int status;
- Node co = d_quantEngine->getTermUtil()->getTypeValueOffset(
- c.getType(), c, offset, status);
- Trace("sygus-sb-simple-debug") << c << " with offset " << offset << " is " << co << ", status=" << status << std::endl;
- if( status==0 && !co.isNull() ){
- if( hasConst( tn, co ) ){
- Trace("sygus-sb-simple") << " sb-simple : by offset reasoning, do not consider const " << c;
- Trace("sygus-sb-simple") << " as arg " << arg << " of " << pk << " since we can use " << co << " under " << ok << " " << std::endl;
- return false;
- }
- }
- }
- }
- }
- }
- return true;
-}
-
-bool TermDbSygus::considerConst( const Datatype& pdt, TypeNode tnp, Node c, Kind pk, int arg ) {
- Assert( hasKind( tnp, pk ) );
- int pc = getKindConsNum( tnp, pk );
- bool ret = true;
- Trace("sygus-sb-debug") << "Consider sygus const " << c << ", parent = " << pk << ", arg = " << arg << "?" << std::endl;
- if (d_quantEngine->getTermUtil()->isIdempotentArg(c, pk, arg))
- {
- if( pdt[pc].getNumArgs()==2 ){
- int oarg = arg==0 ? 1 : 0;
- TypeNode otn = TypeNode::fromType( ((SelectorType)pdt[pc][oarg].getType()).getRangeType() );
- if( otn==tnp ){
- Trace("sygus-sb-simple") << " sb-simple : " << c << " is idempotent arg " << arg << " of " << pk << "..." << std::endl;
- ret = false;
- }
- }
- }else{
- Node sc = d_quantEngine->getTermUtil()->isSingularArg(c, pk, arg);
- if( !sc.isNull() ){
- if( hasConst( tnp, sc ) ){
- Trace("sygus-sb-simple") << " sb-simple : " << c << " is singular arg " << arg << " of " << pk << ", evaluating to " << sc << "..." << std::endl;
- ret = false;
- }
- }
- }
- if( ret ){
- ReqTrie rt;
- Assert( rt.empty() );
- Node max_c = d_quantEngine->getTermUtil()->getTypeMaxValue(c.getType());
- Node zero_c = d_quantEngine->getTermUtil()->getTypeValue(c.getType(), 0);
- Node one_c = d_quantEngine->getTermUtil()->getTypeValue(c.getType(), 1);
- if( pk==XOR || pk==BITVECTOR_XOR ){
- if( c==max_c ){
- rt.d_req_kind = pk==XOR ? NOT : BITVECTOR_NOT;
- }
- }else if( pk==ITE ){
- if( arg==0 ){
- if( c==max_c ){
- rt.d_children[1].d_req_type = tnp;
- }
- else if (c == zero_c)
- {
- rt.d_children[2].d_req_type = tnp;
- }
- }
- }else if( pk==STRING_SUBSTR ){
- if (c == one_c && arg == 2)
- {
- rt.d_req_kind = STRING_CHARAT;
- rt.d_children[0].d_req_type = getArgType( pdt[pc], 0 );
- rt.d_children[1].d_req_type = getArgType( pdt[pc], 1 );
- }
- }
- if( !rt.empty() ){
- //check if satisfied
- if( rt.satisfiedBy( this, tnp ) ){
- Trace("sygus-sb-simple") << " sb-simple : do not consider const " << c << " as arg " << arg << " of " << pk;
- Trace("sygus-sb-simple") << " in " << ((DatatypeType)tnp.toType()).getDatatype().getName() << std::endl;
- //do not need to consider the constant in the search since there are ways to construct equivalent terms
- ret = false;
- }
- }
- }
- // TODO : cache?
- return ret;
-}
-
-int TermDbSygus::solveForArgument( TypeNode tn, unsigned cindex, unsigned arg ) {
- // FIXME
- return -1; // TODO : if using, modify considerArgKind above
- Assert( isRegistered( tn ) );
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- Assert( cindex<dt.getNumConstructors() );
- Assert( arg<dt[cindex].getNumArgs() );
- Kind nk = getConsNumKind( tn, cindex );
- TypeNode tnc = getArgType( dt[cindex], arg );
- const Datatype& cdt = ((DatatypeType)(tnc).toType()).getDatatype();
-
- ReqTrie rt;
- Assert( rt.empty() );
- int solve_ret = -1;
- if( nk==MINUS || nk==BITVECTOR_SUB ){
- if( dt[cindex].getNumArgs()==2 && arg==0 ){
- TypeNode tnco = getArgType( dt[cindex], 1 );
- Node builtin = d_quantEngine->getTermUtil()->getTypeValue(
- sygusToBuiltinType(tnc), 0);
- solve_ret = getConstConsNum( tn, builtin );
- if( solve_ret!=-1 ){
- // t - s -----> ( 0 - s ) + t
- rt.d_req_kind = nk == MINUS ? PLUS : BITVECTOR_PLUS;
- rt.d_children[0].d_req_type = tn; // avoid?
- rt.d_children[0].d_req_kind = nk;
- rt.d_children[0].d_children[0].d_req_const = builtin;
- rt.d_children[0].d_children[0].d_req_type = tnco;
- rt.d_children[1].d_req_type = tnc;
- // TODO : this can be made more general for multiple type grammars to remove MINUS entirely
- }
- }
- }
-
- if( !rt.empty() ){
- Assert( solve_ret>=0 );
- Assert( solve_ret<=(int)cdt.getNumConstructors() );
- //check if satisfied
- if( rt.satisfiedBy( this, tn ) ){
- Trace("sygus-sb-simple") << " sb-simple : ONLY consider " << cdt[solve_ret].getSygusOp() << " as arg " << arg << " of " << nk;
- Trace("sygus-sb-simple") << " in " << ((DatatypeType)tn.toType()).getDatatype().getName() << std::endl;
- return solve_ret;
- }
- }
-
- return -1;
-}
-
void TermDbSygus::registerSygusType( TypeNode tn ) {
std::map< TypeNode, TypeNode >::iterator itr = d_register.find( tn );
if( itr==d_register.end() ){
static_cast<SelectorType>(c[i].getType()).getRangeType());
}
-/** get first occurrence */
-int TermDbSygus::getFirstArgOccurrence( const DatatypeConstructor& c, TypeNode tn ) {
- for( unsigned i=0; i<c.getNumArgs(); i++ ){
- TypeNode tni = getArgType( c, i );
- if( tni==tn ){
- return i;
- }
- }
- return -1;
-}
-
bool TermDbSygus::isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 ) {
if( c1.getNumArgs()!=c2.getNumArgs() ){
return false;
}
}
-Node TermDbSygus::getSemanticSkolem( TypeNode tn, Node n, bool doMk ){
- std::map< Node, Node >::iterator its = d_semantic_skolem[tn].find( n );
- if( its!=d_semantic_skolem[tn].end() ){
- return its->second;
- }else if( doMk ){
- Node ss = NodeManager::currentNM()->mkSkolem( "sem", tn, "semantic skolem for sygus" );
- d_semantic_skolem[tn][n] = ss;
- return ss;
- }else{
- return Node::null();
- }
-}
-
bool TermDbSygus::involvesDivByZero( Node n, std::map< Node, bool >& visited ){
if( visited.find( n )==visited.end() ){
visited[n] = true;
bool isConstArg( TypeNode tn, int i );
/** get arg type */
TypeNode getArgType(const DatatypeConstructor& c, unsigned i) const;
- /** get first occurrence */
- int getFirstArgOccurrence( const DatatypeConstructor& c, TypeNode tn );
/** is type match */
bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 );
/**
/** get comparison kind */
Kind getComparisonKind( TypeNode tn );
Kind getPlusKind( TypeNode tn, bool is_neg = false );
- // get semantic skolem for n (a sygus term whose builtin version is n)
- Node getSemanticSkolem( TypeNode tn, Node n, bool doMk = true );
/** involves div-by-zero */
bool involvesDivByZero( Node n );
/** get anchor */
static Node getAnchor( Node n );
static unsigned getAnchorDepth( Node n );
-
-public: // for symmetry breaking
- bool considerArgKind( TypeNode tn, TypeNode tnp, Kind k, Kind pk, int arg );
- bool considerConst( TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg );
- bool considerConst( const Datatype& pdt, TypeNode tnp, Node c, Kind pk, int arg );
- int solveForArgument( TypeNode tnp, unsigned cindex, unsigned arg );
public:
/** unfold
projects / cvc5.git / commitdiff