summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/quantifiers/first_order_model.cpp10
-rw-r--r--src/theory/quantifiers/first_order_model.h4
-rw-r--r--src/theory/quantifiers/inst_strategy_e_matching.cpp124
-rwxr-xr-xsrc/theory/quantifiers/quant_conflict_find.cpp3
-rw-r--r--src/theory/quantifiers/relevant_domain.cpp94
-rw-r--r--src/theory/quantifiers/relevant_domain.h4
-rw-r--r--test/regress/regress0/bug512.minimized.smt21
-rw-r--r--test/regress/regress0/bug519.smt22
-rw-r--r--test/regress/regress0/decision/Makefile.am1
-rw-r--r--test/regress/regress0/quantifiers/Makefile.am2
-rw-r--r--test/regress/regress0/quantifiers/ex1.smt213
-rw-r--r--test/regress/regress0/quantifiers/ex1.smt2.expect2
-rw-r--r--test/regress/regress0/quantifiers/ex7.smt213
-rw-r--r--test/regress/regress0/quantifiers/ex7.smt2.expect2
14 files changed, 166 insertions, 109 deletions
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index a05abfa29..8c00c5af4 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -603,15 +603,19 @@ void FirstOrderModelFmc::processInitializeModelForTerm(Node n) {
bool FirstOrderModelFmc::isStar(Node n) {
- return n==getStar(n.getType());
+ //return n==getStar(n.getType());
+ return n.getAttribute(IsStarAttribute());
}
Node FirstOrderModelFmc::getStar(TypeNode tn) {
- if( d_type_star.find(tn)==d_type_star.end() ){
+ std::map<TypeNode, Node >::iterator it = d_type_star.find( tn );
+ if( it==d_type_star.end() ){
Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" );
d_type_star[tn] = st;
+ st.setAttribute(IsStarAttribute(), true );
+ return st;
}
- return d_type_star[tn];
+ return it->second;
}
Node FirstOrderModelFmc::getStarElement(TypeNode tn) {
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index ab3a1aa52..2ac9dadcf 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -19,6 +19,7 @@
#include "theory/theory_model.h"
#include "theory/uf/theory_uf_model.h"
+#include "expr/attribute.h"
namespace CVC4 {
namespace theory {
@@ -35,6 +36,9 @@ namespace fmcheck {
}
class FirstOrderModelQInt;
+struct IsStarAttributeId {};
+typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
+
class FirstOrderModel : public TheoryModel
{
protected:
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 25a62a4e8..5e2353e8a 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -359,65 +359,87 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
return STATUS_UNFINISHED;
}else{
//first, try from relevant domain
- Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl;
- bool success;
- ///* TODO: add back
RelevantDomain * rd = d_quantEngine->getRelevantDomain();
- if( rd ){
- rd->compute();
- unsigned final_max_i = 0;
- for(unsigned i=0; i<f[0].getNumChildren(); i++ ){
- unsigned ts = rd->getRDomain( f, i )->d_terms.size();
- if( ts>final_max_i ){
- final_max_i = ts;
+ for( unsigned r=0; r<2; r++ ){
+ if( rd || r==1 ){
+ if( r==0 ){
+ Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl;
+ }else{
+ Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
}
- }
+ rd->compute();
+ unsigned final_max_i = 0;
+ std::vector< unsigned > maxs;
+ for(unsigned i=0; i<f[0].getNumChildren(); i++ ){
+ unsigned ts;
+ if( r==0 ){
+ ts = rd->getRDomain( f, i )->d_terms.size();
+ }else{
+ ts = d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()].size();
+ }
+ maxs.push_back( ts );
+ Trace("inst-alg-rd") << "Variable " << i << " has " << ts << " in relevant domain." << std::endl;
+ if( ts>final_max_i ){
+ final_max_i = ts;
+ }
+ }
+ Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl;
- unsigned max_i = 0;
- while( max_i<=final_max_i ){
- std::vector< unsigned > childIndex;
- int index = 0;
- do {
- while( index>=0 && index<(int)f[0].getNumChildren() ){
- if( index==(int)childIndex.size() ){
- childIndex.push_back( -1 );
- }else{
- Assert( index==(int)(childIndex.size())-1 );
- unsigned nv = childIndex[index]+1;
- if( nv<rd->getRDomain( f, index )->d_terms.size() && nv<max_i ){
- childIndex[index]++;
- index++;
+ unsigned max_i = 0;
+ bool success;
+ while( max_i<=final_max_i ){
+ Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl;
+ std::vector< unsigned > childIndex;
+ int index = 0;
+ do {
+ while( index>=0 && index<(int)f[0].getNumChildren() ){
+ if( index==(int)childIndex.size() ){
+ childIndex.push_back( -1 );
}else{
- childIndex.pop_back();
- index--;
+ Assert( index==(int)(childIndex.size())-1 );
+ unsigned nv = childIndex[index]+1;
+ if( nv<maxs[index] && nv<=max_i ){
+ childIndex[index]++;
+ index++;
+ }else{
+ childIndex.pop_back();
+ index--;
+ }
}
}
- }
- success = index>=0;
- if( success ){
- index--;
- //try instantiation
- std::vector< Node > terms;
- for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
- terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
- }
- if( d_quantEngine->addInstantiation( f, terms, false ) ){
- ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
- return STATUS_UNKNOWN;
+ success = index>=0;
+ if( success ){
+ Trace("inst-alg-rd") << "Try instantiation..." << std::endl;
+ index--;
+ //try instantiation
+ std::vector< Node > terms;
+ for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+ if( r==0 ){
+ terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
+ }else{
+ terms.push_back( d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()][childIndex[i]] );
+ }
+ }
+ if( d_quantEngine->addInstantiation( f, terms, false ) ){
+ Trace("inst-alg-rd") << "Success!" << std::endl;
+ ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
+ return STATUS_UNKNOWN;
+ }
}
- }
- }while( success );
- max_i++;
+ }while( success );
+ max_i++;
+ }
}
- }
- //*/
-
- if( d_guessed.find( f )==d_guessed.end() ){
- Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
- d_guessed[f] = true;
- InstMatch m( f );
- if( d_quantEngine->addInstantiation( f, m ) ){
- ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
+ if( r==0 ){
+ if( d_guessed.find( f )==d_guessed.end() ){
+ Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
+ d_guessed[f] = true;
+ InstMatch m( f );
+ if( d_quantEngine->addInstantiation( f, m ) ){
+ ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
+ return STATUS_UNKNOWN;
+ }
+ }
}
}
return STATUS_UNKNOWN;
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 4a5c92c7e..08bd0f179 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -116,6 +116,7 @@ void QuantInfo::initialize( Node q, Node qn ) {
}
*/
}
+ Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;
}
void QuantInfo::registerNode( Node n, bool hasPol, bool pol ) {
@@ -700,7 +701,7 @@ void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbva
void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars ) {
Trace("qcf-qregister-debug") << "Determine variable order " << d_n << std::endl;
- bool isCom = d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF;
+ bool isCom = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF );
std::map< int, std::vector< int > > c_to_vars;
std::map< int, std::vector< int > > vars_to_c;
std::map< int, int > vb_count;
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 9166b81e8..0452278f2 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -34,9 +34,15 @@ void RelevantDomain::RDomain::merge( RDomain * r ) {
d_terms.clear();
}
-void RelevantDomain::RDomain::addTerm( Node t ) {
- if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){
- d_terms.push_back( t );
+void RelevantDomain::RDomain::addTerm( Node t, bool nonGround ) {
+ if( !nonGround ){
+ if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){
+ d_terms.push_back( t );
+ }
+ }else{
+ if( std::find( d_ng_terms.begin(), d_ng_terms.end(), t )==d_ng_terms.end() ){
+ d_ng_terms.push_back( t );
+ }
}
}
@@ -138,33 +144,83 @@ void RelevantDomain::compute(){
}
void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) {
-
+ Node op = d_qe->getTermDatabase()->getOperator( n );
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- Node op = d_qe->getTermDatabase()->getOperator( n );
if( !op.isNull() ){
RDomain * rf = getRDomain( op, i );
+ if( n[i].getKind()==ITE ){
+ for( unsigned j=1; j<=2; j++ ){
+ computeRelevantDomainOpCh( rf, n[i][j] );
+ }
+ }else{
+ computeRelevantDomainOpCh( rf, n[i] );
+ }
+ }
+ //TODO
+ if( n[i].getKind()!=FORALL ){
+ bool newHasPol;
+ bool newPol;
+ QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
+ computeRelevantDomain( n[i], newHasPol, newPol );
+ }
+ }
+
+ if( n.getKind()==EQUAL || n.getKind()==GEQ ){
+ int varCount = 0;
+ std::vector< RDomain * > rds;
+ int varCh = -1;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
if( n[i].getKind()==INST_CONSTANT ){
Node q = d_qe->getTermDatabase()->getInstConstAttr( n[i] );
- //merge the RDomains
unsigned id = n[i].getAttribute(InstVarNumAttribute());
- Trace("rel-dom-debug") << n[i] << " is variable # " << id << " for " << q;
- Trace("rel-dom-debug") << " with body : " << d_qe->getTermDatabase()->getInstConstantBody( q ) << std::endl;
- RDomain * rq = getRDomain( q, id );
- if( rf!=rq ){
- rq->merge( rf );
+ rds.push_back( getRDomain( q, id ) );
+ varCount++;
+ varCh = i;
+ }else{
+ rds.push_back( NULL );
+ }
+ }
+ if( varCount==2 ){
+ //merge the two relevant domains
+ if( ( !hasPol || pol ) && rds[0]!=rds[1] ){
+ rds[0]->merge( rds[1] );
+ }
+ }else if( varCount==1 ){
+ int oCh = varCh==0 ? 1 : 0;
+ bool ng = d_qe->getTermDatabase()->hasInstConstAttr( n[oCh] );
+ //the negative occurrence adds the term to the domain
+ if( !hasPol || !pol ){
+ rds[varCh]->addTerm( n[oCh] );
+ }
+ //the positive occurence adds other terms
+ if( ( !hasPol || pol ) && n[0].getType().isInteger() ){
+ if( n.getKind()==EQUAL ){
+ for( unsigned i=0; i<2; i++ ){
+ rds[varCh]->addTerm( QuantArith::offset( n[oCh], i==0 ? 1 : -1 ), ng );
+ }
+ }else if( n.getKind()==GEQ ){
+ Node nt = QuantArith::offset( n[oCh], varCh==0 ? 1 : -1 );
+ rds[varCh]->addTerm( QuantArith::offset( n[oCh], varCh==0 ? 1 : -1 ), ng );
}
- }else if( !d_qe->getTermDatabase()->hasInstConstAttr( n[i] ) ){
- //term to add
- rf->addTerm( n[i] );
}
}
+ }
+}
- //TODO
- if( n[i].getKind()!=FORALL ){
- bool newHasPol = hasPol;
- bool newPol = pol;
- computeRelevantDomain( n[i], newHasPol, newPol );
+void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) {
+ if( n.getKind()==INST_CONSTANT ){
+ Node q = d_qe->getTermDatabase()->getInstConstAttr( n );
+ //merge the RDomains
+ unsigned id = n.getAttribute(InstVarNumAttribute());
+ Trace("rel-dom-debug") << n << " is variable # " << id << " for " << q;
+ Trace("rel-dom-debug") << " with body : " << d_qe->getTermDatabase()->getInstConstantBody( q ) << std::endl;
+ RDomain * rq = getRDomain( q, id );
+ if( rf!=rq ){
+ rq->merge( rf );
}
+ }else if( !d_qe->getTermDatabase()->hasInstConstAttr( n ) ){
+ //term to add
+ rf->addTerm( n );
}
}
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index 0f5afcadd..200e49a72 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -33,8 +33,9 @@ private:
void reset() { d_parent = NULL; d_terms.clear(); }
RDomain * d_parent;
std::vector< Node > d_terms;
+ std::vector< Node > d_ng_terms;
void merge( RDomain * r );
- void addTerm( Node t );
+ void addTerm( Node t, bool nonGround = false );
RDomain * getParent();
void removeRedundantTerms( FirstOrderModel * fm );
bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); }
@@ -45,6 +46,7 @@ private:
QuantifiersEngine* d_qe;
FirstOrderModel* d_model;
void computeRelevantDomain( Node n, bool hasPol, bool pol );
+ void computeRelevantDomainOpCh( RDomain * rf, Node n );
bool d_is_computed;
public:
RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m );
diff --git a/test/regress/regress0/bug512.minimized.smt2 b/test/regress/regress0/bug512.minimized.smt2
index 0b19f26df..1a2aaf56f 100644
--- a/test/regress/regress0/bug512.minimized.smt2
+++ b/test/regress/regress0/bug512.minimized.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --tlimit-per 1000
; EXPECT: unknown
(set-logic UF)
(declare-sort T 0)
diff --git a/test/regress/regress0/bug519.smt2 b/test/regress/regress0/bug519.smt2
index 22fdff674..406cb0c1b 100644
--- a/test/regress/regress0/bug519.smt2
+++ b/test/regress/regress0/bug519.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -mi
+; COMMAND-LINE: -mi --tlimit-per 1000
; EXPECT: unknown
; EXPECT: unsat
diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am
index 366204191..90a18f0e2 100644
--- a/test/regress/regress0/decision/Makefile.am
+++ b/test/regress/regress0/decision/Makefile.am
@@ -25,7 +25,6 @@ TESTS = \
bitvec5.smt \
quant-Arrays_Q1-noinfer.smt2 \
quant-ex1.smt2 \
- quant-ex1.disable_miniscope.smt2 \
uflia-xs-09-16-3-4-1-5.delta03.smt \
aufbv-fuzz01.smt \
bug347.smt \
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 93d513d9f..c478248da 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -28,10 +28,8 @@ TESTS = \
bug269.smt2 \
burns13.smt2 \
burns4.smt2 \
- ex1.smt2 \
ex3.smt2 \
ex6.smt2 \
- ex7.smt2 \
opisavailable-12.smt2 \
ricart-agrawala6.smt2 \
set8.smt2 \
diff --git a/test/regress/regress0/quantifiers/ex1.smt2 b/test/regress/regress0/quantifiers/ex1.smt2
deleted file mode 100644
index 20230a6fa..000000000
--- a/test/regress/regress0/quantifiers/ex1.smt2
+++ /dev/null
@@ -1,13 +0,0 @@
-(set-logic AUFLIRA)
-(set-info :smt-lib-version 2.0)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-sort U 0)
-(declare-fun a () U)
-(declare-fun b () U)
-(declare-fun f (U) U)
-(declare-fun p () Bool)
-(assert (and (= a b) (forall ((x U)) (=> (and (= (f x) a) (not (= (f x) b))) p))))
-(check-sat)
-(get-info :reason-unknown)
-(exit)
diff --git a/test/regress/regress0/quantifiers/ex1.smt2.expect b/test/regress/regress0/quantifiers/ex1.smt2.expect
deleted file mode 100644
index 2bd8349de..000000000
--- a/test/regress/regress0/quantifiers/ex1.smt2.expect
+++ /dev/null
@@ -1,2 +0,0 @@
-% EXPECT: unknown
-% EXPECT: (:reason-unknown incomplete)
diff --git a/test/regress/regress0/quantifiers/ex7.smt2 b/test/regress/regress0/quantifiers/ex7.smt2
deleted file mode 100644
index 11a83fdc4..000000000
--- a/test/regress/regress0/quantifiers/ex7.smt2
+++ /dev/null
@@ -1,13 +0,0 @@
-(set-logic AUFLIRA)
-(set-info :smt-lib-version 2.0)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-sort U 0)
-(declare-fun a () U)
-(declare-fun b () U)
-(declare-fun c () U)
-(declare-fun f (U) U)
-(assert (and (= a b) (forall ((x U)) (=> (or (= (f x) c) (= x a)) (= x b)))))
-(check-sat)
-(get-info :reason-unknown)
-(exit)
diff --git a/test/regress/regress0/quantifiers/ex7.smt2.expect b/test/regress/regress0/quantifiers/ex7.smt2.expect
deleted file mode 100644
index 2bd8349de..000000000
--- a/test/regress/regress0/quantifiers/ex7.smt2.expect
+++ /dev/null
@@ -1,2 +0,0 @@
-% EXPECT: unknown
-% EXPECT: (:reason-unknown incomplete)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback