diff options
| -rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv_sol.cpp | 340 | ||||
| -rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv_sol.h | 107 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_database_sygus.cpp | 282 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_database_sygus.h | 17 | ||||
| -rwxr-xr-x | test/regress/regress0/sygus/General_plus10.sy | 2 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/array_search_2.sy | 2 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/c100.sy | 18 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/const-var-test.sy | 2 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/max.sy | 2 |
10 files changed, 469 insertions, 306 deletions
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp index 91c6e3089..74408a7c3 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp @@ -19,19 +19,27 @@ #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/ce_guided_single_inv.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database_sygus.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" -using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; using namespace std; namespace CVC4 { +namespace theory { +namespace quantifiers { + +bool doCompare(Node a, Node b, Kind k) +{ + Node com = NodeManager::currentNM()->mkNode(k, a, b); + com = Rewriter::rewrite(com); + Assert(com.getType().isBoolean()); + return com.isConst() && com.getConst<bool>(); +} CegConjectureSingleInvSol::CegConjectureSingleInvSol(QuantifiersEngine* qe) : d_qe(qe), d_id_count(0), d_root_id() {} @@ -720,7 +728,8 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in return d_rcons_to_id[stn][t]; }else{ status = 1; - d_qe->getTermDatabaseSygus()->registerSygusType( stn ); + // register the type + registerType(stn); int id = allocate( t, stn ); d_rcons_to_status[stn][t] = -1; TypeNode tn = t.getType(); @@ -777,7 +786,7 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in //try constant reconstruction if( min_t.isConst() ){ Trace("csi-rcons-debug") << "...try constant reconstruction." << std::endl; - Node min_t_c = d_qe->getTermDatabaseSygus()->builtinToSygusConst( min_t, stn ); + Node min_t_c = builtinToSygusConst(min_t, stn); if( !min_t_c.isNull() ){ Trace("csi-rcons-debug") << " constant reconstruction success for " << id << ", result = " << min_t_c << std::endl; d_reconstruct[id] = min_t_c; @@ -786,8 +795,8 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in } if( status!=0 ){ //try identity functions - for( unsigned i=0; i<d_qe->getTermDatabaseSygus()->getNumIdFuncs( stn ); i++ ){ - unsigned ii = d_qe->getTermDatabaseSygus()->getIdFuncIndex( stn, i ); + for (unsigned ii : d_id_funcs[stn]) + { Assert( dt[ii].getNumArgs()==1 ); //try to directly reconstruct from single argument std::vector< Node > tchildren; @@ -813,7 +822,8 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in success = false; int index_found; std::vector< Node > args; - if( d_qe->getTermDatabaseSygus()->getMatch( min_t, stn, index_found, args, karg, c_index ) ){ + if (getMatch(min_t, stn, index_found, args, karg, c_index)) + { success = true; status = 0; Node cons = Node::fromExpr( dt[index_found].getConstructor() ); @@ -1068,7 +1078,6 @@ void CegConjectureSingleInvSol::setReconstructed( int id, Node n ) { } void CegConjectureSingleInvSol::getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv ) { - Assert( n.getKind()!=k ); //? if( k==AND || k==OR ){ equiv.push_back( NodeManager::currentNM()->mkNode( k, n, n ) ); equiv.push_back( NodeManager::currentNM()->mkNode( k, n, NodeManager::currentNM()->mkConst( k==AND ) ) ); @@ -1187,4 +1196,317 @@ void CegConjectureSingleInvSol::registerEquivalentTerms( Node n ) { } } +Node CegConjectureSingleInvSol::builtinToSygusConst(Node c, + TypeNode tn, + int rcons_depth) +{ + std::map<Node, Node>::iterator it = d_builtin_const_to_sygus[tn].find(c); + if (it != d_builtin_const_to_sygus[tn].end()) + { + return it->second; + } + TermDbSygus* tds = d_qe->getTermDatabaseSygus(); + NodeManager* nm = NodeManager::currentNM(); + Node sc; + d_builtin_const_to_sygus[tn][c] = sc; + Assert(c.isConst()); + Assert(tn.isDatatype()); + const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype(); + Trace("csi-rcons-debug") << "Try to reconstruct " << c << " in " + << dt.getName() << std::endl; + Assert(dt.isSygus()); + // if we are not interested in reconstructing constants, or the grammar allows + // them, return a proxy + if (!options::cegqiSingleInvReconstructConst() || dt.getSygusAllowConst()) + { + Node k = nm->mkSkolem("sy", tn, "sygus proxy"); + SygusPrintProxyAttribute spa; + k.setAttribute(spa, c); + sc = k; + } + else + { + int carg = tds->getOpConsNum(tn, c); + if (carg != -1) + { + sc = nm->mkNode(APPLY_CONSTRUCTOR, + Node::fromExpr(dt[carg].getConstructor())); + } + else + { + // identity functions + for (unsigned ii : d_id_funcs[tn]) + { + Assert(dt[ii].getNumArgs() == 1); + // try to directly reconstruct from single argument + TypeNode tnc = tds->getArgType(dt[ii], 0); + Trace("csi-rcons-debug") + << "Based on id function " << dt[ii].getSygusOp() + << ", try reconstructing " << c << " instead in " << tnc + << std::endl; + Node n = builtinToSygusConst(c, tnc, rcons_depth); + if (!n.isNull()) + { + sc = nm->mkNode( + APPLY_CONSTRUCTOR, Node::fromExpr(dt[ii].getConstructor()), n); + break; + } + } + if (sc.isNull()) + { + if (rcons_depth < 1000) + { + // accelerated, recursive reconstruction of constants + Kind pk = tds->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())); + Kind pkm = + tds->getPlusKind(TypeNode::fromType(dt.getSygusType()), true); + // get types + Assert(dt[arg].getNumArgs() == 2); + TypeNode tn1 = tds->getArgType(dt[arg], 0); + TypeNode tn2 = tds->getArgType(dt[arg], 1); + // initialize d_const_list for tn1 + registerType(tn1); + // iterate over all positive constants, largest to smallest + int start = d_const_list[tn1].size() - 1; + int end = d_const_list[tn1].size() - d_const_list_pos[tn1]; + for (int i = start; i >= end; --i) + { + Node c1 = d_const_list[tn1][i]; + // only consider if smaller than c, and + if (doCompare(c1, c, ck)) + { + Node c2 = nm->mkNode(pkm, c, c1); + c2 = Rewriter::rewrite(c2); + if (c2.isConst()) + { + // reconstruct constant on the other side + Node sc2 = builtinToSygusConst(c2, tn2, rcons_depth + 1); + if (!sc2.isNull()) + { + Node sc1 = builtinToSygusConst(c1, tn1, rcons_depth); + Assert(!sc1.isNull()); + sc = nm->mkNode(APPLY_CONSTRUCTOR, + Node::fromExpr(dt[arg].getConstructor()), + sc1, + sc2); + break; + } + } + } + } + } + } + } + } + } + } + d_builtin_const_to_sygus[tn][c] = sc; + return sc; +} + +struct sortConstants +{ + Kind d_comp_kind; + bool operator()(Node i, Node j) + { + return i != j && doCompare(i, j, d_comp_kind); + } +}; + +void CegConjectureSingleInvSol::registerType(TypeNode tn) +{ + if (d_const_list_pos.find(tn) != d_const_list_pos.end()) + { + return; + } + d_const_list_pos[tn] = 0; + Assert(tn.isDatatype()); + + TermDbSygus* tds = d_qe->getTermDatabaseSygus(); + // ensure it is registered + tds->registerSygusType(tn); + const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype(); + TypeNode btn = TypeNode::fromType(dt.getSygusType()); + // for constant reconstruction + Kind ck = tds->getComparisonKind(btn); + Node z = d_qe->getTermUtil()->getTypeValue(btn, 0); + + // iterate over constructors + for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) + { + Node n = Node::fromExpr(dt[i].getSygusOp()); + if (n.getKind() != kind::BUILTIN && n.isConst()) + { + d_const_list[tn].push_back(n); + if (ck != UNDEFINED_KIND && doCompare(z, n, ck)) + { + d_const_list_pos[tn]++; + } + } + if (dt[i].isSygusIdFunc()) + { + d_id_funcs[tn].push_back(i); + } + } + // sort the constant list + if (!d_const_list[tn].empty()) + { + if (ck != UNDEFINED_KIND) + { + sortConstants sc; + sc.d_comp_kind = ck; + std::sort(d_const_list[tn].begin(), d_const_list[tn].end(), sc); + } + Trace("csi-rcons") << "Type has " << d_const_list[tn].size() + << " constants..." << std::endl + << " "; + for (unsigned i = 0; i < d_const_list[tn].size(); i++) + { + Trace("csi-rcons") << d_const_list[tn][i] << " "; + } + Trace("csi-rcons") << std::endl; + Trace("csi-rcons") << "Of these, " << d_const_list_pos[tn] + << " are marked as positive." << std::endl; + } +} + +bool CegConjectureSingleInvSol::getMatch(Node p, + Node n, + std::map<int, Node>& s, + std::vector<int>& new_s) +{ + TermDbSygus* tds = d_qe->getTermDatabaseSygus(); + if (tds->isFreeVar(p)) + { + unsigned vnum = tds->getVarNum(p); + Node prev = s[vnum]; + s[vnum] = n; + if (prev.isNull()) + { + new_s.push_back(vnum); + } + return prev.isNull() || prev == n; + } + if (n.getNumChildren() == 0) + { + return p == n; + } + if (n.getKind() == p.getKind() && n.getNumChildren() == p.getNumChildren()) + { + // try both ways? + unsigned rmax = + TermUtil::isComm(n.getKind()) && n.getNumChildren() == 2 ? 2 : 1; + std::vector<int> new_tmp; + for (unsigned r = 0; r < rmax; r++) + { + bool success = true; + for (unsigned i = 0, size = n.getNumChildren(); i < size; i++) + { + int io = r == 0 ? i : (i == 0 ? 1 : 0); + if (!getMatch(p[i], n[io], s, new_tmp)) + { + success = false; + for (unsigned j = 0; j < new_tmp.size(); j++) + { + s.erase(new_tmp[j]); + } + new_tmp.clear(); + break; + } + } + if (success) + { + new_s.insert(new_s.end(), new_tmp.begin(), new_tmp.end()); + return true; + } + } + } + return false; +} + +bool CegConjectureSingleInvSol::getMatch(Node t, + TypeNode st, + int& index_found, + std::vector<Node>& args, + int index_exc, + int index_start) +{ + Assert(st.isDatatype()); + const Datatype& dt = static_cast<DatatypeType>(st.toType()).getDatatype(); + Assert(dt.isSygus()); + std::map<Kind, std::vector<Node> > kgens; + std::vector<Node> gens; + for (unsigned i = index_start, ncons = dt.getNumConstructors(); i < ncons; + i++) + { + if ((int)i != index_exc) + { + Node g = getGenericBase(st, dt, i); + gens.push_back(g); + kgens[g.getKind()].push_back(g); + Trace("csi-sol-debug") << "Check generic base : " << g << " from " + << dt[i].getName() << std::endl; + if (g.getKind() == t.getKind()) + { + Trace("csi-sol-debug") << "Possible match ? " << g << " " << t + << " for " << dt[i].getName() << std::endl; + std::map<int, Node> sigma; + std::vector<int> new_s; + if (getMatch(g, t, sigma, new_s)) + { + // we found an exact match + bool msuccess = true; + for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) + { + if (sigma[j].isNull()) + { + msuccess = false; + break; + } + else + { + args.push_back(sigma[j]); + } + } + if (msuccess) + { + index_found = i; + return true; + } + } + } + } + } + return false; +} + +Node CegConjectureSingleInvSol::getGenericBase(TypeNode tn, + const Datatype& dt, + int c) +{ + std::map<int, Node>::iterator it = d_generic_base[tn].find(c); + if (it != d_generic_base[tn].end()) + { + return it->second; + } + TermDbSygus* tds = d_qe->getTermDatabaseSygus(); + Assert(tds->isRegistered(tn)); + std::map<TypeNode, int> var_count; + std::map<int, Node> pre; + Node g = tds->mkGeneric(dt, c, var_count, pre); + Trace("csi-sol-debug") << "Generic is " << g << std::endl; + Node gr = Rewriter::rewrite(g); + Trace("csi-sol-debug") << "Generic rewritten is " << gr << std::endl; + d_generic_base[tn][c] = gr; + return gr; +} +} +} } diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.h b/src/theory/quantifiers/ce_guided_single_inv_sol.h index c5f976f02..7043e1ecf 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.h +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.h @@ -27,6 +27,12 @@ namespace quantifiers { class CegConjectureSingleInv; +/** CegConjectureSingleInvSol + * + * This function implements Figure 5 of "Counterexample-Guided Quantifier + * Instantiation for Synthesis in SMT", Reynolds et al CAV 2015. + * + */ class CegConjectureSingleInvSol { friend class CegConjectureSingleInv; @@ -47,10 +53,32 @@ private: bool getAssignEquality( Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs ); Node simplifySolutionNode( Node sol, TypeNode stn, std::map< Node, bool >& assign, std::vector< Node >& vars, std::vector< Node >& subs, int status ); -public: + + public: + CegConjectureSingleInvSol(QuantifiersEngine* qe); + /** simplify solution + * + * Returns the simplified version of node sol whose syntax is restricted by + * the grammar corresponding to sygus datatype stn. + */ Node simplifySolution( Node sol, TypeNode stn ); -//solution reconstruction -private: + /** reconstruct solution + * + * Returns (if possible) a node that is equivalent to sol those syntax + * matches the grammar corresponding to sygus datatype stn. + * The value reconstructed is set to 1 if we successfully return a node, + * otherwise it is set to -1. + */ + Node reconstructSolution(Node sol, TypeNode stn, int& reconstructed); + /** preregister conjecture + * + * q : the synthesis conjecture this class is for. + * This is used as a heuristic to find terms in the original conjecture which + * may be helpful for using during reconstruction. + */ + void preregisterConjecture(Node q); + + private: int d_id_count; int d_root_id; std::map< int, Node > d_id_node; @@ -85,11 +113,74 @@ private: void getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv ); //register equivalent terms void registerEquivalentTerms( Node n ); -public: - Node reconstructSolution( Node sol, TypeNode stn, int& reconstructed ); - void preregisterConjecture( Node q ); -public: - CegConjectureSingleInvSol( QuantifiersEngine * qe ); + /** builtin to sygus const + * + * Returns a sygus term of type tn that encodes the builtin constant c. + * If the sygus datatype tn allows any constant, this may return a variable + * with the attribute SygusPrintProxyAttribute that associates it with c. + * + * rcons_depth limits the number of recursive calls when doing accelerated + * constant reconstruction (currently limited to 1000). Notice this is hacky: + * depending upon order of calls, constant rcons may succeed, e.g. 1001, 999 + * vs. 999, 1001. + */ + Node builtinToSygusConst(Node c, TypeNode tn, int rcons_depth = 0); + /** cache for the above function */ + std::map<TypeNode, std::map<Node, Node> > d_builtin_const_to_sygus; + /** sorted list of constants, per type */ + std::map<TypeNode, std::vector<Node> > d_const_list; + /** number of positive constants, per type */ + std::map<TypeNode, unsigned> d_const_list_pos; + /** list of constructor indices whose operators are identity functions */ + std::map<TypeNode, std::vector<int> > d_id_funcs; + /** initialize the above information for sygus type tn */ + void registerType(TypeNode tn); + /** get generic base + * + * This returns the builtin term that is the analog of an application of the + * c^th constructor of dt to fresh variables. + */ + Node getGenericBase(TypeNode tn, const Datatype& dt, int c); + /** cache for the above function */ + std::map<TypeNode, std::map<int, Node> > d_generic_base; + /** get match + * + * This function attempts to find a substitution for which p = n. If + * successful, this function returns a substitution in the form of s/new_s, + * where: + * s : substitution, where the domain are indices of terms in the sygus + * term database, and + * new_s : the members that were added to s on this call. + * Otherwise, this function returns false and s and new_s are unmodified. + */ + bool getMatch(Node p, + Node n, + std::map<int, Node>& s, + std::vector<int>& new_s); + /** get match + * + * This function attempts to find a builtin term that is analog to a value + * of the sygus datatype st that is equivalent to n. If this function returns + * true, then it has found such a term. Then we set: + * index_found : updated to the constructor index of the sygus term whose + * analog to equivalent to n. + * args : builtin terms corresponding to the match, in order. + * Otherwise, this function returns false and index_found and args are + * unmodified. + * For example, for grammar: + * A -> 0 | 1 | x | +( A, A ) + * Given input ( 5 + (x+1) ) and A we would return true, where: + * index_found is set to 3 and args is set to { 5, x+1 }. + * + * index_exc : (if applicable) exclude a constructor index of st + * index_start : start index of constructors of st to try + */ + bool getMatch(Node n, + TypeNode st, + int& index_found, + std::vector<Node>& args, + int index_exc = -1, + int index_start = 0); }; diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp index 8b1ff37f1..87bfa1901 100644 --- a/src/theory/quantifiers/term_database_sygus.cpp +++ b/src/theory/quantifiers/term_database_sygus.cpp @@ -109,127 +109,6 @@ TypeNode TermDbSygus::getSygusTypeForVar( Node v ) { return d_fv_stype[v]; } -bool TermDbSygus::getMatch( Node p, Node n, std::map< int, Node >& s ) { - std::vector< int > new_s; - return getMatch2( p, n, s, new_s ); -} - -bool TermDbSygus::getMatch2( Node p, Node n, std::map< int, Node >& s, std::vector< int >& new_s ) { - std::map< Node, int >::iterator it = d_fv_num.find( p ); - if( it!=d_fv_num.end() ){ - Node prev = s[it->second]; - s[it->second] = n; - if( prev.isNull() ){ - new_s.push_back( it->second ); - } - return prev.isNull() || prev==n; - }else if( n.getNumChildren()==0 ){ - return p==n; - }else if( n.getKind()==p.getKind() && n.getNumChildren()==p.getNumChildren() ){ - //try both ways? - unsigned rmax = TermUtil::isComm( n.getKind() ) && n.getNumChildren()==2 ? 2 : 1; - std::vector< int > new_tmp; - for( unsigned r=0; r<rmax; r++ ){ - bool success = true; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - int io = r==0 ? i : ( i==0 ? 1 : 0 ); - if( !getMatch2( p[i], n[io], s, new_tmp ) ){ - success = false; - for( unsigned j=0; j<new_tmp.size(); j++ ){ - s.erase( new_tmp[j] ); - } - new_tmp.clear(); - break; - } - } - if( success ){ - new_s.insert( new_s.end(), new_tmp.begin(), new_tmp.end() ); - return true; - } - } - } - return false; -} - -bool TermDbSygus::getMatch( Node t, TypeNode st, int& index_found, std::vector< Node >& args, int index_exc, int index_start ) { - Assert( st.isDatatype() ); - const Datatype& dt = ((DatatypeType)(st).toType()).getDatatype(); - Assert( dt.isSygus() ); - std::map< Kind, std::vector< Node > > kgens; - std::vector< Node > gens; - for( unsigned i=index_start; i<dt.getNumConstructors(); i++ ){ - if( (int)i!=index_exc ){ - Node g = getGenericBase( st, dt, i ); - gens.push_back( g ); - kgens[g.getKind()].push_back( g ); - Trace("sygus-db-debug") << "Check generic base : " << g << " from " << dt[i].getName() << std::endl; - if( g.getKind()==t.getKind() ){ - Trace("sygus-db-debug") << "Possible match ? " << g << " " << t << " for " << dt[i].getName() << std::endl; - std::map< int, Node > sigma; - if( getMatch( g, t, sigma ) ){ - //we found an exact match - bool msuccess = true; - for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){ - if( sigma[j].isNull() ){ - msuccess = false; - break; - }else{ - args.push_back( sigma[j] ); - } - } - if( msuccess ){ - index_found = i; - return true; - } - //we found an exact match - //std::map< TypeNode, int > var_count; - //Node new_t = mkGeneric( dt, i, var_count, args ); - //Trace("sygus-db-debug") << "Rewrote to : " << new_t << std::endl; - //return new_t; - } - } - } - } - /* - //otherwise, try to modulate based on kinds - for( std::map< Kind, std::vector< Node > >::iterator it = kgens.begin(); it != kgens.end(); ++it ){ - if( it->second.size()>1 ){ - for( unsigned i=0; i<it->second.size(); i++ ){ - for( unsigned j=0; j<it->second.size(); j++ ){ - if( i!=j ){ - std::map< int, Node > sigma; - if( getMatch( it->second[i], it->second[j], sigma ) ){ - if( sigma.size()==1 ){ - //Node mod_pat = sigma.begin().second; - //Trace("cegqi-si-rcons-debug") << "Modulated pattern " << mod_pat << " from " << it->second[i] << " and " << it->second[j] << std::endl; - } - } - } - } - } - } - } - */ - return false; -} - -Node TermDbSygus::getGenericBase( TypeNode tn, const Datatype& dt, int c ) { - std::map< int, Node >::iterator it = d_generic_base[tn].find( c ); - if( it==d_generic_base[tn].end() ){ - Assert( isRegistered( tn ) ); - std::map< TypeNode, int > var_count; - std::map< int, Node > pre; - Node g = mkGeneric( dt, c, var_count, pre ); - Trace("sygus-db-debug") << "Sygus DB : Generic is " << g << std::endl; - Node gr = Rewriter::rewrite( g ); - Trace("sygus-db-debug") << "Sygus DB : Generic rewritten is " << gr << std::endl; - d_generic_base[tn][c] = gr; - return gr; - }else{ - return it->second; - } -} - 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() ); Assert( dt.isSygus() ); @@ -274,27 +153,32 @@ Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) { std::map< Node, Node >::iterator it = d_sygus_to_builtin[tn].find( n ); if( it==d_sygus_to_builtin[tn].end() ){ Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n << ", type = " << tn << std::endl; - Node ret; const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); if( n.getKind()==APPLY_CONSTRUCTOR ){ unsigned i = Datatype::indexOf( n.getOperator().toExpr() ); Assert( n.getNumChildren()==dt[i].getNumArgs() ); std::map< TypeNode, int > var_count; std::map< int, Node > pre; - for( unsigned j=0; j<n.getNumChildren(); j++ ){ + for (unsigned j = 0, size = n.getNumChildren(); j < size; j++) + { pre[j] = sygusToBuiltin( n[j], getArgType( dt[i], j ) ); } - ret = mkGeneric( dt, i, var_count, pre ); + Node ret = mkGeneric(dt, i, var_count, pre); Trace("sygus-db-debug") << "SygusToBuiltin : Generic is " << ret << std::endl; d_sygus_to_builtin[tn][n] = ret; - }else{ - Assert( isFreeVar( n ) ); - //map to builtin variable type - int fv_num = getVarNum( n ); - Assert( !dt.getSygusType().isNull() ); - TypeNode vtn = TypeNode::fromType( dt.getSygusType() ); - ret = getFreeVar( vtn, fv_num ); + return ret; } + if (n.hasAttribute(SygusPrintProxyAttribute())) + { + // this variable was associated by an attribute to a builtin node + return n.getAttribute(SygusPrintProxyAttribute()); + } + Assert(isFreeVar(n)); + // map to builtin variable type + int fv_num = getVarNum(n); + Assert(!dt.getSygusType().isNull()); + TypeNode vtn = TypeNode::fromType(dt.getSygusType()); + Node ret = getFreeVar(vtn, fv_num); return ret; }else{ return it->second; @@ -305,89 +189,6 @@ Node TermDbSygus::sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& ar Assert( d_var_list[tn].size()==args.size() ); return n.substitute( d_var_list[tn].begin(), d_var_list[tn].end(), args.begin(), args.end() ); } - -//rcons_depth limits the number of recursive calls when doing accelerated constant reconstruction (currently limited to 1000) -//this is hacky : depending upon order of calls, constant rcons may succeed, e.g. 1001, 999 vs. 999, 1001 -Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn, int rcons_depth ) { - std::map< Node, Node >::iterator it = d_builtin_const_to_sygus[tn].find( c ); - if( it==d_builtin_const_to_sygus[tn].end() ){ - Node sc; - d_builtin_const_to_sygus[tn][c] = sc; - Assert( c.isConst() ); - Assert( tn.isDatatype() ); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Trace("csi-rcons-debug") << "Try to reconstruct " << c << " in " << dt.getName() << std::endl; - Assert( dt.isSygus() ); - // if we are not interested in reconstructing constants, or the grammar allows them, return a proxy - if( !options::cegqiSingleInvReconstructConst() || dt.getSygusAllowConst() ){ - Node k = NodeManager::currentNM()->mkSkolem( "sy", tn, "sygus proxy" ); - SygusPrintProxyAttribute spa; - k.setAttribute(spa,c); - sc = k; - }else{ - int carg = getOpConsNum( tn, c ); - if( carg!=-1 ){ - sc = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, Node::fromExpr( dt[carg].getConstructor() ) ); - }else{ - //identity functions - for( unsigned i=0; i<getNumIdFuncs( tn ); i++ ){ - unsigned ii = getIdFuncIndex( tn, i ); - Assert( dt[ii].getNumArgs()==1 ); - //try to directly reconstruct from single argument - TypeNode tnc = getArgType( dt[ii], 0 ); - Trace("csi-rcons-debug") << "Based on id function " << dt[ii].getSygusOp() << ", try reconstructing " << c << " instead in " << tnc << std::endl; - Node n = builtinToSygusConst( c, tnc, rcons_depth ); - if( !n.isNull() ){ - sc = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, Node::fromExpr( dt[ii].getConstructor() ), n ); - break; - } - } - if( sc.isNull() ){ - if( rcons_depth<1000 ){ - //accelerated, recursive reconstruction of constants - Kind pk = getPlusKind( TypeNode::fromType( dt.getSygusType() ) ); - if( pk!=UNDEFINED_KIND ){ - int arg = getKindConsNum( tn, pk ); - if( arg!=-1 ){ - Kind ck = getComparisonKind( TypeNode::fromType( dt.getSygusType() ) ); - Kind pkm = getPlusKind( TypeNode::fromType( dt.getSygusType() ), true ); - //get types - Assert( dt[arg].getNumArgs()==2 ); - TypeNode tn1 = getArgType( dt[arg], 0 ); - TypeNode tn2 = getArgType( dt[arg], 1 ); - //iterate over all positive constants, largest to smallest - int start = d_const_list[tn1].size()-1; - int end = d_const_list[tn1].size()-d_const_list_pos[tn1]; - for( int i=start; i>=end; --i ){ - Node c1 = d_const_list[tn1][i]; - //only consider if smaller than c, and - if( doCompare( c1, c, ck ) ){ - Node c2 = NodeManager::currentNM()->mkNode( pkm, c, c1 ); - c2 = Rewriter::rewrite( c2 ); - if( c2.isConst() ){ - //reconstruct constant on the other side - Node sc2 = builtinToSygusConst( c2, tn2, rcons_depth+1 ); - if( !sc2.isNull() ){ - Node sc1 = builtinToSygusConst( c1, tn1, rcons_depth ); - Assert( !sc1.isNull() ); - sc = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, Node::fromExpr( dt[arg].getConstructor() ), sc1, sc2 ); - break; - } - } - } - } - } - } - } - } - } - } - d_builtin_const_to_sygus[tn][c] = sc; - return sc; - }else{ - return it->second; - } -} Node TermDbSygus::getNormalized(TypeNode t, Node prog) { @@ -825,18 +626,6 @@ int TermDbSygus::solveForArgument( TypeNode tn, unsigned cindex, unsigned arg ) return -1; } -struct sortConstants { - TermDbSygus * d_tds; - Kind d_comp_kind; - bool operator() (Node i, Node j) { - if( i!=j ){ - return d_tds->doCompare( i, j, d_comp_kind ); - }else{ - return false; - } - } -}; - class ReconstructTrie { public: std::map< Node, ReconstructTrie > d_children; @@ -902,11 +691,6 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { }else{ // no arguments to synthesis functions } - //for constant reconstruction - Kind ck = getComparisonKind( TypeNode::fromType( dt.getSygusType() ) ); - Node z = d_quantEngine->getTermUtil()->getTypeValue( - TypeNode::fromType(dt.getSygusType()), 0); - d_const_list_pos[tn] = 0; //iterate over constructors for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ Expr sop = dt[i].getSygusOp(); @@ -922,33 +706,11 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { Trace("sygus-db") << ", constant"; d_consts[tn][n] = i; d_arg_const[tn][i] = n; - d_const_list[tn].push_back( n ); - if( ck!=UNDEFINED_KIND && doCompare( z, n, ck ) ){ - d_const_list_pos[tn]++; - } - } - if( dt[i].isSygusIdFunc() ){ - d_id_funcs[tn].push_back( i ); } d_ops[tn][n] = i; d_arg_ops[tn][i] = n; Trace("sygus-db") << std::endl; } - //sort the constant list - if( !d_const_list[tn].empty() ){ - if( ck!=UNDEFINED_KIND ){ - sortConstants sc; - sc.d_comp_kind = ck; - sc.d_tds = this; - std::sort( d_const_list[tn].begin(), d_const_list[tn].end(), sc ); - } - Trace("sygus-db") << "Type has " << d_const_list[tn].size() << " constants..." << std::endl << " "; - for( unsigned i=0; i<d_const_list[tn].size(); i++ ){ - Trace("sygus-db") << d_const_list[tn][i] << " "; - } - Trace("sygus-db") << std::endl; - Trace("sygus-db") << "Of these, " << d_const_list_pos[tn] << " are marked as positive." << std::endl; - } //register connected types for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){ @@ -1372,14 +1134,6 @@ bool TermDbSygus::isConstArg( TypeNode tn, int i ) { } } -unsigned TermDbSygus::getNumIdFuncs( TypeNode tn ) { - return d_id_funcs[tn].size(); -} - -unsigned TermDbSygus::getIdFuncIndex( TypeNode tn, unsigned i ) { - return d_id_funcs[tn][i]; -} - TypeNode TermDbSygus::getArgType( const DatatypeConstructor& c, int i ) { Assert( i>=0 && i<(int)c.getNumArgs() ); return TypeNode::fromType( ((SelectorType)c[i].getType()).getRangeType() ); @@ -1492,12 +1246,6 @@ Kind TermDbSygus::getPlusKind( TypeNode tn, bool is_neg ) { } } -bool TermDbSygus::doCompare( Node a, Node b, Kind k ) { - Node com = NodeManager::currentNM()->mkNode( k, a, b ); - com = Rewriter::rewrite( com ); - return com==d_true; -} - 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() ){ diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h index 01e518eb1..586ef0777 100644 --- a/src/theory/quantifiers/term_database_sygus.h +++ b/src/theory/quantifiers/term_database_sygus.h @@ -106,13 +106,6 @@ public: int getVarNum( Node n ) { return d_fv_num[n]; } bool hasFreeVar( Node n ); private: - std::map< TypeNode, std::map< int, Node > > d_generic_base; - std::map< TypeNode, std::vector< Node > > d_generic_templ; - bool getMatch( Node p, Node n, std::map< int, Node >& s ); - bool getMatch2( Node p, Node n, std::map< int, Node >& s, std::vector< int >& new_s ); -public: - bool getMatch( Node n, TypeNode st, int& index_found, std::vector< Node >& args, int index_exc = -1, int index_start = 0 ); -private: void computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, unsigned type_depth ); bool involvesDivByZero( Node n, std::map< Node, bool >& visited ); @@ -126,15 +119,10 @@ private: std::map<TypeNode, std::map<Node, int> > d_consts; std::map<TypeNode, std::map<Node, int> > d_ops; std::map<TypeNode, std::map<int, Node> > d_arg_ops; - std::map<TypeNode, std::vector<int> > d_id_funcs; - std::map<TypeNode, std::vector<Node> > - d_const_list; // sorted list of constants for type - std::map<TypeNode, unsigned> d_const_list_pos; std::map<TypeNode, std::map<Node, Node> > d_semantic_skolem; // normalized map std::map<TypeNode, std::map<Node, Node> > d_normalized; std::map<TypeNode, std::map<Node, Node> > d_sygus_to_builtin; - std::map<TypeNode, std::map<Node, Node> > d_builtin_const_to_sygus; // grammar information // root -> type -> _ std::map<TypeNode, std::map<TypeNode, unsigned> > d_min_type_depth; @@ -169,8 +157,6 @@ private: Kind getConsNumKind( TypeNode tn, int i ); bool isKindArg( TypeNode tn, int i ); bool isConstArg( TypeNode tn, int i ); - unsigned getNumIdFuncs( TypeNode tn ); - unsigned getIdFuncIndex( TypeNode tn, unsigned i ); /** get arg type */ TypeNode getArgType( const DatatypeConstructor& c, int i ); /** get first occurrence */ @@ -179,12 +165,10 @@ private: bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 ); TypeNode getSygusTypeForVar( Node v ); - Node getGenericBase( TypeNode tn, const Datatype& dt, int c ); Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre ); Node sygusToBuiltin( Node n, TypeNode tn ); Node sygusToBuiltin( Node n ) { return sygusToBuiltin( n, n.getType() ); } Node sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& args ); - Node builtinToSygusConst( Node c, TypeNode tn, int rcons_depth = 0 ); 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 ); @@ -197,7 +181,6 @@ private: /** get comparison kind */ Kind getComparisonKind( TypeNode tn ); Kind getPlusKind( TypeNode tn, bool is_neg = false ); - bool doCompare( Node a, Node b, Kind k ); // 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 */ diff --git a/test/regress/regress0/sygus/General_plus10.sy b/test/regress/regress0/sygus/General_plus10.sy index 33552f9e2..1792749e2 100755 --- a/test/regress/regress0/sygus/General_plus10.sy +++ b/test/regress/regress0/sygus/General_plus10.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-check-synth-sol +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) (synth-fun fb () Int ((Start Int ((Constant Int))))) diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 0d44a5214..9b9f1feb2 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -77,7 +77,8 @@ TESTS = commutative.sy \ strings-double-rec.sy \ hd-19-d1-prog-dup-op.sy \ real-grammar-neg.sy \ - real-si-all.sy + real-si-all.sy \ + c100.sy # disabled, takes too long with and without CBQI BV # Base16_1.sy diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy index 5786eb649..41346e655 100644 --- a/test/regress/regress0/sygus/array_search_2.sy +++ b/test/regress/regress0/sygus/array_search_2.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-check-synth-sol +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) (synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) (declare-var x1 Int) diff --git a/test/regress/regress0/sygus/c100.sy b/test/regress/regress0/sygus/c100.sy new file mode 100644 index 000000000..ef124c953 --- /dev/null +++ b/test/regress/regress0/sygus/c100.sy @@ -0,0 +1,18 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status + +(set-logic LIA) + +(synth-fun constant ((x Int)) Int + ((Start Int (0 + 2 + 3 + 5 + (+ Start Start) + (- Start Start) + )) + )) +(declare-var x Int) +(constraint (= (constant x) 100)) +(check-synth) + diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy index af2d8b25b..305f5783a 100644 --- a/test/regress/regress0/sygus/const-var-test.sy +++ b/test/regress/regress0/sygus/const-var-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-check-synth-sol +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) diff --git a/test/regress/regress0/sygus/max.sy b/test/regress/regress0/sygus/max.sy index cbe2bccea..37ed848ef 100644 --- a/test/regress/regress0/sygus/max.sy +++ b/test/regress/regress0/sygus/max.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-check-synth-sol +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) (synth-fun max ((x Int) (y Int)) Int |