theory/quantifiers/sygus_grammar_cons.h \
theory/quantifiers/sygus_grammar_norm.cpp \
theory/quantifiers/sygus_grammar_norm.h \
+ theory/quantifiers/sygus_grammar_red.cpp \
+ theory/quantifiers/sygus_grammar_red.h \
theory/quantifiers/sygus_process_conj.cpp \
theory/quantifiers/sygus_process_conj.h \
theory/quantifiers/sygus_sampler.cpp \
option sygusMinGrammar --sygus-min-grammar bool :default true
statically minimize sygus grammars
-option sygusMinGrammarAgg --sygus-min-grammar-agg bool :default false
- aggressively minimize sygus grammars
option sygusAddConstGrammar --sygus-add-const-grammar bool :default true
statically add constants appearing in conjecture to grammars
option sygusGrammarNorm --sygus-grammar-norm bool :default false
#endif
}
+Node DatatypesRewriter::mkSplit(Node n, const Datatype& dt)
+{
+ std::vector<Node> splits;
+ for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+ {
+ Node test = mkTester(n, i, dt);
+ splits.push_back(test);
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ return splits.size() == 1 ? splits[0] : nm->mkNode(kind::OR, splits);
+}
+
bool DatatypesRewriter::isNullaryApplyConstructor(Node n)
{
Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
static int isTester(Node n);
/** make tester is-C( n ), where C is the i^{th} constructor of dt */
static Node mkTester(Node n, int i, const Datatype& dt);
+ /** make tester split
+ *
+ * Returns the formula (OR is-C1( n ) ... is-Ck( n ) ), where C1...Ck
+ * are the constructors of n's type (dt).
+ */
+ static Node mkSplit(Node n, const Datatype& dt);
/** returns true iff n is a constructor term with no datatype children */
static bool isNullaryApplyConstructor(Node n);
/** returns true iff c is a constructor with no datatype children */
using namespace CVC4::theory;
using namespace CVC4::theory::datatypes;
-Node SygusSplitNew::getSygusSplit( quantifiers::TermDbSygus * tds, Node n, const Datatype& dt ) {
- TypeNode tnn = n.getType();
- tds->registerSygusType( tnn );
- std::vector< Node > curr_splits;
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- Trace("sygus-split-debug2") << "Add split " << n << " : constructor " << dt[i].getName() << " : ";
- if( !tds->isGenericRedundant( tnn, i ) ){
- std::vector< Node > test_c;
- test_c.push_back( DatatypesRewriter::mkTester( n, i, dt ) );
- Node test = test_c.size()==1 ? test_c[0] : NodeManager::currentNM()->mkNode( AND, test_c );
- curr_splits.push_back( test );
- Trace("sygus-split-debug2") << "SUCCESS" << std::endl;
- Trace("sygus-split-debug") << "Disjunct #" << curr_splits.size() << " : " << test << std::endl;
- }else{
- Trace("sygus-split-debug2") << "redundant operator" << std::endl;
- }
- }
- Assert( !curr_splits.empty() );
- return curr_splits.size()==1 ? curr_splits[0] : NodeManager::currentNM()->mkNode( OR, curr_splits );
-
-}
-
-void SygusSplitNew::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits, std::vector< Node >& lemmas ) {
- Assert( dt.isSygus() );
- if( d_splits.find( n )==d_splits.end() ){
- Trace("sygus-split") << "Get sygus splits " << n << std::endl;
- Node split = getSygusSplit( d_tds, n, dt );
- Assert( !split.isNull() );
- d_splits[n].push_back( split );
- }
- //copy to splits
- splits.insert( splits.end(), d_splits[n].begin(), d_splits[n].end() );
-}
-
SygusSymBreakNew::SygusSymBreakNew(TheoryDatatypes* td,
quantifiers::TermDbSygus* tds,
context::Context* c)
}
Node SygusSymBreakNew::getTermOrderPredicate( Node n1, Node n2 ) {
+ NodeManager* nm = NodeManager::currentNM();
std::vector< Node > comm_disj;
// (1) size of left is greater than size of right
- Node sz_less = NodeManager::currentNM()->mkNode( GT, NodeManager::currentNM()->mkNode( DT_SIZE, n1 ),
- NodeManager::currentNM()->mkNode( DT_SIZE, n2 ) );
+ Node sz_less =
+ nm->mkNode(GT, nm->mkNode(DT_SIZE, n1), nm->mkNode(DT_SIZE, n2));
comm_disj.push_back( sz_less );
// (2) ...or sizes are equal and first child is less by term order
- std::vector< Node > sz_eq_cases;
- Node sz_eq = NodeManager::currentNM()->mkNode( EQUAL, NodeManager::currentNM()->mkNode( DT_SIZE, n1 ),
- NodeManager::currentNM()->mkNode( DT_SIZE, n2 ) );
+ std::vector<Node> sz_eq_cases;
+ Node sz_eq =
+ nm->mkNode(EQUAL, nm->mkNode(DT_SIZE, n1), nm->mkNode(DT_SIZE, n2));
sz_eq_cases.push_back( sz_eq );
if( options::sygusOpt1() ){
TypeNode tnc = n1.getType();
const Datatype& cdt = ((DatatypeType)(tnc).toType()).getDatatype();
for( unsigned j=0; j<cdt.getNumConstructors(); j++ ){
- if( !d_tds->isGenericRedundant( tnc, j ) ){
- std::vector< Node > case_conj;
- for( unsigned k=0; k<j; k++ ){
- if( !d_tds->isGenericRedundant( tnc, k ) ){
- case_conj.push_back( DatatypesRewriter::mkTester( n2, k, cdt ).negate() );
- }
- }
- if( !case_conj.empty() ){
- Node corder = NodeManager::currentNM()->mkNode( kind::OR, DatatypesRewriter::mkTester( n1, j, cdt ).negate(),
- case_conj.size()==1 ? case_conj[0] : NodeManager::currentNM()->mkNode( kind::AND, case_conj ) );
- sz_eq_cases.push_back( corder );
- }
+ std::vector<Node> case_conj;
+ for (unsigned k = 0; k < j; k++)
+ {
+ case_conj.push_back(DatatypesRewriter::mkTester(n2, k, cdt).negate());
+ }
+ if (!case_conj.empty())
+ {
+ Node corder = nm->mkNode(
+ kind::OR,
+ DatatypesRewriter::mkTester(n1, j, cdt).negate(),
+ case_conj.size() == 1 ? case_conj[0]
+ : nm->mkNode(kind::AND, case_conj));
+ sz_eq_cases.push_back(corder);
}
}
}
- Node sz_eqc = sz_eq_cases.size()==1 ? sz_eq_cases[0] : NodeManager::currentNM()->mkNode( kind::AND, sz_eq_cases );
+ Node sz_eqc = sz_eq_cases.size() == 1 ? sz_eq_cases[0]
+ : nm->mkNode(kind::AND, sz_eq_cases);
comm_disj.push_back( sz_eqc );
-
- return NodeManager::currentNM()->mkNode( kind::OR, comm_disj );
+
+ return nm->mkNode(kind::OR, comm_disj);
}
void SygusSymBreakNew::registerTerm( Node n, std::vector< Node >& lemmas ) {
std::vector< Node > disj;
bool excl = false;
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- if( !d_tds->isGenericRedundant( ntn, i ) ){
- int sindexi = dt[i].getSelectorIndexInternal( selExpr );
- if( sindexi!=-1 ){
- disj.push_back( DatatypesRewriter::mkTester( n[0], i, dt ) );
- }else{
- excl = true;
- }
+ int sindexi = dt[i].getSelectorIndexInternal(selExpr);
+ if (sindexi != -1)
+ {
+ disj.push_back(DatatypesRewriter::mkTester(n[0], i, dt));
+ }
+ else
+ {
+ excl = true;
}
}
Assert( !disj.empty() );
TypeNode tnc = nc.getType();
const Datatype& cdt = ((DatatypeType)(tnc).toType()).getDatatype();
for( unsigned k=0; k<cdt.getNumConstructors(); k++ ){
- // if not already generic redundant
- if( !d_tds->isGenericRedundant( tnc, k ) ){
- Kind nck = d_tds->getConsNumKind( tnc, k );
- bool red = false;
- //check if the argument is redundant
- if( nck!=UNDEFINED_KIND ){
- Trace("sygus-sb-simple-debug") << " argument " << j << " " << k << " is : " << nck << std::endl;
- red = !d_tds->considerArgKind( tnc, tn, nck, nk, j );
+ Kind nck = d_tds->getConsNumKind(tnc, k);
+ bool red = false;
+ // check if the argument is redundant
+ if (nck != UNDEFINED_KIND)
+ {
+ Trace("sygus-sb-simple-debug")
+ << " argument " << j << " " << k << " is : " << nck
+ << std::endl;
+ red = !d_tds->considerArgKind(tnc, tn, nck, nk, j);
+ }
+ else
+ {
+ Node cc = d_tds->getConsNumConst(tnc, k);
+ if (!cc.isNull())
+ {
+ Trace("sygus-sb-simple-debug")
+ << " argument " << j << " " << k
+ << " is constant : " << cc << std::endl;
+ red = !d_tds->considerConst(tnc, tn, cc, nk, j);
}else{
- Node cc = d_tds->getConsNumConst( tnc, k );
- if( !cc.isNull() ){
- Trace("sygus-sb-simple-debug") << " argument " << j << " " << k << " is constant : " << cc << std::endl;
- red = !d_tds->considerConst( tnc, tn, cc, nk, j );
- }else{
- //defined function?
- }
- }
- if( red ){
- Trace("sygus-sb-simple-debug") << " ...redundant." << std::endl;
- sbp_conj.push_back( DatatypesRewriter::mkTester( nc, k, cdt ).negate() );
+ // defined function?
}
}
+ if (red)
+ {
+ Trace("sygus-sb-simple-debug")
+ << " ...redundant." << std::endl;
+ sbp_conj.push_back(
+ DatatypesRewriter::mkTester(nc, k, cdt).negate());
+ }
}
}
}
}
}
-void SygusSymBreakNew::getPossibleCons( const Datatype& dt, TypeNode tn, std::vector< bool >& pcons ) {
- Assert( pcons.size()==dt.getNumConstructors() );
- d_tds->registerSygusType( tn );
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- if( d_tds->isGenericRedundant( tn, i ) ){
- pcons[i] = false;
- }
- }
-}
-
bool SygusSymBreakNew::debugTesters( Node n, Node vn, int ind, std::vector< Node >& lemmas ) {
Assert( vn.getKind()==kind::APPLY_CONSTRUCTOR );
if( Trace.isOn("sygus-sb-warn") ){
Trace("sygus-sb-warn") << "- has tester : " << tst << " : " << ( hastst ? "true" : "false" );
Trace("sygus-sb-warn") << ", value=" << tstrep << std::endl;
if( !hastst ){
- Node split = SygusSplitNew::getSygusSplit( d_tds, n, dt );
+ Node split = DatatypesRewriter::mkSplit(n, dt);
Assert( !split.isNull() );
lemmas.push_back( split );
return false;
class TheoryDatatypes;
-class SygusSplitNew
-{
-private:
- quantifiers::TermDbSygus * d_tds;
- std::map< Node, std::vector< Node > > d_splits;
-public:
- SygusSplitNew( quantifiers::TermDbSygus * tds ) : d_tds( tds ){}
- virtual ~SygusSplitNew(){}
- /** get sygus splits */
- void getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits, std::vector< Node >& lemmas );
- static Node getSygusSplit( quantifiers::TermDbSygus * tds, Node n, const Datatype& dt );
-};
-
class SygusSymBreakNew
{
private:
void assertFact( Node n, bool polarity, std::vector< Node >& lemmas );
void preRegisterTerm( TNode n, std::vector< Node >& lemmas );
void check( std::vector< Node >& lemmas );
- void getPossibleCons( const Datatype& dt, TypeNode tn, std::vector< bool >& pcons );
public:
Node getNextDecisionRequest( unsigned& priority, std::vector< Node >& lemmas );
};
d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
d_dtfCounter = 0;
- d_sygus_split = NULL;
d_sygus_sym_break = NULL;
}
Assert(current != NULL);
delete current;
}
- delete d_sygus_split;
delete d_sygus_sym_break;
}
d_out->requirePhase( test, true );
}else{
Trace("dt-split") << "*************Split for constructors on " << n << endl;
- std::vector< Node > children;
- if( dt.isSygus() && d_sygus_split ){
- Trace("dt-split") << "DtSygus : split on " << n
- << std::endl;
- std::vector< Node > lemmas;
- d_sygus_split->getSygusSplits( n, dt, children, lemmas );
- Trace("dt-split") << "Finished compute split, returned "
- << lemmas.size() << " lemmas."
- << std::endl;
- for( unsigned i=0; i<lemmas.size(); i++ ){
- Trace("dt-lemma-sygus") << "Dt sygus lemma : " << lemmas[i] << std::endl;
- doSendLemma( lemmas[i] );
- }
- }else{
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- Node test = DatatypesRewriter::mkTester( n, i, dt );
- children.push_back( test );
- }
- }
- Assert( !children.empty() );
- Node lemma = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::OR, children );
+ Node lemma = DatatypesRewriter::mkSplit(n, dt);
Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl;
//doSendLemma( lemma );
d_out->lemma( lemma, false, false, true );
if( getQuantifiersEngine() && options::ceGuidedInst() ){
quantifiers::TermDbSygus * tds = getQuantifiersEngine()->getTermDatabaseSygus();
Assert( tds!=NULL );
- d_sygus_split = new SygusSplitNew( tds );
d_sygus_sym_break = new SygusSymBreakNew( this, tds, getSatContext() );
}
}
Assert( tindex!=-1 );
pcons[ tindex ] = false;
}
- //further limit the possibilities based on grammar minimization
- if( d_sygus_sym_break && dt.isSygus() ){
- d_sygus_sym_break->getPossibleCons( dt, tn, pcons );
- }
}
}
}
break;
}
}
- Assert( dt.isSygus() || testerIndex!=-1 );
+ Assert(testerIndex != -1);
//we must explain why each term in the set of testers for this equivalence class is equal
std::vector< Node > eq_terms;
NodeBuilder<> nb(kind::AND);
bool areCareDisequal( TNode x, TNode y );
TNode getRepresentative( TNode a );
private:
- /** sygus utilities */
- SygusSplitNew * d_sygus_split;
- SygusSymBreakNew * d_sygus_sym_break;
+ /** sygus symmetry breaking utility */
+ SygusSymBreakNew* d_sygus_sym_break;
+
public:
Node getNextDecisionRequest( unsigned& priority );
};/* class TheoryDatatypes */
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/quantifiers/ce_guided_conjecture.h"
+#include "theory/quantifiers/sygus_grammar_red.h"
#include "theory/quantifiers/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
Trace("sygus-grammar-normalize") << "---------------------------------\n";
}
+void SygusGrammarNorm::TransfDrop::buildType(SygusGrammarNorm* sygus_norm,
+ TypeObject& to,
+ const Datatype& dt,
+ std::vector<unsigned>& op_pos)
+{
+ std::vector<unsigned> difference;
+ std::set_difference(op_pos.begin(),
+ op_pos.end(),
+ d_drop_indices.begin(),
+ d_drop_indices.end(),
+ std::back_inserter(difference));
+ op_pos = difference;
+}
+
/* TODO #1304: have more operators and types. Moreover, have more general ways
of finding kind of operator, e.g. if op is (\lambda xy. x + y) this
function should realize that it is chainable for integers */
{
NodeManager* nm = NodeManager::currentNM();
TypeNode sygus_tn = TypeNode::fromType(dt.getSygusType());
- /* TODO #1304: step 0: look for redundant constructors to drop */
+ Trace("sygus-gnorm") << "Infer transf for " << dt.getName() << "..."
+ << std::endl;
+ Trace("sygus-gnorm") << " #cons = " << op_pos.size() << " / "
+ << dt.getNumConstructors() << std::endl;
+ // look for redundant constructors to drop
+ if (options::sygusMinGrammar() && dt.getNumConstructors() == op_pos.size())
+ {
+ SygusRedundantCons src;
+ src.initialize(d_qe, tn);
+ std::vector<unsigned> rindices;
+ src.getRedundant(rindices);
+ if (!rindices.empty())
+ {
+ Trace("sygus-gnorm") << "...drop transf, " << rindices.size() << "/"
+ << op_pos.size() << " constructors." << std::endl;
+ Assert(rindices.size() < op_pos.size());
+ return new TransfDrop(rindices);
+ }
+ }
+
+ // if normalization option is not enabled, we do not infer the transformations
+ // below
+ if (!options::sygusGrammarNorm())
+ {
+ return nullptr;
+ }
+
/* TODO #1304: step 1: look for singleton */
/* step 2: look for chain */
unsigned chain_op_pos = dt.getNumConstructors();
/* Typenode admits a chain transformation for normalization */
if (chain_op_pos != dt.getNumConstructors() && !elem_pos.empty())
{
+ Trace("sygus-gnorm") << "...chain transf." << std::endl;
Trace("sygus-grammar-normalize-infer")
<< "\tInfering chain transformation\n";
return new TransfChain(chain_op_pos, elem_pos);
}
/* Creates type object for normalization */
TypeObject to(tn, unres_tn);
- /* If normalization option enabled, infer transformations to be applied in the
- * type */
- if (options::sygusGrammarNorm())
+
+ /* Determine normalization transformation based on sygus type and given
+ * operators */
+ Transf* transformation = inferTransf(tn, dt, op_pos);
+ /* If a transformation was selected, apply it */
+ if (transformation != nullptr)
{
- /* Determine normalization transformation based on sygus type and given
- * operators */
- Transf* transformation = inferTransf(tn, dt, op_pos);
- /* If a transformation was selected, apply it */
- if (transformation != nullptr)
- {
- transformation->buildType(this, to, dt, op_pos);
- }
+ transformation->buildType(this, to, dt, op_pos);
}
+
/* Remaining operators are rebuilt as they are */
for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
{
std::vector<unsigned>& op_pos) = 0;
}; /* class Transf */
+ /** Drop transformation class
+ *
+ * This class builds a type by dropping a set of redundant constructors,
+ * whose indices are given as input to the constructor of this class.
+ */
+ class TransfDrop : public Transf
+ {
+ public:
+ TransfDrop(std::vector<unsigned>& indices) : d_drop_indices(indices) {}
+ /** build type */
+ virtual void buildType(SygusGrammarNorm* sygus_norm,
+ TypeObject& to,
+ const Datatype& dt,
+ std::vector<unsigned>& op_pos);
+
+ private:
+ std::vector<unsigned> d_drop_indices;
+ };
+
/** Chain transformation class
*
* Determines how to build normalized types by chaining the application of one
class TransfChain : public Transf
{
public:
- TransfChain(unsigned chain_op_pos, std::vector<unsigned> elem_pos)
+ TransfChain(unsigned chain_op_pos, std::vector<unsigned>& elem_pos)
: d_chain_op_pos(chain_op_pos), d_elem_pos(elem_pos){};
/** builds types encoding a chain in which each link contains a repetition
--- /dev/null
+/********************* */
+/*! \file sygus_grammar_red.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 sygus_grammar_red
+ **/
+
+#include "theory/quantifiers/sygus_grammar_red.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn)
+{
+ Assert(qe != nullptr);
+ Trace("sygus-red") << "Compute redundant cons for " << tn << std::endl;
+ d_type = tn;
+ Assert(tn.isDatatype());
+ TermDbSygus* tds = qe->getTermDatabaseSygus();
+ tds->registerSygusType(tn);
+ const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ Assert(dt.isSygus());
+ TypeNode btn = TypeNode::fromType(dt.getSygusType());
+ for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+ {
+ Trace("sygus-red") << " Is " << dt[i].getName() << " a redundant operator?"
+ << std::endl;
+ std::map<int, Node> pre;
+ Node g = tds->mkGeneric(dt, i, pre);
+ Trace("sygus-red-debug") << " ...pre-rewrite : " << g << std::endl;
+ Assert(g.getNumChildren() == dt[i].getNumArgs());
+ d_gen_terms[i] = g;
+ for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+ {
+ pre[j] = g[j];
+ }
+ std::vector<Node> glist;
+ getGenericList(tds, dt, i, 0, pre, glist);
+ // call the extended rewriter
+ bool red = false;
+ for (const Node& gr : glist)
+ {
+ Trace("sygus-red-debug") << " ...variant : " << gr << std::endl;
+ std::map<Node, unsigned>::iterator itg = d_gen_cons.find(gr);
+ if (itg != d_gen_cons.end() && itg->second != i)
+ {
+ red = true;
+ Trace("sygus-red") << " ......redundant, since a variant of " << g
+ << " and " << d_gen_terms[itg->second]
+ << " both rewrite to " << gr << std::endl;
+ break;
+ }
+ else
+ {
+ d_gen_cons[gr] = i;
+ Trace("sygus-red") << " ......not redundant." << std::endl;
+ }
+ }
+ d_sygus_red_status.push_back(red ? 1 : 0);
+ }
+}
+
+void SygusRedundantCons::getRedundant(std::vector<unsigned>& indices)
+{
+ const Datatype& dt = static_cast<DatatypeType>(d_type.toType()).getDatatype();
+ for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+ {
+ if (isRedundant(i))
+ {
+ indices.push_back(i);
+ }
+ }
+}
+
+bool SygusRedundantCons::isRedundant(unsigned i)
+{
+ Assert(i < d_sygus_red_status.size());
+ return d_sygus_red_status[i] == 1;
+}
+
+void SygusRedundantCons::getGenericList(TermDbSygus* tds,
+ const Datatype& dt,
+ unsigned c,
+ unsigned index,
+ std::map<int, Node>& pre,
+ std::vector<Node>& terms)
+{
+ if (index == dt[c].getNumArgs())
+ {
+ Node gt = tds->mkGeneric(dt, c, pre);
+ gt = tds->getExtRewriter()->extendedRewrite(gt);
+ terms.push_back(gt);
+ return;
+ }
+ // with no swap
+ getGenericList(tds, dt, c, index + 1, pre, terms);
+ // swapping is exponential, only use for operators with small # args.
+ if (dt[c].getNumArgs() <= 5)
+ {
+ TypeNode atype = tds->getArgType(dt[c], index);
+ for (unsigned s = index + 1, nargs = dt[c].getNumArgs(); s < nargs; s++)
+ {
+ if (tds->getArgType(dt[c], s) == atype)
+ {
+ // swap s and index
+ Node tmp = pre[s];
+ pre[s] = pre[index];
+ pre[index] = tmp;
+ getGenericList(tds, dt, c, index + 1, pre, terms);
+ // revert
+ tmp = pre[s];
+ pre[s] = pre[index];
+ pre[index] = tmp;
+ }
+ }
+ }
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file sygus_grammar_red.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 sygus_grammar_red
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
+#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
+
+#include <map>
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** SygusRedundantCons
+ *
+ * This class computes the subset of indices of the constructors of a sygus type
+ * that are redundant. To use this class, first call initialize( qe, tn ),
+ * where tn is a sygus tn. Then, use getRedundant and/or isRedundant to get the
+ * indicies of the constructors of tn that are redundant.
+ */
+class SygusRedundantCons
+{
+ public:
+ SygusRedundantCons() {}
+ ~SygusRedundantCons() {}
+ /** register type tn
+ *
+ * qe : pointer to the quantifiers engine,
+ * tn : the (sygus) type to compute redundant constructors for
+ */
+ void initialize(QuantifiersEngine* qe, TypeNode tn);
+ /** Get the indices of the redundant constructors of the register type */
+ void getRedundant(std::vector<unsigned>& indices);
+ /**
+ * This function returns true if the i^th constructor of the registered type
+ * is redundant.
+ */
+ bool isRedundant(unsigned i);
+
+ private:
+ /** the registered type */
+ TypeNode d_type;
+ /** redundant status
+ *
+ * For each constructor, status indicating whether the constructor is
+ * redundant, where:
+ *
+ * 0 : not redundant,
+ * 1 : redundant since another constructor can be used to construct values for
+ * this constructor.
+ *
+ * For example, for grammar:
+ * A -> C > B | B < C | not D
+ * B -> x | y
+ * C -> 0 | 1 | C+C
+ * D -> B >= C
+ * If A is register with this class, then we store may store { 0, 1, 0 },
+ * noting that the second constructor of A can be simulated with the first.
+ * Notice that the third constructor is not considered redundant.
+ */
+ std::vector<int> d_sygus_red_status;
+ /**
+ * Map from constructor indices to the generic term for that constructor,
+ * where the generic term for a constructor is the (canonical) term returned
+ * by a call to TermDbSygus::mkGeneric.
+ */
+ std::map<unsigned, Node> d_gen_terms;
+ /**
+ * Map from the rewritten form of generic terms for constructors of the
+ * registered type to their corresponding constructor index.
+ */
+ std::map<Node, unsigned> d_gen_cons;
+ /** get generic list
+ *
+ * This function constructs all well-typed variants of a term of the form
+ * op( x1, ..., xn )
+ * where op is the builtin operator for dt[c], and xi = pre[i] for i=1,...,n.
+ *
+ * It constructs a list of terms of the form g * sigma, where sigma
+ * is an automorphism on { x1...xn } such that for all xi -> xj in sigma,
+ * the type for arguments i and j of dt[c] are the same. We store this
+ * list of terms in terms.
+ *
+ * This function recurses on the arguments of g, index is the current argument
+ * we are processing, and pre stores the current arguments of
+ *
+ * For example, for a sygus grammar
+ * A -> and( A, A, B )
+ * B -> false
+ * passing arguments such that g=and( x1, x2, x3 ) to this function will add:
+ * and( x1, x2, x3 ) and and( x2, x1, x3 )
+ * to terms.
+ */
+ void getGenericList(TermDbSygus* tds,
+ const Datatype& dt,
+ unsigned c,
+ unsigned index,
+ std::map<int, Node>& pre,
+ std::vector<Node>& terms);
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */
const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
Assert(dt.isSygus());
Assert(d_rvalue_cindices.find(tn) != d_rvalue_cindices.end());
- Trace("sygus-sample-grammar") << "Sygus random value " << tn
- << ", depth = " << depth
- << ", rchance = " << rchance << std::endl;
+ Trace("sygus-sample-grammar")
+ << "Sygus random value " << tn << ", depth = " << depth
+ << ", rchance = " << rchance << std::endl;
// check if we terminate on this call
// we refuse to enumerate terms of 10+ depth as a hard limit
bool terminate = Random::getRandom().pickWithProb(rchance) || depth >= 10;
unsigned ncons = cindices.size();
// select a random constructor, or random value when index=ncons.
unsigned index = Random::getRandom().pick(0, ncons);
- Trace("sygus-sample-grammar") << "Random index 0..." << ncons
- << " was : " << index << std::endl;
+ Trace("sygus-sample-grammar")
+ << "Random index 0..." << ncons << " was : " << index << std::endl;
if (index < ncons)
{
- Trace("sygus-sample-grammar") << "Recurse constructor index #" << index
- << std::endl;
+ Trace("sygus-sample-grammar")
+ << "Recurse constructor index #" << index << std::endl;
unsigned cindex = cindices[index];
Assert(cindex < dt.getNumConstructors());
const DatatypeConstructor& dtc = dt[cindex];
Trace("sygus-sample-grammar") << "...fail." << std::endl;
break;
}
- Trace("sygus-sample-grammar") << " child #" << i << " : " << c
- << std::endl;
+ Trace("sygus-sample-grammar")
+ << " child #" << i << " : " << c << std::endl;
pre[i] = c;
}
if (success)
return d_fv_stype[v];
}
-Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre ) {
- Assert( c>=0 && c<(int)dt.getNumConstructors() );
+Node TermDbSygus::mkGeneric(const Datatype& dt,
+ unsigned c,
+ std::map<TypeNode, int>& var_count,
+ std::map<int, Node>& pre)
+{
+ Assert(c < dt.getNumConstructors());
Assert( dt.isSygus() );
Assert( !dt[c].getSygusOp().isNull() );
std::vector< Node > children;
children.push_back( op );
}
Trace("sygus-db-debug") << "mkGeneric " << dt.getName() << " " << op << " " << op.getKind() << "..." << std::endl;
- for( int i=0; i<(int)dt[c].getNumArgs(); i++ ){
+ for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
+ {
TypeNode tna = getArgType( dt[c], i );
Node a;
std::map< int, Node >::iterator it = pre.find( i );
}else{
a = getFreeVarInc( tna, var_count, true );
}
+ Trace("sygus-db-debug")
+ << " child " << i << " : " << a << " : " << a.getType() << std::endl;
Assert( !a.isNull() );
children.push_back( a );
}
Node ret;
if( op.getKind()==BUILTIN ){
+ Trace("sygus-db-debug") << "Make builtin node..." << std::endl;
ret = NodeManager::currentNM()->mkNode( op, children );
}else{
Kind ok = getOperatorKind( op );
return n.substitute( d_var_list[tn].begin(), d_var_list[tn].end(), args.begin(), args.end() );
}
-Node TermDbSygus::getNormalized(TypeNode t, Node prog)
-{
- std::map< Node, Node >::iterator itn = d_normalized[t].find( prog );
- if( itn==d_normalized[t].end() ){
- Node progr = Rewriter::rewrite( prog );
- Trace("sygus-sym-break2") << "...rewrites to " << progr << std::endl;
- d_normalized[t][prog] = progr;
- return progr;
- }else{
- return itn->second;
- }
-}
-
unsigned TermDbSygus::getSygusTermSize( Node n ){
if( n.getNumChildren()==0 ){
return 0;
}
}
-unsigned TermDbSygus::getSygusConstructors( Node n, std::vector< Node >& cons ) {
- Assert( n.getKind()==APPLY_CONSTRUCTOR );
- Node op = n.getOperator();
- if( std::find( cons.begin(), cons.end(), op )==cons.end() ){
- cons.push_back( op );
- }
- if( n.getNumChildren()==0 ){
- return 0;
- }else{
- unsigned sum = 0;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- sum += getSygusConstructors( n[i], cons );
- }
- return 1+sum;
- }
-}
-
class ReqTrie {
public:
ReqTrie() : d_req_kind( UNDEFINED_KIND ){}
return -1;
}
-class ReconstructTrie {
-public:
- std::map< Node, ReconstructTrie > d_children;
- std::vector< Node > d_reconstruct;
- void add( std::vector< Node >& cons, Node r, unsigned index = 0 ){
- if( index==cons.size() ){
- d_reconstruct.push_back( r );
- }else{
- d_children[cons[index]].add( cons, r, index+1 );
- }
- }
- Node getReconstruct( std::map< Node, int >& rcons, unsigned depth ) {
- if( !d_reconstruct.empty() ){
- for( unsigned i=0; i<d_reconstruct.size(); i++ ){
- Node r = d_reconstruct[i];
- if( rcons[r]==0 ){
- Trace("sygus-static-enum") << "...eliminate constructor " << r << std::endl;
- rcons[r] = 1;
- return r;
- }
- }
- }
- if( depth>0 ){
- for( unsigned w=0; w<2; w++ ){
- for( std::map< Node, ReconstructTrie >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
- Node n = it->first;
- if( ( w==0 && rcons[n]!=0 ) || ( w==1 && rcons[n]==0 ) ){
- Node r = it->second.getReconstruct( rcons, depth - w );
- if( !r.isNull() ){
- if( w==1 ){
- Trace("sygus-static-enum") << "...use " << n << " to eliminate constructor " << r << std::endl;
- rcons[n] = -1;
- }
- return r;
- }
- }
- }
- }
- }
- return Node::null();
- }
-};
-
void TermDbSygus::registerSygusType( TypeNode tn ) {
std::map< TypeNode, TypeNode >::iterator itr = d_register.find( tn );
if( itr==d_register.end() ){
registerSygusType( getArgType( dt[i], j ) );
}
}
-
- //compute the redundant operators
- if( options::sygusMinGrammar() ){
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- bool nred = true;
- Trace("sygus-split-debug") << "Is " << dt[i].getName() << " a redundant operator?" << std::endl;
- Kind ck = getConsNumKind( tn, i );
- if( ck!=UNDEFINED_KIND ){
- Kind dk;
- if (TermUtil::isAntisymmetric(ck, dk))
- {
- int j = getKindConsNum( tn, dk );
- if( j!=-1 ){
- Trace("sygus-split-debug") << "Possible redundant operator : " << ck << " with " << dk << std::endl;
- //check for type mismatches
- bool success = true;
- for( unsigned k=0; k<2; k++ ){
- unsigned ko = k==0 ? 1 : 0;
- TypeNode tni = TypeNode::fromType( ((SelectorType)dt[i][k].getType()).getRangeType() );
- TypeNode tnj = TypeNode::fromType( ((SelectorType)dt[j][ko].getType()).getRangeType() );
- if( tni!=tnj ){
- Trace("sygus-split-debug") << "Argument types " << tni << " and " << tnj << " are not equal." << std::endl;
- success = false;
- break;
- }
- }
- if( success ){
- Trace("sygus-nf") << "* Sygus norm " << dt.getName() << " : do not consider any " << ck << " terms." << std::endl;
- nred = false;
- }
- }
- }
- }
- if( nred ){
- Trace("sygus-split-debug") << "Check " << dt[i].getName() << " based on generic rewriting" << std::endl;
- std::map< TypeNode, int > var_count;
- std::map< int, Node > pre;
- Node g = mkGeneric( dt, i, var_count, pre );
- nred = !computeGenericRedundant( tn, g );
- Trace("sygus-split-debug") << "...done check " << dt[i].getName() << " based on generic rewriting" << std::endl;
- }
- d_sygus_red_status[tn].push_back( nred ? 0 : 1 );
- }
- // run an enumerator for this type
- if( options::sygusMinGrammarAgg() ){
- TypeEnumerator te(tn);
- unsigned count = 0;
- std::map< Node, std::vector< Node > > builtin_to_orig;
- Trace("sygus-static-enum") << "Static enumerate " << dt.getName() << "..." << std::endl;
- while( !te.isFinished() && count<1000 ){
- Node n = *te;
- Node bn = sygusToBuiltin( n, tn );
- Trace("sygus-static-enum") << " " << bn;
- Node bnr = Rewriter::rewrite( bn );
- Trace("sygus-static-enum") << " ..." << bnr << std::endl;
- builtin_to_orig[bnr].push_back( n );
- ++te;
- count++;
- }
- std::map< Node, bool > reserved;
- for( unsigned i=0; i<=2; i++ ){
- Node rsv =
- i == 2 ? d_quantEngine->getTermUtil()->getTypeMaxValue(btn)
- : d_quantEngine->getTermUtil()->getTypeValue(btn, i);
- if( !rsv.isNull() ){
- reserved[ rsv ] = true;
- }
- }
- Trace("sygus-static-enum") << "...make the reconstruct index data structure..." << std::endl;
- ReconstructTrie rt;
- std::map< Node, int > rcons;
- unsigned max_depth = 0;
- for( std::map< Node, std::vector< Node > >::iterator itb = builtin_to_orig.begin(); itb != builtin_to_orig.end(); ++itb ){
- if( itb->second.size()>0 ){
- std::map< Node, std::vector< Node > > clist;
- Node single_cons;
- for( unsigned j=0; j<itb->second.size(); j++ ){
- Node e = itb->second[j];
- getSygusConstructors( e, clist[e] );
- if( clist[e].size()>max_depth ){
- max_depth = clist[e].size();
- }
- for( unsigned k=0; k<clist[e].size(); k++ ){
- /*
- unsigned cindex = Datatype::indexOf( clist[e][k].toExpr() );
- if( isGenericRedundant( tn, cindex ) ){
- is_gen_redundant = true;
- break;
- }else{
- */
- rcons[clist[e][k]] = 0;
- }
- //if( is_gen_redundant ){
- // clist.erase( e );
- //}else{
- if( clist[e].size()==1 ){
- Trace("sygus-static-enum") << "...single constructor term : " << e << ", builtin is " << itb->first << ", cons is " << clist[e][0] << std::endl;
- if( single_cons.isNull() ){
- single_cons = clist[e][0];
- }else{
- Trace("sygus-static-enum") << "*** already can eliminate constructor " << clist[e][0] << std::endl;
- unsigned cindex = Datatype::indexOf( clist[e][0].toExpr() );
- d_sygus_red_status[tn][cindex] = 1;
- }
- }
- //}
- }
- // do not eliminate 0, 1, or max
- if( !single_cons.isNull() && reserved.find( itb->first )==reserved.end() ){
- Trace("sygus-static-enum") << "...possibly elim " << single_cons << std::endl;
- for( std::map< Node, std::vector< Node > >::iterator itc = clist.begin(); itc != clist.end(); ++itc ){
- if( std::find( itc->second.begin(), itc->second.end(), single_cons )==itc->second.end() ){
- rt.add( itc->second, single_cons );
- }
- }
- }
- }
- }
- Trace("sygus-static-enum") << "...compute reconstructions..." << std::endl;
- Node next_rcons;
- do {
- unsigned depth = 0;
- do{
- next_rcons = rt.getReconstruct( rcons, depth );
- depth++;
- }while( next_rcons.isNull() && depth<=max_depth );
- // if we found a constructor to eliminate
- if( !next_rcons.isNull() ){
- Trace("sygus-static-enum") << "*** eliminate constructor " << next_rcons << std::endl;
- unsigned cindex = Datatype::indexOf( next_rcons.toExpr() );
- d_sygus_red_status[tn][cindex] = 2;
- }
- }while( !next_rcons.isNull() );
- Trace("sygus-static-enum") << "...finished..." << std::endl;
- }
- }else{
- // assume all are non-redundant
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- d_sygus_red_status[tn].push_back( 0 );
- }
- }
}
}
}
if( it==d_min_term_size.end() ){
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- if( !isGenericRedundant( tn, i ) ){
- if( dt[i].getNumArgs()==0 ){
- d_min_term_size[tn] = 0;
- return 0;
- }
+ if (dt[i].getNumArgs() == 0)
+ {
+ d_min_term_size[tn] = 0;
+ return 0;
}
}
// TODO : improve
unsigned TermDbSygus::getMinConsTermSize( TypeNode tn, unsigned cindex ) {
Assert( isRegistered( tn ) );
- Assert( !isGenericRedundant( tn, cindex ) );
std::map< unsigned, unsigned >::iterator it = d_min_cons_term_size[tn].find( cindex );
if( it==d_min_cons_term_size[tn].end() ){
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
}
}
-TypeNode TermDbSygus::getArgType( const DatatypeConstructor& c, int i ) {
- Assert( i>=0 && i<(int)c.getNumArgs() );
+TypeNode TermDbSygus::getArgType(const DatatypeConstructor& c, unsigned i)
+{
+ Assert(i < c.getNumArgs());
return TypeNode::fromType( ((SelectorType)c[i].getType()).getRangeType() );
}
return evaluateWithUnfolding( n, visited );
}
-bool TermDbSygus::computeGenericRedundant( TypeNode tn, Node g ) {
- //everything added to this cache should be mutually exclusive cases
- std::map< Node, bool >::iterator it = d_gen_redundant[tn].find( g );
- if( it==d_gen_redundant[tn].end() ){
- Trace("sygus-gnf") << "Register generic for " << tn << " : " << g << std::endl;
- Node gr = getNormalized(tn, g);
- Trace("sygus-gnf-debug") << "Generic " << g << " rewrites to " << gr << std::endl;
- std::map< Node, Node >::iterator itg = d_gen_terms[tn].find( gr );
- bool red = true;
- if( itg==d_gen_terms[tn].end() ){
- red = false;
- d_gen_terms[tn][gr] = g;
- Trace("sygus-gnf-debug") << "...not redundant." << std::endl;
- Trace("sygus-nf-reg") << "*** Sygus (generic) normal form : normal form of " << g << " is " << gr << std::endl;
- }else{
- Trace("sygus-gnf-debug") << "...redundant." << std::endl;
- Trace("sygus-nf") << "* Sygus normal form : simplify since " << g << " and " << itg->second << " both rewrite to " << gr << std::endl;
- }
- d_gen_redundant[tn][g] = red;
- return red;
- }else{
- return it->second;
- }
-}
-
-bool TermDbSygus::isGenericRedundant( TypeNode tn, unsigned i ) {
- Assert( i<d_sygus_red_status[tn].size() );
- if( options::sygusMinGrammarAgg() ){
- return d_sygus_red_status[tn][i]!=0;
- }else{
- return d_sygus_red_status[tn][i]==1;
- }
-}
-
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
* and var_count[Ti] is incremented.
*/
Node mkGeneric(const Datatype& dt,
- int c,
+ unsigned c,
std::map<TypeNode, int>& var_count,
std::map<int, Node>& pre);
/** same as above, but with empty var_count */
std::map<TypeNode, std::map<Node, int> > d_ops;
std::map<TypeNode, std::map<int, Node> > d_arg_ops;
std::map<TypeNode, std::map<Node, Node> > d_semantic_skolem;
- // normalized map
- std::map<TypeNode, std::map<Node, Node> > d_normalized;
// grammar information
// root -> type -> _
std::map<TypeNode, std::map<TypeNode, unsigned> > d_min_type_depth;
bool isKindArg( TypeNode tn, int i );
bool isConstArg( TypeNode tn, int i );
/** get arg type */
- TypeNode getArgType( const DatatypeConstructor& c, int i );
+ TypeNode getArgType(const DatatypeConstructor& c, unsigned i);
/** get first occurrence */
int getFirstArgOccurrence( const DatatypeConstructor& c, TypeNode tn );
/** is type match */
Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
Node getNormalized(TypeNode t, Node prog);
unsigned getSygusTermSize( Node n );
- // returns size
- unsigned getSygusConstructors( Node n, std::vector< Node >& cons );
/** given a term, construct an equivalent smaller one that respects syntax */
Node minimizeBuiltinTerm( Node n );
/** given a term, expand it into more basic components */
Node evaluateWithUnfolding(
Node n, std::unordered_map<Node, Node, NodeHashFunction>& visited);
Node evaluateWithUnfolding( Node n );
-//for calculating redundant operators
-private:
- //whether each constructor is redundant
- // 0 : not redundant, 1 : redundant, 2 : partially redundant
- std::map< TypeNode, std::vector< int > > d_sygus_red_status;
- // type to (rewritten) to original
- std::map< TypeNode, std::map< Node, Node > > d_gen_terms;
- std::map< TypeNode, std::map< Node, bool > > d_gen_redundant;
- //compute generic redundant
- bool computeGenericRedundant( TypeNode tn, Node g );
-public:
- bool isGenericRedundant( TypeNode tn, unsigned i );
};
}/* CVC4::theory::quantifiers namespace */
hd-19-d1-prog-dup-op.sy \
real-grammar-neg.sy \
real-si-all.sy \
- c100.sy
+ c100.sy \
+ check-generic-red.sy
# disabled, takes too long with and without CBQI BV
# Base16_1.sy
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+(set-logic LIA)
+
+(synth-fun P ((x Int) (y Int)) Bool
+ ((Start Bool ((and Start Start)
+ (not Start)
+ (<= StartInt StartIntC)
+ (<= StartInt StartInt)
+ (>= StartInt StartInt)
+ (<= StartIntC StartInt)
+ (>= StartIntC StartInt)
+ (<= StartIntC StartIntC)
+ ))
+ (StartIntC Int (0 0 1))
+ (StartInt Int (x y 0 1))))
+
+(constraint (P 0 2))
+(check-synth)
projects / cvc5.git / commitdiff