for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
Node prev = d_assertionsToPreprocess[i];
Trace("quantifiers-rewrite-debug") << "Pre-skolemize " << prev << "..." << std::endl;
- vector< Node > fvs;
- d_assertionsToPreprocess[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvs ) );
+ vector< TypeNode > fvTypes;
+ vector< TNode > fvs;
+ d_assertionsToPreprocess[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ) );
if( prev!=d_assertionsToPreprocess[i] ){
Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl;
Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess[i] << endl;
option rrOneInstPerRound --rr-one-inst-per-round bool :default false
add one instance of rewrite rule per round
+option dtStcInduction --dt-stc-ind bool :default false
+ apply strengthening for existential quantification over datatypes based on structural induction
+
endmodule
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/options.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/datatypes/datatypes_rewriter.h"
using namespace std;
using namespace CVC4;
}
}
-Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< Node >& fvs ){
+Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs ){
Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl;
if( n.getKind()==kind::NOT ){
- Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvs );
+ Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvTypes, fvs );
return nn.negate();
}else if( n.getKind()==kind::FORALL ){
if( polarity ){
- vector< Node > children;
- children.push_back( n[0] );
- //add children to current scope
- vector< Node > fvss;
- fvss.insert( fvss.begin(), fvs.begin(), fvs.end() );
- for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
- fvss.push_back( n[0][i] );
- }
- //process body
- children.push_back( preSkolemizeQuantifiers( n[1], polarity, fvss ) );
- if( n.getNumChildren()==3 ){
- children.push_back( n[2] );
+ if( options::preSkolemQuant() ){
+ vector< Node > children;
+ children.push_back( n[0] );
+ //add children to current scope
+ std::vector< TypeNode > fvt;
+ std::vector< TNode > fvss;
+ fvt.insert( fvt.begin(), fvTypes.begin(), fvTypes.end() );
+ fvss.insert( fvss.begin(), fvs.begin(), fvs.end() );
+ for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
+ fvt.push_back( n[0][i].getType() );
+ fvss.push_back( n[0][i] );
+ }
+ //process body
+ children.push_back( preSkolemizeQuantifiers( n[1], polarity, fvt, fvss ) );
+ if( n.getNumChildren()==3 ){
+ children.push_back( n[2] );
+ }
+ //return processed quantifier
+ return NodeManager::currentNM()->mkNode( kind::FORALL, children );
}
- //return processed quantifier
- return NodeManager::currentNM()->mkNode( kind::FORALL, children );
}else{
//process body
- Node nn = preSkolemizeQuantifiers( n[1], polarity, fvs );
- //now, substitute skolems for the variables
- vector< TypeNode > argTypes;
- for( int i=0; i<(int)fvs.size(); i++ ){
- argTypes.push_back( fvs[i].getType() );
- }
- //calculate the variables and substitution
- vector< Node > vars;
- vector< Node > subs;
- for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
- vars.push_back( n[0][i] );
- }
- for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
- //make the new function symbol
- if( argTypes.empty() ){
- Node s = NodeManager::currentNM()->mkSkolem( "sk", n[0][i].getType(), "created during pre-skolemization" );
- subs.push_back( s );
- }else{
- TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, n[0][i].getType() );
- Node op = NodeManager::currentNM()->mkSkolem( "skop", typ, "op created during pre-skolemization" );
- //DOTHIS: set attribute on op, marking that it should not be selected as trigger
- vector< Node > funcArgs;
- funcArgs.push_back( op );
- funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() );
- subs.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs ) );
- }
- }
- //apply substitution
- nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
- return nn;
+ Node nn = preSkolemizeQuantifiers( n[1], polarity, fvTypes, fvs );
+ std::vector< Node > sk;
+ //return skolemized body
+ return TermDb::mkSkolemizedBody( n, nn, fvTypes, fvs, sk );
}
}else{
//check if it contains a quantifier as a subterm
}else if( n.getKind()==kind::IMPLIES ){
nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
}
- return preSkolemizeQuantifiers( nn, polarity, fvs );
+ return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs );
}else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
vector< Node > children;
for( int i=0; i<(int)n.getNumChildren(); i++ ){
- children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) );
+ children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvTypes, fvs ) );
}
return NodeManager::currentNM()->mkNode( n.getKind(), children );
- }else{
- //must pull ite's
}
}
}
- return n;
}
+ return n;
+}
+
+bool QuantifiersRewriter::isDtStrInductionQuantifier( Node q ){
+ Assert( q.getKind()==FORALL );
+ return q[0].getNumChildren()==1 && datatypes::DatatypesRewriter::isTermDatatype( q[0][0] );
}
public:
static Node rewriteRewriteRule( Node r );
static bool containsQuantifiers(Node n);
- static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector<Node>& fvs);
-public:
- //static Node rewriteQuants( Node n, bool isNested = false );
- //static Node rewriteQuant( Node n, bool isNested = false );
+ static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
+private:
+ static bool isDtStrInductionQuantifier( Node q );
};/* class QuantifiersRewriter */
}/* CVC4::theory::quantifiers namespace */
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/options.h"
#include "theory/quantifiers/theory_quantifiers.h"
+#include "util/datatype.h"
+#include "theory/datatypes/datatypes_rewriter.h"
using namespace std;
using namespace CVC4;
}
+void getSelfSel( const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){
+ for( unsigned j=0; j<dc.getNumArgs(); j++ ){
+ TypeNode tn = TypeNode::fromType( ((SelectorType)dc[j].getSelector().getType()).getRangeType() );
+ std::vector< Node > ssc;
+ if( tn==ntn ){
+ ssc.push_back( n );
+ }
+ /* TODO
+ else if( datatypes::DatatypesRewriter::isTypeDatatype( tn ) && std::find( visited.begin(), visited.end(), tn )==visited.end() ){
+ visited.push_back( tn );
+ const Datatype& dt = ((DatatypeType)(subs[0].getType()).toType()).getDatatype();
+ std::vector< Node > disj;
+ for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+ getSelfSel( dt[i], n, ntn, ssc );
+ }
+ visited.pop_back();
+ }
+ */
+ for( unsigned k=0; k<ssc.size(); k++ ){
+ selfSel.push_back( NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, dc[j].getSelector(), n ) );
+ }
+ }
+}
+
+
+Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes, std::vector< TNode >& fvs,
+ std::vector< Node >& sk ) {
+ //calculate the variables and substitution
+ std::vector< TNode > ind_vars;
+ std::vector< unsigned > ind_var_indicies;
+ std::vector< TNode > vars;
+ std::vector< unsigned > var_indicies;
+ for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+ if( options::dtStcInduction() && datatypes::DatatypesRewriter::isTermDatatype( f[0][i] ) ){
+ ind_vars.push_back( f[0][i] );
+ ind_var_indicies.push_back( i );
+ }else{
+ vars.push_back( f[0][i] );
+ var_indicies.push_back( i );
+ }
+ Node s;
+ //make the new function symbol
+ if( argTypes.empty() ){
+ s = NodeManager::currentNM()->mkSkolem( "skv", f[0][i].getType(), "created during skolemization" );
+ }else{
+ TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, f[0][i].getType() );
+ Node op = NodeManager::currentNM()->mkSkolem( "skop", typ, "op created during pre-skolemization" );
+ //DOTHIS: set attribute on op, marking that it should not be selected as trigger
+ std::vector< Node > funcArgs;
+ funcArgs.push_back( op );
+ funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() );
+ s = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs );
+ }
+ sk.push_back( s );
+ }
+ Node ret;
+ if( vars.empty() ){
+ ret = n;
+ }else{
+ std::vector< Node > var_sk;
+ for( unsigned i=0; i<var_indicies.size(); i++ ){
+ var_sk.push_back( sk[var_indicies[i]] );
+ }
+ Assert( vars.size()==var_sk.size() );
+ ret = n.substitute( vars.begin(), vars.end(), var_sk.begin(), var_sk.end() );
+ }
+ if( !ind_vars.empty() ){
+ Trace("stc-ind") << "Ind strengthen : (not " << f << ")" << std::endl;
+ Trace("stc-ind") << "Skolemized is : " << ret << std::endl;
+ for( unsigned v=0; v<ind_vars.size(); v++ ){
+ Node k = sk[ind_var_indicies[v]];
+ TypeNode tn = k.getType();
+ if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
+ //can strengthen this, by asserting that subs[0] is the smallest term such that the existential holds.
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ std::vector< Node > disj;
+ for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+ std::vector< Node > conj;
+ conj.push_back( NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), k ).negate() );
+ std::vector< Node > selfSel;
+ getSelfSel( dt[i], k, tn, selfSel );
+ for( unsigned j=0; j<selfSel.size(); j++ ){
+ conj.push_back( ret.substitute( ind_vars[v], selfSel[j] ).negate() );
+ }
+ disj.push_back( conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( OR, conj ) );
+ }
+ Assert( !disj.empty() );
+ Node n_str_ind = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( AND, disj );
+ Trace("stc-ind") << "Strengthening is : " << n_str_ind << std::endl;
+
+ Node nret = ret.substitute( ind_vars[v], k );
+ ret = NodeManager::currentNM()->mkNode( OR, nret, n_str_ind );
+ }else{
+ Assert( false );
+ }
+ }
+ }
+
+ return ret;
+}
Node TermDb::getSkolemizedBody( Node f ){
Assert( f.getKind()==FORALL );
if( d_skolem_body.find( f )==d_skolem_body.end() ){
- std::vector< Node > vars;
- for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
- Node skv = NodeManager::currentNM()->mkSkolem( "skv", f[0][i].getType(), "is a termdb-created skolemized body" );
- d_skolem_constants[ f ].push_back( skv );
- vars.push_back( f[0][i] );
- //carry information for sort inference
- if( options::sortInference() ){
- d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], skv );
+ std::vector< TypeNode > fvTypes;
+ std::vector< TNode > fvs;
+ d_skolem_body[ f ] = mkSkolemizedBody( f, f[1], fvTypes, fvs, d_skolem_constants[f] );
+ Assert( d_skolem_constants.size()==f[0].getNumChildren() );
+ if( options::sortInference() ){
+ for( unsigned i=0; i<d_skolem_constants[f].size(); i++ ){
+ //carry information for sort inference
+ d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], d_skolem_constants[f][i] );
}
}
- d_skolem_body[ f ] = f[ 1 ].substitute( vars.begin(), vars.end(),
- d_skolem_constants[ f ].begin(), d_skolem_constants[ f ].end() );
}
return d_skolem_body[ f ];
}
/** map from universal quantifiers to their skolemized body */
std::map< Node, Node > d_skolem_body;
public:
- /** get the skolemized body f[e/x] */
- Node getSkolemizedBody( Node f );
+ /** make the skolemized body f[e/x] */
+ static Node mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs,
+ std::vector< Node >& sk );
+ /** get the skolemized body */
+ Node getSkolemizedBody( Node f);
//miscellaneous
public:
void TheoryQuantifiers::assertExistential( Node n ){
Assert( n.getKind()== NOT && n[0].getKind()==FORALL );
- if( options::recurseCbqi() || !TermDb::hasInstConstAttr(n[0]) ){
+ if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n[0]) ){
if( d_skolemized.find( n )==d_skolemized.end() ){
Node body = getQuantifiersEngine()->getTermDatabase()->getSkolemizedBody( n[0] );
NodeBuilder<> nb(kind::OR);
projects / cvc5.git / commitdiff