#include "theory/datatypes/datatypes_sygus.h"
#include "theory/datatypes/datatypes_rewriter.h"
#include "expr/node_manager.h"
-#include "theory/bv/theory_bv_utils.h"
-#include "util/bitvector.h"
-#include "smt/smt_engine_scope.h"
-
+#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/options.h"
using namespace CVC4;
//check if we can strengthen the first argument
if( !arg1.isNull() ){
const Datatype& dt1 = ((DatatypeType)(tn1).toType()).getDatatype();
- Kind k = d_util->getArgKind( tnnp, csIndex );
+ Kind k = d_tds->getArgKind( tnnp, csIndex );
//size comparison for arguments (if necessary)
Node sz_leq;
- if( tn1==tnn && d_util->isComm( k ) ){
+ if( tn1==tnn && d_tds->isComm( k ) ){
sz_leq = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkNode( DT_SIZE, n ), NodeManager::currentNM()->mkNode( DT_SIZE, arg1 ) );
}
std::map< int, std::vector< int > >::iterator it = d_sygus_pc_arg_pos[tnn][csIndex].find( i );
}
}
//other constraints on arguments
- Kind curr = d_util->getArgKind( tnn, i );
+ Kind curr = d_tds->getArgKind( tnn, i );
if( curr!=UNDEFINED_KIND ){
//ITE children must be distinct when properly typed
if( curr==ITE ){
- if( getArgType( dt[i], 1 )==tnn && getArgType( dt[i], 2 )==tnn ){
+ if( d_tds->getArgType( dt[i], 1 )==tnn && d_tds->getArgType( dt[i], 2 )==tnn ){
Node arg_ite1 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[i][1].getSelector() ), n );
Node arg_ite2 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[i][2].getSelector() ), n );
Node deq = arg_ite1.eqNode( arg_ite2 ).negate();
if( d_register[tn].isNull() ){
Trace("sygus-split") << "...not sygus." << std::endl;
}else{
- d_util->registerSygusType( tn );
+ d_tds->registerSygusType( tn );
//compute the redundant operators
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
bool nred = true;
if( options::sygusNormalForm() ){
Trace("sygus-split-debug") << "Is " << dt[i].getName() << " a redundant operator?" << std::endl;
- std::map< int, Kind >::iterator it = d_util->d_arg_kind[tn].find( i );
- if( it!=d_util->d_arg_kind[tn].end() ){
+ Kind ck = d_tds->getArgKind( tn, i );
+ if( ck!=UNDEFINED_KIND ){
Kind dk;
- if( d_util->isAntisymmetric( it->second, dk ) ){
- int j = d_util->getKindArg( tn, dk );
+ if( d_tds->isAntisymmetric( ck, dk ) ){
+ int j = d_tds->getKindArg( tn, dk );
if( j!=-1 ){
- Trace("sygus-split-debug") << "Possible redundant operator : " << it->second << " with " << dk << std::endl;
+ Trace("sygus-split-debug") << "Possible redundant operator : " << ck << " with " << dk << std::endl;
//check for type mismatches
bool success = true;
for( unsigned k=0; k<2; k++ ){
}
}
if( success ){
- Trace("sygus-nf") << "* Sygus norm " << dt.getName() << " : do not consider any " << d_util->d_arg_kind[tn][i] << " terms." << std::endl;
+ Trace("sygus-nf") << "* Sygus norm " << dt.getName() << " : do not consider any " << ck << " terms." << std::endl;
nred = false;
}
}
Trace("sygus-split-debug") << "Check " << dt[i].getName() << " based on generic rewriting" << std::endl;
std::map< TypeNode, int > var_count;
std::map< int, Node > pre;
- Node g = d_util->mkGeneric( dt, i, var_count, pre );
+ Node g = d_tds->mkGeneric( dt, i, var_count, pre );
nred = !isGenericRedundant( tn, g );
Trace("sygus-split-debug") << "...done check " << dt[i].getName() << " based on generic rewriting" << std::endl;
}
}else{
// calculate which constructors we should consider based on normal form for terms
//get parent kind
- Kind parentKind = d_util->getArgKind( tnnp, csIndex );
+ Kind parentKind = d_tds->getArgKind( tnnp, csIndex );
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
Assert( d_sygus_nred.find( tnn )!=d_sygus_nred.end() );
bool addSplit = d_sygus_nred[tnn][i];
if( addSplit && parentKind!=UNDEFINED_KIND ){
- if( d_util->d_arg_kind.find( tnn )!=d_util->d_arg_kind.end() && d_util->d_arg_kind[tnn].find( i )!=d_util->d_arg_kind[tnn].end() ){
- addSplit = considerSygusSplitKind( dt, pdt, tnn, tnnp, d_util->d_arg_kind[tnn][i], parentKind, sIndex );
+ Kind ak = d_tds->getArgKind( tnn, i );
+ if( ak!=UNDEFINED_KIND ){
+ addSplit = considerSygusSplitKind( dt, pdt, tnn, tnnp, ak, parentKind, sIndex );
if( !addSplit ){
- Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider " << dt.getName() << "::" << d_util->d_arg_kind[tnn][i];
+ Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider " << dt.getName() << "::" << ak;
Trace("sygus-nf") << " as argument " << sIndex << " of " << parentKind << "." << std::endl;
}
- }else if( d_util->d_arg_const.find( tnn )!=d_util->d_arg_const.end() && d_util->d_arg_const[tnn].find( i )!=d_util->d_arg_const[tnn].end() ){
- addSplit = considerSygusSplitConst( dt, pdt, tnn, tnnp, d_util->d_arg_const[tnn][i], parentKind, sIndex );
- if( !addSplit ){
- Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider constant " << dt.getName() << "::" << d_util->d_arg_const[tnn][i];
- Trace("sygus-nf") << " as argument " << sIndex << " of " << parentKind << "." << std::endl;
+ }else{
+ Node ac = d_tds->getArgConst( tnn, i );
+ if( !ac.isNull() ){
+ addSplit = considerSygusSplitConst( dt, pdt, tnn, tnnp, ac, parentKind, sIndex );
+ if( !addSplit ){
+ Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider constant " << dt.getName() << "::" << ac;
+ Trace("sygus-nf") << " as argument " << sIndex << " of " << parentKind << "." << std::endl;
+ }
}
}
if( addSplit ){
//generic rewriting
std::map< int, Node > prec;
std::map< TypeNode, int > var_count;
- Node gc = d_util->mkGeneric( dt, i, var_count, prec );
+ Node gc = d_tds->mkGeneric( dt, i, var_count, prec );
std::map< int, Node > pre;
pre[sIndex] = gc;
- Node g = d_util->mkGeneric( pdt, csIndex, var_count, pre );
+ Node g = d_tds->mkGeneric( pdt, csIndex, var_count, pre );
addSplit = !isGenericRedundant( tnnp, g );
}
/*
Trace("sygus-nf-temp") << "Check " << dt[i].getName() << " as argument " << sIndex << " under " << parentKind << std::endl;
std::map< int, Node > prec;
std::map< TypeNode, int > var_count;
- Node gc = d_util->mkGeneric( dt, i, var_count, prec );
+ Node gc = d_tds->mkGeneric( dt, i, var_count, prec );
std::map< int, Node > pre;
pre[sIndex] = gc;
- Node g = d_util->mkGeneric( pdt, csIndex, var_count, pre );
+ Node g = d_tds->mkGeneric( pdt, csIndex, var_count, pre );
bool tmp = !isGenericRedundant( tnnp, g, false );
}
*/
//compute argument relationships for 2-arg constructors
if( parentKind!=UNDEFINED_KIND && pdt[csIndex].getNumArgs()==2 ){
int osIndex = sIndex==0 ? 1 : 0;
- TypeNode tnno = getArgType( pdt[csIndex], osIndex );
+ TypeNode tnno = d_tds->getArgType( pdt[csIndex], osIndex );
if( DatatypesRewriter::isTypeDatatype( tnno ) ){
const Datatype& dto = ((DatatypeType)(tnno).toType()).getDatatype();
registerSygusTypeConstructorArg( tnno, dto, tnnp, pdt, csIndex, osIndex );
Assert( d_sygus_pc_nred[tnn][csIndex].find( sIndex )!=d_sygus_pc_nred[tnn][csIndex].end() );
Assert( d_sygus_pc_nred[tnno][csIndex].find( osIndex )!=d_sygus_pc_nred[tnno][csIndex].end() );
- bool isPComm = d_util->isComm( parentKind );
+ bool isPComm = d_tds->isComm( parentKind );
std::map< int, bool > larg_consider;
for( unsigned i=0; i<dto.getNumConstructors(); i++ ){
if( d_sygus_pc_nred[tnno][csIndex][osIndex][i] ){
//arguments that can be removed
std::map< int, bool > rem_arg;
//collect information about this index
- bool isSingularConst = d_util->isConstArg( tnno, i ) && d_util->isSingularArg( d_util->d_arg_const[tnno][i], parentKind, 1 );
+ Node oac = d_tds->getArgConst( tnno, i );
+ bool isSingularConst = !oac.isNull() && d_tds->isSingularArg( oac, parentKind, 1 );
bool argConsider = false;
for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
if( d_sygus_pc_nred[tnn][csIndex][sIndex][j] ){
rem = true;
Trace("sygus-nf") << "* Sygus norm : RHS singularity arg " << dto[i].getSygusOp() << " of " << parentKind;
Trace("sygus-nf") << " : do not consider " << dt[j].getSygusOp() << " as first arg." << std::endl;
- }else if( d_util->isConstArg( tnn, j ) && d_util->isSingularArg( d_util->d_arg_const[tnn][j], parentKind, 0 ) && larg_consider.find( j )!=larg_consider.end() ){
- rem = true;
- Trace("sygus-nf") << "* Sygus norm : LHS singularity arg " << dt[j].getSygusOp() << " of " << parentKind;
- Trace("sygus-nf") << " : do not consider " << dto[i].getSygusOp() << " as second arg." << std::endl;
}else{
- if( parentKind!=UNDEFINED_KIND ){
- std::map< TypeNode, int > var_count;
- std::map< int, Node > pre;
- Node g1 = d_util->mkGeneric( dt, j, var_count, pre );
- Node g2 = d_util->mkGeneric( dto, i, var_count, pre );
- Node g = NodeManager::currentNM()->mkNode( parentKind, g1, g2 );
- if( isGenericRedundant( tnnp, g ) ){
- rem = true;
+ Node cac = d_tds->getArgConst( tnn, j );
+ if( !cac.isNull() && d_tds->isSingularArg( cac, parentKind, 0 ) && larg_consider.find( j )!=larg_consider.end() ){
+ rem = true;
+ Trace("sygus-nf") << "* Sygus norm : LHS singularity arg " << dt[j].getSygusOp() << " of " << parentKind;
+ Trace("sygus-nf") << " : do not consider " << dto[i].getSygusOp() << " as second arg." << std::endl;
+ }else{
+ if( parentKind!=UNDEFINED_KIND ){
+ std::map< TypeNode, int > var_count;
+ std::map< int, Node > pre;
+ Node g1 = d_tds->mkGeneric( dt, j, var_count, pre );
+ Node g2 = d_tds->mkGeneric( dto, i, var_count, pre );
+ Node g = NodeManager::currentNM()->mkNode( parentKind, g1, g2 );
+ if( isGenericRedundant( tnnp, g ) ){
+ rem = true;
+ }
}
}
}
//this function gets all easy redundant cases, before consulting rewriters
bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt, TypeNode tn, TypeNode tnp, Kind k, Kind parent, int arg ) {
- Assert( d_util->hasKind( tn, k ) );
- Assert( d_util->hasKind( tnp, parent ) );
+ Assert( d_tds->hasKind( tn, k ) );
+ Assert( d_tds->hasKind( tnp, parent ) );
Trace("sygus-split") << "Consider sygus split kind " << k << ", parent = " << parent << ", arg = " << arg << "?" << std::endl;
- int c = d_util->getKindArg( tn, k );
- int pc = d_util->getKindArg( tnp, parent );
+ int c = d_tds->getKindArg( tn, k );
+ int pc = d_tds->getKindArg( tnp, parent );
if( k==parent ){
//check for associativity
- if( d_util->isAssoc( k ) ){
+ if( d_tds->isAssoc( k ) ){
//if the operator is associative, then a repeated occurrence should only occur in the leftmost argument position
int firstArg = getFirstArgOccurrence( pdt[pc], dt );
Assert( firstArg!=-1 );
Trace("sygus-split-debug") << ", reqk = " << reqk;
}
Trace("sygus-split-debug") << "?" << std::endl;
- int pcr = d_util->getKindArg( tnp, nk );
+ int pcr = d_tds->getKindArg( tnp, nk );
if( pcr!=-1 ){
Assert( pcr<(int)pdt.getNumConstructors() );
if( reqk!=UNDEFINED_KIND ){
bool success = true;
std::map< int, TypeNode > childTypes;
for( unsigned i=0; i<pdt[pcr].getNumArgs(); i++ ){
- TypeNode tna = getArgType( pdt[pcr], i );
+ TypeNode tna = d_tds->getArgType( pdt[pcr], i );
Assert( datatypes::DatatypesRewriter::isTypeDatatype( tna ) );
if( reqk!=UNDEFINED_KIND ){
//child must have a NOT
- int nindex = d_util->getKindArg( tna, reqk );
+ int nindex = d_tds->getKindArg( tna, reqk );
if( nindex!=-1 ){
const Datatype& adt = ((DatatypeType)(tn).toType()).getDatatype();
- if( getArgType( dt[c], i )!=getArgType( adt[nindex], 0 ) ){
+ if( d_tds->getArgType( dt[c], i )!=d_tds->getArgType( adt[nindex], 0 ) ){
Trace("sygus-split-debug") << "...arg " << i << " type mismatch." << std::endl;
success = false;
break;
//this function gets all easy redundant cases, before consulting rewriters
bool SygusSplit::considerSygusSplitConst( const Datatype& dt, const Datatype& pdt, TypeNode tn, TypeNode tnp, Node c, Kind parent, int arg ) {
- Assert( d_util->hasConst( tn, c ) );
- Assert( d_util->hasKind( tnp, parent ) );
- int pc = d_util->getKindArg( tnp, parent );
+ Assert( d_tds->hasConst( tn, c ) );
+ Assert( d_tds->hasKind( tnp, parent ) );
+ int pc = d_tds->getKindArg( tnp, parent );
Trace("sygus-split") << "Consider sygus split const " << c << ", parent = " << parent << ", arg = " << arg << "?" << std::endl;
- if( d_util->isIdempotentArg( c, parent, arg ) ){
+ if( d_tds->isIdempotentArg( c, parent, arg ) ){
Trace("sygus-split-debug") << " " << c << " is idempotent arg " << arg << " of " << parent << "..." << std::endl;
if( pdt[pc].getNumArgs()==2 ){
int oarg = arg==0 ? 1 : 0;
return false;
}
}
- }else if( d_util->isSingularArg( c, parent, arg ) ){
+ }else if( d_tds->isSingularArg( c, parent, arg ) ){
Trace("sygus-split-debug") << " " << c << " is singular arg " << arg << " of " << parent << "..." << std::endl;
- if( d_util->hasConst( tnp, c ) ){
+ if( d_tds->hasConst( tnp, c ) ){
return false;
}
}
if( pdt[pc].getNumArgs()==2 ){
Kind ok;
int offset;
- if( d_util->hasOffsetArg( parent, arg, offset, ok ) ){
+ if( d_tds->hasOffsetArg( parent, arg, offset, ok ) ){
Trace("sygus-split-debug") << parent << " has offset arg " << ok << " " << offset << std::endl;
- int ok_arg = d_util->getKindArg( tnp, ok );
+ int ok_arg = d_tds->getKindArg( tnp, ok );
if( ok_arg!=-1 ){
Trace("sygus-split-debug") << "...at argument " << ok_arg << std::endl;
//other operator be the same type
if( isTypeMatch( pdt[ok_arg], pdt[arg] ) ){
int status;
- Node co = d_util->getTypeValueOffset( c.getType(), c, offset, status );
+ Node co = d_tds->getTypeValueOffset( c.getType(), c, offset, status );
Trace("sygus-split-debug") << c << " with offset " << offset << " is " << co << ", status=" << status << std::endl;
if( status==0 && !co.isNull() ){
- if( d_util->hasConst( tn, co ) ){
+ if( d_tds->hasConst( tn, co ) ){
Trace("sygus-split-debug") << "arg " << arg << " " << c << " in " << parent << " can be treated as " << co << " in " << ok << "..." << std::endl;
return false;
}else{
}
bool SygusSplit::isArgDatatype( const DatatypeConstructor& c, int i, const Datatype& dt ) {
- TypeNode tni = getArgType( c, i );
+ TypeNode tni = d_tds->getArgType( c, i );
if( datatypes::DatatypesRewriter::isTypeDatatype( tni ) ){
const Datatype& adt = ((DatatypeType)(tni).toType()).getDatatype();
if( adt==dt ){
return false;
}
-TypeNode SygusSplit::getArgType( const DatatypeConstructor& c, int i ) {
- Assert( i>=0 && i<(int)c.getNumArgs() );
- return TypeNode::fromType( ((SelectorType)c[i].getType()).getRangeType() );
-}
-
bool SygusSplit::isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 ){
if( c1.getNumArgs()!=c2.getNumArgs() ){
return false;
}else{
for( unsigned i=0; i<c1.getNumArgs(); i++ ){
- if( getArgType( c1, i )!=getArgType( c2, i ) ){
+ if( d_tds->getArgType( c1, i )!=d_tds->getArgType( c2, i ) ){
return false;
}
}
std::map< Node, bool >::iterator it = d_gen_redundant[tn].find( g );
if( it==d_gen_redundant[tn].end() ){
Trace("sygus-gnf") << "Register generic for " << tn << " : " << g << std::endl;
- Node gr = d_util->getNormalized( tn, g, false );
+ Node gr = d_tds->getNormalized( tn, g, false );
Trace("sygus-gnf-debug") << "Generic " << g << " rewrites to " << gr << std::endl;
if( active ){
std::map< Node, Node >::iterator itg = d_gen_terms[tn].find( gr );
-SygusSymBreak::SygusSymBreak( SygusUtil * util, context::Context* c ) :
-d_util( util ), d_context( c ) {
+SygusSymBreak::SygusSymBreak( quantifiers::TermDbSygus * tds, context::Context* c ) : d_tds( tds ), d_context( c ) {
}
}
}
}
- return d_parent->d_util->mkGeneric( dt, tindex, var_count, pre );
+ return d_parent->d_tds->mkGeneric( dt, tindex, var_count, pre );
}else{
Trace("sygus-sym-break-debug") << "...failure." << std::endl;
return Node::null();
std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u,
std::map< TypeNode, int >& var_count ) {
Assert( a.getType()==at );
- //Assert( !d_util->d_conflict );
std::map< Node, bool >::iterator it = d_redundant[at].find( prog );
bool red;
if( it==d_redundant[at].end() ){
Trace("sygus-sym-break") << "Currently considering program : " << prog << " at depth " << depth << " for " << a << std::endl;
- Node progr = d_util->getNormalized( at, prog );
+ Node progr = d_tds->getNormalized( at, prog );
Node rep_prog;
std::map< Node, Node >::iterator itnp = d_normalized_to_orig[at].find( progr );
- int tsize = d_util->getTermSize( prog );
+ int tsize = d_tds->getTermSize( prog );
if( itnp==d_normalized_to_orig[at].end() ){
d_normalized_to_orig[at][progr] = prog;
- if( progr.getKind()==SKOLEM && d_util->getSygusType( progr )==at ){
+ if( progr.getKind()==SKOLEM && d_tds->getSygusType( progr )==at ){
Trace("sygus-nf") << "* Sygus sym break : " << prog << " rewrites to variable " << progr << " of same type as self" << std::endl;
d_redundant[at][prog] = true;
red = true;
//generalize conflict
if( prog.getNumChildren()>0 ){
Assert( !testers.empty() );
- d_util->registerSygusType( at );
+ d_tds->registerSygusType( at );
//Trace("sygus-nf-gen-debug") << "Testers are : " << std::endl;
//for( unsigned i=0; i<testers.size(); i++ ){
// Trace("sygus-nf-gen-debug") << "* " << testers[i] << std::endl;
TypeNode tn = testers_u[a][i][0].getType();
children.push_back( prog[i] );
children_stype.push_back( tn );
- Node nc = d_util->getNormalized( tn, prog[i], true );
+ Node nc = d_tds->getNormalized( tn, prog[i], true );
//norm_children[i] = nc;
rlv[i] = true;
nchildren.push_back( nc );
bool argChanged = false;
for( unsigned i=0; i<prog.getNumChildren(); i++ ){
Node prev = children[i];
- children[i] = d_util->getVarInc( children_stype[i], var_count );
+ children[i] = d_tds->getVarInc( children_stype[i], var_count );
Node progcn = NodeManager::currentNM()->mkNode( prog.getKind(), children );
Node progcr = Rewriter::rewrite( progcn );
Trace("sygus-nf-gen-debug") << "Var replace argument " << i << " : " << progcn << " -> " << progcr << std::endl;
st = st.substitute( curr_vars.begin(), curr_vars.end(), curr_subs.begin(), curr_subs.end() );
Trace("sygus-nf-gen-debug") << "...substituted : " << st << std::endl;
}
- TNode nv = d_util->getVarInc( tn, var_count );
+ TNode nv = d_tds->getVarInc( tn, var_count );
progc = progc.substitute( st, nv );
Node progcr = Rewriter::rewrite( progc );
Trace("sygus-nf-gen-debug") << "Var replace content " << st << " : " << progc << " -> " << progcr << std::endl;
}
}
Node lem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj );
- d_util->d_lemmas.push_back( lem );
+ d_lemmas.push_back( lem );
Trace("sygus-sym-break-lemma") << "Sym break lemma : " << lem << std::endl;
}else{
Trace("sygus-sym-break2") << "repeated lemma for " << prog << " from " << a << std::endl;
//we can continue if the tester in question is relevant
if( std::find( rlv_testers.begin(), rlv_testers.end(), tst_curr )!=rlv_testers.end() ){
unsigned tindex = Datatype::indexOf( tst_curr.getOperator().toExpr() );
- Node op = d_util->getArgOp( tn, tindex );
+ Node op = d_tds->getArgOp( tn, tindex );
if( op!=rop ){
Trace("sygus-nf-gen-debug") << "mismatch, success." << std::endl;
return true;
Node SygusSymBreak::getSeparationTemplate( TypeNode tn, Node rep_prog, Node anc_var, int& status ) {
Trace("sygus-nf-gen-debug") << "get separation template " << rep_prog << std::endl;
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- if( d_util->isVar( rep_prog ) ){
+ if( d_tds->isVar( rep_prog ) ){
status = 1;
return anc_var;
}else{
Node rop = rep_prog.getNumChildren()==0 ? rep_prog : rep_prog.getOperator();
- int rop_arg = d_util->getOpArg( tn, rop );
+ int rop_arg = d_tds->getOpArg( tn, rop );
Assert( rop_arg>=0 && rop_arg<(int)dt.getNumConstructors() );
Assert( rep_prog.getNumChildren()==dt[rop_arg].getNumArgs() );
bool SygusSymBreak::processConstantArg( TypeNode tnp, const Datatype & pdt, int pc,
Kind k, int i, Node arg, std::map< unsigned, bool >& rlv ) {
- Assert( d_util->hasKind( tnp, k ) );
+ Assert( d_tds->hasKind( tnp, k ) );
if( k==AND || k==OR || k==IFF || k==XOR || k==IMPLIES || ( k==ITE && i==0 ) ){
return false;
- }else if( d_util->isIdempotentArg( arg, k, i ) ){
+ }else if( d_tds->isIdempotentArg( arg, k, i ) ){
if( pdt[pc].getNumArgs()==2 ){
int oi = i==0 ? 1 : 0;
TypeNode otn = TypeNode::fromType( ((SelectorType)pdt[pc][oi].getType()).getRangeType() );
return false;
}
}
- }else if( d_util->isSingularArg( arg, k, i ) ){
- if( d_util->hasConst( tnp, arg ) ){
+ }else if( d_tds->isSingularArg( arg, k, i ) ){
+ if( d_tds->hasConst( tnp, arg ) ){
return false;
}
}
}
void SygusSymBreak::collectSubterms( Node n, Node tst_curr, std::map< Node, std::vector< Node > >& testers_u, std::map< Node, std::vector< Node > >& nodes ) {
- if( !d_util->isVar( n ) ){
+ if( !d_tds->isVar( n ) ){
nodes[n].push_back( tst_curr );
for( unsigned i=0; i<testers_u[tst_curr[0]].size(); i++ ){
collectSubterms( n[i], testers_u[tst_curr[0]][i], testers_u, nodes );
}
}
}
-
-SygusUtil::SygusUtil( Context* c ) {
- d_split = new SygusSplit( this );
- d_sym_break = new SygusSymBreak( this, c );
-}
-
-TNode SygusUtil::getVar( TypeNode tn, int i ) {
- while( i>=(int)d_fv[tn].size() ){
- std::stringstream ss;
- TypeNode vtn = tn;
- if( datatypes::DatatypesRewriter::isTypeDatatype( tn ) ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- ss << "fv_" << dt.getName() << "_" << i;
- if( !dt.getSygusType().isNull() ){
- vtn = TypeNode::fromType( dt.getSygusType() );
- }
- }else{
- 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[tn].push_back( v );
- }
- return d_fv[tn][i];
-}
-
-TNode SygusUtil::getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count ) {
- std::map< TypeNode, int >::iterator it = var_count.find( tn );
- if( it==var_count.end() ){
- var_count[tn] = 1;
- return getVar( tn, 0 );
- }else{
- int index = it->second;
- var_count[tn]++;
- return getVar( tn, index );
- }
-}
-
-TypeNode SygusUtil::getSygusType( Node v ) {
- Assert( d_fv_stype.find( v )!=d_fv_stype.end() );
- return d_fv_stype[v];
-}
-
-Node SygusUtil::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() );
- Assert( !dt[c].getSygusOp().isNull() );
- std::vector< Node > children;
- Node op = Node::fromExpr( dt[c].getSygusOp() );
- if( op.getKind()!=BUILTIN ){
- children.push_back( op );
- }
- for( int i=0; i<(int)dt[c].getNumArgs(); i++ ){
- TypeNode tna = TypeNode::fromType( ((SelectorType)dt[c][i].getType()).getRangeType() );
- Node a;
- std::map< int, Node >::iterator it = pre.find( i );
- if( it!=pre.end() ){
- a = it->second;
- }else{
- a = getVarInc( tna, var_count );
- }
- Assert( !a.isNull() );
- children.push_back( a );
- }
- if( op.getKind()==BUILTIN ){
- return NodeManager::currentNM()->mkNode( op, children );
- }else{
- if( children.size()==1 ){
- return children[0];
- }else{
- return NodeManager::currentNM()->mkNode( APPLY, children );
- /*
- Node n = NodeManager::currentNM()->mkNode( APPLY, children );
- //must expand definitions
- Node ne = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( n.toExpr() ) );
- Trace("sygus-util-debug") << "Expanded definitions in " << n << " to " << ne << std::endl;
- return ne;
- */
- }
- }
-}
-
-Node SygusUtil::getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs ) {
- return n;
- if( n.getKind()==SKOLEM ){
- std::map< Node, Node >::iterator its = subs.find( n );
- if( its!=subs.end() ){
- return its->second;
- }else{
- std::map< Node, TypeNode >::iterator it = d_fv_stype.find( n );
- if( it!=d_fv_stype.end() ){
- Node v = getVarInc( it->second, var_count );
- subs[n] = v;
- return v;
- }else{
- return n;
- }
- }
- }else{
- if( n.getNumChildren()>0 ){
- std::vector< Node > children;
- if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
- children.push_back( n.getOperator() );
- }
- bool childChanged = false;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- Node nc = getSygusNormalized( n[i], var_count, subs );
- childChanged = childChanged || nc!=n[i];
- children.push_back( nc );
- }
- if( childChanged ){
- return NodeManager::currentNM()->mkNode( n.getKind(), children );
- }
- }
- return n;
- }
-}
-
-Node SygusUtil::getNormalized( TypeNode t, Node prog, bool do_pre_norm ) {
- if( do_pre_norm ){
- std::map< TypeNode, int > var_count;
- std::map< Node, Node > subs;
- prog = getSygusNormalized( prog, var_count, subs );
- }
- std::map< Node, Node >::iterator itn = d_normalized[t].find( prog );
- if( itn==d_normalized[t].end() ){
- Node progr = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( prog.toExpr() ) );
- progr = Rewriter::rewrite( progr );
- std::map< TypeNode, int > var_count;
- std::map< Node, Node > subs;
- progr = getSygusNormalized( progr, var_count, subs );
- Trace("sygus-sym-break2") << "...rewrites to " << progr << std::endl;
- d_normalized[t][prog] = progr;
- return progr;
- }else{
- return itn->second;
- }
-}
-
-int SygusUtil::getTermSize( Node n ){
- if( isVar( n ) ){
- return 0;
- }else{
- int sum = 0;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- sum += getTermSize( n[i] );
- }
- return 1+sum;
- }
-
-}
-
-bool SygusUtil::isAssoc( Kind k ) {
- return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
- k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT;
-}
-
-bool SygusUtil::isComm( Kind k ) {
- return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
- k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR;
-}
-
-bool SygusUtil::isAntisymmetric( Kind k, Kind& dk ) {
- if( k==GT ){
- dk = LT;
- return true;
- }else if( k==GEQ ){
- dk = LEQ;
- return true;
- }else if( k==BITVECTOR_UGT ){
- dk = BITVECTOR_ULT;
- return true;
- }else if( k==BITVECTOR_UGE ){
- dk = BITVECTOR_ULE;
- return true;
- }else if( k==BITVECTOR_SGT ){
- dk = BITVECTOR_SLT;
- return true;
- }else if( k==BITVECTOR_SGE ){
- dk = BITVECTOR_SLE;
- return true;
- }else{
- return false;
- }
-}
-
-bool SygusUtil::isIdempotentArg( Node n, Kind ik, int arg ) {
- TypeNode tn = n.getType();
- if( n==getTypeValue( tn, 0 ) ){
- if( ik==PLUS || ik==OR || ik==XOR || ik==BITVECTOR_PLUS || ik==BITVECTOR_OR || ik==BITVECTOR_XOR ){
- return true;
- }else if( ik==MINUS || ik==BITVECTOR_SHL || ik==BITVECTOR_LSHR || ik==BITVECTOR_SUB ){
- return arg==1;
- }
- }else if( n==getTypeValue( tn, 1 ) ){
- if( ik==MULT || ik==BITVECTOR_MULT ){
- return true;
- }else if( ik==DIVISION || ik==BITVECTOR_UDIV || ik==BITVECTOR_SDIV ){
- return arg==1;
- }
- }else if( n==getTypeMaxValue( tn ) ){
- if( ik==IFF || ik==BITVECTOR_AND || ik==BITVECTOR_XNOR ){
- return true;
- }
- }
- return false;
-}
-
-
-bool SygusUtil::isSingularArg( Node n, Kind ik, int arg ) {
- TypeNode tn = n.getType();
- if( n==getTypeValue( tn, 0 ) ){
- if( ik==AND || ik==MULT || ik==BITVECTOR_AND || ik==BITVECTOR_MULT ){
- return true;
- }else if( ik==DIVISION || ik==BITVECTOR_UDIV || ik==BITVECTOR_SDIV ){
- return arg==0;
- }
- }else if( n==getTypeMaxValue( tn ) ){
- if( ik==OR || ik==BITVECTOR_OR ){
- return true;
- }
- }
- return false;
-}
-
-bool SygusUtil::hasOffsetArg( Kind ik, int arg, int& offset, Kind& ok ) {
- if( ik==LT ){
- Assert( arg==0 || arg==1 );
- offset = arg==0 ? 1 : -1;
- ok = LEQ;
- return true;
- }else if( ik==BITVECTOR_ULT ){
- Assert( arg==0 || arg==1 );
- offset = arg==0 ? 1 : -1;
- ok = BITVECTOR_ULE;
- return true;
- }else if( ik==BITVECTOR_SLT ){
- Assert( arg==0 || arg==1 );
- offset = arg==0 ? 1 : -1;
- ok = BITVECTOR_SLE;
- return true;
- }
- return false;
-}
-
-
-Node SygusUtil::getTypeValue( TypeNode tn, int val ) {
- std::map< int, Node >::iterator it = d_type_value[tn].find( val );
- if( it==d_type_value[tn].end() ){
- Node n;
- if( tn.isInteger() || tn.isReal() ){
- Rational c(val);
- n = NodeManager::currentNM()->mkConst( c );
- }else if( tn.isBitVector() ){
- unsigned int uv = val;
- BitVector bval(tn.getConst<BitVectorSize>(), uv);
- n = NodeManager::currentNM()->mkConst<BitVector>(bval);
- }else if( tn.isBoolean() ){
- if( val==0 ){
- n = NodeManager::currentNM()->mkConst( false );
- }
- }
- d_type_value[tn][val] = n;
- return n;
- }else{
- return it->second;
- }
-}
-
-Node SygusUtil::getTypeMaxValue( TypeNode tn ) {
- std::map< TypeNode, Node >::iterator it = d_type_max_value.find( tn );
- if( it==d_type_max_value.end() ){
- Node n;
- if( tn.isBitVector() ){
- n = bv::utils::mkOnes(tn.getConst<BitVectorSize>());
- }else if( tn.isBoolean() ){
- n = NodeManager::currentNM()->mkConst( true );
- }
- d_type_max_value[tn] = n;
- return n;
- }else{
- return it->second;
- }
-}
-
-Node SygusUtil::getTypeValueOffset( TypeNode tn, Node val, int offset, int& status ) {
- std::map< int, Node >::iterator it = d_type_value_offset[tn][val].find( offset );
- if( it==d_type_value_offset[tn][val].end() ){
- Node val_o;
- Node offset_val = getTypeValue( tn, offset );
- status = -1;
- if( !offset_val.isNull() ){
- if( tn.isInteger() || tn.isReal() ){
- val_o = Rewriter::rewrite( NodeManager::currentNM()->mkNode( PLUS, val, offset_val ) );
- status = 0;
- }else if( tn.isBitVector() ){
- val_o = Rewriter::rewrite( NodeManager::currentNM()->mkNode( BITVECTOR_PLUS, val, offset_val ) );
- }
- }
- d_type_value_offset[tn][val][offset] = val_o;
- d_type_value_offset_status[tn][val][offset] = status;
- return val_o;
- }else{
- status = d_type_value_offset_status[tn][val][offset];
- return it->second;
- }
-}
-
-void SygusUtil::registerSygusType( TypeNode tn ){
- if( d_register.find( tn )==d_register.end() ){
- if( !DatatypesRewriter::isTypeDatatype( tn ) ){
- d_register[tn] = TypeNode::null();
- }else{
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- Trace("sygus-util") << "Register type " << dt.getName() << "..." << std::endl;
- d_register[tn] = TypeNode::fromType( dt.getSygusType() );
- if( d_register[tn].isNull() ){
- Trace("sygus-util") << "...not sygus." << std::endl;
- }else{
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- Expr sop = dt[i].getSygusOp();
- Assert( !sop.isNull() );
- Node n = Node::fromExpr( sop );
- Trace("sygus-util") << " Operator #" << i << " : " << sop;
- if( sop.getKind() == kind::BUILTIN ){
- Kind sk = NodeManager::operatorToKind( n );
- Trace("sygus-util") << ", kind = " << sk;
- d_kinds[tn][sk] = i;
- d_arg_kind[tn][i] = sk;
- }else if( sop.isConst() ){
- Trace("sygus-util") << ", constant";
- d_consts[tn][n] = i;
- d_arg_const[tn][i] = n;
- }
- d_ops[tn][n] = i;
- d_arg_ops[tn][i] = n;
- Trace("sygus-util") << std::endl;
- }
- }
- }
- }
-}
-
-bool SygusUtil::isRegistered( TypeNode tn ) {
- return d_register.find( tn )!=d_register.end();
-}
-
-int SygusUtil::getKindArg( TypeNode tn, Kind k ) {
- Assert( isRegistered( tn ) );
- std::map< TypeNode, std::map< Kind, int > >::iterator itt = d_kinds.find( tn );
- if( itt!=d_kinds.end() ){
- std::map< Kind, int >::iterator it = itt->second.find( k );
- if( it!=itt->second.end() ){
- return it->second;
- }
- }
- return -1;
-}
-
-int SygusUtil::getConstArg( TypeNode tn, Node n ){
- Assert( isRegistered( tn ) );
- std::map< TypeNode, std::map< Node, int > >::iterator itt = d_consts.find( tn );
- if( itt!=d_consts.end() ){
- std::map< Node, int >::iterator it = itt->second.find( n );
- if( it!=itt->second.end() ){
- return it->second;
- }
- }
- return -1;
-}
-
-int SygusUtil::getOpArg( TypeNode tn, Node n ) {
- std::map< Node, int >::iterator it = d_ops[tn].find( n );
- if( it!=d_ops[tn].end() ){
- return it->second;
- }else{
- return -1;
- }
-}
-
-bool SygusUtil::hasKind( TypeNode tn, Kind k ) {
- return getKindArg( tn, k )!=-1;
-}
-bool SygusUtil::hasConst( TypeNode tn, Node n ) {
- return getConstArg( tn, n )!=-1;
-}
-bool SygusUtil::hasOp( TypeNode tn, Node n ) {
- return getOpArg( tn, n )!=-1;
-}
-
-Node SygusUtil::getArgOp( TypeNode tn, int i ) {
- Assert( isRegistered( tn ) );
- std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_ops.find( tn );
- if( itt!=d_arg_ops.end() ){
- std::map< int, Node >::iterator itn = itt->second.find( i );
- if( itn!=itt->second.end() ){
- return itn->second;
- }
- }
- return Node::null();
-}
-
-Kind SygusUtil::getArgKind( TypeNode tn, int i ) {
- Assert( isRegistered( tn ) );
- std::map< TypeNode, std::map< int, Kind > >::iterator itt = d_arg_kind.find( tn );
- if( itt!=d_arg_kind.end() ){
- std::map< int, Kind >::iterator itk = itt->second.find( i );
- if( itk!=itt->second.end() ){
- return itk->second;
- }
- }
- return UNDEFINED_KIND;
-}
-
-bool SygusUtil::isKindArg( TypeNode tn, int i ) {
- return getArgKind( tn, i )!=UNDEFINED_KIND;
-}
-
-bool SygusUtil::isConstArg( TypeNode tn, int i ) {
- Assert( isRegistered( tn ) );
- std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_const.find( tn );
- if( itt!=d_arg_const.end() ){
- return itt->second.find( i )!=itt->second.end();
- }else{
- return false;
- }
-}
-
-
-
-
-
namespace CVC4 {
namespace theory {
+
+namespace quantifiers {
+ class TermDbSygus;
+}
+
namespace datatypes {
-class SygusUtil;
-
class SygusSplit
{
private:
- SygusUtil * d_util;
+ quantifiers::TermDbSygus * d_tds;
std::map< Node, std::vector< Node > > d_splits;
std::map< TypeNode, std::vector< bool > > d_sygus_nred;
std::map< TypeNode, std::map< int, std::map< int, std::vector< bool > > > > d_sygus_pc_nred;
int getFirstArgOccurrence( const DatatypeConstructor& c, const Datatype& dt );
/** is arg datatype */
bool isArgDatatype( const DatatypeConstructor& c, int i, const Datatype& dt );
- /** get arg type */
- TypeNode getArgType( const DatatypeConstructor& c, int i );
/** is type match */
bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 );
private:
// generic cache
bool isGenericRedundant( TypeNode tn, Node g, bool active = true );
public:
- SygusSplit( SygusUtil * util ) : d_util( util ) {}
+ SygusSplit( quantifiers::TermDbSygus * tds ) : d_tds( tds ){}
/** get sygus splits */
void getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits, std::vector< Node >& lemmas );
};
class SygusSymBreak
{
private:
- SygusUtil * d_util;
+ quantifiers::TermDbSygus * d_tds;
context::Context* d_context;
class ProgSearch {
typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
bool isSeparation( Node rep_prog, Node tst_curr, std::map< Node, std::vector< Node > >& testers_u, std::vector< Node >& rlv_testers );
Node getSeparationTemplate( TypeNode tn, Node rep_prog, Node anc_var, int& status );
public:
- SygusSymBreak( SygusUtil * util, context::Context* c );
+ SygusSymBreak( quantifiers::TermDbSygus * tds, context::Context* c );
/** add tester */
void addTester( Node tst );
-};
-
-class SygusUtil
-{
- friend class SygusSplit;
- friend class SygusSymBreak;
-private:
- std::map< TypeNode, std::vector< Node > > d_fv;
- std::map< Node, TypeNode > d_fv_stype;
-private:
- TNode getVar( TypeNode tn, int i );
- TNode getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count );
- bool isVar( Node n ) { return d_fv_stype.find( n )!=d_fv_stype.end(); }
-private:
- SygusSplit * d_split;
- SygusSymBreak * d_sym_break;
- std::map< TypeNode, std::map< Node, Node > > d_normalized;
-private:
- //information for sygus types
- std::map< TypeNode, TypeNode > d_register; //stores sygus type
- std::map< TypeNode, std::map< int, Kind > > d_arg_kind;
- std::map< TypeNode, std::map< Kind, int > > d_kinds;
- std::map< TypeNode, std::map< int, Node > > d_arg_const;
- 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;
-private:
- bool isRegistered( TypeNode tn );
- int getKindArg( TypeNode tn, Kind k );
- int getConstArg( TypeNode tn, Node n );
- int getOpArg( TypeNode tn, Node n );
- bool hasKind( TypeNode tn, Kind k );
- bool hasConst( TypeNode tn, Node n );
- bool hasOp( TypeNode tn, Node n );
- Node getArgOp( TypeNode tn, int i );
- Kind getArgKind( TypeNode tn, int i );
- bool isKindArg( TypeNode tn, int i );
- bool isConstArg( TypeNode tn, int i );
- void registerSygusType( TypeNode tn );
-private:
- //information for builtin types
- std::map< TypeNode, std::map< int, Node > > d_type_value;
- std::map< TypeNode, Node > d_type_max_value;
- std::map< TypeNode, std::map< Node, std::map< int, Node > > > d_type_value_offset;
- std::map< TypeNode, std::map< Node, std::map< int, int > > > d_type_value_offset_status;
- /** is assoc */
- bool isAssoc( Kind k );
- /** is comm */
- bool isComm( Kind k );
- /** isAntisymmetric */
- bool isAntisymmetric( Kind k, Kind& dk );
- /** is idempotent arg */
- bool isIdempotentArg( Node n, Kind ik, int arg );
- /** is singular arg */
- bool isSingularArg( Node n, Kind ik, int arg );
- /** get offset arg */
- bool hasOffsetArg( Kind ik, int arg, int& offset, Kind& ok );
- /** get value */
- Node getTypeValue( TypeNode tn, int val );
- /** get value */
- Node getTypeValueOffset( TypeNode tn, Node val, int offset, int& status );
- /** get value */
- Node getTypeMaxValue( TypeNode tn );
-private:
- TypeNode getSygusType( Node v );
- Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre );
- Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
- Node getNormalized( TypeNode t, Node prog, bool do_pre_norm = false );
- int getTermSize( Node n );
-public:
- SygusUtil( context::Context* c );
- SygusSplit * getSplit() { return d_split; }
- SygusSymBreak * getSymBreak() { return d_sym_break; }
- //context::CDO<bool> d_conflict;
- //Node d_conflictNode;
+ /** lemmas we have generated */
std::vector< Node > d_lemmas;
};
-
}
}
}
#include "theory/theory_model.h"
#include "smt/options.h"
#include "smt/boolean_terms.h"
-#include "theory/quantifiers/options.h"
#include "theory/datatypes/options.h"
#include "theory/type_enumerator.h"
-#include "theory/datatypes/datatypes_sygus.h"
+
+#include "theory/quantifiers/options.h"
+#include "theory/quantifiers_engine.h"
+
#include <map>
d_true = NodeManager::currentNM()->mkConst( true );
d_dtfCounter = 0;
- if( options::ceGuidedInst() ){
- d_sygus_util = new SygusUtil( c );
- }else{
- d_sygus_util = NULL;
- }
+ d_sygus_split = NULL;
+ d_sygus_sym_break = NULL;
}
TheoryDatatypes::~TheoryDatatypes() {
}else{
Trace("dt-split") << "*************Split for constructors on " << n << endl;
std::vector< Node > children;
- if( dt.isSygus() && d_sygus_util ){
+ if( dt.isSygus() && d_sygus_split ){
std::vector< Node > lemmas;
- d_sygus_util->getSplit()->getSygusSplits( n, dt, children, lemmas );
+ d_sygus_split->getSygusSplits( n, dt, children, lemmas );
for( unsigned i=0; i<lemmas.size(); i++ ){
Trace("dt-lemma-sygus") << "Dt sygus lemma : " << lemmas[i] << std::endl;
d_out->lemma( lemmas[i] );
addTester( fact, eqc, rep );
if( !d_conflict && polarity ){
Trace("dt-tester") << "Assert tester : " << atom << std::endl;
- if( d_sygus_util ){
+ if( d_sygus_sym_break ){
//Assert( !d_sygus_util->d_conflict );
- d_sygus_util->getSymBreak()->addTester( atom );
- for( unsigned i=0; i<d_sygus_util->d_lemmas.size(); i++ ){
- Trace("dt-lemma-sygus") << "Sygus symmetry breaking lemma : " << d_sygus_util->d_lemmas[i] << std::endl;
- d_out->lemma( d_sygus_util->d_lemmas[i] );
+ d_sygus_sym_break->addTester( atom );
+ for( unsigned i=0; i<d_sygus_sym_break->d_lemmas.size(); i++ ){
+ Trace("dt-lemma-sygus") << "Sygus symmetry breaking lemma : " << d_sygus_sym_break->d_lemmas[i] << std::endl;
+ d_out->lemma( d_sygus_sym_break->d_lemmas[i] );
}
- d_sygus_util->d_lemmas.clear();
+ d_sygus_sym_break->d_lemmas.clear();
/*
if( d_sygus_util->d_conflict ){
//d_conflict = true;
flushPendingFacts();
}
+void TheoryDatatypes::finishInit() {
+ if( getQuantifiersEngine() && options::ceGuidedInst() ){
+ quantifiers::TermDbSygus * tds = getQuantifiersEngine()->getTermDatabaseSygus();
+ Assert( tds!=NULL );
+ d_sygus_split = new SygusSplit( tds );
+ d_sygus_sym_break = new SygusSymBreak( tds, getSatContext() );
+ }
+}
+
Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) {
switch( n.getKind() ){
case kind::APPLY_SELECTOR: {
#include "util/datatype.h"
#include "util/hash.h"
#include "theory/uf/equality_engine.h"
+#include "theory/datatypes/datatypes_sygus.h"
#include <ext/hash_set>
#include <iostream>
namespace theory {
namespace datatypes {
-class SygusUtil;
-
class TheoryDatatypes : public Theory {
private:
typedef context::CDChunkList<Node> NodeList;
unsigned d_dtfCounter;
/** expand definition skolem functions */
std::map< Node, Node > d_exp_def_skolem;
- /** sygus utility */
- SygusUtil * d_sygus_util;
+ /** sygus utilities */
+ SygusSplit * d_sygus_split;
+ SygusSymBreak * d_sygus_sym_break;
private:
/** assert fact */
void assertFact( Node fact, Node exp );
void check(Effort e);
void preRegisterTerm(TNode n);
+ void finishInit();
Node expandDefinition(LogicRequest &logicRequest, Node n);
Node ppRewrite(TNode n);
void presolve();
Node sol;
if( d_last_inst_si ){
Assert( d_conj->d_ceg_si );
- sol = d_conj->d_ceg_si->getSolution( d_quantEngine, i, Node::fromExpr( dt.getSygusVarList() ) );
+ sol = d_conj->d_ceg_si->getSolution( d_quantEngine, tn, i, Node::fromExpr( dt.getSygusVarList() ) );
}else{
if( !d_conj->d_candidate_inst[i].empty() ){
sol = d_conj->d_candidate_inst[i].back();
}
}
-Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, unsigned i, Node varList ){
+Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, TypeNode stn, unsigned i, Node varList ){
Assert( !d_lemmas_produced.empty() );
Node s = constructSolution( i, 0 );
//TODO : not in grammar
s = simplifySolution( qe, s, sassign, svars, ssubs, subs, 0 );
Trace("cegqi-si-debug-sol") << "Solution (post-simplification): " << s << std::endl;
s = Rewriter::rewrite( s );
- Trace("cegqi-si-debug-sol") << "Solution (pre-rewrite): " << s << std::endl;
+ Trace("cegqi-si-debug-sol") << "Solution (post-rewrite): " << s << std::endl;
d_solution = s;
+ if( options::cegqiSingleInvReconstruct() ){
+ collectReconstructNodes( qe->getTermDatabaseSygus(), d_solution, stn, Node::null(), TypeNode::null(), false );
+ std::vector< TypeNode > rcons_tn;
+ for( std::map< TypeNode, std::map< Node, bool > >::iterator it = d_rcons_to_process.begin(); it != d_rcons_to_process.end(); ++it ){
+ TypeNode tn = it->first;
+ Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ Trace("cegqi-si-rcons") << it->second.size() << " terms to reconstruct of type " << dt.getName() << " : " << std::endl;
+ for( std::map< Node, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+ Trace("cegqi-si-rcons") << " " << it2->first << std::endl;
+ }
+ Assert( !it->second.empty() );
+ rcons_tn.push_back( it->first );
+ }
+ /*
+ bool success;
+ unsigned index = 0;
+ do {
+ success = true;
+ std::vector< TypeNode > to_erase;
+ for( std::map< TypeNode, std::map< Node, bool > >::iterator it = d_rcons_to_process.begin(); it != d_rcons_to_process.end(); ++it ){
+ if( it->second.empty() ){
+ to_erase.push_back( it->first );
+ }else{
+ Node n = qe->getTermDatabase()->getEnumerateType( it->first, index );
+
+ success = false;
+ }
+ }
+ for( unsigned i=0; i<to_erase.size(); i++ ){
+ d_rcons_to_process.erase( to_erase[i] );
+ }
+ index++;
+ }while( !success );
+ */
+ }
if( Trace.isOn("cegqi-si-debug-sol") ){
//debug solution
if( !debugSolution( d_solution ) ){
}
+void CegConjectureSingleInv::collectReconstructNodes( TermDbSygus * tds, Node t, TypeNode stn, Node parent, TypeNode pstn, bool ignoreBoolean ) {
+ if( ignoreBoolean && t.getType().isBoolean() ){
+ if( t.getKind()==OR || t.getKind()==AND || t.getKind()==IFF || t.getKind()==ITE ){
+ for( unsigned i=0; i<t.getNumChildren(); i++ ){
+ collectReconstructNodes( tds, t[i], stn, parent, pstn, ignoreBoolean );
+ }
+ return;
+ }
+ }
+ if( std::find( d_rcons_processed[t].begin(), d_rcons_processed[t].end(), stn )==d_rcons_processed[t].end() ){
+ TypeNode tn = t.getType();
+ d_rcons_processed[t].push_back( stn );
+ Assert( datatypes::DatatypesRewriter::isTypeDatatype( stn ) );
+ const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
+ Assert( dt.isSygus() );
+ Trace("cegqi-si-rcons-debug") << "Check reconstruct " << t << " type " << tn << ", sygus type " << dt.getName() << std::endl;
+ tds->registerSygusType( stn );
+ int arg = tds->getKindArg( stn, t.getKind() );
+ bool processed = false;
+ if( arg!=-1 ){
+ if( t.getNumChildren()==dt[arg].getNumArgs() ){
+ Trace("cegqi-si-rcons-debug") << " Type has kind " << t.getKind() << ", recurse." << std::endl;
+ for( unsigned i=0; i<t.getNumChildren(); i++ ){
+ bool ignB = ( i==0 && t.getKind()==ITE );
+ TypeNode stnc = tds->getArgType( dt[arg], i );
+ collectReconstructNodes( tds, t[i], stnc, t, stn, ignB );
+ }
+ d_reconstructed[t][stn] = Node::fromExpr( dt[arg].getSygusOp() );
+ processed = true;
+ }else{
+ Trace("cegqi-si-rcons-debug") << " Type has kind " << t.getKind() << ", but argument mismatch, with parent " << parent << std::endl;
+ }
+ }
+ int carg = tds->getConstArg( stn, t );
+ if( carg==-1 ){
+ Trace("cegqi-si-rcons") << "...Reconstruction needed for " << t << " sygus type " << dt.getName() << " with parent " << parent << std::endl;
+ }else{
+ d_reconstructed[t][stn] = Node::fromExpr( dt[carg].getSygusOp() );
+ processed = true;
+ Trace("cegqi-si-rcons-debug") << " Type has constant." << std::endl;
+ }
+ //add to parent if necessary
+ if( !parent.isNull() && ( !processed || !d_rcons_graph[0][t][stn].empty() ) ){
+ Assert( !pstn.isNull() );
+ d_rcons_graph[0][parent][pstn][t][stn] = true;
+ d_rcons_to_process[pstn][parent] = true;
+ d_rcons_graph[1][t][stn][parent][pstn] = true;
+ d_rcons_to_process[stn][t] = true;
+ }
+ }
+}
+
+void CegConjectureSingleInv::setReconstructed( Node t, TypeNode stn ) {
+ if( Trace.isOn("cegqi-si-rcons-debug") ){
+ const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
+ Trace("cegqi-si-rcons-debug") << "set rcons : " << t << " in syntax " << dt.getName() << std::endl;
+ }
+ // clear all children, d_rcons_parents
+ std::vector< Node > to_set;
+ std::vector< TypeNode > to_set_tn;
+ for( unsigned r=0; r<2; r++){
+ unsigned ro = r==0 ? 1 : 0;
+ for( std::map< Node, std::map< TypeNode, bool > >::iterator it = d_rcons_graph[r][t][stn].begin(); it != d_rcons_graph[r][t][stn].end(); ++it ){
+ TypeNode stnc;
+ for( std::map< TypeNode, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+ stnc = it2->first;
+ d_rcons_graph[ro][it->first][stnc][t].erase( it2->first );
+ if( d_rcons_graph[ro][it->first][stnc][t].empty() ){
+ d_rcons_graph[ro][it->first][stnc].erase( t );
+ }
+ }
+ if( d_rcons_graph[ro][it->first][stnc].empty() ){
+ to_set.push_back( it->first );
+ to_set_tn.push_back( stnc );
+ }
+ }
+ }
+ for( unsigned r=0; r<2; r++){
+ d_rcons_graph[r].erase( t );
+ }
+ d_rcons_to_process[stn].erase( t );
+ for( unsigned i=0; i<to_set.size(); i++ ){
+ setReconstructed( to_set[i], to_set_tn[i] );
+ }
+}
+
+
+
}
\ No newline at end of file
void collectProgVars( Node n, std::vector< Node >& vars );
Node applyProgVarSubstitution( Node n, std::map< Node, int >& subs_from_model, std::vector< Node >& subs );
- bool debugSolution( Node sol );
- void debugTermSize( Node sol, int& t_size, int& num_ite );
- Node pullITEs( Node n );
- bool pullITECondition( Node root, Node n, std::vector< Node >& conj, Node& t, Node& rem, int depth );
- Node simplifySolution( QuantifiersEngine * qe, Node sol, std::map< Node, bool >& assign,
- std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& args, int status );
- bool getAssign( QuantifiersEngine * qe, bool pol, Node n, std::map< Node, bool >& assign, std::vector< Node >& new_assign,
- std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs, std::vector< Node >& args );
- bool getAssignEquality( QuantifiersEngine * qe, Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs, std::vector< Node >& args );
public:
CegConjectureSingleInv( Node q, CegConjecture * p );
// original conjecture
//check
void check( QuantifiersEngine * qe, std::vector< Node >& lems );
//get solution
- Node getSolution( QuantifiersEngine * qe, unsigned i, Node varList );
+ Node getSolution( QuantifiersEngine * qe, TypeNode stn, unsigned i, Node varList );
+
+
+//solution simplification
+private:
+ bool debugSolution( Node sol );
+ void debugTermSize( Node sol, int& t_size, int& num_ite );
+ Node pullITEs( Node n );
+ bool pullITECondition( Node root, Node n, std::vector< Node >& conj, Node& t, Node& rem, int depth );
+ Node simplifySolution( QuantifiersEngine * qe, Node sol, std::map< Node, bool >& assign,
+ std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& args, int status );
+ bool getAssign( QuantifiersEngine * qe, bool pol, Node n, std::map< Node, bool >& assign, std::vector< Node >& new_assign,
+ std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs, std::vector< Node >& args );
+ bool getAssignEquality( QuantifiersEngine * qe, Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs, std::vector< Node >& args );
+//solution reconstruction
+private:
+ std::map< Node, std::vector< TypeNode > > d_rcons_processed;
+ std::map< Node, std::map< TypeNode, Node > > d_reconstructed;
+ std::map< Node, std::map< TypeNode, std::map< Node, std::map< TypeNode, bool > > > > d_rcons_graph[2];
+ std::map< TypeNode, std::map< Node, bool > > d_rcons_to_process;
+ // term t with sygus type st
+ void collectReconstructNodes( TermDbSygus * tds, Node t, TypeNode stn, Node parent, TypeNode pstn, bool ignoreBoolean );
+ // set reconstructed
+ void setReconstructed( Node t, TypeNode stn );
};
}
#include "theory/quantifiers/ce_guided_instantiation.h"
#include "theory/quantifiers/rewrite_engine.h"
+//for sygus
+#include "theory/bv/theory_bv_utils.h"
+#include "util/bitvector.h"
+#include "smt/smt_engine_scope.h"
+
using namespace std;
using namespace CVC4;
using namespace CVC4::kind;
TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ) {
d_true = NodeManager::currentNM()->mkConst( true );
d_false = NodeManager::currentNM()->mkConst( false );
+ if( options::ceGuidedInst() ){
+ d_sygus_tdb = new TermDbSygus;
+ }else{
+ d_sygus_tdb = NULL;
+ }
}
/** ground terms */
return false;
}
-
bool TermDb::isRewriteRule( Node q ) {
return !getRewriteRule( q ).isNull();
}
return it->second;
}
}
+
+
+
+
+
+TNode TermDbSygus::getVar( TypeNode tn, int i ) {
+ while( i>=(int)d_fv[tn].size() ){
+ std::stringstream ss;
+ TypeNode vtn = tn;
+ if( datatypes::DatatypesRewriter::isTypeDatatype( tn ) ){
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ ss << "fv_" << dt.getName() << "_" << i;
+ if( !dt.getSygusType().isNull() ){
+ vtn = TypeNode::fromType( dt.getSygusType() );
+ }
+ }else{
+ 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[tn].push_back( v );
+ }
+ return d_fv[tn][i];
+}
+
+TNode TermDbSygus::getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count ) {
+ std::map< TypeNode, int >::iterator it = var_count.find( tn );
+ if( it==var_count.end() ){
+ var_count[tn] = 1;
+ return getVar( tn, 0 );
+ }else{
+ int index = it->second;
+ var_count[tn]++;
+ return getVar( tn, index );
+ }
+}
+
+TypeNode TermDbSygus::getSygusType( Node v ) {
+ Assert( d_fv_stype.find( v )!=d_fv_stype.end() );
+ return d_fv_stype[v];
+}
+
+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() );
+ Assert( !dt[c].getSygusOp().isNull() );
+ std::vector< Node > children;
+ Node op = Node::fromExpr( dt[c].getSygusOp() );
+ if( op.getKind()!=BUILTIN ){
+ children.push_back( op );
+ }
+ for( int i=0; i<(int)dt[c].getNumArgs(); i++ ){
+ TypeNode tna = TypeNode::fromType( ((SelectorType)dt[c][i].getType()).getRangeType() );
+ Node a;
+ std::map< int, Node >::iterator it = pre.find( i );
+ if( it!=pre.end() ){
+ a = it->second;
+ }else{
+ a = getVarInc( tna, var_count );
+ }
+ Assert( !a.isNull() );
+ children.push_back( a );
+ }
+ if( op.getKind()==BUILTIN ){
+ return NodeManager::currentNM()->mkNode( op, children );
+ }else{
+ if( children.size()==1 ){
+ return children[0];
+ }else{
+ return NodeManager::currentNM()->mkNode( APPLY, children );
+ /*
+ Node n = NodeManager::currentNM()->mkNode( APPLY, children );
+ //must expand definitions
+ Node ne = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( n.toExpr() ) );
+ Trace("sygus-util-debug") << "Expanded definitions in " << n << " to " << ne << std::endl;
+ return ne;
+ */
+ }
+ }
+}
+
+Node TermDbSygus::getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs ) {
+ return n;
+ if( n.getKind()==SKOLEM ){
+ std::map< Node, Node >::iterator its = subs.find( n );
+ if( its!=subs.end() ){
+ return its->second;
+ }else{
+ std::map< Node, TypeNode >::iterator it = d_fv_stype.find( n );
+ if( it!=d_fv_stype.end() ){
+ Node v = getVarInc( it->second, var_count );
+ subs[n] = v;
+ return v;
+ }else{
+ return n;
+ }
+ }
+ }else{
+ if( n.getNumChildren()>0 ){
+ std::vector< Node > children;
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.push_back( n.getOperator() );
+ }
+ bool childChanged = false;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ Node nc = getSygusNormalized( n[i], var_count, subs );
+ childChanged = childChanged || nc!=n[i];
+ children.push_back( nc );
+ }
+ if( childChanged ){
+ return NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }
+ }
+ return n;
+ }
+}
+
+Node TermDbSygus::getNormalized( TypeNode t, Node prog, bool do_pre_norm ) {
+ if( do_pre_norm ){
+ std::map< TypeNode, int > var_count;
+ std::map< Node, Node > subs;
+ prog = getSygusNormalized( prog, var_count, subs );
+ }
+ std::map< Node, Node >::iterator itn = d_normalized[t].find( prog );
+ if( itn==d_normalized[t].end() ){
+ Node progr = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( prog.toExpr() ) );
+ progr = Rewriter::rewrite( progr );
+ std::map< TypeNode, int > var_count;
+ std::map< Node, Node > subs;
+ progr = getSygusNormalized( progr, var_count, subs );
+ Trace("sygus-sym-break2") << "...rewrites to " << progr << std::endl;
+ d_normalized[t][prog] = progr;
+ return progr;
+ }else{
+ return itn->second;
+ }
+}
+
+int TermDbSygus::getTermSize( Node n ){
+ if( isVar( n ) ){
+ return 0;
+ }else{
+ int sum = 0;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ sum += getTermSize( n[i] );
+ }
+ return 1+sum;
+ }
+
+}
+
+bool TermDbSygus::isAssoc( Kind k ) {
+ return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
+ k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT;
+}
+
+bool TermDbSygus::isComm( Kind k ) {
+ return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
+ k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR;
+}
+
+bool TermDbSygus::isAntisymmetric( Kind k, Kind& dk ) {
+ if( k==GT ){
+ dk = LT;
+ return true;
+ }else if( k==GEQ ){
+ dk = LEQ;
+ return true;
+ }else if( k==BITVECTOR_UGT ){
+ dk = BITVECTOR_ULT;
+ return true;
+ }else if( k==BITVECTOR_UGE ){
+ dk = BITVECTOR_ULE;
+ return true;
+ }else if( k==BITVECTOR_SGT ){
+ dk = BITVECTOR_SLT;
+ return true;
+ }else if( k==BITVECTOR_SGE ){
+ dk = BITVECTOR_SLE;
+ return true;
+ }else{
+ return false;
+ }
+}
+
+bool TermDbSygus::isIdempotentArg( Node n, Kind ik, int arg ) {
+ TypeNode tn = n.getType();
+ if( n==getTypeValue( tn, 0 ) ){
+ if( ik==PLUS || ik==OR || ik==XOR || ik==BITVECTOR_PLUS || ik==BITVECTOR_OR || ik==BITVECTOR_XOR ){
+ return true;
+ }else if( ik==MINUS || ik==BITVECTOR_SHL || ik==BITVECTOR_LSHR || ik==BITVECTOR_SUB ){
+ return arg==1;
+ }
+ }else if( n==getTypeValue( tn, 1 ) ){
+ if( ik==MULT || ik==BITVECTOR_MULT ){
+ return true;
+ }else if( ik==DIVISION || ik==BITVECTOR_UDIV || ik==BITVECTOR_SDIV ){
+ return arg==1;
+ }
+ }else if( n==getTypeMaxValue( tn ) ){
+ if( ik==IFF || ik==BITVECTOR_AND || ik==BITVECTOR_XNOR ){
+ return true;
+ }
+ }
+ return false;
+}
+
+
+bool TermDbSygus::isSingularArg( Node n, Kind ik, int arg ) {
+ TypeNode tn = n.getType();
+ if( n==getTypeValue( tn, 0 ) ){
+ if( ik==AND || ik==MULT || ik==BITVECTOR_AND || ik==BITVECTOR_MULT ){
+ return true;
+ }else if( ik==DIVISION || ik==BITVECTOR_UDIV || ik==BITVECTOR_SDIV ){
+ return arg==0;
+ }
+ }else if( n==getTypeMaxValue( tn ) ){
+ if( ik==OR || ik==BITVECTOR_OR ){
+ return true;
+ }
+ }
+ return false;
+}
+
+bool TermDbSygus::hasOffsetArg( Kind ik, int arg, int& offset, Kind& ok ) {
+ if( ik==LT ){
+ Assert( arg==0 || arg==1 );
+ offset = arg==0 ? 1 : -1;
+ ok = LEQ;
+ return true;
+ }else if( ik==BITVECTOR_ULT ){
+ Assert( arg==0 || arg==1 );
+ offset = arg==0 ? 1 : -1;
+ ok = BITVECTOR_ULE;
+ return true;
+ }else if( ik==BITVECTOR_SLT ){
+ Assert( arg==0 || arg==1 );
+ offset = arg==0 ? 1 : -1;
+ ok = BITVECTOR_SLE;
+ return true;
+ }
+ return false;
+}
+
+
+Node TermDbSygus::getTypeValue( TypeNode tn, int val ) {
+ std::map< int, Node >::iterator it = d_type_value[tn].find( val );
+ if( it==d_type_value[tn].end() ){
+ Node n;
+ if( tn.isInteger() || tn.isReal() ){
+ Rational c(val);
+ n = NodeManager::currentNM()->mkConst( c );
+ }else if( tn.isBitVector() ){
+ unsigned int uv = val;
+ BitVector bval(tn.getConst<BitVectorSize>(), uv);
+ n = NodeManager::currentNM()->mkConst<BitVector>(bval);
+ }else if( tn.isBoolean() ){
+ if( val==0 ){
+ n = NodeManager::currentNM()->mkConst( false );
+ }
+ }
+ d_type_value[tn][val] = n;
+ return n;
+ }else{
+ return it->second;
+ }
+}
+
+Node TermDbSygus::getTypeMaxValue( TypeNode tn ) {
+ std::map< TypeNode, Node >::iterator it = d_type_max_value.find( tn );
+ if( it==d_type_max_value.end() ){
+ Node n;
+ if( tn.isBitVector() ){
+ n = bv::utils::mkOnes(tn.getConst<BitVectorSize>());
+ }else if( tn.isBoolean() ){
+ n = NodeManager::currentNM()->mkConst( true );
+ }
+ d_type_max_value[tn] = n;
+ return n;
+ }else{
+ return it->second;
+ }
+}
+
+Node TermDbSygus::getTypeValueOffset( TypeNode tn, Node val, int offset, int& status ) {
+ std::map< int, Node >::iterator it = d_type_value_offset[tn][val].find( offset );
+ if( it==d_type_value_offset[tn][val].end() ){
+ Node val_o;
+ Node offset_val = getTypeValue( tn, offset );
+ status = -1;
+ if( !offset_val.isNull() ){
+ if( tn.isInteger() || tn.isReal() ){
+ val_o = Rewriter::rewrite( NodeManager::currentNM()->mkNode( PLUS, val, offset_val ) );
+ status = 0;
+ }else if( tn.isBitVector() ){
+ val_o = Rewriter::rewrite( NodeManager::currentNM()->mkNode( BITVECTOR_PLUS, val, offset_val ) );
+ }
+ }
+ d_type_value_offset[tn][val][offset] = val_o;
+ d_type_value_offset_status[tn][val][offset] = status;
+ return val_o;
+ }else{
+ status = d_type_value_offset_status[tn][val][offset];
+ return it->second;
+ }
+}
+
+void TermDbSygus::registerSygusType( TypeNode tn ){
+ if( d_register.find( tn )==d_register.end() ){
+ if( !datatypes::DatatypesRewriter::isTypeDatatype( tn ) ){
+ d_register[tn] = TypeNode::null();
+ }else{
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ Trace("sygus-util") << "Register type " << dt.getName() << "..." << std::endl;
+ d_register[tn] = TypeNode::fromType( dt.getSygusType() );
+ if( d_register[tn].isNull() ){
+ Trace("sygus-util") << "...not sygus." << std::endl;
+ }else{
+ for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+ Expr sop = dt[i].getSygusOp();
+ Assert( !sop.isNull() );
+ Node n = Node::fromExpr( sop );
+ Trace("sygus-util") << " Operator #" << i << " : " << sop;
+ if( sop.getKind() == kind::BUILTIN ){
+ Kind sk = NodeManager::operatorToKind( n );
+ Trace("sygus-util") << ", kind = " << sk;
+ d_kinds[tn][sk] = i;
+ d_arg_kind[tn][i] = sk;
+ }else if( sop.isConst() ){
+ Trace("sygus-util") << ", constant";
+ d_consts[tn][n] = i;
+ d_arg_const[tn][i] = n;
+ }
+ d_ops[tn][n] = i;
+ d_arg_ops[tn][i] = n;
+ Trace("sygus-util") << std::endl;
+ }
+ }
+ }
+ }
+}
+
+bool TermDbSygus::isRegistered( TypeNode tn ) {
+ return d_register.find( tn )!=d_register.end();
+}
+
+int TermDbSygus::getKindArg( TypeNode tn, Kind k ) {
+ Assert( isRegistered( tn ) );
+ std::map< TypeNode, std::map< Kind, int > >::iterator itt = d_kinds.find( tn );
+ if( itt!=d_kinds.end() ){
+ std::map< Kind, int >::iterator it = itt->second.find( k );
+ if( it!=itt->second.end() ){
+ return it->second;
+ }
+ }
+ return -1;
+}
+
+int TermDbSygus::getConstArg( TypeNode tn, Node n ){
+ Assert( isRegistered( tn ) );
+ std::map< TypeNode, std::map< Node, int > >::iterator itt = d_consts.find( tn );
+ if( itt!=d_consts.end() ){
+ std::map< Node, int >::iterator it = itt->second.find( n );
+ if( it!=itt->second.end() ){
+ return it->second;
+ }
+ }
+ return -1;
+}
+
+int TermDbSygus::getOpArg( TypeNode tn, Node n ) {
+ std::map< Node, int >::iterator it = d_ops[tn].find( n );
+ if( it!=d_ops[tn].end() ){
+ return it->second;
+ }else{
+ return -1;
+ }
+}
+
+bool TermDbSygus::hasKind( TypeNode tn, Kind k ) {
+ return getKindArg( tn, k )!=-1;
+}
+bool TermDbSygus::hasConst( TypeNode tn, Node n ) {
+ return getConstArg( tn, n )!=-1;
+}
+bool TermDbSygus::hasOp( TypeNode tn, Node n ) {
+ return getOpArg( tn, n )!=-1;
+}
+
+Node TermDbSygus::getArgOp( TypeNode tn, int i ) {
+ Assert( isRegistered( tn ) );
+ std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_ops.find( tn );
+ if( itt!=d_arg_ops.end() ){
+ std::map< int, Node >::iterator itn = itt->second.find( i );
+ if( itn!=itt->second.end() ){
+ return itn->second;
+ }
+ }
+ return Node::null();
+}
+
+Node TermDbSygus::getArgConst( TypeNode tn, int i ) {
+ Assert( isRegistered( tn ) );
+ std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_const.find( tn );
+ if( itt!=d_arg_const.end() ){
+ std::map< int, Node >::iterator itn = itt->second.find( i );
+ if( itn!=itt->second.end() ){
+ return itn->second;
+ }
+ }
+ return Node::null();
+}
+
+Kind TermDbSygus::getArgKind( TypeNode tn, int i ) {
+ Assert( isRegistered( tn ) );
+ std::map< TypeNode, std::map< int, Kind > >::iterator itt = d_arg_kind.find( tn );
+ if( itt!=d_arg_kind.end() ){
+ std::map< int, Kind >::iterator itk = itt->second.find( i );
+ if( itk!=itt->second.end() ){
+ return itk->second;
+ }
+ }
+ return UNDEFINED_KIND;
+}
+
+bool TermDbSygus::isKindArg( TypeNode tn, int i ) {
+ return getArgKind( tn, i )!=UNDEFINED_KIND;
+}
+
+bool TermDbSygus::isConstArg( TypeNode tn, int i ) {
+ Assert( isRegistered( tn ) );
+ std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_const.find( tn );
+ if( itt!=d_arg_const.end() ){
+ return itt->second.find( i )!=itt->second.end();
+ }else{
+ return false;
+ }
+}
+
+TypeNode TermDbSygus::getArgType( const DatatypeConstructor& c, int i ) {
+ Assert( i>=0 && i<(int)c.getNumArgs() );
+ return TypeNode::fromType( ((SelectorType)c[i].getType()).getRangeType() );
+}
namespace inst{
class Trigger;
}
-namespace rrinst{
- class Trigger;
-}
-
namespace quantifiers {
class FullModelChecker;
}
+class TermDbSygus;
+
class TermDb {
friend class ::CVC4::theory::QuantifiersEngine;
friend class ::CVC4::theory::inst::Trigger;
- friend class ::CVC4::theory::rrinst::Trigger;
friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker;
typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
private:
/** simple check for contains term */
bool containsTerm( Node n, Node t );
+//for sygus
+private:
+ TermDbSygus * d_sygus_tdb;
+public:
+ TermDbSygus * getTermDatabaseSygus() { return d_sygus_tdb; }
+
private:
std::map< Node, bool > d_fun_defs;
public: //general queries concerning quantified formulas wrt modules
};/* class TermDb */
+class TermDbSygus {
+private:
+ std::map< TypeNode, std::vector< Node > > d_fv;
+ std::map< Node, TypeNode > d_fv_stype;
+public:
+ TNode getVar( TypeNode tn, int i );
+ TNode getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count );
+ bool isVar( Node n ) { return d_fv_stype.find( n )!=d_fv_stype.end(); }
+private:
+ //information for sygus types
+ std::map< TypeNode, TypeNode > d_register; //stores sygus type
+ std::map< TypeNode, std::map< int, Kind > > d_arg_kind;
+ std::map< TypeNode, std::map< Kind, int > > d_kinds;
+ std::map< TypeNode, std::map< int, Node > > d_arg_const;
+ 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;
+ //information for builtin types
+ std::map< TypeNode, std::map< int, Node > > d_type_value;
+ std::map< TypeNode, Node > d_type_max_value;
+ std::map< TypeNode, std::map< Node, std::map< int, Node > > > d_type_value_offset;
+ std::map< TypeNode, std::map< Node, std::map< int, int > > > d_type_value_offset_status;
+ //normalized map
+ std::map< TypeNode, std::map< Node, Node > > d_normalized;
+public:
+ TermDbSygus(){}
+ bool isRegistered( TypeNode tn );
+ int getKindArg( TypeNode tn, Kind k );
+ int getConstArg( TypeNode tn, Node n );
+ int getOpArg( TypeNode tn, Node n );
+ bool hasKind( TypeNode tn, Kind k );
+ bool hasConst( TypeNode tn, Node n );
+ bool hasOp( TypeNode tn, Node n );
+ Node getArgConst( TypeNode tn, int i );
+ Node getArgOp( TypeNode tn, int i );
+ Kind getArgKind( TypeNode tn, int i );
+ bool isKindArg( TypeNode tn, int i );
+ bool isConstArg( TypeNode tn, int i );
+ void registerSygusType( TypeNode tn );
+ /** get arg type */
+ TypeNode getArgType( const DatatypeConstructor& c, int i );
+ /** is assoc */
+ bool isAssoc( Kind k );
+ /** is comm */
+ bool isComm( Kind k );
+ /** isAntisymmetric */
+ bool isAntisymmetric( Kind k, Kind& dk );
+ /** is idempotent arg */
+ bool isIdempotentArg( Node n, Kind ik, int arg );
+ /** is singular arg */
+ bool isSingularArg( Node n, Kind ik, int arg );
+ /** get offset arg */
+ bool hasOffsetArg( Kind ik, int arg, int& offset, Kind& ok );
+ /** get value */
+ Node getTypeValue( TypeNode tn, int val );
+ /** get value */
+ Node getTypeValueOffset( TypeNode tn, Node val, int offset, int& status );
+ /** get value */
+ Node getTypeMaxValue( TypeNode tn );
+ TypeNode getSygusType( Node v );
+ Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre );
+ Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
+ Node getNormalized( TypeNode t, Node prog, bool do_pre_norm = false );
+ int getTermSize( Node n );
+};
+
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
return Node::null();
}
+quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() {
+ return getTermDatabase()->getTermDatabaseSygus();
+}
+
void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
std::set< Node > added;
getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure );
namespace quantifiers {
class TermDb;
+ class TermDbSygus;
}
class QuantifiersModule {
quantifiers::FirstOrderModel* getModel() { return d_model; }
/** get term database */
quantifiers::TermDb* getTermDatabase() { return d_term_db; }
+ /** get term database sygus */
+ quantifiers::TermDbSygus* getTermDatabaseSygus();
/** get trigger database */
inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
/** add term to database */
projects / cvc5.git / commitdiff