summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/options_handler.cpp8
-rw-r--r--src/theory/quantifiers/quant_conflict_find.cpp150
-rw-r--r--src/theory/quantifiers/quant_conflict_find.h5
-rw-r--r--src/theory/quantifiers/term_database.h2
4 files changed, 15 insertions, 150 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 8f179531b..6f9d31024 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -331,12 +331,6 @@ prop-eq \n\
conflict \n\
+ Apply QCF algorithm to find conflicts only.\n\
\n\
-partial \n\
-+ Apply QCF algorithm to instantiate heuristically as well. \n\
-\n\
-mc \n\
-+ Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\
-\n\
";
const std::string OptionsHandler::s_userPatModeHelp = "\
@@ -716,8 +710,6 @@ theory::quantifiers::QcfMode OptionsHandler::stringToQcfMode(std::string option,
return theory::quantifiers::QCF_CONFLICT_ONLY;
} else if(optarg == "default" || optarg == "prop-eq") {
return theory::quantifiers::QCF_PROP_EQ;
- } else if(optarg == "partial") {
- return theory::quantifiers::QCF_PARTIAL;
} else if(optarg == "help") {
puts(s_qcfModeHelp.c_str());
exit(1);
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index f7521ff4a..3b2a650ab 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -253,28 +253,6 @@ bool QuantInfo::reset_round( QuantConflictFind * p ) {
d_curr_var_deq.clear();
d_tconstraints.clear();
- //add built-in variable constraints
- for( unsigned r=0; r<2; r++ ){
- for( std::map< int, std::vector< Node > >::iterator it = d_var_constraint[r].begin();
- it != d_var_constraint[r].end(); ++it ){
- for( unsigned j=0; j<it->second.size(); j++ ){
- Node rr = it->second[j];
- if( !isVar( rr ) ){
- rr = p->getRepresentative( rr );
- }
- if( addConstraint( p, it->first, rr, r==0 )==-1 ){
- d_var_constraint[0].clear();
- d_var_constraint[1].clear();
- //quantified formula is actually equivalent to true
- Trace("qcf-qregister") << "Quantifier is equivalent to true!!!" << std::endl;
- d_mg->d_children.clear();
- d_mg->d_n = NodeManager::currentNM()->mkConst( true );
- d_mg->d_type = MatchGen::typ_ground;
- return false;
- }
- }
- }
- }
d_mg->reset_round( p );
for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){
it->second->reset_round( p );
@@ -664,24 +642,6 @@ bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) {
}else{
return chEnt;
}
-/*
- if( chEnt ){
- //check if it is entailed
- Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl;
- std::pair<bool, Node> et = p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, rew );
- ++(p->d_statistics.d_entailment_checks);
- Trace("qcf-tconstraint-debug") << "ET result : " << et.first << " " << et.second << std::endl;
- if( !et.first ){
- Trace("qcf-tconstraint-debug") << "...cannot show entailment of " << rew << "." << std::endl;
- return false;
- }else{
- return true;
- }
- }else{
- Trace("qcf-tconstraint-debug") << "...does not need to be entailed." << std::endl;
- return true;
- }
-*/
}else{
Trace("qcf-tconstraint-debug") << "...rewrites to true." << std::endl;
return true;
@@ -1287,12 +1247,15 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
TNode f = getMatchOperator( p, d_n );
Debug("qcf-match-debug") << " reset: Var will match operators of " << f << std::endl;
TermArgTrie * qni = p->getTermDatabase()->getTermArgTrie( Node::null(), f );
- if( qni!=NULL ){
- d_qn.push_back( qni );
- }else{
+ if (qni == nullptr || qni->empty())
+ {
//inform irrelevant quantifiers
p->setIrrelevantFunction( f );
}
+ else
+ {
+ d_qn.push_back(qni);
+ }
d_matched_basis = false;
}else if( d_type==typ_tsym || d_type==typ_tconstraint ){
for( std::map< int, int >::iterator it = d_qni_var_num.begin(); it != d_qni_var_num.end(); ++it ){
@@ -1526,7 +1489,9 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
Debug("qcf-match") << " ...finished matching for " << d_n << ", success = " << success << std::endl;
d_wasSet = success;
return success;
- }else if( d_type==typ_formula || d_type==typ_ite_var ){
+ }
+ else if (d_type == typ_formula)
+ {
bool success = false;
if( d_child_counter<0 ){
if( d_child_counter<-1 ){
@@ -1597,7 +1562,8 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
d_child_counter++;
getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2) )->reset( p, d_tgt, qi );
}else{
- if( d_child_counter==4 || ( d_type==typ_ite_var && d_child_counter==2 ) ){
+ if (d_child_counter == 4)
+ {
d_child_counter = -1;
}else{
d_child_counter +=2;
@@ -1630,84 +1596,6 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
return false;
}
-bool MatchGen::getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vector< Node >& exp ) {
- if( d_type==typ_eq ){
- Node n[2];
- for( unsigned i=0; i<2; i++ ){
- Trace("qcf-explain") << "Explain term " << d_n[i] << "..." << std::endl;
- n[i] = getExplanationTerm( p, qi, d_n[i], exp );
- }
- Node eq = n[0].eqNode( n[1] );
- if( !d_tgt_orig ){
- eq = eq.negate();
- }
- exp.push_back( eq );
- Trace("qcf-explain") << "Explanation for " << d_n << " (tgt=" << d_tgt_orig << ") is " << eq << ", set = " << d_wasSet << std::endl;
- return true;
- }else if( d_type==typ_pred ){
- Trace("qcf-explain") << "Explain term " << d_n << "..." << std::endl;
- Node n = getExplanationTerm( p, qi, d_n, exp );
- if( !d_tgt_orig ){
- n = n.negate();
- }
- exp.push_back( n );
- Trace("qcf-explain") << "Explanation for " << d_n << " (tgt=" << d_tgt_orig << ") is " << n << ", set = " << d_wasSet << std::endl;
- return true;
- }else if( d_type==typ_formula ){
- Trace("qcf-explain") << "Explanation get for " << d_n << ", counter = " << d_child_counter << ", tgt = " << d_tgt_orig << ", set = " << d_wasSet << std::endl;
- if( d_n.getKind()==OR || d_n.getKind()==AND ){
- if( (d_n.getKind()==AND)==d_tgt ){
- for( unsigned i=0; i<getNumChildren(); i++ ){
- if( !getChild( i )->getExplanation( p, qi, exp ) ){
- return false;
- }
- }
- }else{
- return getChild( d_child_counter )->getExplanation( p, qi, exp );
- }
- }else if( d_n.getKind()==EQUAL ){
- for( unsigned i=0; i<2; i++ ){
- if( !getChild( i )->getExplanation( p, qi, exp ) ){
- return false;
- }
- }
- }else if( d_n.getKind()==ITE ){
- for( unsigned i=0; i<3; i++ ){
- bool isActive = ( ( i==0 && d_child_counter!=5 ) ||
- ( i==1 && d_child_counter!=( d_tgt ? 3 : 1 ) ) ||
- ( i==2 && d_child_counter!=( d_tgt ? 1 : 3 ) ) );
- if( isActive ){
- if( !getChild( i )->getExplanation( p, qi, exp ) ){
- return false;
- }
- }
- }
- }else{
- return false;
- }
- return true;
- }else{
- return false;
- }
-}
-
-Node MatchGen::getExplanationTerm( QuantConflictFind * p, QuantInfo * qi, Node t, std::vector< Node >& exp ) {
- Node v = qi->getCurrentExpValue( t );
- if( isHandledUfTerm( t ) ){
- for( unsigned i=0; i<t.getNumChildren(); i++ ){
- Node vi = getExplanationTerm( p, qi, t[i], exp );
- if( vi!=v[i] ){
- Node eq = vi.eqNode( v[i] );
- if( std::find( exp.begin(), exp.end(), eq )==exp.end() ){
- Trace("qcf-explain") << " add : " << eq << "." << std::endl;
- exp.push_back( eq );
- }
- }
- }
- }
- return v;
-}
-
bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
if( !d_qn.empty() ){
if( d_qn[0]==NULL ){
@@ -1843,7 +1731,6 @@ void MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) {
case typ_pred: Trace(c) << "pred";break;
case typ_formula: Trace(c) << "formula";break;
case typ_var: Trace(c) << "var";break;
- case typ_ite_var: Trace(c) << "ite_var";break;
case typ_bool_var: Trace(c) << "bool_var";break;
}
}else{
@@ -1854,7 +1741,6 @@ void MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) {
case typ_pred: Debug(c) << "pred";break;
case typ_formula: Debug(c) << "formula";break;
case typ_var: Debug(c) << "var";break;
- case typ_ite_var: Debug(c) << "ite_var";break;
case typ_bool_var: Debug(c) << "bool_var";break;
}
}
@@ -1907,10 +1793,6 @@ QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe, context::Context* c)
d_effort(EFFORT_INVALID),
d_needs_computeRelEqr() {}
-Node QuantConflictFind::mkEqNode( Node a, Node b ) {
- return a.eqNode( b );
-}
-
//-------------------------------------------------- registration
void QuantConflictFind::registerQuantifier( Node q ) {
@@ -2031,14 +1913,8 @@ inline QuantConflictFind::Effort QcfEffortStart() {
// Returns the beginning of a range of efforts. The value returned is included
// in the range.
inline QuantConflictFind::Effort QcfEffortEnd() {
- switch (options::qcfMode()) {
- case QCF_PROP_EQ:
- case QCF_PARTIAL:
- return QuantConflictFind::EFFORT_PROP_EQ;
- case QCF_CONFLICT_ONLY:
- default:
- return QuantConflictFind::EFFORT_PROP_EQ;
- }
+ return options::qcfMode() == QCF_PROP_EQ ? QuantConflictFind::EFFORT_PROP_EQ
+ : QuantConflictFind::EFFORT_CONFLICT;
}
} // namespace
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 507d929a7..e4eefe9ad 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -75,7 +75,6 @@ public:
typ_eq,
typ_formula,
typ_var,
- typ_ite_var,
typ_bool_var,
typ_tconstraint,
typ_tsym,
@@ -94,8 +93,6 @@ public:
void reset_round( QuantConflictFind * p );
void reset( QuantConflictFind * p, bool tgt, QuantInfo * qi );
bool getNextMatch( QuantConflictFind * p, QuantInfo * qi );
- bool getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vector< Node >& exp );
- Node getExplanationTerm( QuantConflictFind * p, QuantInfo * qi, Node t, std::vector< Node >& exp );
bool isValid() { return d_type!=typ_invalid; }
void setInvalid();
@@ -138,7 +135,6 @@ public:
std::map< TNode, int > d_var_num;
std::vector< int > d_tsym_vars;
std::map< TNode, bool > d_inMatchConstraint;
- std::map< int, std::vector< Node > > d_var_constraint[2];
int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }
bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); }
int getNumVars() { return (int)d_vars.size(); }
@@ -205,7 +201,6 @@ private:
private:
std::map< Node, Node > d_op_node;
std::map< Node, int > d_fid;
- Node mkEqNode( Node a, Node b );
public: //for ground terms
Node d_true;
Node d_false;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index e9dd371df..7e3806e8c 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -96,6 +96,8 @@ public:
void debugPrint(const char* c, Node n, unsigned depth = 0);
/** clear all data from this trie */
void clear() { d_data.clear(); }
+ /** is empty */
+ bool empty() { return d_data.empty(); }
};/* class TermArgTrie */
namespace fmcheck {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback