diff options
author | Justin Xu <justinx@barrett5.stanford.edu> | 2017-07-12 22:05:26 -0700 |
---|---|---|
committer | Justin Xu <justinx@barrett5.stanford.edu> | 2017-07-24 15:47:17 -0700 |
commit | d6d90bb120c743ebae98f5a6cd87a87c524fbcb7 (patch) | |
tree | 17e47f44267249501d8388d4e10ef5d332f94adb /src/smt | |
parent | 0e3c318e0d88687ab0c2d1bf380a25f9e41817af (diff) |
QuantifiedPass bugged,commented out
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7881449dd..4f3b1b5d6 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -110,6 +110,7 @@ using namespace CVC4::smt; using namespace CVC4::prop; using namespace CVC4::context; using namespace CVC4::theory; +using namespace CVC4::preproc; namespace CVC4 { namespace smt { @@ -3630,6 +3631,11 @@ void SmtEnginePrivate::processAssertions() { } if( d_smt.d_logic.isQuantified() ){ +/* preproc::QuantifiedPass pass(d_resourceManager, d_smt.d_theoryEngine, + d_smt.d_fmfRecFunctionsDefined, d_smt.d_fmfRecFunctionsAbs, + d_smt.d_fmfRecFunctionsConcrete); + pass.apply(&d_assertions);*/ + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << std::endl; dumpAssertions("pre-skolem-quant", d_assertions); @@ -3655,6 +3661,7 @@ void SmtEnginePrivate::processAssertions() { qm.finalizeDefinitions(); } + //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF if( options::fmfFunWellDefined() ){ quantifiers::FunDefFmf fdf; @@ -3685,11 +3692,7 @@ void SmtEnginePrivate::processAssertions() { } } Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << std::endl; - /* preproc::QuantifiedPass pass(d_resourceManager, d_smt.d_theoryEngine, - d_smt.d_fmfRecFunctionsDefined, d_smt.d_fmfRecFunctionsAbs, - d_smt.d_fmfRecFunctionsConcrete); - pass.apply(&d_assertions);*/ - } +} if( options::sortInference() || options::ufssFairnessMonotone() ){ //sort inference technique |