summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r--src/theory/quantifiers_engine.h388
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback