diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-04 00:21:01 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-07-03 22:21:01 -0700 |
commit | fad7a9aafa35210bb8b685261ec1caae2c7e0624 (patch) | |
tree | 71e410d4778ac9fe463a2dad3dcb2b267a0a6797 | |
parent | 45a5d525d26dba9ed3f12d888c8b9fb844c8a8ec (diff) |
Fix fmf-fun for non-equality function definitions (#2134)
Fixes #2133. In that issue, a quantifiers rewrite triggered a model-unsoundness in fmf-fun. The rewrite made a function definition have an ITE at top-level instead of equality. The corrected code was model-unsound, since it assumed that quantified formulas that are not EQUAL can be ignored.
-rw-r--r-- | src/theory/quantifiers/fun_def_process.cpp | 36 |
1 files changed, 22 insertions, 14 deletions
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index fcd0838ef..c40a7c4d9 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -98,20 +98,28 @@ void FunDefFmf::simplify( std::vector< Node >& assertions ) { 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(); - //constant boolean function definitions do not add domain constraints - if( !is_fd || ( is_fd && assertions[i][1].getKind()==EQUAL ) ){ - 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; - PROOF( ProofManager::currentPM()->addDependence(n, assertions[i]); ); - assertions[i] = n; - } + 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; + PROOF(ProofManager::currentPM()->addDependence(n, assertions[i]);); + assertions[i] = n; } } } |