diff options
author | Tim King <taking@cs.nyu.edu> | 2011-11-29 21:11:45 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-11-29 21:11:45 +0000 |
commit | e9198d9b99c6037165362870436b45826674303f (patch) | |
tree | b5e8d01a53d38d353dae7c16351ff9206e1f96c6 /src/prop | |
parent | 8b202bab8442c927e9ac18a35c71a82444acf63b (diff) |
Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic now supports propagating equalities when a slack variable corresponding to a difference of shared terms must be 0. Similarly disequalities are propagated when these variables cannot be zero.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/prop_engine.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 8663a2f68..9b0b93f78 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -173,6 +173,8 @@ Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) { Node PropEngine::getValue(TNode node) const { Assert(node.getType().isBoolean()); + Assert(d_cnfStream->hasLiteral(node)); + SatLiteral lit = d_cnfStream->getLiteral(node); SatLiteralValue v = d_satSolver->value(lit); @@ -196,6 +198,8 @@ bool PropEngine::isTranslatedSatLiteral(TNode node) const { bool PropEngine::hasValue(TNode node, bool& value) const { Assert(node.getType().isBoolean()); + Assert(d_cnfStream->hasLiteral(node)); + SatLiteral lit = d_cnfStream->getLiteral(node); SatLiteralValue v = d_satSolver->value(lit); |