diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 53 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.h | 19 |
3 files changed, 52 insertions, 22 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 908dde528..9a6728c29 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -873,7 +873,7 @@ bool CegSingleInvSol::getMatch(Node p, TermDbSygus* tds = d_qe->getTermDatabaseSygus(); if (tds->isFreeVar(p)) { - unsigned vnum = tds->getVarNum(p); + size_t vnum = tds->getFreeVarId(p); Node prev = s[vnum]; s[vnum] = n; if (prev.isNull()) diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index ee028bff0..f53637ebb 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -65,15 +65,21 @@ bool TermDbSygus::reset( Theory::Effort e ) { TNode TermDbSygus::getFreeVar( TypeNode tn, int i, bool useSygusType ) { unsigned sindex = 0; TypeNode vtn = tn; - if( useSygusType ){ - if( tn.isDatatype() ){ - const DType& dt = tn.getDType(); - if( !dt.getSygusType().isNull() ){ - vtn = dt.getSygusType(); + TypeNode builtinType = tn; + if (tn.isDatatype()) + { + const DType& dt = tn.getDType(); + if (!dt.getSygusType().isNull()) + { + builtinType = dt.getSygusType(); + if (useSygusType) + { + vtn = builtinType; sindex = 1; - } + } } } + NodeManager* nm = NodeManager::currentNM(); while( i>=(int)d_fv[sindex][tn].size() ){ std::stringstream ss; if( tn.isDatatype() ){ @@ -83,9 +89,13 @@ TNode TermDbSygus::getFreeVar( TypeNode tn, int i, bool useSygusType ) { ss << "fv_" << tn << "_" << i; } Assert(!vtn.isNull()); - Node v = NodeManager::currentNM()->mkSkolem( ss.str(), vtn, "for sygus normal form testing" ); - d_fv_stype[v] = tn; - d_fv_num[v] = i; + Node v = nm->mkSkolem(ss.str(), vtn, "for sygus invariance testing"); + // store its id, which is unique per builtin type, regardless of how it is + // otherwise cached. + d_fvId[v] = d_fvTypeIdCounter[builtinType]; + d_fvTypeIdCounter[builtinType]++; + Trace("sygus-db-debug") << "Free variable id " << v << " = " << d_fvId[v] + << ", " << builtinType << std::endl; d_fv[sindex][tn].push_back( v ); } return d_fv[sindex][tn][i]; @@ -103,6 +113,22 @@ TNode TermDbSygus::getFreeVarInc( TypeNode tn, std::map< TypeNode, int >& var_co } } +bool TermDbSygus::isFreeVar(Node n) const +{ + return d_fvId.find(n) != d_fvId.end(); +} +size_t TermDbSygus::getFreeVarId(Node n) const +{ + std::map<Node, size_t>::const_iterator it = d_fvId.find(n); + if (it == d_fvId.end()) + { + Assert(false) << "TermDbSygus::isFreeVar: " << n + << " is not a cached free variable."; + return 0; + } + return it->second; +} + bool TermDbSygus::hasFreeVar( Node n, std::map< Node, bool >& visited ){ if( visited.find( n )==visited.end() ){ visited[n] = true; @@ -153,11 +179,6 @@ Node TermDbSygus::getProxyVariable(TypeNode tn, Node c) return it->second; } -TypeNode TermDbSygus::getSygusTypeForVar( Node v ) { - Assert(d_fv_stype.find(v) != d_fv_stype.end()); - return d_fv_stype[v]; -} - Node TermDbSygus::mkGeneric(const DType& dt, unsigned c, std::map<TypeNode, int>& var_count, @@ -321,10 +342,12 @@ Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn) } Assert(isFreeVar(n)); // map to builtin variable type - int fv_num = getVarNum(n); + size_t fv_num = getFreeVarId(n); Assert(!dt.getSygusType().isNull()); TypeNode vtn = dt.getSygusType(); Node ret = getFreeVar(vtn, fv_num); + Trace("sygus-db-debug") << "SygusToBuiltin: variable for " << n << " is " + << ret << ", fv_num=" << fv_num << std::endl; return ret; } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 516515c05..acc875780 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -201,9 +201,9 @@ class TermDbSygus { std::map<TypeNode, int>& var_count, bool useSygusType = false); /** returns true if n is a cached free variable (in d_fv). */ - bool isFreeVar(Node n) { return d_fv_stype.find(n) != d_fv_stype.end(); } - /** returns the index of n in the free variable cache (d_fv). */ - int getVarNum(Node n) { return d_fv_num[n]; } + bool isFreeVar(Node n) const; + /** returns the identifier for a cached free variable. */ + size_t getFreeVarId(Node n) const; /** returns true if n has a cached free variable (in d_fv). */ bool hasFreeVar(Node n); /** get sygus proxy variable @@ -373,8 +373,16 @@ class TermDbSygus { std::map<TypeNode, std::vector<Node> > d_fv[2]; /** Maps free variables to the domain type they are associated with in d_fv */ std::map<Node, TypeNode> d_fv_stype; - /** Maps free variables to their index in d_fv. */ - std::map<Node, int> d_fv_num; + /** Id count for free variables terms */ + std::map<TypeNode, size_t> d_fvTypeIdCounter; + /** + * Maps free variables to a unique identifier for their builtin type. Notice + * that, e.g. free variables of type Int and those that are of a sygus + * datatype type that encodes Int must have unique identifiers. This is + * to ensure that sygusToBuiltin for non-ground terms maps variables to + * unique variabales. + */ + std::map<Node, size_t> d_fvId; /** recursive helper for hasFreeVar, visited stores nodes we have visited. */ bool hasFreeVar(Node n, std::map<Node, bool>& visited); /** cache of getProxyVariable */ @@ -440,7 +448,6 @@ class TermDbSygus { std::vector<TypeNode>& argts, bool aggr = false); - TypeNode getSygusTypeForVar( Node v ); 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 ); |