diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-08 20:26:11 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-08 20:26:11 -0500 |
commit | 2f8caabd570dd5bb2936d9f094b7b302a510aa6d (patch) | |
tree | 5ae3497d2dcd9bf39cc0686a1a0d23b0113571d2 /src/smt/process_assertions.h | |
parent | df1ea6b9cdc1f424073151d0f7fda639d4405622 (diff) |
Split ProcessAssertions module from SmtEngine (#4210)
This is a step towards refactoring the SmtEngine. It splits several core components of SmtEnginePrivate to its own independent module, ProcessAssertions which is responsible for applying preprocessing passes , simplification and expand definitions.
The main change involved moving these functions from SmtEnginePrivate to this new class. A few other minor changes were done to make this move:
A few things changed order within processAssertions to allow SmtEnginePrivate-specific things to happen outside of the main scope of processAssertions.
processAssertions had some logic to catch incompatible options and silently disable options. This was moved to setDefaults.
A few data members in SmtEngine were moved to ProcessAssertions.
Two utilities that were sitting in smt_engine.cpp were moved to their own files.
Another refactoring step will be to make ProcessAssertions take only the utilities it needs instead of taking a SmtEngine reference. This requires further detangling of Options.
Diffstat (limited to 'src/smt/process_assertions.h')
-rw-r--r-- | src/smt/process_assertions.h | 150 |
1 files changed, 150 insertions, 0 deletions
diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h new file mode 100644 index 000000000..ddf5a6cba --- /dev/null +++ b/src/smt/process_assertions.h @@ -0,0 +1,150 @@ +/********************* */ +/*! \file process_assertions.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 The module for processing assertions for an SMT engine. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__SMT__PROCESS_ASSERTIONS_H +#define CVC4__SMT__PROCESS_ASSERTIONS_H + +#include <map> + +#include "context/cdhashmap.h" +#include "context/cdlist.h" +#include "expr/node.h" +#include "expr/type_node.h" +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" +#include "smt/smt_engine_stats.h" +#include "util/resource_manager.h" + +namespace CVC4 { + +class SmtEngine; + +namespace smt { + +/** + * Module in charge of processing assertions for an SMT engine. + * + * Its main features are: + * (1) apply(AssertionsPipeline&), which updates the assertions based on our + * preprocessing steps, + * (2) expandDefinitions(TNode, ...), which returns the expanded formula of a + * term. + * The method finishInit(...) must be called before these methods are called. + * + * It is designed to be agnostic to whether we are in incremental mode. That is, + * it processes assertions in a way that assumes that apply(...) could be + * applied multiple times to different sets of assertions. + */ +class ProcessAssertions +{ + /** The types for the recursive function definitions */ + typedef context::CDList<Node> NodeList; + typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap; + typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap; + + public: + ProcessAssertions(SmtEngine& smt, ResourceManager& rm); + ~ProcessAssertions(); + /** Finish initialize + * + * This initializes the preprocessing passes owned by this module. + */ + void finishInit(preprocessing::PreprocessingPassContext* pc); + /** Cleanup + * + * This deletes the processing passes owned by this module. + */ + void cleanup(); + /** + * Process the formulas in assertions. Returns true if there + * was no conflict when processing the assertions. + */ + bool apply(preprocessing::AssertionPipeline& assertions); + /** + * Expand definitions in term n. Return the expanded form of n. + * + * If expandOnly is true, then the expandDefinitions function of TheoryEngine + * of the SmtEngine this calls is associated with is not called on subterms of + * n. + */ + Node expandDefinitions(TNode n, + NodeToNodeHashMap& cache, + bool expandOnly = false); + + private: + /** Reference to the SMT engine */ + SmtEngine& d_smt; + /** Reference to resource manager */ + ResourceManager& d_resourceManager; + /** The preprocess context */ + preprocessing::PreprocessingPassContext* d_preprocessingPassContext; + /** True node */ + Node d_true; + /** + * Map of preprocessing pass instances, mapping from names to preprocessing + * pass instance + */ + std::unordered_map<std::string, + std::unique_ptr<preprocessing::PreprocessingPass>> + d_passes; + /** + * Number of calls of simplify assertions active. + */ + unsigned d_simplifyAssertionsDepth; + /** recursive function definition abstractions for fmf-fun */ + std::map<Node, TypeNode> d_fmfRecFunctionsAbs; + /** map to concrete definitions for fmf-fun */ + std::map<Node, std::vector<Node>> d_fmfRecFunctionsConcrete; + /** List of defined recursive functions processed by fmf-fun */ + NodeList* d_fmfRecFunctionsDefined; + /** Spend resource r by the resource manager of this class. */ + void spendResource(ResourceManager::Resource r); + /** + * Perform non-clausal simplification of a Node. This involves + * Theory implementations, but does NOT involve the SAT solver in + * any way. + * + * Returns false if the formula simplifies to "false" + */ + bool simplifyAssertions(preprocessing::AssertionPipeline& assertions); + /** + * Dump assertions. Print the current assertion list to the dump + * assertions:`key` if it is enabled. + */ + void dumpAssertions(const char* key, + const preprocessing::AssertionPipeline& assertionList); + /** + * Helper function to fix up assertion list to restore invariants needed after + * ite removal. + */ + void collectSkolems(IteSkolemMap& iskMap, + TNode n, + set<TNode>& skolemSet, + NodeToBoolHashMap& cache); + /** + * Helper function to fix up assertion list to restore invariants needed after + * ite removal. + */ + bool checkForBadSkolems(IteSkolemMap& iskMap, + TNode n, + TNode skolem, + NodeToBoolHashMap& cache); +}; + +} // namespace smt +} // namespace CVC4 + +#endif |