From: Andrew Reynolds Date: Fri, 1 Dec 2017 17:43:02 +0000 (-0600) Subject: Minor additions for sygus (#1419) X-Git-Tag: cvc5-1.0.0~5436 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ffc78cdf25327d18f7ff5b265f78480248907cab;p=cvc5.git Minor additions for sygus (#1419) --- diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 8b6384dcc..f96066e80 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -181,17 +181,19 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){ d_sygus_allow_all = allow_all; } -void Datatype::addSygusConstructor(CVC4::Expr op, +void Datatype::addSygusConstructor(Expr op, std::string& cname, - std::vector& cargs, - std::shared_ptr spc) + std::vector& cargs, + std::shared_ptr spc, + int weight) { Debug("dt-sygus") << "--> Add constructor " << cname << " to " << getName() << std::endl; Debug("dt-sygus") << " sygus op : " << op << std::endl; std::string name = getName() + "_" + cname; std::string testerId("is-"); testerId.append(name); - CVC4::DatatypeConstructor c(name, testerId ); + unsigned cweight = weight >= 0 ? weight : (cargs.empty() ? 0 : 1); + DatatypeConstructor c(name, testerId, cweight); c.setSygus(op, spc); for( unsigned j=0; j DatatypeConstructor::getSygusPrintCallback() const { PrettyCheckArgument( diff --git a/src/expr/datatype.h b/src/expr/datatype.h index b899b0099..b3c81911f 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -229,8 +229,13 @@ class CVC4_PUBLIC DatatypeConstructor { * Create a new Datatype constructor with the given name for the * constructor and the given name for the tester. The actual * constructor and tester aren't created until resolution time. + * weight is the value that this constructor carries when computing size. + * For example, if A, B, C have weights 0, 1, and 3 respectively, then + * C( B( A() ), B( A() ) ) has size 5. */ - DatatypeConstructor(std::string name, std::string tester); + DatatypeConstructor(std::string name, + std::string tester, + unsigned weight = 1); ~DatatypeConstructor() {} /** @@ -295,12 +300,19 @@ class CVC4_PUBLIC DatatypeConstructor { */ bool isSygusIdFunc() const; /** get sygus print callback + * * This class stores custom ways of printing * sygus datatype constructors, for instance, * to handle defined or let expressions that * appear in user-provided grammars. */ std::shared_ptr getSygusPrintCallback() const; + /** get weight + * + * Get the weight of this constructor. This value is used when computing the + * size of datatype terms that involve this constructor. + */ + unsigned getWeight() const; /** * Get the tester name for this Datatype constructor. @@ -446,6 +458,8 @@ class CVC4_PUBLIC DatatypeConstructor { Expr d_sygus_op; /** sygus print callback */ std::shared_ptr d_sygus_pc; + /** weight */ + unsigned d_weight; /** shared selectors for each type * @@ -659,11 +673,17 @@ public: * encode the arguments of op. For example, a sygus constructor * with op = PLUS should be such that cargs.size()>=2 and * the sygus type of cargs[i] is Real/Int for each i. + * + * weight denotes the value added by the constructor when computing the size + * of datatype terms. Passing a value <0 denotes the default weight for the + * constructor, which is 0 for nullary constructors and 1 for non-nullary + * constructors. */ - void addSygusConstructor(CVC4::Expr op, + void addSygusConstructor(Expr op, std::string& cname, - std::vector& cargs, - std::shared_ptr spc = nullptr); + std::vector& cargs, + std::shared_ptr spc = nullptr, + int weight = -1); /** set that this datatype is a tuple */ void setTuple(); diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 49e8a6888..4fcb6d718 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -159,13 +159,15 @@ public: children.push_back( NodeManager::currentNM()->mkNode( kind::DT_SIZE, in[0][i] ) ); } } - Node res; - if( !children.empty() ){ - children.push_back( NodeManager::currentNM()->mkConst( Rational(1) ) ); - res = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::PLUS, children ); - }else{ - res = NodeManager::currentNM()->mkConst( Rational(0) ); - } + TNode constructor = in[0].getOperator(); + size_t constructorIndex = Datatype::indexOf(constructor.toExpr()); + const Datatype& dt = Datatype::datatypeOf(constructor.toExpr()); + const DatatypeConstructor& c = dt[constructorIndex]; + unsigned weight = c.getWeight(); + children.push_back(NodeManager::currentNM()->mkConst(Rational(weight))); + Node res = children.size() == 1 + ? children[0] + : NodeManager::currentNM()->mkNode(kind::PLUS, children); Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: rewrite size " << in << " to " << res << std::endl; return RewriteResponse(REWRITE_AGAIN_FULL, res ); } diff --git a/src/theory/quantifiers/ce_guided_pbe.cpp b/src/theory/quantifiers/ce_guided_pbe.cpp index d46fed686..bee19daeb 100644 --- a/src/theory/quantifiers/ce_guided_pbe.cpp +++ b/src/theory/quantifiers/ce_guided_pbe.cpp @@ -1054,6 +1054,7 @@ void CegConjecturePbe::staticLearnRedundantOps( // ------------------------------------------- solution construction from enumeration void CegConjecturePbe::getCandidateList( std::vector< Node >& candidates, std::vector< Node >& clist ) { + Valuation& valuation = d_qe->getValuation(); for( unsigned i=0; i::iterator it = d_cinfo.find( v ); @@ -1062,7 +1063,9 @@ void CegConjecturePbe::getCandidateList( std::vector< Node >& candidates, std::v Node e = it->second.d_esym_list[j]; std::map< Node, EnumInfo >::iterator it = d_einfo.find( e ); Assert( it != d_einfo.end() ); - if( getGuardStatus( it->second.d_active_guard )==1 ){ + Node gstatus = valuation.getSatValue(it->second.d_active_guard); + if (!gstatus.isNull() && gstatus.getConst()) + { clist.push_back( e ); } } @@ -1112,7 +1115,9 @@ bool CegConjecturePbe::constructCandidates( std::vector< Node >& enums, std::vec void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& lems ) { std::map< Node, EnumInfo >::iterator it = d_einfo.find( x ); Assert( it != d_einfo.end() ); - if( getGuardStatus( it->second.d_active_guard )==1 ){ + Node gstatus = d_qe->getValuation().getSatValue(it->second.d_active_guard); + if (!gstatus.isNull() && gstatus.getConst()) + { Assert( std::find( it->second.d_enum_vals.begin(), it->second.d_enum_vals.end(), v )==it->second.d_enum_vals.end() ); Node c = it->second.d_parent_candidate; Node exp_exc; @@ -2356,19 +2361,6 @@ bool CegConjecturePbe::UnifContext::isStringSolved( return true; } -int CegConjecturePbe::getGuardStatus( Node g ) { - bool value; - if( d_qe->getValuation().hasSatValue( g, value ) ) { - if( value ){ - return 1; - }else{ - return -1; - } - }else{ - return 0; - } -} - CegConjecturePbe::StrategyNode::~StrategyNode() { for (unsigned j = 0, size = d_strats.size(); j < size; j++) diff --git a/src/theory/quantifiers/ce_guided_pbe.h b/src/theory/quantifiers/ce_guided_pbe.h index 1abdda6a6..8cfed253c 100644 --- a/src/theory/quantifiers/ce_guided_pbe.h +++ b/src/theory/quantifiers/ce_guided_pbe.h @@ -742,14 +742,6 @@ class CegConjecturePbe { std::map< Node, std::vector< unsigned > > incr, UnifContext& x ); //------------------------------ end constructing solutions - - /** get guard status - * - * Returns 1 if g is asserted true in the SAT solver. - * Returns -1 if g is asserted false in the SAT solver. - * Returns 0 otherwise. - */ - int getGuardStatus(Node g); }; }/* namespace CVC4::theory::quantifiers */