diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-06 09:35:49 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-06 09:35:59 +0100 |
| commit | 363e4c378f0bc9598a93c80bce9ecaebca2efdd1 (patch) | |
| tree | e40a637326719738866bfbb790aa704a3522a2c1 /src/theory/quantifiers/quant_util.cpp | |
| parent | fca6fd532abda44c4da48d5c167b77600690e221 (diff) | |
Handle missing cases for single inv solution reconstruction. Minor fixes. Refactor.
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
| -rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 8d24c2cef..ccc4cfd15 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -23,7 +23,15 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; - +bool QuantArith::getMonomial( Node n, Node& c, Node& v ){ + if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){ + c = n[0]; + v = n[1]; + return true; + }else{ + return false; + } +} bool QuantArith::getMonomial( Node n, std::map< Node, Node >& msum ) { if ( n.getKind()==MULT ){ if( n.getNumChildren()==2 && msum.find(n[1])==msum.end() && n[0].isConst() ){ |