From f625c0b8dbab3830198e6ad4ea9748cecd301389 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 2 May 2014 07:11:08 -0500 Subject: [PATCH] Add option --dt-stc-ind for strengthening skolemization. Refactor skolemization. --- src/smt/smt_engine.cpp | 5 +- src/theory/quantifiers/options | 3 + .../quantifiers/quantifiers_rewriter.cpp | 85 +++++-------- src/theory/quantifiers/quantifiers_rewriter.h | 7 +- src/theory/quantifiers/term_database.cpp | 120 ++++++++++++++++-- src/theory/quantifiers/term_database.h | 7 +- src/theory/quantifiers/theory_quantifiers.cpp | 2 +- 7 files changed, 159 insertions(+), 70 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6dd1f4465..a411530e6 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2893,8 +2893,9 @@ void SmtEnginePrivate::processAssertions() { 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; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index f4acfb926..10c538dd9 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -134,4 +134,7 @@ option quantRewriteRules --rewrite-rules bool :default true 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 diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 6af42e159..38fc1d919 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -15,6 +15,7 @@ #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; @@ -1115,60 +1116,39 @@ bool QuantifiersRewriter::containsQuantifiers(Node n) { } } -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 @@ -1189,18 +1169,21 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v }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] ); } diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 4cbdb0cd1..0cb76f686 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -83,10 +83,9 @@ private: public: static Node rewriteRewriteRule( Node r ); static bool containsQuantifiers(Node n); - static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector& 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& fvs); +private: + static bool isDtStrInductionQuantifier( Node q ); };/* class QuantifiersRewriter */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 3168d21a0..67e3fa0e9 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -19,6 +19,8 @@ #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; @@ -407,22 +409,120 @@ Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector & var } +void getSelfSel( const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){ + for( unsigned j=0; j 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; imkNode( 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; imkSkolem( "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 disj; + for( unsigned i=0; i 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; jmkNode( 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; igetTheoryEngine()->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 ]; } diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 757a76baa..2a72cf808 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -203,8 +203,11 @@ private: /** 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: diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 19a915ae9..5802632da 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -157,7 +157,7 @@ void TheoryQuantifiers::assertUniversal( Node n ){ 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); -- 2.30.2