** Major contributors: none\r
** Minor contributors (to current version): none\r
** This file is part of the CVC4 project.\r
- ** Copyright (c) 2009-2013 New York University and The University of Iowa\r
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa\r
** See the file COPYING in the top-level source directory for licensing\r
** information.\endverbatim\r
**\r
#include "context/cdhashmap.h"\r
#include "context/cdchunk_list.h"\r
#include "theory/quantifiers_engine.h"\r
+#include "theory/quantifiers/term_database.h"\r
\r
namespace CVC4 {\r
namespace theory {\r
namespace quantifiers {\r
\r
-class QcfNode;\r
-\r
class QuantConflictFind;\r
-\r
-class QcfNodeIndex {\r
-public:\r
- std::map< TNode, QcfNodeIndex > d_children;\r
- void clear() { d_children.clear(); }\r
- void debugPrint( const char * c, int t );\r
- Node existsTerm( TNode n, std::vector< TNode >& reps, int index = 0 );\r
- Node addTerm( TNode n, std::vector< TNode >& reps, int index = 0 );\r
-};\r
-\r
class QuantInfo;\r
\r
//match generator\r
class MatchGen {\r
+ friend class QuantInfo;\r
private:\r
//current children information\r
int d_child_counter;\r
//children of this object\r
- //std::vector< int > d_children_order;\r
+ std::vector< int > d_children_order;\r
unsigned getNumChildren() { return d_children.size(); }\r
- //MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }\r
- MatchGen * getChild( int i ) { return &d_children[i]; }\r
+ MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }\r
+ //MatchGen * getChild( int i ) { return &d_children[i]; }\r
//current matching information\r
- std::vector< QcfNodeIndex * > d_qn;\r
- std::vector< std::map< TNode, QcfNodeIndex >::iterator > d_qni;\r
+ std::vector< TermArgTrie * > d_qn;\r
+ std::vector< std::map< TNode, TermArgTrie >::iterator > d_qni;\r
bool doMatching( QuantConflictFind * p, QuantInfo * qi );\r
//for matching : each index is either a variable or a ground term\r
unsigned d_qni_size;\r
std::map< int, TNode > d_qni_gterm;\r
std::map< int, TNode > d_qni_gterm_rep;\r
std::map< int, int > d_qni_bound;\r
+ std::vector< int > d_qni_bound_except;\r
std::map< int, TNode > d_qni_bound_cons;\r
std::map< int, int > d_qni_bound_cons_var;\r
std::map< int, int >::iterator d_binding_it;\r
+ //std::vector< int > d_independent;\r
+ bool d_matched_basis;\r
bool d_binding;\r
//int getVarBindingVar();\r
std::map< int, Node > d_ground_eval;\r
+ //determine variable order\r
+ void determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars );\r
+ void collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars );\r
public:\r
//type of the match generator\r
enum {\r
typ_eq,\r
typ_formula,\r
typ_var,\r
- typ_top,\r
+ typ_ite_var,\r
+ typ_bool_var,\r
+ typ_tconstraint,\r
+ typ_tsym,\r
};\r
void debugPrintType( const char * c, short typ, bool isTrace = false );\r
public:\r
MatchGen() : d_type( typ_invalid ){}\r
- MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop = false, bool isVar = false );\r
+ MatchGen( QuantInfo * qi, Node n, bool isVar = false );\r
bool d_tgt;\r
+ bool d_tgt_orig;\r
+ bool d_wasSet;\r
Node d_n;\r
std::vector< MatchGen > d_children;\r
short d_type;\r
void reset_round( QuantConflictFind * p );\r
void reset( QuantConflictFind * p, bool tgt, QuantInfo * qi );\r
bool getNextMatch( QuantConflictFind * p, QuantInfo * qi );\r
+ bool getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vector< Node >& exp );\r
+ Node getExplanationTerm( QuantConflictFind * p, QuantInfo * qi, Node t, std::vector< Node >& exp );\r
bool isValid() { return d_type!=typ_invalid; }\r
void setInvalid();\r
+\r
+ // is this term treated as UF application?\r
+ static bool isHandledBoolConnective( TNode n );\r
+ static bool isHandledUfTerm( TNode n );\r
+ static Node getOperator( QuantConflictFind * p, Node n );\r
+ //can this node be handled by the algorithm\r
+ static bool isHandled( TNode n );\r
};\r
\r
//info for quantifiers\r
class QuantInfo {\r
+private:\r
+ void registerNode( Node n, bool hasPol, bool pol, bool beneathQuant = false );\r
+ void flatten( Node n, bool beneathQuant );\r
+private: //for completing match\r
+ std::vector< int > d_unassigned;\r
+ std::vector< TypeNode > d_unassigned_tn;\r
+ int d_unassigned_nvar;\r
+ int d_una_index;\r
+ std::vector< int > d_una_eqc_count;\r
public:\r
QuantInfo() : d_mg( NULL ) {}\r
+ ~QuantInfo() { delete d_mg; }\r
std::vector< TNode > d_vars;\r
std::map< TNode, int > d_var_num;\r
- //std::map< EqRegistry *, bool > d_rel_eqr;\r
+ std::vector< int > d_tsym_vars;\r
+ std::map< TNode, bool > d_inMatchConstraint;\r
std::map< int, std::vector< Node > > d_var_constraint[2];\r
int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }\r
bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); }\r
int getNumVars() { return (int)d_vars.size(); }\r
TNode getVar( int i ) { return d_vars[i]; }\r
+\r
MatchGen * d_mg;\r
Node d_q;\r
std::map< int, MatchGen * > d_var_mg;\r
void reset_round( QuantConflictFind * p );\r
public:\r
//initialize\r
- void initialize( Node q );\r
+ void initialize( Node q, Node qn );\r
//current constraints\r
std::vector< TNode > d_match;\r
std::vector< TNode > d_match_term;\r
std::map< int, std::map< TNode, int > > d_curr_var_deq;\r
+ std::map< Node, bool > d_tconstraints;\r
int getCurrentRepVar( int v );\r
TNode getCurrentValue( TNode n );\r
+ TNode getCurrentExpValue( TNode n );\r
bool getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq = false );\r
int addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity );\r
int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove );\r
bool setMatch( QuantConflictFind * p, int v, TNode n );\r
bool isMatchSpurious( QuantConflictFind * p );\r
- bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned );\r
+ bool isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms );\r
+ bool entailmentTest( QuantConflictFind * p, Node lit, bool chEnt = true );\r
+ bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false );\r
+ void revertMatch( std::vector< int >& assigned );\r
void debugPrintMatch( const char * c );\r
bool isConstrainedVar( int v );\r
+public:\r
+ void getMatch( std::vector< Node >& terms );\r
};\r
\r
class QuantConflictFind : public QuantifiersModule\r
{\r
- friend class QcfNodeIndex;\r
friend class MatchGen;\r
friend class QuantInfo;\r
typedef context::CDChunkList<Node> NodeList;\r
private:\r
context::Context* d_c;\r
context::CDO< bool > d_conflict;\r
- bool d_performCheck;\r
- //void registerAssertion( Node n );\r
- void registerNode( Node q, Node n, bool hasPol, bool pol );\r
- void flatten( Node q, Node n );\r
+ std::vector< Node > d_quant_order;\r
+ std::map< Kind, Node > d_zero;\r
+ //for storing nodes created during t-constraint solving (prevents memory leaks)\r
+ std::vector< Node > d_tempCache;\r
private:\r
std::map< Node, Node > d_op_node;\r
- Node getFunction( Node n, int& index, bool isQuant = false );\r
int d_fid_count;\r
std::map< Node, int > d_fid;\r
Node mkEqNode( Node a, Node b );\r
public: //for ground terms\r
Node d_true;\r
Node d_false;\r
+ TNode getZero( Kind k );\r
private:\r
Node evaluateTerm( Node n );\r
int evaluate( Node n, bool pref = false, bool hasPref = false );\r
NodeList d_qassert;\r
std::map< Node, QuantInfo > d_qinfo;\r
private: //for equivalence classes\r
- eq::EqualityEngine * getEqualityEngine();\r
- bool areDisequal( Node n1, Node n2 );\r
- bool areEqual( Node n1, Node n2 );\r
- Node getRepresentative( Node n );\r
-\r
-/*\r
- class EqcInfo {\r
- public:\r
- EqcInfo( context::Context* c ) : d_diseq( c ) {}\r
- NodeBoolMap d_diseq;\r
- bool isDisequal( Node n ) { return d_diseq.find( n )!=d_diseq.end() && d_diseq[n]; }\r
- void setDisequal( Node n, bool val = true ) { d_diseq[n] = val; }\r
- //NodeBoolMap& getRelEqr( int index ) { return index==0 ? d_rel_eqr_e : d_rel_eqr_d; }\r
- };\r
- std::map< Node, EqcInfo * > d_eqc_info;\r
- EqcInfo * getEqcInfo( Node n, bool doCreate = true );\r
-*/\r
- // operator -> index(terms)\r
- std::map< TNode, QcfNodeIndex > d_uf_terms;\r
- // operator -> index(eqc -> terms)\r
- std::map< TNode, QcfNodeIndex > d_eqc_uf_terms;\r
- //get qcf node index\r
- QcfNodeIndex * getQcfNodeIndex( Node eqc, Node f );\r
- QcfNodeIndex * getQcfNodeIndex( Node f );\r
// type -> list(eqc)\r
std::map< TypeNode, std::vector< TNode > > d_eqcs;\r
- //mapping from UF terms to representatives of their arguments\r
- std::map< TNode, std::vector< TNode > > d_arg_reps;\r
- //compute arg reps\r
- void computeArgReps( TNode n );\r
- // is this term treated as UF application?\r
- bool isHandledUfTerm( TNode n );\r
+ std::map< TypeNode, Node > d_model_basis;\r
public:\r
enum {\r
effort_conflict,\r
effort_prop_eq,\r
- effort_prop_deq,\r
+ effort_mc,\r
};\r
short d_effort;\r
- //for effort_prop\r
- TNode d_prop_eq[2];\r
- bool d_prop_pol;\r
- bool isPropagationSet();\r
+ void setEffort( int e ) { d_effort = e; }\r
+ static short getMaxQcfEffort();\r
bool areMatchEqual( TNode n1, TNode n2 );\r
bool areMatchDisequal( TNode n1, TNode n2 );\r
public:\r
QuantConflictFind( QuantifiersEngine * qe, context::Context* c );\r
-\r
- /** register assertions */\r
- //void registerAssertions( std::vector< Node >& assertions );\r
/** register quantifier */\r
void registerQuantifier( Node q );\r
-\r
public:\r
/** assert quantifier */\r
void assertNode( Node q );\r
void merge( Node a, Node b );\r
/** assert disequal */\r
void assertDisequal( Node a, Node b );\r
- /** check */\r
- void check( Theory::Effort level );\r
/** needs check */\r
bool needsCheck( Theory::Effort level );\r
+ /** reset round */\r
+ void reset_round( Theory::Effort level );\r
+ /** check */\r
+ void check( Theory::Effort level, unsigned quant_e );\r
private:\r
+ bool d_needs_computeRelEqr;\r
+public:\r
void computeRelevantEqr();\r
private:\r
void debugPrint( const char * c );\r
IntStat d_inst_rounds;\r
IntStat d_conflict_inst;\r
IntStat d_prop_inst;\r
+ IntStat d_entailment_checks;\r
Statistics();\r
~Statistics();\r
};\r
Statistics d_statistics;\r
+ /** Identify this module */\r
+ std::string identify() const { return "QcfEngine"; }\r
};\r
\r
}\r
projects / cvc5.git / blobdiff