diff options
author | Justin Xu <justinx@barrett5.stanford.edu> | 2017-07-24 13:21:40 -0700 |
---|---|---|
committer | Justin Xu <justinx@barrett5.stanford.edu> | 2017-07-24 13:21:40 -0700 |
commit | e07aa10dea10fcc6ce1775cc7c67b6baa0d09750 (patch) | |
tree | f5114ec900f8dcb40c3c30ef94c5ff5bd42163d1 | |
parent | 9d792f6f05d5348fab414a70405cd26451bd38da (diff) |
ContrainSubtypes and ExpandingDefinitions classes
-rw-r--r-- | src/' | 779 | ||||
-rw-r--r-- | src/preproc/preprocessing_pass.h | 19 | ||||
-rw-r--r-- | src/preproc/preprocessing_passes_core.cpp | 658 | ||||
-rw-r--r-- | src/preproc/preprocessing_passes_core.h | 37 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 43 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 13 |
6 files changed, 1490 insertions, 59 deletions
@@ -0,0 +1,779 @@ +/********************* */ +/*! \file smt_engine.h + ** \verbatim + ** Top contributors (to current version): + ** Morgan Deters, Tim King, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 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 SmtEngine: the main public entry point of libcvc4. + ** + ** SmtEngine: the main public entry point of libcvc4. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__SMT_ENGINE_H +#define __CVC4__SMT_ENGINE_H + +#include <string> +#include <vector> + +#include "base/modal_exception.h" +#include "context/cdhashmap_forward.h" +#include "context/cdhashset_forward.h" +#include "context/cdlist_forward.h" +#include "expr/expr.h" +#include "expr/expr_manager.h" +#include "expr/expr_stream.h" +#include "options/options.h" +#include "proof/unsat_core.h" +#include "smt/logic_exception.h" +#include "smt_util/lemma_channels.h" +#include "theory/logic_info.h" +#include "util/hash.h" +#include "util/proof.h" +#include "util/result.h" +#include "util/sexpr.h" +#include "util/statistics.h" +#include "util/unsafe_interrupt_exception.h" + +// In terms of abstraction, this is below (and provides services to) +// ValidityChecker and above (and requires the services of) +// PropEngine. + +namespace CVC4 { + +template <bool ref_count> class NodeTemplate; +typedef NodeTemplate<true> Node; +typedef NodeTemplate<false> TNode; +struct NodeHashFunction; + +class Command; +class GetModelCommand; + +class SmtEngine; +class DecisionEngine; +class TheoryEngine; + +class ProofManager; + +class Model; +class LogicRequest; +class StatisticsRegistry; + +namespace context { + class Context; + class UserContext; +}/* CVC4::context namespace */ + +namespace prop { + class PropEngine; +}/* CVC4::prop namespace */ + +namespace expr { + namespace attr { + class AttributeManager; + struct SmtAttributes; + }/* CVC4::expr::attr namespace */ +}/* CVC4::expr namespace */ + +namespace smt { + /** + * Representation of a defined function. We keep these around in + * SmtEngine to permit expanding definitions late (and lazily), to + * support getValue() over defined functions, to support user output + * in terms of defined functions, etc. + */ + class DefinedFunction; + + struct SmtEngineStatistics; + class SmtEnginePrivate; + class SmtScope; + class BooleanTermConverter; + + ProofManager* currentProofManager(); + + struct CommandCleanup; + typedef context::CDList<Command*, CommandCleanup> CommandList; +}/* CVC4::smt namespace */ + +namespace theory { + class TheoryModel; +}/* CVC4::theory namespace */ + +namespace preproc{ +// class DefinedFunction; + class DoStaticLearningPass; + class QuantifiedPass; + class SimplifyAssertionsPass; + class ExpandingDefinitionsPass; + class ConstrainSubtypesPass; +}/* CVC4::preproc namespace */ + +// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the +// hood): use a type parameter and have check() delegate, or subclass +// SmtEngine and override check()? +// +// Probably better than that is to have a configuration object that +// indicates which passes are desired. The configuration occurs +// elsewhere (and can even occur at runtime). A simple "pass manager" +// of sorts determines check()'s behavior. +// +// The CNF conversion can go on in PropEngine. + +class CVC4_PUBLIC SmtEngine { + /** The type of our internal map of defined functions */ + typedef context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction> + DefinedFunctionMap; + /** The type of our internal assertion list */ + typedef context::CDList<Expr> AssertionList; + /** The type of our internal assignment set */ + typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet; + /** The types for the recursive function definitions */ + typedef context::CDList<Node> NodeList; + + /** Expr manager context */ + context::Context* d_context; + + /** The context levels of user pushes */ + std::vector<int> d_userLevels; + /** User level context */ + context::UserContext* d_userContext; + + /** Our expression manager */ + ExprManager* d_exprManager; + /** Our internal expression/node manager */ + NodeManager* d_nodeManager; + /** The decision engine */ + DecisionEngine* d_decisionEngine; + /** The theory engine */ + TheoryEngine* d_theoryEngine; + /** The propositional engine */ + prop::PropEngine* d_propEngine; + /** The proof manager */ + ProofManager* d_proofManager; + /** An index of our defined functions */ + DefinedFunctionMap* d_definedFunctions; + /** recursive function definition abstractions for --fmf-fun */ + std::map< Node, TypeNode > d_fmfRecFunctionsAbs; + std::map< Node, std::vector< Node > > d_fmfRecFunctionsConcrete; + NodeList* d_fmfRecFunctionsDefined; + + /** + * The assertion list (before any conversion) for supporting + * getAssertions(). Only maintained if in interactive mode. + */ + AssertionList* d_assertionList; + + /** + * List of items for which to retrieve values using getAssignment(). + */ + AssignmentSet* d_assignments; + + /** + * A list of commands that should be in the Model globally (i.e., + * regardless of push/pop). Only maintained if produce-models option + * is on. + */ + std::vector<Command*> d_modelGlobalCommands; + + /** + * A list of commands that should be in the Model locally (i.e., + * it is context-dependent on push/pop). Only maintained if + * produce-models option is on. + */ + smt::CommandList* d_modelCommands; + + /** + * A vector of declaration commands waiting to be dumped out. + * Once the SmtEngine is fully initialized, we'll dump them. + * This ensures the declarations come after the set-logic and + * any necessary set-option commands are dumped. + */ + std::vector<Command*> d_dumpCommands; + + /** + *A vector of command definitions to be imported in the new + *SmtEngine when checking unsat-cores. + */ + std::vector<Command*> d_defineCommands; + + /** + * The logic we're in. + */ + LogicInfo d_logic; + + /** + * Keep a copy of the original option settings (for reset()). + */ + Options d_originalOptions; + + /** + * Number of internal pops that have been deferred. + */ + unsigned d_pendingPops; + + /** + * Whether or not this SmtEngine has been fully initialized (that is, + * the ). This post-construction initialization is automatically + * triggered by the use of the SmtEngine; e.g. when setLogic() is + * called, or the first assertion is made, etc. + */ + bool d_fullyInited; + + /** + * Whether or not we have added any assertions/declarations/definitions, + * or done push/pop, since the last checkSat/query, and therefore we're + * not responsible for models or proofs. + */ + bool d_problemExtended; + + /** + * Whether or not a query() or checkSat() has already been made through + * this SmtEngine. If true, and incrementalSolving is false, then + * attempting an additional query() or checkSat() will fail with a + * ModalException. + */ + bool d_queryMade; + + /** + * Internal status flag to indicate whether we've sent a theory + * presolve() notification and need to match it with a postsolve(). + */ + bool d_needPostsolve; + + /* + * Whether to call theory preprocessing during simplification - on + * by default* but gets turned off if arithRewriteEq is on + */ + bool d_earlyTheoryPP; + + /** + * Most recent result of last checkSat/query or (set-info :status). + */ + Result d_status; + + /** + * The name of the input (if any). + */ + std::string d_filename; + + /** + * Verbosity of various commands. + */ + std::map<std::string, Integer> d_commandVerbosity; + + /** ReplayStream for the solver. */ + ExprStream* d_replayStream; + + /** + * A private utility class to SmtEngine. + */ + smt::SmtEnginePrivate* d_private; + + /** + * Check that a generated proof (via getProof()) checks. + */ + void checkProof(); + + /** + * Check that an unsatisfiable core is indeed unsatisfiable. + */ + void checkUnsatCore(); + + /** + * Check that a generated Model (via getModel()) actually satisfies + * all user assertions. + */ + void checkModel(bool hardFailure = true); + + /** + * Postprocess a value for output to the user. Involves doing things + * like turning datatypes back into tuples, length-1-bitvectors back + * into booleans, etc. + */ + Node postprocess(TNode n, TypeNode expectedType) const; + + /** + * This is something of an "init" procedure, but is idempotent; call + * as often as you like. Should be called whenever the final options + * and logic for the problem are set (at least, those options that are + * not permitted to change after assertions and queries are made). + */ + void finalOptionsAreSet(); + + /** + * Apply heuristics settings and other defaults. Done once, at + * finishInit() time. + */ + void setDefaults(); + + /** + * Create theory engine, prop engine, decision engine. Called by + * finalOptionsAreSet() + */ + void finishInit(); + + /** + * This is called by the destructor, just before destroying the + * PropEngine, TheoryEngine, and DecisionEngine (in that order). It + * is important because there are destruction ordering issues + * between PropEngine and Theory. + */ + void shutdown(); + + /** + * Full check of consistency in current context. Returns true iff + * consistent. + */ + Result check(); + + /** + * Quick check of consistency in current context: calls + * processAssertionList() then look for inconsistency (based only on + * that). + */ + Result quickCheck(); + + /** + * Fully type-check the argument, and also type-check that it's + * actually Boolean. + */ + void ensureBoolean(const Expr& e) throw(TypeCheckingException); + + void internalPush(); + + void internalPop(bool immediate = false); + + void doPendingPops(); + + /** + * Internally handle the setting of a logic. This function should always + * be called when d_logic is updated. + */ + void setLogicInternal() throw(); + + friend class ::CVC4::preproc::DoStaticLearningPass; + friend class ::CVC4::preproc::QuantifiedPass; + friend class ::CVC4::preproc::SimplifyAssertionsPass; + friend class ::CVC4::preproc::ExpandingDefinitionsPass; + friend class ::CVC4::preproc::ConstrainSubtypesPass; + friend class ::CVC4::smt::SmtEnginePrivate; + friend class ::CVC4::smt::SmtScope; + friend class ::CVC4::smt::BooleanTermConverter; + friend ProofManager* ::CVC4::smt::currentProofManager(); + friend class ::CVC4::LogicRequest; + // to access d_modelCommands + friend class ::CVC4::Model; + friend class ::CVC4::theory::TheoryModel; + // to access SmtAttributes + friend class expr::attr::AttributeManager; + // to access getModel(), which is private (for now) + friend class GetModelCommand; + + /** + * There's something of a handshake between the expr package's + * AttributeManager and the SmtEngine because the expr package + * doesn't have a Context on its own (that's owned by the + * SmtEngine). Thus all context-dependent attributes are stored + * here. + */ + expr::attr::SmtAttributes* d_smtAttributes; + + StatisticsRegistry* d_statisticsRegistry; + + smt::SmtEngineStatistics* d_stats; + + /** Container for the lemma input and output channels for this SmtEngine.*/ + LemmaChannels* d_channels; + + /** + * Add to Model command. This is used for recording a command + * that should be reported during a get-model call. + */ + void addToModelCommandAndDump(const Command& c, uint32_t flags = 0, bool userVisible = true, const char* dumpTag = "declarations"); + + /** + * Get the model (only if immediately preceded by a SAT + * or INVALID query). Only permitted if CVC4 was built with model + * support and produce-models is on. + */ + Model* getModel(); + + // disallow copy/assignment + SmtEngine(const SmtEngine&) CVC4_UNDEFINED; + SmtEngine& operator=(const SmtEngine&) CVC4_UNDEFINED; + + //check satisfiability (for query and check-sat) + Result checkSatisfiability(const Expr& e, bool inUnsatCore, bool isQuery); +public: + + /** + * Construct an SmtEngine with the given expression manager. + */ + SmtEngine(ExprManager* em) throw(); + + /** + * Destruct the SMT engine. + */ + ~SmtEngine() throw(); + + /** + * Set the logic of the script. + */ + void setLogic(const std::string& logic) throw(ModalException, LogicException); + + /** + * Set the logic of the script. + */ + void setLogic(const char* logic) throw(ModalException, LogicException); + + /** + * Set the logic of the script. + */ + void setLogic(const LogicInfo& logic) throw(ModalException); + + /** + * Get the logic information currently set + */ + LogicInfo getLogicInfo() const; + + /** + * Set information about the script executing. + */ + void setInfo(const std::string& key, const CVC4::SExpr& value) + throw(OptionException, ModalException); + + /** + * Query information about the SMT environment. + */ + CVC4::SExpr getInfo(const std::string& key) const; + + /** + * Set an aspect of the current SMT execution environment. + */ + void setOption(const std::string& key, const CVC4::SExpr& value) + throw(OptionException, ModalException); + + /** + * Get an aspect of the current SMT execution environment. + */ + CVC4::SExpr getOption(const std::string& key) const + throw(OptionException); + + /** + * Add a formula to the current context: preprocess, do per-theory + * setup, use processAssertionList(), asserting to T-solver for + * literals and conjunction of literals. Returns false if + * immediately determined to be inconsistent. + */ + void defineFunction(Expr func, + const std::vector<Expr>& formals, + Expr formula); + + /** is defined function */ + bool isDefinedFunction(Expr func); + + /** + * Add a formula to the current context: preprocess, do per-theory + * setup, use processAssertionList(), asserting to T-solver for + * literals and conjunction of literals. Returns false if + * immediately determined to be inconsistent. This version + * takes a Boolean flag to determine whether to include this asserted + * formula in an unsat core (if one is later requested). + */ + Result assertFormula(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, LogicException, UnsafeInterruptException); + + /** + * Check validity of an expression with respect to the current set + * of assertions by asserting the query expression's negation and + * calling check(). Returns valid, invalid, or unknown result. + */ + Result query(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, ModalException, LogicException); + + /** + * Assert a formula (if provided) to the current context and call + * check(). Returns sat, unsat, or unknown result. + */ + Result checkSat(const Expr& e = Expr(), bool inUnsatCore = true) throw(TypeCheckingException, ModalException, LogicException); + + /** + * Assert a synthesis conjecture to the current context and call + * check(). Returns sat, unsat, or unknown result. + */ + Result checkSynth(const Expr& e) throw(TypeCheckingException, ModalException, LogicException); + + /** + * Simplify a formula without doing "much" work. Does not involve + * the SAT Engine in the simplification, but uses the current + * definitions, assertions, and the current partial model, if one + * has been constructed. It also involves theory normalization. + * + * @todo (design) is this meant to give an equivalent or an + * equisatisfiable formula? + */ + Expr simplify(const Expr& e) throw(TypeCheckingException, LogicException, UnsafeInterruptException); + + /** + * Expand the definitions in a term or formula. No other + * simplification or normalization is done. + */ + Expr expandDefinitions(const Expr& e) throw(TypeCheckingException, LogicException, UnsafeInterruptException); + + /** + * Get the assigned value of an expr (only if immediately preceded + * by a SAT or INVALID query). Only permitted if the SmtEngine is + * set to operate interactively and produce-models is on. + */ + Expr getValue(const Expr& e) const throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException); + + /** + * Add a function to the set of expressions whose value is to be + * later returned by a call to getAssignment(). The expression + * should be a Boolean zero-ary defined function or a Boolean + * variable. Rather than throwing a ModalException on modal + * failures (not in interactive mode or not producing assignments), + * this function returns true if the expression was added and false + * if this request was ignored. + */ + bool addToAssignment(const Expr& e); + + /** + * Get the assignment (only if immediately preceded by a SAT or + * INVALID query). Only permitted if the SmtEngine is set to + * operate interactively and produce-assignments is on. + */ + CVC4::SExpr getAssignment(); + + /** + * Get the last proof (only if immediately preceded by an UNSAT + * or VALID query). Only permitted if CVC4 was built with proof + * support and produce-proofs is on. + */ + Proof* getProof(); + + /** + * Print all instantiations made by the quantifiers module. + */ + void printInstantiations( std::ostream& out ); + + /** + * Print solution for synthesis conjectures found by ce_guided_instantiation module + */ + void printSynthSolution( std::ostream& out ); + + /** + * Do quantifier elimination, doFull false means just output one disjunct, strict is whether to output warnings. + */ + Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict=true) throw(TypeCheckingException, ModalException, LogicException); + + /** + * Get list of quantified formulas that were instantiated + */ + void getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ); + + /** + * Get instantiations + */ + void getInstantiations( Expr q, std::vector< Expr >& insts ); + void getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs ); + + /** + * Get an unsatisfiable core (only if immediately preceded by an + * UNSAT or VALID query). Only permitted if CVC4 was built with + * unsat-core support and produce-unsat-cores is on. + */ + UnsatCore getUnsatCore(); + + /** + * Get the current set of assertions. Only permitted if the + * SmtEngine is set to operate interactively. + */ + std::vector<Expr> getAssertions(); + + /** + * Push a user-level context. + */ + void push() throw(ModalException, LogicException, UnsafeInterruptException); + + /** + * Pop a user-level context. Throws an exception if nothing to pop. + */ + void pop(); + + /** + * Completely reset the state of the solver, as though destroyed and + * recreated. The result is as if newly constructed (so it still + * retains the same options structure and ExprManager). + */ + void reset() throw(); + + /** + * Reset all assertions, global declarations, etc. + */ + void resetAssertions() throw(); + + /** + * Interrupt a running query. This can be called from another thread + * or from a signal handler. Throws a ModalException if the SmtEngine + * isn't currently in a query. + */ + void interrupt() throw(ModalException); + + /** + * Set a resource limit for SmtEngine operations. This is like a time + * limit, but it's deterministic so that reproducible results can be + * obtained. Currently, it's based on the number of conflicts. + * However, please note that the definition may change between different + * versions of CVC4 (as may the number of conflicts required, anyway), + * and it might even be different between instances of the same version + * of CVC4 on different platforms. + * + * A cumulative and non-cumulative (per-call) resource limit can be + * set at the same time. A call to setResourceLimit() with + * cumulative==true replaces any cumulative resource limit currently + * in effect; a call with cumulative==false replaces any per-call + * resource limit currently in effect. Time limits can be set in + * addition to resource limits; the SmtEngine obeys both. That means + * that up to four independent limits can control the SmtEngine + * at the same time. + * + * When an SmtEngine is first created, it has no time or resource + * limits. + * + * Currently, these limits only cause the SmtEngine to stop what its + * doing when the limit expires (or very shortly thereafter); no + * heuristics are altered by the limits or the threat of them expiring. + * We reserve the right to change this in the future. + * + * @param units the resource limit, or 0 for no limit + * @param cumulative whether this resource limit is to be a cumulative + * resource limit for all remaining calls into the SmtEngine (true), or + * whether it's a per-call resource limit (false); the default is false + */ + void setResourceLimit(unsigned long units, bool cumulative = false); + + /** + * Set a time limit for SmtEngine operations. + * + * A cumulative and non-cumulative (per-call) time limit can be + * set at the same time. A call to setTimeLimit() with + * cumulative==true replaces any cumulative time limit currently + * in effect; a call with cumulative==false replaces any per-call + * time limit currently in effect. Resource limits can be set in + * addition to time limits; the SmtEngine obeys both. That means + * that up to four independent limits can control the SmtEngine + * at the same time. + * + * Note that the cumulative timer only ticks away when one of the + * SmtEngine's workhorse functions (things like assertFormula(), + * query(), checkSat(), and simplify()) are running. Between calls, + * the timer is still. + * + * When an SmtEngine is first created, it has no time or resource + * limits. + * + * Currently, these limits only cause the SmtEngine to stop what its + * doing when the limit expires (or very shortly thereafter); no + * heuristics are altered by the limits or the threat of them expiring. + * We reserve the right to change this in the future. + * + * @param millis the time limit in milliseconds, or 0 for no limit + * @param cumulative whether this time limit is to be a cumulative + * time limit for all remaining calls into the SmtEngine (true), or + * whether it's a per-call time limit (false); the default is false + */ + void setTimeLimit(unsigned long millis, bool cumulative = false); + + /** + * Get the current resource usage count for this SmtEngine. This + * function can be used to ascertain reasonable values to pass as + * resource limits to setResourceLimit(). + */ + unsigned long getResourceUsage() const; + + /** + * Get the current millisecond count for this SmtEngine. + */ + unsigned long getTimeUsage() const; + + /** + * Get the remaining resources that can be consumed by this SmtEngine + * according to the currently-set cumulative resource limit. If there + * is not a cumulative resource limit set, this function throws a + * ModalException. + */ + unsigned long getResourceRemaining() const throw(ModalException); + + /** + * Get the remaining number of milliseconds that can be consumed by + * this SmtEngine according to the currently-set cumulative time limit. + * If there is not a cumulative resource limit set, this function + * throws a ModalException. + */ + unsigned long getTimeRemaining() const throw(ModalException); + + /** + * Permit access to the underlying ExprManager. + */ + ExprManager* getExprManager() const { + return d_exprManager; + } + + /** + * Export statistics from this SmtEngine. + */ + Statistics getStatistics() const throw(); + + /** + * Get the value of one named statistic from this SmtEngine. + */ + SExpr getStatistic(std::string name) const throw(); + + /** + * Flush statistic from this SmtEngine. Safe to use in a signal handler. + */ + void safeFlushStatistics(int fd) const; + + /** + * Returns the most recent result of checkSat/query or (set-info :status). + */ + Result getStatusOfLastCommand() const throw() { + return d_status; + } + + /** + * Set user attribute. + * This function is called when an attribute is set by a user. + * In SMT-LIBv2 this is done via the syntax (! expr :attr) + */ + void setUserAttribute(const std::string& attr, Expr expr, std::vector<Expr> expr_values, std::string str_value); + + /** + * Set print function in model + */ + void setPrintFuncInModel(Expr f, bool p); + + + /** Throws a ModalException if the SmtEngine has been fully initialized. */ + void beforeSearch() throw(ModalException); + + LemmaChannels* channels() { return d_channels; } + + + /** + * Expermintal feature: Sets the sequence of decisions. + * This currently requires very fine grained knowledge about literal + * translation. + */ + void setReplayStream(ExprStream* exprStream); + +};/* class SmtEngine */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__SMT_ENGINE_H */ diff --git a/src/preproc/preprocessing_pass.h b/src/preproc/preprocessing_pass.h index d956993aa..739db58ff 100644 --- a/src/preproc/preprocessing_pass.h +++ b/src/preproc/preprocessing_pass.h @@ -11,6 +11,8 @@ #include "theory/rewriter.h" #include "theory/theory_engine.h" +using namespace std; + namespace CVC4 { namespace preproc { @@ -28,6 +30,23 @@ public: } }; +class DefinedFunction { + Node d_func; + vector<Node> d_formals; + Node d_formula; +public: + DefinedFunction() {} + DefinedFunction(Node func, vector<Node> formals, Node formula) : + d_func(func), + d_formals(formals), + d_formula(formula) { + } + Node getFunction() const { return d_func; } + vector<Node> getFormals() const { return d_formals; } + Node getFormula() const { return d_formula; } +}; +/* class DefinedFunction */ + class AssertionPipeline { std::vector<Node> d_nodes; diff --git a/src/preproc/preprocessing_passes_core.cpp b/src/preproc/preprocessing_passes_core.cpp index c43d80979..14599ea22 100644 --- a/src/preproc/preprocessing_passes_core.cpp +++ b/src/preproc/preprocessing_passes_core.cpp @@ -2,6 +2,8 @@ #include <ext/hash_map> #include <string> +#include <stack> +#include "expr/node_manager_attributes.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/fun_def_process.h" @@ -14,21 +16,188 @@ #include "options/bv_bitblast_mode.h" #include "options/bv_options.h" #include "options/uf_options.h" +#include "options/proof_options.h" +#include "util/ntuple.h" + +using namespace std; namespace CVC4 { namespace preproc { -ExpandingDefinitionsPass::ExpandingDefinitionsPass(ResourceManager* resourceManager, TimerStat definitionExpansionTime) : PreprocessingPass(resourceManager), d_definitionExpansionTime(definitionExpansionTime){ +ExpandingDefinitionsPass::ExpandingDefinitionsPass(ResourceManager* resourceManager, SmtEngine* smt, TimerStat definitionExpansionTime) : PreprocessingPass(resourceManager), d_smt(smt), d_definitionExpansionTime(definitionExpansionTime){ +} + +Node ExpandingDefinitionsPass::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly) + throw(TypeCheckingException, LogicException, UnsafeInterruptException) { + stack< triple<Node, Node, bool> > worklist; + stack<Node> result; + worklist.push(make_triple(Node(n), Node(n), false)); + // The worklist is made of triples, each is input / original node then the output / rewritten node + // and finally a flag tracking whether the children have been explored (i.e. if this is a downward + // or upward pass). + + do { + spendResource(options::preprocessStep()); + n = worklist.top().first; // n is the input / original + Node node = worklist.top().second; // node is the output / result + bool childrenPushed = worklist.top().third; + worklist.pop(); + + // Working downwards + if(!childrenPushed) { + Kind k = n.getKind(); + + // Apart from apply, we can short circuit leaves + if(k != kind::APPLY && n.getNumChildren() == 0) { + SmtEngine::DefinedFunctionMap::const_iterator i = d_smt->d_definedFunctions->find(n); + if(i != d_smt->d_definedFunctions->end()) { + // replacement must be closed + if((*i).second.getFormals().size() > 0) { + result.push(d_smt->d_nodeManager->mkNode(kind::LAMBDA, d_smt->d_nodeManager->mkNode(kind::BOUND_VAR_LIST, (*i).second.getFormals()), (*i).second.getFormula())); + continue; + } + // don't bother putting in the cache + result.push((*i).second.getFormula()); + continue; + } + // don't bother putting in the cache + result.push(n); + continue; + } + + // maybe it's in the cache + hash_map<Node, Node, NodeHashFunction>::iterator cacheHit = cache.find(n); + if(cacheHit != cache.end()) { + TNode ret = (*cacheHit).second; + result.push(ret.isNull() ? n : ret); + continue; + } + + // otherwise expand it + bool doExpand = k == kind::APPLY; + if( !doExpand ){ + if( options::macrosQuant() ){ + //expand if we have inferred an operator corresponds to a defined function + doExpand = k==kind::APPLY_UF && d_smt->isDefinedFunction( n.getOperator().toExpr() ); + } + } + if (doExpand) { + vector<Node> formals; + TNode fm; + if( n.getOperator().getKind() == kind::LAMBDA ){ + TNode op = n.getOperator(); + // lambda + for( unsigned i=0; i<op[0].getNumChildren(); i++ ){ + formals.push_back( op[0][i] ); + } + fm = op[1]; + }else{ + // application of a user-defined symbol + TNode func = n.getOperator(); + SmtEngine::DefinedFunctionMap::const_iterator i = d_smt->d_definedFunctions->find(func); + if(i == d_smt->d_definedFunctions->end()) { + throw TypeCheckingException(n.toExpr(), string("Undefined function: `") + func.toString() + "'"); + } + DefinedFunction def = (*i).second; + formals = def.getFormals(); + + if(Debug.isOn("expand")) { + Debug("expand") << "found: " << n << endl; + Debug("expand") << " func: " << func << endl; + string name = func.getAttribute(expr::VarNameAttr()); + Debug("expand") << " : \"" << name << "\"" << endl; + } + if(Debug.isOn("expand")) { + Debug("expand") << " defn: " << def.getFunction() << endl + << " ["; + if(formals.size() > 0) { + copy( formals.begin(), formals.end() - 1, + ostream_iterator<Node>(Debug("expand"), ", ") ); + Debug("expand") << formals.back(); + } + Debug("expand") << "]" << endl + << " " << def.getFunction().getType() << endl + << " " << def.getFormula() << endl; + } + + fm = def.getFormula(); + } + + Node instance = fm.substitute(formals.begin(), formals.end(), + n.begin(), n.end()); + Debug("expand") << "made : " << instance << endl; + + Node expanded = expandDefinitions(instance, cache, expandOnly); + cache[n] = (n == expanded ? Node::null() : expanded); + result.push(expanded); + continue; + + } else if(! expandOnly) { + // do not do any theory stuff if expandOnly is true + + theory::Theory* t = d_smt->d_theoryEngine->theoryOf(node); + + Assert(t != NULL); + LogicRequest req(*d_smt); + node = t->expandDefinition(req, n); + } + + // there should be children here, otherwise we short-circuited a result-push/continue, above + if (node.getNumChildren() == 0) { + Debug("expand") << "Unexpectedly no children..." << node << endl; + } + // This invariant holds at the moment but it is concievable that a new theory + // might introduce a kind which can have children before definition expansion but doesn't + // afterwards. If this happens, remove this assertion. + Assert(node.getNumChildren() > 0); + + // the partial functions can fall through, in which case we still + // consider their children + worklist.push(make_triple(Node(n), node, true)); // Original and rewritten result + + for(size_t i = 0; i < node.getNumChildren(); ++i) { + worklist.push(make_triple(node[i], node[i], false)); // Rewrite the children of the result only + } + + } else { + // Working upwards + // Reconstruct the node from it's (now rewritten) children on the stack + + Debug("expand") << "cons : " << node << endl; + //cout << "cons : " << node << endl; + NodeBuilder<> nb(node.getKind()); + if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { + Debug("expand") << "op : " << node.getOperator() << endl; + //cout << "op : " << node.getOperator() << endl; + nb << node.getOperator(); + } + for(size_t i = 0; i < node.getNumChildren(); ++i) { + Assert(!result.empty()); + Node expanded = result.top(); + result.pop(); + //cout << "exchld : " << expanded << endl; + Debug("expand") << "exchld : " << expanded << endl; + nb << expanded; + } + node = nb; + cache[n] = n == node ? Node::null() : node; // Only cache once all subterms are expanded + result.push(node); + } + } while(!worklist.empty()); + + AlwaysAssert(result.size() == 1); + + return result.top(); } PreprocessingPassResult ExpandingDefinitionsPass::apply(AssertionPipeline* assertionsToPreprocess){ -/* Chat() << "expanding definitions..." << std::endl; + Chat() << "expanding definitions..." << std::endl; Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl; TimerStat::CodeTimer codeTimer(d_definitionExpansionTime); hash_map<Node, Node, NodeHashFunction> cache; for(unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) { assertionsToPreprocess->replace(i, expandDefinitions((*assertionsToPreprocess)[i], cache)); - }*/ + } return PreprocessingPassResult(true); } @@ -501,6 +670,78 @@ PreprocessingPassResult BVAbstractionPass::apply(AssertionPipeline* assertionsTo return PreprocessingPassResult(true); } +ConstrainSubtypesPass::ConstrainSubtypesPass(ResourceManager* resourceManager, SmtEngine* smt) : PreprocessingPass(resourceManager), d_smt(smt) { +} + +void ConstrainSubtypesPass::constrainSubtypes(TNode top, AssertionPipeline& assertions) + throw() { + Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top << endl; + + set<TNode> done; + stack<TNode> worklist; + worklist.push(top); + done.insert(top); + + do { + TNode n = worklist.top(); + worklist.pop(); + + TypeNode t = n.getType(); + if(t.isPredicateSubtype()) { + WarningOnce() << "Warning: CVC4 doesn't yet do checking that predicate subtypes are nonempty domains" << endl; + Node pred = t.getSubtypePredicate(); + Kind k; + // pred can be a LAMBDA, a function constant, or a datatype tester + Trace("constrainSubtypes") << "constrainSubtypes(): pred.getType() == " << pred.getType() << endl; + if(d_smt->d_definedFunctions->find(pred) != d_smt->d_definedFunctions->end()) { + k = kind::APPLY; + } else if(pred.getType().isTester()) { + k = kind::APPLY_TESTER; + } else { + k = kind::APPLY_UF; + } + Node app = NodeManager::currentNM()->mkNode(k, pred, n); + Trace("constrainSubtypes") << "constrainSubtypes(): assert(" << k << ") " << app << endl; + assertions.push_back(app); + } else if(t.isSubrange()) { + SubrangeBounds bounds = t.getSubrangeBounds(); + Trace("constrainSubtypes") << "constrainSubtypes(): got bounds " << bounds << endl; + if(bounds.lower.hasBound()) { + Node c = NodeManager::currentNM()->mkConst(Rational(bounds.lower.getBound())); + Node lb = NodeManager::currentNM()->mkNode(kind::LEQ, c, n); + Trace("constrainSubtypes") << "constrainSubtypes(): assert " << lb << endl; + assertions.push_back(lb); + } + if(bounds.upper.hasBound()) { + Node c = NodeManager::currentNM()->mkConst(Rational(bounds.upper.getBound())); + Node ub = NodeManager::currentNM()->mkNode(kind::LEQ, n, c); + Trace("constrainSubtypes") << "constrainSubtypes(): assert " << ub << endl; + assertions.push_back(ub); + } + } + + for(TNode::iterator i = n.begin(); i != n.end(); ++i) { + if(done.find(*i) == done.end()) { + worklist.push(*i); + done.insert(*i); + } + } + } while(! worklist.empty()); +} + +PreprocessingPassResult ConstrainSubtypesPass::apply(AssertionPipeline* assertionsToPreprocess){ + // Any variables of subtype types need to be constrained properly. + // Careful, here: constrainSubtypes() adds to the back of + // d_assertions, but we don't need to reprocess those. + // We also can't use an iterator, because the vector may be moved in + // memory during this loop. + Chat() << "constraining subtypes..." << endl; + for(unsigned i = 0, i_end = assertionsToPreprocess->size(); i != i_end; ++i) { + constrainSubtypes((*assertionsToPreprocess)[i], *assertionsToPreprocess); + } + return PreprocessingPassResult(true); +} + UnconstrainedSimpPass::UnconstrainedSimpPass(ResourceManager* resourceManager, TimerStat unconstrainedSimpTime, TheoryEngine* theoryEngine) : PreprocessingPass(resourceManager), @@ -833,6 +1074,7 @@ PreprocessingPassResult NoConflictPass::apply(AssertionPipeline* assertionsToPre return PreprocessingPassResult(true); } +/** RepeatSimpPass::RepeatSimpPass(ResourceManager* resourceManager, theory::SubstitutionMap* topLevelSubstitutions, unsigned simplifyAssertionsDepth, bool* noConflict, @@ -904,7 +1146,7 @@ void RepeatSimpPass::collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<Nod PreprocessingPassResult RepeatSimpPass::apply(AssertionPipeline* assertionsToPreprocess){ - /* Chat() << "re-simplifying assertions..." << std::endl; + Chat() << "re-simplifying assertions..." << std::endl; ScopeCounter depth(d_simplifyAssertionsDepth); // *noConflict &= simplifyAssertions(); if (*noConflict) { @@ -969,21 +1211,391 @@ PreprocessingPassResult RepeatSimpPass::apply(AssertionPipeline* assertionsToPre removeITEs(); // Assert(iteRewriteAssertionsEnd == d_assertions.size()); } - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << std::endl;*/ + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << std::endl; return PreprocessingPassResult(true); } SimplifyAssertionsPass::SimplifyAssertionsPass( - ResourceManager* resourceManager, unsigned simplifyAssertionsDepth) : + ResourceManager* resourceManager, unsigned simplifyAssertionsDepth, + SmtEngine* smt, bool propagatorNeedsFinish, + theory::booleans::CircuitPropagator propagator, + context::CDO<unsigned> substitutionsIndex, + std::vector<Node> nonClausalLearnedLiterals, Node dtrue, + TimerStat nonclausalSimplificationTime) : PreprocessingPass(resourceManager), - d_simplifyAssertionsDepth(simplifyAssertionsDepth){ + d_simplifyAssertionsDepth(simplifyAssertionsDepth), + d_smt(smt), d_propagatorNeedsFinish(propagatorNeedsFinish), + d_propagator(propagator), d_substitutionsIndex(substitutionsIndex), + d_nonClausalLearnedLiterals(nonClausalLearnedLiterals), + d_true(dtrue), d_nonclausalSimplificationTime(nonclausalSimplificationTime) { +} + +void SimplifyAssertionsPass::addFormula(TNode n, bool inUnsatCore, bool inInput, AssertionPipeline d_assertions) + throw(TypeCheckingException, LogicException) { + + if (n == d_true) { + // nothing to do + return; + } + + Trace("smt") << "SmtEnginePrivate::addFormula(" << n << "), inUnsatCore = " << inUnsatCore << ", inInput = " << inInput << endl; + + // Give it to proof manager + PROOF( + if( inInput ){ + // n is an input assertion + if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) { + + ProofManager::currentPM()->addCoreAssertion(n.toExpr()); + } + }else{ + // n is the result of an unknown preprocessing step, add it to dependency map to null + ProofManager::currentPM()->addDependence(n, Node::null()); + } + // rewrite rules are by default in the unsat core because + // they need to be applied until saturation + if(options::unsatCores() && + n.getKind() == kind::REWRITE_RULE ){ + ProofManager::currentPM()->addUnsatCore(n.toExpr()); + } + ); + + // Add the normalized formula to the queue + d_assertions.push_back(n); + //d_assertions.push_back(Rewriter::rewrite(n)); +} + +// returns false if it learns a conflict +bool SimplifyAssertionsPass::nonClausalSimplify(AssertionPipeline &d_assertions) { + spendResource(options::preprocessStep()); + d_smt->finalOptionsAreSet(); + + if(options::unsatCores() || options::fewerPreprocessingHoles()) { + return true; + } + + TimerStat::CodeTimer nonclausalTimer(d_nonclausalSimplificationTime); + + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl; + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + Trace("simplify") << "Assertion #" << i << " : " << d_assertions[i] << std::endl; + } + + if(d_propagatorNeedsFinish) { + d_propagator.finish(); + d_propagatorNeedsFinish = false; + } + d_propagator.initialize(); + + // Assert all the assertions to the propagator + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " + << "asserting to propagator" << endl; + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]); + // Don't reprocess substitutions + if (d_substitutionsIndex > 0 && i == d_substitutionsIndex) { + continue; + } + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertions[i] << endl; + Debug("cores") << "d_propagator assertTrue: " << d_assertions[i] << std::endl; + d_propagator.assertTrue(d_assertions[i]); + } + + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " + << "propagating" << endl; + if (d_propagator.propagate()) { + // If in conflict, just return false + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " + << "conflict in non-clausal propagation" << endl; + Node falseNode = NodeManager::currentNM()->mkConst<bool>(false); + Assert(!options::unsatCores() && !options::fewerPreprocessingHoles()); + d_assertions.clear(); + addFormula(falseNode, false, false, d_assertions); + d_propagatorNeedsFinish = true; + return false; + } + + + Trace("simplify") << "Iterate through " << d_nonClausalLearnedLiterals.size() << " learned literals." << std::endl; + // No conflict, go through the literals and solve them + theory::SubstitutionMap constantPropagations(d_smt->d_context); + theory::SubstitutionMap newSubstitutions(d_smt->d_context); + theory::SubstitutionMap::iterator pos; + unsigned j = 0; + for(unsigned i = 0, i_end = d_nonClausalLearnedLiterals.size(); i < i_end; ++ i) { + // Simplify the literal we learned wrt previous substitutions + Node learnedLiteral = d_nonClausalLearnedLiterals[i]; + Assert(theory::Rewriter::rewrite(learnedLiteral) == learnedLiteral); + Assert(d_topLevelSubstitutions.apply(learnedLiteral) == learnedLiteral); + Trace("simplify") << "Process learnedLiteral : " << learnedLiteral << std::endl; + Node learnedLiteralNew = newSubstitutions.apply(learnedLiteral); + if (learnedLiteral != learnedLiteralNew) { + learnedLiteral = theory::Rewriter::rewrite(learnedLiteralNew); + } + Trace("simplify") << "Process learnedLiteral, after newSubs : " << learnedLiteral << std::endl; + for (;;) { + learnedLiteralNew = constantPropagations.apply(learnedLiteral); + if (learnedLiteralNew == learnedLiteral) { + break; + } + ++d_smt->d_stats->d_numConstantProps; + learnedLiteral = theory::Rewriter::rewrite(learnedLiteralNew); + } + Trace("simplify") << "Process learnedLiteral, after constProp : " << learnedLiteral << std::endl; + // It might just simplify to a constant + if (learnedLiteral.isConst()) { + if (learnedLiteral.getConst<bool>()) { + // If the learned literal simplifies to true, it's redundant + continue; + } else { + // If the learned literal simplifies to false, we're in conflict + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " + << "conflict with " + << d_nonClausalLearnedLiterals[i] << endl; + Assert(!options::unsatCores()); + d_assertions.clear(); + addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false, d_assertions); + d_propagatorNeedsFinish = true; + return false; + } + } + + // Solve it with the corresponding theory, possibly adding new + // substitutions to newSubstitutions + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " + << "solving " << learnedLiteral << endl; + + Theory::PPAssertStatus solveStatus = + d_smt->d_theoryEngine->solve(learnedLiteral, newSubstitutions); + + switch (solveStatus) { + case Theory::PP_ASSERT_STATUS_SOLVED: { + // The literal should rewrite to true + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " + << "solved " << learnedLiteral << endl; + Assert(theory::Rewriter::rewrite(newSubstitutions.apply(learnedLiteral)).isConst()); + // vector<pair<Node, Node> > equations; + // constantPropagations.simplifyLHS(d_topLevelSubstitutions, equations, true); + // if (equations.empty()) { + // break; + // } + // Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second); + // else fall through + break; + } + case Theory::PP_ASSERT_STATUS_CONFLICT: + // If in conflict, we return false + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " + << "conflict while solving " + << learnedLiteral << endl; + Assert(!options::unsatCores()); + d_assertions.clear(); + addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false, d_assertions); + d_propagatorNeedsFinish = true; + return false; + default: + if (d_doConstantProp && learnedLiteral.getKind() == kind::EQUAL && (learnedLiteral[0].isConst() || learnedLiteral[1].isConst())) { + // constant propagation + TNode t; + TNode c; + if (learnedLiteral[0].isConst()) { + t = learnedLiteral[1]; + c = learnedLiteral[0]; + } + else { + t = learnedLiteral[0]; + c = learnedLiteral[1]; + } + Assert(!t.isConst()); + Assert(constantPropagations.apply(t) == t); + Assert(d_topLevelSubstitutions.apply(t) == t); + Assert(newSubstitutions.apply(t) == t); + constantPropagations.addSubstitution(t, c); + // vector<pair<Node,Node> > equations; + // constantPropagations.simplifyLHS(t, c, equations, true); + // if (!equations.empty()) { + // Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second); + // d_assertions.clear(); + // addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false); + // return; + // } + // d_topLevelSubstitutions.simplifyRHS(constantPropagations); + } + else { + // Keep the literal + d_nonClausalLearnedLiterals[j++] = d_nonClausalLearnedLiterals[i]; + } + break; + } + } + +#ifdef CVC4_ASSERTIONS + // NOTE: When debugging this code, consider moving this check inside of the + // loop over d_nonClausalLearnedLiterals. This check has been moved outside + // because it is costly for certain inputs (see bug 508). + // + // Check data structure invariants: + // 1. for each lhs of d_topLevelSubstitutions, does not appear anywhere in rhs of d_topLevelSubstitutions or anywhere in constantPropagations + // 2. each lhs of constantPropagations rewrites to itself + // 3. if l -> r is a constant propagation and l is a subterm of l' with l' -> r' another constant propagation, then l'[l/r] -> r' should be a + // constant propagation too + // 4. each lhs of constantPropagations is different from each rhs + for (pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos) { + Assert((*pos).first.isVar()); + Assert(d_topLevelSubstitutions.apply((*pos).first) == (*pos).first); + Assert(d_topLevelSubstitutions.apply((*pos).second) == (*pos).second); + Assert(newSubstitutions.apply(newSubstitutions.apply((*pos).second)) == newSubstitutions.apply((*pos).second)); + } + for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) { + Assert((*pos).second.isConst()); + Assert(theory::Rewriter::rewrite((*pos).first) == (*pos).first); + // Node newLeft = d_topLevelSubstitutions.apply((*pos).first); + // if (newLeft != (*pos).first) { + // newLeft = Rewriter::rewrite(newLeft); + // Assert(newLeft == (*pos).second || + // (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second)); + // } + // newLeft = constantPropagations.apply((*pos).first); + // if (newLeft != (*pos).first) { + // newLeft = Rewriter::rewrite(newLeft); + // Assert(newLeft == (*pos).second || + // (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second)); + // } + Assert(constantPropagations.apply((*pos).second) == (*pos).second); + } +//#endif CVC4_ASSERTIONS + + // Resize the learnt + Trace("simplify") << "Resize non-clausal learned literals to " << j << std::endl; + d_nonClausalLearnedLiterals.resize(j); + + hash_set<TNode, TNodeHashFunction> s; + Trace("debugging") << "NonClausal simplify pre-preprocess\n"; + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + Node assertion = d_assertions[i]; + Node assertionNew = newSubstitutions.apply(assertion); + Trace("debugging") << "assertion = " << assertion << endl; + Trace("debugging") << "assertionNew = " << assertionNew << endl; + if (assertion != assertionNew) { + assertion = theory::Rewriter::rewrite(assertionNew); + Trace("debugging") << "rewrite(assertion) = " << assertion << endl; + } + Assert(theory::Rewriter::rewrite(assertion) == assertion); + for (;;) { + assertionNew = constantPropagations.apply(assertion); + if (assertionNew == assertion) { + break; + } + ++d_smt->d_stats->d_numConstantProps; + Trace("debugging") << "assertionNew = " << assertionNew << endl; + assertion = theory::Rewriter::rewrite(assertionNew); + Trace("debugging") << "assertionNew = " << assertionNew << endl; + } + Trace("debugging") << "\n"; + s.insert(assertion); + d_assertions.replace(i, assertion); + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " + << "non-clausal preprocessed: " + << assertion << endl; + } + + // If in incremental mode, add substitutions to the list of assertions + if (d_substitutionsIndex > 0) { + NodeBuilder<> substitutionsBuilder(kind::AND); + substitutionsBuilder << d_assertions[d_substitutionsIndex]; + pos = newSubstitutions.begin(); + for (; pos != newSubstitutions.end(); ++pos) { + // Add back this substitution as an assertion + TNode lhs = (*pos).first, rhs = newSubstitutions.apply((*pos).second); + Node n = NodeManager::currentNM()->mkNode(kind::EQUAL, lhs, rhs); + substitutionsBuilder << n; + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n << endl; + } + if (substitutionsBuilder.getNumChildren() > 1) { + d_assertions.replace(d_substitutionsIndex, + theory::Rewriter::rewrite(Node(substitutionsBuilder))); + } + } else { + // If not in incremental mode, must add substitutions to model + TheoryModel* m = d_smt->d_theoryEngine->getModel(); + if(m != NULL) { + for(pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos) { + Node n = (*pos).first; + Node v = newSubstitutions.apply((*pos).second); + Trace("model") << "Add substitution : " << n << " " << v << endl; + m->addSubstitution( n, v ); + } + } + } + + NodeBuilder<> learnedBuilder(kind::AND); + Assert(d_realAssertionsEnd <= d_assertions.size()); + learnedBuilder << d_assertions[d_realAssertionsEnd - 1]; + + for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) { + Node learned = d_nonClausalLearnedLiterals[i]; + Assert(d_topLevelSubstitutions.apply(learned) == learned); + Node learnedNew = newSubstitutions.apply(learned); + if (learned != learnedNew) { + learned = theory::Rewriter::rewrite(learnedNew); + } + Assert(theory::Rewriter::rewrite(learned) == learned); + for (;;) { + learnedNew = constantPropagations.apply(learned); + if (learnedNew == learned) { + break; + } + ++d_smt->d_stats->d_numConstantProps; + learned = theory::Rewriter::rewrite(learnedNew); + } + if (s.find(learned) != s.end()) { + continue; + } + s.insert(learned); + learnedBuilder << learned; + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " + << "non-clausal learned : " + << learned << endl; + } + d_nonClausalLearnedLiterals.clear(); + + for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) { + Node cProp = (*pos).first.eqNode((*pos).second); + Assert(d_topLevelSubstitutions.apply(cProp) == cProp); + Node cPropNew = newSubstitutions.apply(cProp); + if (cProp != cPropNew) { + cProp = theory::Rewriter::rewrite(cPropNew); + Assert(theory::Rewriter::rewrite(cProp) == cProp); + } + if (s.find(cProp) != s.end()) { + continue; + } + s.insert(cProp); + learnedBuilder << cProp; + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " + << "non-clausal constant propagation : " + << cProp << endl; + } + + // Add new substitutions to topLevelSubstitutions + // Note that we don't have to keep rhs's in full solved form + // because SubstitutionMap::apply does a fixed-point iteration when substituting + d_topLevelSubstitutions.addSubstitutions(newSubstitutions); + + if(learnedBuilder.getNumChildren() > 1) { + d_assertions.replace(d_realAssertionsEnd - 1, + theory::Rewriter::rewrite(Node(learnedBuilder))); + } + + d_propagatorNeedsFinish = true; + return true; } // returns false if simplification led to "false" PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* assertionsToPreprocess) throw(TypeCheckingException, LogicException, UnsafeInterruptException) { - /* spendResource(options::preprocessStep()); - Assert(d_smt.d_pendingPops == 0); + spendResource(options::preprocessStep()); + Assert(d_smt->d_pendingPops == 0); try { ScopeCounter depth(d_simplifyAssertionsDepth); @@ -996,7 +1608,7 @@ PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* asserti Chat() << "...performing nonclausal simplification..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): " << "performing non-clausal simplification" << endl; - bool noConflict = nonClausalSimplify(); + bool noConflict = nonClausalSimplify(*assertionsToPreprocess); if(!noConflict) { return false; } @@ -1008,7 +1620,7 @@ PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* asserti // miplib rewrites aren't safe in incremental mode ! options::incrementalSolving() && // only useful in arith - d_smt.d_logic.isTheoryEnabled(THEORY_ARITH) && + d_smt->d_logic.isTheoryEnabled(THEORY_ARITH) && // we add new assertions and need this (in practice, this // restriction only disables miplib processing during // re-simplification, which we don't expect to be useful anyway) @@ -1017,7 +1629,7 @@ PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* asserti Trace("simplify") << "SmtEnginePrivate::simplify(): " << "looking for miplib pseudobooleans..." << endl; - TimerStat::CodeTimer miplibTimer(d_smt.d_stats->d_miplibPassTime); + TimerStat::CodeTimer miplibTimer(d_smt->d_stats->d_miplibPassTime); doMiplibTrick(); } else { @@ -1031,20 +1643,20 @@ PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* asserti Debug("smt") << " d_assertions : " << assertionsToPreprocess->size() << endl; // before ppRewrite check if only core theory for BV theory - d_smt.d_theoryEngine->staticInitializeBVOptions(assertionsToPreprocess->ref()); + d_smt->d_theoryEngine->staticInitializeBVOptions(assertionsToPreprocess->ref()); dumpAssertions("pre-theorypp", *assertionsToPreprocess); // Theory preprocessing - if (d_smt.d_earlyTheoryPP) { + if (d_smt->d_earlyTheoryPP) { Chat() << "...doing early theory preprocessing..." << endl; - TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime); + TimerStat::CodeTimer codeTimer(d_smt->d_stats->d_theoryPreprocessTime); // Call the theory preprocessors - d_smt.d_theoryEngine->preprocessStart(); + d_smt->d_theoryEngine->preprocessStart(); for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) { - Assert(Rewriter::rewrite((*assertionsToPreprocess)[i]) == (*assertionsTopreprocess)[i]); - assertionsToPreprocess->replace(i, d_smt.d_theoryEngine->preprocess((*assertionsToPreprocess)[i])); - Assert(Rewriter::rewrite((*assertionsToPreprocess)[i]) == (*assertionsToPreprocess)[i]); + Assert(theory::Rewriter::rewrite((*assertionsToPreprocess)[i]) == (*assertionsTopreprocess)[i]); + assertionsToPreprocess->replace(i, d_smt->d_theoryEngine->preprocess((*assertionsToPreprocess)[i])); + Assert(theory::Rewriter::rewrite((*assertionsToPreprocess)[i]) == (*assertionsToPreprocess)[i]); } } @@ -1070,7 +1682,7 @@ PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* asserti // Unconstrained simplification if(options::unconstrainedSimp()) { Chat() << "...doing unconstrained simplification..." << endl; - preproc::UnconstrainedSimpPass pass(d_resourceManager, d_smt.d_stats->d_unconstrainedSimpTime, d_smt.d_theoryEngine); + preproc::UnconstrainedSimpPass pass(d_resourceManager, d_smt->d_stats->d_unconstrainedSimpTime, d_smt->d_theoryEngine); pass.apply(assertionsToPreprocess); } @@ -1082,7 +1694,7 @@ PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* asserti Chat() << "...doing another round of nonclausal simplification..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): " << " doing repeated simplification" << endl; - bool noConflict = nonClausalSimplify(); + bool noConflict = nonClausalSimplify(*assertionsToPreprocess); if(!noConflict) { return false; } @@ -1102,10 +1714,10 @@ PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* asserti ss << "A bad expression was produced. Original exception follows:\n" << tcep; InternalError(ss.str().c_str()); - }*/ + } return PreprocessingPassResult(true); } - +**/ } // namespace preproc } // namespace CVC4 diff --git a/src/preproc/preprocessing_passes_core.h b/src/preproc/preprocessing_passes_core.h index c27890853..0e113a761 100644 --- a/src/preproc/preprocessing_passes_core.h +++ b/src/preproc/preprocessing_passes_core.h @@ -6,6 +6,7 @@ #include "preproc/preprocessing_pass.h" #include "theory/substitutions.h" #include "theory/arith/pseudoboolean_proc.h" +#include "theory/booleans/circuit_propagator.h" #include "smt/smt_engine.h" #include "smt/term_formula_removal.h" #include "decision/decision_engine.h" @@ -20,10 +21,13 @@ typedef context::CDList<Node> NodeList; class ExpandingDefinitionsPass : public PreprocessingPass { public: virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); - ExpandingDefinitionsPass(ResourceManager* resourceManager, TimerStat definitionExpansionTime); + ExpandingDefinitionsPass(ResourceManager* resourceManager, SmtEngine* smt, TimerStat definitionExpansionTime); private: + SmtEngine* d_smt; TimerStat d_definitionExpansionTime; - Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly); + Node expandDefinitions(TNode n, NodeToNodeHashMap& cache, + bool expandOnly = false) + throw(TypeCheckingException, LogicException, UnsafeInterruptException); }; class NlExtPurifyPass : public PreprocessingPass { @@ -82,6 +86,16 @@ class BVAbstractionPass : public PreprocessingPass { void bvAbstraction(AssertionPipeline* assertionsToPreprocess); }; +class ConstrainSubtypesPass : public PreprocessingPass { + public: + virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); + ConstrainSubtypesPass(ResourceManager* resourceManager, SmtEngine* smt); + private: + SmtEngine* d_smt; + void constrainSubtypes(TNode n, AssertionPipeline& assertions) + throw(); +}; + class UnconstrainedSimpPass : public PreprocessingPass { public: virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); @@ -201,7 +215,8 @@ class NoConflictPass : public PreprocessingPass { unsigned d_realAssertionsEnd; IteSkolemMap* d_iteSkolemMap; }; - + +/* class RepeatSimpPass : public PreprocessingPass { public: virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); @@ -221,11 +236,21 @@ class SimplifyAssertionsPass : public PreprocessingPass { public: virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess) throw(TypeCheckingException, LogicException, UnsafeInterruptException); - SimplifyAssertionsPass(ResourceManager* resourceManager, unsigned simplifyAssertionsDepth); + SimplifyAssertionsPass(ResourceManager* resourceManager, unsigned simplifyAssertionsDepth, SmtEngine* smt, bool propagatorNeedsFinish, theory::booleans::CircuitPropagator propagator, context::CDO<unsigned> substitutionsIndex, std::vector<Node> nonClausalLearnedLiterals, Node dtrue, TimerStat nonclausalSimplificationTime); private: - unsigned d_simplifyAssertionsDepth; - + unsigned d_simplifyAssertionsDepth; + SmtEngine* d_smt; + bool d_propagatorNeedsFinish; + theory::booleans::CircuitPropagator d_propagator; + context::CDO<unsigned> d_substitutionsIndex; + std::vector<Node> d_nonClausalLearnedLiterals; + Node d_true; + TimerStat d_nonclausalSimplificationTime; + bool nonClausalSimplify(AssertionPipeline &d_assertions); + void addFormula(TNode n, bool inUnsatCore, bool inInput = true, AssertionPipeline d_assertions) + throw(TypeCheckingException, LogicException); }; +*/ } // namespace preproc } // namespace CVC4 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4819d9674..63840cb52 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -142,7 +142,8 @@ public: * support getValue() over defined functions, to support user output * in terms of defined functions, etc. */ -class DefinedFunction { + +/*class DefinedFunction { Node d_func; vector<Node> d_formals; Node d_formula; @@ -156,7 +157,8 @@ public: Node getFunction() const { return d_func; } vector<Node> getFormals() const { return d_formals; } Node getFormula() const { return d_formula; } -};/* class DefinedFunction */ +};*/ +/* class DefinedFunction */ /*class AssertionPipeline { vector<Node> d_nodes; @@ -1028,7 +1030,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_userContext->push(); d_context->push(); - d_definedFunctions = new(true) DefinedFunctionMap(d_userContext); + d_definedFunctions = new(true) DefinedFunctionMap(d_userContext); d_fmfRecFunctionsDefined = new(true) NodeList(d_userContext); d_modelCommands = new(true) smt::CommandList(d_userContext); } @@ -3573,16 +3575,10 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-definition-expansion" << endl; dumpAssertions("pre-definition-expansion", d_assertions); { -/* preproc::ExpandingDefinitionsPass pass(d_resourceManager, d_smt.d_stats->d_definitionExpansionTime); - pass.apply(&d_assertions);*/ - Chat() << "expanding definitions..." << endl; - Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl; - TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime); - hash_map<Node, Node, NodeHashFunction> cache; - for(unsigned i = 0; i < d_assertions.size(); ++ i) { - d_assertions.replace(i, expandDefinitions(d_assertions[i], cache)); - } - } + preproc::ExpandingDefinitionsPass pass(d_resourceManager, &d_smt, d_smt.d_stats->d_definitionExpansionTime); + pass.apply(&d_assertions); + } + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl; dumpAssertions("post-definition-expansion", d_assertions); @@ -3644,16 +3640,9 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("pre-constrain-subtypes", d_assertions); { - // Any variables of subtype types need to be constrained properly. - // Careful, here: constrainSubtypes() adds to the back of - // d_assertions, but we don't need to reprocess those. - // We also can't use an iterator, because the vector may be moved in - // memory during this loop. - Chat() << "constraining subtypes..." << endl; - for(unsigned i = 0, i_end = d_assertions.size(); i != i_end; ++i) { - constrainSubtypes(d_assertions[i], d_assertions); - } - } + preproc::ConstrainSubtypesPass pass(d_resourceManager, &d_smt); + pass.apply(&d_assertions); + } dumpAssertions("post-constrain-subtypes", d_assertions); Debug("smt") << " d_assertions : " << d_assertions.size() << endl; @@ -3781,12 +3770,12 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("pre-repeat-simplify", d_assertions); if(options::repeatSimp()) { - preproc::SimplifyAssertionsPass pass(d_resourceManager, d_simplifyAssertionsDepth); +/* preproc::SimplifyAssertionsPass pass(d_resourceManager, d_simplifyAssertionsDepth, &d_smt, d_propagatorNeedsFinish, d_propagator, d_substitutionsIndex, d_nonClausalLearnedLiterals, d_true, d_smt.d_stats->d_nonclausalSimplificationTime); noConflict &= pass.apply(&d_assertions).d_noConflict; preproc::RepeatSimpPass pass1(d_resourceManager, &d_topLevelSubstitutions, d_simplifyAssertionsDepth, &noConflict, d_iteSkolemMap, d_realAssertionsEnd); - pass1.apply(&d_assertions); -/* Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl; + pass1.apply(&d_assertions);*/ + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl; Chat() << "re-simplifying assertions..." << endl; ScopeCounter depth(d_simplifyAssertionsDepth); noConflict &= simplifyAssertions(); @@ -3852,7 +3841,7 @@ void SmtEnginePrivate::processAssertions() { removeITEs(); // Assert(iteRewriteAssertionsEnd == d_assertions.size()); } - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl;*/ + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl; } dumpAssertions("post-repeat-simplify", d_assertions); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 8de31809e..faf718334 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -88,7 +88,7 @@ namespace smt { * support getValue() over defined functions, to support user output * in terms of defined functions, etc. */ - class DefinedFunction; +// class DefinedFunction; struct SmtEngineStatistics; class SmtEnginePrivate; @@ -106,8 +106,12 @@ namespace theory { }/* CVC4::theory namespace */ namespace preproc{ + class DefinedFunction; class DoStaticLearningPass; class QuantifiedPass; + class SimplifyAssertionsPass; + class ExpandingDefinitionsPass; + class ConstrainSubtypesPass; }/* CVC4::preproc namespace */ // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the @@ -123,7 +127,7 @@ namespace preproc{ class CVC4_PUBLIC SmtEngine { /** The type of our internal map of defined functions */ - typedef context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction> + typedef context::CDHashMap<Node, preproc::DefinedFunction, NodeHashFunction> DefinedFunctionMap; /** The type of our internal assertion list */ typedef context::CDList<Expr> AssertionList; @@ -352,9 +356,12 @@ class CVC4_PUBLIC SmtEngine { * be called when d_logic is updated. */ void setLogicInternal() throw(); - + friend class ::CVC4::preproc::DefinedFunction; friend class ::CVC4::preproc::DoStaticLearningPass; friend class ::CVC4::preproc::QuantifiedPass; + friend class ::CVC4::preproc::SimplifyAssertionsPass; + friend class ::CVC4::preproc::ExpandingDefinitionsPass; + friend class ::CVC4::preproc::ConstrainSubtypesPass; friend class ::CVC4::smt::SmtEnginePrivate; friend class ::CVC4::smt::SmtScope; friend class ::CVC4::smt::BooleanTermConverter; |