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/ce_guided_instantiation.cpp | |
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/ce_guided_instantiation.cpp')
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 9 |
1 files changed, 8 insertions, 1 deletions
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; } } |