#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() {}
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();
//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;
}
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;
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() );
}
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 ) ) );
}
}
+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;
+}
+}
+}
}
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;
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;
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);
};
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() );
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;
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)
{
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;
}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();
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++ ){
}
}
-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() );
}
}
-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() ){
bool isFreeVar( Node n ) { return d_fv_stype.find( n )!=d_fv_stype.end(); }
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 );
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;
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 */
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 );
/** 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 */
; 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)))))
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
; 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)
--- /dev/null
+; 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)
+
; 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)
; 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
projects / cvc5.git / commitdiff