From c66033a67511b10b5ee22b7072b9ceab45552a79 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Sat, 25 Aug 2018 14:31:32 -0700 Subject: [PATCH] Refactor quantifier macros preprocessing pass (#1840) Moved `src/theory/quantifiers/macros.{cpp,h}` to `src/preprocessing/passes/quantifier_macros.{cpp,h}`, and added the necessary methods for inheritance from PreprocessingPass. No need to add a test - regress0 fails when adding Assert(false) when assertions had changed. --- src/Makefile.am | 4 +- .../passes/quantifier_macros.cpp} | 64 ++++++++++--- src/preprocessing/passes/quantifier_macros.h | 89 +++++++++++++++++++ src/smt/smt_engine.cpp | 16 ++-- src/theory/quantifiers/macros.h | 74 --------------- 5 files changed, 149 insertions(+), 98 deletions(-) rename src/{theory/quantifiers/macros.cpp => preprocessing/passes/quantifier_macros.cpp} (92%) create mode 100644 src/preprocessing/passes/quantifier_macros.h delete mode 100644 src/theory/quantifiers/macros.h diff --git a/src/Makefile.am b/src/Makefile.am index d399602cb..e0a9fb807 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -95,6 +95,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/bv_to_bool.h \ preprocessing/passes/quantifiers_preprocess.cpp \ preprocessing/passes/quantifiers_preprocess.h \ + preprocessing/passes/quantifier_macros.cpp \ + preprocessing/passes/quantifier_macros.h \ preprocessing/passes/real_to_int.cpp \ preprocessing/passes/real_to_int.h \ preprocessing/passes/rewrite.cpp \ @@ -482,8 +484,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/lazy_trie.h \ theory/quantifiers/local_theory_ext.cpp \ theory/quantifiers/local_theory_ext.h \ - theory/quantifiers/macros.cpp \ - theory/quantifiers/macros.h \ theory/quantifiers/quant_conflict_find.cpp \ theory/quantifiers/quant_conflict_find.h \ theory/quantifiers/quant_epr.cpp \ diff --git a/src/theory/quantifiers/macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp similarity index 92% rename from src/theory/quantifiers/macros.cpp rename to src/preprocessing/passes/quantifier_macros.cpp index d88f8eec9..e3bc02309 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file macros.cpp +/*! \file quantifier_macros.cpp ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Kshitij Bansal @@ -14,7 +14,7 @@ ** This class implements quantifiers macro definitions. **/ -#include "theory/quantifiers/macros.h" +#include "preprocessing/passes/quantifier_macros.h" #include @@ -27,19 +27,48 @@ #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" #include "theory/rewriter.h" -using namespace CVC4; using namespace std; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; using namespace CVC4::kind; +namespace CVC4 { +namespace preprocessing { +namespace passes { -QuantifierMacros::QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){ +QuantifierMacros::QuantifierMacros(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "quantifier-macros"), + d_ground_macros(false) +{ +} + +PreprocessingPassResult QuantifierMacros::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + bool success; + do + { + success = simplify(assertionsToPreprocess->ref(), true); + } while (success); + finalizeDefinitions(); + clearMaps(); + return PreprocessingPassResult::NO_CONFLICT; +} + +void QuantifierMacros::clearMaps() +{ + d_macro_basis.clear(); + d_macro_defs.clear(); + d_macro_defs_new.clear(); + d_macro_def_contains.clear(); + d_simplify_cache.clear(); + d_quant_macros.clear(); d_ground_macros = false; } - + bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){ unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_ALL ? 2 : 1; for( unsigned r=0; r& assertions, bool doRewrite //for now, it is dependent upon all assertions involving macros, this is an over-approximation. //a more fine-grained unsat core computation would require caching dependencies for each subterm of the formula, // which is expensive. - PROOF( - ProofManager::currentPM()->addDependence(curr, assertions[i]); - for( unsigned j=0; jaddDependence(curr,macro_assertions[j]); - } - } - ); + PROOF(ProofManager::currentPM()->addDependence(curr, assertions[i]); + for (unsigned j = 0; j < macro_assertions.size(); j++) { + if (macro_assertions[j] != assertions[i]) + { + ProofManager::currentPM()->addDependence( + curr, macro_assertions[j]); + } + }); assertions[i] = curr; retVal = true; } @@ -154,7 +183,10 @@ bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){ } bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) { - Node icn = d_qe->getTermUtil()->substituteBoundVariablesToInstConstants(n, f); + Node icn = d_preprocContext->getTheoryEngine() + ->getQuantifiersEngine() + ->getTermUtil() + ->substituteBoundVariablesToInstConstants(n, f); Trace("macros-debug2") << "Get free variables in " << icn << std::endl; std::vector< Node > var; quantifiers::TermUtil::computeInstConstContainsForQuant(f, icn, var); @@ -512,3 +544,7 @@ void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) { } } } + +} // passes +} // preprocessing +} // CVC4 diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h new file mode 100644 index 000000000..092a62942 --- /dev/null +++ b/src/preprocessing/passes/quantifier_macros.h @@ -0,0 +1,89 @@ +/********************* */ +/*! \file quantifier_macros.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Pre-process step for detecting quantifier macro definitions + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H +#define __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H + +#include +#include +#include +#include "expr/node.h" +#include "expr/type_node.h" +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +class QuantifierMacros : public PreprocessingPass +{ + public: + QuantifierMacros(PreprocessingPassContext* preprocContext); + ~QuantifierMacros() {} + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + bool processAssertion(Node n); + bool isBoundVarApplyUf(Node n); + bool process(Node n, bool pol, std::vector& args, Node f); + bool containsBadOp(Node n, + Node op, + std::vector& opc, + std::map& visited); + bool isMacroLiteral(Node n, bool pol); + bool isGroundUfTerm(Node f, Node n); + void getMacroCandidates(Node n, + std::vector& candidates, + std::map& visited); + Node solveInEquality(Node n, Node lit); + bool getFreeVariables(Node n, + std::vector& v_quant, + std::vector& vars, + bool retOnly, + std::map& visited); + bool getSubstitution(std::vector& v_quant, + std::map& solved, + std::vector& vars, + std::vector& subs, + bool reqComplete); + void addMacro(Node op, Node n, std::vector& opc); + void debugMacroDefinition(Node oo, Node n); + bool simplify(std::vector& assertions, bool doRewrite = false); + Node simplify(Node n); + void finalizeDefinitions(); + void clearMaps(); + + // map from operators to macro basis terms + std::map > d_macro_basis; + // map from operators to macro definition + std::map d_macro_defs; + std::map d_macro_defs_new; + // operators to macro ops that contain them + std::map > d_macro_def_contains; + // simplify caches + std::map d_simplify_cache; + std::map d_quant_macros; + bool d_ground_macros; +}; + +} // passes +} // preprocessing +} // CVC4 + +#endif /*__CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 70e575487..0497c2814 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -85,6 +85,8 @@ #include "preprocessing/passes/ite_simp.h" #include "preprocessing/passes/nl_ext_purify.h" #include "preprocessing/passes/pseudo_boolean_processor.h" +#include "preprocessing/passes/quantifier_macros.h" +#include "preprocessing/passes/quantifier_macros.h" #include "preprocessing/passes/quantifiers_preprocess.h" #include "preprocessing/passes/real_to_int.h" #include "preprocessing/passes/rewrite.h" @@ -118,7 +120,6 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/logic_info.h" #include "theory/quantifiers/fun_def_process.h" -#include "theory/quantifiers/macros.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/single_inv_partition.h" #include "theory/quantifiers/sygus/ce_guided_instantiation.h" @@ -2686,6 +2687,8 @@ void SmtEnginePrivate::finishInit() std::move(bvAckermann)); d_preprocessingPassRegistry.registerPass("bv-eager-atoms", std::move(bvEagerAtoms)); + std::unique_ptr quantifierMacros( + new QuantifierMacros(d_preprocessingPassContext.get())); d_preprocessingPassRegistry.registerPass("bv-gauss", std::move(bvGauss)); d_preprocessingPassRegistry.registerPass("bv-intro-pow2", std::move(bvIntroPow2)); @@ -2715,6 +2718,8 @@ void SmtEnginePrivate::finishInit() std::move(sygusInfer)); d_preprocessingPassRegistry.registerPass("sym-break", std::move(sbProc)); d_preprocessingPassRegistry.registerPass("synth-rr", std::move(srrProc)); + d_preprocessingPassRegistry.registerPass("quantifier-macros", + std::move(quantifierMacros)); } Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map& cache, bool expandOnly) @@ -4078,13 +4083,8 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-skolem-quant", d_assertions); if( options::macrosQuant() ){ //quantifiers macro expansion - quantifiers::QuantifierMacros qm( d_smt.d_theoryEngine->getQuantifiersEngine() ); - bool success; - do{ - success = qm.simplify( d_assertions.ref(), true ); - }while( success ); - //finalize the definitions - qm.finalizeDefinitions(); + d_preprocessingPassRegistry.getPass("quantifier-macros") + ->apply(&d_assertions); } //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h deleted file mode 100644 index b36be7aec..000000000 --- a/src/theory/quantifiers/macros.h +++ /dev/null @@ -1,74 +0,0 @@ -/********************* */ -/*! \file macros.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Pre-process step for detecting quantifier macro definitions - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__QUANTIFIERS_MACROS_H -#define __CVC4__QUANTIFIERS_MACROS_H - -#include -#include -#include -#include -#include "expr/node.h" -#include "expr/type_node.h" -#include "theory/quantifiers_engine.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -class QuantifierMacros{ -private: - QuantifiersEngine * d_qe; -private: - bool d_ground_macros; - bool processAssertion( Node n ); - bool isBoundVarApplyUf( Node n ); - bool process( Node n, bool pol, std::vector< Node >& args, Node f ); - bool containsBadOp( Node n, Node op, std::vector< Node >& opc, std::map< Node, bool >& visited ); - bool isMacroLiteral( Node n, bool pol ); - bool isGroundUfTerm( Node f, Node n ); - void getMacroCandidates( Node n, std::vector< Node >& candidates, std::map< Node, bool >& visited ); - Node solveInEquality( Node n, Node lit ); - bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly, std::map< Node, bool >& visited ); - bool getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved, - std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete ); - //map from operators to macro basis terms - std::map< Node, std::vector< Node > > d_macro_basis; - //map from operators to macro definition - std::map< Node, Node > d_macro_defs; - std::map< Node, Node > d_macro_defs_new; - //operators to macro ops that contain them - std::map< Node, std::vector< Node > > d_macro_def_contains; - //simplify caches - std::map< Node, Node > d_simplify_cache; - std::map< Node, bool > d_quant_macros; -private: - Node simplify( Node n ); - void addMacro( Node op, Node n, std::vector< Node >& opc ); - void debugMacroDefinition( Node oo, Node n ); -public: - QuantifierMacros( QuantifiersEngine * qe ); - ~QuantifierMacros(){} - - bool simplify( std::vector< Node >& assertions, bool doRewrite = false ); - void finalizeDefinitions(); -}; - -} -} -} - -#endif -- 2.30.2