diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-03 15:09:12 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-03 15:09:26 -0500 |
commit | b6d5d0b11cf7624cd7a3e0a2f6f77d83d2f7001a (patch) | |
tree | b0e5acbce9023c28bf1bb85eee5da97b79c94561 /src/theory/quantifiers | |
parent | 8a8455d955c084c9a9f7add1f4e4da6b1dbc35eb (diff) |
Add priorities to getNextDecision. Properly handle case for finite types + unbounded heaps in sep logic. Fix another simple memory leak in sygus.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/bounded_integers.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/bounded_integers.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_util.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.h | 2 |
9 files changed, 20 insertions, 10 deletions
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 54853ceaf..dc0019383 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -417,7 +417,7 @@ void BoundedIntegers::assertNode( Node n ) { d_assertions[nlit] = n.getKind()!=NOT; } -Node BoundedIntegers::getNextDecisionRequest() { +Node BoundedIntegers::getNextDecisionRequest( unsigned& priority ) { Trace("bound-int-dec-debug") << "bi: Get next decision request?" << std::endl; for( unsigned i=0; i<d_ranges.size(); i++) { Node d = d_rms[d_ranges[i]]->getNextDecisionRequest(); @@ -435,6 +435,7 @@ Node BoundedIntegers::getNextDecisionRequest() { i--; } }else{ + priority = 1; Trace("bound-int-dec") << "Bounded Integers : Decide " << d << std::endl; return d; } diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index c3fb05641..0dfd7eafd 100644 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h @@ -146,7 +146,7 @@ public: void check( Theory::Effort e, unsigned quant_e ); void registerQuantifier( Node f ); void assertNode( Node n ); - Node getNextDecisionRequest(); + Node getNextDecisionRequest( unsigned& priority ); bool isBoundVar( Node q, Node v ) { return std::find( d_set[q].begin(), d_set[q].end(), v )!=d_set[q].end(); } unsigned getBoundVarType( Node q, Node v ); unsigned getNumBoundVars( Node q ) { return d_set[q].size(); } diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 54415d974..ecf4bb74d 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -229,6 +229,10 @@ CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c d_last_inst_si = false; } +CegInstantiation::~CegInstantiation(){ + delete d_conj; +} + bool CegInstantiation::needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } @@ -345,7 +349,7 @@ void CegInstantiation::registerQuantifier( Node q ) { void CegInstantiation::assertNode( Node n ) { } -Node CegInstantiation::getNextDecisionRequest() { +Node CegInstantiation::getNextDecisionRequest( unsigned& priority ) { //enforce fairness if( d_conj->isAssigned() ){ d_conj->initializeGuard( d_quantEngine ); @@ -363,6 +367,7 @@ Node CegInstantiation::getNextDecisionRequest() { bool value; if( !d_quantEngine->getValuation().hasSatValue( req_dec[i], value ) ) { Trace("cegqi-debug") << "CEGQI : Decide next on : " << req_dec[i] << "..." << std::endl; + priority = 0; return req_dec[i]; }else{ Trace("cegqi-debug2") << "CEGQI : " << req_dec[i] << " already has value " << value << std::endl; @@ -377,10 +382,12 @@ Node CegInstantiation::getNextDecisionRequest() { d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 ); lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl; + priority = 1; return lit; } }else{ Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl; + priority = 1; return lit; } } diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index c8b41c035..7f36f4d25 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -154,6 +154,7 @@ private: Node getModelTerm( Node n ); public: CegInstantiation( QuantifiersEngine * qe, context::Context* c ); + ~CegInstantiation(); public: bool needsCheck( Theory::Effort e ); unsigned needsModel( Theory::Effort e ); @@ -163,7 +164,7 @@ public: void preRegisterQuantifier( Node q ); void registerQuantifier( Node q ); void assertNode( Node n ); - Node getNextDecisionRequest(); + Node getNextDecisionRequest( unsigned& priority ); /** Identify this module (for debugging, dynamic configuration, etc..) */ std::string identify() const { return "CegInstantiation"; } /** print solution for synthesis conjectures */ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index ac6e1edbe..895a0c93c 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -592,12 +592,13 @@ Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool return Node::null(); } -Node InstStrategyCbqi::getNextDecisionRequest(){ +Node InstStrategyCbqi::getNextDecisionRequest( unsigned& priority ){ std::map< Node, bool > proc; for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); Node d = getNextDecisionRequestProc( q, proc ); if( !d.isNull() ){ + priority = 0; return d; } } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index c9f62243f..2cd5f6e1c 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -107,7 +107,7 @@ public: void preRegisterQuantifier( Node q ); void registerQuantifier( Node q ); /** get next decision request */ - Node getNextDecisionRequest(); + Node getNextDecisionRequest( unsigned& priority ); }; //generalized counterexample guided quantifier instantiation diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 3ff21aa6e..b4264135c 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -61,7 +61,7 @@ public: virtual void registerQuantifier( Node q ) = 0; virtual void assertNode( Node n ) {} virtual void propagate( Theory::Effort level ){} - virtual Node getNextDecisionRequest() { return TNode::null(); } + virtual Node getNextDecisionRequest( unsigned& priority ) { return TNode::null(); } /** Identify this module (for debugging, dynamic configuration, etc..) */ virtual std::string identify() const = 0; public: diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index e97a76ce6..0b4f3c0c7 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -179,8 +179,8 @@ void TheoryQuantifiers::check(Effort e) { getQuantifiersEngine()->check( e ); } -Node TheoryQuantifiers::getNextDecisionRequest(){ - return getQuantifiersEngine()->getNextDecisionRequest(); +Node TheoryQuantifiers::getNextDecisionRequest( unsigned& priority ){ + return getQuantifiersEngine()->getNextDecisionRequest( priority ); } void TheoryQuantifiers::assertUniversal( Node n ){ diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index ba5a75d86..308514b92 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -63,7 +63,7 @@ public: void presolve(); void ppNotifyAssertions( std::vector< Node >& assertions ); void check(Effort e); - Node getNextDecisionRequest(); + Node getNextDecisionRequest( unsigned& priority ); Node getValue(TNode n); void collectModelInfo( TheoryModel* m, bool fullModel ); void shutdown() { } |