diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-11 14:36:50 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-11 14:36:50 -0500 |
| commit | 0b2f9943d55152e0958369083649dd71340864c9 (patch) | |
| tree | cd040f1dd12816c6af37548597bd674cafb45271 /src/util | |
| parent | 8ebd49cb903ba19f9330820d02af08e226c9b791 (diff) | |
More preparation for CASC proofs. Minor fix for sort inference (rewrite new assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.
Diffstat (limited to 'src/util')
| -rw-r--r-- | src/util/sort_inference.cpp | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index ce12b59f1..b38ed7d63 100644 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -22,7 +22,7 @@ #include "util/sort_inference.h" #include "theory/uf/options.h" #include "smt/options.h" -//#include "theory/rewriter.h" +#include "theory/rewriter.h" using namespace CVC4; using namespace std; @@ -172,6 +172,7 @@ bool SortInference::simplify( std::vector< Node >& assertions ){ std::map< Node, Node > var_bound; assertions[i] = simplify( assertions[i], var_bound ); if( prev!=assertions[i] ){ + assertions[i] = theory::Rewriter::rewrite( assertions[i] ); rewritten = true; Trace("sort-inference-rewrite") << prev << std::endl; Trace("sort-inference-rewrite") << " --> " << assertions[i] << std::endl; @@ -626,11 +627,13 @@ Node SortInference::mkInjection( TypeNode tn1, TypeNode tn2 ) { Trace("sort-inference") << "-> Make injection " << f << " from " << tn1 << " to " << tn2 << std::endl; Node v1 = NodeManager::currentNM()->mkBoundVar( "?x", tn1 ); Node v2 = NodeManager::currentNM()->mkBoundVar( "?y", tn1 ); - return NodeManager::currentNM()->mkNode( kind::FORALL, - NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, v1, v2 ), - NodeManager::currentNM()->mkNode( kind::IMPLIES, - NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v1 ).eqNode( NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v2 ) ), - v1.eqNode( v2 ) ) ); + Node ret = NodeManager::currentNM()->mkNode( kind::FORALL, + NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, v1, v2 ), + NodeManager::currentNM()->mkNode( kind::OR, + NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v1 ).eqNode( NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v2 ) ).negate(), + v1.eqNode( v2 ) ) ); + ret = theory::Rewriter::rewrite( ret ); + return ret; } int SortInference::getSortId( Node n ) { |