**
** \brief Sort inference module
**
- ** This class implements pre-process steps for well-defined functions
+ ** This class implements pre-process steps for admissible recursive function definitions (Reynolds et al IJCAR2016)
**/
#include <vector>
using namespace CVC4::kind;
-void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
+void FunDefFmf::simplify( std::vector< Node >& assertions ) {
std::vector< int > fd_assertions;
std::map< int, Node > subs_head;
//first pass : find defined functions, transform quantifiers
std::map< int, std::map< Node, Node > > visited;
std::map< int, std::map< Node, Node > > visited_cons;
for( unsigned i=0; i<assertions.size(); i++ ){
- int is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end() ? 1 : 0;
+ bool is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end();
//constant boolean function definitions do not add domain constraints
- if( is_fd==0 || ( is_fd==1 && assertions[i][1].getKind()==EQUAL ) ){
+ if( !is_fd || ( is_fd && assertions[i][1].getKind()==EQUAL ) ){
std::vector< Node > constraints;
- Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i] << ", is_fd = " << is_fd << std::endl;
- Node n = simplifyFormula( assertions[i], true, true, constraints, is_fd==1 ? subs_head[i] : Node::null(), is_fd, visited, visited_cons );
+ Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i] << ", is function definition = " << is_fd << std::endl;
+ Node n = simplifyFormula( assertions[i], true, true, constraints, is_fd ? subs_head[i] : Node::null(), is_fd, visited, visited_cons );
Assert( constraints.empty() );
if( n!=assertions[i] ){
n = Rewriter::rewrite( n );
}
}
-//is_fun_def 1 : top of fun-def, 2 : top of fun-def body, 0 : not top
-Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, int is_fun_def,
+Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, bool is_fun_def,
std::map< int, std::map< Node, Node > >& visited,
std::map< int, std::map< Node, Node > >& visited_cons ) {
Assert( constraints.empty() );
- int index = is_fun_def + 3*( hasPol ? ( pol ? 1 : -1 ) : 0 );
+ int index = ( is_fun_def ? 1 : 0 ) + 2*( hasPol ? ( pol ? 1 : -1 ) : 0 );
std::map< Node, Node >::iterator itv = visited[index].find( n );
if( itv!=visited[index].end() ){
//constraints.insert( visited_cons[index]
}else{
Node nn = n;
bool isBool = n.getType().isBoolean();
- if( isBool && n.getKind()!=APPLY_UF && is_fun_def!=2 ){
+ if( isBool && n.getKind()!=APPLY_UF ){
std::vector< Node > children;
bool childChanged = false;
+ // are we at a branch position (not all children are necessarily relevant)?
+ bool branch_pos = ( n.getKind()==ITE || n.getKind()==OR || n.getKind()==AND );
+ std::vector< Node > branch_constraints;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
Node c = n[i];
//do not process LHS of definition
- if( is_fun_def!=1 || c!=hd ){
+ if( !is_fun_def || c!=hd ){
bool newHasPol;
bool newPol;
QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
//get child constraints
std::vector< Node > cconstraints;
- c = simplifyFormula( n[i], newPol, newHasPol, cconstraints, hd, is_fun_def==1 ? 2 : 0, visited, visited_cons );
+ c = simplifyFormula( n[i], newPol, newHasPol, cconstraints, hd, false, visited, visited_cons );
+ if( branch_pos ){
+ // if at a branching position, the other constraints don't matter if this is satisfied
+ Node bcons = cconstraints.empty() ? NodeManager::currentNM()->mkConst( true ) :
+ ( cconstraints.size()==1 ? cconstraints[0] : NodeManager::currentNM()->mkNode( AND, cconstraints ) );
+ branch_constraints.push_back( bcons );
+ Trace("fmf-fun-def-debug2") << "Branching constraint at arg " << i << " is " << bcons << std::endl;
+ }
constraints.insert( constraints.end(), cconstraints.begin(), cconstraints.end() );
}
children.push_back( c );
if( childChanged ){
nn = NodeManager::currentNM()->mkNode( n.getKind(), children );
}
+ if( branch_pos && !constraints.empty() ){
+ // if we are at a branching position in the formula, we can
+ // minimize recursive constraints on recursively defined predicates if we know one child forces
+ // the overall evaluation of this formula.
+ Node branch_cond;
+ if( n.getKind()==ITE ){
+ // always care about constraints on the head of the ITE, but only care about one of the children depending on how it evaluates
+ branch_cond = NodeManager::currentNM()->mkNode( kind::AND, branch_constraints[0],
+ NodeManager::currentNM()->mkNode( kind::ITE, n[0], branch_constraints[1], branch_constraints[2] ) );
+ }else{
+ // in the default case, we care about all conditions
+ branch_cond = constraints.size()==1 ? constraints[0] : NodeManager::currentNM()->mkNode( AND, constraints );
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ // if this child holds with forcing polarity (true child of OR or false child of AND),
+ // then we only care about its associated recursive conditions
+ branch_cond = NodeManager::currentNM()->mkNode( kind::ITE,
+ ( n.getKind()==OR ? n[i] : n[i].negate() ), branch_constraints[i], branch_cond );
+ }
+ }
+ Trace("fmf-fun-def-debug2") << "Made branching condition " << branch_cond << std::endl;
+ constraints.clear();
+ constraints.push_back( branch_cond );
+ }
}else{
//simplify term
std::map< Node, bool > visited;
}else{
ret = NodeManager::currentNM()->mkNode( OR, nn, cons.negate() );
}
+ Trace("fmf-fun-def-debug2") << "Add constraint to obtain " << ret << std::endl;
constraints.clear();
}else{
ret = nn;
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
- ** \brief Pre-process steps for well-defined functions
+ ** \brief Pre-process step for admissible recursively defined functions
**/
#include "cvc4_private.h"
namespace theory {
namespace quantifiers {
-//find finite models for well-defined functions
+//Preprocessing pass to allow finite model finding for admissible recursive function definitions
+// For details, see Reynolds et al "Model Finding for Recursive Functions" IJCAR 2016
class FunDefFmf {
private:
- //simplify
- Node simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, int is_fun_def,
+ /** simplify formula
+ * This is A_0 in Figure 1 of Reynolds et al "Model Finding for Recursive Functions".
+ * The input of A_0 in that paper is a pair ( term t, polarity p )
+ * The return value of A_0 in that paper is a pair ( term t', set of formulas X ).
+ *
+ * This function implements this such that :
+ * n is t
+ * pol/hasPol is p
+ * the return value is t'
+ * the set of formulas X are stored in "constraints"
+ *
+ * Additionally, is_fun_def is whether we are currently processing the top of a function defintion,
+ * since this affects whether we process the head of the definition.
+ */
+ Node simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, bool is_fun_def,
std::map< int, std::map< Node, Node > >& visited,
std::map< int, std::map< Node, Node > >& visited_cons );
- //simplify term
+ /** simplify term
+ * This computes constraints for the final else branch of A_0 in Figure 1
+ * of Reynolds et al "Model Finding for Recursive Functions".
+ */
void simplifyTerm( Node n, std::vector< Node >& constraints, std::map< Node, bool >& visited );
public:
FunDefFmf(){}
std::map< Node, std::vector< Node > > d_input_arg_inj;
// (newly) defined functions
std::vector< Node > d_funcs;
- //simplify
- void simplify( std::vector< Node >& assertions, bool doRewrite = false );
+ /** simplify, which does the following:
+ * (1) records all top-level recursive function definitions in assertions,
+ * (2) runs Figure 1 of Reynolds et al "Model Finding for Recursive Functions"
+ * IJCAR 2016 on all formulas in assertions based on the definitions from part (1),
+ * which are Sigma^{dfn} in that paper.
+ */
+ void simplify( std::vector< Node >& assertions );
};
projects / cvc5.git / commitdiff