From 315815067f79683045ca515867ed09ea72d8e2c3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 14 Aug 2019 11:17:09 -0500 Subject: [PATCH] Minor cleaning of sygus term database (#3159) --- .../sygus/ce_guided_single_inv_sol.cpp | 129 +++++++++++++----- .../sygus/ce_guided_single_inv_sol.h | 12 ++ .../quantifiers/sygus/term_database_sygus.cpp | 91 ------------ .../quantifiers/sygus/term_database_sygus.h | 7 - 4 files changed, 110 insertions(+), 129 deletions(-) diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index 9802ce049..fea2ce15a 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -17,6 +17,7 @@ #include "expr/datatype.h" #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" +#include "theory/arith/arith_msum.h" #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_attributes.h" @@ -230,7 +231,7 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status) int carg = -1; int karg = -1; // first, do standard minimizations - Node min_t = d_qe->getTermDatabaseSygus()->minimizeBuiltinTerm( t ); + Node min_t = minimizeBuiltinTerm(t); Trace("csi-rcons-debug") << "Minimized term is : " << min_t << std::endl; //check if op is in syntax sort carg = d_qe->getTermDatabaseSygus()->getOpConsNum( stn, min_t ); @@ -447,32 +448,6 @@ bool CegSingleInvSol::collectReconstructNodes(int pid, return true; } - /* - //flatten ITEs if necessary TODO : carry assignment or move this elsewhere - if( t.getKind()==ITE ){ - TypeNode cstn = tds->getArgType( dt[karg], 0 ); - tds->registerSygusType( cstn ); - Node prev_t; - while( !tds->hasKind( cstn, t[0].getKind() ) && t!=prev_t ){ - prev_t = t; - Node exp_c = tds->expandBuiltinTerm( t[0] ); - if( !exp_c.isNull() ){ - t = NodeManager::currentNM()->mkNode( ITE, exp_c, t[1], t[2] ); - Trace("csi-rcons-debug") << "Pre expand to " << t << std::endl; - } - t = flattenITEs( t, false ); - if( t!=prev_t ){ - Trace("csi-rcons-debug") << "Flatten ITE to " << t << std::endl; - std::map< Node, bool > sassign; - std::vector< Node > svars; - std::vector< Node > ssubs; - t = simplifySolutionNode( t, sassign, svars, ssubs, 0 ); - } - Assert( t.getKind()==ITE ); - } - } - */ - Node CegSingleInvSol::CegSingleInvSol::getReconstructedSolution(int id, bool mod_eq) { @@ -765,16 +740,16 @@ Node CegSingleInvSol::builtinToSygusConst(Node c, TypeNode tn, int rcons_depth) if (rcons_depth < 1000) { // accelerated, recursive reconstruction of constants - Kind pk = tds->getPlusKind(TypeNode::fromType(dt.getSygusType())); + Kind pk = getPlusKind(TypeNode::fromType(dt.getSygusType())); if (pk != UNDEFINED_KIND) { int arg = tds->getKindConsNum(tn, pk); if (arg != -1) { Kind ck = - tds->getComparisonKind(TypeNode::fromType(dt.getSygusType())); + getComparisonKind(TypeNode::fromType(dt.getSygusType())); Kind pkm = - tds->getPlusKind(TypeNode::fromType(dt.getSygusType()), true); + getPlusKind(TypeNode::fromType(dt.getSygusType()), true); // get types Assert(dt[arg].getNumArgs() == 2); TypeNode tn1 = tds->getArgType(dt[arg], 0); @@ -843,7 +818,7 @@ void CegSingleInvSol::registerType(TypeNode tn) const Datatype& dt = static_cast(tn.toType()).getDatatype(); TypeNode btn = TypeNode::fromType(dt.getSygusType()); // for constant reconstruction - Kind ck = tds->getComparisonKind(btn); + Kind ck = getComparisonKind(btn); Node z = d_qe->getTermUtil()->getTypeValue(btn, 0); // iterate over constructors @@ -1011,6 +986,98 @@ Node CegSingleInvSol::getGenericBase(TypeNode tn, const Datatype& dt, int c) d_generic_base[tn][c] = gr; return gr; } + +Node CegSingleInvSol::minimizeBuiltinTerm(Node n) +{ + Kind nk = n.getKind(); + if ((nk != EQUAL && nk != LEQ && nk != LT && nk != GEQ && nk != GT) + || !n[0].getType().isReal()) + { + return n; + } + NodeManager* nm = NodeManager::currentNM(); + bool changed = false; + std::vector mon[2]; + for (unsigned r = 0; r < 2; r++) + { + unsigned ro = r == 0 ? 1 : 0; + Node c; + Node nc; + if (n[r].getKind() == PLUS) + { + for (unsigned i = 0; i < n[r].getNumChildren(); i++) + { + if (ArithMSum::getMonomial(n[r][i], c, nc) + && c.getConst().isNegativeOne()) + { + mon[ro].push_back(nc); + changed = true; + } + else + { + if (!n[r][i].isConst() || !n[r][i].getConst().isZero()) + { + mon[r].push_back(n[r][i]); + } + } + } + } + else + { + if (ArithMSum::getMonomial(n[r], c, nc) + && c.getConst().isNegativeOne()) + { + mon[ro].push_back(nc); + changed = true; + } + else + { + if (!n[r].isConst() || !n[r].getConst().isZero()) + { + mon[r].push_back(n[r]); + } + } + } + } + if (changed) + { + Node nn[2]; + for (unsigned r = 0; r < 2; r++) + { + nn[r] = mon[r].size() == 0 + ? nm->mkConst(Rational(0)) + : (mon[r].size() == 1 ? mon[r][0] : nm->mkNode(PLUS, mon[r])); + } + return nm->mkNode(n.getKind(), nn[0], nn[1]); + } + return n; +} + +Kind CegSingleInvSol::getComparisonKind(TypeNode tn) +{ + if (tn.isInteger() || tn.isReal()) + { + return LT; + } + else if (tn.isBitVector()) + { + return BITVECTOR_ULT; + } + return UNDEFINED_KIND; +} + +Kind CegSingleInvSol::getPlusKind(TypeNode tn, bool is_neg) +{ + if (tn.isInteger() || tn.isReal()) + { + return is_neg ? MINUS : PLUS; + } + else if (tn.isBitVector()) + { + return is_neg ? BITVECTOR_SUB : BITVECTOR_PLUS; + } + return UNDEFINED_KIND; +} } } } diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h index d8239b530..c319080af 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h @@ -181,6 +181,18 @@ private: std::vector& args, int index_exc = -1, int index_start = 0); + /** given a term, construct an equivalent smaller one that respects syntax */ + Node minimizeBuiltinTerm(Node n); + /** + * Return the kind of "is less than" for type tn, where tn is either Int or + * BV. + */ + static Kind getComparisonKind(TypeNode tn); + /** + * Return the kind of "plus" for type tn, or "minus" if is_neg is true, where + * tn is either Int or BV. + */ + static Kind getPlusKind(TypeNode tn, bool is_neg = false); }; diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index af8c93e45..208c8b9a0 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -1294,89 +1294,6 @@ bool TermDbSygus::canConstructKind(TypeNode tn, return false; } -Node TermDbSygus::minimizeBuiltinTerm( Node n ) { - if( ( n.getKind()==EQUAL || n.getKind()==LEQ || n.getKind()==LT || n.getKind()==GEQ || n.getKind()==GT ) && - ( n[0].getType().isInteger() || n[0].getType().isReal() ) ){ - bool changed = false; - std::vector< Node > mon[2]; - for( unsigned r=0; r<2; r++ ){ - unsigned ro = r==0 ? 1 : 0; - Node c; - Node nc; - if( n[r].getKind()==PLUS ){ - for( unsigned i=0; i().isNegativeOne()) - { - mon[ro].push_back( nc ); - changed = true; - }else{ - if( !n[r][i].isConst() || !n[r][i].getConst().isZero() ){ - mon[r].push_back( n[r][i] ); - } - } - } - }else{ - if (ArithMSum::getMonomial(n[r], c, nc) - && c.getConst().isNegativeOne()) - { - mon[ro].push_back( nc ); - changed = true; - }else{ - if( !n[r].isConst() || !n[r].getConst().isZero() ){ - mon[r].push_back( n[r] ); - } - } - } - } - if( changed ){ - Node nn[2]; - for( unsigned r=0; r<2; r++ ){ - nn[r] = mon[r].size()==0 ? NodeManager::currentNM()->mkConst( Rational(0) ) : ( mon[r].size()==1 ? mon[r][0] : NodeManager::currentNM()->mkNode( PLUS, mon[r] ) ); - } - return NodeManager::currentNM()->mkNode( n.getKind(), nn[0], nn[1] ); - } - } - return n; -} - -Node TermDbSygus::expandBuiltinTerm( Node t ){ - if( t.getKind()==EQUAL ){ - if( t[0].getType().isReal() ){ - return NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, t[0], t[1] ), - NodeManager::currentNM()->mkNode( LEQ, t[1], t[0] ) ); - }else if( t[0].getType().isBoolean() ){ - return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ), - NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) ); - } - }else if( t.getKind()==ITE && t.getType().isBoolean() ){ - return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ), - NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[2] ) ); - } - return Node::null(); -} - - -Kind TermDbSygus::getComparisonKind( TypeNode tn ) { - if( tn.isInteger() || tn.isReal() ){ - return LT; - }else if( tn.isBitVector() ){ - return BITVECTOR_ULT; - }else{ - return UNDEFINED_KIND; - } -} - -Kind TermDbSygus::getPlusKind( TypeNode tn, bool is_neg ) { - if( tn.isInteger() || tn.isReal() ){ - return is_neg ? MINUS : PLUS; - }else if( tn.isBitVector() ){ - return is_neg ? BITVECTOR_SUB : BITVECTOR_PLUS; - }else{ - return UNDEFINED_KIND; - } -} - bool TermDbSygus::involvesDivByZero( Node n, std::map< Node, bool >& visited ){ if( visited.find( n )==visited.end() ){ visited[n] = true; @@ -1410,14 +1327,6 @@ bool TermDbSygus::involvesDivByZero( Node n ) { return involvesDivByZero( n, visited ); } -void doStrReplace(std::string& str, const std::string& oldStr, const std::string& newStr){ - size_t pos = 0; - while((pos = str.find(oldStr, pos)) != std::string::npos){ - str.replace(pos, oldStr.length(), newStr); - pos += newStr.length(); - } -} - Node TermDbSygus::getAnchor( Node n ) { if( n.getKind()==APPLY_SELECTOR_TOTAL ){ return getAnchor( n[0] ); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 2854ecab6..e0312c516 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -564,13 +564,6 @@ class TermDbSygus { 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 ); - /** 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 expandBuiltinTerm( Node n ); - /** get comparison kind */ - Kind getComparisonKind( TypeNode tn ); - Kind getPlusKind( TypeNode tn, bool is_neg = false ); /** involves div-by-zero */ bool involvesDivByZero( Node n ); /** get anchor */ -- 2.30.2