diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-02 17:42:31 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-02 17:42:31 +0100 |
commit | 8deb9d980d7b0e281a0190539b756896a487c451 (patch) | |
tree | ce0bfe29b53cc16c8854fa6833f2dda3b9122c6f /src/theory/quantifiers/quant_util.cpp | |
parent | 6d37c136a251b957197269aeb389a9f1ae07e620 (diff) |
Single invocation module for counterexample guided quantifier instantiation --cegqi-si. Minor improvements to syntax-guided case, refactoring. Do not apply exhaustive tester inference for sygus datatypes.
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index f73bc7bb2..2dd800592 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -92,7 +92,7 @@ bool QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind if( r.isOne() ){ veq = negate(veq); }else{ - //TODO + //TODO : lcd computation return false; } } @@ -118,6 +118,23 @@ Node QuantArith::offset( Node t, int i ) { return tt; } +void QuantArith::debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c ) { + for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + Trace(c) << " "; + if( !it->second.isNull() ){ + Trace(c) << it->second; + if( !it->first.isNull() ){ + Trace(c) << " * "; + } + } + if( !it->first.isNull() ){ + Trace(c) << it->first; + } + Trace(c) << std::endl; + } + Trace(c) << std::endl; +} + void QuantRelevance::registerQuantifier( Node f ){ //compute symbols in f |