summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/fmf/model_builder.cpp1
-rw-r--r--src/theory/quantifiers/fun_def_process.cpp356
-rw-r--r--src/theory/quantifiers/fun_def_process.h93
-rw-r--r--src/theory/quantifiers/quantifiers_attributes.h9
4 files changed, 9 insertions, 450 deletions
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index d41cd7310..796ee85fa 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -17,7 +17,6 @@
#include "options/quantifiers_options.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/fmf/model_engine.h"
-#include "theory/quantifiers/fun_def_process.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quant_rep_bound_ext.h"
#include "theory/quantifiers_engine.h"
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
deleted file mode 100644
index 350da8003..000000000
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ /dev/null
@@ -1,356 +0,0 @@
-/********************* */
-/*! \file fun_def_process.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Haniel Barbosa, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Sort inference module
- **
- ** This class implements pre-process steps for admissible recursive function definitions (Reynolds et al IJCAR2016)
- **/
-
-#include "theory/quantifiers/fun_def_process.h"
-
-#include <vector>
-
-#include "options/smt_options.h"
-#include "proof/proof_manager.h"
-#include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
-
-using namespace CVC4;
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::kind;
-
-
-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
- NodeManager* nm = NodeManager::currentNM();
- for( unsigned i=0; i<assertions.size(); i++ ){
- Node n = QuantAttributes::getFunDefHead( assertions[i] );
- if( !n.isNull() ){
- Assert(n.getKind() == APPLY_UF);
- Node f = n.getOperator();
-
- //check if already defined, if so, throw error
- if( d_sorts.find( f )!=d_sorts.end() ){
- Message() << "Cannot define function " << f << " more than once." << std::endl;
- AlwaysAssert(false);
- }
-
- Node bd = QuantAttributes::getFunDefBody( assertions[i] );
- Trace("fmf-fun-def-debug") << "Process function " << n << ", body = " << bd << std::endl;
- if( !bd.isNull() ){
- d_funcs.push_back( f );
- bd = NodeManager::currentNM()->mkNode( EQUAL, n, bd );
-
- //create a sort S that represents the inputs of the function
- std::stringstream ss;
- ss << "I_" << f;
- TypeNode iType = NodeManager::currentNM()->mkSort( ss.str() );
- AbsTypeFunDefAttribute atfda;
- iType.setAttribute(atfda,true);
- d_sorts[f] = iType;
-
- //create functions f1...fn mapping from this sort to concrete elements
- for( unsigned j=0; j<n.getNumChildren(); j++ ){
- TypeNode typ = NodeManager::currentNM()->mkFunctionType( iType, n[j].getType() );
- std::stringstream ssf;
- ssf << f << "_arg_" << j;
- d_input_arg_inj[f].push_back(
- nm->mkSkolem(ssf.str(), typ, "op created during fun def fmf"));
- }
-
- //construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn]
- std::vector< Node > children;
- Node bv = NodeManager::currentNM()->mkBoundVar("?i", iType );
- Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bv );
- std::vector< Node > subs;
- std::vector< Node > vars;
- for( unsigned j=0; j<n.getNumChildren(); j++ ){
- vars.push_back( n[j] );
- subs.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], bv ) );
- }
- bd = bd.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
- subs_head[i] = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-
- Trace("fmf-fun-def") << "FMF fun def: FUNCTION : rewrite " << assertions[i] << std::endl;
- Trace("fmf-fun-def") << " to " << std::endl;
- Node new_q = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
- new_q = Rewriter::rewrite( new_q );
- if (options::unsatCores())
- {
- ProofManager::currentPM()->addDependence(new_q, assertions[i]);
- }
- assertions[i] = new_q;
- Trace("fmf-fun-def") << " " << assertions[i] << std::endl;
- fd_assertions.push_back( i );
- }else{
- //can be, e.g. in corner cases forall x. f(x)=f(x), forall x. f(x)=f(x)+1
- }
- }
- }
- //second pass : rewrite assertions
- 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++ ){
- bool is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end();
- std::vector<Node> constraints;
- 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);
- Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i]
- << std::endl;
- Trace("fmf-fun-def-rewrite") << " to " << std::endl;
- Trace("fmf-fun-def-rewrite") << " " << n << std::endl;
- if (options::unsatCores())
- {
- ProofManager::currentPM()->addDependence(n, assertions[i]);
- }
- assertions[i] = n;
- }
- }
-}
-
-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 ? 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]
- std::map< Node, Node >::iterator itvc = visited_cons[index].find( n );
- if( itvc != visited_cons[index].end() ){
- constraints.push_back( itvc->second );
- }
- return itv->second;
- }else{
- Node ret;
- Trace("fmf-fun-def-debug2") << "Simplify " << n << " " << pol << " " << hasPol << " " << is_fun_def << std::endl;
- if( n.getKind()==FORALL ){
- Node c = simplifyFormula( n[1], pol, hasPol, constraints, hd, is_fun_def, visited, visited_cons );
- //append prenex to constraints
- for( unsigned i=0; i<constraints.size(); i++ ){
- constraints[i] = NodeManager::currentNM()->mkNode( FORALL, n[0], constraints[i] );
- constraints[i] = Rewriter::rewrite( constraints[i] );
- }
- if( c!=n[1] ){
- ret = NodeManager::currentNM()->mkNode( FORALL, n[0], c );
- }else{
- ret = n;
- }
- }else{
- Node nn = n;
- bool isBool = n.getType().isBoolean();
- 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 || 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, 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 );
- childChanged = c!=n[i] || childChanged;
- }
- 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, Node> visitedT;
- getConstraints(n, constraints, visitedT);
- }
- if( !constraints.empty() && isBool && hasPol ){
- //conjoin with current
- Node cons = constraints.size()==1 ? constraints[0] : NodeManager::currentNM()->mkNode( AND, constraints );
- if( pol ){
- ret = NodeManager::currentNM()->mkNode( AND, nn, cons );
- }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;
- }
- }
- if( !constraints.empty() ){
- Node cons;
- //flatten to AND node for the purposes of caching
- if( constraints.size()>1 ){
- cons = NodeManager::currentNM()->mkNode( AND, constraints );
- cons = Rewriter::rewrite( cons );
- constraints.clear();
- constraints.push_back( cons );
- }else{
- cons = constraints[0];
- }
- visited_cons[index][n] = cons;
- Assert(constraints.size() == 1 && constraints[0] == cons);
- }
- visited[index][n] = ret;
- return ret;
- }
-}
-
-void FunDefFmf::getConstraints(Node n,
- std::vector<Node>& constraints,
- std::map<Node, Node>& visited)
-{
- std::map<Node, Node>::iterator itv = visited.find(n);
- if (itv != visited.end())
- {
- // already visited
- if (!itv->second.isNull())
- {
- // add the cached constraint if it does not already occur
- if (std::find(constraints.begin(), constraints.end(), itv->second)
- == constraints.end())
- {
- constraints.push_back(itv->second);
- }
- }
- return;
- }
- visited[n] = Node::null();
- std::vector<Node> currConstraints;
- NodeManager* nm = NodeManager::currentNM();
- if (n.getKind() == ITE)
- {
- // collect constraints for the condition
- getConstraints(n[0], currConstraints, visited);
- // collect constraints for each branch
- Node cs[2];
- for (unsigned i = 0; i < 2; i++)
- {
- std::vector<Node> ccons;
- getConstraints(n[i + 1], ccons, visited);
- cs[i] = ccons.empty()
- ? nm->mkConst(true)
- : (ccons.size() == 1 ? ccons[0] : nm->mkNode(AND, ccons));
- }
- if (!cs[0].isConst() || !cs[1].isConst())
- {
- Node itec = nm->mkNode(ITE, n[0], cs[0], cs[1]);
- currConstraints.push_back(itec);
- Trace("fmf-fun-def-debug")
- << "---> add constraint " << itec << " for " << n << std::endl;
- }
- }
- else
- {
- if (n.getKind() == APPLY_UF)
- {
- // check if f is defined, if so, we must enforce domain constraints for
- // this f-application
- Node f = n.getOperator();
- std::map<Node, TypeNode>::iterator it = d_sorts.find(f);
- if (it != d_sorts.end())
- {
- // create existential
- Node z = nm->mkBoundVar("?z", it->second);
- Node bvl = nm->mkNode(BOUND_VAR_LIST, z);
- std::vector<Node> children;
- for (unsigned j = 0, size = n.getNumChildren(); j < size; j++)
- {
- Node uz = nm->mkNode(APPLY_UF, d_input_arg_inj[f][j], z);
- children.push_back(uz.eqNode(n[j]));
- }
- Node bd =
- children.size() == 1 ? children[0] : nm->mkNode(AND, children);
- bd = bd.negate();
- Node ex = nm->mkNode(FORALL, bvl, bd);
- ex = ex.negate();
- currConstraints.push_back(ex);
- Trace("fmf-fun-def-debug")
- << "---> add constraint " << ex << " for " << n << std::endl;
- }
- }
- for (const Node& cn : n)
- {
- getConstraints(cn, currConstraints, visited);
- }
- }
- // set the visited cache
- if (!currConstraints.empty())
- {
- Node finalc = currConstraints.size() == 1
- ? currConstraints[0]
- : nm->mkNode(AND, currConstraints);
- visited[n] = finalc;
- // add to constraints
- getConstraints(n, constraints, visited);
- }
-}
diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h
deleted file mode 100644
index 1f687d4f3..000000000
--- a/src/theory/quantifiers/fun_def_process.h
+++ /dev/null
@@ -1,93 +0,0 @@
-/********************* */
-/*! \file fun_def_process.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Pre-process step for admissible recursively defined functions
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__QUANTIFIERS_FUN_DEF_PROCESS_H
-#define CVC4__QUANTIFIERS_FUN_DEF_PROCESS_H
-
-#include <map>
-#include <vector>
-#include "expr/attribute.h"
-#include "expr/node.h"
-#include "expr/type_node.h"
-
-namespace CVC4 {
-namespace theory {
-
-/**
- * Attribute marked true for types that are used as abstraction types in
- * the algorithm below.
- */
-struct AbsTypeFunDefAttributeId
-{
-};
-typedef expr::Attribute<AbsTypeFunDefAttributeId, bool> AbsTypeFunDefAttribute;
-
-namespace quantifiers {
-
-//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 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 );
-public:
- FunDefFmf(){}
- ~FunDefFmf(){}
- //defined functions to input sort (alpha)
- std::map< Node, TypeNode > d_sorts;
- //defined functions to injections input -> argument elements (gamma)
- std::map< Node, std::vector< Node > > d_input_arg_inj;
- // (newly) defined functions
- std::vector< Node > d_funcs;
- /** 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 );
- /** get constraints
- *
- * This computes constraints for the final else branch of A_0 in Figure 1
- * of Reynolds et al "Model Finding for Recursive Functions". The range of
- * the cache visited stores the constraint (if any) for each node.
- */
- void getConstraints(Node n,
- std::vector<Node>& constraints,
- std::map<Node, Node>& visited);
-};
-
-
-}
-}
-}
-
-#endif
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 88f291b2b..9fdb127e6 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -89,6 +89,15 @@ typedef expr::Attribute<SygusVarToTermAttributeId, Node>
SygusVarToTermAttribute;
/**
+ * Attribute marked true for types that are used as abstraction types in
+ * the finite model finding for function definitions algorithm.
+ */
+struct AbsTypeFunDefAttributeId
+{
+};
+typedef expr::Attribute<AbsTypeFunDefAttributeId, bool> AbsTypeFunDefAttribute;
+
+/**
* Attribute true for quantifiers that have been internally generated, e.g.
* for reductions of string operators.
*
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback