diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/theory/quantifiers_engine.h | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 388 |
1 files changed, 388 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h new file mode 100644 index 000000000..d0c5fb00b --- /dev/null +++ b/src/theory/quantifiers_engine.h @@ -0,0 +1,388 @@ +/********************* */ +/*! \file quantifiers_engine.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Theory instantiator, Instantiation Engine classes + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS_ENGINE_H +#define __CVC4__THEORY__QUANTIFIERS_ENGINE_H + +#include "theory/theory.h" +#include "util/hash.h" +#include "theory/trigger.h" + +#include "util/stats.h" + +#include <ext/hash_set> +#include <iostream> +#include <map> + +namespace CVC4 { + +class TheoryEngine; + +// attribute for "contains instantiation constants from" +struct InstConstantAttributeId {}; +typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute; + +struct InstLevelAttributeId {}; +typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute; + +struct InstVarNumAttributeId {}; +typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute; + +namespace theory { + +class QuantifiersEngine; + +class InstStrategy { +public: + enum Status { + STATUS_UNFINISHED, + STATUS_UNKNOWN, + STATUS_SAT, + };/* enum Status */ +protected: + /** reference to the instantiation engine */ + QuantifiersEngine* d_quantEngine; +protected: + /** giving priorities */ + std::vector< InstStrategy* > d_priority_over; + /** do not instantiate list */ + std::vector< Node > d_no_instantiate; + std::vector< Node > d_no_instantiate_temp; + /** reset instantiation */ + virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; + /** process method */ + virtual int process( Node f, Theory::Effort effort, int e, int limitInst = 0 ) = 0; +public: + InstStrategy( QuantifiersEngine* ie ) : d_quantEngine( ie ){} + virtual ~InstStrategy(){} + + /** reset instantiation */ + void resetInstantiationRound( Theory::Effort effort ); + /** do instantiation round method */ + int doInstantiation( Node f, Theory::Effort effort, int e, int limitInst = 0 ); + /** update status */ + static void updateStatus( int& currStatus, int addStatus ){ + if( addStatus==STATUS_UNFINISHED ){ + currStatus = STATUS_UNFINISHED; + }else if( addStatus==STATUS_UNKNOWN ){ + if( currStatus==STATUS_SAT ){ + currStatus = STATUS_UNKNOWN; + } + } + } + /** identify */ + virtual std::string identify() const { return std::string("Unknown"); } +public: + /** set priority */ + void setPriorityOver( InstStrategy* is ) { d_priority_over.push_back( is ); } + /** set no instantiate */ + void setNoInstantiate( Node n ) { d_no_instantiate.push_back( n ); } + /** should instantiate */ + bool shouldInstantiate( Node n ) { + return std::find( d_no_instantiate_temp.begin(), d_no_instantiate_temp.end(), n )==d_no_instantiate_temp.end(); + } +};/* class InstStrategy */ + +class QuantifiersModule { +public: + QuantifiersModule(){} + ~QuantifiersModule(){} + /* Call during check registerQuantifier has already been called */ + virtual void check( Theory::Effort e ) = 0; + /* Called for new quantifiers */ + virtual void registerQuantifier( Node n ) = 0; + virtual void assertNode( Node n ) = 0; + virtual void propagate( Theory::Effort level ) = 0; + virtual Node explain(TNode n) = 0; +};/* class QuantifiersModule */ + +class TermArgTrie { +private: + bool addTerm2( QuantifiersEngine* qe, Node n, int argIndex ); +public: + /** the data */ + std::map< Node, TermArgTrie > d_data; +public: + bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); } +};/* class TermArgTrie */ + +class TermDb { +private: + /** reference to the quantifiers engine */ + QuantifiersEngine* d_quantEngine; + /** calculated no match terms */ + bool d_matching_active; + /** terms processed */ + std::map< Node, bool > d_processed; +public: + TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ), d_matching_active( true ){} + ~TermDb(){} + /** map from APPLY_UF operators to ground terms for that operator */ + std::map< Node, std::vector< Node > > d_op_map; + /** map from APPLY_UF functions to trie */ + std::map< Node, TermArgTrie > d_func_map_trie; + /** map from APPLY_UF predicates to trie */ + std::map< Node, TermArgTrie > d_pred_map_trie[2]; + /** map from type nodes to terms of that type */ + std::map< TypeNode, std::vector< Node > > d_type_map; + /** add a term to the database */ + void addTerm( Node n, std::vector< Node >& added, bool withinQuant = false ); + /** reset (calculate which terms are active) */ + void reset( Theory::Effort effort ); + /** set active */ + void setMatchingActive( bool a ) { d_matching_active = a; } + /** get active */ + bool getMatchingActive() { return d_matching_active; } +public: + /** parent structure (for efficient E-matching): + n -> op -> index -> L + map from node "n" to a list of nodes "L", where each node n' in L + has operator "op", and n'["index"] = n. + for example, d_parents[n][f][1] = { f( t1, n ), f( t2, n ), ... } + */ + std::map< Node, std::map< Node, std::map< int, std::vector< Node > > > > d_parents; +};/* class TermDb */ + +namespace quantifiers { + class InstantiationEngine; +}/* CVC4::theory::quantifiers */ + +class QuantifiersEngine { + friend class quantifiers::InstantiationEngine; + friend class InstMatch; +private: + typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; + /** reference to theory engine object */ + TheoryEngine* d_te; + /** vector of modules for quantifiers */ + std::vector< QuantifiersModule* > d_modules; + /** equality query class */ + EqualityQuery* d_eq_query; + + /** list of all quantifiers */ + std::vector< Node > d_quants; + /** list of quantifiers asserted in the current context */ + context::CDList<Node> d_forall_asserts; + /** map from universal quantifiers to the list of variables */ + std::map< Node, std::vector< Node > > d_vars; + /** map from universal quantifiers to the list of skolem constants */ + std::map< Node, std::vector< Node > > d_skolem_constants; + /** map from universal quantifiers to their skolemized body */ + std::map< Node, Node > d_skolem_body; + /** map from universal quantifiers to their bound body */ + std::map< Node, Node > d_bound_body; + /** instantiation constants to universal quantifiers */ + std::map< Node, Node > d_inst_constants_map; + /** map from universal quantifiers to their counterexample body */ + std::map< Node, Node > d_counterexample_body; + /** map from universal quantifiers to the list of instantiation constants */ + std::map< Node, std::vector< Node > > d_inst_constants; + /** map from quantifiers to whether they are active */ + BoolMap d_active; + /** lemmas produced */ + std::map< Node, bool > d_lemmas_produced; + /** lemmas waiting */ + std::vector< Node > d_lemmas_waiting; + /** inst matches produced for each quantifier */ + std::map< Node, InstMatchTrie > d_inst_match_trie; + /** free variable for instantiation constant type */ + std::map< TypeNode, Node > d_free_vars; + /** owner of quantifiers */ + std::map< Node, Theory* > d_owner; + /** term database */ + TermDb* d_term_db; + /** universal quantifiers that have been rewritten */ + std::map< Node, std::vector< Node > > d_quant_rewritten; + /** map from rewritten universal quantifiers to the quantifier they are the consequence of */ + std::map< Node, Node > d_rewritten_quant; +private: + /** for computing relavance */ + /** map from quantifiers to symbols they contain */ + std::map< Node, std::vector< Node > > d_syms; + /** map from symbols to quantifiers */ + std::map< Node, std::vector< Node > > d_syms_quants; + /** relevance for quantifiers and symbols */ + std::map< Node, int > d_relevance; + /** compute symbols */ + void computeSymbols( Node n, std::vector< Node >& syms ); +private: + /** helper functions compute phase requirements */ + static void computePhaseReqs2( Node n, bool polarity, std::map< Node, int >& phaseReqs ); + /** set instantiation level attr */ + void setInstantiationLevelAttr( Node n, uint64_t level ); + /** set instantiation constant attr */ + void setInstantiationConstantAttr( Node n, Node f ); + /** make instantiation constants for */ + void makeInstantiationConstantsFor( Node f ); + + KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time"); + +public: + QuantifiersEngine(context::Context* c, TheoryEngine* te); + ~QuantifiersEngine(){} + /** get instantiator for id */ + Instantiator* getInstantiator( int id ); + /** get theory engine */ + TheoryEngine* getTheoryEngine() { return d_te; } + /** get equality query object */ + EqualityQuery* getEqualityQuery() { return d_eq_query; } + /** set equality query object */ + void setEqualityQuery( EqualityQuery* eq ) { d_eq_query = eq; } +public: + /** add module */ + void addModule( QuantifiersModule* qm ) { d_modules.push_back( qm ); } + /** check at level */ + void check( Theory::Effort e ); + /** register (non-rewritten) quantifier */ + void registerQuantifier( Node f ); + /** register (non-rewritten) quantifier */ + void registerPattern( std::vector<Node> & pattern); + /** assert (universal) quantifier */ + void assertNode( Node f ); + /** propagate */ + void propagate( Theory::Effort level ); +public: + /** add lemma lem */ + bool addLemma( Node lem ); + /** instantiate f with arguments terms */ + bool addInstantiation( Node f, std::vector< Node >& terms ); + /** do instantiation specified by m */ + bool addInstantiation( Node f, InstMatch& m, bool addSplits = false ); + /** split on node n */ + bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true ); + /** add split equality */ + bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true ); + /** has added lemma */ + bool hasAddedLemma() { return !d_lemmas_waiting.empty(); } + /** flush lemmas */ + void flushLemmas( OutputChannel* out ); + /** get number of waiting lemmas */ + int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); } +public: + /** get number of quantifiers */ + int getNumQuantifiers() { return (int)d_quants.size(); } + /** get quantifier */ + Node getQuantifier( int i ) { return d_quants[i]; } + /** get number of asserted quantifiers */ + int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); } + /** get asserted quantifier */ + Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; } + /** get instantiation constants */ + void getInstantiationConstantsFor( Node f, std::vector< Node >& ics ) { + ics.insert( ics.begin(), d_inst_constants[f].begin(), d_inst_constants[f].end() ); + } + /** get the i^th instantiation constant of f */ + Node getInstantiationConstant( Node f, int i ) { return d_inst_constants[f][i]; } + /** get number of instantiation constants for f */ + int getNumInstantiationConstants( Node f ) { return (int)d_inst_constants[f].size(); } + std::vector<Node> createInstVariable( std::vector<Node> & vars ); +public: + /** get the ce body f[e/x] */ + Node getCounterexampleBody( Node f ); + /** get the skolemized body f[e/x] */ + Node getSkolemizedBody( Node f ); + /** set active */ + void setActive( Node n, bool val ) { d_active[n] = val; } + /** get active */ + bool getActive( Node n ) { return d_active.find( n )!=d_active.end() && d_active[n]; } +public: + /** phase requirements for each quantifier for each instantiation literal */ + std::map< Node, std::map< Node, bool > > d_phase_reqs; + std::map< Node, std::map< Node, bool > > d_phase_reqs_equality; + std::map< Node, std::map< Node, Node > > d_phase_reqs_equality_term; +public: + /** is phase required */ + bool isPhaseReq( Node f, Node lit ) { return d_phase_reqs[f].find( lit )!=d_phase_reqs[f].end(); } + /** get phase requirement */ + bool getPhaseReq( Node f, Node lit ) { return d_phase_reqs[f].find( lit )==d_phase_reqs[f].end() ? false : d_phase_reqs[f][ lit ]; } + /** get term req terms */ + void getPhaseReqTerms( Node f, std::vector< Node >& nodes ); + /** helper functions compute phase requirements */ + static void computePhaseReqs( Node n, bool polarity, std::map< Node, bool >& phaseReqs ); + /** compute phase requirements */ + void generatePhaseReqs( Node f, Node n ); +public: + /** returns node n with bound vars of f replaced by instantiation constants of f + node n : is the futur pattern + node f : is the quantifier containing which bind the variable + return a pattern where the variable are replaced by variable for + instantiation. + */ + Node getSubstitutedNode( Node n, Node f ); + /** same as before but node f is just linked to the new pattern by the + applied attribute + vars the bind variable + nvars the same variable but with an attribute + */ + Node convertNodeToPattern( Node n, Node f, + const std::vector<Node> & vars, + const std::vector<Node> & nvars); + /** get free variable for instantiation constant */ + Node getFreeVariableForInstConstant( Node n ); + /** get bound variable for variable */ + Node getBoundVariableForVariable( Node n ); +public: + /** has owner */ + bool hasOwner( Node f ) { return d_owner.find( f )!=d_owner.end(); } + /** get owner */ + Theory* getOwner( Node f ) { return d_owner[f]; } + /** set owner */ + void setOwner( Node f, Theory* t ) { d_owner[f] = t; } +public: + /** get term database */ + TermDb* getTermDatabase() { return d_term_db; } + /** add term to database */ + void addTermToDatabase( Node n, bool withinQuant = false ); +private: + /** set relevance */ + void setRelevance( Node s, int r ); +public: + /** get relevance */ + int getRelevance( Node s ) { return d_relevance.find( s )==d_relevance.end() ? -1 : d_relevance[s]; } + /** get number of quantifiers for symbol s */ + int getNumQuantifiersForSymbol( Node s ) { return (int)d_syms_quants[s].size(); } +public: + /** statistics class */ + class Statistics { + public: + IntStat d_num_quant; + IntStat d_instantiation_rounds; + IntStat d_instantiation_rounds_lc; + IntStat d_instantiations; + IntStat d_max_instantiation_level; + IntStat d_splits; + IntStat d_total_inst_var; + IntStat d_total_inst_var_unspec; + IntStat d_inst_unspec; + IntStat d_inst_duplicate; + IntStat d_lit_phase_req; + IntStat d_lit_phase_nreq; + IntStat d_triggers; + IntStat d_simple_triggers; + IntStat d_multi_triggers; + IntStat d_multi_trigger_instantiations; + Statistics(); + ~Statistics(); + };/* class QuantifiersEngine::Statistics */ + Statistics d_statistics; +};/* class QuantifiersEngine */ + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS_ENGINE_H */ |