diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-27 19:21:18 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-27 19:21:18 -0500 |
commit | 1fe3247a0bf4b806f99c161dcc9c6644aabb38c1 (patch) | |
tree | 0922af2e81c62268ea4747e085dc2b57441f5edf /src/theory/quantifiers/quant_util.cpp | |
parent | 36bf9f8bcb2a1a3aea1f90eb4d13aed3bbf6da8f (diff) |
Document quant arith (#1271)
* Initial documentation, incomplete.
* Document arith utilities in quantifiers.
* Minor
* Clang format
* Minor
* Clang format.
* Minor
* Apply new clang format.
* Document ordering.
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 30 |
1 files changed, 27 insertions, 3 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 1e30914ef..88fdec6f3 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -149,9 +149,6 @@ Node QuantArith::mkCoeffTerm( Node coeff, Node t ) { } } -// given (msum <k> 0), solve (veq_c * v <k> val) or (val <k> veq_c * v), where: -// veq_c is either null (meaning 1), or positive. -// return value 1: veq_c*v is RHS, -1: veq_c*v is LHS, 0: failed. int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ) { std::map< Node, Node >::iterator itv = msum.find( v ); if( itv!=msum.end() ){ @@ -229,6 +226,9 @@ Node QuantArith::solveEqualityFor( Node lit, Node v ) { Node val, veqc; if( QuantArith::isolate( v, msum, veqc, val, EQUAL )!=0 ){ if( veqc.isNull() ){ + // in this case, we have an integer equality with a coefficient + // on the variable we solved for that could not be eliminated, + // hence we fail. return val; } } @@ -238,6 +238,30 @@ Node QuantArith::solveEqualityFor( Node lit, Node v ) { return Node::null(); } +bool QuantArith::decompose(Node n, Node v, Node& coeff, Node& rem) +{ + std::map<Node, Node> msum; + if (getMonomialSum(n, msum)) + { + std::map<Node, Node>::iterator it = msum.find(v); + if (it == msum.end()) + { + return false; + } + else + { + coeff = it->second; + msum.erase(v); + rem = mkNode(msum); + return true; + } + } + else + { + return false; + } +} + Node QuantArith::negate( Node t ) { Node tt = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) ), t ); tt = Rewriter::rewrite( tt ); |