diff options
author | Tim King <taking@cs.nyu.edu> | 2010-02-04 21:03:07 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-02-04 21:03:07 +0000 |
commit | a34b66437f97f66d9dcd1caa0919f66cf316e238 (patch) | |
tree | 3c3b8fc01cbc6ac4e97a45de16218d120ca3cca8 /src/prop/cnf_stream.h | |
parent | c6f86de8077f667ab2b2e9aac53d60d93ea2da93 (diff) |
Changed mapping from atoms to literals in the prop engine to be atoms to vars.
Diffstat (limited to 'src/prop/cnf_stream.h')
-rw-r--r-- | src/prop/cnf_stream.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 9be5efcd3..ca2e6dedd 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -61,6 +61,8 @@ private: std::map<Node, minisat::Lit> d_translationCache; protected: + bool isAtomMapped(const Node & n) const; + minisat::Var lookupAtom(const Node & n) const; /** * Uniform interface for sending a clause back to d_propEngine. @@ -83,8 +85,7 @@ protected: //negotiates the mapping of atoms to literals with PropEngine - void registerMapping(const Node & node, minisat::Lit lit, bool atom = false); - minisat::Lit acquireFreshLit(const Node & n); + void cacheTranslation(const Node & node, minisat::Lit lit); minisat::Lit aquireAndRegister(const Node & n, bool atom = false); public: |