From 4ff2946e1338d3f500b7e6bababee50fadad68d6 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 12 Apr 2016 10:13:45 -0500 Subject: Optimizations for QCF to check relevant domain of variable argument positions eagerly, global ordering mechanism for quantified formulas within check. Refactoring of term database. --- src/theory/quantifiers/rewrite_engine.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/theory/quantifiers/rewrite_engine.cpp') diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 5bf8d8a8d..07b1462c6 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -285,7 +285,7 @@ void RewriteEngine::registerQuantifier( Node f ) { //make the quantified formula d_qinfo_n[f] = NodeManager::currentNM()->mkNode( FORALL, qcfn_c ); Trace("rr-register") << " qcf formula is : " << d_qinfo_n[f] << std::endl; - d_qinfo[f].initialize( d_qinfo_n[f], d_qinfo_n[f][1] ); + d_qinfo[f].initialize( qcf, d_qinfo_n[f], d_qinfo_n[f][1] ); } } } -- cgit v1.2.3