From da756247012b6934999e9e66b8797b3655a01764 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 7 Aug 2018 23:03:57 -0500 Subject: [PATCH] Document/refactor datatypes sygus simple symmetry breaking (#2233) --- src/Makefile.am | 2 + src/theory/datatypes/datatypes_sygus.cpp | 14 +- src/theory/datatypes/datatypes_sygus.h | 5 +- src/theory/datatypes/sygus_simple_sym.cpp | 594 ++++++++++++++++++ src/theory/datatypes/sygus_simple_sym.h | 107 ++++ src/theory/datatypes/theory_datatypes.cpp | 5 +- .../quantifiers/sygus/term_database_sygus.cpp | 435 ------------- .../quantifiers/sygus/term_database_sygus.h | 10 - 8 files changed, 717 insertions(+), 455 deletions(-) create mode 100644 src/theory/datatypes/sygus_simple_sym.cpp create mode 100644 src/theory/datatypes/sygus_simple_sym.h diff --git a/src/Makefile.am b/src/Makefile.am index 677b99d9a..c2a620f57 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -370,6 +370,8 @@ libcvc4_la_SOURCES = \ 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 \ diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index d95a5763c..aea449fd1 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -35,14 +35,16 @@ using namespace CVC4::theory; 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); } @@ -481,7 +483,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn, std::map 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; @@ -622,7 +624,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn, { 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 { @@ -632,7 +634,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn, 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 diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index 5f6ca935d..c5f3fe560 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -29,6 +29,7 @@ #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" @@ -60,7 +61,7 @@ class SygusSymBreakNew public: SygusSymBreakNew(TheoryDatatypes* td, - quantifiers::TermDbSygus* tds, + QuantifiersEngine* qe, context::Context* c); ~SygusSymBreakNew(); /** @@ -117,6 +118,8 @@ class 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 diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp new file mode 100644 index 000000000..4aef1231c --- /dev/null +++ b/src/theory/datatypes/sygus_simple_sym.cpp @@ -0,0 +1,594 @@ +/********************* */ +/*! \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 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::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 argts; + if (tdb->canConstructKind(tn, d_req_kind, argts)) + { + bool ret = true; + for (std::map::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 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(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::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(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 diff --git a/src/theory/datatypes/sygus_simple_sym.h b/src/theory/datatypes/sygus_simple_sym.h new file mode 100644 index 000000000..7fb7f4653 --- /dev/null +++ b/src/theory/datatypes/sygus_simple_sym.h @@ -0,0 +1,107 @@ +/********************* */ +/*! \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 +#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 */ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index cf690af57..f886c6d3f 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -540,9 +540,8 @@ void TheoryDatatypes::preRegisterTerm(TNode n) { 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); } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 54e731694..64adea6c5 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -322,417 +322,6 @@ unsigned TermDbSygus::getSygusTermSize( Node n ){ 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 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::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 (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( cindexgetTermUtil()->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() ){ @@ -1260,17 +849,6 @@ TypeNode TermDbSygus::getArgType(const DatatypeConstructor& c, unsigned i) const static_cast(c[i].getType()).getRangeType()); } -/** get first occurrence */ -int TermDbSygus::getFirstArgOccurrence( const DatatypeConstructor& c, TypeNode tn ) { - for( unsigned i=0; i::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; diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 3631ee520..fee556cf8 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -378,8 +378,6 @@ class TermDbSygus { 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 ); /** @@ -431,19 +429,11 @@ class TermDbSygus { /** 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 -- 2.30.2