d_sygus_allow_all = allow_all;
}
-void Datatype::addSygusConstructor(CVC4::Expr op,
+void Datatype::addSygusConstructor(Expr op,
std::string& cname,
- std::vector<CVC4::Type>& cargs,
- std::shared_ptr<SygusPrintCallback> spc)
+ std::vector<Type>& cargs,
+ std::shared_ptr<SygusPrintCallback> 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<cargs.size(); j++ ){
Debug("parser-sygus-debug") << " arg " << j << " : " << cargs[j] << std::endl;
d_name(name + '\0' + "is_" + name), // default tester name is "is_FOO"
d_tester(),
d_args(),
- d_sygus_pc(nullptr)
+ d_sygus_pc(nullptr),
+ d_weight(1)
{
PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
}
-DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester)
+DatatypeConstructor::DatatypeConstructor(std::string name,
+ std::string tester,
+ unsigned weight)
: // We don't want to introduce a new data member, because eventually
// we're going to be a constant stuffed inside a node. So we stow
// the tester name away inside the constructor name until
d_name(name + '\0' + tester),
d_tester(),
d_args(),
- d_sygus_pc(nullptr)
+ d_sygus_pc(nullptr),
+ d_weight(weight)
{
PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
PrettyCheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
&& d_sygus_op[0][0] == d_sygus_op[1]);
}
+unsigned DatatypeConstructor::getWeight() const
+{
+ PrettyCheckArgument(
+ isResolved(), this, "this datatype constructor is not yet resolved");
+ return d_weight;
+}
+
std::shared_ptr<SygusPrintCallback> DatatypeConstructor::getSygusPrintCallback() const
{
PrettyCheckArgument(
* 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() {}
/**
*/
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<SygusPrintCallback> 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.
Expr d_sygus_op;
/** sygus print callback */
std::shared_ptr<SygusPrintCallback> d_sygus_pc;
+ /** weight */
+ unsigned d_weight;
/** shared selectors for each type
*
* 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<CVC4::Type>& cargs,
- std::shared_ptr<SygusPrintCallback> spc = nullptr);
+ std::vector<Type>& cargs,
+ std::shared_ptr<SygusPrintCallback> spc = nullptr,
+ int weight = -1);
/** set that this datatype is a tuple */
void setTuple();
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 );
}
// ------------------------------------------- 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<candidates.size(); i++ ){
Node v = candidates[i];
std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( 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<bool>())
+ {
clist.push_back( e );
}
}
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<bool>())
+ {
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;
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++)
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 */
projects / cvc5.git / commitdiff