diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-09 15:51:26 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-09 15:51:26 +0200 |
commit | 3f59801357808a538934b04ce7bf0894dec1b0dd (patch) | |
tree | 9a32729a077f25fbd7ef2e84825d1e177d29bafd /src/theory/quantifiers/fun_def_process.cpp | |
parent | 7443276e61db276e5ba48d605cb6b08a35c5a100 (diff) |
Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, and strings preprocessing. Minor fix for conjecture generation for finite types.
Diffstat (limited to 'src/theory/quantifiers/fun_def_process.cpp')
-rw-r--r-- | src/theory/quantifiers/fun_def_process.cpp | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index b80d9d744..f47cb8f1e 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -20,6 +20,7 @@ #include "theory/rewriter.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/quant_util.h" +#include "proof/proof_manager.h" using namespace CVC4; using namespace std; @@ -75,8 +76,10 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << std::endl; Trace("fmf-fun-def") << " to " << std::endl; - assertions[i] = NodeManager::currentNM()->mkNode( FORALL, bvl, bd ); - assertions[i] = Rewriter::rewrite( assertions[i] ); + Node new_q = NodeManager::currentNM()->mkNode( FORALL, bvl, bd ); + new_q = Rewriter::rewrite( new_q ); + PROOF( ProofManager::currentPM()->addDependence(new_q, assertions[i]); ); + assertions[i] = new_q; Trace("fmf-fun-def") << " " << assertions[i] << std::endl; fd_assertions.push_back( i ); } @@ -95,6 +98,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { 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; } } |