From 9712a20e6585728c7d0453e64e1e3b06a7d37b7f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 19 May 2020 19:34:18 -0500 Subject: [PATCH] Fix cached free variable identifiers in sygus term database (#4394) Fixes an issue with over-pruning in SyGuS where using multiple sygus types that map to the same builtin type. Our mapping sygusToBuiltin did not ensure that free variables were unique. Fixes #4383. --- .../sygus/ce_guided_single_inv_sol.cpp | 2 +- .../quantifiers/sygus/term_database_sygus.cpp | 53 +++++++++++++------ .../quantifiers/sygus/term_database_sygus.h | 19 ++++--- test/regress/CMakeLists.txt | 1 + .../regress0/sygus/issue4383-cache-fv-id.sy | 23 ++++++++ 5 files changed, 76 insertions(+), 22 deletions(-) create mode 100644 test/regress/regress0/sygus/issue4383-cache-fv-id.sy 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::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& 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& 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 > d_fv[2]; /** Maps free variables to the domain type they are associated with in d_fv */ std::map d_fv_stype; - /** Maps free variables to their index in d_fv. */ - std::map d_fv_num; + /** Id count for free variables terms */ + std::map 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 d_fvId; /** recursive helper for hasFreeVar, visited stores nodes we have visited. */ bool hasFreeVar(Node n, std::map& visited); /** cache of getProxyVariable */ @@ -440,7 +448,6 @@ class TermDbSygus { std::vector& 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 ); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 336bbdd32..8a9151c17 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1003,6 +1003,7 @@ set(regress_0_tests regress0/sygus/issue3356-syg-inf-usort.smt2 regress0/sygus/issue3624.sy regress0/sygus/issue3645-grammar-sets.smt2 + regress0/sygus/issue4383-cache-fv-id.sy regress0/sygus/let-ringer.sy regress0/sygus/let-simp.sy regress0/sygus/no-logic.sy diff --git a/test/regress/regress0/sygus/issue4383-cache-fv-id.sy b/test/regress/regress0/sygus/issue4383-cache-fv-id.sy new file mode 100644 index 000000000..27378d9ca --- /dev/null +++ b/test/regress/regress0/sygus/issue4383-cache-fv-id.sy @@ -0,0 +1,23 @@ +; EXPECT: unsat +; COMMAND-LINE: --lang=sygus2 --sygus-out=status +(set-logic ALL) +(synth-fun args_0_refinement_0 + ((r Int)) Bool + ((fv_B Bool)) + ( + (fv_B Bool (true)) + ) +) +(synth-fun ret_refinement_0 + ((x0 Int) (r Bool)) Bool + ((fv_B Bool) (B Bool) (I Int)) + ( + (fv_B Bool (r true (=> B fv_B))) + (B Bool ((Variable Bool) (= I I))) + (I Int ((Variable Int) 1)) + ) +) +(constraint (ret_refinement_0 1 true)) +(constraint (not (ret_refinement_0 1 false))) +(constraint (and (ret_refinement_0 0 false))) +(check-synth) -- 2.30.2