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/util | |
| 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/util')
| -rw-r--r-- | src/util/sort_inference.cpp | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index dbd1dcd16..14d37e068 100644 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -24,6 +24,7 @@ #include "smt/options.h" #include "theory/rewriter.h" #include "theory/quantifiers/options.h" +#include "proof/proof_manager.h" using namespace CVC4; using namespace std; @@ -172,13 +173,15 @@ bool SortInference::simplify( std::vector< Node >& assertions ){ Node prev = assertions[i]; std::map< Node, Node > var_bound; Trace("sort-inference-debug") << "Rewrite " << assertions[i] << std::endl; - assertions[i] = simplify( assertions[i], var_bound ); + Node curr = simplify( assertions[i], var_bound ); Trace("sort-inference-debug") << "Done." << std::endl; - if( prev!=assertions[i] ){ - assertions[i] = theory::Rewriter::rewrite( assertions[i] ); + if( curr!=assertions[i] ){ + curr = theory::Rewriter::rewrite( curr ); rewritten = true; - Trace("sort-inference-rewrite") << prev << std::endl; - Trace("sort-inference-rewrite") << " --> " << assertions[i] << std::endl; + Trace("sort-inference-rewrite") << assertions << std::endl; + Trace("sort-inference-rewrite") << " --> " << curr << std::endl; + PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); ); + assertions[i] = curr; } } //now, ensure constants are distinct |